(* Title: HOL/Tools/recfun_codegen.ML
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Code generator for recursive functions.
*)
signature RECFUN_CODEGEN =
sig
val add: string option -> attribute
val add_default: attribute
val del: attribute
val setup: theory -> theory
end;
structure RecfunCodegen : RECFUN_CODEGEN =
struct
open Codegen;
structure ModuleData = TheoryDataFun
(
type T = string Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ = Symtab.merge (K true);
);
fun add_thm add NONE thm thy = add thm thy
| add_thm add (SOME module_name) thm thy =
case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
in thy
|> ModuleData.map (Symtab.update (c, module_name))
|> add thm'
end
| NONE => add thm thy;
fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
(add_thm Code.add_eqn opt_module thm) I);
val add_default = Thm.declaration_attribute (fn thm => Context.mapping
(add_thm Code.add_default_eqn NONE thm) I);
val del = Thm.declaration_attribute (fn thm => Context.mapping
(Code.del_eqn thm) I);
fun meta_eq_to_obj_eq thy thm =
let
val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm;
in if Sign.of_sort thy (T, @{sort type})
then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm]))
else NONE
end;
fun expand_eta thy [] = []
| expand_eta thy (thms as thm :: _) =
let
val (_, ty) = Code_Unit.const_typ_eqn thm;
in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty
then thms
else map (Code_Unit.expand_eta thy 1) thms
end;
fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
let
val c' = AxClass.unoverload_const thy (c, T);
val opt_name = Symtab.lookup (ModuleData.get thy) c';
val thms = Code.these_raw_eqns thy c'
|> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
|> expand_eta thy
|> map (AxClass.overload thy)
|> map_filter (meta_eq_to_obj_eq thy)
|> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
|> map (rpair opt_name)
in if null thms then NONE else SOME thms end;
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
val const_of = dest_Const o head_of o fst o dest_eqn;
fun get_equations thy defs (s, T) =
(case retrieve_equations thy (s, T) of
NONE => ([], "")
| SOME thms =>
let val thms' = filter (fn (thm, _) => is_instance T
(snd (const_of (prop_of thm)))) thms
in if null thms' then ([], "")
else (preprocess thy (map fst thms'),
case snd (snd (split_last thms')) of
NONE => (case get_defn thy defs s T of
NONE => Codegen.thyname_of_const thy s
| SOME ((_, (thyname, _)), _) => thyname)
| SOME thyname => thyname)
end);
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
exception EQN of string * typ * string;
fun cycle g (xs, x : string) =
if member (op =) xs x then xs
else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x)));
fun add_rec_funs thy defs gr dep eqs module =
let
fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
dest_eqn (rename_term t));
val eqs' = map dest_eq eqs;
val (dname, _) :: _ = eqs';
val (s, T) = const_of (hd eqs);
fun mk_fundef module fname first gr [] = (gr, [])
| mk_fundef module fname first gr ((fname' : string, (lhs, rhs)) :: xs) =
let
val prfx = if first then
(case strip_comb lhs of (_, []) => "val " | _ => "fun ")
else "and ";
val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs);
val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);
val (gr3, rest) = mk_fundef module fname' false gr2 xs
in
(gr3, Pretty.blk (4, [str (if fname = fname' then " | " else prfx),
pl, str " =", Pretty.brk 1, pr]) :: rest)
end;
fun put_code module fundef = map_node dname
(K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
in
(case try (get_node gr) dname of
NONE =>
let
val gr1 = add_edge (dname, dep)
(new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
val (gr2, fundef) = mk_fundef module "" true gr1 eqs';
val xs = cycle gr2 ([], dname);
val cs = map (fn x => case get_node gr2 x of
(SOME (EQN (s, T, _)), _, _) => (s, T)
| _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
implode (separate ", " xs))) xs
in (case xs of
[_] => (put_code module fundef gr2, module)
| _ =>
if not (dep mem xs) then
let
val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
val module' = if_library thyname module;
val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
val (gr3, fundef') = mk_fundef module' "" true
(add_edge (dname, dep)
(foldr (uncurry new_node) (del_nodes xs gr2)
(map (fn k =>
(k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs''
in (put_code module' fundef' gr3, module') end
else (gr2, module))
end
| SOME (SOME (EQN (_, _, s)), module', _) =>
(if s = "" then
if dname = dep then gr else add_edge (dname, dep) gr
else if s = dep then gr else add_edge (s, dep) gr,
module'))
end;
fun recfun_codegen thy defs gr dep module brack t = (case strip_comb t of
(Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
(([], _), _) => NONE
| (_, SOME _) => NONE
| ((eqns, thyname), NONE) =>
let
val module' = if_library thyname module;
val (gr', ps) = foldl_map
(invoke_codegen thy defs dep module true) (gr, ts);
val suffix = mk_suffix thy defs p;
val (gr'', module'') =
add_rec_funs thy defs gr' dep (map prop_of eqns) module';
val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr''
in
SOME (gr''', mk_app brack (str (mk_qual_id module fname)) ps)
end)
| _ => NONE);
val setup =
add_codegen "recfun" recfun_codegen
#> Code.add_attribute ("", Args.del |-- Scan.succeed del
|| Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
end;