276 in |
276 in |
277 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
277 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
278 end |
278 end |
279 *} |
279 *} |
280 |
280 |
|
281 ML AList.lookup |
|
282 |
281 (* We assume no bindings in the type on which bn is defined *) |
283 (* We assume no bindings in the type on which bn is defined *) |
282 (* TODO: currently works only with current fv_bn function *) |
284 (* TODO: currently works only with current fv_bn function *) |
283 ML {* |
285 ML {* |
284 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) = |
286 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) = |
285 let |
287 let |
286 val {descr, sorts, ...} = dt_info; |
288 val {descr, sorts, ...} = dt_info; |
287 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
289 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
288 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
289 val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp)); |
|
290 fun fv_bn_constr (cname, dts) args_in_bn = |
290 fun fv_bn_constr (cname, dts) args_in_bn = |
291 let |
291 let |
292 val Ts = map (typ_of_dtyp descr sorts) dts; |
292 val Ts = map (typ_of_dtyp descr sorts) dts; |
293 val names = Datatype_Prop.make_tnames Ts; |
293 val names = Datatype_Prop.make_tnames Ts; |
294 val args = map Free (names ~~ Ts); |
294 val args = map Free (names ~~ Ts); |
295 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
295 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
296 fun fv_arg ((dt, x), arg_no) = |
296 fun fv_arg ((dt, x), arg_no) = |
297 let |
297 let |
298 val ty = fastype_of x |
298 val ty = fastype_of x |
|
299 val _ = tracing (PolyML.makestring args_in_bn); |
|
300 val _ = tracing (PolyML.makestring bn_fvbn); |
299 in |
301 in |
300 if arg_no mem args_in_bn then |
302 case AList.lookup (op=) args_in_bn arg_no of |
301 (if is_rec_type dt then |
303 SOME NONE => @{term "{} :: atom set"} |
302 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.") |
304 | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x |
303 else @{term "{} :: atom set"}) else |
305 | NONE => |
304 if is_atom thy ty then mk_single_atom x else |
306 if is_atom thy ty then mk_single_atom x else |
305 if is_atom_set thy ty then mk_atom_set x else |
307 if is_atom_set thy ty then mk_atom_set x else |
306 if is_atom_fset thy ty then mk_atom_fset x else |
308 if is_atom_fset thy ty then mk_atom_fset x else |
307 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
309 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
308 @{term "{} :: atom set"} |
310 @{term "{} :: atom set"} |
309 end; |
311 end; |
310 val arg_nos = 0 upto (length dts - 1) |
312 val arg_nos = 0 upto (length dts - 1) |
311 in |
313 in |
312 HOLogic.mk_Trueprop (HOLogic.mk_eq |
314 HOLogic.mk_Trueprop (HOLogic.mk_eq |
313 (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
315 (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
314 end; |
316 end; |
315 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
317 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
316 val eqs = map2i fv_bn_constr constrs args_in_bns |
318 val eqs = map2i fv_bn_constr constrs args_in_bns |
317 in |
319 in |
318 ((bn, fvbn), (fvbn_name, eqs)) |
320 ((bn, fvbn), eqs) |
319 end |
321 end |
320 *} |
322 *} |
321 |
323 |
322 ML {* |
324 ML {* |
323 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = |
325 fun fv_bns thy dt_info fv_frees rel_bns = |
|
326 let |
|
327 fun mk_fvbn_free (bn, ith, _) = |
|
328 let |
|
329 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
330 in |
|
331 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
|
332 end; |
|
333 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free rel_bns); |
|
334 val bn_fvbn = (map (fn (bn, _, _) => bn) rel_bns) ~~ fvbn_frees |
|
335 val (l1, l2) = split_list (map (fv_bn thy dt_info fv_frees bn_fvbn) (fvbn_frees ~~ rel_bns)); |
|
336 in |
|
337 (l1, (fvbn_names ~~ l2)) |
|
338 end |
|
339 *} |
|
340 |
|
341 |
|
342 ML {* |
|
343 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, is_rec)) = |
324 let |
344 let |
325 val {descr, sorts, ...} = dt_info; |
345 val {descr, sorts, ...} = dt_info; |
326 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
346 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
327 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
328 val alpha_bn_type = |
|
329 (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*) |
|
330 nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}; |
|
331 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
|
332 val pi = Free("pi", @{typ perm}) |
347 val pi = Free("pi", @{typ perm}) |
333 fun alpha_bn_constr (cname, dts) args_in_bn = |
348 fun alpha_bn_constr (cname, dts) args_in_bn = |
334 let |
349 let |
335 val Ts = map (typ_of_dtyp descr sorts) dts; |
350 val Ts = map (typ_of_dtyp descr sorts) dts; |
336 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
351 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
343 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
358 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
344 let |
359 let |
345 val argty = fastype_of arg; |
360 val argty = fastype_of arg; |
346 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
361 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
347 in |
362 in |
348 if is_rec_type dt then |
363 case AList.lookup (op=) args_in_bn arg_no of |
349 if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2 |
364 SOME NONE => @{term True} |
350 else (nth alpha_frees (body_index dt)) $ arg $ arg2 |
365 | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2 |
351 else |
366 | NONE => |
352 if arg_no mem args_in_bn then @{term True} |
367 if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2 |
353 else HOLogic.mk_eq (arg, arg2) |
368 else HOLogic.mk_eq (arg, arg2) |
354 end |
369 end |
355 val arg_nos = 0 upto (length dts - 1) |
370 val arg_nos = 0 upto (length dts - 1) |
356 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
371 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
357 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
372 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
358 in |
373 in |
359 eq |
374 eq |
360 end |
375 end |
361 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
376 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
362 val eqs = map2i alpha_bn_constr constrs args_in_bns |
377 val eqs = map2i alpha_bn_constr constrs args_in_bns |
363 in |
378 in |
364 ((bn, alpha_bn_free), (alpha_bn_name, eqs)) |
379 ((bn, alpha_bn_free), eqs) |
365 end |
380 end |
366 *} |
381 *} |
|
382 |
|
383 ML {* |
|
384 fun alpha_bns thy dt_info alpha_frees rel_bns bns_rec = |
|
385 let |
|
386 val {descr, sorts, ...} = dt_info; |
|
387 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
388 fun mk_alphabn_free (bn, ith, _) = |
|
389 let |
|
390 val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
391 val alphabn_type = nth_dtyp ith --> nth_dtyp ith --> @{typ bool}; |
|
392 val alphabn_free = Free(alphabn_name, alphabn_type); |
|
393 in |
|
394 (alphabn_name, alphabn_free) |
|
395 end; |
|
396 val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free rel_bns); |
|
397 val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees; |
|
398 val pair = split_list (map (alpha_bn thy dt_info alpha_frees bn_alphabn) |
|
399 (rel_bns ~~ (alphabn_frees ~~ bns_rec))) |
|
400 in |
|
401 (alphabn_names, pair) |
|
402 end |
|
403 *} |
|
404 |
367 |
405 |
368 (* Checks that a list of bindings contains only compatible ones *) |
406 (* Checks that a list of bindings contains only compatible ones *) |
369 ML {* |
407 ML {* |
370 fun bns_same l = |
408 fun bns_same l = |
371 length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1 |
409 length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1 |
382 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
420 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
383 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
421 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
384 val fv_frees = map Free (fv_names ~~ fv_types); |
422 val fv_frees = map Free (fv_names ~~ fv_types); |
385 val nr_bns = non_rec_binds bindsall; |
423 val nr_bns = non_rec_binds bindsall; |
386 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
424 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
387 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
425 val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns; |
388 val fvbns = map snd bn_fv_bns; |
426 val fvbns = map snd bn_fv_bns; |
389 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
427 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
390 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
428 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
391 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
429 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
392 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
430 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
393 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
431 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
394 (* We assume that a bn is either recursive or not *) |
432 (* We assume that a bn is either recursive or not *) |
395 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
433 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
396 val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec)) |
434 val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) = |
397 val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs; |
435 alpha_bns thy dt_info alpha_frees bns bns_rec |
398 val alpha_bn_frees = map snd bn_alpha_bns; |
436 val alpha_bn_frees = map snd bn_alpha_bns; |
399 val alpha_bn_types = map fastype_of alpha_bn_frees; |
437 val alpha_bn_types = map fastype_of alpha_bn_frees; |
400 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
438 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
401 let |
439 let |
402 val Ts = map (typ_of_dtyp descr sorts) dts; |
440 val Ts = map (typ_of_dtyp descr sorts) dts; |