Merge pull request #969 from CakeML/issue-916

Lift out and name monop/binop functions in compute
CakeML · Aug 24, 2023 · f5af8f6 · f5af8f6
2 parents a50a290 + 6ff7f36
commit f5af8f6
Show file tree

Hide file tree

Showing 4 changed files with 144 additions and 17 deletions.
diff --git a/candle/prover/candle_kernelProgScript.sml b/candle/prover/candle_kernelProgScript.sml
@@ -142,10 +142,20 @@ val _ = use_mem_intro := false;
 
 val r = translate compute_default_clock; (* TODO _def *)
 val r = translate indexedListsTheory.findi_def
+val r = translate compute_execTheory.monop_fst_def
+val r = translate compute_execTheory.monop_snd_def
+val r = translate compute_execTheory.monop_ispair_def
 val r = translate compute_execTheory.monop_def
 val r = translate compute_execTheory.to_num_def
 val r = translate compute_execTheory.cv_T_def
 val r = translate compute_execTheory.cv_F_def
+val r = translate compute_execTheory.binop_add_def
+val r = translate compute_execTheory.binop_sub_def
+val r = translate compute_execTheory.binop_mul_def
+val r = translate compute_execTheory.binop_div_def
+val r = translate compute_execTheory.binop_mod_def
+val r = translate compute_execTheory.binop_eq_def
+val r = translate compute_execTheory.binop_less_def
 val r = translate compute_execTheory.binop_def
 val r = translate compute_execTheory.to_ce_def
 val r = translate compute_execTheory.compile_to_ce_def

diff --git a/candle/prover/candle_kernel_permsScript.sml b/candle/prover/candle_kernel_permsScript.sml
@@ -940,13 +940,83 @@ Proof
   \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
 QED
 
+Theorem perms_ok_monop_fst_v[simp]:
+  perms_ok ps monop_fst_v
+Proof
+  rw[perms_ok_def, monop_fst_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_monop_snd_v[simp]:
+  perms_ok ps monop_snd_v
+Proof
+  rw[perms_ok_def, monop_snd_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_monop_ispair_v[simp]:
+  perms_ok ps monop_ispair_v
+Proof
+  rw[perms_ok_def, monop_ispair_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
 Theorem perms_ok_monop_v[simp]:
   perms_ok ps monop_v
 Proof
   rw[perms_ok_def, monop_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
   \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
 QED
 
+Theorem perms_ok_binop_add_v[simp]:
+  perms_ok ps binop_add_v
+Proof
+  rw[perms_ok_def, binop_add_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_binop_sub_v[simp]:
+  perms_ok ps binop_sub_v
+Proof
+  rw[perms_ok_def, binop_sub_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_binop_mul_v[simp]:
+  perms_ok ps binop_mul_v
+Proof
+  rw[perms_ok_def, binop_mul_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_binop_div_v[simp]:
+  perms_ok ps binop_div_v
+Proof
+  rw[perms_ok_def, binop_div_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_binop_mod_v[simp]:
+  perms_ok ps binop_mod_v
+Proof
+  rw[perms_ok_def, binop_mod_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_binop_eq_v[simp]:
+  perms_ok ps binop_eq_v
+Proof
+  rw[perms_ok_def, binop_eq_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
+Theorem perms_ok_binop_less_v[simp]:
+  perms_ok ps binop_less_v
+Proof
+  rw[perms_ok_def, binop_less_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  \\ gs [] \\ pop_assum mp_tac \\ eval_nsLookup_tac \\ rw[]
+QED
+
 Theorem perms_ok_binop_v[simp]:
   perms_ok ps binop_v
 Proof
@@ -1543,3 +1613,4 @@ Theorem evaluate_empty_perms =
   |> SIMP_RULE (srw_ss()) [];
 
 val _ = export_theory ();
+
diff --git a/candle/prover/compute/compute_execProofScript.sml b/candle/prover/compute/compute_execProofScript.sml
@@ -118,7 +118,8 @@ Theorem do_uop_from_cv:
   do_uop uop (from_cv a) s = (M_success (from_cv (monop uop a)),s)
 Proof
   Cases_on ‘uop’ \\ Cases_on ‘a’
-  \\ fs [do_uop_def,monop_def,do_fst_def,do_snd_def,do_ispair_def,st_ex_return_def]
+  \\ fs [do_uop_def,monop_def,do_fst_def,do_snd_def,do_ispair_def,st_ex_return_def,
+         monop_ispair_def,monop_snd_def,monop_fst_def]
 QED
 
 Theorem from_cv_11:
@@ -131,8 +132,9 @@ Theorem do_binop_from_cv:
   do_binop bop (from_cv a) (from_cv b) s = (M_success (from_cv (binop bop a b)),s)
 Proof
   Cases_on ‘bop’ \\ Cases_on ‘a’ \\ Cases_on ‘b’ \\ fs []
-  \\ fs [binop_def,do_binop_def,do_arith_def,st_ex_return_def,
-         SAFEDIV_def,SAFEMOD_def,do_reln_def,cv_T_def,cv_F_def]
+  \\ fs [binop_def,do_binop_def,do_arith_def,st_ex_return_def, SAFEDIV_def,
+         SAFEMOD_def,do_reln_def,cv_T_def,cv_F_def,binop_add_def,binop_sub_def,
+         binop_mul_def,binop_div_def,binop_mod_def,binop_less_def,binop_eq_def]
   \\ rw [] \\ fs [DIV_EQ_X,do_eq_def,st_ex_return_def,from_cv_11]
   \\ rw []
 QED
@@ -445,3 +447,4 @@ Proof
 QED
 
 val _ = export_theory ();
+
diff --git a/candle/prover/compute/compute_execScript.sml b/candle/prover/compute/compute_execScript.sml
@@ -113,10 +113,22 @@ Termination
   \\ rw [] \\ fs []
 End
 
+Definition monop_fst_def:
+  monop_fst = λx. case x of Pair y z => y | _ => Num 0
+End
+
+Definition monop_snd_def:
+  monop_snd = λx. case x of Pair y z => z | _ => Num 0
+End
+
+Definition monop_ispair_def:
+  monop_ispair = λx. case x of Pair y z => Num 1 | _ => Num 0
+End
+
 Definition monop_def:
-  (monop Fst    = λx. case x of Pair y z => y | _ => Num 0) ∧
-  (monop Snd    = λx. case x of Pair y z => z | _ => Num 0) ∧
-  (monop IsPair = λx. case x of Pair y z => Num 1 | _ => Num 0)
+  monop Fst = monop_fst ∧
+  monop Snd = monop_snd ∧
+  monop IsPair = monop_ispair
 End
 
 Definition to_num_def[simp]:
@@ -132,20 +144,50 @@ Definition cv_F_def:
   cv_F = Num 0 : cv
 End
 
+Definition binop_add_def:
+  binop_add = λx y. Num (to_num x + to_num y)
+End
+
+Definition binop_sub_def:
+  binop_sub = λx y. Num (to_num x - to_num y)
+End
+
+Definition binop_mul_def:
+  binop_mul = λx y. Num (to_num x * to_num y)
+End
+
+Definition binop_div_def:
+  binop_div = λx y. Num (let k = to_num y in if k = 0 then 0 else to_num x DIV k)
+End
+
+Definition binop_mod_def:
+  binop_mod =
+    λx y. Num (let k = to_num y in if k = 0 then to_num x else to_num x MOD k)
+End
+
+Definition binop_eq_def:
+  binop_eq = λx y. if x = y then cv_T else cv_F
+End
+
+Definition binop_less_def:
+  binop_less =
+    λx y. case x of
+          | Pair _ _ => cv_F
+          | Num n    => case y of
+                        | Pair _ _ => cv_F
+                        | Num m    => if n < m then cv_T else cv_F
+End
+
 Definition binop_def:
   binop op =
     case op of
-    | Add => (λx y. Num (to_num x + to_num y))
-    | Sub => (λx y. Num (to_num x - to_num y))
-    | Mul => (λx y. Num (to_num x * to_num y))
-    | Div => (λx y. Num (let k = to_num y in if k = 0 then 0 else to_num x DIV k))
-    | Mod => (λx y. Num (let k = to_num y in if k = 0 then to_num x else to_num x MOD k))
-    | Eq   => (λx y. if x = y then cv_T else cv_F)
-    | Less => (λx y. case x of
-                     | Pair _ _ => cv_F
-                     | Num n    => case y of
-                                   | Pair _ _ => cv_F
-                                   | Num m    => if n < m then cv_T else cv_F)
+    | Add => binop_add
+    | Sub => binop_sub
+    | Mul => binop_mul
+    | Div => binop_div
+    | Mod => binop_mod
+    | Eq => binop_eq
+    | Less => binop_less
 End
 
 Definition to_ce_def:
@@ -182,3 +224,4 @@ Definition cv2term_def:
 End
 
 val _ = export_theory ();
+