WIP: autocorres: refactor measureT

tools/autocorres/autocorres_util2.ML

@@ -60,6 +60,9 @@ in
   (Symset.dest (#callees fn_info), Symset.dest (#rec_callees fn_info))
 end
 
+(* Measure variables are currently hardcoded as nats. *)
+val measureT = @{typ nat};
+
 (*
  * Assume theorems for called functions.
  *

tools/autocorres/heap_lift2.ML

@@ -682,7 +682,7 @@ let
 
     (* Fix measure variable. *)
     val ([measure_var_name], lthy) = Variable.variant_fixes ["rec_measure'"] lthy;
-    val measure_var = Free (measure_var_name, LocalVarExtract2.measureT);
+    val measure_var = Free (measure_var_name, AutoCorresUtil2.measureT);
 
   (* Add callee assumptions. *)
     val (lthy, export_thm, callee_terms) =

tools/autocorres/local_var_extract2.ML

@@ -1210,13 +1210,11 @@ in
         (l1_term |> head_of |> PolyML.makestring)
 end
 
-val measureT = @{typ nat};
-
 (* Get the expected type of a function from its name. *)
 fun get_expected_l2_fn_type prog_info l1_infos fn_name =
 let
   val fn_info = the (Symtab.lookup l1_infos fn_name)
-  val fn_params_typ = measureT :: map snd (#args fn_info)
+  val fn_params_typ = AutoCorresUtil2.measureT :: map snd (#args fn_info)
 in
   fn_params_typ ---> mk_l2monadT (#globals_type prog_info) (#return_type fn_info) @{typ unit}
 end
@@ -1408,7 +1406,8 @@ let
    * and this gets annoying pretty quickly. But it is probably unavoidable.
    *)
   val (fn_names, fn_defs) = split_list (Symtab.dest l2_infos);
-  val measure = Free ("rec_measure'", measureT)
+  val ([measure_var_name], lthy) = Variable.variant_fixes ["rec_measure'"] lthy;
+  val measure = Free (measure_var_name, AutoCorresUtil2.measureT)
   fun make_mono_step_stmt current_def =
       let
           (* def should be of the form "func ?locale_args... ?measure ?args... = ..." *)
@@ -1526,7 +1525,7 @@ fun convert
 
   (* Fix measure variable. *)
   val ([measure_var_name], lthy') = Variable.variant_fixes ["rec_measure'"] lthy;
-  val measure_var = Free (measure_var_name, measureT);
+  val measure_var = Free (measure_var_name, AutoCorresUtil2.measureT);
 
   (* Add callee assumptions. Note that our define code has to use the same assumption order. *)
   val (lthy'', export_thm, callee_terms) =
@@ -1590,7 +1589,6 @@ fun define
       : FunctionInfo2.function_info Symtab.table * local_theory = let
   val funcs' = funcs |>
         map (fn (name, def as (body, callee_consts, thm, frees)) =>
-                   (* FIXME: abstract_fn_body should really be moved into define_funcs *)
                    (name, ((AutoCorresUtil2.abstract_fn_body l1_infos (name, def), thm, frees))));
   val (new_thms, (), lthy') =
         AutoCorresUtil2.define_funcs FunctionInfo2.L2 filename l1_infos

tools/autocorres/simpl_conv2.ML

@@ -455,10 +455,8 @@ let
   (* TODO sanity check:
      - all SIMPL defs exist *)
 
-  val measureT = @{typ nat};
-
   (* All L1 functions have the same signature: measure \<Rightarrow> L1_monad *)
-  val l1_fn_type = measureT --> mk_l1monadT (#state_type prog_info);
+  val l1_fn_type = AutoCorresUtil2.measureT --> mk_l1monadT (#state_type prog_info);
 
   (* L1corres for f's callees. *)
   fun get_l1_fn_assumption ctxt fn_name free _ _ measure_var =
@@ -468,7 +466,7 @@ let
 
   (* Fix measure variable. *)
   val ([measure_var_name], lthy') = Variable.variant_fixes ["rec_measure'"] lthy;
-  val measure_var = Free (measure_var_name, measureT);
+  val measure_var = Free (measure_var_name, AutoCorresUtil2.measureT);
 
   (* Add callee assumptions. Note that our define code has to use the same assumption order. *)
   val (lthy'', export_thm, callee_terms) =
@@ -517,11 +515,8 @@ fun define
       (* name, raw body, callee consts, corres thm, arg frees *)
       (funcs: (string * (term * term Symtab.table * thm * (string * typ) list)) list)
       : FunctionInfo2.function_info Symtab.table * local_theory = let
-  (* FIXME: dedup with convert *)
-
   (* All L1 functions have the same signature: measure \<Rightarrow> L1_monad *)
-  val measureT = @{typ nat};
-  val l1_fn_type = measureT --> mk_l1monadT (#state_type prog_info);
+  val l1_fn_type = AutoCorresUtil2.measureT --> mk_l1monadT (#state_type prog_info);
 
   (* L1corres for f's callees. *)
   fun get_l1_fn_assumption ctxt fn_name free _ _ measure_var =

tools/autocorres/type_strengthen2.ML

@@ -320,7 +320,7 @@ let
      * FIXME: recalculate call graph prior to this *)
     val all_arg_names = (if is_recursive then ["rec_measure'"] else []) @
                         map fst (#args fn_info)
-    val all_arg_types = (if is_recursive then [LocalVarExtract2.measureT] else []) @
+    val all_arg_types = (if is_recursive then [AutoCorresUtil2.measureT] else []) @
                         map snd (#args fn_info)
     val (all_arg_names, lthy') = Variable.variant_fixes all_arg_names lthy
     val (measure_param, fn_args) =

tools/autocorres/word_abstract2.ML

@@ -181,7 +181,7 @@ let
 
     (* Fix measure variable. *)
     val ([measure_var_name], lthy) = Variable.variant_fixes ["rec_measure'"] lthy;
-    val measure_var = Free (measure_var_name, LocalVarExtract2.measureT);
+    val measure_var = Free (measure_var_name, AutoCorresUtil2.measureT);
 
     (* Add callee assumptions. *)
     val (lthy, export_thm, callee_terms) =