allow more general coercion maps; tuned;
authortraytel
Tue Mar 05 09:47:15 2013 +0100 (2013-03-05)
changeset 513356bac04a6a197
parent 51334 fd531bd984d8
child 51336 6c06b8de72f9
child 51354 45579fbe5a24
allow more general coercion maps; tuned;
src/HOL/ex/Coercion_Examples.thy
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/ex/Coercion_Examples.thy	Tue Mar 05 10:16:15 2013 +0100
     1.2 +++ b/src/HOL/ex/Coercion_Examples.thy	Tue Mar 05 09:47:15 2013 +0100
     1.3 @@ -178,6 +178,12 @@
     1.4  
     1.5  term "ys=[[[[[1::nat]]]]]"
     1.6  
     1.7 +typedecl ('a, 'b, 'c) F
     1.8 +consts Fmap :: "('a \<Rightarrow> 'd) \<Rightarrow> ('a, 'b, 'c) F \<Rightarrow> ('d, 'b, 'c) F"
     1.9 +consts z :: "(bool, nat, bool) F"
    1.10 +declare [[coercion_map "Fmap :: ('a \<Rightarrow> 'd) \<Rightarrow> ('a, 'b, 'c) F \<Rightarrow> ('d, 'b, 'c) F"]]
    1.11 +term "z :: (nat, nat, bool) F"
    1.12 +
    1.13  consts
    1.14    case_nil :: "'a \<Rightarrow> 'b"
    1.15    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     2.1 --- a/src/Tools/subtyping.ML	Tue Mar 05 10:16:15 2013 +0100
     2.2 +++ b/src/Tools/subtyping.ML	Tue Mar 05 09:47:15 2013 +0100
     2.3 @@ -119,6 +119,8 @@
     2.4  val is_freeT = fn (TFree _) => true | _ => false;
     2.5  val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
     2.6  val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false;
     2.7 +
     2.8 +fun mk_identity T = Abs (Name.uu, T, Bound 0);
     2.9  val is_identity = fn (Abs (_, _, Bound 0)) => true | _ => false;
    2.10  
    2.11  fun instantiate t Ts = Term.subst_TVars
    2.12 @@ -665,7 +667,7 @@
    2.13      fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of
    2.14          (T1 as (Type (a, [])), T2 as (Type (b, []))) =>
    2.15              if a = b
    2.16 -            then Abs (Name.uu, Type (a, []), Bound 0)
    2.17 +            then mk_identity T1
    2.18              else
    2.19                (case Symreltab.lookup (coes_of ctxt) (a, b) of
    2.20                  NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
    2.21 @@ -692,31 +694,35 @@
    2.22                    end)
    2.23              else
    2.24                let
    2.25 -                fun sub_co (COVARIANT, TU) = SOME (gen TU)
    2.26 -                  | sub_co (CONTRAVARIANT, TU) = SOME (gen (swap TU))
    2.27 -                  | sub_co (INVARIANT_TO _, _) = NONE;
    2.28 +                fun sub_co (COVARIANT, TU) = (SOME (gen TU), NONE)
    2.29 +                  | sub_co (CONTRAVARIANT, TU) = (SOME (gen (swap TU)), NONE)
    2.30 +                  | sub_co (INVARIANT, (T, _)) = (NONE, SOME T)
    2.31 +                  | sub_co (INVARIANT_TO T, _) = (NONE, NONE);
    2.32                  fun ts_of [] = []
    2.33                    | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
    2.34                in
    2.35                  (case Symtab.lookup (tmaps_of ctxt) a of
    2.36                    NONE =>
    2.37                      if Type.could_unify (T1, T2)
    2.38 -                    then Abs (Name.uu, T1, Bound 0)
    2.39 +                    then mk_identity T1
    2.40                      else raise COERCION_GEN_ERROR
    2.41                        (err ++> "No map function for " ^ quote a ^ " known")
    2.42 -                | SOME tmap =>
    2.43 +                | SOME (tmap, variances) =>
    2.44                      let
    2.45 -                      val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));
    2.46 +                      val (used_coes, invarTs) =
    2.47 +                        map_split sub_co (variances ~~ (Ts ~~ Us))
    2.48 +                        |>> map_filter I
    2.49 +                        ||> map_filter I;
    2.50 +                      val Tinsts = ts_of (map fastype_of used_coes) @ invarTs;
    2.51                      in
    2.52                        if null (filter (not o is_identity) used_coes)
    2.53 -                      then Abs (Name.uu, Type (a, Ts), Bound 0)
    2.54 -                      else Term.list_comb
    2.55 -                        (instantiate (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
    2.56 +                      then mk_identity (Type (a, Ts))
    2.57 +                      else Term.list_comb (instantiate tmap Tinsts, used_coes)
    2.58                      end)
    2.59                end
    2.60        | (T, U) =>
    2.61              if Type.could_unify (T, U)
    2.62 -            then Abs (Name.uu, T, Bound 0)
    2.63 +            then mk_identity T
    2.64              else raise COERCION_GEN_ERROR (err ++> "Cannot generate coercion from " ^
    2.65                quote (Syntax.string_of_typ ctxt T) ^ " to " ^
    2.66                quote (Syntax.string_of_typ ctxt U)));
    2.67 @@ -875,17 +881,18 @@
    2.68        handle List.Empty => error ("Not a proper map function:" ^ err_str t);
    2.69  
    2.70      fun gen_arg_var ([], []) = []
    2.71 -      | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
    2.72 +      | gen_arg_var (Ts, (U, U') :: Us) =
    2.73            if U = U' then
    2.74 -            if is_stypeT U then INVARIANT_TO U :: gen_arg_var ((T, T') :: Ts, Us)
    2.75 -            else error ("Invariant xi and yi should be base types:" ^ err_str t)
    2.76 -          else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
    2.77 -          else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
    2.78 -          else error ("Functions do not apply to arguments correctly:" ^ err_str t)
    2.79 -      | gen_arg_var (_, Ts) =
    2.80 -          if forall (op = andf is_stypeT o fst) Ts
    2.81 -          then map (INVARIANT_TO o fst) Ts
    2.82 -          else error ("Different numbers of functions and variant arguments\n" ^ err_str t);
    2.83 +            if null (Term.add_tvarsT U []) then INVARIANT_TO U :: gen_arg_var (Ts, Us)
    2.84 +            else if Term.is_TVar U then INVARIANT :: gen_arg_var (Ts, Us)
    2.85 +            else error ("Invariant xi and yi should be variables or variable-free:" ^ err_str t)
    2.86 +          else
    2.87 +            (case Ts of
    2.88 +              [] => error ("Different numbers of functions and variant arguments\n" ^ err_str t)
    2.89 +            | (T, T') :: Ts =>
    2.90 +              if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
    2.91 +              else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
    2.92 +              else error ("Functions do not apply to arguments correctly:" ^ err_str t));
    2.93  
    2.94      (*retry flag needed to adjust the type lists, when given a map over type constructor fun*)
    2.95      fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry =
    2.96 @@ -915,7 +922,7 @@
    2.97      val path' = fst (split_last path) ~~ tl path;
    2.98      val coercions = map (fst o the o Symreltab.lookup tab) path';
    2.99      val trans_co = singleton (Variable.polymorphic ctxt)
   2.100 -      (fold safe_app coercions (Abs (Name.uu, dummyT, Bound 0)));
   2.101 +      (fold safe_app coercions (mk_identity dummyT));
   2.102      val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co))
   2.103    in
   2.104      (trans_co, ((Ts, Us), coercions))