avoid implicit arguments via refs;
authorwenzelm
Sat Jun 05 13:07:49 2004 +0200 (2004-06-05)
changeset 14875c48d086264c4
parent 14874 23c73484312f
child 14876 477c414000f8
avoid implicit arguments via refs;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Sat Jun 05 13:07:31 2004 +0200
     1.2 +++ b/src/Pure/pattern.ML	Sat Jun 05 13:07:49 2004 +0200
     1.3 @@ -46,19 +46,16 @@
     1.4  
     1.5  val trace_unify_fail = ref false;
     1.6  
     1.7 -(* Only for communication between unification and error message printing *)
     1.8 -val sgr = ref Sign.pre_pure
     1.9 -
    1.10 -fun string_of_term env binders t = Sign.string_of_term (!sgr)
    1.11 +fun string_of_term sg env binders t = Sign.string_of_term sg
    1.12    (Envir.norm_term env (subst_bounds(map Free binders,t)));
    1.13  
    1.14  fun bname binders i = fst(nth_elem(i,binders));
    1.15  fun bnames binders is = space_implode " " (map (bname binders) is);
    1.16  
    1.17 -fun typ_clash(tye,T,U) =
    1.18 +fun typ_clash sg (tye,T,U) =
    1.19    if !trace_unify_fail
    1.20 -  then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T)
    1.21 -           and u = Sign.string_of_typ (!sgr) (Envir.norm_type tye U)
    1.22 +  then let val t = Sign.string_of_typ sg (Envir.norm_type tye T)
    1.23 +           and u = Sign.string_of_typ sg (Envir.norm_type tye U)
    1.24         in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
    1.25    else ()
    1.26  
    1.27 @@ -76,11 +73,11 @@
    1.28    if !trace_unify_fail then clash (boundVar binders i) s
    1.29    else ()
    1.30  
    1.31 -fun proj_fail(env,binders,F,is,t) =
    1.32 +fun proj_fail sg (env,binders,F,is,t) =
    1.33    if !trace_unify_fail
    1.34    then let val f = Syntax.string_of_vname F
    1.35             val xs = bnames binders is
    1.36 -           val u = string_of_term env binders t
    1.37 +           val u = string_of_term sg env binders t
    1.38             val ys = bnames binders (loose_bnos t \\ is)
    1.39         in tracing("Cannot unify variable " ^ f ^
    1.40                 " (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^
    1.41 @@ -88,10 +85,10 @@
    1.42         end
    1.43    else ()
    1.44  
    1.45 -fun ocheck_fail(F,t,binders,env) =
    1.46 +fun ocheck_fail sg (F,t,binders,env) =
    1.47    if !trace_unify_fail
    1.48    then let val f = Syntax.string_of_vname F
    1.49 -           val u = string_of_term env binders t
    1.50 +           val u = string_of_term sg env binders t
    1.51         in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
    1.52                    "\nCannot unify!\n")
    1.53         end
    1.54 @@ -229,31 +226,29 @@
    1.55                   end;
    1.56    in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    1.57  
    1.58 -val tsgr = ref(Type.empty_tsig);
    1.59 -
    1.60 -fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.61 +fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.62    if T=U then env
    1.63 -  else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
    1.64 +  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (U, T)
    1.65         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.66 -       handle Type.TUNIFY => (typ_clash(iTs,T,U); raise Unif);
    1.67 +       handle Type.TUNIFY => (typ_clash sg (iTs,T,U); raise Unif);
    1.68  
    1.69 -fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.70 +fun unif sg binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.71        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
    1.72           let val name = if ns = "" then nt else ns
    1.73 -         in unif ((name,Ts)::binders) (env,(ts,tt)) end
    1.74 -    | (Abs(ns,Ts,ts),t) => unif ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
    1.75 -    | (t,Abs(nt,Tt,tt)) => unif ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
    1.76 -    | p => cases(binders,env,p)
    1.77 +         in unif sg ((name,Ts)::binders) (env,(ts,tt)) end
    1.78 +    | (Abs(ns,Ts,ts),t) => unif sg ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
    1.79 +    | (t,Abs(nt,Tt,tt)) => unif sg ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
    1.80 +    | p => cases sg (binders,env,p)
    1.81  
    1.82 -and cases(binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
    1.83 +and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
    1.84         ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
    1.85           if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
    1.86                    else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
    1.87 -      | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of' env ss,t)
    1.88 -      | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of' env ts,s)
    1.89 -      | ((Const c,ss),(Const d,ts))   => rigidrigid(env,binders,c,d,ss,ts)
    1.90 -      | ((Free(f),ss),(Free(g),ts))   => rigidrigid(env,binders,f,g,ss,ts)
    1.91 -      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts)
    1.92 +      | ((Var(F,_),ss),_)             => flexrigid sg (env,binders,F,ints_of' env ss,t)
    1.93 +      | (_,(Var(F,_),ts))             => flexrigid sg (env,binders,F,ints_of' env ts,s)
    1.94 +      | ((Const c,ss),(Const d,ts))   => rigidrigid sg (env,binders,c,d,ss,ts)
    1.95 +      | ((Free(f),ss),(Free(g),ts))   => rigidrigid sg (env,binders,f,g,ss,ts)
    1.96 +      | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
    1.97        | ((Abs(_),_),_)                => raise Pattern
    1.98        | (_,(Abs(_),_))                => raise Pattern
    1.99        | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
   1.100 @@ -264,22 +259,21 @@
   1.101        | ((Bound i,_),(Free(f,_),_))    => (clashB binders i f; raise Unif)
   1.102  
   1.103  
   1.104 -and rigidrigid (env,binders,(a,Ta),(b,Tb),ss,ts) =
   1.105 +and rigidrigid sg (env,binders,(a,Ta),(b,Tb),ss,ts) =
   1.106        if a<>b then (clash a b; raise Unif)
   1.107 -      else foldl (unif binders) (unify_types(Ta,Tb,env), ss~~ts)
   1.108 +      else foldl (unif sg binders) (unify_types sg (Ta,Tb,env), ss~~ts)
   1.109  
   1.110 -and rigidrigidB (env,binders,i,j,ss,ts) =
   1.111 +and rigidrigidB sg (env,binders,i,j,ss,ts) =
   1.112       if i <> j then (clashBB binders i j; raise Unif)
   1.113 -     else foldl (unif binders) (env ,ss~~ts)
   1.114 +     else foldl (unif sg binders) (env ,ss~~ts)
   1.115  
   1.116 -and flexrigid (params as (env,binders,F,is,t)) =
   1.117 -      if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif)
   1.118 +and flexrigid sg (params as (env,binders,F,is,t)) =
   1.119 +      if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
   1.120        else (let val (u,env') = proj(t,env,binders,is)
   1.121              in Envir.update((F,mkabs(binders,is,u)),env') end
   1.122 -            handle Unif => (proj_fail params; raise Unif));
   1.123 +            handle Unif => (proj_fail sg params; raise Unif));
   1.124  
   1.125 -fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg;
   1.126 -                         foldl (unif []) (env,tus));
   1.127 +fun unify(sg,env,tus) = foldl (unif sg []) (env,tus);
   1.128  
   1.129  
   1.130  (*Eta-contract a term (fully)*)