493 | Type ("fun" , [ty1, ty2]) => |
493 | Type ("fun" , [ty1, ty2]) => |
494 get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] |
494 get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] |
495 | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys) |
495 | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys) |
496 | _ => raise ERROR ("no type variables")) |
496 | _ => raise ERROR ("no type variables")) |
497 end |
497 end |
498 *} |
498 fun get_fun_noex flag (rty, qty) lthy ty = |
499 |
499 fst (get_fun_noexchange flag (rty, qty) lthy ty) |
500 ML {* |
|
501 fun old_get_fun flag rty qty lthy ty = |
|
502 get_fun_noexchange flag (rty, qty) lthy ty |
|
503 *} |
500 *} |
504 |
501 |
505 ML {* |
502 ML {* |
506 fun find_matching_types rty ty = |
503 fun find_matching_types rty ty = |
507 let val (s, tys) = dest_Type ty in |
504 if Type.raw_instance (Logic.varifyT ty, rty) |
508 if Type.raw_instance (Logic.varifyT ty, rty) |
505 then [ty] |
509 then [ty] |
506 else |
510 else flat (map (find_matching_types rty) tys) |
507 let val (s, tys) = dest_Type ty in |
511 end |
508 flat (map (find_matching_types rty) tys) |
512 *} |
509 end |
513 |
510 handle _ => [] |
514 ML {* |
511 *} |
515 fun get_fun_new flag rty qty lthy ty = |
512 |
|
513 ML {* |
|
514 fun get_fun_new flag (rty, qty) lthy ty = |
516 let |
515 let |
517 val tys = find_matching_types rty ty; |
516 val tys = find_matching_types rty ty; |
518 val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; |
517 val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; |
519 val xchg_ty = exchange_ty lthy rty qty ty |
518 val xchg_ty = exchange_ty lthy rty qty ty |
520 in |
519 in |
532 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} |
531 ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *} |
533 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} |
532 ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *} |
534 ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *} |
533 ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *} |
535 |
534 |
536 ML {* |
535 ML {* |
537 fst (get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt)) |
536 get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt) |
538 *} |
537 *} |
539 ML {* |
538 ML {* |
540 fst (get_fun_new absF al aq @{context} (fastype_of ttt)) |
539 get_fun_new absF al aq @{context} (fastype_of ttt) |
541 *} |
540 *} |
542 ML {* |
541 ML {* |
543 fun mk_abs tm = |
542 fun mk_abs tm = |
544 let |
543 let |
545 val ty = fastype_of tm |
544 val ty = fastype_of tm |
546 in fst (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end |
545 in (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end |
547 fun mk_repabs tm = |
546 fun mk_repabs tm = |
548 let |
547 let |
549 val ty = fastype_of tm |
548 val ty = fastype_of tm |
550 in fst (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end |
549 in (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end |
551 *} |
550 *} |
552 ML {* |
551 ML {* |
553 cterm_of @{theory} (mk_repabs ttt) |
552 cterm_of @{theory} (mk_repabs ttt) |
554 *} |
553 *} |
555 *) |
554 *) |
600 val qty = Logic.varifyT qty; |
599 val qty = Logic.varifyT qty; |
601 |
600 |
602 fun mk_abs tm = |
601 fun mk_abs tm = |
603 let |
602 let |
604 val ty = fastype_of tm |
603 val ty = fastype_of tm |
605 in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end |
604 in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end |
606 fun mk_repabs tm = |
605 fun mk_repabs tm = |
607 let |
606 let |
608 val ty = fastype_of tm |
607 val ty = fastype_of tm |
609 in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ (mk_abs tm) end |
608 in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end |
610 |
609 |
611 fun is_constructor (Const (x, _)) = member (op =) constructors x |
610 fun is_constructor (Const (x, _)) = member (op =) constructors x |
612 | is_constructor _ = false; |
611 | is_constructor _ = false; |
613 |
612 |
614 fun build_aux lthy tm = |
613 fun build_aux lthy tm = |
935 fun absty ty = |
934 fun absty ty = |
936 exchange_ty lthy rty qty ty |
935 exchange_ty lthy rty qty ty |
937 fun mk_rep tm = |
936 fun mk_rep tm = |
938 let |
937 let |
939 val ty = exchange_ty lthy qty rty (fastype_of tm) |
938 val ty = exchange_ty lthy qty rty (fastype_of tm) |
940 in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end; |
939 in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end; |
941 fun mk_abs tm = |
940 fun mk_abs tm = |
942 let |
941 let |
943 val ty = fastype_of tm |
942 val ty = fastype_of tm |
944 in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end |
943 in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end |
945 val (l, ltl) = Term.strip_type ty; |
944 val (l, ltl) = Term.strip_type ty; |
946 val nl = map absty l; |
945 val nl = map absty l; |
947 val vs = map (fn _ => "x") l; |
946 val vs = map (fn _ => "x") l; |
948 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
947 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
949 val args = map Free (vfs ~~ nl); |
948 val args = map Free (vfs ~~ nl); |