117 val is_stypeT = fn (Type (_, [])) => true | _ => false; |
117 val is_stypeT = fn (Type (_, [])) => true | _ => false; |
118 val is_compT = fn (Type (_, _ :: _)) => true | _ => false; |
118 val is_compT = fn (Type (_, _ :: _)) => true | _ => false; |
119 val is_freeT = fn (TFree _) => true | _ => false; |
119 val is_freeT = fn (TFree _) => true | _ => false; |
120 val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false; |
120 val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false; |
121 val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false; |
121 val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false; |
|
122 |
|
123 fun mk_identity T = Abs (Name.uu, T, Bound 0); |
122 val is_identity = fn (Abs (_, _, Bound 0)) => true | _ => false; |
124 val is_identity = fn (Abs (_, _, Bound 0)) => true | _ => false; |
123 |
125 |
124 fun instantiate t Ts = Term.subst_TVars |
126 fun instantiate t Ts = Term.subst_TVars |
125 ((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts) t; |
127 ((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts) t; |
126 |
128 |
663 fun gen_coercion ctxt err tye TU = |
665 fun gen_coercion ctxt err tye TU = |
664 let |
666 let |
665 fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of |
667 fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of |
666 (T1 as (Type (a, [])), T2 as (Type (b, []))) => |
668 (T1 as (Type (a, [])), T2 as (Type (b, []))) => |
667 if a = b |
669 if a = b |
668 then Abs (Name.uu, Type (a, []), Bound 0) |
670 then mk_identity T1 |
669 else |
671 else |
670 (case Symreltab.lookup (coes_of ctxt) (a, b) of |
672 (case Symreltab.lookup (coes_of ctxt) (a, b) of |
671 NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^ |
673 NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^ |
672 " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2)) |
674 " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2)) |
673 | SOME (co, _) => co) |
675 | SOME (co, _) => co) |
690 Abs (Name.uu, T1, Library.foldr (op $) |
692 Abs (Name.uu, T1, Library.foldr (op $) |
691 (filter (not o is_identity) [co_after, co', co_before], Bound 0)) |
693 (filter (not o is_identity) [co_after, co', co_before], Bound 0)) |
692 end) |
694 end) |
693 else |
695 else |
694 let |
696 let |
695 fun sub_co (COVARIANT, TU) = SOME (gen TU) |
697 fun sub_co (COVARIANT, TU) = (SOME (gen TU), NONE) |
696 | sub_co (CONTRAVARIANT, TU) = SOME (gen (swap TU)) |
698 | sub_co (CONTRAVARIANT, TU) = (SOME (gen (swap TU)), NONE) |
697 | sub_co (INVARIANT_TO _, _) = NONE; |
699 | sub_co (INVARIANT, (T, _)) = (NONE, SOME T) |
|
700 | sub_co (INVARIANT_TO T, _) = (NONE, NONE); |
698 fun ts_of [] = [] |
701 fun ts_of [] = [] |
699 | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); |
702 | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); |
700 in |
703 in |
701 (case Symtab.lookup (tmaps_of ctxt) a of |
704 (case Symtab.lookup (tmaps_of ctxt) a of |
702 NONE => |
705 NONE => |
703 if Type.could_unify (T1, T2) |
706 if Type.could_unify (T1, T2) |
704 then Abs (Name.uu, T1, Bound 0) |
707 then mk_identity T1 |
705 else raise COERCION_GEN_ERROR |
708 else raise COERCION_GEN_ERROR |
706 (err ++> "No map function for " ^ quote a ^ " known") |
709 (err ++> "No map function for " ^ quote a ^ " known") |
707 | SOME tmap => |
710 | SOME (tmap, variances) => |
708 let |
711 let |
709 val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us)); |
712 val (used_coes, invarTs) = |
|
713 map_split sub_co (variances ~~ (Ts ~~ Us)) |
|
714 |>> map_filter I |
|
715 ||> map_filter I; |
|
716 val Tinsts = ts_of (map fastype_of used_coes) @ invarTs; |
710 in |
717 in |
711 if null (filter (not o is_identity) used_coes) |
718 if null (filter (not o is_identity) used_coes) |
712 then Abs (Name.uu, Type (a, Ts), Bound 0) |
719 then mk_identity (Type (a, Ts)) |
713 else Term.list_comb |
720 else Term.list_comb (instantiate tmap Tinsts, used_coes) |
714 (instantiate (fst tmap) (ts_of (map fastype_of used_coes)), used_coes) |
|
715 end) |
721 end) |
716 end |
722 end |
717 | (T, U) => |
723 | (T, U) => |
718 if Type.could_unify (T, U) |
724 if Type.could_unify (T, U) |
719 then Abs (Name.uu, T, Bound 0) |
725 then mk_identity T |
720 else raise COERCION_GEN_ERROR (err ++> "Cannot generate coercion from " ^ |
726 else raise COERCION_GEN_ERROR (err ++> "Cannot generate coercion from " ^ |
721 quote (Syntax.string_of_typ ctxt T) ^ " to " ^ |
727 quote (Syntax.string_of_typ ctxt T) ^ " to " ^ |
722 quote (Syntax.string_of_typ ctxt U))); |
728 quote (Syntax.string_of_typ ctxt U))); |
723 in |
729 in |
724 gen TU |
730 gen TU |
873 |
879 |
874 val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) |
880 val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t)) |
875 handle List.Empty => error ("Not a proper map function:" ^ err_str t); |
881 handle List.Empty => error ("Not a proper map function:" ^ err_str t); |
876 |
882 |
877 fun gen_arg_var ([], []) = [] |
883 fun gen_arg_var ([], []) = [] |
878 | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) = |
884 | gen_arg_var (Ts, (U, U') :: Us) = |
879 if U = U' then |
885 if U = U' then |
880 if is_stypeT U then INVARIANT_TO U :: gen_arg_var ((T, T') :: Ts, Us) |
886 if null (Term.add_tvarsT U []) then INVARIANT_TO U :: gen_arg_var (Ts, Us) |
881 else error ("Invariant xi and yi should be base types:" ^ err_str t) |
887 else if Term.is_TVar U then INVARIANT :: gen_arg_var (Ts, Us) |
882 else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) |
888 else error ("Invariant xi and yi should be variables or variable-free:" ^ err_str t) |
883 else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) |
889 else |
884 else error ("Functions do not apply to arguments correctly:" ^ err_str t) |
890 (case Ts of |
885 | gen_arg_var (_, Ts) = |
891 [] => error ("Different numbers of functions and variant arguments\n" ^ err_str t) |
886 if forall (op = andf is_stypeT o fst) Ts |
892 | (T, T') :: Ts => |
887 then map (INVARIANT_TO o fst) Ts |
893 if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) |
888 else error ("Different numbers of functions and variant arguments\n" ^ err_str t); |
894 else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) |
|
895 else error ("Functions do not apply to arguments correctly:" ^ err_str t)); |
889 |
896 |
890 (*retry flag needed to adjust the type lists, when given a map over type constructor fun*) |
897 (*retry flag needed to adjust the type lists, when given a map over type constructor fun*) |
891 fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry = |
898 fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry = |
892 if C1 = C2 andalso not (null fis) andalso forall is_funtype fis |
899 if C1 = C2 andalso not (null fis) andalso forall is_funtype fis |
893 then ((map dest_funT fis, Ts ~~ Us), C1) |
900 then ((map dest_funT fis, Ts ~~ Us), C1) |
913 end; |
920 end; |
914 val path = hd (Graph.irreducible_paths G (a, b)); |
921 val path = hd (Graph.irreducible_paths G (a, b)); |
915 val path' = fst (split_last path) ~~ tl path; |
922 val path' = fst (split_last path) ~~ tl path; |
916 val coercions = map (fst o the o Symreltab.lookup tab) path'; |
923 val coercions = map (fst o the o Symreltab.lookup tab) path'; |
917 val trans_co = singleton (Variable.polymorphic ctxt) |
924 val trans_co = singleton (Variable.polymorphic ctxt) |
918 (fold safe_app coercions (Abs (Name.uu, dummyT, Bound 0))); |
925 (fold safe_app coercions (mk_identity dummyT)); |
919 val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co)) |
926 val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co)) |
920 in |
927 in |
921 (trans_co, ((Ts, Us), coercions)) |
928 (trans_co, ((Ts, Us), coercions)) |
922 end; |
929 end; |
923 |
930 |