more sharing of operations, without aliases;
authorwenzelm
Fri Oct 29 22:54:54 2010 +0200 (2010-10-29)
changeset 40286b928e3960446
parent 40285 80136c4240cc
child 40287 4af3706bcd5d
more sharing of operations, without aliases;
src/Pure/type_infer.ML
src/Tools/subtyping.ML
     1.1 --- a/src/Pure/type_infer.ML	Fri Oct 29 22:22:36 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Fri Oct 29 22:54:54 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    val is_param: indexname -> bool
     1.5    val is_paramT: typ -> bool
     1.6    val param: int -> string * sort -> typ
     1.7 +  val mk_param: int -> sort -> typ
     1.8    val anyT: sort -> typ
     1.9    val paramify_vars: typ -> typ
    1.10    val paramify_dummies: typ -> int -> typ * int
     2.1 --- a/src/Tools/subtyping.ML	Fri Oct 29 22:22:36 2010 +0200
     2.2 +++ b/src/Tools/subtyping.ML	Fri Oct 29 22:54:54 2010 +0200
     2.3 @@ -73,13 +73,9 @@
     2.4  
     2.5  (** utils **)
     2.6  
     2.7 -val is_param = Type_Infer.is_param
     2.8 -val is_paramT = Type_Infer.is_paramT
     2.9 -val deref = Type_Infer.deref
    2.10 -fun mk_param i S = TVar (("?'a", i), S); (* TODO dup? see src/Pure/type_infer.ML *)
    2.11 -
    2.12  fun nameT (Type (s, [])) = s;
    2.13  fun t_of s = Type (s, []);
    2.14 +
    2.15  fun sort_of (TFree (_, S)) = SOME S
    2.16    | sort_of (TVar (_, S)) = SOME S
    2.17    | sort_of _ = NONE;
    2.18 @@ -87,7 +83,7 @@
    2.19  val is_typeT = fn (Type _) => true | _ => false;
    2.20  val is_compT = fn (Type (_, _ :: _)) => true | _ => false;
    2.21  val is_freeT = fn (TFree _) => true | _ => false;
    2.22 -val is_fixedvarT = fn (TVar (xi, _)) => not (is_param xi) | _ => false;
    2.23 +val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
    2.24  
    2.25  
    2.26  (* unification *)  (* TODO dup? needed for weak unification *)
    2.27 @@ -116,10 +112,11 @@
    2.28        | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) =
    2.29            if Sign.subsort thy (S', S) then tye_idx
    2.30            else if Type_Infer.is_param xi then
    2.31 -            (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
    2.32 +            (Vartab.update_new
    2.33 +              (xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1)
    2.34            else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
    2.35      and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
    2.36 -          meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
    2.37 +          meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx)
    2.38        | meets _ tye_idx = tye_idx;
    2.39  
    2.40      val weak_meet = if weak then fn _ => I else meet
    2.41 @@ -149,7 +146,7 @@
    2.42        quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
    2.43  
    2.44      fun unif (T1, T2) (env as (tye, _)) =
    2.45 -      (case pairself (`is_paramT o deref tye) (T1, T2) of
    2.46 +      (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
    2.47          ((true, TVar (xi, S)), (_, T)) => assign xi T S env
    2.48        | ((_, T), (true, TVar (xi, S))) => assign xi T S env
    2.49        | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
    2.50 @@ -257,8 +254,8 @@
    2.51            let
    2.52              val (T, tye_idx', cs') = gen cs bs t tye_idx;
    2.53              val (U', (tye, idx), cs'') = gen cs' bs u tye_idx';
    2.54 -            val U = mk_param idx [];
    2.55 -            val V = mk_param (idx + 1) [];
    2.56 +            val U = Type_Infer.mk_param idx [];
    2.57 +            val V = Type_Infer.mk_param (idx + 1) [];
    2.58              val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2)
    2.59                handle NO_UNIFIER (msg, tye') => err_appl ctxt msg tye' bs t T u U;
    2.60              val error_pack = (bs, t $ u, U, V, U');
    2.61 @@ -318,8 +315,8 @@
    2.62                (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
    2.63              val test_update = is_compT orf is_freeT orf is_fixedvarT;
    2.64              val (ch, done') =
    2.65 -              if not (null new) then ([],   done)
    2.66 -              else split_cs (test_update o deref tye') done;
    2.67 +              if not (null new) then ([], done)
    2.68 +              else split_cs (test_update o Type_Infer.deref tye') done;
    2.69              val todo' = ch @ todo;
    2.70            in
    2.71              simplify done' (new @ todo') (tye', idx')
    2.72 @@ -328,25 +325,25 @@
    2.73          and expand varleq xi S a Ts error_pack done todo tye idx =
    2.74            let
    2.75              val n = length Ts;
    2.76 -            val args = map2 mk_param (idx upto idx + n - 1) (arity_sorts a S);
    2.77 +            val args = map2 Type_Infer.mk_param (idx upto idx + n - 1) (arity_sorts a S);
    2.78              val tye' = Vartab.update_new (xi, Type(a, args)) tye;
    2.79 -            val (ch, done') = split_cs (is_compT o deref tye') done;
    2.80 +            val (ch, done') = split_cs (is_compT o Type_Infer.deref tye') done;
    2.81              val todo' = ch @ todo;
    2.82              val new =
    2.83                if varleq then (Type(a, args), Type (a, Ts))
    2.84 -              else (Type (a, Ts), Type(a, args));
    2.85 +              else (Type (a, Ts), Type (a, args));
    2.86            in
    2.87              simplify done' ((new, error_pack) :: todo') (tye', idx + n)
    2.88            end
    2.89          (*TU is a pair of a parameter and a free/fixed variable*)
    2.90          and eliminate TU error_pack done todo tye idx =
    2.91            let
    2.92 -            val [TVar (xi, S)] = filter is_paramT TU;
    2.93 -            val [T] = filter_out is_paramT TU;
    2.94 +            val [TVar (xi, S)] = filter Type_Infer.is_paramT TU;
    2.95 +            val [T] = filter_out Type_Infer.is_paramT TU;
    2.96              val SOME S' = sort_of T;
    2.97              val test_update = if is_freeT T then is_freeT else is_fixedvarT;
    2.98              val tye' = Vartab.update_new (xi, T) tye;
    2.99 -            val (ch, done') = split_cs (test_update o deref tye') done;
   2.100 +            val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done;
   2.101              val todo' = ch @ todo;
   2.102            in
   2.103              if subsort (S', S) (*TODO check this*)
   2.104 @@ -355,13 +352,13 @@
   2.105            end
   2.106          and simplify done [] tye_idx = (done, tye_idx)
   2.107            | simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) =
   2.108 -              (case (deref tye T, deref tye U) of
   2.109 +              (case (Type_Infer.deref tye T, Type_Infer.deref tye U) of
   2.110                  (Type (a, []), Type (b, [])) =>
   2.111                    if a = b then simplify done todo tye_idx
   2.112                    else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx
   2.113 -                  else err_subtype ctxt (a ^" is not a subtype of " ^ b) (fst tye_idx) error_pack
   2.114 +                  else err_subtype ctxt (a ^ " is not a subtype of " ^ b) (fst tye_idx) error_pack
   2.115                | (Type (a, Ts), Type (b, Us)) =>
   2.116 -                  if a<>b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack
   2.117 +                  if a <> b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack
   2.118                    else contract a Ts Us error_pack done todo tye idx
   2.119                | (TVar (xi, S), Type (a, Ts as (_ :: _))) =>
   2.120                    expand true xi S a Ts error_pack done todo tye idx
   2.121 @@ -370,7 +367,7 @@
   2.122                | (T, U) =>
   2.123                    if T = U then simplify done todo tye_idx
   2.124                    else if exists (is_freeT orf is_fixedvarT) [T, U] andalso
   2.125 -                    exists is_paramT [T, U]
   2.126 +                    exists Type_Infer.is_paramT [T, U]
   2.127                    then eliminate [T, U] error_pack done todo tye idx
   2.128                    else if exists (is_freeT orf is_fixedvarT) [T, U]
   2.129                    then err_subtype ctxt "Not eliminated free/fixed variables"
   2.130 @@ -472,18 +469,21 @@
   2.131        end;
   2.132  
   2.133      fun assign_bound lower G key (tye_idx as (tye, _)) =
   2.134 -      if is_paramT (deref tye key) then
   2.135 +      if Type_Infer.is_paramT (Type_Infer.deref tye key) then
   2.136          let
   2.137 -          val TVar (xi, S) = deref tye key;
   2.138 +          val TVar (xi, S) = Type_Infer.deref tye key;
   2.139            val get_bound = if lower then get_preds else get_succs;
   2.140            val raw_bound = get_bound G key;
   2.141 -          val bound = map (deref tye) raw_bound;
   2.142 -          val not_params = filter_out is_paramT bound;
   2.143 +          val bound = map (Type_Infer.deref tye) raw_bound;
   2.144 +          val not_params = filter_out Type_Infer.is_paramT bound;
   2.145            fun to_fulfil T =
   2.146              (case sort_of T of
   2.147                NONE => NONE
   2.148              | SOME S =>
   2.149 -                SOME (map nameT (filter_out is_paramT (map (deref tye) (get_bound G T))), S));
   2.150 +                SOME
   2.151 +                  (map nameT
   2.152 +                    (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))),
   2.153 +                      S));
   2.154            val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound);
   2.155            val assignment =
   2.156              if null bound orelse null not_params then NONE
   2.157 @@ -493,10 +493,10 @@
   2.158            (case assignment of
   2.159              NONE => tye_idx
   2.160            | SOME T =>
   2.161 -              if is_paramT T then tye_idx
   2.162 +              if Type_Infer.is_paramT T then tye_idx
   2.163                else if lower then (*upper bound check*)
   2.164                  let
   2.165 -                  val other_bound = map (deref tye) (get_succs G key);
   2.166 +                  val other_bound = map (Type_Infer.deref tye) (get_succs G key);
   2.167                    val s = nameT T;
   2.168                  in
   2.169                    if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s)
   2.170 @@ -519,7 +519,7 @@
   2.171            val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
   2.172              |> fold (assign_ub G) ts;
   2.173          in
   2.174 -          assign_alternating ts (filter (is_paramT o deref tye) ts) G tye_idx'
   2.175 +          assign_alternating ts (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
   2.176          end;
   2.177  
   2.178      (*Unify all weakly connected components of the constraint forest,
   2.179 @@ -527,7 +527,8 @@
   2.180        params anyway.*)
   2.181      fun unify_params G (tye_idx as (tye, _)) =
   2.182        let
   2.183 -        val max_params = filter (is_paramT o deref tye) (Typ_Graph.maximals G);
   2.184 +        val max_params =
   2.185 +          filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
   2.186          val to_unify = map (fn T => T :: get_preds G T) max_params;
   2.187        in
   2.188          fold unify_list to_unify tye_idx
   2.189 @@ -548,7 +549,7 @@
   2.190  fun insert_coercions ctxt tye ts =
   2.191    let
   2.192      fun deep_deref T =
   2.193 -      (case deref tye T of
   2.194 +      (case Type_Infer.deref tye T of
   2.195          Type (a, Ts) => Type (a, map deep_deref Ts)
   2.196        | U => U);
   2.197