src/Pure/pattern.ML
changeset 14875 c48d086264c4
parent 14861 ca5cae7fb65a
child 14981 e73f8140af78
--- a/src/Pure/pattern.ML	Sat Jun 05 13:07:31 2004 +0200
+++ b/src/Pure/pattern.ML	Sat Jun 05 13:07:49 2004 +0200
@@ -46,19 +46,16 @@
 
 val trace_unify_fail = ref false;
 
-(* Only for communication between unification and error message printing *)
-val sgr = ref Sign.pre_pure
-
-fun string_of_term env binders t = Sign.string_of_term (!sgr)
+fun string_of_term sg env binders t = Sign.string_of_term sg
   (Envir.norm_term env (subst_bounds(map Free binders,t)));
 
 fun bname binders i = fst(nth_elem(i,binders));
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
-fun typ_clash(tye,T,U) =
+fun typ_clash sg (tye,T,U) =
   if !trace_unify_fail
-  then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T)
-           and u = Sign.string_of_typ (!sgr) (Envir.norm_type tye U)
+  then let val t = Sign.string_of_typ sg (Envir.norm_type tye T)
+           and u = Sign.string_of_typ sg (Envir.norm_type tye U)
        in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   else ()
 
@@ -76,11 +73,11 @@
   if !trace_unify_fail then clash (boundVar binders i) s
   else ()
 
-fun proj_fail(env,binders,F,is,t) =
+fun proj_fail sg (env,binders,F,is,t) =
   if !trace_unify_fail
   then let val f = Syntax.string_of_vname F
            val xs = bnames binders is
-           val u = string_of_term env binders t
+           val u = string_of_term sg env binders t
            val ys = bnames binders (loose_bnos t \\ is)
        in tracing("Cannot unify variable " ^ f ^
                " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
@@ -88,10 +85,10 @@
        end
   else ()
 
-fun ocheck_fail(F,t,binders,env) =
+fun ocheck_fail sg (F,t,binders,env) =
   if !trace_unify_fail
   then let val f = Syntax.string_of_vname F
-           val u = string_of_term env binders t
+           val u = string_of_term sg env binders t
        in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
                   "\nCannot unify!\n")
        end
@@ -229,31 +226,29 @@
                  end;
   in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
-val tsgr = ref(Type.empty_tsig);
-
-fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
+fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
-  else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
+  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (U, T)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
-       handle Type.TUNIFY => (typ_clash(iTs,T,U); raise Unif);
+       handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif);
 
-fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
+fun unif sg binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
          let val name = if ns = "" then nt else ns
-         in unif ((name,Ts)::binders) (env,(ts,tt)) end
-    | (Abs(ns,Ts,ts),t) => unif ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
-    | (t,Abs(nt,Tt,tt)) => unif ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
-    | p => cases(binders,env,p)
+         in unif sg ((name,Ts)::binders) (env,(ts,tt)) end
+    | (Abs(ns,Ts,ts),t) => unif sg ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
+    | (t,Abs(nt,Tt,tt)) => unif sg ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
+    | p => cases sg (binders,env,p)
 
-and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
+and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
        ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
          if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
                   else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
-      | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of' env ss,t)
-      | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of' env ts,s)
-      | ((Const c,ss),(Const d,ts))   => rigidrigid(env,binders,c,d,ss,ts)
-      | ((Free(f),ss),(Free(g),ts))   => rigidrigid(env,binders,f,g,ss,ts)
-      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
+      | ((Var(F,_),ss),_)             => flexrigid sg (env,binders,F,ints_of' env ss,t)
+      | (_,(Var(F,_),ts))             => flexrigid sg (env,binders,F,ints_of' env ts,s)
+      | ((Const c,ss),(Const d,ts))   => rigidrigid sg (env,binders,c,d,ss,ts)
+      | ((Free(f),ss),(Free(g),ts))   => rigidrigid sg (env,binders,f,g,ss,ts)
+      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern
       | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
@@ -264,22 +259,21 @@
       | ((Bound i,_),(Free(f,_),_))    => (clashB binders i f; raise Unif)
 
 
-and rigidrigid (env,binders,(a,Ta),(b,Tb),ss,ts) =
+and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) =
       if a<>b then (clash a b; raise Unif)
-      else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts)
+      else foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts)
 
-and rigidrigidB (env,binders,i,j,ss,ts) =
+and rigidrigidB sg (env,binders,i,j,ss,ts) =
      if i <> j then (clashBB binders i j; raise Unif)
-     else foldl (unif binders) (env ,ss~~ts)
+     else foldl (unif sg binders) (env ,ss~~ts)
 
-and flexrigid (params as (env,binders,F,is,t)) =
-      if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif)
+and flexrigid sg (params as (env,binders,F,is,t)) =
+      if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
       else (let val (u,env') = proj(t,env,binders,is)
             in Envir.update((F,mkabs(binders,is,u)),env') end
-            handle Unif => (proj_fail params; raise Unif));
+            handle Unif => (proj_fail sg params; raise Unif));
 
-fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg;
-                         foldl (unif []) (env,tus));
+fun unify(sg,env,tus) = foldl (unif sg []) (env,tus);
 
 
 (*Eta-contract a term (fully)*)