Make ml_progLib more space efficient

translator/ml_progLib.sml

@@ -72,11 +72,51 @@ fun cond_abbrev dest conv eval name th = let
        val th = CONV_RULE (conv (REWR_CONV (GSYM def))) th
        in (th,[def]) end end
 
+fun cond_env_abbrev dest conv name th = let
+  val tm = dest th
+  val (x,vs) = strip_comb tm handle HOL_ERR _ => (tm,[])
+  in if is_const x andalso all is_var vs then (th,[])
+     else let
+       val def = define_abbrev false (find_name name) tm |> SPEC_ALL
+       val th = CONV_RULE (conv (REWR_CONV (GSYM def))) th
+       val env_const = def |> concl |> dest_eq |> fst
+       (* compute lookup_var thm *)
+       val v = lookup_var_def |> concl |> dest_forall |> fst
+       val lookup_var_tm =
+         lookup_var_def |> SPECL [v,env_const] |> concl |> dest_eq |> fst
+       val lookup_var_eq = lookup_var_tm |> REWRITE_CONV [def,
+              lookup_var_write,
+              lookup_var_write_mod,
+              lookup_var_write_cons,
+              lookup_var_empty_env,
+              lookup_var_merge_env] |> REWRITE_RULE [lookup_var_def]
+       val var_thm_name = "lookup_var_" ^ fst (dest_const env_const)
+       val _ = save_thm(var_thm_name ^ "[compute]",lookup_var_eq)
+       (* compute lookup_cons thm *)
+       val v = lookup_cons_def |> concl |> dest_forall |> fst
+       val lookup_cons_tm =
+         lookup_cons_def |> SPECL [v,env_const] |> concl |> dest_eq |> fst
+       val lookup_cons_eq = lookup_cons_tm |> REWRITE_CONV [def,
+              lookup_var_write,
+              lookup_var_write_mod,
+              lookup_var_write_cons,
+              lookup_var_empty_env,
+              lookup_var_merge_env] |> REWRITE_RULE [lookup_cons_def]
+       val cons_thm_name = "lookup_cons_" ^ fst (dest_const env_const)
+       val _ = save_thm(cons_thm_name ^ "[compute]",lookup_cons_eq)
+       in (th,[def]) end end
+
+(*
+val (ML_code (ss,envs,vs,th)) = (ML_code (ss,envs,v_def :: vs,th))
+*)
+
 fun clean (ML_code (ss,envs,vs,th)) = let
   val (th,new_ss) = cond_abbrev (rand o concl)
                       RAND_CONV reduce_conv "auto_state" th
-  val (th,new_envs) = cond_abbrev (rand o rator o concl)
-                        (RATOR_CONV o RAND_CONV) EVAL "auto_env" th
+  val dest = (rand o rator o concl)
+  val conv = (RATOR_CONV o RAND_CONV)
+  val name = "auto_env"
+  val (th,new_envs) = cond_env_abbrev dest conv name th
   in ML_code (new_ss @ ss, new_envs @ envs, vs,  th) end
 
 (* --- *)
@@ -143,6 +183,11 @@ fun add_Dlet eval_thm var_str v_thms (ML_code (ss,envs,vs,th)) = let
   val th = th |> SPEC (stringSyntax.fromMLstring var_str)
   in clean (ML_code (ss,envs,v_thms @ vs,th)) end
 
+(*
+val (ML_code (ss,envs,vs,th)) = s
+val (n,v,exp) = (v_tm,w,body)
+*)
+
 fun add_Dlet_Fun n v exp v_name (ML_code (ss,envs,vs,th)) = let
   val th = MATCH_MP ML_code_NONE_Dlet_Fun th
            handle HOL_ERR _ =>
@@ -180,6 +225,10 @@ fun get_mod_prefix (ML_code (ss,envs,vs,th)) = let
        (tm |> rand |> rator |> rand |> stringSyntax.fromHOLstring) ^ "_"
   end
 
+(*
+val dec_tm = dec1_tm
+*)
+
 fun add_dec dec_tm pick_name s =
   if is_Dexn dec_tm then let
     val (x1,x2) = dest_Dexn dec_tm
@@ -281,11 +330,6 @@ fun clean_state (ML_code (ss,envs,vs,th)) = let
 
 (*
 
-val s = init_state
-val dec1_tm = ``Dlet (Pvar "f") (Fun "x" (Var (Short "x")))``
-val dec2_tm = ``Dlet (Pvar "g") (Fun "x" (Var (Short "x")))``
-val prog_tm = ``[Tdec ^dec1_tm; Tdec ^dec2_tm]``
-
 fun pick_name str =
   if str = "<" then "lt" else
   if str = ">" then "gt" else
@@ -299,6 +343,11 @@ fun pick_name str =
   if str = "!" then "deref" else
   if str = ":=" then "update" else str
 
+val s = init_state
+val dec1_tm = ``Dlet (Pvar "f") (Fun "x" (Var (Short "x")))``
+val dec2_tm = ``Dlet (Pvar "g") (Fun "x" (Var (Short "x")))``
+val prog_tm = ``[Tdec ^dec1_tm; Tdec ^dec2_tm]``
+
 val s = (add_prog prog_tm pick_name init_state)
 
 val th = get_env s1

translator/ml_progScript.sml

@@ -627,4 +627,85 @@ val DISJOINT_set_simp = Q.store_thm("DISJOINT_set_simp",
     (DISJOINT (set (x::xs)) s <=> ~(x IN s) /\ DISJOINT (set xs) s)`,
   fs [DISJOINT_DEF,EXTENSION] \\ metis_tac []);
 
+(* lookup function definitions *)
+
+val lookup_var_def = Define `
+  lookup_var name (env:v sem_env) = nsLookup env.v (Short name)`;
+
+val lookup_cons_def = Define `
+  lookup_cons name (env:v sem_env) = nsLookup env.c (Short name)`;
+
+(* theorems about lookup functions *)
+
+val nsLookup_write = Q.store_thm("nsLookup_write",
+  `(nsLookup (write n v env).v (Short name)  =
+       if n = name then SOME v else nsLookup env.v (Short name) ) /\
+   (nsLookup (write n v env).v (Long mn lname)  =
+       nsLookup env.v (Long mn lname))`,
+  fs [write_def] \\ EVAL_TAC \\ rw []);
+
+(* No idea why this is sparated out *)
+val lookup_var_write = Q.store_thm("lookup_var_write",
+  `(lookup_var v (write w x env) = if v = w then SOME x else lookup_var v env) /\
+    (nsLookup (write w x env).v (Short v)  =
+       if v = w then SOME x else nsLookup env.v (Short v) ) /\
+   (nsLookup (write w x env).v (Long mn lname)  =
+       nsLookup env.v (Long mn lname)) ∧
+    (lookup_cons name (write w x env) = lookup_cons name env)`,
+  fs [lookup_var_def,write_def,lookup_cons_def] \\ rw []);
+
+val lookup_var_write_mod = Q.store_thm("lookup_var_write_mod",
+  `(lookup_var v (write_mod mn e1 env) = lookup_var v env) /\
+    (*(lookup_mod m (write_mod mn e1 env) =
+     if m = mn then SOME e1.v else lookup_mod m env) /\*)
+    (lookup_cons name (write_mod mn e1 env) = lookup_cons name env)`,
+  fs [lookup_var_def,write_mod_def,
+      lookup_cons_def] \\ rw [] \\ Cases_on`name` \\ fs[namespacePropsTheory.nsLookup_nsLift_append]);
+ (*fs [lookup_var_id_def,lookup_var_def,write_mod_def,
+      lookup_cons_thm,lookup_mod_def] \\ rw []
+  \\ Cases_on `env.c` \\ fs [] \\ fs [lookup_alist_mod_env_def]);*)
+
+val lookup_var_write_cons = Q.store_thm("lookup_var_write_cons",
+  `(lookup_var v (write_cons n d env) = lookup_var v env) /\
+    (*(lookup_mod m (write_cons n d env) = lookup_mod m env) /\*)
+    (lookup_cons name (write_cons n d env) =
+     if name = n then SOME d else lookup_cons name env)`,
+  fs [lookup_var_def,write_cons_def,lookup_cons_def] \\ rw []);
+  (*
+  fs [lookup_var_id_def,lookup_var_def,write_cons_def,
+      lookup_cons_thm,lookup_mod_def] \\ rw []
+  \\ Cases_on `env.c` \\ fs []
+  \\ fs [lookup_alist_mod_env_def,merge_alist_mod_env_def]);*)
+
+val lookup_var_empty_env = Q.store_thm("lookup_var_empty_env",
+  `(lookup_var v empty_env = NONE) /\
+    (nsLookup empty_env.v (Short k) = NONE) /\
+    (nsLookup empty_env.v (Long mn m) = NONE) /\
+    (lookup_cons name empty_env = NONE)`,
+  fs[lookup_var_def,empty_env_def,lookup_cons_def]);
+  (*fs [lookup_var_id_def,lookup_var_def,empty_env_def,lookup_cons_thm] \\ rw []
+  \\ fs [lookup_alist_mod_env_def]);*)
+
+val lookup_var_merge_env = Q.store_thm("lookup_var_merge_env",
+  `(lookup_var v1 (merge_env e1 e2) =
+       case lookup_var v1 e1 of
+       | NONE => lookup_var v1 e2
+       | res => res) /\
+    (lookup_cons v1 (merge_env e1 e2) =
+       case lookup_cons v1 e1 of
+       | NONE => lookup_cons v1 e2
+       | res => res)
+    (*(lookup_mod v1 (merge_env e1 e2) =
+       case lookup_mod v1 e1 of
+       | NONE => lookup_mod v1 e2
+       | res => res)*)`,
+  fs [lookup_var_def,lookup_cons_def,merge_env_def] \\ rw[] \\ every_case_tac \\
+  fs[namespacePropsTheory.nsLookup_nsAppend_some]
+  >-
+    (Cases_on`nsLookup e2.v (Short v1)`>>
+    fs[namespacePropsTheory.nsLookup_nsAppend_none,namespacePropsTheory.nsLookup_nsAppend_some,namespaceTheory.id_to_mods_def])
+  >>
+    (Cases_on`nsLookup e2.c (Short v1)`>>
+    fs[namespacePropsTheory.nsLookup_nsAppend_none,namespacePropsTheory.nsLookup_nsAppend_some,namespaceTheory.id_to_mods_def]));
+
 val _ = export_theory();

translator/ml_translatorLib.sml

@@ -2491,6 +2491,10 @@ fun move_Eval_conv tm =
     else NO_CONV tm
   end
 
+(*
+val th = D res
+*)
+
 fun clean_assumptions th = let
   val lhs1 = ``nsLookup env name`` (*TODO: Probably want to generate this programmatically instead.. *)
   val pattern1 = mk_eq(lhs1,mk_var("_",type_of lhs1))
@@ -2499,6 +2503,7 @@ fun clean_assumptions th = let
   val lookup_assums = find_terms (fn tm => can (match_term pattern1) tm
                                     orelse can (match_term pattern2) tm) (concl th)
   val lemmas = map EVAL lookup_assums
+
                |> filter (fn th => th |> concl |> rand |> is_const)
   val th = REWRITE_RULE lemmas th
   (* lift EqualityType assumptions out *)

translator/ml_translatorScript.sml

@@ -175,103 +175,6 @@ val Eval_Let = Q.store_thm("Eval_Let",
   rw[Once evaluate_cases,PULL_EXISTS,namespaceTheory.nsOptBind_def] \\
   metis_tac[APPEND_ASSOC]);
 
-val lookup_var_def = Define `
-  lookup_var name (env:v sem_env) = nsLookup env.v (Short name)`;
-
-val lookup_cons_def = Define `
-  lookup_cons name (env:v sem_env) = nsLookup env.c (Short name)`;
-
-(*
-val lookup_mod_def = Define `
-  lookup_mod name env = ALOOKUP env.m name`;
-
-val lookup_cons_thm = Q.store_thm("lookup_cons_thm",
-  `lookup_cons name (env:v sem_env) =
-      lookup_alist_mod_env (Short name) env.c`,
-  Cases_on `env.c`
-  \\ fs [lookup_cons_def,lookup_alist_mod_env_def,SND_ALOOKUP_EQ_ALOOKUP]);
-
-Note: replaced by nsLookup??
-
-val lookup_var_thm = Q.store_thm("lookup_var_thm",
-  `(lookup_var_id (Short v) env = lookup_var v env) /\
-    (lookup_var_id (Long mn v) env =
-       case lookup_mod mn env of
-       | NONE => NONE
-       | SOME env1 => ALOOKUP env1 v)`,
-  fs [lookup_var_id_def,lookup_mod_def,lookup_var_def] \\ CASE_TAC \\ fs []);
-*)
-val nsLookup_write = Q.store_thm("nsLookup_write",
-  `(nsLookup (write n v env).v (Short name)  =
-       if n = name then SOME v else nsLookup env.v (Short name) ) /\
-   (nsLookup (write n v env).v (Long mn lname)  =
-       nsLookup env.v (Long mn lname))`,
-  fs [write_def] \\ EVAL_TAC \\ rw []);
-
-(* No idea why this is sparated out *)
-val lookup_var_write = Q.store_thm("lookup_var_write",
-  `(lookup_var v (write w x env) = if v = w then SOME x else lookup_var v env) /\
-    (nsLookup (write w x env).v (Short v)  =
-       if v = w then SOME x else nsLookup env.v (Short v) ) /\
-   (nsLookup (write w x env).v (Long mn lname)  =
-       nsLookup env.v (Long mn lname)) ∧
-    (lookup_cons name (write w x env) = lookup_cons name env)`,
-  fs [lookup_var_def,write_def,lookup_cons_def] \\ rw []);
-
-val lookup_var_write_mod = Q.store_thm("lookup_var_write_mod",
-  `(lookup_var v (write_mod mn e1 env) = lookup_var v env) /\
-    (*(lookup_mod m (write_mod mn e1 env) =
-     if m = mn then SOME e1.v else lookup_mod m env) /\*)
-    (lookup_cons name (write_mod mn e1 env) = lookup_cons name env)`,
-  fs [lookup_var_def,write_mod_def,
-      lookup_cons_def] \\ rw [] \\ Cases_on`name` \\ fs[namespacePropsTheory.nsLookup_nsLift_append]);
- (*fs [lookup_var_id_def,lookup_var_def,write_mod_def,
-      lookup_cons_thm,lookup_mod_def] \\ rw []
-  \\ Cases_on `env.c` \\ fs [] \\ fs [lookup_alist_mod_env_def]);*)
-
-val lookup_var_write_cons = Q.store_thm("lookup_var_write_mod",
-  `(lookup_var v (write_cons n d env) = lookup_var v env) /\
-    (*(lookup_mod m (write_cons n d env) = lookup_mod m env) /\*)
-    (lookup_cons name (write_cons n d env) =
-     if name = n then SOME d else lookup_cons name env)`,
-  fs [lookup_var_def,write_cons_def,lookup_cons_def] \\ rw []);
-  (*
-  fs [lookup_var_id_def,lookup_var_def,write_cons_def,
-      lookup_cons_thm,lookup_mod_def] \\ rw []
-  \\ Cases_on `env.c` \\ fs []
-  \\ fs [lookup_alist_mod_env_def,merge_alist_mod_env_def]);*)
-
-val lookup_var_empty_env = Q.store_thm("lookup_var_empty_env",
-  `(lookup_var v empty_env = NONE) /\
-    (nsLookup empty_env.v (Short k) = NONE) /\
-    (nsLookup empty_env.v (Long mn m) = NONE) /\
-    (lookup_cons name empty_env = NONE)`,
-  fs[lookup_var_def,empty_env_def,lookup_cons_def]);
-  (*fs [lookup_var_id_def,lookup_var_def,empty_env_def,lookup_cons_thm] \\ rw []
-  \\ fs [lookup_alist_mod_env_def]);*)
-
-val lookup_var_merge_env = Q.store_thm("lookup_var_merge_env",
-  `(lookup_var v1 (merge_env e1 e2) =
-       case lookup_var v1 e1 of
-       | NONE => lookup_var v1 e2
-       | res => res) /\
-    (lookup_cons v1 (merge_env e1 e2) =
-       case lookup_cons v1 e1 of
-       | NONE => lookup_cons v1 e2
-       | res => res)
-    (*(lookup_mod v1 (merge_env e1 e2) =
-       case lookup_mod v1 e1 of
-       | NONE => lookup_mod v1 e2
-       | res => res)*)`,
-  fs [lookup_var_def,lookup_cons_def,merge_env_def] \\ rw[] \\ every_case_tac \\
-  fs[namespacePropsTheory.nsLookup_nsAppend_some]
-  >-
-    (Cases_on`nsLookup e2.v (Short v1)`>>
-    fs[namespacePropsTheory.nsLookup_nsAppend_none,namespacePropsTheory.nsLookup_nsAppend_some,namespaceTheory.id_to_mods_def])
-  >>
-    (Cases_on`nsLookup e2.c (Short v1)`>>
-    fs[namespacePropsTheory.nsLookup_nsAppend_none,namespacePropsTheory.nsLookup_nsAppend_some,namespaceTheory.id_to_mods_def]));
-
 val Eval_Var_Short = Q.store_thm("Eval_Var_Short",
   `P v ==> !name env.
                (nsLookup env.v (Short name) = SOME v) ==>
@@ -1697,17 +1600,6 @@ val Eval_Var = Q.store_thm("Eval_Var",
   >- METIS_TAC[]
   \\ rw[state_component_equality]);
 
-(*
-val LookupEval_def = Define`
-  LookupEval name v P =
-    !env. lookup_var_id name env = SOME v ==>
-          Eval env (Var name) P`;
-    LOOKUP_VAR_def
-    lookup_var_def
-    type_of``semanticPrimitives$lookup``
-    f"lookup_alist"
-*)
-
 val Eval_Fun_Var_intro = Q.store_thm("Eval_Fun_Var_intro",
   `Eval cl_env (Fun n exp) P ==>
    ∀name. LOOKUP_VAR name env (Closure cl_env n exp) ==>
@@ -1721,12 +1613,6 @@ val Eval_Var_LOOKUP_VAR_elim = Q.store_thm("Eval_Var_LOOKUP_VAR_elim",
   \\ qexists_tac`<| v := nsSing name v |>`
   \\ EVAL_TAC);
 
-(*
-val lookup_var_eq_lookup_var_id = Q.store_thm("lookup_var_eq_lookup_var_id",
-  `lookup_var n = lookup_var_id (Short n)`,
-  fs [FUN_EQ_THM] \\ EVAL_TAC \\ fs []);
-*)
-
 val PRECONDITION_T = save_thm("PRECONDITION_T",EVAL ``PRECONDITION T``);
 
 val Eval_constant = Q.store_thm("Eval_constant",

translator/ml_translatorSyntax.sml

@@ -25,10 +25,12 @@ val TRUE  = prim_mk_const{Thy="ml_translator",Name="TRUE"}
 val FALSE = prim_mk_const{Thy="ml_translator",Name="FALSE"}
 
 val binop = HolKernel.syntax_fns2 "ml_translator"
-
 val (TAG,mk_TAG,dest_TAG,is_TAG) = binop "TAG";
 val (PreImp,mk_PreImp,dest_PreImp,is_PreImp) = binop "PreImp";
+
+val binop = HolKernel.syntax_fns2 "ml_prog"
 val (lookup_cons,mk_lookup_cons,dest_lookup_cons,is_lookup_cons) = binop "lookup_cons";
+val (lookup_var,mk_lookup_var,dest_lookup_var,is_lookup_var) = binop "lookup_var";
 
 val (Eval,mk_Eval,dest_Eval,is_Eval) = HolKernel.syntax_fns3 "ml_translator" "Eval";