src/Pure/unify.ML

 val trace_bound = ref 25	(*tracing starts above this depth, 0 for full*)
 and search_bound = ref 30	(*unification quits above this depth*)
 and trace_simp = ref false	(*print dpairs before calling SIMPL*)
 and trace_types = ref false	(*announce potential incompleteness
 				  of type unification*)
+
+val thy_ref = ref (NONE: theory option);
+fun thy () = the (! thy_ref);
 
 type binderlist = (string*typ) list;
 
 type dpair = binderlist * term * term;
 

 
 exception CANTUNIFY;	(*Signals non-unifiability.  Does not signal errors!*)
 exception ASSIGN;	(*Raised if not an assignment*)
 
 
-fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
+fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
-  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T)
+  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise CANTUNIFY;
 
-fun test_unify_types thy (args as (T,U,_)) =
-let val str_of = Sign.string_of_typ thy;
-    fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
-    val env' = unify_types thy args
+fun test_unify_types(args as (T,U,_)) =
+let val sot = Sign.string_of_typ (thy ());
+    fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
+    val env' = unify_types(args)
 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    env'
 end;
 
 (*Is the term eta-convertible to a single variable with the given rbinder?

 
 
 (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
   If v occurs rigidly then nonunifiable.
   If v occurs nonrigidly then must use full algorithm. *)
-fun assignment thy (env, rbinder, t, u) =
+fun assignment (env, rbinder, t, u) =
     let val vT as (v,T) = get_eta_var (rbinder, 0, t)
     in  case rigid_occurs_term (ref [], env, v, u) of
-	      NoOcc => let val env = unify_types thy (body_type env T,
+	      NoOcc => let val env = unify_types(body_type env T,
 						 fastype env (rbinder,u),env)
 		in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
 	    | Nonrigid =>  raise ASSIGN
 	    | Rigid =>  raise CANTUNIFY
     end;

 (*Extends an rbinder with a new disagreement pair, if both are abstractions.
   Tries to unify types of the bound variables!
   Checks that binders have same length, since terms should be eta-normal;
     if not, raises TERM, probably indicating type mismatch.
   Uses variable a (unless the null string) to preserve user's naming.*) 
-fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
-	let val env' = unify_types thy (T,U,env)
+fun new_dpair (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
+	let val env' = unify_types(T,U,env)
 	    val c = if a="" then b else a
-	in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
-    | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
-    | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
-    | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
-
-
-fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env =
-     new_dpair thy (rbinder,
+	in new_dpair((c,T) :: rbinder, body1, body2, env') end
+    | new_dpair (_, Abs _, _, _) = raise TERM ("new_dpair", [])
+    | new_dpair (_, _, Abs _, _) = raise TERM ("new_dpair", [])
+    | new_dpair (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
+
+
+fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
+     new_dpair (rbinder,
 		eta_norm env (rbinder, Envir.head_norm env t),
 	  	eta_norm env (rbinder, Envir.head_norm env u), env);
 
 
 

   Does not perform assignments for flex-flex pairs:
     may create nonrigid paths, which prevent other assignments.
   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
     do so caused numerous problems with no compensating advantage.
 *)
-fun SIMPL0 thy (dp0, (env,flexflex,flexrigid))
+fun SIMPL0 (dp0, (env,flexflex,flexrigid))
 	: Envir.env * dpair list * dpair list =
-    let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0);
+    let val (dp as (rbinder,t,u), env) = head_norm_dpair(env,dp0);
 	    fun SIMRANDS(f$t, g$u, env) =
-			SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env))
+			SIMPL0((rbinder,t,u), SIMRANDS(f,g,env))
 	      | SIMRANDS (t as _$_, _, _) =
 		raise TERM ("SIMPL: operands mismatch", [t,u])
 	      | SIMRANDS (t, u as _$_, _) =
 		raise TERM ("SIMPL: operands mismatch", [t,u])
 	      | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
     in case (head_of t, head_of u) of
        (Var(_,T), Var(_,U)) =>
 	    let val T' = body_type env T and U' = body_type env U;
-		val env = unify_types thy (T',U',env)
+		val env = unify_types(T',U',env)
 	    in (env, dp::flexflex, flexrigid) end
      | (Var _, _) =>
-	    ((assignment thy (env,rbinder,t,u), flexflex, flexrigid)
+	    ((assignment (env,rbinder,t,u), flexflex, flexrigid)
 	     handle ASSIGN => (env, flexflex, dp::flexrigid))
      | (_, Var _) =>
-	    ((assignment thy (env,rbinder,u,t), flexflex, flexrigid)
+	    ((assignment (env,rbinder,u,t), flexflex, flexrigid)
 	     handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
      | (Const(a,T), Const(b,U)) =>
-	    if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
+	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
 	    else raise CANTUNIFY
      | (Bound i,    Bound j)    =>
 	    if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
      | (Free(a,T),  Free(b,U))  =>
-	    if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
+	    if a=b then SIMRANDS(t,u, unify_types(T,U,env))
 	    else raise CANTUNIFY
      | _ => raise CANTUNIFY
     end;
 
 

   | changed _ = false;
 
 
 (*Recursion needed if any of the 'head variables' have been updated
   Clever would be to re-do just the affected dpairs*)
-fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
+fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
     let val all as (env',flexflex,flexrigid) =
-	    foldr (SIMPL0 thy) (env,[],[]) dpairs;
+	    foldr SIMPL0 (env,[],[]) dpairs;
 	val dps = flexrigid@flexflex
     in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
-       then SIMPL thy (env',dps) else all
+       then SIMPL(env',dps) else all
     end;
 
 
 (*computes t(Bound(n+k-1),...,Bound(n))  *)
 fun combound (t, n, k) = 

     or if u is a variable (flex-flex dpair).
   Returns long sequence of every way of copying u, for backtracking
   For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   The order for trying projections is crucial in ?b'(?a)   
   NB "vname" is only used in the call to make_args!!   *)
-fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
+fun matchcopy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs)) 
 	: (term * (Envir.env * dpair list))Seq.seq =
 let (*Produce copies of uarg and cons them in front of uargs*)
     fun copycons uarg (uargs, (env, dpairs)) =
 	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
 	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),

     val base = body_type env (fastype env (rbinder,uhead));
     fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
     (*attempt projection on argument with given typ*)
     val Ts = map (curry (fastype env) rbinder) targs;
     fun projenv (head, (Us,bary), targ, tail) = 
-	let val env = if !trace_types then test_unify_types thy (base,bary,env)
-		      else unify_types thy (base,bary,env)
+	let val env = if !trace_types then test_unify_types(base,bary,env)
+		      else unify_types(base,bary,env)
 	in Seq.make (fn () =>  
 	    let val (env',args) = make_args vname (Ts,env,Us);
 		(*higher-order projection: plug in targs for bound vars*)
 		fun plugin arg = list_comb(head_of arg, targs);
 		val dp = (rbinder, list_comb(targ, map plugin args), u);
-		val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs)
+		val (env2,frigid,fflex) = SIMPL (env', dp::dpairs)
 		    (*may raise exception CANTUNIFY*)
 	    in  SOME ((list_comb(head,args), (env2, frigid@fflex)),
 			tail)
 	    end  handle CANTUNIFY => Seq.pull tail)
 	end handle CANTUNIFY => tail;

 end
 in mc end;
 
 
 (*Call matchcopy to produce assignments to the variable in the dpair*)
-fun MATCH thy (env, (rbinder,t,u), dpairs)
+fun MATCH (env, (rbinder,t,u), dpairs)
 	: (Envir.env * dpair list)Seq.seq = 
   let val (Var (vT as (v, T)), targs) = strip_comb t;
       val Ts = binder_types env T;
       fun new_dset (u', (env',dpairs')) =
 	  (*if v was updated to s, must unify s with u' *)
 	  case Envir.lookup (env', vT) of
 	      NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
 	    | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   in Seq.map new_dset
-         (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs)))
+         (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
   end;
 
 
 
 (**** Flex-flex processing ****)
 
 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   Attempts to update t with u, raising ASSIGN if impossible*)
-fun ff_assign thy (env, rbinder, t, u) : Envir.env = 
+fun ff_assign(env, rbinder, t, u) : Envir.env = 
 let val vT as (v,T) = get_eta_var(rbinder,0,t)
 in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
-   else let val env = unify_types thy (body_type env T,
+   else let val env = unify_types(body_type env T,
 				  fastype env (rbinder,u),
 				  env)
 	in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
 end;
 

   in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
 
 
 (*Simplify both terms and check for assignments.
   Bound vars in the binder are "banned" unless used in both t AND u *)
-fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) = 
+fun clean_ffpair ((rbinder, t, u), (env,tpairs)) = 
   let val loot = loose_bnos t  and  loou = loose_bnos u
       fun add_index (((a,T), j), (bnos, newbinder)) = 
             if  j mem_int loot  andalso  j mem_int loou 
             then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
             else  (j::bnos, newbinder);		(*remove*)
       val indices = 0 upto (length rbinder - 1);
       val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
       val (env', t') = clean_term banned (env, t);
       val (env'',u') = clean_term banned (env',u)
-  in  (ff_assign thy (env'', rbin', t', u'), tpairs)
-      handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs)
+  in  (ff_assign(env'', rbin', t', u'), tpairs)
+      handle ASSIGN => (ff_assign(env'', rbin', u', t'), tpairs)
       handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
   end
   handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
 
 
 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   eliminates trivial tpairs like t=t, as well as repeated ones
   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t 
   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
-fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) 
+fun add_ffpair ((rbinder,t0,u0), (env,tpairs)) 
       : Envir.env * (term*term)list =
   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   in  case  (head_of t, head_of u) of
       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
 	if eq_ix(v,w) then     (*...occur check would falsely return true!*)
 	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
 	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
 	else if xless(v,w) then (*prefer to update the LARGER variable*)
-	     clean_ffpair thy ((rbinder, u, t), (env,tpairs))
-        else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
+	     clean_ffpair ((rbinder, u, t), (env,tpairs))
+        else clean_ffpair ((rbinder, t, u), (env,tpairs))
     | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
   end;
 
 
 (*Print a tracing message + list of dpairs.
   In t==u print u first because it may be rigid or flexible --
     t is always flexible.*)
-fun print_dpairs thy msg (env,dpairs) =
+fun print_dpairs msg (env,dpairs) =
   let fun pdp (rbinder,t,u) =
-        let fun termT t = Sign.pretty_term thy
+        let fun termT t = Sign.pretty_term (thy ())
                               (Envir.norm_term env (rlist_abs(rbinder,t)))
             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
                           termT t];
         in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
   in  tracing msg;  List.app pdp dpairs  end;

   : (Envir.env * (term*term)list)Seq.seq =
   let fun add_unify tdepth ((env,dpairs), reseq) =
 	  Seq.make (fn()=>
 	  let val (env',flexflex,flexrigid) = 
 	       (if tdepth> !trace_bound andalso !trace_simp
-		then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
-		SIMPL thy (env,dpairs))
+		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
+		SIMPL (env,dpairs))
 	  in case flexrigid of
-	      [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq)
+	      [] => SOME (foldr add_ffpair (env',[]) flexflex, reseq)
 	    | dp::frigid' => 
 		if tdepth > !search_bound then
 		    (warning "Unification bound exceeded"; Seq.pull reseq)
 		else
 		(if tdepth > !trace_bound then
-		    print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
+		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)
 		 else ();
 		 Seq.pull (Seq.it_right (add_unify (tdepth+1))
-			   (MATCH thy (env',dp, frigid'@flexflex), reseq)))
+			   (MATCH (env',dp, frigid'@flexflex), reseq)))
 	  end
 	  handle CANTUNIFY => 
 	    (if tdepth > !trace_bound then tracing"Failure node" else ();
 	     Seq.pull reseq));
      val dps = map (fn(t,u)=> ([],t,u)) tus
+     val _ = thy_ref := SOME thy;
   in add_unify 1 ((env, dps), Seq.empty) end;
 
 fun unifiers params =
   Seq.cons ((Pattern.unify params, []), Seq.empty)
     handle Pattern.Unif => Seq.empty