Merge remote-tracking branch 'origin/master' into gh859

CakeML · Jul 4, 2022 · 4cba312 · 4cba312
2 parents efd5fd8 + 187e699
commit 4cba312
Show file tree

Hide file tree

Showing 6 changed files with 181 additions and 84 deletions.
diff --git a/basis/DoubleProgScript.sml b/basis/DoubleProgScript.sml
@@ -24,14 +24,20 @@ val _ = ml_prog_update (add_dec
 
 val _ = ml_prog_update open_local_block;
 
-val _ = ml_prog_update open_local_in_block;
-
 val replaceMLneg_def = Define ‘replaceMLneg x = if x = #"~" then #"-" else x’;
 val _ = translate replaceMLneg_def;
 
 val prepareString_def = Define ‘prepareString (s:mlstring) = translate replaceMLneg s’
 val _ = translate prepareString_def;
 
+val _ = ml_prog_update open_local_in_block;
+
+val _ = append_prog “[Dlet unknown_loc (Pvar "fromWord")
+                        (Fun "v1" (App FpFromWord [Var (Short "v1")]))]”
+
+val _ = append_prog “[Dlet unknown_loc (Pvar "toWord")
+                        (Fun "v1" (App FpToWord [Var (Short "v1")]))]”
+
 val _ = process_topdecs
   `fun fromString s =
     let
@@ -47,7 +53,7 @@ val _ = process_topdecs
       val g = Word8Array.sub iobuff 6;
       val h = Word8Array.sub iobuff 7;
     in
-      Word64.concatAll a b c d e f g h
+      fromWord (Word64.concatAll a b c d e f g h)
     end;` |> append_prog;
 
 val _ = ml_prog_update close_local_blocks;
@@ -82,15 +88,16 @@ val _ = ml_prog_update open_local_in_block;
 val _ = process_topdecs
   `fun toString d =
     let
+      val w = toWord d
       val iobuff = Word8Array.array (256) (Word8.fromInt 0);
-      val _ = Word8Array.update iobuff 0 (byte_0 d);
-      val _ = Word8Array.update iobuff 1 (byte_1 d);
-      val _ = Word8Array.update iobuff 2 (byte_2 d);
-      val _ = Word8Array.update iobuff 3 (byte_3 d);
-      val _ = Word8Array.update iobuff 4 (byte_4 d);
-      val _ = Word8Array.update iobuff 5 (byte_5 d);
-      val _ = Word8Array.update iobuff 6 (byte_6 d);
-      val _ = Word8Array.update iobuff 7 (byte_7 d);
+      val _ = Word8Array.update iobuff 0 (byte_0 w);
+      val _ = Word8Array.update iobuff 1 (byte_1 w);
+      val _ = Word8Array.update iobuff 2 (byte_2 w);
+      val _ = Word8Array.update iobuff 3 (byte_3 w);
+      val _ = Word8Array.update iobuff 4 (byte_4 w);
+      val _ = Word8Array.update iobuff 5 (byte_5 w);
+      val _ = Word8Array.update iobuff 6 (byte_6 w);
+      val _ = Word8Array.update iobuff 7 (byte_7 w);
       val _ = #(double_toString) "" iobuff;
       val n = fst (Option.valOf (Word8Array.findi is_0_byte iobuff));
     in
@@ -100,23 +107,42 @@ val _ = process_topdecs
 val _ = ml_prog_update close_local_blocks;
 
 (* Ternary operations *)
-val _ = trans "fma" ``fp64_mul_add roundTiesToEven``;
+
+val fma = “[Dlet unknown_loc (Pvar "fma")
+  (Fun "v1" (Fun "v2" (Fun "v3" (FpOptimise NoOpt (App (FP_top FP_Fma)
+  [Var (Short "v3"); Var (Short "v1"); Var (Short "v2")])))))]”
+
+val _ = append_prog fma;
 
 (* Binary operations *)
-val _ = trans "+" ``fp64_add roundTiesToEven``;
-val _ = trans "-" ``fp64_sub roundTiesToEven``;
-val _ = trans "*" ``fp64_mul roundTiesToEven``;
-val _ = trans "/" ``fp64_div roundTiesToEven``;
-val _ = trans "<" ``fp64_lessThan``;
-val _ = trans ">" ``fp64_greaterThan``;
-val _ = trans "<=" ``fp64_lessEqual``;
-val _ = trans ">=" ``fp64_greaterEqual``;
-val _ = trans "=" ``fp64_equal``;
+
+fun binop s b = “[Dlet unknown_loc (Pvar ^s)
+  (Fun "v1" (Fun "v2" (FpOptimise NoOpt (App (FP_bop ^b) [Var (Short
+  "v1"); Var (Short "v2")]))))]”
+
+fun cmp s b = “[Dlet unknown_loc (Pvar ^s)
+  (Fun "v1" (Fun "v2" (FpOptimise NoOpt (App (FP_cmp ^b) [Var (Short
+  "v1"); Var (Short "v2")]))))]”
+
+val _ = append_prog $ binop “"+"” “FP_Add”;
+val _ = append_prog $ binop “"-"” “FP_Sub”;
+val _ = append_prog $ binop “"*"” “FP_Mul”;
+val _ = append_prog $ binop “"/"” “FP_Div”;
+
+val _ = append_prog $ cmp “"<"” “FP_Less”;
+val _ = append_prog $ cmp “"<="” “FP_LessEqual”;
+val _ = append_prog $ cmp “">"” “FP_Greater”;
+val _ = append_prog $ cmp “">="” “FP_GreaterEqual”;
+val _ = append_prog $ cmp “"="” “FP_Equal”;
 
 (* Unary operations *)
-val _ = trans "abs" ``fp64_abs``;
-val _ = trans "sqrt" ``fp64_sqrt roundTiesToEven``;
-val _ = trans "~" ``fp64_negate``;
+
+fun monop s b = “[Dlet unknown_loc (Pvar ^s)
+  (Fun "v1" (FpOptimise NoOpt (App (FP_uop ^b) [Var (Short "v1")])))]”
+
+val _ = append_prog $ monop “"abs"” “FP_Abs”;
+val _ = append_prog $ monop “"sqrt"” “FP_Sqrt”;
+val _ = append_prog $ monop “"~"” “FP_Neg”;
 
 val _ = ml_prog_update (close_module NONE);
 

diff --git a/basis/DoubleProofScript.sml b/basis/DoubleProofScript.sml
@@ -61,12 +61,43 @@ Definition string2Double_def:
   string2Double (s:string) (df:doubleFuns) = (df.fromString (explode (prepareString (strlit s))))
 End
 
+Theorem double_fromWord_spec:
+  WORD w v ⇒
+  app (p:'ffi ffi_proj) Double_fromWord_v [v]
+      (emp)
+      (POSTv v. cond (v = FP_WordTree $ Fp_const w))
+Proof
+  xcf_with_def "fromWord" Double_fromWord_v_def
+  \\ gs[cf_fpfromword_def, local_def, emp_def] \\ rpt strip_tac
+  \\ qexists_tac ‘GC’ \\ qexists_tac ‘emp’
+  \\ gs[emp_def, GC_def, set_sepTheory.SEP_EXISTS, set_sepTheory.STAR_def,
+        SPLIT_def, WORD_def, app_fpfromword_def]
+  \\ qexists_tac ‘(λ v. λ h. v = Val $ FP_WordTree $ Fp_const w) *+ GC’
+  \\ rpt conj_tac
+  >- (qexists_tac ‘λ x. T’ \\ gs[])
+  >- (
+    qexists_tac ‘w’ \\ gs[exp2v_def] \\ rpt conj_tac
+    >- EVAL_TAC
+    >- (
+      gs[set_sepTheory.SEP_IMP_def, STARPOST_def, GC_def]
+      \\ rpt strip_tac \\ gs[set_sepTheory.STAR_def]
+      \\ qexists_tac ‘EMPTY’ \\ qexists_tac ‘s’ \\ gs[SPLIT_def, SEP_EXISTS]
+      \\ asm_exists_tac \\ gs[])
+    \\ gs[SEP_IMPPOSTv_inv_def, SEP_IMPPOSTe_def, SEP_IMPPOSTf_def,
+          SEP_IMPPOSTd_def, SEP_IMP_def, STARPOST_def, set_sepTheory.STAR_def])
+  >- (
+    rw[SEP_IMPPOST_def, SEP_IMP_def, POSTv_def, STARPOST_def, POST_def,
+       set_sepTheory.STAR_def]
+    \\ gvs[cond_def, GC_def, SEP_EXISTS, SPLIT_def]
+    \\ qexists_tac ‘λ x. y v'’ \\ gs[])
+QED
+
 Theorem double_fromString_spec:
   ! s sv.
   STRING_TYPE (strlit s) sv ==>
   app (p:'ffi ffi_proj) Double_fromString_v [sv]
     (DoubleIO df)
-    (POSTv v. cond (WORD (string2Double s df) v) * DoubleIO df)
+    (POSTv v. cond (v = FP_WordTree $ Fp_const $ string2Double s df) * DoubleIO df)
 Proof
   xcf_with_def "Double.fromString" Double_fromString_v_def
   \\ reverse (Cases_on `doubleFuns_ok df`)
@@ -75,26 +106,25 @@ Proof
   \\ ntac 3 (xlet_auto >- (fs[] \\ xsimpl))
   \\ rename [`W8ARRAY iobuff`]
   \\ xlet `POSTv v. W8ARRAY iobuff (into_bytes 8 (df.fromString (explode (prepareString (strlit s))))) * DoubleIO df`
-  >- (fs[DoubleIO_def, IOx_def, double_ffi_part_def, IO_def, mk_ffi_next_def]
-      \\ xpull \\ xffi \\ xsimpl
-      \\ fs[STRING_TYPE_def] \\ rveq
-      \\ qexists_tac `MAP (n2w o ORD) (explode (prepareString (strlit s)))` \\ fs[MAP_MAP_o]
-      \\ qexists_tac `emp`
-      \\ xsimpl
-      \\ rewrite_tac [one_one_eq] \\ fs[]
-      \\ conj_tac
-      >- (fs[MAP_CHR_w2n_n2w_ORD_id, STRING_TYPE_def, prepareString_def]
-          \\ gs[STRING_TYPE_def, translate_thm, implode_def])
-      \\ fs[mk_ffi_next_def, ffi_fromString_def]
-      \\ xsimpl
-      \\ rewrite_tac [one_one_eq] \\ fs[MAP_MAP_o, MAP_CHR_w2n_n2w_ORD_id])
-  \\ ntac 8
+  >- (
+    fs[DoubleIO_def, IOx_def, double_ffi_part_def, IO_def, mk_ffi_next_def]
+    \\ xpull \\ xffi \\ xsimpl
+    \\ fs[STRING_TYPE_def] \\ rveq
+    \\ qexists_tac `MAP (n2w o ORD) (explode (prepareString (strlit s)))` \\ fs[MAP_MAP_o]
+    \\ qexists_tac `emp`
+    \\ xsimpl
+    \\ rewrite_tac [one_one_eq] \\ fs[]
+    \\ conj_tac
+    >- (
+      fs[MAP_CHR_w2n_n2w_ORD_id, STRING_TYPE_def, prepareString_def]
+      \\ gs[STRING_TYPE_def, translate_thm, implode_def])
+    \\ fs[mk_ffi_next_def, ffi_fromString_def]
+    \\ xsimpl
+    \\ rewrite_tac [one_one_eq] \\ fs[MAP_MAP_o, MAP_CHR_w2n_n2w_ORD_id])
+  \\ ntac 9
     (xlet_auto
     >- (xsimpl \\ TRY (qexists_tac `df`) \\ fs[into_bytes_len]))
-  \\ xapp
-  \\ xsimpl
-  \\ ntac 8 (asm_exists_tac\\ fs[])
-  \\ rpt strip_tac
+  \\ xapp \\ xsimpl
   \\ Cases_on `df` \\ fs[doubleFuns_ok_def, WORD_def, concat_all_into_bytes_id]
 QED
 
@@ -177,17 +207,48 @@ Proof
   Induct_on `s1` \\ fs[TAKE]
 QED
 
+Theorem double_toWord_spec:
+  v = FP_WordTree fp ⇒
+  app (p:'ffi ffi_proj) Double_toWord_v [v]
+      (emp)
+      (POSTv v. cond (WORD (compress_word fp) v))
+Proof
+  xcf_with_def "toWord" Double_toWord_v_def
+  \\ gs[cf_fptoword_def, local_def, emp_def] \\ rpt strip_tac
+  \\ qexists_tac ‘GC’ \\ qexists_tac ‘emp’
+  \\ gs[emp_def, GC_def, set_sepTheory.SEP_EXISTS, set_sepTheory.STAR_def,
+        SPLIT_def, WORD_def, app_fptoword_def]
+  \\ qexists_tac ‘(λ v. λ h. v = Val $ Litv $ Word64 $ compress_word fp) *+ GC’
+  \\ rpt conj_tac
+  >- (qexists_tac ‘λ x. T’ \\ gs[])
+  >- (
+    qexists_tac ‘fp’ \\ gs[exp2v_def] \\ rpt conj_tac
+    >- EVAL_TAC
+    >- (
+      gs[set_sepTheory.SEP_IMP_def, STARPOST_def, GC_def]
+      \\ rpt strip_tac \\ gs[set_sepTheory.STAR_def]
+      \\ qexists_tac ‘EMPTY’ \\ qexists_tac ‘s’ \\ gs[SPLIT_def, SEP_EXISTS]
+      \\ asm_exists_tac \\ gs[])
+    \\ gs[SEP_IMPPOSTv_inv_def, SEP_IMPPOSTe_def, SEP_IMPPOSTf_def,
+          SEP_IMPPOSTd_def, SEP_IMP_def, STARPOST_def, set_sepTheory.STAR_def])
+  >- (
+    rw[SEP_IMPPOST_def, SEP_IMP_def, POSTv_def, STARPOST_def, POST_def,
+       set_sepTheory.STAR_def]
+    \\ gvs[cond_def, GC_def, SEP_EXISTS, SPLIT_def]
+    \\ qexists_tac ‘λ x. y v'’ \\ gs[])
+QED
+
 Theorem double_toString_spec:
-  ! (w:word64) wv.
-  WORD w wv ==>
-  app (p:'ffi ffi_proj) Double_toString_v [wv]
-    (DoubleIO df)
-    (POSTv v. cond (STRING_TYPE (implode (df.toString w)) v) * DoubleIO df)
+  ! (w:word64) fp.
+    compress_word fp = w ⇒
+    app (p:'ffi ffi_proj) Double_toString_v [FP_WordTree fp]
+        (DoubleIO df)
+        (POSTv v. cond (STRING_TYPE (implode (df.toString w)) v) * DoubleIO df)
 Proof
   xcf_with_def "Double.toString" Double_toString_v_def
   \\ reverse (Cases_on `doubleFuns_ok df`)
   >- (fs[DoubleIO_def] \\ xpull)
-  \\ ntac 18 (xlet_auto >- (fs[] \\ xsimpl))
+  \\ ntac 19 (xlet_auto >- (fs[] \\ xsimpl))
   \\ rename [`W8ARRAY iobuff`]
   \\ fs[concat_all_bytes_i]
   \\ qabbrev_tac `res_str = df.toString w`
@@ -202,42 +263,46 @@ Proof
   \\ qabbrev_tac `final_str = (MAP (n2w o ORD) (res_str ++ [CHR 0]) ++
                     DROP (LENGTH res_str + 1) updBuf):word8 list`
   \\ xlet `POSTv v. W8ARRAY iobuff final_str * DoubleIO df`
-  >- (fs[DoubleIO_def, IOx_def, double_ffi_part_def, IO_def, mk_ffi_next_def]
-      \\ xpull \\ xffi \\ xsimpl
-      \\ qexists_tac `emp`
-      \\ fs [SEP_CLAUSES, one_one_eq]
-      \\ fs [mk_ffi_next_def, ffi_toString_def]
-      \\ unabbrev_all_tac
-      \\ fs [EVAL ``REPLICATE 256 x``]
-      \\ fs [EL_LUPDATE, HD_LUPDATE]
-      \\ fs[concat_all_bytes_i]
-      \\ xsimpl \\ fs[one_one_eq])
+  >- (
+    fs[DoubleIO_def, IOx_def, double_ffi_part_def, IO_def, mk_ffi_next_def]
+    \\ xpull \\ xffi \\ xsimpl
+    \\ qexists_tac `emp`
+    \\ fs [SEP_CLAUSES, one_one_eq]
+    \\ fs [mk_ffi_next_def, ffi_toString_def]
+    \\ unabbrev_all_tac
+    \\ fs [EVAL ``REPLICATE 256 x``]
+    \\ fs [EL_LUPDATE, HD_LUPDATE]
+    \\ fs[concat_all_bytes_i]
+    \\ xsimpl \\ fs[one_one_eq])
   \\ xlet `POSTv v. W8ARRAY iobuff final_str *
           DoubleIO df *
           cond (OPTION_TYPE (PAIR_TYPE NUM WORD8) (findi is_0_byte final_str) v)`
-    >- (xapp \\ xsimpl
-        \\ qexists_tac `is_0_byte` \\ fs[is_0_byte_v_thm])
+    >- (
+      xapp \\ xsimpl
+      \\ qexists_tac `is_0_byte` \\ fs[is_0_byte_v_thm])
   \\ IMP_RES_TAC toString_has_0byte
   \\ first_x_assum (qspecl_then [`w`, `df.toString w`] assume_tac)
   \\ fs[]
   \\ xlet_auto \\ fs[]
-  >- (xsimpl
-      \\ unabbrev_all_tac
-      \\ fs[concat_all_bytes_i])
+  >- (
+    xsimpl
+    \\ unabbrev_all_tac
+    \\ fs[concat_all_bytes_i])
   \\ xlet_auto >- xsimpl
   \\ xapp \\ xsimpl
   \\ once_rewrite_tac [CONJ_COMM] \\ rewrite_tac [GSYM CONJ_ASSOC]
   \\ asm_exists_tac \\ fs[]
   \\ rpt conj_tac
-  >- (rpt strip_tac
-      \\ fs[STRING_TYPE_def, mlstringTheory.implode_def]
-      \\ `findi is_0_byte final_str = SOME (STRLEN (df.toString w), 0w)`
-          by (unabbrev_all_tac \\ fs[])
-      \\ fs[]
-      \\ `TAKE (STRLEN (df.toString w)) final_str = MAP (n2w o ORD) (df.toString w)`
-        by (unabbrev_all_tac \\ fs[concat_all_bytes_i, TAKE_STRLEN_id2])
-      \\ unabbrev_all_tac \\ fs[]
-      \\ fs[MAP_MAP_o, MAP_CHR_w2n_n2w_ORD_id])
+  >- (
+    rpt strip_tac
+    \\ fs[STRING_TYPE_def, mlstringTheory.implode_def]
+    \\ `findi is_0_byte final_str = SOME (STRLEN (df.toString w), 0w)`
+      by (unabbrev_all_tac \\ fs[])
+    \\ fs[]
+    \\ `TAKE (STRLEN (df.toString w)) final_str = MAP (n2w o ORD) (df.toString w)`
+      by (unabbrev_all_tac \\ fs[concat_all_bytes_i, TAKE_STRLEN_id2])
+    \\ unabbrev_all_tac \\ fs[]
+    \\ fs[MAP_MAP_o, MAP_CHR_w2n_n2w_ORD_id])
   \\ unabbrev_all_tac
   \\ fs[]
 QED

diff --git a/candle/prover/candle_kernel_funsScript.sml b/candle/prover/candle_kernel_funsScript.sml
@@ -479,7 +479,7 @@ Proof
     Cases_on ‘th’ \\ gs [THM_TYPE_def, do_opapp_cases])
   \\ rename [‘f ∈ kernel_funs’]
   \\ Cases_on ‘f ∈ { call_type_subst_v; call_freesin_v; call_vfree_in_v;
-                     call_variant_v; vsubst_v; inst_v; trans_v; abs_1_v; eq_mp_v;
+                     call_variant_v; vsubst_v; inst_v; trans_v; abs_v; eq_mp_v;
                      deduct_antisym_rule_v; inst_type_v; inst_1_v; trans_v }’ THEN1
    (gvs []
     \\ qpat_x_assum ‘do_opapp _ = _’ mp_tac
@@ -1974,10 +1974,10 @@ Proof
     \\ irule TERM_IMP_v_ok
     \\ first_assum $ irule_at $ Any
     \\ rw[])
-  \\ Cases_on ‘f = abs_1_v’ \\ gvs [] >- (
-    drule_all_then strip_assume_tac abs_1_v_head \\ gvs[]
+  \\ Cases_on ‘f = abs_v’ \\ gvs [] >- (
+    drule_all_then strip_assume_tac abs_v_head \\ gvs[]
     >- (first_assum $ irule_at Any \\ rw[])
-    \\ assume_tac abs_1_v_thm
+    \\ assume_tac abs_v_thm
     \\ drule_then drule v_ok_TERM_TYPE_HEAD \\ strip_tac
     \\ drule_then drule v_ok_THM_TYPE_HEAD \\ strip_tac
     \\ fs[state_ok_def]

diff --git a/candle/prover/candle_kernel_permsScript.sml b/candle/prover/candle_kernel_permsScript.sml
@@ -995,10 +995,10 @@ Proof
   \\ rw[]
 QED
 
-Theorem perms_ok_abs_1_v[simp]:
-  perms_ok kernel_perms abs_1_v
+Theorem perms_ok_abs_v[simp]:
+  perms_ok kernel_perms abs_v
 Proof
-  rw[perms_ok_def, abs_1_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  rw[perms_ok_def, abs_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
   \\ pop_assum mp_tac \\ eval_nsLookup_tac
   \\ rw[]
 QED

diff --git a/candle/prover/candle_kernel_valsScript.sml b/candle/prover/candle_kernel_valsScript.sml
@@ -68,7 +68,7 @@ Definition kernel_funs_def:
     refl_v;
     trans_v;
     mk_comb_1_v;
-    abs_1_v;
+    abs_v;
     beta_v;
     assume_v;
     eq_mp_v;
@@ -91,9 +91,11 @@ Theorem kernel_funs_v_def =
   |> filter (fn tm => not (mem (fst (dest_const tm)) ["INSERT","EMPTY"]))
   |> map (fn c => DB.find (fst (dest_const c) ^ "_def"))
   |> map (fn t => hd t |> snd |> fst)
-  |> curry (op @) [constants_v_def]
+  |> curry (op @) [constants_v_def,abs_v_def]
   |> LIST_CONJ;
 
+Theorem abs_v_def[compute] = abs_v_def;
+
 Definition kernel_locs_def:
   kernel_locs =
     { l | Loc l ∈ { the_type_constants
@@ -1362,8 +1364,8 @@ Proof
   prove_head_tac
 QED
 
-Theorem abs_1_v_head:
-  do_partial_app abs_1_v v = SOME g ∧
+Theorem abs_v_head:
+  do_partial_app abs_v v = SOME g ∧
   do_opapp [g; w] = SOME (env, exp) ∧
   evaluate ^s env [exp] = (s', res) ⇒
     ^safe_error_goal ∨