Merge pull request #1002 from CakeML/to_data_cv

In-logic compilation updated to use cv compute

basis/pure/README.md

@@ -6,6 +6,9 @@ from these by the translator.
 [basisComputeLib.sml](basisComputeLib.sml):
 compset for the pure basis functions.
 
+[basis_cvScript.sml](basis_cvScript.sml):
+Translation of basis types and functions for use with cv_compute.
+
 [mlintScript.sml](mlintScript.sml):
 Pure functions for the Int module.
 

basis/pure/basis_cvScript.sml

@@ -0,0 +1,53 @@
+(*
+  Translation of basis types and functions for use with cv_compute.
+*)
+open preamble cv_transLib cv_stdTheory;
+
+val _ = new_theory "basis_cv";
+
+val _ = cv_memLib.use_long_names := true;
+
+Triviality list_mem[cv_inline] = listTheory.MEM;
+
+val _ = cv_trans sptreeTheory.fromAList_def;
+val _ = cv_trans miscTheory.SmartAppend_def;
+val _ = cv_trans miscTheory.append_aux_def;
+val _ = cv_trans miscTheory.append_def;
+val _ = cv_trans miscTheory.tlookup_def;
+val _ = cv_trans mlstringTheory.implode_def;
+val _ = cv_trans mlstringTheory.explode_thm;
+val _ = cv_trans mlstringTheory.strcat_thm;
+val _ = cv_trans mlstringTheory.str_def;
+val _ = cv_auto_trans mlstringTheory.concat_def;
+val _ = cv_trans miscTheory.list_max_def;
+val _ = cv_trans (miscTheory.max3_def |> PURE_REWRITE_RULE [GREATER_DEF]);
+
+val toChar_pre = cv_trans_pre mlintTheory.toChar_def
+val num_to_chars_pre = cv_auto_trans_pre mlintTheory.num_to_chars_def;
+
+Theorem IMP_toChar_pre:
+  n < 16 ⇒ mlint_toChar_pre n
+Proof
+  gvs [toChar_pre]
+QED
+
+Theorem num_to_chars_pre[cv_pre,local]:
+  ∀a0 a1 a2 a3. mlint_num_to_chars_pre a0 a1 a2 a3
+Proof
+  ho_match_mp_tac mlintTheory.num_to_chars_ind \\ rw []
+  \\ rw [] \\ simp [Once num_to_chars_pre]
+  \\ once_rewrite_tac [toChar_pre] \\ gvs [] \\ rw []
+  \\ ‘k MOD 10 < 10’ by gvs [] \\ simp []
+QED
+
+Triviality Num_ABS:
+  Num (ABS i) = Num i
+Proof
+  Cases_on ‘i’ \\ gvs []
+QED
+
+val _ = cv_trans (mlintTheory.toString_def |> SRULE [Num_ABS]);
+val _ = cv_trans mlintTheory.num_to_str_def;
+
+val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
+val _ = export_theory();

compiler/backend/README.md

@@ -1,5 +1,8 @@
 The CakeML compiler backend.
 
+[San](San):
+A case study for the shared memory feature.
+
 [ag32](ag32):
 This directory contains the Silver-specific part of the compiler
 backend and associated proofs.

compiler/backend/ag32/proofs/ag32_configProofScript.sml

@@ -79,4 +79,63 @@ val ag32_compile_correct =
   |> DISCH_ALL
   |> curry save_thm"ag32_compile_correct";
 
+Theorem get_shmem_info_LENGTH:
+  ∀xs c l1 l2.
+    get_shmem_info xs c l1 l2 = (t1,t2) ∧ LENGTH l1 = LENGTH l2 ⇒
+    LENGTH t1 = LENGTH t2
+Proof
+  ho_match_mp_tac lab_to_targetTheory.get_shmem_info_ind \\ rw []
+  \\ gvs [lab_to_targetTheory.get_shmem_info_def]
+  \\ pairarg_tac \\ gvs []
+QED
+
+Triviality IMP_EVERY_list_add_if_fresh:
+  ∀xs x p. p x ∧ EVERY p xs ⇒ EVERY p (list_add_if_fresh x xs)
+Proof
+  Induct \\ gvs [lab_to_targetTheory.list_add_if_fresh_def] \\ rw []
+QED
+
+Theorem find_ffi_names_ExtCall:
+  ∀xs. EVERY (λx. ∃i. ExtCall i = x) (find_ffi_names xs)
+Proof
+  ho_match_mp_tac lab_to_targetTheory.find_ffi_names_ind
+  \\ rpt strip_tac
+  \\ asm_rewrite_tac [lab_to_targetTheory.find_ffi_names_def,EVERY_DEF]
+  \\ Cases_on ‘x’ \\ gvs []
+  \\ Cases_on ‘a’ \\ gvs []
+  \\ irule IMP_EVERY_list_add_if_fresh \\ gvs []
+QED
+
+Theorem MAP_ExtCall_ffinames:
+  ∀xs.
+    EVERY (λx. ∃i. ExtCall i = x) xs ⇒
+    xs = MAP ExtCall (ffinames_to_string_list xs)
+Proof
+  Induct \\ gvs [backendTheory.ffinames_to_string_list_def]
+  \\ Cases \\ gvs [backendTheory.ffinames_to_string_list_def]
+QED
+
+Theorem compile_imp_ffi_names:
+  backend$compile c p = SOME (b,d,c1) ∧
+  c1.lab_conf.shmem_extra = [] ∧ f ≠ [] ∧
+  c.lab_conf.ffi_names = NONE ∧
+  ffinames_to_string_list (the [] c1.lab_conf.ffi_names) = f ⇒
+  c1.lab_conf.ffi_names = SOME (MAP ExtCall f)
+Proof
+  Cases_on ‘c1.lab_conf.ffi_names’
+  \\ gvs [libTheory.the_def,backendTheory.ffinames_to_string_list_def]
+  \\ gvs [backendTheory.compile_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [oneline backendTheory.attach_bitmaps_def, AllCaseEqs()]
+  \\ strip_tac \\ gvs []
+  \\ gvs [lab_to_targetTheory.compile_def]
+  \\ gvs [lab_to_targetTheory.compile_lab_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [AllCaseEqs()]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ drule get_shmem_info_LENGTH \\ gvs [] \\ rw []
+  \\ irule MAP_ExtCall_ffinames
+  \\ gvs [find_ffi_names_ExtCall]
+QED
+
 val _ = export_theory();

compiler/backend/backendScript.sml

@@ -669,7 +669,6 @@ Proof
        lab_to_targetTheory.shmem_info_num_component_equality]>>fs[]
 QED
 
-
 Theorem inc_config_to_config_inv:
   asm_c = c.lab_conf.asm_conf ==>
   inc_config_to_config asm_c  (config_to_inc_config c) = c
@@ -805,4 +804,58 @@ Proof
   \\ fs [FUN_EQ_THM,FORALL_PROD]
 QED
 
+Definition ffinames_to_string_list_def:
+  (ffinames_to_string_list [] = []) ∧
+  (ffinames_to_string_list ((ExtCall s)::rest) =
+    s::(ffinames_to_string_list rest)) ∧
+  (ffinames_to_string_list ((SharedMem _)::rest) =
+    ffinames_to_string_list rest)
+End
+
+
+Definition inc_set_oracle_def:
+  inc_set_oracle c oracle =
+    c with inc_word_to_word_conf :=
+        (c.inc_word_to_word_conf with col_oracle := oracle)
+End
+
+Definition set_oracle_def:
+  set_oracle c oracle =
+    c with
+    word_to_word_conf := c.word_to_word_conf with col_oracle := oracle
+End
+
+Definition set_asm_conf_def:
+  set_asm_conf c asm_c =
+    c with lab_conf := c.lab_conf with asm_conf := asm_c
+End
+
+Theorem inc_set_oracle_pull:
+  ∀oracle c. inc_config_to_config b (inc_set_oracle c oracle) =
+             set_oracle (inc_config_to_config b c) oracle
+Proof
+  gvs [inc_set_oracle_def,inc_config_to_config_def,set_oracle_def]
+QED
+
+Theorem inc_config_to_config_config_to_inc_config:
+  inc_config_to_config asm_c (config_to_inc_config c) =
+  set_asm_conf c asm_c
+Proof
+  gvs [inc_config_to_config_def,
+       config_to_inc_config_def,
+       lab_to_targetTheory.inc_config_to_config_def,
+       lab_to_targetTheory.config_to_inc_config_def,
+       config_component_equality,
+       lab_to_targetTheory.config_component_equality,
+       set_asm_conf_def]
+QED
+
+Theorem set_asm_conf_id:
+  c.lab_conf.asm_conf = asm_c ⇒
+  set_asm_conf c asm_c = c
+Proof
+  gvs [set_asm_conf_def, fetch "-" "config_component_equality",
+       lab_to_targetTheory.config_component_equality]
+QED
+
 val _ = export_theory();

compiler/backend/bvi_letScript.sml

@@ -42,25 +42,28 @@ open preamble bviTheory;
 
 val _ = new_theory "bvi_let";
 
-val extract_def = Define `
+Definition extract_def:
   (extract ((Var n):bvi$exp) ys = n + LENGTH ys + 1) /\
-  (extract _ _ = 0)`
+  (extract _ _ = 0)
+End
 
-val extract_list_def = Define `
+Definition extract_list_def:
   (extract_list [] = []) /\
-  (extract_list (x::xs) = extract x xs :: extract_list xs)`
+  (extract_list (x::xs) = extract x xs :: extract_list xs)
+End
 
-val delete_var_def = Define `
+Definition delete_var_def:
   (delete_var ((Var n):bvi$exp) = Op (Const 0) []) /\
-  (delete_var x = x)`;
+  (delete_var x = x)
+End
 
 Theorem exp2_size_APPEND:
    !xs ys. exp2_size (xs++ys) = exp2_size xs + exp2_size ys
 Proof
   Induct \\ fs [exp_size_def]
 QED
 
-val compile_def = tDefine "compile" `
+Definition compile_def:
   (compile env d [] = []) /\
   (compile env d (x::y::xs) = compile env d [x] ++ compile env d (y::xs)) /\
   (compile env d [(Var v):bvi$exp] =
@@ -90,14 +93,66 @@ val compile_def = tDefine "compile" `
   (compile env d [Call t dest xs h] =
      [Call t dest (compile env d xs)
          (case h of NONE => NONE
-                  | SOME e => SOME (HD (compile (0::env) d [e])))])`
- (WF_REL_TAC `measure (bvi$exp2_size o SND o SND)`
+                  | SOME e => SOME (HD (compile (0::env) d [e])))])
+Termination
+  WF_REL_TAC `measure (bvi$exp2_size o SND o SND)`
   \\ rw [] \\ fs [LENGTH_NIL]
   \\ imp_res_tac (METIS_PROVE [SNOC_CASES] ``m <> [] ==> ?x y. m = SNOC x y``)
   \\ full_simp_tac std_ss [LAST_SNOC,LENGTH_SNOC,FRONT_SNOC]
-  \\ fs [exp2_size_APPEND,SNOC_APPEND,exp_size_def]);
+  \\ fs [exp2_size_APPEND,SNOC_APPEND,exp_size_def]
+End
 
-val compile_ind = theorem"compile_ind";
+Definition compile_sing_def:
+  (compile_sing env d ((Var v):bvi$exp) =
+     case LLOOKUP env v of
+     | SOME n => Var (v + n)
+     | _ => Var (v + d)) /\
+  (compile_sing env d (If x1 x2 x3) =
+     (If (compile_sing env d x1)
+         (compile_sing env d x2)
+         (compile_sing env d x3))) /\
+  (compile_sing env d (Let xs x2) =
+     let l = LENGTH xs in
+       if l = 0 then compile_sing env d x2 else
+         let k = l-1 in
+           if x2 = Var k then
+             (* moves the last exp into tail-position if the body is a Var *)
+             let ys = compile_list env d (BUTLAST xs) in
+               (Let ys ((compile_sing (MAP ((+)k) env) (d+k) (LAST xs))))
+           else
+             let ys = compile_list env d xs in
+               (Let (MAP delete_var ys)
+                 ((compile_sing (extract_list ys ++ env) d x2)))) /\
+  (compile_sing env d (Raise x1) =
+     (Raise ((compile_sing env d x1)))) /\
+  (compile_sing env d (Op op xs) = (Op op (compile_list env d xs))) /\
+  (compile_sing env d (Tick x) = (Tick (compile_sing env d x))) /\
+  (compile_sing env d (Call t dest xs h) =
+     (Call t dest (compile_list env d xs)
+         (case h of NONE => NONE
+                  | SOME e => SOME ((compile_sing (0::env) d e))))) /\
+  (compile_list env d [] = []) /\
+  (compile_list env d (x::xs) =
+    compile_sing env d x :: compile_list env d xs)
+Termination
+  WF_REL_TAC ‘measure $ λx. case x of
+                            | INL (_,_,e) => bvi$exp_size e
+                            | INR (_,_,es) => bvi$exp2_size es’
+  \\ conj_tac \\ Cases using SNOC_CASES
+  \\ gvs [SNOC_APPEND,exp2_size_APPEND,bviTheory.exp_size_def]
+End
+
+Theorem compile_sing:
+  (∀n d e. compile n d [e] = [compile_sing n d e]) ∧
+  (∀n d e. compile_list n d e = compile n d e)
+Proof
+  ho_match_mp_tac compile_sing_ind \\ rpt strip_tac
+  \\ gvs [compile_sing_def,compile_def]
+  \\ every_case_tac \\ gvs []
+  \\ rename [‘compile n d (e::es)’]
+  \\ Cases_on ‘es’ \\ gvs []
+  \\ gvs [compile_sing_def,compile_def]
+QED
 
 Theorem compile_length[simp]:
    !n d xs. LENGTH (compile n d xs) = LENGTH xs
@@ -114,7 +169,11 @@ Proof
   \\ Cases_on `compile n d [x]` \\ fs [LENGTH_NIL]
 QED
 
-val compile_exp_def = Define `
-  compile_exp x = case compile [] 0 [x] of (y::_) => y | _ => Var 0 (* impossible *)`;
+Definition compile_exp_def:
+  compile_exp x =
+    case compile [] 0 [x] of (y::_) => y | _ => Var 0 (* impossible *)
+End
+
+Theorem compile_exp_eq = compile_exp_def |> SRULE [compile_sing];
 
 val _ = export_theory();