adapted tsig interface;
authorwenzelm
Fri May 21 21:24:22 2004 +0200 (2004-05-21)
changeset 14787724ce6e574e3
parent 14786 24a7bc97a27a
child 14788 9776f0c747c8
adapted tsig interface;
src/Pure/pattern.ML
src/Pure/proofterm.ML
     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))
     2.1 --- a/src/Pure/proofterm.ML	Fri May 21 21:23:37 2004 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Fri May 21 21:24:22 2004 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4    val add_prf_rrules : (proof * proof) list -> theory -> theory
     2.5    val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
     2.6      theory -> theory
     2.7 -  val rewrite_proof : Type.type_sig -> (proof * proof) list *
     2.8 +  val rewrite_proof : Type.tsig -> (proof * proof) list *
     2.9      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    2.10    val rewrite_proof_notypes : (proof * proof) list *
    2.11      (string * (typ list -> proof -> proof option)) list -> proof -> proof