moved combound, rlist_abs to logic.ML;
authorwenzelm
Mon Feb 06 20:59:42 2006 +0100 (2006-02-06)
changeset 189450b15863018a8
parent 18944 7d2ed9063477
child 18946 ce65d2d2e0c2
moved combound, rlist_abs to logic.ML;
src/Pure/unify.ML
     1.1 --- a/src/Pure/unify.ML	Mon Feb 06 20:59:11 2006 +0100
     1.2 +++ b/src/Pure/unify.ML	Mon Feb 06 20:59:42 2006 +0100
     1.3 @@ -18,8 +18,6 @@
     1.4    val trace_types: bool ref
     1.5    val search_bound: int ref
     1.6    (*other exports*)
     1.7 -  val combound: term * int * int -> term
     1.8 -  val rlist_abs: (string * typ) list * term -> term
     1.9    val smash_unifiers: theory * Envir.env * (term * term) list -> Envir.env Seq.seq
    1.10    val unifiers: theory * Envir.env * ((term * term) list) ->
    1.11      (Envir.env * (term * term) list) Seq.seq
    1.12 @@ -198,11 +196,6 @@
    1.13    | get_eta_var _ = raise ASSIGN;
    1.14  
    1.15  
    1.16 -(* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
    1.17 -fun rlist_abs ([], body) = body
    1.18 -  | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
    1.19 -
    1.20 -
    1.21  (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
    1.22    If v occurs rigidly then nonunifiable.
    1.23    If v occurs nonrigidly then must use full algorithm. *)
    1.24 @@ -211,7 +204,7 @@
    1.25      in  case rigid_occurs_term (ref [], env, v, u) of
    1.26  	      NoOcc => let val env = unify_types thy (body_type env T,
    1.27  						 fastype env (rbinder,u),env)
    1.28 -		in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
    1.29 +		in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
    1.30  	    | Nonrigid =>  raise ASSIGN
    1.31  	    | Rigid =>  raise CANTUNIFY
    1.32      end;
    1.33 @@ -295,11 +288,6 @@
    1.34      end;
    1.35  
    1.36  
    1.37 -(*computes t(Bound(n+k-1),...,Bound(n))  *)
    1.38 -fun combound (t, n, k) = 
    1.39 -    if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
    1.40 -
    1.41 -
    1.42  (*Makes the terms E1,...,Em,    where Ts = [T...Tm]. 
    1.43    Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
    1.44    The B.j are bound vars of binder.
    1.45 @@ -309,7 +297,7 @@
    1.46    | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
    1.47         let fun funtype T = binder--->T;
    1.48  	   val (env', vars) = Envir.genvars name (env, map funtype Ts)
    1.49 -       in  (env',  map (fn var=> combound(var, 0, length binder)) vars)  end;
    1.50 +       in  (env',  map (fn var=> Logic.combound(var, 0, length binder)) vars)  end;
    1.51  
    1.52  
    1.53  (*Abstraction over a list of types, like list_abs*)
    1.54 @@ -379,7 +367,7 @@
    1.55        | Var (w,uary) => 
    1.56  	    (*a flex-flex dpair: make variable for t*)
    1.57  	    let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
    1.58 -		val tabs = combound(newhd, 0, length Ts)
    1.59 +		val tabs = Logic.combound(newhd, 0, length Ts)
    1.60  		val tsub = list_comb(newhd,targs)
    1.61  	    in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs)) 
    1.62  	    end
    1.63 @@ -414,7 +402,7 @@
    1.64     else let val env = unify_types thy (body_type env T,
    1.65  				  fastype env (rbinder,u),
    1.66  				  env)
    1.67 -	in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
    1.68 +	in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end
    1.69  end;
    1.70  
    1.71  
    1.72 @@ -503,7 +491,7 @@
    1.73  fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
    1.74    if t0 aconv u0 then tpairs  
    1.75    else
    1.76 -  let val t = rlist_abs(rbinder, t0)  and  u = rlist_abs(rbinder, u0);
    1.77 +  let val t = Logic.rlist_abs(rbinder, t0)  and  u = Logic.rlist_abs(rbinder, u0);
    1.78        fun same(t',u') = (t aconv t') andalso (u aconv u')
    1.79    in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
    1.80  
    1.81 @@ -552,7 +540,7 @@
    1.82  fun print_dpairs thy msg (env,dpairs) =
    1.83    let fun pdp (rbinder,t,u) =
    1.84          let fun termT t = Sign.pretty_term thy
    1.85 -                              (Envir.norm_term env (rlist_abs(rbinder,t)))
    1.86 +                              (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
    1.87              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
    1.88                            termT t];
    1.89          in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;