adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

WIP: autocorres: refactor prepare_fn_body

This commit is contained in:
Japheth Lim 2016-06-28 15:03:27 +10:00
parent 46460cedf0
commit 2d24e1ebef
5 changed files with 33 additions and 103 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
tools/autocorres/autocorres_util2.ML
View File

@ -181,6 +181,35 @@ fun get_rec_callees
|> Termtab.make;
in get_body_callees callee_lookup body end;
(* Given a function body containing arguments and assumed function calls,
* abstract the code over those parameters.
*
* The returned body will have free variables as placeholders for the function's
* measure parameter and other arguments, as well as for the functions it calls.
*
* We modify the body to be of the form:
*
* %fun1 fun2 rec1 rec2 measure arg1 arg2. f <...>
*
* That is, all non-recursive calls are abstracted out the front, followed by
* recursive calls, followed by the measure variable, followed by function
* arguments. This is the format expected by define_funcs.
*)
fun abstract_fn_body
(prev_fn_infos: FunctionInfo2.function_info Symtab.table)
(fn_name, (body, callee_consts, corres_thm, arg_frees)) = let
val _ = @{trace} ("L2 prepare_fn_body", fn_name, corres_thm);
val (callees, rec_callees) = get_callees prev_fn_infos fn_name;
val calls = map (the o Symtab.lookup callee_consts) callees;
val rec_calls = map (the o Symtab.lookup callee_consts) rec_callees;
val abs_body = body
|> fold lambda (rev (map Free arg_frees))
|> fold lambda (rev rec_calls)
|> fold lambda (rev calls);
in abs_body end;
(*
* Given one or more function specs, define them and instantiate corres proofs.
*

27
tools/autocorres/heap_lift2.ML
View File

@ -836,35 +836,10 @@ let
(* 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, LocalVarExtract *)
fun prepare_fn_body (fn_name, (body, callee_consts, corres_thm, arg_frees)) = let
val _ = @{trace} ("HL prepare_fn_body", fn_name, corres_thm);
val (callees, rec_callees) = AutoCorresUtil2.get_callees l2_infos fn_name;
val calls = map (the o Symtab.lookup callee_consts) callees;
val rec_calls = map (the o Symtab.lookup callee_consts) rec_callees;
(*
* The returned body will have free variables as placeholders for the function's
* measure parameter and other arguments, and schematic variables for the functions it calls.
*
* We modify the body to be of the form:
*
* %fun1 fun2 rec1 rec2 measure arg1 arg2. f <...>
*
* That is, all non-recursive calls are abstracted out the front, followed by
* recursive calls, followed by the measure variable, followed by function
* arguments. This is the format expected by define_funcs.
*)
val abs_body = body
|> fold lambda (rev (map Free arg_frees))
|> fold lambda (rev rec_calls)
|> fold lambda (rev calls);
in abs_body end;
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,
prepare_fn_body (name, def))));
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');
val (new_thms, (), lthy') =
AutoCorresUtil2.define_funcs FunctionInfo2.HL filename l2_infos

27
tools/autocorres/local_var_extract2.ML
View File

@ -1588,36 +1588,11 @@ 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 *)
fun prepare_fn_body (fn_name, (body, callee_consts, corres_thm, arg_frees)) = let
val _ = @{trace} ("L2 prepare_fn_body", fn_name, corres_thm);
val (callees, rec_callees) = AutoCorresUtil2.get_callees l1_infos fn_name;
val calls = map (the o Symtab.lookup callee_consts) callees;
val rec_calls = map (the o Symtab.lookup callee_consts) rec_callees;
(*
* The returned body will have free variables as placeholders for the function's
* measure parameter and other arguments, and schematic variables for the functions it calls.
*
* We modify the body to be of the form:
*
* %fun1 fun2 rec1 rec2 measure arg1 arg2. f <...>
*
* That is, all non-recursive calls are abstracted out the front, followed by
* recursive calls, followed by the measure variable, followed by function
* arguments. This is the format expected by define_funcs.
*)
val abs_body = body
|> fold lambda (rev (map Free arg_frees))
|> fold lambda (rev rec_calls)
|> fold lambda (rev calls);
in abs_body end;
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,
prepare_fn_body (name, def))));
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');
val (new_thms, (), lthy') =
AutoCorresUtil2.define_funcs FunctionInfo2.L2 filename l1_infos

26
tools/autocorres/simpl_conv2.ML
View File

@ -528,35 +528,11 @@ fun define
mk_L1corres_call_prop ctxt prog_info check_termination
(the (Symtab.lookup simpl_defs fn_name)) (betapply (free, measure_var));
fun prepare_fn_body (fn_name, (body, callee_consts, corres_thm, [measure_free])) = let
val _ = @{trace} ("L1 prepare_fn_body", fn_name, corres_thm);
val (callees, rec_callees) = AutoCorresUtil2.get_callees simpl_defs fn_name;
val calls = map (the o Symtab.lookup callee_consts) callees;
val rec_calls = map (the o Symtab.lookup callee_consts) rec_callees;
(*
* The returned body will have free variables as placeholders for the function's
* measure parameter and other arguments, and schematic variables for the functions it calls.
*
* We modify the body to be of the form:
*
* %fun1 fun2 rec1 rec2 measure arg1 arg2. f <...>
*
* That is, all non-recursive calls are abstracted out the front, followed by
* recursive calls, followed by the measure variable, followed by function
* arguments (none for L1). This is the format expected by define_funcs.
*)
val abs_body = body
|> lambda (Free measure_free)
|> fold lambda (rev rec_calls)
|> fold lambda (rev calls);
in abs_body end;
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,
prepare_fn_body (name, def))));
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');
val (new_thms, (), lthy') =
AutoCorresUtil2.define_funcs FunctionInfo2.L1 filename simpl_defs

27
tools/autocorres/word_abstract2.ML
View File

@ -416,35 +416,10 @@ let
(* 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, LocalVarExtract *)
fun prepare_fn_body (fn_name, (body, callee_consts, corres_thm, arg_frees)) = let
val _ = @{trace} ("WA prepare_fn_body", fn_name, corres_thm);
val (callees, rec_callees) = AutoCorresUtil2.get_callees l2_infos fn_name;
val calls = map (the o Symtab.lookup callee_consts) callees;
val rec_calls = map (the o Symtab.lookup callee_consts) rec_callees;
(*
* The returned body will have free variables as placeholders for the function's
* measure parameter and other arguments, and schematic variables for the functions it calls.
*
* We modify the body to be of the form:
*
* %fun1 fun2 rec1 rec2 measure arg1 arg2. f <...>
*
* That is, all non-recursive calls are abstracted out the front, followed by
* recursive calls, followed by the measure variable, followed by function
* arguments. This is the format expected by define_funcs.
*)
val abs_body = body
|> fold lambda (rev (map Free arg_frees))
|> fold lambda (rev rec_calls)
|> fold lambda (rev calls);
in abs_body end;
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,
prepare_fn_body (name, def))));
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');
val (new_thms, (), lthy') =
AutoCorresUtil2.define_funcs FunctionInfo2.WA filename l2_infos