37 val xs = sort (int_ord o pairself snd) |
37 val xs = sort (int_ord o pairself snd) |
38 (List.mapPartial (fn (s, dts) => Option.map (pair s) |
38 (List.mapPartial (fn (s, dts) => Option.map (pair s) |
39 (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) |
39 (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs) |
40 in case xs of [] => NONE | x :: _ => SOME x end; |
40 in case xs of [] => NONE | x :: _ => SOME x end; |
41 |
41 |
42 fun add_dt_defs thy defs dep gr (descr: DatatypeAux.descr) = |
42 fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) = |
43 let |
43 let |
44 val sg = sign_of thy; |
44 val sg = sign_of thy; |
45 val tab = DatatypePackage.get_datatypes thy; |
45 val tab = DatatypePackage.get_datatypes thy; |
46 |
46 |
47 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
47 val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; |
48 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
48 val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => |
49 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
49 exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); |
50 |
50 |
51 val (_, (tname, _, (dname, _) :: _)) :: _ = descr'; |
51 val (_, (tname, _, _)) :: _ = descr'; |
52 val thyname = thyname_of_type tname thy; |
52 val node_id = tname ^ " (type)"; |
|
53 val module' = if_library (thyname_of_type tname thy) module; |
53 |
54 |
54 fun mk_dtdef gr prfx [] = (gr, []) |
55 fun mk_dtdef gr prfx [] = (gr, []) |
55 | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) = |
56 | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) = |
56 let |
57 let |
57 val tvs = map DatatypeAux.dest_DtTFree dts; |
58 val tvs = map DatatypeAux.dest_DtTFree dts; |
58 val sorts = map (rpair []) tvs; |
59 val sorts = map (rpair []) tvs; |
59 val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; |
60 val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; |
60 val (gr', ps) = foldl_map (fn (gr, (cname, cargs)) => |
61 val (gr', (_, type_id)) = mk_type_id module' tname gr; |
61 apsnd (pair cname) (foldl_map |
62 val (gr'', ps) = |
62 (invoke_tycodegen thy defs dname thyname false) (gr, cargs))) (gr, cs'); |
63 foldl_map (fn (gr, (cname, cargs)) => |
63 val (gr'', rest) = mk_dtdef gr' "and " xs |
64 foldl_map (invoke_tycodegen thy defs node_id module' false) |
|
65 (gr, cargs) |>>> |
|
66 mk_const_id module' cname) (gr', cs'); |
|
67 val (gr''', rest) = mk_dtdef gr'' "and " xs |
64 in |
68 in |
65 (gr'', |
69 (gr''', |
66 Pretty.block (Pretty.str prfx :: |
70 Pretty.block (Pretty.str prfx :: |
67 (if null tvs then [] else |
71 (if null tvs then [] else |
68 [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @ |
72 [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @ |
69 [Pretty.str (mk_type_id sg thyname thyname tname ^ " ="), Pretty.brk 1] @ |
73 [Pretty.str (type_id ^ " ="), Pretty.brk 1] @ |
70 List.concat (separate [Pretty.brk 1, Pretty.str "| "] |
74 List.concat (separate [Pretty.brk 1, Pretty.str "| "] |
71 (map (fn (cname, ps') => [Pretty.block |
75 (map (fn (ps', (_, cname)) => [Pretty.block |
72 (Pretty.str (mk_const_id sg thyname thyname cname) :: |
76 (Pretty.str cname :: |
73 (if null ps' then [] else |
77 (if null ps' then [] else |
74 List.concat ([Pretty.str " of", Pretty.brk 1] :: |
78 List.concat ([Pretty.str " of", Pretty.brk 1] :: |
75 separate [Pretty.str " *", Pretty.brk 1] |
79 separate [Pretty.str " *", Pretty.brk 1] |
76 (map single ps'))))]) ps))) :: rest) |
80 (map single ps'))))]) ps))) :: rest) |
77 end; |
81 end; |
78 |
82 |
79 fun mk_term_of_def prfx [] = [] |
83 fun mk_term_of_def gr prfx [] = [] |
80 | mk_term_of_def prfx ((_, (tname, dts, cs)) :: xs) = |
84 | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) = |
81 let |
85 let |
82 val tvs = map DatatypeAux.dest_DtTFree dts; |
86 val tvs = map DatatypeAux.dest_DtTFree dts; |
83 val sorts = map (rpair []) tvs; |
87 val sorts = map (rpair []) tvs; |
84 val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; |
88 val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs; |
85 val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts; |
89 val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts; |
86 val T = Type (tname, dts'); |
90 val T = Type (tname, dts'); |
87 val rest = mk_term_of_def "and " xs; |
91 val rest = mk_term_of_def gr "and " xs; |
88 val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) => |
92 val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) => |
89 let val args = map (fn i => |
93 let val args = map (fn i => |
90 Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts) |
94 Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts) |
91 in (" | ", Pretty.blk (4, |
95 in (" | ", Pretty.blk (4, |
92 [Pretty.str prfx, mk_term_of thy thyname false T, Pretty.brk 1, |
96 [Pretty.str prfx, mk_term_of gr module' false T, Pretty.brk 1, |
93 if null Ts then Pretty.str (mk_const_id sg thyname thyname cname) |
97 if null Ts then Pretty.str (snd (get_const_id cname gr)) |
94 else parens (Pretty.block |
98 else parens (Pretty.block |
95 [Pretty.str (mk_const_id sg thyname thyname cname), |
99 [Pretty.str (snd (get_const_id cname gr)), |
96 Pretty.brk 1, mk_tuple args]), |
100 Pretty.brk 1, mk_tuple args]), |
97 Pretty.str " =", Pretty.brk 1] @ |
101 Pretty.str " =", Pretty.brk 1] @ |
98 List.concat (separate [Pretty.str " $", Pretty.brk 1] |
102 List.concat (separate [Pretty.str " $", Pretty.brk 1] |
99 ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1, |
103 ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1, |
100 mk_type false (Ts ---> T), Pretty.str ")"] :: |
104 mk_type false (Ts ---> T), Pretty.str ")"] :: |
101 map (fn (x, U) => [Pretty.block [mk_term_of thy thyname false U, |
105 map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U, |
102 Pretty.brk 1, x]]) (args ~~ Ts))))) |
106 Pretty.brk 1, x]]) (args ~~ Ts))))) |
103 end) (prfx, cs') |
107 end) (prfx, cs') |
104 in eqs @ rest end; |
108 in eqs @ rest end; |
105 |
109 |
106 fun mk_gen_of_def prfx [] = [] |
110 fun mk_gen_of_def gr prfx [] = [] |
107 | mk_gen_of_def prfx ((i, (tname, dts, cs)) :: xs) = |
111 | mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) = |
108 let |
112 let |
109 val tvs = map DatatypeAux.dest_DtTFree dts; |
113 val tvs = map DatatypeAux.dest_DtTFree dts; |
110 val sorts = map (rpair []) tvs; |
114 val sorts = map (rpair []) tvs; |
111 val (cs1, cs2) = |
115 val (cs1, cs2) = |
112 List.partition (exists DatatypeAux.is_rec_type o snd) cs; |
116 List.partition (exists DatatypeAux.is_rec_type o snd) cs; |
164 else [Pretty.blk (4, separate (Pretty.brk 1) |
168 else [Pretty.blk (4, separate (Pretty.brk 1) |
165 (Pretty.str ("and " ^ gen_name) :: gs @ [Pretty.str "i"]) @ |
169 (Pretty.str ("and " ^ gen_name) :: gs @ [Pretty.str "i"]) @ |
166 [Pretty.str " =", Pretty.brk 1] @ |
170 [Pretty.str " =", Pretty.brk 1] @ |
167 separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @ |
171 separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @ |
168 [Pretty.str "i", Pretty.str "i"]))]) @ |
172 [Pretty.str "i", Pretty.str "i"]))]) @ |
169 mk_gen_of_def "and " xs |
173 mk_gen_of_def gr "and " xs |
170 end |
174 end |
171 |
175 |
172 in |
176 in |
173 ((Graph.add_edge_acyclic (dname, dep) gr |
177 (add_edge_acyclic (node_id, dep) gr |
174 handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ => |
178 handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ => |
175 let |
179 let |
176 val gr1 = Graph.add_edge (dname, dep) |
180 val gr1 = add_edge (node_id, dep) |
177 (Graph.new_node (dname, (NONE, "", "")) gr); |
181 (new_node (node_id, (NONE, "", "")) gr); |
178 val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr'; |
182 val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr'; |
179 in |
183 in |
180 Graph.map_node dname (K (NONE, thyname, |
184 map_node node_id (K (NONE, module', |
181 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ |
185 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ |
182 [Pretty.str ";"])) ^ "\n\n" ^ |
186 [Pretty.str ";"])) ^ "\n\n" ^ |
183 (if "term_of" mem !mode then |
187 (if "term_of" mem !mode then |
184 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk |
188 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk |
185 (mk_term_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" |
189 (mk_term_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" |
186 else "") ^ |
190 else "") ^ |
187 (if "test" mem !mode then |
191 (if "test" mem !mode then |
188 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk |
192 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk |
189 (mk_gen_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" |
193 (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" |
190 else ""))) gr2 |
194 else ""))) gr2 |
191 end, thyname) |
195 end |
192 end; |
196 end; |
193 |
197 |
194 |
198 |
195 (**** case expressions ****) |
199 (**** case expressions ****) |
196 |
200 |
197 fun pretty_case thy defs gr dep thyname brack constrs (c as Const (_, T)) ts = |
201 fun pretty_case thy defs gr dep module brack constrs (c as Const (_, T)) ts = |
198 let val i = length constrs |
202 let val i = length constrs |
199 in if length ts <= i then |
203 in if length ts <= i then |
200 invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts (i+1)) |
204 invoke_codegen thy defs dep module brack (gr, eta_expand c ts (i+1)) |
201 else |
205 else |
202 let |
206 let |
203 val ts1 = Library.take (i, ts); |
207 val ts1 = Library.take (i, ts); |
204 val t :: ts2 = Library.drop (i, ts); |
208 val t :: ts2 = Library.drop (i, ts); |
205 val names = foldr add_term_names |
209 val names = foldr add_term_names |
211 let |
215 let |
212 val j = length cargs; |
216 val j = length cargs; |
213 val xs = variantlist (replicate j "x", names); |
217 val xs = variantlist (replicate j "x", names); |
214 val Us' = Library.take (j, fst (strip_type U)); |
218 val Us' = Library.take (j, fst (strip_type U)); |
215 val frees = map Free (xs ~~ Us'); |
219 val frees = map Free (xs ~~ Us'); |
216 val (gr0, cp) = invoke_codegen thy defs dep thyname false |
220 val (gr0, cp) = invoke_codegen thy defs dep module false |
217 (gr, list_comb (Const (cname, Us' ---> dT), frees)); |
221 (gr, list_comb (Const (cname, Us' ---> dT), frees)); |
218 val t' = Envir.beta_norm (list_comb (t, frees)); |
222 val t' = Envir.beta_norm (list_comb (t, frees)); |
219 val (gr1, p) = invoke_codegen thy defs dep thyname false (gr0, t'); |
223 val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t'); |
220 val (ps, gr2) = pcase gr1 cs ts Us; |
224 val (ps, gr2) = pcase gr1 cs ts Us; |
221 in |
225 in |
222 ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2) |
226 ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2) |
223 end; |
227 end; |
224 |
228 |
225 val (ps1, gr1) = pcase gr constrs ts1 Ts; |
229 val (ps1, gr1) = pcase gr constrs ts1 Ts; |
226 val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1); |
230 val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1); |
227 val (gr2, p) = invoke_codegen thy defs dep thyname false (gr1, t); |
231 val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t); |
228 val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep thyname true) (gr2, ts2) |
232 val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2) |
229 in (gr3, (if not (null ts2) andalso brack then parens else I) |
233 in (gr3, (if not (null ts2) andalso brack then parens else I) |
230 (Pretty.block (separate (Pretty.brk 1) |
234 (Pretty.block (separate (Pretty.brk 1) |
231 (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of", |
235 (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of", |
232 Pretty.brk 1] @ ps @ [Pretty.str ")"]) :: ps2)))) |
236 Pretty.brk 1] @ ps @ [Pretty.str ")"]) :: ps2)))) |
233 end |
237 end |
234 end; |
238 end; |
235 |
239 |
236 |
240 |
237 (**** constructors ****) |
241 (**** constructors ****) |
238 |
242 |
239 fun pretty_constr thy defs gr dep thyname brack args (c as Const (s, T)) ts = |
243 fun pretty_constr thy defs gr dep module brack args (c as Const (s, T)) ts = |
240 let val i = length args |
244 let val i = length args |
241 in if i > 1 andalso length ts < i then |
245 in if i > 1 andalso length ts < i then |
242 invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts i) |
246 invoke_codegen thy defs dep module brack (gr, eta_expand c ts i) |
243 else |
247 else |
244 let |
248 let |
245 val thyname' = thyname_of_type (fst (dest_Type (body_type T))) thy; |
249 val id = mk_qual_id module (get_const_id s gr); |
246 val id = mk_const_id (sign_of thy) thyname thyname' s; |
|
247 val (gr', ps) = foldl_map |
250 val (gr', ps) = foldl_map |
248 (invoke_codegen thy defs dep thyname (i = 1)) (gr, ts); |
251 (invoke_codegen thy defs dep module (i = 1)) (gr, ts); |
249 in (case args of |
252 in (case args of |
250 _ :: _ :: _ => (gr', (if brack then parens else I) |
253 _ :: _ :: _ => (gr', (if brack then parens else I) |
251 (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps])) |
254 (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps])) |
252 | _ => (gr', mk_app brack (Pretty.str id) ps)) |
255 | _ => (gr', mk_app brack (Pretty.str id) ps)) |
253 end |
256 end |
254 end; |
257 end; |
255 |
258 |
256 |
259 |
257 (**** code generators for terms and types ****) |
260 (**** code generators for terms and types ****) |
258 |
261 |
259 fun datatype_codegen thy defs gr dep thyname brack t = (case strip_comb t of |
262 fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of |
260 (c as Const (s, T), ts) => |
263 (c as Const (s, T), ts) => |
261 (case find_first (fn (_, {index, descr, case_name, ...}) => |
264 (case find_first (fn (_, {index, descr, case_name, ...}) => |
262 s = case_name orelse |
265 s = case_name orelse |
263 isSome (assoc (#3 (valOf (assoc (descr, index))), s))) |
266 isSome (assoc (#3 (valOf (assoc (descr, index))), s))) |
264 (Symtab.dest (DatatypePackage.get_datatypes thy)) of |
267 (Symtab.dest (DatatypePackage.get_datatypes thy)) of |
265 NONE => NONE |
268 NONE => NONE |
266 | SOME (tname, {index, descr, ...}) => |
269 | SOME (tname, {index, descr, ...}) => |
267 if isSome (get_assoc_code thy s T) then NONE else |
270 if isSome (get_assoc_code thy s T) then NONE else |
268 let val SOME (_, _, constrs) = assoc (descr, index) |
271 let val SOME (_, _, constrs) = assoc (descr, index) |
269 in (case (assoc (constrs, s), strip_type T) of |
272 in (case (assoc (constrs, s), strip_type T) of |
270 (NONE, _) => SOME (pretty_case thy defs gr dep thyname brack |
273 (NONE, _) => SOME (pretty_case thy defs gr dep module brack |
271 (#3 (valOf (assoc (descr, index)))) c ts) |
274 (#3 (valOf (assoc (descr, index)))) c ts) |
272 | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs |
275 | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs |
273 (fst (invoke_tycodegen thy defs dep thyname false |
276 (fst (invoke_tycodegen thy defs dep module false |
274 (gr, snd (strip_type T)))) |
277 (gr, snd (strip_type T)))) |
275 dep thyname brack args c ts) |
278 dep module brack args c ts) |
276 | _ => NONE) |
279 | _ => NONE) |
277 end) |
280 end) |
278 | _ => NONE); |
281 | _ => NONE); |
279 |
282 |
280 fun datatype_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = |
283 fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) = |
281 (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of |
284 (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of |
282 NONE => NONE |
285 NONE => NONE |
283 | SOME {descr, ...} => |
286 | SOME {descr, ...} => |
284 if isSome (get_assoc_type thy s) then NONE else |
287 if isSome (get_assoc_type thy s) then NONE else |
285 let |
288 let |
286 val (gr', ps) = foldl_map |
289 val (gr', ps) = foldl_map |
287 (invoke_tycodegen thy defs dep thyname false) (gr, Ts); |
290 (invoke_tycodegen thy defs dep module false) (gr, Ts); |
288 val (gr'', thyname') = add_dt_defs thy defs dep gr' descr |
291 val gr'' = add_dt_defs thy defs dep module gr' descr |
289 in SOME (gr'', |
292 in SOME (gr'', |
290 Pretty.block ((if null Ts then [] else |
293 Pretty.block ((if null Ts then [] else |
291 [mk_tuple ps, Pretty.str " "]) @ |
294 [mk_tuple ps, Pretty.str " "]) @ |
292 [Pretty.str (mk_type_id (sign_of thy) thyname thyname' s)])) |
295 [Pretty.str (mk_qual_id module (get_type_id s gr''))])) |
293 end) |
296 end) |
294 | datatype_tycodegen _ _ _ _ _ _ _ = NONE; |
297 | datatype_tycodegen _ _ _ _ _ _ _ = NONE; |
295 |
298 |
296 |
299 |
297 val setup = |
300 val setup = |