src/Pure/unify.ML
changeset 16602 0eda2f8a74aa
parent 16425 2427be27cc60
child 16622 f90894e13a3e
     1.1 --- a/src/Pure/unify.ML	Wed Jun 29 15:13:31 2005 +0200
     1.2 +++ b/src/Pure/unify.ML	Wed Jun 29 15:13:32 2005 +0200
     1.3 @@ -36,9 +36,6 @@
     1.4  and trace_types = ref false	(*announce potential incompleteness
     1.5  				  of type unification*)
     1.6  
     1.7 -val thy_ref = ref (NONE: theory option);
     1.8 -fun thy () = the (! thy_ref);
     1.9 -
    1.10  type binderlist = (string*typ) list;
    1.11  
    1.12  type dpair = binderlist * term * term;
    1.13 @@ -177,16 +174,16 @@
    1.14  exception ASSIGN;	(*Raised if not an assignment*)
    1.15  
    1.16  
    1.17 -fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.18 +fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.19    if T=U then env
    1.20 -  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T)
    1.21 +  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T)
    1.22         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.23         handle Type.TUNIFY => raise CANTUNIFY;
    1.24  
    1.25 -fun test_unify_types(args as (T,U,_)) =
    1.26 -let val sot = Sign.string_of_typ (thy ());
    1.27 -    fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
    1.28 -    val env' = unify_types(args)
    1.29 +fun test_unify_types thy (args as (T,U,_)) =
    1.30 +let val str_of = Sign.string_of_typ thy;
    1.31 +    fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
    1.32 +    val env' = unify_types thy args
    1.33  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    1.34     env'
    1.35  end;
    1.36 @@ -209,10 +206,10 @@
    1.37  (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
    1.38    If v occurs rigidly then nonunifiable.
    1.39    If v occurs nonrigidly then must use full algorithm. *)
    1.40 -fun assignment (env, rbinder, t, u) =
    1.41 +fun assignment thy (env, rbinder, t, u) =
    1.42      let val vT as (v,T) = get_eta_var (rbinder, 0, t)
    1.43      in  case rigid_occurs_term (ref [], env, v, u) of
    1.44 -	      NoOcc => let val env = unify_types(body_type env T,
    1.45 +	      NoOcc => let val env = unify_types thy (body_type env T,
    1.46  						 fastype env (rbinder,u),env)
    1.47  		in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
    1.48  	    | Nonrigid =>  raise ASSIGN
    1.49 @@ -225,17 +222,17 @@
    1.50    Checks that binders have same length, since terms should be eta-normal;
    1.51      if not, raises TERM, probably indicating type mismatch.
    1.52    Uses variable a (unless the null string) to preserve user's naming.*) 
    1.53 -fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
    1.54 -	let val env' = unify_types(T,U,env)
    1.55 +fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
    1.56 +	let val env' = unify_types thy (T,U,env)
    1.57  	    val c = if a="" then b else a
    1.58 -	in new_dpair((c,T) :: rbinder, body1, body2, env') end
    1.59 -    | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
    1.60 -    | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
    1.61 -    | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
    1.62 +	in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
    1.63 +    | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
    1.64 +    | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
    1.65 +    | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
    1.66  
    1.67  
    1.68 -fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
    1.69 -     new_dpair (rbinder,
    1.70 +fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env =
    1.71 +     new_dpair thy (rbinder,
    1.72  		eta_norm env (rbinder, Envir.head_norm env t),
    1.73  	  	eta_norm env (rbinder, Envir.head_norm env u), env);
    1.74  
    1.75 @@ -247,11 +244,11 @@
    1.76    Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
    1.77      do so caused numerous problems with no compensating advantage.
    1.78  *)
    1.79 -fun SIMPL0 (dp0, (env,flexflex,flexrigid))
    1.80 +fun SIMPL0 thy (dp0, (env,flexflex,flexrigid))
    1.81  	: Envir.env * dpair list * dpair list =
    1.82 -    let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
    1.83 +    let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0);
    1.84  	    fun SIMRANDS(f$t, g$u, env) =
    1.85 -			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
    1.86 +			SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env))
    1.87  	      | SIMRANDS (t as _$_, _, _) =
    1.88  		raise TERM ("SIMPL: operands mismatch", [t,u])
    1.89  	      | SIMRANDS (t, u as _$_, _) =
    1.90 @@ -260,21 +257,21 @@
    1.91      in case (head_of t, head_of u) of
    1.92         (Var(_,T), Var(_,U)) =>
    1.93  	    let val T' = body_type env T and U' = body_type env U;
    1.94 -		val env = unify_types(T',U',env)
    1.95 +		val env = unify_types thy (T',U',env)
    1.96  	    in (env, dp::flexflex, flexrigid) end
    1.97       | (Var _, _) =>
    1.98 -	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
    1.99 +	    ((assignment thy (env,rbinder,t,u), flexflex, flexrigid)
   1.100  	     handle ASSIGN => (env, flexflex, dp::flexrigid))
   1.101       | (_, Var _) =>
   1.102 -	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
   1.103 +	    ((assignment thy (env,rbinder,u,t), flexflex, flexrigid)
   1.104  	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
   1.105       | (Const(a,T), Const(b,U)) =>
   1.106 -	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.107 +	    if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
   1.108  	    else raise CANTUNIFY
   1.109       | (Bound i,    Bound j)    =>
   1.110  	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
   1.111       | (Free(a,T),  Free(b,U))  =>
   1.112 -	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
   1.113 +	    if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
   1.114  	    else raise CANTUNIFY
   1.115       | _ => raise CANTUNIFY
   1.116      end;
   1.117 @@ -289,12 +286,12 @@
   1.118  
   1.119  (*Recursion needed if any of the 'head variables' have been updated
   1.120    Clever would be to re-do just the affected dpairs*)
   1.121 -fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
   1.122 +fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
   1.123      let val all as (env',flexflex,flexrigid) =
   1.124 -	    foldr SIMPL0 (env,[],[]) dpairs;
   1.125 +	    foldr (SIMPL0 thy) (env,[],[]) dpairs;
   1.126  	val dps = flexrigid@flexflex
   1.127      in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   1.128 -       then SIMPL(env',dps) else all
   1.129 +       then SIMPL thy (env',dps) else all
   1.130      end;
   1.131  
   1.132  
   1.133 @@ -332,7 +329,7 @@
   1.134    For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   1.135    The order for trying projections is crucial in ?b'(?a)   
   1.136    NB "vname" is only used in the call to make_args!!   *)
   1.137 -fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   1.138 +fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
   1.139  	: (term * (Envir.env * dpair list))Seq.seq =
   1.140  let (*Produce copies of uarg and cons them in front of uargs*)
   1.141      fun copycons uarg (uargs, (env, dpairs)) =
   1.142 @@ -349,14 +346,14 @@
   1.143      (*attempt projection on argument with given typ*)
   1.144      val Ts = map (curry (fastype env) rbinder) targs;
   1.145      fun projenv (head, (Us,bary), targ, tail) = 
   1.146 -	let val env = if !trace_types then test_unify_types(base,bary,env)
   1.147 -		      else unify_types(base,bary,env)
   1.148 +	let val env = if !trace_types then test_unify_types thy (base,bary,env)
   1.149 +		      else unify_types thy (base,bary,env)
   1.150  	in Seq.make (fn () =>  
   1.151  	    let val (env',args) = make_args vname (Ts,env,Us);
   1.152  		(*higher-order projection: plug in targs for bound vars*)
   1.153  		fun plugin arg = list_comb(head_of arg, targs);
   1.154  		val dp = (rbinder, list_comb(targ, map plugin args), u);
   1.155 -		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
   1.156 +		val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs)
   1.157  		    (*may raise exception CANTUNIFY*)
   1.158  	    in  SOME ((list_comb(head,args), (env2, frigid@fflex)),
   1.159  			tail)
   1.160 @@ -393,7 +390,7 @@
   1.161  
   1.162  
   1.163  (*Call matchcopy to produce assignments to the variable in the dpair*)
   1.164 -fun MATCH (env, (rbinder,t,u), dpairs)
   1.165 +fun MATCH thy (env, (rbinder,t,u), dpairs)
   1.166  	: (Envir.env * dpair list)Seq.seq = 
   1.167    let val (Var (vT as (v, T)), targs) = strip_comb t;
   1.168        val Ts = binder_types env T;
   1.169 @@ -403,7 +400,7 @@
   1.170  	      NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
   1.171  	    | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   1.172    in Seq.map new_dset
   1.173 -         (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   1.174 +         (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs)))
   1.175    end;
   1.176  
   1.177  
   1.178 @@ -412,10 +409,10 @@
   1.179  
   1.180  (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   1.181    Attempts to update t with u, raising ASSIGN if impossible*)
   1.182 -fun ff_assign(env, rbinder, t, u) : Envir.env = 
   1.183 +fun ff_assign thy (env, rbinder, t, u) : Envir.env = 
   1.184  let val vT as (v,T) = get_eta_var(rbinder,0,t)
   1.185  in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
   1.186 -   else let val env = unify_types(body_type env T,
   1.187 +   else let val env = unify_types thy (body_type env T,
   1.188  				  fastype env (rbinder,u),
   1.189  				  env)
   1.190  	in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
   1.191 @@ -514,7 +511,7 @@
   1.192  
   1.193  (*Simplify both terms and check for assignments.
   1.194    Bound vars in the binder are "banned" unless used in both t AND u *)
   1.195 -fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   1.196 +fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = 
   1.197    let val loot = loose_bnos t  and  loou = loose_bnos u
   1.198        fun add_index (((a,T), j), (bnos, newbinder)) = 
   1.199              if  j mem_int loot  andalso  j mem_int loou 
   1.200 @@ -524,8 +521,8 @@
   1.201        val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
   1.202        val (env', t') = clean_term banned (env, t);
   1.203        val (env'',u') = clean_term banned (env',u)
   1.204 -  in  (ff_assign(env'', rbin', t', u'), tpairs)
   1.205 -      handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
   1.206 +  in  (ff_assign thy (env'', rbin', t', u'), tpairs)
   1.207 +      handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs)
   1.208        handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   1.209    end
   1.210    handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
   1.211 @@ -535,7 +532,7 @@
   1.212    eliminates trivial tpairs like t=t, as well as repeated ones
   1.213    trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   1.214    Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
   1.215 -fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
   1.216 +fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) 
   1.217        : Envir.env * (term*term)list =
   1.218    let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   1.219    in  case  (head_of t, head_of u) of
   1.220 @@ -544,8 +541,8 @@
   1.221  	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
   1.222  	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
   1.223  	else if xless(v,w) then (*prefer to update the LARGER variable*)
   1.224 -	     clean_ffpair ((rbinder, u, t), (env,tpairs))
   1.225 -        else clean_ffpair ((rbinder, t, u), (env,tpairs))
   1.226 +	     clean_ffpair thy ((rbinder, u, t), (env,tpairs))
   1.227 +        else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
   1.228      | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   1.229    end;
   1.230  
   1.231 @@ -553,9 +550,9 @@
   1.232  (*Print a tracing message + list of dpairs.
   1.233    In t==u print u first because it may be rigid or flexible --
   1.234      t is always flexible.*)
   1.235 -fun print_dpairs msg (env,dpairs) =
   1.236 +fun print_dpairs thy msg (env,dpairs) =
   1.237    let fun pdp (rbinder,t,u) =
   1.238 -        let fun termT t = Sign.pretty_term (thy ())
   1.239 +        let fun termT t = Sign.pretty_term thy
   1.240                                (Envir.norm_term env (rlist_abs(rbinder,t)))
   1.241              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   1.242                            termT t];
   1.243 @@ -572,25 +569,24 @@
   1.244  	  Seq.make (fn()=>
   1.245  	  let val (env',flexflex,flexrigid) = 
   1.246  	       (if tdepth> !trace_bound andalso !trace_simp
   1.247 -		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   1.248 -		SIMPL (env,dpairs))
   1.249 +		then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
   1.250 +		SIMPL thy (env,dpairs))
   1.251  	  in case flexrigid of
   1.252 -	      [] => SOME (foldr add_ffpair (env',[]) flexflex, reseq)
   1.253 +	      [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq)
   1.254  	    | dp::frigid' => 
   1.255  		if tdepth > !search_bound then
   1.256  		    (warning "Unification bound exceeded"; Seq.pull reseq)
   1.257  		else
   1.258  		(if tdepth > !trace_bound then
   1.259 -		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
   1.260 +		    print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
   1.261  		 else ();
   1.262  		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
   1.263 -			   (MATCH (env',dp, frigid'@flexflex), reseq)))
   1.264 +			   (MATCH thy (env',dp, frigid'@flexflex), reseq)))
   1.265  	  end
   1.266  	  handle CANTUNIFY => 
   1.267  	    (if tdepth > !trace_bound then tracing"Failure node" else ();
   1.268  	     Seq.pull reseq));
   1.269       val dps = map (fn(t,u)=> ([],t,u)) tus
   1.270 -     val _ = thy_ref := SOME thy;
   1.271    in add_unify 1 ((env, dps), Seq.empty) end;
   1.272  
   1.273  fun unifiers params =