From 0fa2cdf5bf93e7bb6a4392cb8acb72c4619d6ef5 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sat, 7 Sep 2019 12:32:29 +0200 Subject: [PATCH 1/3] Make translator remove unreachable v thms Progress on #683 --- translator/ml_translatorLib.sig | 2 ++ translator/ml_translatorLib.sml | 38 +++++++++++++++++++--- translator/ml_translator_testScript.sml | 42 +++++++++++++++++++++++++ 3 files changed, 78 insertions(+), 4 deletions(-) diff --git a/translator/ml_translatorLib.sig b/translator/ml_translatorLib.sig index bdba6bd8f8..4cee243f08 100644 --- a/translator/ml_translatorLib.sig +++ b/translator/ml_translatorLib.sig @@ -122,6 +122,8 @@ sig val lookup_v_thm : term -> thm val get_v_thms_ref : unit -> (string * string * term * thm * thm * string list) list ref val remove_Eq_from_v_thm : thm -> thm + val clean_v_thms : unit -> unit + val filter_v_thms : ((string * string * term * thm * thm * string list) -> bool) -> int (* Internal - handling type constructor names *) val mk_cons_name : term -> string diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index 8f4cf577a9..99a3330105 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -46,12 +46,17 @@ exception NotFoundVThm of term; local val use_string_type_ref = ref false; + val finalise_function = ref (I:unit -> unit); in fun use_string_type b = (use_string_type_ref := b; if b then print "Translator now treats `char list` as a CakeML string.\n" else print "Translator now treats `char list` as a list of characters in CakeML.\n"); fun use_hol_string_type () = !use_string_type_ref + fun add_finalise_function f = let + val old_f = !finalise_function + in (finalise_function := (fn () => (old_f (); f ()))) end + fun run_finalise_function () = (!finalise_function) () end (* / non-persistent state *) @@ -223,6 +228,11 @@ in val _ = if Teq (concl pre_def) then () else (print ("\nWARNING: " ^ml_name^" has a precondition.\n\n")) in (v_thms := (name,ml_name,tm,th,pre_def,modules) :: (!v_thms)) end; + fun filter_v_thms f = let + val xs = (!v_thms) + val ys = filter f xs + val _ = (v_thms := ys) + in length xs - length ys end (* if the order didn't matter... fun replace_v_thm c th = let val (found_v_thms,left_v_thms) = partition (same_const c o get_const) (!v_thms) @@ -828,6 +838,7 @@ in fun finalise_translation () = if !finalised then () else let val _ = (finalised := true) + val _ = run_finalise_function () val _ = pack_state () val _ = print_translation_output () in () end @@ -3018,9 +3029,10 @@ fun move_Eval_conv tm = (* val th = D res +val be_quiet = true *) -fun clean_assumptions th = let +fun clean_assumptions_aux be_quiet th = let val start = start_timing "clean assumptions" val lhs1 = get_term "nsLookup_pat" val pattern1 = mk_eq(lhs1,mk_var("_",type_of lhs1)) @@ -3032,9 +3044,10 @@ fun clean_assumptions th = let |> filter (fn th => th |> concl |> rand |> is_const) val _ = case List.find (fn l => Feq (l |> concl |> rand)) lemmas of NONE => () - | SOME t => (print "clean_assumptions: false assumption\n\n"; - print_thm t; print "\n\n"; failwith ("clean_assumptions: false" - ^ Parse.thm_to_string t)) + | SOME t => ((if be_quiet then () else + (print "clean_assumptions: false assumption\n\n"; + print_thm t; print "\n\n")) ; + failwith ("clean_assumptions: false" ^ Parse.thm_to_string t)) val th = REWRITE_RULE lemmas th (* lift EqualityType assumptions out *) val pattern = get_term "eq type" @@ -3055,6 +3068,9 @@ fun clean_assumptions th = let val _ = end_timing start in th end; +fun clean_assumptions th = clean_assumptions_aux false th; +fun clean_assumptions_quietly th = clean_assumptions_aux true th; + fun get_pre_var lhs fname = let fun list_mk_type [] ret_ty = ret_ty | list_mk_type (x::xs) ret_ty = mk_type("fun",[type_of x,list_mk_type xs ret_ty]) @@ -4594,6 +4610,20 @@ val state = state' *) +(* + val xs = get_v_thms () + val (_,_,c_tm,_,_,_) = hd (tl (get_v_thms ())) +*) +fun clean_v_thms () = let + val inst_env = INST [env_tm |-> get_curr_env()] + fun can_lookup_constant (_,_,c_tm,_,_,_) = + can clean_assumptions_quietly (D (inst_env (hol2deep c_tm))) + val delete_count = filter_v_thms can_lookup_constant + in if delete_count < 1 then () else + print ("Removed " ^ int_to_string delete_count ^ + " unreachable v thms from translator's state.\n") end; +val _ = add_finalise_function clean_v_thms; + fun mlDefine q = let val def = Define q val th = translate def diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml index 02362c027a..d57d9b00b5 100644 --- a/translator/ml_translator_testScript.sml +++ b/translator/ml_translator_testScript.sml @@ -10,6 +10,47 @@ val _ = new_theory "ml_translator_test"; open listTheory pairTheory ml_translatorLib ml_translatorTheory; open ml_progLib; +(* test hiding of functions in local .. in .. end *) + +fun def_of_const tm = let + val res = dest_thy_const tm handle HOL_ERR _ => + failwith ("Unable to translate: " ^ term_to_string tm) + val name = (#Name res) + fun def_from_thy thy name = + DB.fetch thy (name ^ "_pmatch") handle HOL_ERR _ => + DB.fetch thy (name ^ "_def") handle HOL_ERR _ => + DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ => + DB.fetch thy name + val def = def_from_thy (#Thy res) name handle HOL_ERR _ => + failwith ("Unable to find definition of " ^ name) + in def end; + +val _ = (find_def_for_const := def_of_const); + +Definition hidden_def: + hidden x = x + 5:num +End + +Definition uses_hidden1_def: + uses_hidden1 x = hidden x +End + +Definition uses_hidden2_def: + uses_hidden2 x = hidden x * uses_hidden1 x +End + +val _ = ml_prog_update open_local_block; +val _ = translate hidden_def; +val _ = ml_prog_update open_local_in_block; +val _ = translate uses_hidden1_def; +val _ = ml_prog_update close_local_blocks; +val _ = clean_v_thms () (* <-- this makes the translator realise that hidden + needs to be retranslated; clean_v_thms runs + automatically on theory export *) +val _ = translate uses_hidden2_def; + +(* test side conditions *) + val ZIP2_def = Define ` (ZIP2 ([],[]) z = []) /\ (ZIP2 (x::xs,y::ys) z = (x,y) :: ZIP2 (xs, ys) (5:int))` @@ -395,4 +436,5 @@ val res = translate TAKE_def; val res = translate DROP_def; val res = translate chop_str_def +val _ = filter_v_thms (fn (n,_,_,_,_,_) => not (String.isPrefix "test" n)); val _ = export_theory(); From 26f4bae8dd00abd7a5ed6212dd12cda0d3d99af5 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sat, 7 Sep 2019 12:33:16 +0200 Subject: [PATCH 2/3] Fix name changes due to previous commit Closes #683 --- basis/StringProgScript.sml | 4 ++-- basis/VectorProgScript.sml | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/basis/StringProgScript.sml b/basis/StringProgScript.sml index 8491b15b6f..2462d8b060 100644 --- a/basis/StringProgScript.sml +++ b/basis/StringProgScript.sml @@ -174,7 +174,7 @@ val _ = translate mlstring_gt_def; val _ = ml_prog_update open_local_block; val result = translate collate_aux_def; -val collate_aux_side_def = theorem"collate_aux_1_side_def"; +val collate_aux_side_def = theorem"collate_aux_side_def"; val _ = ml_prog_update open_local_in_block; val _ = next_ml_names := ["collate"]; @@ -185,7 +185,7 @@ val collate_aux_side_thm = Q.prove ( `!f s1 s2 ord n len. (n + len = if strlen s1 < strlen s2 then strlen s1 - else strlen s2) ==> collate_aux_1_side f s1 s2 ord n len`, + else strlen s2) ==> collate_aux_side f s1 s2 ord n len`, Induct_on `len` \\ rw [Once collate_aux_side_def]); val collate_side_thm = Q.prove ( diff --git a/basis/VectorProgScript.sml b/basis/VectorProgScript.sml index 341ac6758f..5ca88b7d5e 100644 --- a/basis/VectorProgScript.sml +++ b/basis/VectorProgScript.sml @@ -51,20 +51,20 @@ val result = translate mapi_def; val _ = ml_prog_update open_local_block; val result = translate foldli_aux_def; -val foldli_aux_1_side_def = theorem"foldli_aux_1_side_def" +val foldli_aux_side_def = theorem"foldli_aux_side_def" val _ = ml_prog_update open_local_in_block; val _ = next_ml_names := ["foldli"]; val result = translate foldli_def; val foldli_side_def = definition"foldli_side_def"; -val foldli_aux_1_side_thm = Q.prove( - `!f e vec n len. n + len = length vec ==> foldli_aux_1_side f e vec n len`, - Induct_on`len` \\ rw[Once foldli_aux_1_side_def]); +val foldli_aux_side_thm = Q.prove( + `!f e vec n len. n + len = length vec ==> foldli_aux_side f e vec n len`, + Induct_on`len` \\ rw[Once foldli_aux_side_def]); val foldli_side_thm = Q.prove( `foldli_side f e vec`, - rw[foldli_side_def,foldli_aux_1_side_thm]) |> update_precondition; + rw[foldli_side_def,foldli_aux_side_thm]) |> update_precondition; val _ = ml_prog_update open_local_block; val result = translate foldl_aux_def; From a8e2240b45c8f858615a65f130198101bb07e6b6 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sat, 7 Sep 2019 21:55:11 +0200 Subject: [PATCH 3/3] Remove a bug from ml_translatorLib.clean_v_thms --- translator/ml_translatorLib.sml | 3 ++- translator/ml_translator_testScript.sml | 1 - 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index 99a3330105..9b3494caae 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -4617,7 +4617,8 @@ val state = state' fun clean_v_thms () = let val inst_env = INST [env_tm |-> get_curr_env()] fun can_lookup_constant (_,_,c_tm,_,_,_) = - can clean_assumptions_quietly (D (inst_env (hol2deep c_tm))) + ((can clean_assumptions_quietly (D (inst_env (lookup_v_thm c_tm)))) + handle Interrupt => raise Interrupt | _ => false) val delete_count = filter_v_thms can_lookup_constant in if delete_count < 1 then () else print ("Removed " ^ int_to_string delete_count ^ diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml index d57d9b00b5..c1fe51a861 100644 --- a/translator/ml_translator_testScript.sml +++ b/translator/ml_translator_testScript.sml @@ -436,5 +436,4 @@ val res = translate TAKE_def; val res = translate DROP_def; val res = translate chop_str_def -val _ = filter_v_thms (fn (n,_,_,_,_,_) => not (String.isPrefix "test" n)); val _ = export_theory();