165 fun print_dts (dts, (funs, feqs)) lthy = |
165 fun print_dts (dts, (funs, feqs)) lthy = |
166 let |
166 let |
167 val _ = warning (implode (separate "\n" (map (single_dt lthy) dts))); |
167 val _ = warning (implode (separate "\n" (map (single_dt lthy) dts))); |
168 val _ = warning (implode (separate "\n" (map single_fun_fix funs))); |
168 val _ = warning (implode (separate "\n" (map single_fun_fix funs))); |
169 val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs))); |
169 val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs))); |
|
170 in |
|
171 () |
|
172 end |
|
173 *} |
|
174 |
|
175 ML {* |
|
176 fun fv_dts (dts, (funs, feqs)) lthy = |
|
177 let |
170 val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts))); |
178 val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts))); |
171 in |
179 in |
172 lthy |
180 lthy |
173 end |
181 end |
174 *} |
182 *} |
175 |
183 |
176 ML {* |
184 ML {* |
177 parser; |
185 parser; |
178 Datatype.datatype_cmd; |
186 Datatype.datatype_cmd; |
199 *} |
207 *} |
200 |
208 |
201 ML {* |
209 ML {* |
202 fun fn_defn [] [] lthy = lthy |
210 fun fn_defn [] [] lthy = lthy |
203 | fn_defn funs feqs lthy = |
211 | fn_defn funs feqs lthy = |
204 Function_Fun.add_fun Function_Common.default_config funs feqs false lthy |
212 Function_Fun.add_fun Function_Common.default_config funs feqs false lthy |
|
213 *} |
|
214 |
|
215 ML {* |
|
216 fun fn_defn_cmd [] [] lthy = lthy |
|
217 | fn_defn_cmd funs feqs lthy = |
|
218 Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
205 *} |
219 *} |
206 |
220 |
207 ML {* |
221 ML {* |
208 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
222 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
209 let |
223 let |
210 val thy' = dt_defn (map transp_dt dts) thy |
224 val thy' = dt_defn (map transp_dt dts) thy |
211 val lthy = Theory_Target.init NONE thy' |
225 val lthy = Theory_Target.init NONE thy' |
|
226 val lthy' = fn_defn_cmd funs feqs lthy |
212 fun parse_fun (b, NONE, m) = (b, NONE, m) |
227 fun parse_fun (b, NONE, m) = (b, NONE, m) |
213 | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m); |
228 | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy' ty), m); |
214 val funs = map parse_fun funs |
229 val funs = map parse_fun funs |
215 fun parse_feq (b, t) = (b, Syntax.read_prop lthy t); |
230 fun parse_feq (b, t) = (b, Syntax.read_prop lthy' t); |
216 val feqs = map parse_feq feqs |
231 val feqs = map parse_feq feqs |
217 fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy ty); |
232 fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy' ty); |
218 fun parse_constr (((constr_name, ty_args), bind), mx) = |
233 fun parse_constr (((constr_name, ty_args), bind), mx) = |
219 (((constr_name, map parse_anno_ty ty_args), bind), mx); |
234 (((constr_name, map parse_anno_ty ty_args), bind), mx); |
220 fun parse_dt (((ty_args, ty_name), mx), constrs) = |
235 fun parse_dt (((ty_args, ty_name), mx), constrs) = |
221 (((ty_args, ty_name), mx), map parse_constr constrs); |
236 (((ty_args, ty_name), mx), map parse_constr constrs); |
222 val dts = map parse_dt dts |
237 val dts = map parse_dt dts |
223 in |
238 val _ = print_dts (dts, (funs, feqs)) lthy |
224 fn_defn funs feqs lthy |
239 in |
225 |> print_dts (dts, (funs, feqs)) |
240 fv_dts (dts, (funs, feqs)) lthy |
226 |> Local_Theory.exit_global |
241 |> Local_Theory.exit_global |
227 end |
242 end |
228 *} |
243 *} |
229 |
244 |
230 (* Command Keyword *) |
245 (* Command Keyword *) |