author  wenzelm 
Mon, 08 Oct 2007 18:13:06 +0200  
changeset 24907  bfb2e82b61fe 
parent 24624  b8383b1bbae3 
child 25389  3e58c7cb5a73 
permissions  rwrr 
24584  1 
(* Title: HOL/Tools/recfun_codegen.ML 
12447  2 
ID: $Id$ 
3 
Author: Stefan Berghofer, TU Muenchen 

4 

5 
Code generator for recursive functions. 

6 
*) 

7 

8 
signature RECFUN_CODEGEN = 

9 
sig 

18728  10 
val add: string option > attribute 
24624
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

11 
val add_default: attribute 
18728  12 
val del: attribute 
18708  13 
val setup: theory > theory 
12447  14 
end; 
15 

16 
structure RecfunCodegen : RECFUN_CODEGEN = 

17 
struct 

18 

19 
open Codegen; 

20 

20597  21 
structure RecCodegenData = TheoryDataFun 
22846  22 
( 
16645  23 
type T = (thm * string option) list Symtab.table; 
12447  24 
val empty = Symtab.empty; 
25 
val copy = I; 

16424  26 
val extend = I; 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21410
diff
changeset

27 
fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst); 
22846  28 
); 
12447  29 

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

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

31 
val lhs_of = fst o dest_eqn o prop_of; 
12447  32 
val const_of = dest_Const o head_of o fst o dest_eqn; 
33 

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

35 
string_of_thm thm); 

36 

24624
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

37 
fun add_thm opt_module thm = 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

38 
if Pattern.pattern (lhs_of thm) then 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

39 
RecCodegenData.map 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

40 
(Symtab.update_list ((fst o const_of o prop_of) thm, (thm, opt_module))) 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

41 
else tap (fn _ => warn thm) 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

42 
handle TERM _ => tap (fn _ => warn thm); 
12447  43 

24624
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

44 
fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

45 
(add_thm opt_module thm #> Code.add_liberal_func thm) I); 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

46 

b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

47 
val add_default = Thm.declaration_attribute (fn thm => Context.mapping 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

48 
(add_thm NONE thm #> Code.add_default_func thm) I); 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

49 

b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

50 
fun del_thm thm = case try const_of (prop_of thm) 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

51 
of SOME (s, _) => RecCodegenData.map 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

52 
(Symtab.map_entry s (remove (Thm.eq_thm o apsnd fst) thm)) 
b8383b1bbae3
distinction between regular and default code theorems
haftmann
parents:
24584
diff
changeset

53 
 NONE => tap (fn _ => warn thm); 
19344  54 

55 
val del = Thm.declaration_attribute 

24219  56 
(fn thm => Context.mapping (del_thm thm #> Code.del_func thm) I) 
14196  57 

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

58 
fun del_redundant thy eqs [] = eqs 
694f9d3ce90d
Reimplemented some operations on "code lemma" table to avoid that code
berghofe
parents:
15257
diff
changeset

59 
 del_redundant thy eqs (eq :: eqs') = 
694f9d3ce90d
Reimplemented some operations on "code lemma" table to avoid that code
berghofe
parents:
15257
diff
changeset

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

61 
val matches = curry 
17203  62 
(Pattern.matches thy o pairself (lhs_of o fst)) 
15321
694f9d3ce90d
Reimplemented some operations on "code lemma" table to avoid that code
berghofe
parents:
15257
diff
changeset

63 
in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end; 
694f9d3ce90d
Reimplemented some operations on "code lemma" table to avoid that code
berghofe
parents:
15257
diff
changeset

64 

16645  65 
fun get_equations thy defs (s, T) = 
20597  66 
(case Symtab.lookup (RecCodegenData.get thy) s of 
16645  67 
NONE => ([], "") 
68 
 SOME thms => 

69 
let val thms' = del_redundant thy [] 

24907
bfb2e82b61fe
Codegen.is_instance: raw match, ignore sort constraints;
wenzelm
parents:
24624
diff
changeset

70 
(filter (fn (thm, _) => is_instance T 
16645  71 
(snd (const_of (prop_of thm)))) thms) 
72 
in if null thms' then ([], "") 

73 
else (preprocess thy (map fst thms'), 

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

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

76 
NONE => thyname_of_const s thy 

77 
 SOME ((_, (thyname, _)), _) => thyname) 

78 
 SOME thyname => thyname) 

79 
end); 

12447  80 

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

84 
exception EQN of string * typ * string; 

85 

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

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

12447  89 

17144  90 
fun add_rec_funs thy defs gr dep eqs module = 
12447  91 
let 
16645  92 
fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t), 
93 
dest_eqn (rename_term t)); 

12447  94 
val eqs' = map dest_eq eqs; 
95 
val (dname, _) :: _ = eqs'; 

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

97 

17144  98 
fun mk_fundef module fname prfx gr [] = (gr, []) 
21410  99 
 mk_fundef module fname prfx gr ((fname' : string, (lhs, rhs)) :: xs) = 
12447  100 
let 
17144  101 
val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs); 
102 
val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs); 

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

12447  104 
in 
105 
(gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  " else prfx), 

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

107 
end; 

108 

17144  109 
fun put_code module fundef = map_node dname 
110 
(K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0, 

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

113 
in 

17144  114 
(case try (get_node gr) dname of 
15531  115 
NONE => 
12447  116 
let 
17144  117 
val gr1 = add_edge (dname, dep) 
118 
(new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); 

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

12447  120 
val xs = cycle gr2 ([], dname); 
17144  121 
val cs = map (fn x => case get_node gr2 x of 
16645  122 
(SOME (EQN (s, T, _)), _, _) => (s, T) 
12447  123 
 _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ 
124 
implode (separate ", " xs))) xs 

125 
in (case xs of 

17144  126 
[_] => (put_code module fundef gr2, module) 
12447  127 
 _ => 
128 
if not (dep mem xs) then 

129 
let 

16645  130 
val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; 
17144  131 
val module' = if_library thyname module; 
16645  132 
val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss)); 
17144  133 
val (gr3, fundef') = mk_fundef module' "" "fun " 
134 
(add_edge (dname, dep) 

135 
(foldr (uncurry new_node) (del_nodes xs gr2) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

136 
(map (fn k => 
17144  137 
(k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs'' 
138 
in (put_code module' fundef' gr3, module') end 

139 
else (gr2, module)) 

12447  140 
end 
17144  141 
 SOME (SOME (EQN (_, _, s)), module', _) => 
142 
(if s = "" then 

143 
if dname = dep then gr else add_edge (dname, dep) gr 

144 
else if s = dep then gr else add_edge (s, dep) gr, 

145 
module')) 

12447  146 
end; 
147 

17144  148 
fun recfun_codegen thy defs gr dep module brack t = (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

149 
(Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of 
16645  150 
(([], _), _) => NONE 
15531  151 
 (_, SOME _) => NONE 
17144  152 
 ((eqns, thyname), NONE) => 
16645  153 
let 
17144  154 
val module' = if_library thyname module; 
16645  155 
val (gr', ps) = foldl_map 
17144  156 
(invoke_codegen thy defs dep module true) (gr, ts); 
157 
val suffix = mk_suffix thy defs p; 

158 
val (gr'', module'') = 

159 
add_rec_funs thy defs gr' dep (map prop_of eqns) module'; 

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

12447  161 
in 
17144  162 
SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps) 
12447  163 
end) 
15531  164 
 _ => NONE); 
12447  165 

166 

18708  167 
val setup = 
24219  168 
add_codegen "recfun" recfun_codegen 
169 
#> Code.add_attribute ("", Args.del  Scan.succeed del 

21128  170 
 Scan.option (Args.$$$ "target"  Args.colon  Args.name) >> add); 
12447  171 

172 
end; 