WIP: autocorres: restore incremental translation behaviour
The incremental translation demo in crefine has not been updated yet.
This commit is contained in:
Japheth Lim
parent
1ad6d39192
commit
1181b9bc1f
|
|
@ -380,13 +380,17 @@ let
|
|||
val _ = if not (isSome existing_phases) then () else
|
||||
tracing ("Attempting to restart from previous translation of " ^ filename)
|
||||
|
||||
fun get_existing_phase phase =
|
||||
fun get_existing_optional_phase phase =
|
||||
case existing_phases of
|
||||
NONE => Symtab.empty
|
||||
| SOME phases =>
|
||||
case FunctionInfo2.Phasetab.lookup phases phase of
|
||||
NONE => Symtab.empty
|
||||
| SOME infos => infos
|
||||
NONE => SOME Symtab.empty
|
||||
| SOME phases => FunctionInfo2.Phasetab.lookup phases phase
|
||||
fun get_existing_phase phase =
|
||||
Option.getOpt (get_existing_optional_phase phase, Symtab.empty)
|
||||
(* FIXME: if skip_heap_abs or skip_word_abs are used for some parts of
|
||||
* an incremental translation, some functions will be missing.
|
||||
* We ought to either handle this nicely (by carrying the
|
||||
* L2/HL versions forward), or detect it early and
|
||||
* produce an error report. *)
|
||||
val [existing_simpl_info,
|
||||
existing_l1_info,
|
||||
existing_l2_info,
|
||||
|
|
@ -581,11 +585,14 @@ let
|
|||
(* FIXME: collect from existing_phases *)
|
||||
val l1_results =
|
||||
SimplConv2.translate
|
||||
filename prog_info simpl_info (!(#no_c_termination opt) <> SOME true)
|
||||
filename prog_info simpl_info existing_simpl_info existing_l1_info
|
||||
(!(#no_c_termination opt) <> SOME true)
|
||||
do_opt trace_opt (prefix "l1_" o make_function_name) lthy
|
||||
|
||||
val l2_results =
|
||||
LocalVarExtract2.translate filename prog_info l1_results do_opt trace_opt (prefix "l2_" o make_function_name)
|
||||
LocalVarExtract2.translate
|
||||
filename prog_info l1_results existing_l1_info existing_l2_info
|
||||
do_opt trace_opt (prefix "l2_" o make_function_name)
|
||||
|
||||
val skip_heap_abs = !(#skip_heap_abs opt) = SOME true
|
||||
val hl_results =
|
||||
|
|
@ -595,10 +602,10 @@ let
|
|||
val (l2_results', HL_setup) =
|
||||
HeapLift2.prepare_heap_lift
|
||||
filename prog_info l2_results lthy all_simpl_info
|
||||
make_lifted_globals_field_name gen_word_heaps heap_abs_syntax
|
||||
make_lifted_globals_field_name gen_word_heaps heap_abs_syntax;
|
||||
in HeapLift2.translate
|
||||
filename prog_info l2_results' HL_setup
|
||||
no_heap_abs force_heap_abs
|
||||
filename prog_info l2_results' existing_l2_info existing_hl_info
|
||||
HL_setup no_heap_abs force_heap_abs
|
||||
heap_abs_syntax keep_going
|
||||
(these (!(#trace_heap_lift opt))) do_opt trace_opt
|
||||
(prefix "hl_" o make_function_name)
|
||||
|
|
@ -608,15 +615,16 @@ let
|
|||
if skip_word_abs
|
||||
then hl_results
|
||||
else WordAbstract2.translate
|
||||
filename prog_info hl_results
|
||||
filename prog_info hl_results existing_hl_info existing_wa_info
|
||||
unsigned_word_abs no_signed_word_abs
|
||||
(these (!(#trace_word_abs opt))) do_opt trace_opt
|
||||
(prefix "wa_" o make_function_name)
|
||||
|
||||
val ts_results =
|
||||
TypeStrengthen2.translate
|
||||
ts_rules ts_force filename prog_info wa_results make_function_name
|
||||
keep_going do_opt
|
||||
ts_rules ts_force filename prog_info
|
||||
wa_results existing_wa_info existing_ts_info
|
||||
make_function_name keep_going do_opt
|
||||
|
||||
(* Collect final translation results. *)
|
||||
val l1_info = FSeq.list_of l1_results |> map snd |> Utils.symtab_merge false;
|
||||
|
|
@ -665,14 +673,22 @@ let
|
|||
(* FIXME: merge with existing_phases *)
|
||||
|
||||
(* Save function info for future reference. *)
|
||||
val simpl_info' = Symtab.merge (K false) (existing_simpl_info, simpl_info);
|
||||
val l1_info' = Symtab.merge (K false) (existing_l1_info, l1_info);
|
||||
val l2_info' = Symtab.merge (K false) (existing_l2_info, l2_info);
|
||||
val hl_info' = Symtab.merge (K false) (existing_hl_info, hl_info);
|
||||
val wa_info' = Symtab.merge (K false) (existing_wa_info, wa_info);
|
||||
val ts_info' = Symtab.merge (K false) (existing_ts_info, ts_info);
|
||||
val new_results =
|
||||
FunctionInfo2.Phasetab.make
|
||||
([(FunctionInfo2.CP, simpl_info),
|
||||
(FunctionInfo2.L1, l1_info),
|
||||
(FunctionInfo2.L2, l2_info),
|
||||
(FunctionInfo2.TS, ts_info)]
|
||||
@ (if skip_heap_abs then [] else [(FunctionInfo2.HL, hl_info)])
|
||||
@ (if skip_word_abs then [] else [(FunctionInfo2.WA, wa_info)])
|
||||
([(FunctionInfo2.CP, simpl_info'),
|
||||
(FunctionInfo2.L1, l1_info'),
|
||||
(FunctionInfo2.L2, l2_info'),
|
||||
(FunctionInfo2.TS, ts_info')]
|
||||
@ (if skip_heap_abs andalso Symtab.is_empty existing_hl_info
|
||||
then [] else [(FunctionInfo2.HL, hl_info')])
|
||||
@ (if skip_word_abs andalso Symtab.is_empty existing_wa_info
|
||||
then [] else [(FunctionInfo2.WA, wa_info')])
|
||||
)
|
||||
|
||||
val _ = tracing "Saving function info to AutoCorresFunctionInfo."
|
||||
|
|
|
|||
|
|
@ -401,6 +401,24 @@ fun define_funcs
|
|||
(results, accum, ctxt)
|
||||
end
|
||||
|
||||
(* Support function for incremental translation.
|
||||
* This updates #callees of the functions we are translating, to include
|
||||
* background functions that have already been translated.
|
||||
* (We don't need to handle #rec_callees because recursive groups
|
||||
* cannot be translated piecemeal.) *)
|
||||
fun add_background_callees
|
||||
(background: FunctionInfo2.function_info Symtab.table)
|
||||
: FunctionInfo2.function_info Symtab.table ->
|
||||
FunctionInfo2.function_info Symtab.table = let
|
||||
val bg_consts =
|
||||
Symtab.dest background
|
||||
|> map (fn (f, bg_info) => (#raw_const bg_info, f))
|
||||
|> Termtab.make;
|
||||
in Symtab.map (K (fn fn_info => let
|
||||
val bg_callees = get_body_callees bg_consts (Thm.prop_of (#definition fn_info));
|
||||
in FunctionInfo2.function_info_upd_callees (Symset.union (#callees fn_info) bg_callees) fn_info end))
|
||||
end;
|
||||
|
||||
(* Utility for doing conversions in parallel.
|
||||
* The conversion of each function f should depend only on the previous
|
||||
* define phase for f (which necessarily also includes f's callees). *)
|
||||
|
|
@ -413,9 +431,12 @@ type convert_result = {
|
|||
traces: (string * AutoCorresData.Trace) list (* traces *)
|
||||
}
|
||||
fun par_convert
|
||||
(* Worker: lthy -> function_infos for func and callees -> fn_name -> results *)
|
||||
(* Worker: lthy -> function_infos for func and callees -> func name -> results *)
|
||||
(convert: local_theory -> FunctionInfo2.function_info Symtab.table ->
|
||||
string -> convert_result)
|
||||
(* Functions from prior incremental translation *)
|
||||
(existing_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(* Functions from previous phase *)
|
||||
(prev_results: FunctionInfo2.phase_results)
|
||||
(* Return converted functions in recursive groups.
|
||||
* The groups are tagged with fn_infos from prev_results to identify them. *)
|
||||
|
|
@ -424,6 +445,7 @@ fun par_convert
|
|||
* we accumulate its function_infos, which will be a superset
|
||||
* of the callee infos that each conversion requires. *)
|
||||
FSeq.fold_map (fn fn_infos_accum => fn (lthy, fn_infos) => let
|
||||
val fn_infos = add_background_callees existing_infos fn_infos;
|
||||
val fn_infos_accum = Symtab.merge (K false) (fn_infos_accum, fn_infos);
|
||||
(* Convert fn_infos in parallel, but join the results right away.
|
||||
* This is fine because we will define them together. *)
|
||||
|
|
@ -433,7 +455,7 @@ fun par_convert
|
|||
(f, convert lthy fn_infos_accum f))
|
||||
|> Symtab.make;
|
||||
in ((fn_infos, conv_results), fn_infos_accum) end)
|
||||
Symtab.empty prev_results;
|
||||
existing_infos prev_results;
|
||||
|
||||
(* Given a function body containing arguments and assumed function calls,
|
||||
* abstract the code over those parameters.
|
||||
|
|
@ -451,13 +473,10 @@ fun par_convert
|
|||
*)
|
||||
fun abstract_fn_body
|
||||
(prev_fn_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(fn_name, {body, rec_callees, callee_consts, arg_frees, ...} : convert_result) = let
|
||||
(* Omit rec_callees if our function become non-recursive *)
|
||||
val is_recursive = true (*not (Symset.is_empty rec_callees)*)
|
||||
(fn_name, {body, callee_consts, arg_frees, ...} : convert_result) = let
|
||||
val (callees, rec_callees) = get_callees prev_fn_infos fn_name;
|
||||
val calls = map (the o Symtab.lookup callee_consts) callees;
|
||||
val rec_calls =
|
||||
if is_recursive then map (the o Symtab.lookup callee_consts) rec_callees else [];
|
||||
val rec_calls = map (the o Symtab.lookup callee_consts) rec_callees;
|
||||
|
||||
val abs_body = body
|
||||
|> fold lambda (rev (map Free arg_frees))
|
||||
|
|
@ -489,17 +508,22 @@ fun define_funcs_sequence
|
|||
convert_result Symtab.table ->
|
||||
(* new infos for functions *)
|
||||
FunctionInfo2.function_info Symtab.table * local_theory)
|
||||
(* accumulator, initially empty *)
|
||||
(* previous infos from prior translation (in incremental mode) *)
|
||||
(existing_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(* functions defined so far, initially populated from prior translation *)
|
||||
(defined_so_far: FunctionInfo2.function_info Symtab.table)
|
||||
(converted_groups: (FunctionInfo2.function_info Symtab.table *
|
||||
convert_result Symtab.table) FSeq.fseq)
|
||||
: FunctionInfo2.phase_results =
|
||||
FSeq.mk (fn () =>
|
||||
: FunctionInfo2.phase_results = FSeq.mk (fn () =>
|
||||
case FSeq.uncons converted_groups of
|
||||
NONE => NONE
|
||||
| SOME ((prev_infos, conv_group), remaining_groups) => SOME let
|
||||
(* NB: we don't need to add_background_callees to prev_infos because
|
||||
* par_convert already does that *)
|
||||
(* Define the function group, then split into minimal recursive groups. *)
|
||||
val (new_infos, lthy') = define_worker lthy prev_infos defined_so_far conv_group;
|
||||
val (new_infos, lthy') =
|
||||
define_worker lthy (Symtab.merge (K false) (prev_infos, existing_infos))
|
||||
defined_so_far conv_group;
|
||||
val new_infoss = FunctionInfo2.recalc_callees defined_so_far new_infos;
|
||||
val defined_so_far = Symtab.merge (K false) (defined_so_far, new_infos);
|
||||
(* We can't wrap the first result because we're already in FSeq.mk.
|
||||
|
|
@ -507,12 +531,13 @@ fun define_funcs_sequence
|
|||
val new_infos1 :: new_infoss = new_infoss;
|
||||
(* Output new group(s) in the result sequence. *)
|
||||
val remaining_results =
|
||||
define_funcs_sequence lthy' define_worker defined_so_far remaining_groups;
|
||||
define_funcs_sequence lthy' define_worker
|
||||
existing_infos defined_so_far remaining_groups;
|
||||
in
|
||||
((lthy', new_infos1),
|
||||
FSeq.append
|
||||
(FSeq.of_list (map (fn defs => (lthy', defs)) new_infoss))
|
||||
remaining_results)
|
||||
end);
|
||||
end);
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -616,7 +616,9 @@ let
|
|||
fun translate
|
||||
(filename : string)
|
||||
(prog_info : ProgramInfo.prog_info)
|
||||
(l2_results: FunctionInfo2.phase_results)
|
||||
(l2_results : FunctionInfo2.phase_results)
|
||||
(existing_l2_infos : FunctionInfo2.function_info Symtab.table)
|
||||
(existing_hl_infos : FunctionInfo2.function_info Symtab.table)
|
||||
(HL_setup : HeapLiftBase.heap_lift_setup)
|
||||
(no_heap_abs : Symset.key Symset.set)
|
||||
(force_heap_abs : Symset.key Symset.set)
|
||||
|
|
@ -658,20 +660,27 @@ let
|
|||
fun lookup_l2_results f_name =
|
||||
FSeq.find (fn (_, l2_infos) => Symtab.defined l2_infos f_name) l2_results
|
||||
|> the' ("HL: missing L2 results for " ^ f_name);
|
||||
fun is_function_lifted f_name = let
|
||||
val (lthy, l2_infos) = lookup_l2_results f_name;
|
||||
val can_lift =
|
||||
if can_lift_function lthy prog_info (the (Symtab.lookup l2_infos f_name))
|
||||
then not (Symset.contains no_heap_abs f_name)
|
||||
else if Symset.contains force_heap_abs f_name
|
||||
then true
|
||||
else (* Report functions that we're not lifting,
|
||||
* but not if the user has overridden explicitly *)
|
||||
(if Symset.contains no_heap_abs f_name then () else
|
||||
writeln ("HL: disabling heap lift for: " ^ f_name ^
|
||||
" (use force_heap_abs to enable)");
|
||||
false);
|
||||
in can_lift end;
|
||||
fun is_function_lifted f_name =
|
||||
case Symtab.lookup existing_hl_infos f_name of
|
||||
SOME info => let
|
||||
(* We heap-lifted this function earlier. Check its state type. *)
|
||||
val body = #definition info |> Thm.prop_of |> Utils.rhs_of_eq;
|
||||
val stT = LocalVarExtract2.l2monad_state_type body;
|
||||
in stT = #globals_type heap_info end
|
||||
| NONE => let
|
||||
val (lthy, l2_infos) = lookup_l2_results f_name;
|
||||
val can_lift =
|
||||
if can_lift_function lthy prog_info (the (Symtab.lookup l2_infos f_name))
|
||||
then not (Symset.contains no_heap_abs f_name)
|
||||
else if Symset.contains force_heap_abs f_name
|
||||
then true
|
||||
else (* Report functions that we're not lifting,
|
||||
* but not if the user has overridden explicitly *)
|
||||
(if Symset.contains no_heap_abs f_name then () else
|
||||
writeln ("HL: disabling heap lift for: " ^ f_name ^
|
||||
" (use force_heap_abs to enable)");
|
||||
false);
|
||||
in can_lift end;
|
||||
(* Cache answers for which functions we are lifting. *)
|
||||
val is_function_lifted = String_Memo.memo is_function_lifted;
|
||||
|
||||
|
|
@ -862,7 +871,7 @@ let
|
|||
in (new_infos, lthy') end;
|
||||
|
||||
(* Do conversions in parallel. *)
|
||||
val converted_groups = AutoCorresUtil2.par_convert convert l2_results;
|
||||
val converted_groups = AutoCorresUtil2.par_convert convert existing_l2_infos l2_results;
|
||||
|
||||
(* Sequence of new function_infos and intermediate lthys *)
|
||||
val def_results = FSeq.mk (fn _ =>
|
||||
|
|
@ -871,7 +880,7 @@ let
|
|||
let (* Get initial lthy from end of L2 defs *)
|
||||
val (l2_lthy, _) = FSeq.list_of l2_results |> List.last;
|
||||
val results = AutoCorresUtil2.define_funcs_sequence
|
||||
l2_lthy define Symtab.empty converted_groups;
|
||||
l2_lthy define existing_l2_infos existing_hl_infos converted_groups;
|
||||
in FSeq.uncons results end);
|
||||
|
||||
(* Produce a mapping from each function group to its L1 phase_infos and the
|
||||
|
|
|
|||
|
|
@ -1618,16 +1618,18 @@ fun translate
|
|||
(filename: string)
|
||||
(prog_info: ProgramInfo.prog_info)
|
||||
(l1_results: FunctionInfo2.phase_results)
|
||||
(existing_l1_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(existing_l2_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(do_opt: bool)
|
||||
(trace_opt: bool)
|
||||
(l2_function_name: string -> string)
|
||||
: FunctionInfo2.phase_results =
|
||||
let
|
||||
let;
|
||||
(* Do conversions in parallel. *)
|
||||
val converted_groups =
|
||||
AutoCorresUtil2.par_convert
|
||||
(fn lthy => fn l1_infos => convert lthy prog_info l1_infos do_opt trace_opt l2_function_name)
|
||||
l1_results;
|
||||
existing_l1_infos l1_results;
|
||||
|
||||
(* Sequence of new function_infos and intermediate lthys *)
|
||||
val def_results = FSeq.mk (fn _ =>
|
||||
|
|
@ -1638,7 +1640,7 @@ let
|
|||
fun define_worker lthy l2_callee_infos l1_infos f_convs =
|
||||
define lthy filename prog_info l2_callee_infos l1_infos l2_function_name f_convs;
|
||||
val results = AutoCorresUtil2.define_funcs_sequence
|
||||
l1_lthy define_worker Symtab.empty converted_groups;
|
||||
l1_lthy define_worker existing_l1_infos existing_l2_infos converted_groups;
|
||||
in FSeq.uncons results end);
|
||||
|
||||
(* Produce a mapping from each function group to its L1 phase_infos and the
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ fun mk_L1corres_call_prop ctxt prog_info check_termination target_fn term =
|
|||
fun simpl_conv'
|
||||
(prog_info : ProgramInfo.prog_info)
|
||||
(simpl_defs : FunctionInfo2.function_info Symtab.table)
|
||||
(simpl_calls : FunctionInfo2.call_graph_info)
|
||||
(const_to_function : string Termtab.table)
|
||||
(ctxt : Proof.context)
|
||||
(callee_terms : (bool * term * thm) Symtab.table)
|
||||
(measure_var : term)
|
||||
|
|
@ -92,7 +92,7 @@ fun simpl_conv'
|
|||
let
|
||||
fun prove_term subterms base_thm result_term =
|
||||
let
|
||||
val subterms' = map (simpl_conv' prog_info simpl_defs simpl_calls ctxt
|
||||
val subterms' = map (simpl_conv' prog_info simpl_defs const_to_function ctxt
|
||||
callee_terms measure_var) subterms;
|
||||
val converted_terms = map fst subterms';
|
||||
val subproofs = map snd subterms';
|
||||
|
|
@ -174,7 +174,7 @@ fun simpl_conv'
|
|||
| (Const (@{const_name call}, _) $ a $ (fn_const as Const (b, _)) $ c $ (Abs (_, _, Abs (_, _, (Const (@{const_name Basic}, _) $ d))))) =>
|
||||
let
|
||||
val state_type = #state_type prog_info
|
||||
val target_fn_name = Termtab.lookup (#const_to_function simpl_calls) fn_const
|
||||
val target_fn_name = Termtab.lookup const_to_function fn_const
|
||||
in
|
||||
case Option.mapPartial (Symtab.lookup callee_terms) target_fn_name of
|
||||
NONE =>
|
||||
|
|
@ -194,7 +194,7 @@ fun simpl_conv'
|
|||
* If the callee isn't recursive, it doesn't use the measure var
|
||||
* and we can just give an arbitrary value.
|
||||
*)
|
||||
val target_fn_name = (the target_fn_name)
|
||||
val target_fn_name = the target_fn_name
|
||||
val target_fn = Utils.the' ("missing SIMPL def for " ^ target_fn_name)
|
||||
(Symtab.lookup simpl_defs target_fn_name)
|
||||
val target_rec = FunctionInfo2.is_function_recursive target_fn
|
||||
|
|
@ -302,7 +302,8 @@ end
|
|||
fun get_simpl_body ctxt simpl_defs fn_name =
|
||||
let
|
||||
(* Find the definition of the given function. *)
|
||||
val simpl_thm = #definition (the (Symtab.lookup simpl_defs fn_name))
|
||||
val simpl_thm = #definition (Utils.the' ("SimplConv.get_simpl_body: no such function: " ^ fn_name)
|
||||
(Symtab.lookup simpl_defs fn_name))
|
||||
handle ERROR _ => raise FunctionNotFound fn_name;
|
||||
|
||||
(* Unfold terms in the body which we don't want to deal with. *)
|
||||
|
|
@ -326,9 +327,11 @@ in
|
|||
(unfolded_simpl_term, unfolded_simpl_thm, impl_thm)
|
||||
end
|
||||
|
||||
fun get_l1corres_thm prog_info simpl_defs simpl_calls check_termination ctxt do_opt trace_opt
|
||||
fun get_l1corres_thm prog_info simpl_defs const_to_function
|
||||
check_termination ctxt do_opt trace_opt
|
||||
fn_name callee_terms measure_var = let
|
||||
val fn_def = the (Symtab.lookup simpl_defs fn_name);
|
||||
val fn_def = Utils.the' ("SimplConv.get_l1corres_thm: no such function: " ^ fn_name)
|
||||
(Symtab.lookup simpl_defs fn_name);
|
||||
val thy = Proof_Context.theory_of ctxt
|
||||
val (simpl_term, simpl_thm, impl_thm) = get_simpl_body ctxt simpl_defs fn_name
|
||||
|
||||
|
|
@ -339,7 +342,7 @@ fun get_l1corres_thm prog_info simpl_defs simpl_calls check_termination ctxt do_
|
|||
* Do the conversion. We receive a new monadic version of the SIMPL
|
||||
* term and a tactic for proving correspondence.
|
||||
*)
|
||||
val (monad, tactic) = simpl_conv' prog_info simpl_defs simpl_calls ctxt
|
||||
val (monad, tactic) = simpl_conv' prog_info simpl_defs const_to_function ctxt
|
||||
callee_terms measure_var simpl_term
|
||||
|
||||
(*
|
||||
|
|
@ -360,7 +363,7 @@ fun get_l1corres_thm prog_info simpl_defs simpl_calls check_termination ctxt do_
|
|||
* SIMPL body (with folded constants) and the output monad term.
|
||||
*)
|
||||
in
|
||||
mk_L1corres_call_prop ctxt prog_info check_termination (the (Symtab.lookup simpl_defs fn_name)) monad
|
||||
mk_L1corres_call_prop ctxt prog_info check_termination fn_def monad
|
||||
|> Thm.cterm_of ctxt
|
||||
|> Goal.init
|
||||
|> (case impl_thm of
|
||||
|
|
@ -448,7 +451,7 @@ fun convert
|
|||
(lthy: local_theory)
|
||||
(prog_info: ProgramInfo.prog_info)
|
||||
(simpl_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(simpl_call_graph: FunctionInfo2.call_graph_info)
|
||||
(const_to_function: string Termtab.table)
|
||||
(check_termination: bool)
|
||||
(do_opt: bool)
|
||||
(trace_opt: bool)
|
||||
|
|
@ -462,6 +465,8 @@ let
|
|||
val ([measure_var_name], lthy') = Variable.variant_fixes ["rec_measure'"] lthy;
|
||||
val measure_var = Free (measure_var_name, AutoCorresUtil2.measureT);
|
||||
|
||||
val _ = @{trace} ("convert", f_name, Symtab.keys simpl_infos, Symset.dest (#callees f_info), Symset.dest (#rec_callees f_info))
|
||||
|
||||
(* Add callee assumptions. Note that our define code has to use the same assumption order. *)
|
||||
val (lthy'', export_thm, callee_terms) =
|
||||
AutoCorresUtil2.assume_called_functions_corres lthy'
|
||||
|
|
@ -475,7 +480,7 @@ let
|
|||
val (thm, opt_traces) =
|
||||
if #is_simpl_wrapper f_info
|
||||
then (mk_l1corres_call_simpl_thm check_termination lthy'' f_info, [])
|
||||
else get_l1corres_thm prog_info simpl_infos simpl_call_graph check_termination lthy''
|
||||
else get_l1corres_thm prog_info simpl_infos const_to_function 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));
|
||||
|
|
@ -487,7 +492,7 @@ let
|
|||
callee_terms |> map (fn (callee, (_, const, _)) => (callee, const)) |> Symtab.make;
|
||||
in
|
||||
{ body = f_body,
|
||||
(* Expose callee assumptions and generalizes calle vars *)
|
||||
(* Expose callee assumptions and generalizes callee vars *)
|
||||
proof = Morphism.thm export_thm thm,
|
||||
rec_callees = rec_callees,
|
||||
callee_consts = callee_consts,
|
||||
|
|
@ -549,11 +554,12 @@ fun define
|
|||
* correspondence between our generated specs and the original SIMPL
|
||||
* code).
|
||||
*)
|
||||
(* FIXME: use AutoCorresUtil.Future instead of default *)
|
||||
fun translate
|
||||
(filename: string)
|
||||
(prog_info: ProgramInfo.prog_info)
|
||||
(simpl_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(existing_simpl_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(existing_l1_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(check_termination: bool)
|
||||
(do_opt: bool)
|
||||
(trace_opt: bool)
|
||||
|
|
@ -573,18 +579,26 @@ let
|
|||
in (lthy, f_infos) end)
|
||||
|> FSeq.of_list;
|
||||
|
||||
(* We also need to update the const_to_function table *)
|
||||
val const_to_function =
|
||||
Termtab.merge (K false)
|
||||
(#const_to_function simpl_call_graph,
|
||||
Symtab.dest existing_simpl_infos
|
||||
|> map (fn (f, info) => (#raw_const info, f))
|
||||
|> Termtab.make);
|
||||
|
||||
(* Do conversions in parallel. *)
|
||||
val converted_groups =
|
||||
AutoCorresUtil2.par_convert
|
||||
(fn lthy => fn l1_infos =>
|
||||
convert lthy prog_info simpl_infos simpl_call_graph check_termination
|
||||
(fn lthy => fn simpl_infos =>
|
||||
convert lthy prog_info simpl_infos const_to_function check_termination
|
||||
do_opt trace_opt l1_function_name)
|
||||
initial_results;
|
||||
existing_simpl_infos initial_results;
|
||||
|
||||
(* Sequence of new function_infos and intermediate lthys *)
|
||||
val def_results = AutoCorresUtil2.define_funcs_sequence
|
||||
lthy (define filename prog_info check_termination l1_function_name)
|
||||
Symtab.empty converted_groups;
|
||||
existing_simpl_infos existing_l1_infos converted_groups;
|
||||
|
||||
(* Produce a mapping from each function group to its L1 phase_infos and the
|
||||
* earliest intermediate lthy where it is defined. *)
|
||||
|
|
|
|||
|
|
@ -21,7 +21,6 @@ install_C_file "type_strengthen.c"
|
|||
|
||||
(* Translate only opt_j *)
|
||||
autocorres [
|
||||
ts_rules = nondet,
|
||||
scope_depth = 0,
|
||||
scope = opt_j
|
||||
] "type_strengthen.c"
|
||||
|
|
|
|||
|
|
@ -573,7 +573,9 @@ fun translate
|
|||
(force_lift : Monad_Types.monad_type Symtab.table)
|
||||
(filename : string)
|
||||
(prog_info : ProgramInfo.prog_info)
|
||||
(l2_results: FunctionInfo2.phase_results)
|
||||
(l2_results : FunctionInfo2.phase_results)
|
||||
(existing_l2_infos : FunctionInfo2.function_info Symtab.table)
|
||||
(existing_ts_infos : FunctionInfo2.function_info Symtab.table)
|
||||
(make_function_name : string -> string)
|
||||
(keep_going : bool)
|
||||
(do_opt : bool)
|
||||
|
|
@ -594,6 +596,10 @@ let
|
|||
in FunctionInfo2.function_info_upd_definition pretty_def info end)
|
||||
l2_infos;
|
||||
|
||||
(* Add prior L2 translations to round out L2 callees. *)
|
||||
val l2_infos = AutoCorresUtil2.add_background_callees existing_l2_infos l2_infos;
|
||||
val l2_infos = Symtab.merge (K false) (l2_infos, existing_l2_infos);
|
||||
|
||||
(* For now, just works sequentially like the old TypeStrengthen. *)
|
||||
fun translate_group fn_names (lthy, _, ts_infos) =
|
||||
let
|
||||
|
|
@ -610,7 +616,7 @@ let
|
|||
in (lthy, new_ts_infos, Symtab.merge (K false) (ts_infos, new_ts_infos)) end;
|
||||
|
||||
val ts_results =
|
||||
Utils.accumulate translate_group (lthy, Symtab.empty, Symtab.empty)
|
||||
Utils.accumulate translate_group (lthy, Symtab.empty, existing_ts_infos)
|
||||
(map (map fst o Symtab.dest o snd) l2_results)
|
||||
|> fst
|
||||
|> map (fn (lthy, ts_infos, _) => (lthy, ts_infos));
|
||||
|
|
|
|||
|
|
@ -157,7 +157,11 @@ end
|
|||
fun translate
|
||||
(filename: string)
|
||||
(prog_info: ProgramInfo.prog_info)
|
||||
(* Note that we refer to the previous phase as "l2"; it may be
|
||||
* from the L2 or HL phase. *)
|
||||
(l2_results: FunctionInfo2.phase_results)
|
||||
(existing_l2_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(existing_wa_infos: FunctionInfo2.function_info Symtab.table)
|
||||
(unsigned_abs: Symset.key Symset.set)
|
||||
(no_signed_abs: Symset.key Symset.set)
|
||||
(trace_funcs: string list)
|
||||
|
|
@ -411,7 +415,7 @@ let
|
|||
end
|
||||
|
||||
(* Define a previously-converted function (or recursive function group).
|
||||
* lthy must include all definitions from l2_callees. *)
|
||||
* lthy must include all definitions from wa_callees. *)
|
||||
fun define
|
||||
(lthy: local_theory)
|
||||
(l2_infos: FunctionInfo2.function_info Symtab.table)
|
||||
|
|
@ -447,7 +451,7 @@ let
|
|||
in (new_infos, lthy') end;
|
||||
|
||||
(* Do conversions in parallel. *)
|
||||
val converted_groups = AutoCorresUtil2.par_convert convert l2_results;
|
||||
val converted_groups = AutoCorresUtil2.par_convert convert existing_l2_infos l2_results;
|
||||
|
||||
(* Sequence of intermediate states: (lthy, new_defs) *)
|
||||
val def_results = FSeq.mk (fn _ =>
|
||||
|
|
@ -456,7 +460,7 @@ let
|
|||
let (* Get initial lthy from end of L2 defs *)
|
||||
val (l2_lthy, _) = FSeq.list_of l2_results |> List.last;
|
||||
val results = AutoCorresUtil2.define_funcs_sequence
|
||||
l2_lthy define Symtab.empty converted_groups;
|
||||
l2_lthy define existing_l2_infos existing_wa_infos converted_groups;
|
||||
in FSeq.uncons results end);
|
||||
|
||||
(* Produce a mapping from each function group to its L1 phase_infos and the
|
||||
|
|
|
|||
Loading…
Reference in New Issue