Merge pull request #375 from CakeML/issue365

Better support for w2w in translator and compiler

compiler/backend/backendComputeLib.sml

@@ -184,7 +184,7 @@ val add_backend_compset = computeLib.extend_compset
     [closLangTheory.pure_def
     ,closLangTheory.pure_op_def
       (* ---- pat_to_clos ---- *)
-    ,pat_to_closTheory.compile_def
+    ,pat_to_closTheory.dest_WordToInt_def
     ,pat_to_closTheory.CopyByteStr_def
     ,pat_to_closTheory.CopyByteAw8_def
     ,pat_to_closTheory.vector_tag_def

compiler/backend/closLangScript.sml

@@ -56,6 +56,7 @@ val _ = Datatype `
      | WordShift word_size shift num
      | WordFromInt
      | WordToInt
+     | WordFromWord bool
      | FP_cmp fp_cmp
      | FP_uop fp_uop
      | FP_bop fp_bop

compiler/backend/data_liveScript.sml

@@ -34,6 +34,7 @@ val is_pure_def = Define `
   (is_pure (WordShift W64 _ _) = F) /\
   (is_pure WordFromInt = F) /\
   (is_pure WordToInt = F) /\
+  (is_pure (WordFromWord b) = F) /\
   (is_pure (FP_uop _) = F) /\
   (is_pure (FP_bop _) = F) /\
   (is_pure ConfigGC = F) /\
@@ -67,6 +68,7 @@ val is_pure_pmatch = Q.store_thm("is_pure_pmatch",`!op.
     | WordShift W64 _ _ => F
     | WordFromInt => F
     | WordToInt => F
+    | WordFromWord b => F
     | FP_uop _ => F
     | FP_bop _ => F
     | ConfigGC => F

compiler/backend/data_spaceScript.sml

@@ -12,10 +12,12 @@ val op_space_req_def = Define `
   (op_space_req (WordShift W64 _ _) _ = 3) /\
   (op_space_req WordFromInt _ = 3) /\
   (op_space_req WordToInt _ = 3) /\
+  (op_space_req (WordFromWord F) _ = 3) /\
   (op_space_req (FP_uop _) v9 = 3) /\
   (op_space_req (FP_bop _) v9 = 3) /\
   (op_space_req _ _ = 0)`;
 
+(*
 val op_space_req_pmatch = Q.store_thm("op_space_req_pmatch",`!op l.
   op_space_req op l =
     case op of
@@ -25,12 +27,14 @@ val op_space_req_pmatch = Q.store_thm("op_space_req_pmatch",`!op l.
     | WordShift W64 _ _ => 3
     | WordFromInt => 3
     | WordToInt => 3
+    | WordFromWord b => (if b then 0 else 3)
     | FP_uop _ => 3
     | FP_bop _ => 3
     | _ => 0`,
   rpt strip_tac
   >> CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV)
   >> every_case_tac >> fs[op_space_req_def]);
+*)
 
 val pMakeSpace_def = Define `
   (pMakeSpace (INL c) = c) /\

compiler/backend/data_to_wordScript.sml

@@ -1342,6 +1342,30 @@ local val assign_quotation = `
                  WordShift64_on_32 sh n;
                  WriteWord64_on_32 c header dest 33 31],l))
        | _ => (Skip,l))
+    | WordFromWord b => (dtcase args of
+      | [v1] =>
+          if b then
+            (list_Seq [Assign 1 (real_addr c (adjust_var v1));
+                       Assign 1 (Load (Op Add [Var 1;
+                         Const (if dimindex (:'a) = 32
+                                then 2w * bytes_in_word else bytes_in_word)]));
+                       Assign 1 (Op And [Var 1; Const 255w]);
+                       Assign (adjust_var dest) (ShiftVar Lsl 1 2)],l)
+          else
+          (let
+             len = if dimindex (:α) < 64 then 2 else 1
+           in
+             dtcase encode_header c 3 len of
+               NONE => (GiveUp,l)
+             | SOME header =>
+                (if len = 1 then
+                   (list_Seq [Assign 3 (Shift Lsr (Var (adjust_var v1)) (Nat 2));
+                              WriteWord64 c header dest 3],l)
+                 else
+                   (list_Seq [Assign 5 (Shift Lsr (Var (adjust_var v1)) (Nat 2));
+                              Assign 3 (Const 0w);
+                              WriteWord64_on_32 c header dest 5 3],l)))
+      | _ => (Skip, l))
     | WordFromInt => (dtcase args of
       | [v1] =>
         let len = if dimindex(:'a) < 64 then 2 else 1 in

compiler/backend/pat_to_closScript.sml

@@ -31,6 +31,27 @@ val checkF = check1
 val CopyByteStr_def = Define`CopyByteStr tra = ^checkT`;
 val CopyByteAw8_def = Define`CopyByteAw8 tra = ^checkF`;
 
+val dest_WordToInt_def = Define `
+  (dest_WordToInt w [App _ op [x]] =
+    (if op = (Op (Op (WordToInt w))) then SOME x else NONE)) /\
+  (dest_WordToInt w _ = NONE)`
+
+val exp_size_def = patLangTheory.exp_size_def
+
+val MEM_exp1_size = prove(
+  ``!es. MEM a es ==> exp_size a < exp1_size es``,
+  Induct_on`es` >> simp[exp_size_def] >>
+  rw[] >> res_tac >> fs[] >> simp[exp_size_def] >>
+  Cases_on`es`>>fs[LENGTH_NIL,exp_size_def] >> simp[] >>
+  Cases_on`t`>>fs[exp_size_def] >> rw[] >> simp[]>>
+  Cases_on`t'`>>fs[exp_size_def] >> rw[] >> simp[]);
+
+val dest_WordToInt_exp_size = prove(
+  ``!w es e. (dest_WordToInt w es = SOME e) ==>
+             exp_size e < exp1_size es``,
+  ho_match_mp_tac (theorem "dest_WordToInt_ind")
+  \\ fs [dest_WordToInt_def] \\ fs [exp_size_def]);
+
 val compile_def = tDefine"compile" `
   (compile (Raise tra e) =
     Raise tra (compile e)) ∧
@@ -107,9 +128,14 @@ val compile_def = tDefine"compile" `
   (compile (App tra (Op (Op Opref)) es) =
     Op tra Ref (REVERSE (MAP compile es))) ∧
   (compile (App tra (Op (Op (WordFromInt W8))) es) =
-      Op (tra§0) Mod ((Op (tra§1) (Const 256) [])::(REVERSE (MAP compile es)))) ∧
+      case dest_WordToInt W64 es of
+      | SOME e => Op tra (WordFromWord T) [compile e]
+      | NONE =>  Op (tra§0) Mod
+          ((Op (tra§1) (Const 256) [])::(REVERSE (MAP compile es)))) ∧
   (compile (App tra (Op (Op (WordFromInt W64))) es) =
-      Op tra WordFromInt (REVERSE (MAP compile es))) ∧
+      case dest_WordToInt W8 es of
+      | SOME e => Op tra (WordFromWord F) [compile e]
+      | NONE => (Op tra WordFromInt (REVERSE (MAP compile es)))) ∧
   (compile (App tra (Op (Op (WordToInt W8))) es) =
     if LENGTH es ≠ 1 then Op tra Sub (REVERSE (MAP compile es)) else
                      compile (HD es)) ∧
@@ -226,11 +252,9 @@ val compile_def = tDefine"compile" `
     WF_REL_TAC `measure exp_size` >>
     simp[exp_size_def] >>
     rpt conj_tac >> rpt gen_tac >>
-    Induct_on`es` >> simp[exp_size_def] >>
-    rw[] >> res_tac >> fs[] >> simp[exp_size_def] >>
-    Cases_on`es`>>fs[LENGTH_NIL,exp_size_def] >> simp[] >>
-    Cases_on`t`>>fs[exp_size_def] >> rw[] >> simp[]>>
-    Cases_on`t'`>>fs[exp_size_def] >> rw[] >> simp[]
+    rw[] >> imp_res_tac MEM_exp1_size >> fs [] >>
+    fs [LENGTH_EQ_NUM_compute,exp_size_def] >>
+    imp_res_tac dest_WordToInt_exp_size >> fs []
   end
 val _ = export_rewrites["compile_def"]
 

compiler/backend/proofs/clos_annotateProofScript.sml

@@ -308,6 +308,9 @@ val do_app_thm = Q.prove(
   THEN1 (* FP_cmp *)
    (fs [do_app_cases_val] \\ rveq \\ fs [PULL_EXISTS]
     \\ rveq \\ fs [v_rel_simp] \\ SRW_TAC [] [])
+  THEN1 (* WordFromWord *)
+   (full_simp_tac(srw_ss())[do_app_def] \\ BasicProvers.EVERY_CASE_TAC \\ full_simp_tac(srw_ss())[]
+    \\ SRW_TAC [] [] \\ full_simp_tac(srw_ss())[v_rel_simp] \\ SRW_TAC [] [])
   THEN1 (* WordToInt *)
    (full_simp_tac(srw_ss())[do_app_def] \\ BasicProvers.EVERY_CASE_TAC \\ full_simp_tac(srw_ss())[]
     \\ SRW_TAC [] [] \\ full_simp_tac(srw_ss())[v_rel_simp] \\ SRW_TAC [] [])

compiler/backend/proofs/clos_callProofScript.sml

@@ -1568,7 +1568,7 @@ val do_app_thm = Q.prove(
    (rw [] \\ fs [do_app_def,state_rel_def] \\ every_case_tac \\ fs []
     \\ rw [] \\ fs [] \\ fs [v_rel_def,Boolv_def] \\ rw []
     \\ imp_res_tac LIST_REL_LENGTH \\ fs [])
-  \\ Cases_on `(?w oo. op = WordOp w oo) \/
+  \\ Cases_on `(?w oo. op = WordOp w oo) \/ (?b. op = WordFromWord b) \/
                op = WordFromInt \/ op = WordToInt \/
                (?w s n. op = WordShift w s n)` THEN1
    (rw [] \\ fs [do_app_def,state_rel_def] \\ every_case_tac \\ fs []

compiler/backend/proofs/data_to_word_assignProofScript.sml

@@ -2005,6 +2005,115 @@ val not_less_zero_int_eq = prove(
   ``~(i < 0:int) <=> ?n. i = &n``,
   Cases_on `i` \\ fs []);
 
+val th = Q.store_thm("assign_WordFromWord",
+  `(?b. op = WordFromWord b) ==> ^assign_thm_goal`,
+  rpt strip_tac \\ drule (evaluate_GiveUp |> GEN_ALL) \\ rw [] \\ fs []
+  \\ `t.termdep <> 0` by fs[]
+  \\ imp_res_tac state_rel_cut_IMP \\ pop_assum mp_tac
+  \\ qpat_x_assum `state_rel c l1 l2 s t [] locs` kall_tac \\ strip_tac
+  \\ imp_res_tac get_vars_IMP_LENGTH
+  \\ Cases_on `b`
+  THEN1
+   (fs[do_app,case_eq_thms]
+    \\ every_case_tac \\ fs[]
+    \\ clean_tac
+    \\ imp_res_tac state_rel_get_vars_IMP
+    \\ fs[LENGTH_EQ_NUM_compute] \\ clean_tac
+    \\ fs[state_rel_thm] \\ eval_tac
+    \\ full_simp_tac std_ss [GSYM APPEND_ASSOC]
+    \\ rpt_drule (memory_rel_get_vars_IMP |> GEN_ALL)
+    \\ strip_tac
+    \\ fs[wordSemTheory.get_vars_def,case_eq_thms]
+    \\ every_case_tac \\ fs[] \\ clean_tac
+    \\ fs[assign_def,good_dimindex_def]
+    \\ rpt_drule memory_rel_Word64_IMP \\ fs [good_dimindex_def]
+    \\ strip_tac
+    \\ fs [list_Seq_def,eq_eval]
+    \\ rpt_drule (get_var_get_real_addr_lemma
+          |> SIMP_RULE std_ss [wordSemTheory.get_var_def,good_dimindex_def])
+    \\ disch_then kall_tac
+    \\ rfs [good_dimindex_def] \\ rfs [WORD_MUL_LSL]
+    \\ once_rewrite_tac [word_exp_set_var_ShiftVar_lemma] \\ fs [eq_eval]
+    \\ fs [adjust_var_11]
+    \\ TRY (conj_tac THEN1 rw [])
+    \\ simp[inter_insert_ODD_adjust_set]
+    \\ full_simp_tac std_ss [GSYM APPEND_ASSOC]
+    \\ match_mp_tac memory_rel_insert
+    \\ fs []
+    \\ qmatch_goalsub_abbrev_tac`Number i,Word sn`
+    \\ qsuff_tac `sn = Smallnum i /\ small_int (:'a) i`
+    \\ TRY (rw [] \\ fs []
+            \\ match_mp_tac IMP_memory_rel_Number  \\ fs [good_dimindex_def])
+    \\ unabbrev_all_tac
+    \\ fs [small_int_def,dimword_def,w2w_def,Smallnum_def]
+    \\ Cases_on `c'` \\ fs [word_extract_n2w]
+    \\ rewrite_tac [LSL_BITWISE]
+    \\ rewrite_tac [WORD_AND_EXP_SUB1 |> Q.SPEC `8` |> SIMP_RULE (srw_ss()) []]
+    \\ fs [WORD_MUL_LSL,word_mul_n2w,dimword_def]
+    \\ fs [bitTheory.BITS_THM]
+    \\ rw [] \\ TRY (match_mp_tac LESS_TRANS \\ qexists_tac `256` \\ fs [])
+    \\ rewrite_tac [GSYM (EVAL ``256n * 16777216``)]
+    \\ rewrite_tac [MATCH_MP MOD_MULT_MOD (DECIDE ``0 < 256n /\ 0 < 16777216n``)])
+  \\ fs[do_app,case_eq_thms]
+  \\ every_case_tac \\ fs[]
+  \\ clean_tac
+  \\ imp_res_tac state_rel_get_vars_IMP
+  \\ fs[LENGTH_EQ_NUM_compute] \\ clean_tac
+  \\ fs[state_rel_thm] \\ eval_tac
+  \\ full_simp_tac std_ss [GSYM APPEND_ASSOC]
+  \\ rpt_drule (memory_rel_get_vars_IMP |> GEN_ALL)
+  \\ strip_tac
+  \\ fs[wordSemTheory.get_vars_def,case_eq_thms]
+  \\ every_case_tac \\ fs[] \\ clean_tac
+  \\ fs[assign_def,some_def] \\ rveq
+  \\ rpt_drule (memory_rel_Number_IMP
+        |> REWRITE_RULE [CONJ_ASSOC]
+        |> ONCE_REWRITE_RULE [CONJ_COMM])
+  \\ strip_tac \\ rveq
+  \\ TOP_CASE_TAC \\ fs [] \\ fs [good_dimindex_def,list_Seq_def] \\ rfs []
+  \\ fs [eq_eval,num_exp_def,word_sh_def,Smallnum_def]
+  \\ qpat_abbrev_tac `ww = _ >>> 2`
+  \\ `ww = n2w (w2n w)` by
+   (unabbrev_all_tac
+    \\ once_rewrite_tac [GSYM w2n_11]
+    \\ rewrite_tac [w2n_lsr]
+    \\ Cases_on `w` \\ fs [dimword_def]
+    \\ once_rewrite_tac [MULT_COMM] \\ fs [MULT_DIV])
+  \\ rveq \\ fs []
+  THEN1
+   (assume_tac (GEN_ALL evaluate_WriteWord64_on_32)
+    \\ SEP_I_TAC "evaluate"
+    \\ pop_assum mp_tac \\ fs [join_env_locals_def]
+    \\ fs [wordSemTheory.get_var_def,lookup_insert]
+    \\ fs [inter_insert_ODD_adjust_set_alt]
+    \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND]
+    \\ disch_then drule
+    \\ disch_then (qspec_then `w2w w` mp_tac)
+    \\ impl_keep_tac THEN1
+     (fs [consume_space_def]
+      \\ Cases_on `w` \\ fs [w2w_def,word_extract_n2w,dimword_def]
+      \\ fs [bitTheory.BITS_THM2,LESS_DIV_EQ_ZERO])
+    \\ strip_tac \\ fs [w2w_def]
+    \\ fs [consume_space_def] \\ rveq \\ fs[]
+    \\ conj_tac THEN1 rw []
+    \\ fs [FAPPLY_FUPDATE_THM])
+  THEN1
+   (assume_tac (GEN_ALL evaluate_WriteWord64)
+    \\ SEP_I_TAC "evaluate"
+    \\ pop_assum mp_tac \\ fs [join_env_locals_def]
+    \\ fs [wordSemTheory.get_var_def,lookup_insert]
+    \\ fs [inter_insert_ODD_adjust_set_alt]
+    \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND]
+    \\ disch_then drule
+    \\ impl_keep_tac THEN1 (fs [consume_space_def])
+    \\ strip_tac \\ fs [w2w_def]
+    \\ fs [consume_space_def] \\ rveq \\ fs[]
+    \\ conj_tac THEN1 rw []
+    \\ fs [FAPPLY_FUPDATE_THM,w2w_def]
+    \\ Cases_on `w` \\ fs [] \\ rfs [dimword_def] \\ fs []
+    \\ match_mp_tac (GEN_ALL memory_rel_less_space)
+    \\ qexists_tac`x.space - 2` \\ fs[]));
+
 val th = Q.store_thm("assign_CopyByte",
   `(?new_flag. op = CopyByte new_flag /\ ¬ new_flag) ==> ^assign_thm_goal`,
   rpt strip_tac \\ drule (evaluate_GiveUp |> GEN_ALL) \\ rw [] \\ fs []