235 *} |
235 *} |
236 |
236 |
237 ML {* |
237 ML {* |
238 fun forth (_, _, _, x) = x |
238 fun forth (_, _, _, x) = x |
239 |
239 |
240 fun find_all eq [] _ = [] |
240 fun find_all eq xs k' = |
241 | find_all eq ((key, value)::xs) key' = |
241 maps (fn (k, v) => if eq (k, k') then [v] else []) xs |
242 let |
242 *} |
243 val values = find_all eq xs key' |
243 |
244 in if eq (key', key) then value :: values else values end; |
244 ML {* |
245 |
|
246 fun mk_env xs = |
245 fun mk_env xs = |
247 let |
246 let |
248 fun mapp (_: int) [] = [] |
247 fun mapp (_: int) [] = [] |
249 | mapp i ((a, _) :: xs) = |
248 | mapp i (a :: xs) = |
250 case a of |
249 case a of |
251 NONE => mapp (i + 1) xs |
250 NONE => mapp (i + 1) xs |
252 | SOME x => (x, i) :: mapp (i + 1) xs |
251 | SOME x => (x, i) :: mapp (i + 1) xs |
253 in mapp 0 xs end |
252 in mapp 0 xs end |
254 |
253 *} |
|
254 |
|
255 ML {* |
255 fun env_lookup xs x = |
256 fun env_lookup xs x = |
256 case AList.lookup (op =) xs x of |
257 case AList.lookup (op =) xs x of |
257 SOME x => x |
258 SOME x => x |
258 | NONE => error ("cannot find " ^ x ^ " in the binding specification.") |
259 | NONE => error ("cannot find " ^ x ^ " in the binding specification.") |
259 *} |
260 *} |
260 |
261 |
261 ML {* |
262 ML {* |
262 fun prepare_binds dt_strs lthy = |
263 fun prepare_binds dt_strs lthy = |
263 let |
264 let |
264 fun prep_bn env str = |
265 fun extract_cnstrs dt_strs = |
265 (case Syntax.read_term lthy str of |
266 map ((map (fn (_, antys, _, bns) => (antys, bns))) o forth) dt_strs |
266 Free (x, _) => (env_lookup env x, NONE) |
267 |
267 | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T))) |
268 fun prep_bn env bn_str = |
268 | x => error (str ^ " not allowed as binding specification.")) |
269 case (Syntax.read_term lthy bn_str) of |
|
270 Free (x, _) => (env_lookup env x, NONE) |
|
271 | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T))) |
|
272 | _ => error (bn_str ^ " not allowed as binding specification."); |
269 |
273 |
270 fun prep_typ env (opt_name, _) = |
274 fun prep_typ env (opt_name, _) = |
271 (case opt_name of |
275 case opt_name of |
272 NONE => [] |
276 NONE => [] |
273 | SOME x => find_all (op=) env x) |
277 | SOME x => find_all (op=) env x; |
274 |
278 |
275 fun prep_binds (_, anno_tys, _, bind_strs) = |
279 fun prep_binds (anno_tys, bind_strs) = |
276 let |
280 let |
277 val env = mk_env anno_tys |
281 val env = mk_env (map fst anno_tys) |
278 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
282 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
279 in |
283 in |
280 map (prep_typ binds) anno_tys |
284 map (prep_typ binds) anno_tys |
281 end |
285 end |
282 in |
286 in |
283 map ((map prep_binds) o forth) dt_strs |
287 map (map prep_binds) (extract_cnstrs dt_strs) |
284 end |
288 end |
285 *} |
289 *} |
286 |
290 |
287 ML {* |
291 ML {* |
288 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
292 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
289 let |
293 let |
290 val t = start_timing () |
|
291 |
|
292 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) |
294 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) |
293 |
295 |
294 val ((dts, (bn_fun, bn_eq)), binds) = |
296 val ((dts, (bn_fun, bn_eq)), binds) = |
295 lthy |
297 lthy |
296 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
298 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
297 |> prepare_dts dt_strs |
299 |> prepare_dts dt_strs |
298 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
300 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
299 ||> prepare_binds dt_strs |
301 ||> prepare_binds dt_strs |
300 |
302 |
301 val _ = tracing (PolyML.makestring binds) |
303 val _ = tracing (PolyML.makestring binds) |
302 val _ = tracing (#message (end_timing t)) |
|
303 in |
304 in |
304 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
305 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
305 end |
306 end |
306 *} |
307 *} |
307 |
308 |