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();