author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29272  fb3ccf499df5 
child 31036  64ff53fc0c0c 
permissions  rwrr 
24584  1 
(* Title: HOL/Tools/recfun_codegen.ML 
12447  2 
Author: Stefan Berghofer, TU Muenchen 
3 

4 
Code generator for recursive functions. 

5 
*) 

6 

7 
signature RECFUN_CODEGEN = 

8 
sig 

18708  9 
val setup: theory > theory 
12447  10 
end; 
11 

12 
structure RecfunCodegen : RECFUN_CODEGEN = 

13 
struct 

14 

15 
open Codegen; 

16 

28522  17 
structure ModuleData = TheoryDataFun 
22846  18 
( 
28522  19 
type T = string Symtab.table; 
12447  20 
val empty = Symtab.empty; 
21 
val copy = I; 

16424  22 
val extend = I; 
28522  23 
fun merge _ = Symtab.merge (K true); 
22846  24 
); 
12447  25 

28703  26 
fun add_thm NONE thm thy = Code.add_eqn thm thy 
27 
 add_thm (SOME module_name) thm thy = 

28522  28 
case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm 
29 
of SOME (thm', _) => let val c = Code_Unit.const_eqn thm' 

30 
in thy 

31 
> ModuleData.map (Symtab.update (c, module_name)) 

28703  32 
> Code.add_eqn thm' 
28522  33 
end 
28703  34 
 NONE => Code.add_eqn thm thy; 
24624
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

35 

28522  36 
fun meta_eq_to_obj_eq thy thm = 
37 
let 

38 
val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm; 

39 
in if Sign.of_sort thy (T, @{sort type}) 

40 
then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm])) 

41 
else NONE 

42 
end; 

19344  43 

28522  44 
fun expand_eta thy [] = [] 
45 
 expand_eta thy (thms as thm :: _) = 

46 
let 

47 
val (_, ty) = Code_Unit.const_typ_eqn thm; 

29272  48 
in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty 
28522  49 
then thms 
50 
else map (Code_Unit.expand_eta thy 1) thms 

51 
end; 

14196  52 

28522  53 
fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else 
54 
let 

55 
val c' = AxClass.unoverload_const thy (c, T); 

56 
val opt_name = Symtab.lookup (ModuleData.get thy) c'; 

57 
val thms = Code.these_raw_eqns thy c' 

58 
> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) 

59 
> expand_eta thy 

60 
> map (AxClass.overload thy) 

61 
> map_filter (meta_eq_to_obj_eq thy) 

62 
> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var 

63 
> map (rpair opt_name) 

64 
in if null thms then NONE else SOME thms end; 

65 

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

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

15321
694f9d3ce90d
Reimplemented some operations on "code lemma" table to avoid that code
berghofe
parents:
15257
diff
changeset

68 

16645  69 
fun get_equations thy defs (s, T) = 
28522  70 
(case retrieve_equations thy (s, T) of 
16645  71 
NONE => ([], "") 
72 
 SOME thms => 

28522  73 
let val thms' = filter (fn (thm, _) => is_instance T 
74 
(snd (const_of (prop_of thm)))) thms 

16645  75 
in if null thms' then ([], "") 
76 
else (preprocess thy (map fst thms'), 

77 
case snd (snd (split_last thms')) of 

78 
NONE => (case get_defn thy defs s T of 

27398
768da1da59d6
simplified retrieval of theory names of consts and types
haftmann
parents:
26975
diff
changeset

79 
NONE => Codegen.thyname_of_const thy s 
16645  80 
 SOME ((_, (thyname, _)), _) => thyname) 
81 
 SOME thyname => thyname) 

82 
end); 

12447  83 

16645  84 
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of 
17144  85 
SOME (_, SOME i) => " def" ^ string_of_int i  _ => ""); 
12447  86 

87 
exception EQN of string * typ * string; 

88 

22887  89 
fun cycle g (xs, x : string) = 
90 
if member (op =) xs x then xs 

91 
else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x))); 

12447  92 

28535  93 
fun add_rec_funs thy defs dep module eqs gr = 
12447  94 
let 
16645  95 
fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t), 
96 
dest_eqn (rename_term t)); 

12447  97 
val eqs' = map dest_eq eqs; 
98 
val (dname, _) :: _ = eqs'; 

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

100 

28535  101 
fun mk_fundef module fname first [] gr = ([], gr) 
102 
 mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr = 

12447  103 
let 
28535  104 
val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr; 
105 
val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1; 

106 
val (rest, gr3) = mk_fundef module fname' false xs gr2 ; 

107 
val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3; 

108 
val num_args = (length o snd o strip_comb) lhs; 

109 
val prfx = if fname = fname' then " " 

110 
else if not first then "and" 

111 
else if num_args = 0 then "val" 

112 
else "fun"; 

113 
val pl' = Pretty.breaks (str prfx 

114 
:: (if num_args = 0 then [pl, str ":", ty] else [pl])); 

12447  115 
in 
28535  116 
(Pretty.blk (4, pl' 
117 
@ [str " =", Pretty.brk 1, pr]) :: rest, gr4) 

12447  118 
end; 
119 

17144  120 
fun put_code module fundef = map_node dname 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26928
diff
changeset

121 
(K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26928
diff
changeset

122 
separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n")); 
12447  123 

124 
in 

17144  125 
(case try (get_node gr) dname of 
15531  126 
NONE => 
12447  127 
let 
17144  128 
val gr1 = add_edge (dname, dep) 
129 
(new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); 

28535  130 
val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ; 
12447  131 
val xs = cycle gr2 ([], dname); 
17144  132 
val cs = map (fn x => case get_node gr2 x of 
16645  133 
(SOME (EQN (s, T, _)), _, _) => (s, T) 
12447  134 
 _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ 
135 
implode (separate ", " xs))) xs 

136 
in (case xs of 

28535  137 
[_] => (module, put_code module fundef gr2) 
12447  138 
 _ => 
139 
if not (dep mem xs) then 

140 
let 

16645  141 
val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; 
17144  142 
val module' = if_library thyname module; 
16645  143 
val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss)); 
28535  144 
val (fundef', gr3) = mk_fundef module' "" true eqs'' 
17144  145 
(add_edge (dname, dep) 
30190  146 
(List.foldr (uncurry new_node) (del_nodes xs gr2) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

147 
(map (fn k => 
28535  148 
(k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) 
149 
in (module', put_code module' fundef' gr3) end 

150 
else (module, gr2)) 

12447  151 
end 
17144  152 
 SOME (SOME (EQN (_, _, s)), module', _) => 
28535  153 
(module', if s = "" then 
17144  154 
if dname = dep then gr else add_edge (dname, dep) gr 
28535  155 
else if s = dep then gr else add_edge (s, dep) gr)) 
12447  156 
end; 
157 

28535  158 
fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22887
diff
changeset

159 
(Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of 
16645  160 
(([], _), _) => NONE 
15531  161 
 (_, SOME _) => NONE 
17144  162 
 ((eqns, thyname), NONE) => 
16645  163 
let 
17144  164 
val module' = if_library thyname module; 
28535  165 
val (ps, gr') = fold_map 
166 
(invoke_codegen thy defs dep module true) ts gr; 

17144  167 
val suffix = mk_suffix thy defs p; 
28535  168 
val (module'', gr'') = 
169 
add_rec_funs thy defs dep module' (map prop_of eqns) gr'; 

170 
val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr'' 

12447  171 
in 
28535  172 
SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''') 
12447  173 
end) 
15531  174 
 _ => NONE); 
12447  175 

28703  176 
val setup = let 
177 
fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping 

178 
(add_thm opt_module thm) I); 

179 
val del = Thm.declaration_attribute (fn thm => Context.mapping 

180 
(Code.del_eqn thm) I); 

181 
in 

24219  182 
add_codegen "recfun" recfun_codegen 
183 
#> Code.add_attribute ("", Args.del  Scan.succeed del 

28703  184 
 Scan.option (Args.$$$ "target"  Args.colon  Args.name) >> add) 
185 
end; 

12447  186 

187 
end; 