Move register_type into Map structure

CakeML · Aug 19, 2018 · de7418a · de7418a
1 parent 0d54e74
commit de7418a
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 8 deletions.
diff --git a/basis/MapProgScript.sml b/basis/MapProgScript.sml
@@ -6,14 +6,12 @@ val _ = new_theory "MapProg"
 
 val _ = translation_extends "CompareProg";
 
-(* TODO: move this definition below open_module once the translater
-         has better support for defining datatypes inside modules. *)
+val _ = ml_prog_update (open_module "Map");
+
 val _ = (use_full_type_names := false);
 val _ = register_type ``:('a,'b) balanced_map$balanced_map``;
 val _ = (use_full_type_names := true);
 
-val _ = ml_prog_update (open_module "Map");
-
 val _ = next_ml_names := ["size", "singleton"];
 val _ = translate size_def;
 val _ = translate singleton_def;

diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
@@ -152,8 +152,8 @@ local
                             thm (* certificate: Eval env exp (P tm) *)) list);
   val prog_state = ref ml_progLib.init_state;
   val cons_name_state = ref ([] : (string  *       (* %%thy%%type%%ctor *)
-                                (term *         (* constructor name  *)
-                                 string option) (* module name       *)) list);
+                                  (term *         (* constructor name  *)
+                                   string option) (* module name       *)) list);
 in
   fun get_ml_name (_:string,nm:string,_:term,_:thm,_:thm,_:string option) = nm
   fun get_const (_:string,_:string,tm:term,_:thm,_:thm,_:string option) = tm
@@ -163,8 +163,7 @@ in
   fun v_thms_reset () =
     (v_thms := [];
      eval_thms := [];
-     prog_state := ml_progLib.init_state
-     (* cons_name_state := []; *) (* TODO ?? *));
+     prog_state := ml_progLib.init_state);
   fun ml_prog_update f = (prog_state := f (!prog_state));
   fun get_ml_prog_state () = (!prog_state)
   fun get_curr_env () = get_env (!prog_state);