WIP: autocorres: refactor define_funcs a bit more

tools/autocorres/autocorres_util2.ML

@@ -213,23 +213,27 @@ fun abstract_fn_body
 (*
  * Given one or more function specs, define them and instantiate corres proofs.
  *
- *   "callee_thms" contains a table mapping function names to complete
- *   corres proofs for those functions. At this point, the functions are
- *   still free variables.
+ *   "callee_thms" contains corres theorems for already-defined functions.
  *
  *   "fn_infos" is used to look up function callees. It is expected
  *   to consist of the previous translation output for the functions
  *   being defined, but may of course contain other entries.
  *
- *   "functions" contains a list of (fn_name, (proof, body)).
- *   The body should be of the form generated by gen_corres_for_function,
+ *   "functions" contains a list of (fn_name, (body, corres proof, arg_frees)).
+ *   The body should be of the form generated by abstract_fn_body,
  *   with lambda abstractions for all callees and arguments.
  *
+ *   The given corres proof is expected to use the free variables in
+ *   arg_frees for the function's arguments (including the measure variable,
+ *   if there if there is one). It is also expected to use schematic
+ *   variables for assumed callees.
+ *   (FIXME: this interface should be simplified a bit.)
+ *
  *   We assume that all functions in this list are mutually recursive.
  *   (If not, you should call "define_funcs" multiple times, each
  *   time with a single function.)
  *
- * Returns the new function constants, definitions, corres proofs,
+ * Returns the new function constants, definitions, final corres proofs,
  * and local theory.
  *)
 fun define_funcs
@@ -244,15 +248,19 @@ fun define_funcs
     (ctxt : Proof.context)
     (callee_thms : thm Symtab.table)
     (accum : 'a) (* translate allows an accumulator, but we don't use it here *)
-    (functions : (string * (thm * term)) list)
+    (functions : (string * (term * thm * (string * typ) list)) list)
   : (term * thm * thm) Symtab.table * 'a * Proof.context =
   let
     val fn_names = map fst functions
-    val fn_thms = map (snd #> #1) functions
-    val fn_bodies = map (snd #> #2) functions
+    val fn_bodies = map (snd #> #1) functions
+    (* Generalise over the function arguments *)
+    val fn_thms = map (snd #> (fn (_, thm, frees) =>
+                        (Thm.generalize ([], map fst frees) (Thm.maxidx_of thm + 1) thm)))
+                      functions
 
     val _ = writeln ("Defining (" ^ FunctionInfo2.string_of_phase phase ^ ") " ^
                      (Utils.commas (map get_const_name fn_names)))
+    val _ = @{trace} (Symtab.dest callee_thms, map (apsnd #1) functions)
 
     (*
      * Determine if we are in a recursive case by checking to see if the

tools/autocorres/heap_lift2.ML

@@ -838,9 +838,8 @@ let
         : FunctionInfo2.function_info Symtab.table * local_theory = let
     val funcs' = funcs |>
           map (fn (name, def as (body, callee_consts, thm, frees)) =>
-                     (name, (Thm.generalize ([], map fst frees) (Thm.maxidx_of thm + 1) thm,
-                            AutoCorresUtil2.abstract_fn_body l2_infos (name, def))));
-    val _ = @{trace} ("HL.define", map (fn (name, (thm, body)) => (name, thm, Thm.cterm_of lthy body)) funcs');
+                     (* FIXME: abstract_fn_body should really be moved into define_funcs *)
+                     (name, ((AutoCorresUtil2.abstract_fn_body l2_infos (name, def), thm, frees))));
     val (new_thms, (), lthy') =
           AutoCorresUtil2.define_funcs FunctionInfo2.HL filename l2_infos
               hl_function_name

tools/autocorres/local_var_extract2.ML

@@ -1590,10 +1590,8 @@ fun define
       : FunctionInfo2.function_info Symtab.table * local_theory = let
   val funcs' = funcs |>
         map (fn (name, def as (body, callee_consts, thm, frees)) =>
-                   (name, (* FIXME: define_funcs needs this currently *)
-                          (Thm.generalize ([], map fst frees) (Thm.maxidx_of thm + 1) thm,
-                          AutoCorresUtil2.abstract_fn_body l1_infos (name, def))));
-  val _ = @{trace} ("L2.define", map (fn (name, (thm, body)) => (name, thm, Thm.cterm_of lthy body)) funcs');
+                   (* 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
             l2_function_name

tools/autocorres/simpl_conv2.ML

@@ -530,10 +530,8 @@ fun define
 
   val funcs' = funcs |>
         map (fn (name, def as (body, callee_consts, thm, frees)) =>
-                   (name, (* FIXME: define_funcs needs this currently *)
-                          (Thm.generalize ([], map fst frees) (Thm.maxidx_of thm + 1) thm,
-                          AutoCorresUtil2.abstract_fn_body simpl_defs (name, def))));
-  val _ = @{trace} ("L1.define", map (fn (name, (thm, body)) => (name, thm, Thm.cterm_of lthy body)) funcs');
+                   (* FIXME: abstract_fn_body should really be moved into define_funcs *)
+                   (name, ((AutoCorresUtil2.abstract_fn_body simpl_defs (name, def), thm, frees))));
   val (new_thms, (), lthy') =
         AutoCorresUtil2.define_funcs FunctionInfo2.L1 filename simpl_defs
             l1_function_name (K l1_fn_type) get_l1_fn_assumption (K []) @{thm L1corres_recguard_0}

tools/autocorres/type_strengthen2.ML

@@ -213,7 +213,7 @@ let
   (* Get the newly rewritten term. *)
   val new_term = Thm.concl_of thm_ml |> Utils.rhs_of
 
-  (* Export assumptions. *)
+  (* Export assumptions, converting callees to schematics. *)
   val thm_ml = Morphism.thm m thm_ml
 
   (*val _ = @{trace} (fn_name, #name rule_set, cterm_of (Proof_Context.theory_of ctxt) new_term)*)
@@ -369,7 +369,7 @@ let
   in
     ((make_function_name fn_name, measure_param @ fn_args, term), lthy')
   end
-  (* NB: discard lthy because the same argument vars will be fixed in define_funcs *)
+  (* NB: discard lthy because we don't want the placeholders to be fixed during define_functions *)
   val (input_defs, _) = fold_map gen_fun_def_term (Utils.zip3 fn_names dicts thms) lthy
   val (ts_defs, lthy) = Utils.define_functions input_defs false is_recursive lthy
 

tools/autocorres/word_abstract2.ML

@@ -418,9 +418,8 @@ let
         : FunctionInfo2.function_info Symtab.table * local_theory = let
     val funcs' = funcs |>
           map (fn (name, def as (body, callee_consts, thm, frees)) =>
-                     (name, (Thm.generalize ([], map fst frees) (Thm.maxidx_of thm + 1) thm,
-                            AutoCorresUtil2.abstract_fn_body l2_infos (name, def))));
-    val _ = @{trace} ("WA.define", map (fn (name, (thm, body)) => (name, thm, Thm.cterm_of lthy body)) funcs');
+                     (* FIXME: abstract_fn_body should really be moved into define_funcs *)
+                     (name, ((AutoCorresUtil2.abstract_fn_body l2_infos (name, def), thm, frees))));
     val (new_thms, (), lthy') =
           AutoCorresUtil2.define_funcs FunctionInfo2.WA filename l2_infos
               wa_function_name