Removed bug in type unification. Negative indexes are not used any longer.
authornipkow
Thu Jan 11 10:29:31 1996 +0100 (1996-01-11)
changeset 1435aefcd255ed4a
parent 1434 834da5152421
child 1436 88b73ad6b0da
Removed bug in type unification. Negative indexes are not used any longer.
Had to change interface to Type.unify to pass maxidx. Thus changes in the
clients.
src/Pure/drule.ML
src/Pure/pattern.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/drule.ML	Tue Jan 09 13:45:58 1996 +0100
     1.2 +++ b/src/Pure/drule.ML	Thu Jan 11 10:29:31 1996 +0100
     1.3 @@ -615,16 +615,17 @@
     1.4  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
     1.5    Instantiates distinct Vars by terms, inferring type instantiations. *)
     1.6  local
     1.7 -  fun add_types ((ct,cu), (sign,tye)) =
     1.8 -    let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
     1.9 -        and {sign=signu, t=u, T= U, ...} = rep_cterm cu
    1.10 +  fun add_types ((ct,cu), (sign,tye,maxidx)) =
    1.11 +    let val {sign=signt, t=t, T= T, maxidx=maxidxt,...} = rep_cterm ct
    1.12 +        and {sign=signu, t=u, T= U, maxidx=maxidxu,...} = rep_cterm cu;
    1.13 +        val maxi = max[maxidx,maxidxt,maxidxu];
    1.14          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
    1.15 -        val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye)
    1.16 +        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
    1.17            handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
    1.18 -    in  (sign', tye')  end;
    1.19 +    in  (sign', tye', maxi')  end;
    1.20  in
    1.21  fun cterm_instantiate ctpairs0 th =
    1.22 -  let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[]))
    1.23 +  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
    1.24        val tsig = #tsig(Sign.rep_sg sign);
    1.25        fun instT(ct,cu) = let val inst = subst_TVars tye
    1.26                           in (cterm_fun inst ct, cterm_fun inst cu) end
     2.1 --- a/src/Pure/pattern.ML	Tue Jan 09 13:45:58 1996 +0100
     2.2 +++ b/src/Pure/pattern.ML	Thu Jan 11 10:29:31 1996 +0100
     2.3 @@ -184,8 +184,8 @@
     2.4  
     2.5  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     2.6    if T=U then env
     2.7 -  else let val iTs' = Type.unify (!tsgr) ((U,T),iTs)
     2.8 -       in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'} end
     2.9 +  else let val (iTs',maxidx') = Type.unify (!tsgr) maxidx iTs (U,T)
    2.10 +       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    2.11         handle Type.TUNIFY => raise Unif;
    2.12  
    2.13  fun unif binders (env,(s,t)) = case (devar env s,devar env t) of
     3.1 --- a/src/Pure/type.ML	Tue Jan 09 13:45:58 1996 +0100
     3.2 +++ b/src/Pure/type.ML	Thu Jan 11 10:29:31 1996 +0100
     3.3 @@ -54,8 +54,8 @@
     3.4    val typ_instance: type_sig * typ * typ -> bool
     3.5    val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
     3.6      -> (indexname * typ) list
     3.7 -  val unify: type_sig -> (typ * typ) * (indexname * typ) list
     3.8 -    -> (indexname * typ) list
     3.9 +  val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ)
    3.10 +    -> (indexname * typ) list * int
    3.11    val raw_unify: typ * typ -> bool
    3.12    exception TUNIFY
    3.13    exception TYPE_MATCH
    3.14 @@ -779,32 +779,32 @@
    3.15      - the substitution needed to unify the actual type of the term with its
    3.16        expected type; only the TVars in the expected type are included.
    3.17  
    3.18 -  During type inference all TVars in the term have negative index. This keeps
    3.19 -  them apart from normal TVars, which is essential, because at the end the
    3.20 -  type of the term is unified with the expected type, which contains normal
    3.21 -  TVars.
    3.22 +  During type inference all TVars in the term have index > maxidx, where
    3.23 +  maxidx is the max. index in the expected type of the term (T). This keeps
    3.24 +  them apart, because at the end the type of the term is unified with T.
    3.25  
    3.26    1. Add initial type information to the term (attach_types).
    3.27       This freezes (freeze_vars) TVars in explicitly provided types (eg
    3.28       constraints or defaults) by turning them into TFrees.
    3.29 -  2. Carry out type inference, possibly introducing new negative TVars.
    3.30 +  2. Carry out type inference.
    3.31    3. Unify actual and expected type.
    3.32 -  4. Turn all (negative) TVars into unique new TFrees (freeze).
    3.33 +  4. Turn all local (i.e. > maxidx) TVars into unique new TFrees (freeze).
    3.34    5. Thaw all TVars frozen in step 1 (thaw_vars).
    3.35  *)
    3.36  
    3.37  (*Raised if types are not unifiable*)
    3.38  exception TUNIFY;
    3.39  
    3.40 -val tyvar_count = ref ~1;
    3.41 +val tyvar_count = ref 0;
    3.42  
    3.43 -fun tyinit() = (tyvar_count := ~1);
    3.44 +fun tyinit(i) = (tyvar_count := i);
    3.45  
    3.46 -fun new_tvar_inx () = (tyvar_count := ! tyvar_count - 1; ! tyvar_count)
    3.47 +fun new_tvar_inx () = (tyvar_count := !tyvar_count + 1; !tyvar_count)
    3.48  
    3.49  (*
    3.50 -Generate new TVar.  Index is < ~1 to distinguish it from TVars generated from
    3.51 -variable names (see id_type).  Name is arbitrary because index is new.
    3.52 +Generate new TVar.  Index is > maxidx+1 to distinguish it from TVars
    3.53 +generated from variable names (see id_type).
    3.54 +Name is arbitrary because index is new.
    3.55  *)
    3.56  
    3.57  fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()), S);
    3.58 @@ -862,7 +862,7 @@
    3.59  (* Order-sorted Unification of Types (U)  *)
    3.60  
    3.61  (* Precondition: both types are well-formed w.r.t. type constructor arities *)
    3.62 -fun unify (tsig as TySg{subclass, arities, ...}) =
    3.63 +fun unify1 (tsig as TySg{subclass, arities, ...}) =
    3.64    let fun unif ((T, U), tye) =
    3.65          case (devar(T, tye), devar(U, tye)) of
    3.66            (T as TVar(v, S1), U as TVar(w, S2)) =>
    3.67 @@ -880,11 +880,13 @@
    3.68          | (T, U) => if T=U then tye else raise TUNIFY
    3.69    in unif end;
    3.70  
    3.71 +fun unify tsig maxidx tye TU =
    3.72 +  (tyinit maxidx; (unify1 tsig (TU,tye), !tyvar_count) );
    3.73  
    3.74  (* raw_unify (ignores sorts) *)
    3.75  
    3.76  fun raw_unify (ty1, ty2) =
    3.77 -  (unify tsig0 ((rem_sorts ty1, rem_sorts ty2), []); true)
    3.78 +  (unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true)
    3.79      handle TUNIFY => false;
    3.80  
    3.81  
    3.82 @@ -905,11 +907,11 @@
    3.83  		val msg = "function type is incompatible with argument type"
    3.84              in case T of
    3.85                   Type("fun", [T1, T2]) =>
    3.86 -                   ( (T2, unify tsig ((T1, U), tyeT))
    3.87 +                   ( (T2, unify1 tsig ((T1, U), tyeT))
    3.88                       handle TUNIFY => err msg)
    3.89                 | TVar _ =>
    3.90                     let val T2 = gen_tyvar([])
    3.91 -                   in (T2, unify tsig ((T, U-->T2), tyeT))
    3.92 +                   in (T2, unify1 tsig ((T, U-->T2), tyeT))
    3.93                        handle TUNIFY => err msg
    3.94                     end
    3.95                 | _ => err"function type is expected in application"
    3.96 @@ -925,8 +927,10 @@
    3.97  (*Find type of ident.  If not in table then use ident's name for tyvar
    3.98    to get consistent typing.*)
    3.99  fun new_id_type a = TVar(("'"^a, new_tvar_inx()), []);
   3.100 -fun type_of_ixn(types, ixn as (a, _)) =
   3.101 -  case types ixn of Some T => freeze_vars T | None => TVar(("'"^a, ~1), []);
   3.102 +
   3.103 +fun type_of_ixn(types, ixn as (a, _),maxidx1) =
   3.104 +  case types ixn of Some T => freeze_vars T
   3.105 +                  | None   => TVar(("'"^a, maxidx1), []);
   3.106  
   3.107  fun constrain (term, T) = Const (Syntax.constrainC, T --> T) $ term;
   3.108  
   3.109 @@ -944,12 +948,11 @@
   3.110    The atoms in the resulting term satisfy the following spec:
   3.111  
   3.112    Const (a, T):
   3.113 -    T is a renamed copy of the generic type of a; renaming decreases index of
   3.114 -    all TVars by new_tvar_inx(), which is less than ~1. The index of all
   3.115 -    TVars in the generic type must be 0 for this to work!
   3.116 +    T is a renamed copy of the generic type of a; renaming increases index of
   3.117 +    all TVars by new_tvar_inx(), which is > maxidx+1.
   3.118  
   3.119    Free (a, T), Var (ixn, T):
   3.120 -    T is either the frozen default type of a or TVar (("'"^a, ~1), [])
   3.121 +    T is either the frozen default type of a or TVar (("'"^a, maxidx+1), [])
   3.122  
   3.123    Abs (a, T, _):
   3.124      T is either a type constraint or TVar (("'" ^ a, i), []), where i is
   3.125 @@ -959,7 +962,7 @@
   3.126  
   3.127  (* FIXME consistency of sort_env / sorts (!?) *)
   3.128  
   3.129 -fun attach_types (tsig, const_type, types, sorts) tm =
   3.130 +fun attach_types (tsig, const_type, types, sorts, maxidx1) tm =
   3.131    let
   3.132      val sort_env = Syntax.raw_term_sorts tm;
   3.133      fun def_sort xi = if_none (sorts xi) (defaultS tsig);
   3.134 @@ -974,8 +977,8 @@
   3.135        | add (Free (a, _)) =
   3.136            (case const_type a of
   3.137              Some T => type_const (a, T)
   3.138 -          | None => Free (a, type_of_ixn (types, (a, ~1))))
   3.139 -      | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn))
   3.140 +          | None => Free (a, type_of_ixn (types,(a,~1),maxidx1)))
   3.141 +      | add (Var (ixn, _)) = Var (ixn, type_of_ixn (types, ixn, maxidx1))
   3.142        | add (Bound i) = Bound i
   3.143        | add (Abs (a, _, body)) = Abs (a, new_id_type a, add body)
   3.144        | add ((f as Const (a, _) $ t1) $ t2) =
   3.145 @@ -1039,9 +1042,9 @@
   3.146    in map_type_tfree thaw end;
   3.147  
   3.148  
   3.149 -fun restrict tye =
   3.150 +fun restrict maxidx1 tye =
   3.151    let fun clean(tye1, ((a, i), T)) =
   3.152 -        if i < 0 then tye1 else ((a, i), inst_typ tye T) :: tye1
   3.153 +        if i >= maxidx1 then tye1 else ((a, i), inst_typ tye T) :: tye1
   3.154    in foldl clean ([], tye) end
   3.155  
   3.156  
   3.157 @@ -1051,24 +1054,23 @@
   3.158    sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   3.159    used is the list of already used type variables.
   3.160    If freeze then internal TVars are turned into TFrees, else TVars.*)
   3.161 -fun infer_terms (tsig, const_type, types, sorts, used, freeze, Ts, ts) =
   3.162 +fun infer_types (tsig, const_type, types, sorts, used, freeze, Ts, ts) =
   3.163    let
   3.164 -    val us = map (attach_types (tsig, const_type, types, sorts)) ts;
   3.165 +    val maxidx1 = max(map maxidx_of_typ Ts)+1;
   3.166 +    val () = tyinit(maxidx1+1);
   3.167 +    val us = map (attach_types (tsig, const_type, types, sorts, maxidx1)) ts;
   3.168      val u = list_comb(Const("",Ts ---> propT),us)
   3.169      val (_, tye) = infer tsig ([], u, []);
   3.170      val uu = unconstrain u;
   3.171 -    val Ttye = restrict tye (*restriction to TVars in Ts*)
   3.172 +    val Ttye = restrict maxidx1 tye (*restriction to TVars in Ts*)
   3.173      val all = Const("", Type("", map snd Ttye)) $ (inst_types tye uu)
   3.174        (*all is a dummy term which contains all exported TVars*)
   3.175      val Const(_, Type(_, Us)) $ u'' =
   3.176 -      map_term_types thaw_vars (convert used freeze (fn (_, i) => i < 0) all)
   3.177 +      map_term_types thaw_vars (convert used freeze (fn (_,i) => i >= maxidx1) all)
   3.178        (*convert all internally generated TVars into TFrees or TVars
   3.179          and thaw all initially frozen TVars*)
   3.180    in
   3.181      (snd(strip_comb u''), (map fst Ttye) ~~ Us)
   3.182    end;
   3.183  
   3.184 -fun infer_types args = (tyinit (); infer_terms args);
   3.185 -
   3.186 -
   3.187  end;
     4.1 --- a/src/Pure/unify.ML	Tue Jan 09 13:45:58 1996 +0100
     4.2 +++ b/src/Pure/unify.ML	Thu Jan 11 10:29:31 1996 +0100
     4.3 @@ -242,10 +242,11 @@
     4.4  
     4.5  
     4.6  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     4.7 -	if T=U then env else
     4.8 -	let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs)
     4.9 -	in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'}
    4.10 -	end handle Sign.Type.TUNIFY => raise CANTUNIFY;
    4.11 +  if T=U then env
    4.12 +  else let val (iTs',maxidx') = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr)))
    4.13 +                                                maxidx iTs (U,T)
    4.14 +       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    4.15 +       handle Sign.Type.TUNIFY => raise CANTUNIFY;
    4.16  
    4.17  fun test_unify_types(args as (T,U,_)) =
    4.18  let val sot = Sign.string_of_typ (!sgr);