src/Pure/pattern.ML
changeset 14787 724ce6e574e3
parent 14643 130076a81b84
child 14861 ca5cae7fb65a
     1.1 --- a/src/Pure/pattern.ML	Fri May 21 21:23:37 2004 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri May 21 21:24:22 2004 +0200
     1.3 @@ -15,39 +15,32 @@
     1.4  infix aeconv;
     1.5  
     1.6  signature PATTERN =
     1.7 -  sig
     1.8 -  type type_sig
     1.9 -  type sg
    1.10 -  type env
    1.11 +sig
    1.12    val trace_unify_fail  : bool ref
    1.13    val aeconv            : term * term -> bool
    1.14    val eta_contract      : term -> term
    1.15    val eta_long          : typ list -> term -> term
    1.16    val beta_eta_contract : term -> term
    1.17    val eta_contract_atom : term -> term
    1.18 -  val match             : type_sig -> term * term
    1.19 +  val match             : Type.tsig -> term * term
    1.20                            -> (indexname*typ)list * (indexname*term)list
    1.21 -  val first_order_match : type_sig -> term * term
    1.22 +  val first_order_match : Type.tsig -> term * term
    1.23                            -> (indexname*typ)list * (indexname*term)list
    1.24 -  val matches           : type_sig -> term * term -> bool
    1.25 -  val matches_subterm   : type_sig -> term * term -> bool
    1.26 -  val unify             : sg * env * (term * term)list -> env
    1.27 +  val matches           : Type.tsig -> term * term -> bool
    1.28 +  val matches_subterm   : Type.tsig -> term * term -> bool
    1.29 +  val unify             : Sign.sg * Envir.env * (term * term)list -> Envir.env
    1.30    val first_order       : term -> bool
    1.31    val pattern           : term -> bool
    1.32 -  val rewrite_term      : type_sig -> (term * term) list -> (term -> term option) list
    1.33 +  val rewrite_term      : Type.tsig -> (term * term) list -> (term -> term option) list
    1.34                            -> term -> term
    1.35    exception Unif
    1.36    exception MATCH
    1.37    exception Pattern
    1.38 -  end;
    1.39 +end;
    1.40  
    1.41  structure Pattern : PATTERN =
    1.42  struct
    1.43  
    1.44 -type type_sig = Type.type_sig
    1.45 -type sg = Sign.sg
    1.46 -type env = Envir.env
    1.47 -
    1.48  exception Unif;
    1.49  exception Pattern;
    1.50  
    1.51 @@ -238,7 +231,7 @@
    1.52                   end;
    1.53    in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    1.54  
    1.55 -val tsgr = ref(Type.tsig0);
    1.56 +val tsgr = ref(Type.empty_tsig);
    1.57  
    1.58  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.59    if T=U then env
    1.60 @@ -296,16 +289,16 @@
    1.61  fun eta_contract t =
    1.62    let
    1.63      exception SAME;
    1.64 -    fun eta (Abs (a, T, body)) = 
    1.65 +    fun eta (Abs (a, T, body)) =
    1.66        ((case eta body of
    1.67 -          body' as (f $ Bound 0) => 
    1.68 -	    if loose_bvar1 (f, 0) then Abs(a, T, body')
    1.69 -	    else incr_boundvars ~1 f
    1.70 +          body' as (f $ Bound 0) =>
    1.71 +            if loose_bvar1 (f, 0) then Abs(a, T, body')
    1.72 +            else incr_boundvars ~1 f
    1.73          | body' => Abs (a, T, body')) handle SAME =>
    1.74         (case body of
    1.75 -          (f $ Bound 0) => 
    1.76 -	    if loose_bvar1 (f, 0) then raise SAME
    1.77 -	    else incr_boundvars ~1 f
    1.78 +          (f $ Bound 0) =>
    1.79 +            if loose_bvar1 (f, 0) then raise SAME
    1.80 +            else incr_boundvars ~1 f
    1.81          | _ => raise SAME))
    1.82        | eta (f $ t) =
    1.83            (let val f' = eta f
    1.84 @@ -333,7 +326,7 @@
    1.85  fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
    1.86    | eta_long Ts t = (case strip_comb t of
    1.87        (Abs _, _) => eta_long Ts (Envir.beta_norm t)
    1.88 -    | (u, ts) => 
    1.89 +    | (u, ts) =>
    1.90        let
    1.91          val Us = binder_types (fastype_of1 (Ts, t));
    1.92          val i = length Us
    1.93 @@ -524,7 +517,7 @@
    1.94              Abs (_, _, body) =>
    1.95                let val tm' = subst_bound (tm2, body)
    1.96                in Some (if_none (rew2 skel0 tm') tm') end
    1.97 -          | _ => 
    1.98 +          | _ =>
    1.99              let val (skel1, skel2) = (case skel of
   1.100                  skel1 $ skel2 => (skel1, skel2)
   1.101                | _ => (skel0, skel0))