12447

1 
(* Title: HOL/recfun_codegen.ML


2 
ID: $Id$


3 
Author: Stefan Berghofer, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)


5 


6 
Code generator for recursive functions.


7 
*)


8 


9 
signature RECFUN_CODEGEN =


10 
sig


11 
val add: theory attribute


12 
val setup: (theory > theory) list


13 
end;


14 


15 
structure RecfunCodegen : RECFUN_CODEGEN =


16 
struct


17 


18 
open Codegen;


19 

12556

20 
structure CodegenArgs =

12447

21 
struct


22 
val name = "HOL/recfun_codegen";


23 
type T = thm list Symtab.table;


24 
val empty = Symtab.empty;


25 
val copy = I;


26 
val prep_ext = I;


27 
val merge = Symtab.merge_multi eq_thm;


28 
fun print _ _ = ();


29 
end;


30 

12556

31 
structure CodegenData = TheoryDataFun(CodegenArgs);

12447

32 


33 
val prop_of = #prop o rep_thm;


34 
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;


35 
val const_of = dest_Const o head_of o fst o dest_eqn;


36 


37 
fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^


38 
string_of_thm thm);


39 


40 
fun add (p as (thy, thm)) =


41 
let


42 
val tsig = Sign.tsig_of (sign_of thy);

12556

43 
val tab = CodegenData.get thy;

12447

44 
val (s, _) = const_of (prop_of thm);


45 


46 
val matches = curry


47 
(Pattern.matches tsig o pairself (fst o dest_eqn o prop_of));


48 

12556

49 
in (CodegenData.put (Symtab.update ((s,

12447

50 
filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @ [thm]),


51 
tab)) thy, thm)


52 
end handle TERM _ => (warn thm; p)  Pattern.Pattern => (warn thm; p);


53 


54 
fun get_equations thy (s, T) =

12556

55 
(case Symtab.lookup (CodegenData.get thy, s) of

12447

56 
None => []


57 
 Some thms => filter (fn thm => is_instance thy T


58 
(snd (const_of (prop_of thm)))) thms);


59 


60 
fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^


61 
(case get_defn thy s T of


62 
Some (_, Some i) => "_def" ^ string_of_int i


63 
 _ => "");


64 


65 
exception EQN of string * typ * string;


66 


67 
fun cycle g (xs, x) =


68 
if x mem xs then xs


69 
else foldl (cycle g) (x :: xs, flat (Graph.find_paths g (x, x)));


70 


71 
fun add_rec_funs thy gr dep eqs =


72 
let


73 
fun dest_eq t =


74 
(mk_poly_id thy (const_of t), dest_eqn (rename_term t));


75 
val eqs' = map dest_eq eqs;


76 
val (dname, _) :: _ = eqs';


77 
val (s, T) = const_of (hd eqs);


78 


79 
fun mk_fundef fname prfx gr [] = (gr, [])


80 
 mk_fundef fname prfx gr ((fname', (lhs, rhs)) :: xs) =


81 
let


82 
val (gr1, pl) = invoke_codegen thy dname false (gr, lhs);


83 
val (gr2, pr) = invoke_codegen thy dname false (gr1, rhs);


84 
val (gr3, rest) = mk_fundef fname' "and " gr2 xs


85 
in


86 
(gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  " else prfx),


87 
pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)


88 
end;


89 


90 
fun put_code fundef = Graph.map_node dname


91 
(K (Some (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0,


92 
separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));


93 


94 
in


95 
(case try (Graph.get_node gr) dname of


96 
None =>


97 
let


98 
val gr1 = Graph.add_edge (dname, dep)


99 
(Graph.new_node (dname, (Some (EQN (s, T, "")), "")) gr);


100 
val (gr2, fundef) = mk_fundef "" "fun " gr1 eqs';


101 
val xs = cycle gr2 ([], dname);


102 
val cs = map (fn x => case Graph.get_node gr2 x of


103 
(Some (EQN (s, T, _)), _) => (s, T)


104 
 _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^


105 
implode (separate ", " xs))) xs


106 
in (case xs of


107 
[_] => put_code fundef gr2


108 
 _ =>


109 
if not (dep mem xs) then


110 
let


111 
val eqs'' = map (dest_eq o prop_of)


112 
(flat (map (get_equations thy) cs));


113 
val (gr3, fundef') = mk_fundef "" "fun "


114 
(Graph.add_edge (dname, dep)


115 
(foldr (uncurry Graph.new_node) (map (fn k =>


116 
(k, (Some (EQN ("", dummyT, dname)), ""))) xs,


117 
Graph.del_nodes xs gr2))) eqs''


118 
in put_code fundef' gr3 end


119 
else gr2)


120 
end


121 
 Some (Some (EQN (_, _, s)), _) =>


122 
if s = "" then


123 
if dname = dep then gr else Graph.add_edge (dname, dep) gr


124 
else if s = dep then gr else Graph.add_edge (s, dep) gr)


125 
end;


126 


127 
fun recfun_codegen thy gr dep brack t = (case strip_comb t of


128 
(Const p, ts) => (case get_equations thy p of


129 
[] => None


130 
 eqns =>


131 
let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)


132 
in


133 
Some (add_rec_funs thy gr' dep (map prop_of eqns),


134 
mk_app brack (Pretty.str (mk_poly_id thy p)) ps)


135 
end)


136 
 _ => None);


137 


138 


139 
val setup =

12556

140 
[CodegenData.init,

12447

141 
add_codegen "recfun" recfun_codegen,

12556

142 
add_attribute "" add];

12447

143 


144 
end;
