author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 30076  f3043dafef5f 
child 30242  aea5d7fa7ef5 
permissions  rwrr 
24589  1 
(* Title: HOL/Tools/datatype_codegen.ML 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset

2 
Author: Stefan Berghofer and Florian Haftmann, TU Muenchen 
12445  3 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

4 
Code generator facilities for inductive datatypes. 
12445  5 
*) 
6 

7 
signature DATATYPE_CODEGEN = 

8 
sig 

30076  9 
val mk_eq: theory > string > thm list 
10 
val mk_case_cert: theory > string > thm 

18708  11 
val setup: theory > theory 
12445  12 
end; 
13 

14 
structure DatatypeCodegen : DATATYPE_CODEGEN = 

15 
struct 

16 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

17 
(** SML code generator **) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

18 

12445  19 
open Codegen; 
20 

21 
(**** datatype definition ****) 

22 

14104  23 
(* find shortest path to constructor with no recursive arguments *) 
24 

25 
fun find_nonempty (descr: DatatypeAux.descr) is i = 

26 
let 

17521  27 
val (_, _, constrs) = valOf (AList.lookup (op =) descr i); 
15531  28 
fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE 
15570  29 
else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i) 
15531  30 
 arg_nonempty _ = SOME 0; 
15570  31 
fun max xs = Library.foldl 
15531  32 
(fn (NONE, _) => NONE 
33 
 (SOME i, SOME j) => SOME (Int.max (i, j)) 

34 
 (_, NONE) => NONE) (SOME 0, xs); 

14104  35 
val xs = sort (int_ord o pairself snd) 
15570  36 
(List.mapPartial (fn (s, dts) => Option.map (pair s) 
14104  37 
(max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) 
15531  38 
in case xs of [] => NONE  x :: _ => SOME x end; 
14104  39 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

40 
fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr = 
12445  41 
let 
15570  42 
val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; 
43 
val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => 

14104  44 
exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); 
12445  45 

17144  46 
val (_, (tname, _, _)) :: _ = descr'; 
47 
val node_id = tname ^ " (type)"; 

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

48 
val module' = if_library (thyname_of_type thy tname) module; 
12445  49 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

50 
fun mk_dtdef prfx [] gr = ([], gr) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

51 
 mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr = 
12445  52 
let 
53 
val tvs = map DatatypeAux.dest_DtTFree dts; 

54 
val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

55 
val ((_, type_id), gr') = mk_type_id module' tname gr; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

56 
val (ps, gr'') = gr' > 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

57 
fold_map (fn (cname, cargs) => 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

58 
fold_map (invoke_tycodegen thy defs node_id module' false) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

59 
cargs ##>> 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

60 
mk_const_id module' cname) cs'; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

61 
val (rest, gr''') = mk_dtdef "and " xs gr'' 
12445  62 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

63 
(Pretty.block (str prfx :: 
12445  64 
(if null tvs then [] else 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

65 
[mk_tuple (map str tvs), str " "]) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

66 
[str (type_id ^ " ="), Pretty.brk 1] @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

67 
List.concat (separate [Pretty.brk 1, str " "] 
17144  68 
(map (fn (ps', (_, cname)) => [Pretty.block 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

69 
(str cname :: 
12445  70 
(if null ps' then [] else 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

71 
List.concat ([str " of", Pretty.brk 1] :: 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

72 
separate [str " *", Pretty.brk 1] 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

73 
(map single ps'))))]) ps))) :: rest, gr''') 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

74 
end; 
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

75 

25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

76 
fun mk_constr_term cname Ts T ps = 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

77 
List.concat (separate [str " $", Pretty.brk 1] 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

78 
([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

79 
mk_type false (Ts > T), str ")"] :: ps)); 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

80 

17144  81 
fun mk_term_of_def gr prfx [] = [] 
82 
 mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) = 

13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

83 
let 
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

84 
val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; 
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

85 
val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts; 
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

86 
val T = Type (tname, dts'); 
17144  87 
val rest = mk_term_of_def gr "and " xs; 
30190  88 
val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) => 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

89 
let val args = map (fn i => 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

90 
str ("x" ^ string_of_int i)) (1 upto length Ts) 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

91 
in ("  ", Pretty.blk (4, 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

92 
[str prfx, mk_term_of gr module' false T, Pretty.brk 1, 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

93 
if null Ts then str (snd (get_const_id gr cname)) 
16645  94 
else parens (Pretty.block 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

95 
[str (snd (get_const_id gr cname)), 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

96 
Pretty.brk 1, mk_tuple args]), 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

97 
str " =", Pretty.brk 1] @ 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

98 
mk_constr_term cname Ts T 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

99 
(map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U, 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

100 
Pretty.brk 1, x]]) (args ~~ Ts)))) 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

101 
end) (prfx, cs') 
14104  102 
in eqs @ rest end; 
103 

17144  104 
fun mk_gen_of_def gr prfx [] = [] 
105 
 mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) = 

14104  106 
let 
107 
val tvs = map DatatypeAux.dest_DtTFree dts; 

25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

108 
val Us = map (DatatypeAux.typ_of_dtyp descr sorts) dts; 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

109 
val T = Type (tname, Us); 
14104  110 
val (cs1, cs2) = 
15570  111 
List.partition (exists DatatypeAux.is_rec_type o snd) cs; 
15531  112 
val SOME (cname, _) = find_nonempty descr [i] i; 
14104  113 

114 
fun mk_delay p = Pretty.block 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

115 
[str "fn () =>", Pretty.brk 1, p]; 
14104  116 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

117 
fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"]; 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

118 

15397
5260ac75e07c
Fixed bug in mk_gen_of_def that could cause nontermination of the generator
berghofe
parents:
14981
diff
changeset

119 
fun mk_constr s b (cname, dts) = 
14104  120 
let 
17144  121 
val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s 
15397
5260ac75e07c
Fixed bug in mk_gen_of_def that could cause nontermination of the generator
berghofe
parents:
14981
diff
changeset

122 
(DatatypeAux.typ_of_dtyp descr sorts dt)) 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

123 
[str (if b andalso DatatypeAux.is_rec_type dt then "0" 
15397
5260ac75e07c
Fixed bug in mk_gen_of_def that could cause nontermination of the generator
berghofe
parents:
14981
diff
changeset

124 
else "j")]) dts; 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

125 
val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts; 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

126 
val xs = map str 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

127 
(DatatypeProp.indexify_names (replicate (length dts) "x")); 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

128 
val ts = map str 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

129 
(DatatypeProp.indexify_names (replicate (length dts) "t")); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

130 
val (_, id) = get_const_id gr cname 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

131 
in 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

132 
mk_let 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

133 
(map2 (fn p => fn q => mk_tuple [p, q]) xs ts ~~ gs) 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

134 
(mk_tuple 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

135 
[case xs of 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

136 
_ :: _ :: _ => Pretty.block 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

137 
[str id, Pretty.brk 1, mk_tuple xs] 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

138 
 _ => mk_app false (str id) xs, 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

139 
mk_delay (Pretty.block (mk_constr_term cname Ts T 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

140 
(map (single o mk_force) ts)))]) 
14104  141 
end; 
142 

15397
5260ac75e07c
Fixed bug in mk_gen_of_def that could cause nontermination of the generator
berghofe
parents:
14981
diff
changeset

143 
fun mk_choice [c] = mk_constr "(i1)" false c 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

144 
 mk_choice cs = Pretty.block [str "one_of", 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

145 
Pretty.brk 1, Pretty.blk (1, str "[" :: 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

146 
List.concat (separate [str ",", Pretty.fbrk] 
15397
5260ac75e07c
Fixed bug in mk_gen_of_def that could cause nontermination of the generator
berghofe
parents:
14981
diff
changeset

147 
(map (single o mk_delay o mk_constr "(i1)" false) cs)) @ 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

148 
[str "]"]), Pretty.brk 1, str "()"]; 
14104  149 

25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

150 
val gs = maps (fn s => 
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

151 
let val s' = strip_tname s 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

152 
in [str (s' ^ "G"), str (s' ^ "T")] end) tvs; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

153 
val gen_name = "gen_" ^ snd (get_type_id gr tname) 
14104  154 

155 
in 

156 
Pretty.blk (4, separate (Pretty.brk 1) 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

157 
(str (prfx ^ gen_name ^ 
14104  158 
(if null cs1 then "" else "'")) :: gs @ 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

159 
(if null cs1 then [] else [str "i"]) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

160 
[str "j"]) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

161 
[str " =", Pretty.brk 1] @ 
14104  162 
(if not (null cs1) andalso not (null cs2) 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

163 
then [str "frequency", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

164 
Pretty.blk (1, [str "[", 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

165 
mk_tuple [str "i", mk_delay (mk_choice cs1)], 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

166 
str ",", Pretty.fbrk, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

167 
mk_tuple [str "1", mk_delay (mk_choice cs2)], 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

168 
str "]"]), Pretty.brk 1, str "()"] 
14104  169 
else if null cs2 then 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

170 
[Pretty.block [str "(case", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

171 
str "i", Pretty.brk 1, str "of", 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

172 
Pretty.brk 1, str "0 =>", Pretty.brk 1, 
17521  173 
mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)), 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

174 
Pretty.brk 1, str " _ =>", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

175 
mk_choice cs1, str ")"]] 
14104  176 
else [mk_choice cs2])) :: 
177 
(if null cs1 then [] 

178 
else [Pretty.blk (4, separate (Pretty.brk 1) 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

179 
(str ("and " ^ gen_name) :: gs @ [str "i"]) @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

180 
[str " =", Pretty.brk 1] @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

181 
separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

182 
[str "i", str "i"]))]) @ 
17144  183 
mk_gen_of_def gr "and " xs 
14104  184 
end 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

185 

12445  186 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

187 
(module', (add_edge_acyclic (node_id, dep) gr 
12445  188 
handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ => 
189 
let 

17144  190 
val gr1 = add_edge (node_id, dep) 
191 
(new_node (node_id, (NONE, "", "")) gr); 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

192 
val (dtdef, gr2) = mk_dtdef "datatype " descr' gr1 ; 
12445  193 
in 
17144  194 
map_node node_id (K (NONE, module', 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

195 
string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

196 
[str ";"])) ^ "\n\n" ^ 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

197 
(if "term_of" mem !mode then 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

198 
string_of (Pretty.blk (0, separate Pretty.fbrk 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

199 
(mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" 
14104  200 
else "") ^ 
201 
(if "test" mem !mode then 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

202 
string_of (Pretty.blk (0, separate Pretty.fbrk 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

203 
(mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" 
13754
021cf00435a9
Code generator for datatypes now also generates suitable term_of functions (when
berghofe
parents:
12890
diff
changeset

204 
else ""))) gr2 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

205 
end) 
12445  206 
end; 
207 

208 

209 
(**** case expressions ****) 

210 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

211 
fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr = 
12445  212 
let val i = length constrs 
213 
in if length ts <= i then 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

214 
invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr 
12445  215 
else 
216 
let 

15570  217 
val ts1 = Library.take (i, ts); 
218 
val t :: ts2 = Library.drop (i, ts); 

30190  219 
val names = List.foldr OldTerm.add_term_names 
220 
(map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1; 

15570  221 
val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T))); 
12445  222 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

223 
fun pcase [] [] [] gr = ([], gr) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

224 
 pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr = 
12445  225 
let 
226 
val j = length cargs; 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19886
diff
changeset

227 
val xs = Name.variant_list names (replicate j "x"); 
15570  228 
val Us' = Library.take (j, fst (strip_type U)); 
12445  229 
val frees = map Free (xs ~~ Us'); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

230 
val (cp, gr0) = invoke_codegen thy defs dep module false 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

231 
(list_comb (Const (cname, Us' > dT), frees)) gr; 
12445  232 
val t' = Envir.beta_norm (list_comb (t, frees)); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

233 
val (p, gr1) = invoke_codegen thy defs dep module false t' gr0; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

234 
val (ps, gr2) = pcase cs ts Us gr1; 
12445  235 
in 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

236 
([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2) 
12445  237 
end; 
238 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

239 
val (ps1, gr1) = pcase constrs ts1 Ts gr ; 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

240 
val ps = List.concat (separate [Pretty.brk 1, str " "] ps1); 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

241 
val (p, gr2) = invoke_codegen thy defs dep module false t gr1; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

242 
val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

243 
in ((if not (null ts2) andalso brack then parens else I) 
12445  244 
(Pretty.block (separate (Pretty.brk 1) 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

245 
(Pretty.block ([str "(case ", p, str " of", 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

246 
Pretty.brk 1] @ ps @ [str ")"]) :: ps2))), gr3) 
12445  247 
end 
248 
end; 

249 

250 

251 
(**** constructors ****) 

252 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

253 
fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr = 
12445  254 
let val i = length args 
255 
in if i > 1 andalso length ts < i then 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

256 
invoke_codegen thy defs dep module brack (eta_expand c ts i) gr 
12445  257 
else 
258 
let 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

259 
val id = mk_qual_id module (get_const_id gr s); 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

260 
val (ps, gr') = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

261 
(invoke_codegen thy defs dep module (i = 1)) ts gr; 
12445  262 
in (case args of 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

263 
_ :: _ :: _ => (if brack then parens else I) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

264 
(Pretty.block [str id, Pretty.brk 1, mk_tuple ps]) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

265 
 _ => (mk_app brack (str id) ps), gr') 
12445  266 
end 
267 
end; 

268 

269 

270 
(**** code generators for terms and types ****) 

271 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

272 
fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of 
12445  273 
(c as Const (s, T), ts) => 
22778
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

274 
(case DatatypePackage.datatype_of_case thy s of 
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

275 
SOME {index, descr, ...} => 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22778
diff
changeset

276 
if is_some (get_assoc_code thy (s, T)) then NONE else 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

277 
SOME (pretty_case thy defs dep module brack 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

278 
(#3 (the (AList.lookup op = descr index))) c ts gr ) 
22778
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

279 
 NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of 
28639
9788fb18a142
datatype_codegen now checks name of result type of constructor
berghofe
parents:
28537
diff
changeset

280 
(SOME {index, descr, ...}, (_, U as Type (tyname, _))) => 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22778
diff
changeset

281 
if is_some (get_assoc_code thy (s, T)) then NONE else 
28639
9788fb18a142
datatype_codegen now checks name of result type of constructor
berghofe
parents:
28537
diff
changeset

282 
let 
9788fb18a142
datatype_codegen now checks name of result type of constructor
berghofe
parents:
28537
diff
changeset

283 
val SOME (tyname', _, constrs) = AList.lookup op = descr index; 
9788fb18a142
datatype_codegen now checks name of result type of constructor
berghofe
parents:
28537
diff
changeset

284 
val SOME args = AList.lookup op = constrs s 
22778
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

285 
in 
28639
9788fb18a142
datatype_codegen now checks name of result type of constructor
berghofe
parents:
28537
diff
changeset

286 
if tyname <> tyname' then NONE 
9788fb18a142
datatype_codegen now checks name of result type of constructor
berghofe
parents:
28537
diff
changeset

287 
else SOME (pretty_constr thy defs 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

288 
dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr))) 
22778
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

289 
end 
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

290 
 _ => NONE) 
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

291 
 _ => NONE); 
12445  292 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

293 
fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr = 
22778
a5b87573f427
Streamlined datatype_codegen function using new datatype_of_case
berghofe
parents:
22746
diff
changeset

294 
(case DatatypePackage.get_datatype thy s of 
15531  295 
NONE => NONE 
25889
c93803252748
Test data generation and conversion to terms is now more closely
berghofe
parents:
25864
diff
changeset

296 
 SOME {descr, sorts, ...} => 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22778
diff
changeset

297 
if is_some (get_assoc_type thy s) then NONE else 
16645  298 
let 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

299 
val (ps, gr') = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

300 
(invoke_tycodegen thy defs dep module false) Ts gr; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

301 
val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

302 
val (tyid, gr''') = mk_type_id module' s gr'' 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

303 
in SOME (Pretty.block ((if null Ts then [] else 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26732
diff
changeset

304 
[mk_tuple ps, str " "]) @ 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28423
diff
changeset

305 
[str (mk_qual_id module tyid)]), gr''') 
12445  306 
end) 
16645  307 
 datatype_tycodegen _ _ _ _ _ _ _ = NONE; 
12445  308 

18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18220
diff
changeset

309 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

310 
(** generic code generator **) 
20105  311 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

312 
(* specification *) 
20426  313 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

314 
fun add_datatype_spec vs dtco cos thy = 
20835  315 
let 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

316 
val cs = map (fn (c, tys) => (c, tys > Type (dtco, map TFree vs))) cos; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

317 
in 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

318 
thy 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

319 
> try (Code.add_datatype cs) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

320 
> the_default thy 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

321 
end; 
21516  322 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

323 

d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

324 
(* case certificates *) 
19346  325 

30076  326 
fun mk_case_cert thy tyco = 
23811  327 
let 
328 
val raw_thms = 

329 
(#case_rewrites o DatatypePackage.the_datatype thy) tyco; 

330 
val thms as hd_thm :: _ = raw_thms 

331 
> Conjunction.intr_balanced 

24976
821628d16552
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24845
diff
changeset

332 
> Thm.unvarify 
23811  333 
> Conjunction.elim_balanced (length raw_thms) 
334 
> map Simpdata.mk_meta_eq 

335 
> map Drule.zero_var_indexes 

336 
val params = fold_aterms (fn (Free (v, _)) => insert (op =) v 

337 
 _ => I) (Thm.prop_of hd_thm) []; 

338 
val rhs = hd_thm 

339 
> Thm.prop_of 

340 
> Logic.dest_equals 

341 
> fst 

342 
> Term.strip_comb 

343 
> apsnd (fst o split_last) 

344 
> list_comb; 

345 
val lhs = Free (Name.variant params "case", Term.fastype_of rhs); 

346 
val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs); 

347 
in 

348 
thms 

349 
> Conjunction.intr_balanced 

350 
> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm] 

351 
> Thm.implies_intr asm 

352 
> Thm.generalize ([], params) 0 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25569
diff
changeset

353 
> AxClass.unoverload thy 
23811  354 
> Thm.varifyT 
355 
end; 

356 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

357 
fun add_datatype_cases dtco thy = 
25505  358 
let 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

359 
val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco; 
30076  360 
val cert = mk_case_cert thy dtco; 
361 
fun add_case_liberal thy = thy 

362 
> try (Code.add_case cert) 

363 
> the_default thy; 

20426  364 
in 
365 
thy 

30076  366 
> add_case_liberal 
28370  367 
> fold_rev Code.add_default_eqn case_rewrites 
20426  368 
end; 
369 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

370 

d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

371 
(* equality *) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

372 

d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

373 
local 
20426  374 

30076  375 
val not_sym = @{thm HOL.not_sym}; 
376 
val not_false_true = iffD2 OF [nth @{thms HOL.simp_thms} 7, TrueI]; 

377 
val refl = @{thm refl}; 

378 
val eqTrueI = @{thm eqTrueI}; 

20835  379 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

380 
fun mk_distinct cos = 
22423  381 
let 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

382 
fun sym_product [] = [] 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

383 
 sym_product (x::xs) = map (pair x) xs @ sym_product xs; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

384 
fun mk_co_args (co, tys) ctxt = 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

385 
let 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

386 
val names = Name.invents ctxt "a" (length tys); 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

387 
val ctxt' = fold Name.declare names ctxt; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

388 
val vs = map2 (curry Free) names tys; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

389 
in (vs, ctxt') end; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

390 
fun mk_dist ((co1, tys1), (co2, tys2)) = 
22423  391 
let 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

392 
val ((xs1, xs2), _) = Name.context 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

393 
> mk_co_args (co1, tys1) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

394 
>> mk_co_args (co2, tys2); 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

395 
val prem = HOLogic.mk_eq 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

396 
(list_comb (co1, xs1), list_comb (co2, xs2)); 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

397 
val t = HOLogic.mk_not prem; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

398 
in HOLogic.mk_Trueprop t end; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

399 
in map mk_dist (sym_product cos) end; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

400 

d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

401 
in 
20426  402 

30076  403 
fun mk_eq thy dtco = 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

404 
let 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

405 
val (vs, cs) = DatatypePackage.the_datatype_spec thy dtco; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

406 
fun mk_triv_inject co = 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

407 
let 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

408 
val ct' = Thm.cterm_of thy 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

409 
(Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs))) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

410 
val cty' = Thm.ctyp_of_term ct'; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

411 
val SOME (ct, cty) = fold_aterms (fn Var (v, ty) => 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

412 
(K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty)  _ => I) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

413 
(Thm.prop_of refl) NONE; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

414 
in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

415 
val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co)  _ => NONE) cs 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

416 
val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

417 
val ctxt = ProofContext.init thy; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

418 
val simpset = Simplifier.context ctxt 
29302  419 
(Simplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]); 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

420 
val cos = map (fn (co, tys) => 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

421 
(Const (co, tys > Type (dtco, map TFree vs)), tys)) cs; 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

422 
val tac = ALLGOALS (simp_tac simpset) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

423 
THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]); 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

424 
val distinct = 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

425 
mk_distinct cos 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

426 
> map (fn t => Goal.prove_global thy [] [] t (K tac)) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

427 
> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms) 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

428 
in inject1 @ inject2 @ distinct end; 
20426  429 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

430 
end; 
20835  431 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

432 
fun add_datatypes_equality vs dtcos thy = 
20597  433 
let 
26513  434 
val vs' = (map o apsnd) 
435 
(curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs; 

28350  436 
fun add_def dtco lthy = 
26513  437 
let 
28350  438 
val ty = Type (dtco, map TFree vs'); 
26513  439 
fun mk_side const_name = Const (const_name, ty > ty > HOLogic.boolT) 
440 
$ Free ("x", ty) $ Free ("y", ty); 

441 
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq 

26732  442 
(mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="})); 
26513  443 
val def' = Syntax.check_term lthy def; 
444 
val ((_, (_, thm)), lthy') = Specification.definition 

28965  445 
(NONE, (Attrib.empty_binding, def')) lthy; 
26513  446 
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy); 
447 
val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; 

448 
in (thm', lthy') end; 

449 
fun tac thms = Class.intro_classes_tac [] 

450 
THEN ALLGOALS (ProofContext.fact_tac thms); 

30076  451 
fun mk_eq' thy dtco = mk_eq thy dtco 
28423  452 
> map (Code_Unit.constrain_thm thy [HOLogic.class_eq]) 
26513  453 
> map Simpdata.mk_eq 
28423  454 
> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]) 
455 
> map (AxClass.unoverload thy); 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

456 
fun add_eq_thms dtco thy = 
20597  457 
let 
28350  458 
val ty = Type (dtco, map TFree vs'); 
24137
8d7896398147
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23811
diff
changeset

459 
val thy_ref = Theory.check_thy thy; 
26732  460 
val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco); 
28350  461 
val eq_refl = @{thm HOL.eq_refl} 
462 
> Thm.instantiate 

463 
([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []) 

28423  464 
> Simpdata.mk_eq 
465 
> AxClass.unoverload thy; 

30076  466 
fun mk_thms () = (eq_refl, false) 
467 
:: rev (map (rpair true) (mk_eq' (Theory.deref thy_ref) dtco)); 

20597  468 
in 
30076  469 
Code.add_eqnl (const, Lazy.lazy mk_thms) thy 
20597  470 
end; 
471 
in 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

472 
thy 
25864  473 
> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq]) 
26513  474 
> fold_map add_def dtcos 
475 
> (fn thms => Class.prove_instantiation_instance (K (tac thms)) 

28394  476 
#> LocalTheory.exit_global 
28370  477 
#> fold Code.del_eqn thms 
26513  478 
#> fold add_eq_thms dtcos) 
20597  479 
end; 
480 

20426  481 

482 
(** theory setup **) 

483 

25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

484 
fun add_datatype_code dtcos thy = 
23513  485 
let 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

486 
val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos; 
25489  487 
in 
25505  488 
thy 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

489 
> fold2 (add_datatype_spec vs) dtcos coss 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

490 
> fold add_datatype_cases dtcos 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

491 
> add_datatypes_equality vs dtcos 
25489  492 
end; 
493 

19008  494 
val setup = 
20597  495 
add_codegen "datatype" datatype_codegen 
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24624
diff
changeset

496 
#> add_tycodegen "datatype" datatype_tycodegen 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset

497 
#> DatatypePackage.interpretation add_datatype_code 
20597  498 

12445  499 
end; 