106 trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) |
105 trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) |
107 *} |
106 *} |
108 |
107 |
109 ML {* |
108 ML {* |
110 fun get_cnstrs dts = |
109 fun get_cnstrs dts = |
111 flat (map (fn (_, _, _, constrs) => constrs) dts) |
110 map (fn (_, _, _, constrs) => constrs) dts |
112 |
111 |
113 fun get_typed_cnstrs dts = |
112 fun get_typed_cnstrs dts = |
114 flat (map (fn (_, bn, _, constrs) => |
113 flat (map (fn (_, bn, _, constrs) => |
115 (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) |
114 (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) |
116 |
115 |
117 fun get_cnstr_strs dts = |
116 fun get_cnstr_strs dts = |
118 map (fn (bn, _, _) => Binding.name_of bn) (get_cnstrs dts) |
117 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) |
119 |
118 |
120 fun get_bn_fun_strs bn_funs = |
119 fun get_bn_fun_strs bn_funs = |
121 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
120 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
122 *} |
121 *} |
123 |
122 |
244 |> pair (bn_funs', bn_eqs) |
243 |> pair (bn_funs', bn_eqs) |
245 end |
244 end |
246 *} |
245 *} |
247 |
246 |
248 ML {* |
247 ML {* |
249 fun forth (_, _, _, x) = x |
248 fun find_all eq xs (k',i) = |
250 |
249 maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs |
251 fun find_all eq xs k' = |
250 *} |
252 maps (fn (k, v) => if eq (k, k') then [v] else []) xs |
251 |
253 *} |
252 ML {* |
254 |
253 (* associates every SOME with the index in the list; drops NONEs *) |
255 ML {* |
|
256 (* associates every SOME with the index in the list *) |
|
257 fun mk_env xs = |
254 fun mk_env xs = |
258 let |
255 let |
259 fun mapp (_: int) [] = [] |
256 fun mapp (_: int) [] = [] |
260 | mapp i (a :: xs) = |
257 | mapp i (a :: xs) = |
261 case a of |
258 case a of |
269 case AList.lookup (op =) xs x of |
266 case AList.lookup (op =) xs x of |
270 SOME x => x |
267 SOME x => x |
271 | NONE => error ("cannot find " ^ x ^ " in the binding specification."); |
268 | NONE => error ("cannot find " ^ x ^ " in the binding specification."); |
272 *} |
269 *} |
273 |
270 |
274 |
|
275 |
|
276 ML {* |
271 ML {* |
277 fun prepare_binds dt_strs lthy = |
272 fun prepare_binds dt_strs lthy = |
278 let |
273 let |
279 fun extract_annos_binds dt_strs = |
274 fun extract_annos_binds dt_strs = |
280 map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs |
275 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
281 |
276 |
282 fun prep_bn env bn_str = |
277 fun prep_bn env bn_str = |
283 case (Syntax.read_term lthy bn_str) of |
278 case (Syntax.read_term lthy bn_str) of |
284 Free (x, _) => (env_lookup env x, NONE) |
279 Free (x, _) => (NONE, env_lookup env x) |
285 | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T))) |
280 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x) |
286 | _ => error (bn_str ^ " not allowed as binding specification."); |
281 | _ => error (bn_str ^ " not allowed as binding specification."); |
287 |
282 |
288 fun prep_typ env opt_name = |
283 fun prep_typ env (i, opt_name) = |
289 case opt_name of |
284 case opt_name of |
290 NONE => [] |
285 NONE => [] |
291 | SOME x => find_all (op=) env x; |
286 | SOME x => find_all (op=) env (x,i); |
292 |
287 |
293 (* annos - list of annotation for each type (either NONE or SOME fo a type *) |
288 (* annos - list of annotation for each type (either NONE or SOME fo a type *) |
294 |
289 |
295 fun prep_binds (annos, bind_strs) = |
290 fun prep_binds (annos, bind_strs) = |
296 let |
291 let |
297 val env = mk_env annos (* for ever label the index *) |
292 val env = mk_env annos (* for every label the index *) |
298 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
293 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
299 in |
294 in |
300 map (prep_typ binds) annos |
295 map_index (prep_typ binds) annos |
301 end |
296 end |
302 |
297 |
303 in |
298 in |
304 map (map prep_binds) (extract_annos_binds dt_strs) |
299 map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)) |
305 end |
300 end |
306 *} |
301 *} |
307 |
302 |
308 ML {* |
303 ML {* |
309 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
304 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
315 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
310 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
316 |> prepare_dts dt_strs |
311 |> prepare_dts dt_strs |
317 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
312 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
318 ||> prepare_binds dt_strs |
313 ||> prepare_binds dt_strs |
319 |
314 |
320 (*val _ = tracing (PolyML.makestring binds)*) |
315 val _ = tracing (PolyML.makestring binds) |
321 in |
316 in |
322 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
317 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
323 end |
318 end |
324 *} |
319 *} |
325 |
320 |