Merge pull request #688 from CakeML/issue683

Close issue 683

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 (

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;

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

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,21 @@ 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 (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 ^
+              " 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

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))`