src/Pure/unify.ML
changeset 16425 2427be27cc60
parent 15797 a63605582573
child 16602 0eda2f8a74aa
     1.1 --- a/src/Pure/unify.ML	Fri Jun 17 18:33:05 2005 +0200
     1.2 +++ b/src/Pure/unify.ML	Fri Jun 17 18:33:08 2005 +0200
     1.3 @@ -1,33 +1,31 @@
     1.4  (*  Title:      Pure/unify.ML
     1.5      ID:         $Id$
     1.6 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   Cambridge University 1992
     1.9  
    1.10 -Higher-Order Unification
    1.11 +Higher-Order Unification.
    1.12  
    1.13 -Types as well as terms are unified.  The outermost functions assume the
    1.14 -terms to be unified already have the same type.  In resolution, this is
    1.15 -assured because both have type "prop".
    1.16 +Types as well as terms are unified.  The outermost functions assume
    1.17 +the terms to be unified already have the same type.  In resolution,
    1.18 +this is assured because both have type "prop".
    1.19  *)
    1.20  
    1.21 -
    1.22 -signature UNIFY = 
    1.23 -  sig
    1.24 +signature UNIFY =
    1.25 +sig
    1.26    (*references for control and tracing*)
    1.27    val trace_bound: int ref
    1.28    val trace_simp: bool ref
    1.29    val trace_types: bool ref
    1.30    val search_bound: int ref
    1.31    (*other exports*)
    1.32 -  val combound : (term*int*int) -> term
    1.33 -  val rlist_abs: (string*typ)list * term -> term   
    1.34 -  val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    1.35 -	-> (Envir.env Seq.seq)
    1.36 -  val unifiers: Sign.sg * Envir.env * ((term*term)list)
    1.37 -	-> (Envir.env * (term * term)list) Seq.seq
    1.38 -  end;
    1.39 +  val combound: term * int * int -> term
    1.40 +  val rlist_abs: (string * typ) list * term -> term
    1.41 +  val smash_unifiers: theory * Envir.env * (term * term) list -> Envir.env Seq.seq
    1.42 +  val unifiers: theory * Envir.env * ((term * term) list) ->
    1.43 +    (Envir.env * (term * term) list) Seq.seq
    1.44 +end
    1.45  
    1.46 -structure Unify	: UNIFY = 
    1.47 +structure Unify	: UNIFY =
    1.48  struct
    1.49  
    1.50  (*Unification options*)
    1.51 @@ -38,7 +36,8 @@
    1.52  and trace_types = ref false	(*announce potential incompleteness
    1.53  				  of type unification*)
    1.54  
    1.55 -val sgr = ref(Sign.pre_pure);
    1.56 +val thy_ref = ref (NONE: theory option);
    1.57 +fun thy () = the (! thy_ref);
    1.58  
    1.59  type binderlist = (string*typ) list;
    1.60  
    1.61 @@ -180,12 +179,12 @@
    1.62  
    1.63  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.64    if T=U then env
    1.65 -  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (U, T)
    1.66 +  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T)
    1.67         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.68         handle Type.TUNIFY => raise CANTUNIFY;
    1.69  
    1.70  fun test_unify_types(args as (T,U,_)) =
    1.71 -let val sot = Sign.string_of_typ (!sgr);
    1.72 +let val sot = Sign.string_of_typ (thy ());
    1.73      fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
    1.74      val env' = unify_types(args)
    1.75  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    1.76 @@ -556,7 +555,7 @@
    1.77      t is always flexible.*)
    1.78  fun print_dpairs msg (env,dpairs) =
    1.79    let fun pdp (rbinder,t,u) =
    1.80 -        let fun termT t = Sign.pretty_term (!sgr)
    1.81 +        let fun termT t = Sign.pretty_term (thy ())
    1.82                                (Envir.norm_term env (rlist_abs(rbinder,t)))
    1.83              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
    1.84                            termT t];
    1.85 @@ -567,7 +566,7 @@
    1.86  (*Unify the dpairs in the environment.
    1.87    Returns flex-flex disagreement pairs NOT IN normal form. 
    1.88    SIMPL may raise exception CANTUNIFY. *)
    1.89 -fun hounifiers (sg,env, tus : (term*term)list) 
    1.90 +fun hounifiers (thy,env, tus : (term*term)list) 
    1.91    : (Envir.env * (term*term)list)Seq.seq =
    1.92    let fun add_unify tdepth ((env,dpairs), reseq) =
    1.93  	  Seq.make (fn()=>
    1.94 @@ -591,14 +590,13 @@
    1.95  	    (if tdepth > !trace_bound then tracing"Failure node" else ();
    1.96  	     Seq.pull reseq));
    1.97       val dps = map (fn(t,u)=> ([],t,u)) tus
    1.98 -  in sgr := sg;
    1.99 -     add_unify 1 ((env,dps), Seq.empty) 
   1.100 -  end;
   1.101 +     val _ = thy_ref := SOME thy;
   1.102 +  in add_unify 1 ((env, dps), Seq.empty) end;
   1.103  
   1.104 -fun unifiers(params) =
   1.105 -      Seq.cons((Pattern.unify(params), []),   Seq.empty)
   1.106 -      handle Pattern.Unif => Seq.empty
   1.107 -           | Pattern.Pattern => hounifiers(params);
   1.108 +fun unifiers params =
   1.109 +  Seq.cons ((Pattern.unify params, []), Seq.empty)
   1.110 +    handle Pattern.Unif => Seq.empty
   1.111 +         | Pattern.Pattern => hounifiers params;
   1.112  
   1.113  
   1.114  (*For smash_flexflex1*)
   1.115 @@ -630,7 +628,7 @@
   1.116    foldr smash_flexflex1 env tpairs;
   1.117  
   1.118  (*Returns unifiers with no remaining disagreement pairs*)
   1.119 -fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
   1.120 -    Seq.map smash_flexflex (unifiers(sg,env,tus));
   1.121 +fun smash_unifiers (thy, env, tus) : Envir.env Seq.seq =
   1.122 +    Seq.map smash_flexflex (unifiers(thy,env,tus));
   1.123  
   1.124  end;