author  berghofe 
Wed, 13 Nov 2002 15:28:41 +0100  
changeset 13708  a3a410782c95 
parent 13105  3d1e7a199bdc 
child 14196  be5e838f37bd 
permissions  rwrr 
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; 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12556
diff
changeset

27 
val merge = Symtab.merge_multi Drule.eq_thm_prop; 
12447  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; 