43 fun mk_tyexpr [] s = Codegen.str s |
44 fun mk_tyexpr [] s = Codegen.str s |
44 | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)] |
45 | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)] |
45 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
46 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
46 |
47 |
47 fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr = |
48 fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr = |
48 (case Typedef.get_info thy s of |
49 (case Typedef.get_info_global thy s of |
49 NONE => NONE |
50 (* FIXME handle multiple typedef interpretations (!??) *) |
50 | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} => |
51 [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] => |
51 if is_some (Codegen.get_assoc_type thy tname) then NONE else |
52 if is_some (Codegen.get_assoc_type thy tname) then NONE |
52 let |
53 else |
53 val module' = Codegen.if_library |
54 let |
54 (Codegen.thyname_of_type thy tname) module; |
55 val module' = Codegen.if_library |
55 val node_id = tname ^ " (type)"; |
56 (Codegen.thyname_of_type thy tname) module; |
56 val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map |
57 val node_id = tname ^ " (type)"; |
57 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) |
58 val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map |
58 Ts ||>> |
59 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) |
59 Codegen.mk_const_id module' Abs_name ||>> |
60 Ts ||>> |
60 Codegen.mk_const_id module' Rep_name ||>> |
61 Codegen.mk_const_id module' Abs_name ||>> |
61 Codegen.mk_type_id module' s; |
62 Codegen.mk_const_id module' Rep_name ||>> |
62 val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id) |
63 Codegen.mk_type_id module' s; |
63 in SOME (tyexpr, case try (Codegen.get_node gr') node_id of |
64 val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id) |
64 NONE => |
65 in |
65 let |
66 SOME (tyexpr, case try (Codegen.get_node gr') node_id of |
66 val (p :: ps, gr'') = fold_map |
67 NONE => |
67 (Codegen.invoke_tycodegen thy defs node_id module' false) |
68 let |
68 (oldT :: Us) (Codegen.add_edge (node_id, dep) |
69 val (p :: ps, gr'') = fold_map |
69 (Codegen.new_node (node_id, (NONE, "", "")) gr')); |
70 (Codegen.invoke_tycodegen thy defs node_id module' false) |
70 val s = |
71 (oldT :: Us) (Codegen.add_edge (node_id, dep) |
71 Codegen.string_of (Pretty.block [Codegen.str "datatype ", |
72 (Codegen.new_node (node_id, (NONE, "", "")) gr')); |
72 mk_tyexpr ps (snd ty_id), |
73 val s = |
73 Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"), |
74 Codegen.string_of (Pretty.block [Codegen.str "datatype ", |
74 Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^ |
75 mk_tyexpr ps (snd ty_id), |
75 Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), |
76 Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"), |
76 Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, |
77 Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^ |
77 Codegen.str "x) = x;"]) ^ "\n\n" ^ |
78 Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), |
78 (if "term_of" mem !Codegen.mode then |
79 Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, |
79 Codegen.string_of (Pretty.block [Codegen.str "fun ", |
80 Codegen.str "x) = x;"]) ^ "\n\n" ^ |
80 Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, |
81 (if "term_of" mem !Codegen.mode then |
81 Codegen.str ("(" ^ Abs_id), Pretty.brk 1, |
82 Codegen.string_of (Pretty.block [Codegen.str "fun ", |
82 Codegen.str "x) =", Pretty.brk 1, |
83 Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, |
83 Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","), |
84 Codegen.str ("(" ^ Abs_id), Pretty.brk 1, |
84 Pretty.brk 1, Codegen.mk_type false (oldT --> newT), |
85 Codegen.str "x) =", Pretty.brk 1, |
85 Codegen.str ")"], Codegen.str " $", Pretty.brk 1, |
86 Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","), |
86 Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, |
87 Pretty.brk 1, Codegen.mk_type false (oldT --> newT), |
87 Codegen.str "x;"]) ^ "\n\n" |
88 Codegen.str ")"], Codegen.str " $", Pretty.brk 1, |
88 else "") ^ |
89 Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, |
89 (if "test" mem !Codegen.mode then |
90 Codegen.str "x;"]) ^ "\n\n" |
90 Codegen.string_of (Pretty.block [Codegen.str "fun ", |
91 else "") ^ |
91 Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, |
92 (if "test" mem !Codegen.mode then |
92 Codegen.str "i =", Pretty.brk 1, |
93 Codegen.string_of (Pretty.block [Codegen.str "fun ", |
93 Pretty.block [Codegen.str (Abs_id ^ " ("), |
94 Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, |
94 Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1, |
95 Codegen.str "i =", Pretty.brk 1, |
95 Codegen.str "i);"]]) ^ "\n\n" |
96 Pretty.block [Codegen.str (Abs_id ^ " ("), |
96 else "") |
97 Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1, |
97 in Codegen.map_node node_id (K (NONE, module', s)) gr'' end |
98 Codegen.str "i);"]]) ^ "\n\n" |
98 | SOME _ => Codegen.add_edge (node_id, dep) gr') |
99 else "") |
99 end) |
100 in Codegen.map_node node_id (K (NONE, module', s)) gr'' end |
|
101 | SOME _ => Codegen.add_edge (node_id, dep) gr') |
|
102 end |
|
103 | _ => NONE) |
100 | typedef_tycodegen thy defs dep module brack _ gr = NONE; |
104 | typedef_tycodegen thy defs dep module brack _ gr = NONE; |
101 |
105 |
102 val setup = |
106 val setup = |
103 Codegen.add_codegen "typedef" typedef_codegen |
107 Codegen.add_codegen "typedef" typedef_codegen |
104 #> Codegen.add_tycodegen "typedef" typedef_tycodegen |
108 #> Codegen.add_tycodegen "typedef" typedef_tycodegen |