equal
deleted
inserted
replaced
198 [Pretty.str "i", Pretty.str "i"]))]) @ |
198 [Pretty.str "i", Pretty.str "i"]))]) @ |
199 mk_gen_of_def gr "and " xs |
199 mk_gen_of_def gr "and " xs |
200 end |
200 end |
201 |
201 |
202 in |
202 in |
203 (add_edge_acyclic (node_id, dep) gr |
203 ((add_edge_acyclic (node_id, dep) gr |
204 handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ => |
204 handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ => |
205 let |
205 let |
206 val gr1 = add_edge (node_id, dep) |
206 val gr1 = add_edge (node_id, dep) |
207 (new_node (node_id, (NONE, "", "")) gr); |
207 (new_node (node_id, (NONE, "", "")) gr); |
208 val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr'; |
208 val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr'; |
216 else "") ^ |
216 else "") ^ |
217 (if "test" mem !mode then |
217 (if "test" mem !mode then |
218 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk |
218 Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk |
219 (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" |
219 (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n" |
220 else ""))) gr2 |
220 else ""))) gr2 |
221 end |
221 end, |
|
222 module') |
222 end; |
223 end; |
223 |
224 |
224 |
225 |
225 (**** case expressions ****) |
226 (**** case expressions ****) |
226 |
227 |
312 | SOME {descr, ...} => |
313 | SOME {descr, ...} => |
313 if isSome (get_assoc_type thy s) then NONE else |
314 if isSome (get_assoc_type thy s) then NONE else |
314 let |
315 let |
315 val (gr', ps) = foldl_map |
316 val (gr', ps) = foldl_map |
316 (invoke_tycodegen thy defs dep module false) (gr, Ts); |
317 (invoke_tycodegen thy defs dep module false) (gr, Ts); |
317 val gr'' = add_dt_defs thy defs dep module gr' descr |
318 val (gr'', module') = add_dt_defs thy defs dep module gr' descr; |
318 in SOME (gr'', |
319 val (gr''', tyid) = mk_type_id module' s gr'' |
|
320 in SOME (gr''', |
319 Pretty.block ((if null Ts then [] else |
321 Pretty.block ((if null Ts then [] else |
320 [mk_tuple ps, Pretty.str " "]) @ |
322 [mk_tuple ps, Pretty.str " "]) @ |
321 [Pretty.str (mk_qual_id module (get_type_id s gr''))])) |
323 [Pretty.str (mk_qual_id module tyid)])) |
322 end) |
324 end) |
323 | datatype_tycodegen _ _ _ _ _ _ _ = NONE; |
325 | datatype_tycodegen _ _ _ _ _ _ _ = NONE; |
324 |
326 |
325 |
327 |
326 (** datatypes for code 2nd generation **) |
328 (** datatypes for code 2nd generation **) |