equal
deleted
inserted
replaced
60 fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs; |
60 fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs; |
61 fun print _ _ = (); |
61 fun print _ _ = (); |
62 end); |
62 end); |
63 |
63 |
64 fun put_typedef newT oldT Abs_name Rep_name = |
64 fun put_typedef newT oldT Abs_name Rep_name = |
65 TypedefData.map (Symtab.curried_update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name))); |
65 TypedefData.map (Symtab.update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name))); |
66 |
66 |
67 |
67 |
68 |
68 |
69 (** type declarations **) |
69 (** type declarations **) |
70 |
70 |
297 val (gr'', ps) = |
297 val (gr'', ps) = |
298 foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts); |
298 foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts); |
299 val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') |
299 val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') |
300 in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; |
300 in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; |
301 fun lookup f T = |
301 fun lookup f T = |
302 (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of |
302 (case Symtab.lookup (TypedefData.get thy) (get_name T) of |
303 NONE => "" |
303 NONE => "" |
304 | SOME s => f s); |
304 | SOME s => f s); |
305 in |
305 in |
306 (case strip_comb t of |
306 (case strip_comb t of |
307 (Const (s, Type ("fun", [T, U])), ts) => |
307 (Const (s, Type ("fun", [T, U])), ts) => |
318 fun mk_tyexpr [] s = Pretty.str s |
318 fun mk_tyexpr [] s = Pretty.str s |
319 | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] |
319 | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] |
320 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
320 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
321 |
321 |
322 fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = |
322 fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = |
323 (case Symtab.curried_lookup (TypedefData.get thy) s of |
323 (case Symtab.lookup (TypedefData.get thy) s of |
324 NONE => NONE |
324 NONE => NONE |
325 | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => |
325 | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => |
326 if is_some (Codegen.get_assoc_type thy tname) then NONE else |
326 if is_some (Codegen.get_assoc_type thy tname) then NONE else |
327 let |
327 let |
328 val module' = Codegen.if_library |
328 val module' = Codegen.if_library |