Refactor ml_translatorLib

compiler/bootstrap/translation/caml_lexProgScript.sml

@@ -11,6 +11,7 @@ open preamble caml_lexTheory;
 open parserProgTheory ml_translatorLib ml_translatorTheory;
 
 val _ = translation_extends "parserProg";
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "caml_lexProg");
 
 (* -------------------------------------------------------------------------
  * Translator setup
@@ -157,6 +158,6 @@ val r = translate scan_float_or_int_def;
 val r = translate (caml_lexTheory.next_sym_def |> REWRITE_RULE [GSYM sub_check_def]);
 
 val r = translate caml_lexTheory.lexer_fun_def;
-
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 
 val () = ml_translatorLib.clean_on_exit := true;

compiler/bootstrap/translation/reg_allocProgScript.sml

@@ -20,6 +20,8 @@ open basisProgTheory
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
 val _ = translation_extends "pancake_parseProg";
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "reg_allocProg");
+
 val _ = ml_translatorLib.use_sub_check true;
 (*
 val _ = translation_extends "basisProg";
@@ -451,4 +453,5 @@ val _ = disable_astPP()
 
 *)
 
+val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = (ml_translatorLib.clean_on_exit := true);

translator/alist_tree2Lib.sig

@@ -0,0 +1,52 @@
+(* Code to recall that some partial functions (of type 'a -> 'b option)
+can be represented as sorted alists, and derive a fast conversion on
+applications of those functions. *)
+
+signature alist_tree2Lib = sig
+
+include Abbrev
+
+(* Syntax *)
+val alookup_tm : term;
+val option_choice_tm : term;
+val repr_tm : term;
+
+(* The repr set type *)
+type 'a alist_reprs
+
+(*
+   Representations of partial functions using sorted trees.
+   Requires a relation R and a theorem that shows
+   it is irreflexive and transitive. The destructor maps terms
+   of the domain type to some type that can be sorted in ML.
+   The conversion must prove R x y for any x, y where x is
+   sorted before y by the destructor and comparison.
+*)
+val mk_alist_reprs : thm -> conv -> (term -> 'a)
+    -> (('a * 'a) -> order) -> 'a alist_reprs
+
+(*
+   The representation set contains representations of various
+   partial functions, initially none.
+*)
+val peek_functions_in_rs : 'a alist_reprs -> term list
+
+(*
+   Adds a function's representation.
+
+   Requires a theorem f = rhs with a valid rhs.
+   A valid rhs is:
+     - ALOOKUP xs
+     - a function g in the repr set.
+     - option_choice_f of two valid rhs values
+*)
+val add_alist_repr : 'a alist_reprs -> thm -> unit
+
+(*
+   Converts f x to a concrete value (SOME y/NONE)
+   for functions f in the repr set.
+*)
+val reprs_conv : 'a alist_reprs -> conv
+
+end
+