WIP: autocorres: refactor rec_callees calculation

tools/autocorres/autocorres_util2.ML

@@ -152,6 +152,35 @@ in
   (ctxt', m, res)
 end
 
+(* Determine which functions are called by a code fragment.
+ * Only function terms in callee_consts are used. *)
+fun get_body_callees
+      (callee_consts: string Termtab.table)
+      (body: term)
+      : symset =
+  Term.fold_aterms (fn t => fn a =>
+      (Termtab.lookup callee_consts t
+          |> Option.map single
+          |> the_default []) @ a)
+      body []
+  |> Symset.make;
+
+(* Determine which recursive calls are actually used by a code fragment.
+ * This is used to make adjustments to recursive function groups
+ * between conversion and definition steps.
+ *
+ * callee_terms is a list of (is_recursive, func const, thm)
+ * as provided by assume_called_functions_corres *)
+fun get_rec_callees
+      (callee_terms: (string * (bool * term * thm)) list)
+      (body: term)
+      : symset = let
+    val callee_lookup =
+          callee_terms |> List.mapPartial (fn (callee, (is_rec, const, _)) =>
+              if is_rec then SOME (const, callee) else NONE)
+          |> Termtab.make;
+    in get_body_callees callee_lookup body end;
+
 (*
  * Given one or more function specs, define them and instantiate corres proofs.
  *

tools/autocorres/heap_lift2.ML

@@ -811,28 +811,16 @@ let
     val _ = Statistics.gather lthy "HLsimp" f
         (Thm.prop_of thm |> HOLogic.dest_Trueprop |> (fn t => Utils.term_nth_arg t 1))
 
+    val f_body = dest_L2Tcorres_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm));
     (* Get actual recursive callees *)
-    val rec_consts =
-          callee_terms |> List.mapPartial (fn (callee, (is_rec, const, _)) =>
-              if is_rec then SOME (const, callee) else NONE)
-          |> Termtab.make;
-    val rec_callees =
-          Term.fold_aterms (fn t => fn a =>
-              (Termtab.lookup rec_consts t
-                  |> Option.map single
-                  |> the_default []) @ a)
-              (dest_L2Tcorres_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm))) []
-            |> Symset.make;
+    val rec_callees = AutoCorresUtil2.get_rec_callees callee_terms f_body;
 
-    (* Generalize the arguments, but not assumed callees *)
-    val thm = Variable.gen_all lthy thm;
-    val fn_body = dest_L2Tcorres_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm));
     (* Return the constants that we fixed. This will be used to process the returned body. *)
     val callee_consts =
           callee_terms |> map (fn (callee, (_, const, _)) => (callee, const)) |> Symtab.make;
   in
-    (fn_body,
-     Morphism.thm export_thm thm, (* Also generalizes callees *)
+    (f_body,
+     Morphism.thm export_thm thm,
      rec_callees,
      callee_consts,
      map dest_Free (measure_var :: arg_frees),

tools/autocorres/local_var_extract2.ML

@@ -1557,28 +1557,18 @@ fun convert
              (betapply (#const f_info, measure_var))
              f_l1_def;
 
-    (* Get actual recursive callees *)
-    val rec_consts =
-          callee_terms |> List.mapPartial (fn (callee, (is_rec, const, _)) =>
-              if is_rec then SOME (const, callee) else NONE)
-          |> Termtab.make;
-    val rec_callees =
-          Term.fold_aterms (fn t => fn a =>
-              (Termtab.lookup rec_consts t
-                  |> Option.map single
-                  |> the_default []) @ a)
-              (dest_L2corres_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm))) []
-            |> Symset.make;
+  val f_body = dest_L2corres_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm));
+  (* Get actual recursive callees *)
+  val rec_callees = AutoCorresUtil2.get_rec_callees callee_terms f_body;
+
+  val _ = @{trace} ("L2 convert thms", Morphism.thm export_thm thm, Morphism.thm export_thm (Variable.gen_all lthy thm));
 
-  (* Generalize the arguments, but not assumed callees *)
-  val thm = Variable.gen_all lthy thm;
-  val fn_body = dest_L2corres_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm));
   (* Return the constants that we fixed. This will be used to process the returned body. *)
   val callee_consts =
         callee_terms |> map (fn (callee, (_, const, _)) => (callee, const)) |> Symtab.make;
   in
-    (fn_body,
-     Morphism.thm export_thm thm, (* Also generalizes callees *)
+    (f_body,
+     Morphism.thm export_thm thm, (* Expose callee assumptions *)
      rec_callees,
      callee_consts,
      dest_Free measure_var :: arg_frees,

tools/autocorres/simpl_conv2.ML

@@ -486,27 +486,15 @@ let
       else get_l1corres_thm prog_info simpl_defs simpl_calls check_termination lthy'' do_opt trace_opt f_name
                             (Symtab.make callee_terms) measure_var;
 
+  val f_body = get_L1corres_monad (HOLogic.dest_Trueprop (Thm.concl_of thm));
   (* Get actual recursive callees *)
-  val rec_consts =
-        callee_terms |> List.mapPartial (fn (callee, (is_rec, const, _)) =>
-            if is_rec then SOME (const, callee) else NONE)
-        |> Termtab.make;
-  val rec_callees =
-        Term.fold_aterms (fn t => fn a =>
-            (Termtab.lookup rec_consts t
-                |> Option.map single
-                |> the_default []) @ a)
-            (get_L1corres_monad (HOLogic.dest_Trueprop (Thm.concl_of thm))) []
-          |> Symset.make;
+  val rec_callees = AutoCorresUtil2.get_rec_callees callee_terms f_body;
 
-  (* Generalize the arguments, but not assumed callees *)
-  val thm = Variable.gen_all lthy thm;
-  val fn_body = get_L1corres_monad (HOLogic.dest_Trueprop (Thm.concl_of thm));
   (* Return the constants that we fixed. This will be used to process the returned body. *)
   val callee_consts =
         callee_terms |> map (fn (callee, (_, const, _)) => (callee, const)) |> Symtab.make;
   in
-     (fn_body,
+     (f_body,
       Morphism.thm export_thm thm, (* Also generalizes callees *)
       rec_callees,
       callee_consts,

tools/autocorres/word_abstract2.ML

@@ -382,38 +382,25 @@ let
           |> HOLogic.dest_Trueprop
           |> (fn t => Utils.term_nth_arg t 3))
 
-    (* Generalize the arguments, but not assumed callees *)
-    val thm = Variable.gen_all lthy thm;
+    (* Convert All-quantified vars in the concrete body to schematics. *)
+    val thm = Variable.gen_all lthy thm
 
     (* Extract the abstract term out of a corresTA thm. *)
-    fun dest_corresWA_term_abs @{term_pat "corresTA _ _ _ ?t _"} = t
-    fun get_body_of_thm thm =
+    fun dest_corresTA_term_abs @{term_pat "corresTA _ _ _ ?t _"} = t
+    val f_body =
         Thm.concl_of thm
         |> HOLogic.dest_Trueprop
-        |> dest_corresWA_term_abs
-    val fn_body = dest_corresWA_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm));
+        |> dest_corresTA_term_abs;
 
     (* Get actual recursive callees *)
-    val rec_consts =
-          callee_terms |> List.mapPartial (fn (callee, (is_rec, const, _)) =>
-              if is_rec then SOME (const, callee) else NONE)
-          |> Termtab.make;
-    val rec_callees =
-          Term.fold_aterms (fn t => fn a =>
-              (Termtab.lookup rec_consts t
-                  |> Option.map single
-                  |> the_default []) @ a)
-              (dest_corresWA_term_abs (HOLogic.dest_Trueprop (Thm.concl_of thm))) []
-            |> Symset.make;
+    val rec_callees = AutoCorresUtil2.get_rec_callees callee_terms f_body;
 
     (* Return the constants that we fixed. This will be used to process the returned body. *)
     val callee_consts =
           callee_terms |> map (fn (callee, (_, const, _)) => (callee, const)) |> Symtab.make;
-
-    val _ = @{trace} ("WA convert", f, Thm.cterm_of lthy fn_body, thm, Morphism.thm export_thm thm);
   in
-    (fn_body,
-     Morphism.thm export_thm thm, (* Also generalizes callees *)
+    (f_body,
+     Morphism.thm export_thm thm,
      rec_callees,
      callee_consts,
      map dest_Free (measure_var :: arg_frees),