diff -r 80136c4240cc -r b928e3960446 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Fri Oct 29 22:22:36 2010 +0200 +++ b/src/Tools/subtyping.ML Fri Oct 29 22:54:54 2010 +0200 @@ -73,13 +73,9 @@ (** utils **) -val is_param = Type_Infer.is_param -val is_paramT = Type_Infer.is_paramT -val deref = Type_Infer.deref -fun mk_param i S = TVar (("?'a", i), S); (* TODO dup? see src/Pure/type_infer.ML *) - fun nameT (Type (s, [])) = s; fun t_of s = Type (s, []); + fun sort_of (TFree (_, S)) = SOME S | sort_of (TVar (_, S)) = SOME S | sort_of _ = NONE; @@ -87,7 +83,7 @@ val is_typeT = fn (Type _) => true | _ => false; val is_compT = fn (Type (_, _ :: _)) => true | _ => false; val is_freeT = fn (TFree _) => true | _ => false; -val is_fixedvarT = fn (TVar (xi, _)) => not (is_param xi) | _ => false; +val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false; (* unification *) (* TODO dup? needed for weak unification *) @@ -116,10 +112,11 @@ | meet (TVar (xi, S'), S) (tye_idx as (tye, idx)) = if Sign.subsort thy (S', S) then tye_idx else if Type_Infer.is_param xi then - (Vartab.update_new (xi, mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) + (Vartab.update_new + (xi, Type_Infer.mk_param idx (Sign.inter_sort thy (S', S))) tye, idx + 1) else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye) and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) = - meets (Ts, Ss) (meet (deref tye T, S) tye_idx) + meets (Ts, Ss) (meet (Type_Infer.deref tye T, S) tye_idx) | meets _ tye_idx = tye_idx; val weak_meet = if weak then fn _ => I else meet @@ -149,7 +146,7 @@ quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); fun unif (T1, T2) (env as (tye, _)) = - (case pairself (`is_paramT o deref tye) (T1, T2) of + (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of ((true, TVar (xi, S)), (_, T)) => assign xi T S env | ((_, T), (true, TVar (xi, S))) => assign xi T S env | ((_, Type (a, Ts)), (_, Type (b, Us))) => @@ -257,8 +254,8 @@ let val (T, tye_idx', cs') = gen cs bs t tye_idx; val (U', (tye, idx), cs'') = gen cs' bs u tye_idx'; - val U = mk_param idx []; - val V = mk_param (idx + 1) []; + val U = Type_Infer.mk_param idx []; + val V = Type_Infer.mk_param (idx + 1) []; val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2) handle NO_UNIFIER (msg, tye') => err_appl ctxt msg tye' bs t T u U; val error_pack = (bs, t $ u, U, V, U'); @@ -318,8 +315,8 @@ (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx))); val test_update = is_compT orf is_freeT orf is_fixedvarT; val (ch, done') = - if not (null new) then ([], done) - else split_cs (test_update o deref tye') done; + if not (null new) then ([], done) + else split_cs (test_update o Type_Infer.deref tye') done; val todo' = ch @ todo; in simplify done' (new @ todo') (tye', idx') @@ -328,25 +325,25 @@ and expand varleq xi S a Ts error_pack done todo tye idx = let val n = length Ts; - val args = map2 mk_param (idx upto idx + n - 1) (arity_sorts a S); + val args = map2 Type_Infer.mk_param (idx upto idx + n - 1) (arity_sorts a S); val tye' = Vartab.update_new (xi, Type(a, args)) tye; - val (ch, done') = split_cs (is_compT o deref tye') done; + val (ch, done') = split_cs (is_compT o Type_Infer.deref tye') done; val todo' = ch @ todo; val new = if varleq then (Type(a, args), Type (a, Ts)) - else (Type (a, Ts), Type(a, args)); + else (Type (a, Ts), Type (a, args)); in simplify done' ((new, error_pack) :: todo') (tye', idx + n) end (*TU is a pair of a parameter and a free/fixed variable*) and eliminate TU error_pack done todo tye idx = let - val [TVar (xi, S)] = filter is_paramT TU; - val [T] = filter_out is_paramT TU; + val [TVar (xi, S)] = filter Type_Infer.is_paramT TU; + val [T] = filter_out Type_Infer.is_paramT TU; val SOME S' = sort_of T; val test_update = if is_freeT T then is_freeT else is_fixedvarT; val tye' = Vartab.update_new (xi, T) tye; - val (ch, done') = split_cs (test_update o deref tye') done; + val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done; val todo' = ch @ todo; in if subsort (S', S) (*TODO check this*) @@ -355,13 +352,13 @@ end and simplify done [] tye_idx = (done, tye_idx) | simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) = - (case (deref tye T, deref tye U) of + (case (Type_Infer.deref tye T, Type_Infer.deref tye U) of (Type (a, []), Type (b, [])) => if a = b then simplify done todo tye_idx else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx - else err_subtype ctxt (a ^" is not a subtype of " ^ b) (fst tye_idx) error_pack + else err_subtype ctxt (a ^ " is not a subtype of " ^ b) (fst tye_idx) error_pack | (Type (a, Ts), Type (b, Us)) => - if a<>b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack + if a <> b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack else contract a Ts Us error_pack done todo tye idx | (TVar (xi, S), Type (a, Ts as (_ :: _))) => expand true xi S a Ts error_pack done todo tye idx @@ -370,7 +367,7 @@ | (T, U) => if T = U then simplify done todo tye_idx else if exists (is_freeT orf is_fixedvarT) [T, U] andalso - exists is_paramT [T, U] + exists Type_Infer.is_paramT [T, U] then eliminate [T, U] error_pack done todo tye idx else if exists (is_freeT orf is_fixedvarT) [T, U] then err_subtype ctxt "Not eliminated free/fixed variables" @@ -472,18 +469,21 @@ end; fun assign_bound lower G key (tye_idx as (tye, _)) = - if is_paramT (deref tye key) then + if Type_Infer.is_paramT (Type_Infer.deref tye key) then let - val TVar (xi, S) = deref tye key; + val TVar (xi, S) = Type_Infer.deref tye key; val get_bound = if lower then get_preds else get_succs; val raw_bound = get_bound G key; - val bound = map (deref tye) raw_bound; - val not_params = filter_out is_paramT bound; + val bound = map (Type_Infer.deref tye) raw_bound; + val not_params = filter_out Type_Infer.is_paramT bound; fun to_fulfil T = (case sort_of T of NONE => NONE | SOME S => - SOME (map nameT (filter_out is_paramT (map (deref tye) (get_bound G T))), S)); + SOME + (map nameT + (filter_out Type_Infer.is_paramT (map (Type_Infer.deref tye) (get_bound G T))), + S)); val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound); val assignment = if null bound orelse null not_params then NONE @@ -493,10 +493,10 @@ (case assignment of NONE => tye_idx | SOME T => - if is_paramT T then tye_idx + if Type_Infer.is_paramT T then tye_idx else if lower then (*upper bound check*) let - val other_bound = map (deref tye) (get_succs G key); + val other_bound = map (Type_Infer.deref tye) (get_succs G key); val s = nameT T; in if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s) @@ -519,7 +519,7 @@ val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx |> fold (assign_ub G) ts; in - assign_alternating ts (filter (is_paramT o deref tye) ts) G tye_idx' + assign_alternating ts (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx' end; (*Unify all weakly connected components of the constraint forest, @@ -527,7 +527,8 @@ params anyway.*) fun unify_params G (tye_idx as (tye, _)) = let - val max_params = filter (is_paramT o deref tye) (Typ_Graph.maximals G); + val max_params = + filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G); val to_unify = map (fn T => T :: get_preds G T) max_params; in fold unify_list to_unify tye_idx @@ -548,7 +549,7 @@ fun insert_coercions ctxt tye ts = let fun deep_deref T = - (case deref tye T of + (case Type_Infer.deref tye T of Type (a, Ts) => Type (a, map deep_deref Ts) | U => U);