80 ML {* |
80 ML {* |
81 fun print_str_option NONE = "NONE" |
81 fun print_str_option NONE = "NONE" |
82 | print_str_option (SOME s) = (s:bstring) |
82 | print_str_option (SOME s) = (s:bstring) |
83 *} |
83 *} |
84 |
84 |
85 ML {* |
85 ML {* |
86 fun print_anno_typ (NONE, ty) = ty |
86 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty |
87 | print_anno_typ (SOME x, ty) = x ^ ":" ^ ty |
87 | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty |
88 *} |
88 *} |
89 |
89 |
90 ML {* |
90 ML {* |
91 fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2 |
91 fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2 |
92 | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2 |
92 | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2 |
93 *} |
93 *} |
94 |
94 |
95 ML {* |
95 ML {* |
96 fun print_constr (((name, anno_tys), bds), syn) = |
96 fun print_constr lthy (((name, anno_tys), bds), syn) = |
97 (Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ " " |
97 (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
100 *} |
100 *} |
101 |
101 |
102 ML Local_Theory.exit_global |
102 ML Local_Theory.exit_global |
103 |
103 |
104 ML {* |
104 (* TODO: replace with proper thing *) |
105 fun fv_constr prefix (((name, anno_tys), bds), syn) = |
105 ML {* |
106 prefix ^ " (" ^ (Binding.name_of name) ^ ") = " |
106 fun is_atom ty = Binding.name_of ty = "name" |
107 *} |
107 *} |
108 |
108 |
109 ML {* |
109 ML {* |
110 fun single_dt (((s2, s3), syn), constrs) = |
110 fun fv_constr lthy prefix (((name, anno_tys), bds), syn) = |
|
111 let |
|
112 fun prepare_name (NONE, ty) = ("", ty) |
|
113 | prepare_name (SOME n, ty) = (n, ty); |
|
114 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
|
115 val var_strs = map (Syntax.string_of_term lthy) vars; |
|
116 in |
|
117 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " |
|
118 end |
|
119 *} |
|
120 |
|
121 ML {* |
|
122 fun single_dt lthy (((s2, s3), syn), constrs) = |
111 ["constructor declaration"] |
123 ["constructor declaration"] |
112 @ ["type arguments: "] @ s2 |
124 @ ["type arguments: "] @ s2 |
113 @ ["datatype name: ", Binding.name_of s3] |
125 @ ["datatype name: ", Binding.name_of s3] |
114 @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)] |
126 @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)] |
115 @ ["constructors: "] @ (map print_constr constrs) |
127 @ ["constructors: "] @ (map (print_constr lthy) constrs) |
116 |> separate "\n" |
128 |> separate "\n" |
117 |> implode |
129 |> implode |
118 *} |
130 *} |
119 |
131 |
120 ML {* |
132 ML {* |
121 fun fv_dt (((s2, s3), syn), constrs) = |
133 fun fv_dt lthy (((s2, s3), syn), constrs) = |
122 map (fv_constr ("fv_" ^ Binding.name_of s3)) constrs |
134 map (fv_constr lthy ("fv_" ^ Binding.name_of s3)) constrs |
123 |> separate "\n" |
135 |> separate "\n" |
124 |> implode |
136 |> implode |
125 *} |
137 *} |
126 |
138 |
127 ML {* fun single_fun_eq (at, s) = |
139 ML {* fun single_fun_eq lthy (at, s) = |
128 ["function equations: ", s] |
140 ["function equations: ", (Syntax.string_of_term lthy s)] |
129 |> separate "\n" |
141 |> separate "\n" |
130 |> implode |
142 |> implode |
131 *} |
143 *} |
132 |
144 |
133 ML {* fun single_fun_fix (b, _, _) = |
145 ML {* fun single_fun_fix (b, _, _) = |
174 *} |
186 *} |
175 |
187 |
176 ML {* |
188 ML {* |
177 fun fn_defn [] [] lthy = lthy |
189 fun fn_defn [] [] lthy = lthy |
178 | fn_defn funs feqs lthy = |
190 | fn_defn funs feqs lthy = |
179 Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
191 Function_Fun.add_fun Function_Common.default_config funs feqs false lthy |
180 *} |
192 *} |
181 |
|
182 |
193 |
183 ML {* |
194 ML {* |
184 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
195 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
185 dt_defn (map transp_dt dts) thy |
196 let |
186 |> Theory_Target.init NONE |
197 val thy' = dt_defn (map transp_dt dts) thy |
187 |> fn_defn funs feqs |
198 val lthy = Theory_Target.init NONE thy' |
|
199 fun parse_fun (b, NONE, m) = (b, NONE, m) |
|
200 | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m); |
|
201 val funs = map parse_fun funs |
|
202 fun parse_feq (b, t) = (b, Syntax.read_prop lthy t); |
|
203 val feqs = map parse_feq feqs |
|
204 fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy ty); |
|
205 fun parse_constr (((constr_name, ty_args), bind), mx) = |
|
206 (((constr_name, map parse_anno_ty ty_args), bind), mx); |
|
207 fun parse_dt (((ty_args, ty_name), mx), constrs) = |
|
208 (((ty_args, ty_name), mx), map parse_constr constrs); |
|
209 val dts = map parse_dt dts |
|
210 in |
|
211 fn_defn funs feqs lthy |
188 |> print_dts (dts, (funs, feqs)) |
212 |> print_dts (dts, (funs, feqs)) |
189 |> Local_Theory.exit_global |
213 |> Local_Theory.exit_global |
|
214 end |
190 *} |
215 *} |
191 |
216 |
192 (* Command Keyword *) |
217 (* Command Keyword *) |
193 ML {* |
218 ML {* |
194 let |
219 let |