src/Pure/pattern.ML
changeset 18182 786d83044780
parent 18011 685d95c793ff
child 18940 d8e12bf337a3
     1.1 --- a/src/Pure/pattern.ML	Wed Nov 16 17:45:27 2005 +0100
     1.2 +++ b/src/Pure/pattern.ML	Wed Nov 16 17:45:28 2005 +0100
     1.3 @@ -21,11 +21,13 @@
     1.4    val eta_long: typ list -> term -> term
     1.5    val beta_eta_contract: term -> term
     1.6    val eta_contract_atom: term -> term
     1.7 -  val match: theory -> term * term -> Type.tyenv * Envir.tenv
     1.8 -  val first_order_match: theory -> term * term -> Type.tyenv * Envir.tenv
     1.9 +  val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
    1.10 +  val first_order_match: theory -> term * term
    1.11 +    -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
    1.12    val matches: theory -> term * term -> bool
    1.13 +  val matches_list: theory -> (term * term) list -> bool
    1.14    val matches_subterm: theory -> term * term -> bool
    1.15 -  val unify: theory * Envir.env * (term * term)list -> Envir.env
    1.16 +  val unify: theory -> term * term -> Envir.env -> Envir.env
    1.17    val first_order: term -> bool
    1.18    val pattern: term -> bool
    1.19    val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
    1.20 @@ -220,18 +222,18 @@
    1.21                   end;
    1.22    in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    1.23  
    1.24 -fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    1.25 +fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
    1.26    if T=U then env
    1.27    else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
    1.28         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.29         handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
    1.30  
    1.31 -fun unif thy binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.32 +fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.33        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
    1.34           let val name = if ns = "" then nt else ns
    1.35 -         in unif thy ((name,Ts)::binders) (env,(ts,tt)) end
    1.36 -    | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
    1.37 -    | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
    1.38 +         in unif thy ((name,Ts)::binders) (ts,tt) env end
    1.39 +    | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
    1.40 +    | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
    1.41      | p => cases thy (binders,env,p)
    1.42  
    1.43  and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
    1.44 @@ -255,11 +257,11 @@
    1.45  
    1.46  and rigidrigid thy (env,binders,(a,Ta),(b,Tb),ss,ts) =
    1.47        if a<>b then (clash a b; raise Unif)
    1.48 -      else Library.foldl (unif thy binders) (unify_types thy (Ta,Tb,env), ss~~ts)
    1.49 +      else env |> unify_types thy (Ta,Tb) |> fold (unif thy binders) (ss~~ts)
    1.50  
    1.51  and rigidrigidB thy (env,binders,i,j,ss,ts) =
    1.52       if i <> j then (clashBB binders i j; raise Unif)
    1.53 -     else Library.foldl (unif thy binders) (env ,ss~~ts)
    1.54 +     else fold (unif thy binders) (ss~~ts) env
    1.55  
    1.56  and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
    1.57        if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
    1.58 @@ -267,7 +269,7 @@
    1.59              in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
    1.60              handle Unif => (proj_fail thy params; raise Unif));
    1.61  
    1.62 -fun unify(thy,env,tus) = Library.foldl (unif thy []) (env,tus);
    1.63 +fun unify thy = unif thy [];
    1.64  
    1.65  
    1.66  (*Eta-contract a term (fully)*)
    1.67 @@ -338,38 +340,36 @@
    1.68  
    1.69  exception MATCH;
    1.70  
    1.71 -fun typ_match thy (tyenv, TU) = Sign.typ_match thy TU tyenv
    1.72 +fun typ_match thy TU tyenv = Sign.typ_match thy TU tyenv
    1.73    handle Type.TYPE_MATCH => raise MATCH;
    1.74  
    1.75  (*First-order matching;
    1.76 -  fomatch thy (pattern, object) returns a (tyvar,typ)list and (var,term)list.
    1.77    The pattern and object may have variables in common.
    1.78    Instantiation does not affect the object, so matching ?a with ?a+1 works.
    1.79    Object is eta-contracted on the fly (by eta-expanding the pattern).
    1.80    Precondition: the pattern is already eta-contracted!
    1.81 -  Note: types are matched on the fly *)
    1.82 -fun fomatch thy =
    1.83 +  Types are matched on the fly*)
    1.84 +fun first_order_match thy =
    1.85    let
    1.86      fun mtch (instsp as (tyinsts,insts)) = fn
    1.87          (Var(ixn,T), t)  =>
    1.88            if loose_bvar(t,0) then raise MATCH
    1.89            else (case Envir.lookup' (insts, (ixn, T)) of
    1.90 -                  NONE => (typ_match thy (tyinsts, (T, fastype_of t)),
    1.91 +                  NONE => (typ_match thy (T, fastype_of t) tyinsts,
    1.92                             Vartab.update_new (ixn, (T, t)) insts)
    1.93                  | SOME u => if t aeconv u then instsp else raise MATCH)
    1.94        | (Free (a,T), Free (b,U)) =>
    1.95 -          if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
    1.96 +          if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
    1.97        | (Const (a,T), Const (b,U))  =>
    1.98 -          if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
    1.99 +          if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
   1.100        | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
   1.101        | (Abs(_,T,t), Abs(_,U,u))  =>
   1.102 -          mtch (typ_match thy (tyinsts,(T,U)),insts) (t,u)
   1.103 +          mtch (typ_match thy (T,U) tyinsts, insts) (t,u)
   1.104        | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
   1.105        | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
   1.106        | _ => raise MATCH
   1.107 -  in mtch end;
   1.108 +  in fn tu => fn env => mtch env tu end;
   1.109  
   1.110 -fun first_order_match thy = fomatch thy (Vartab.empty, Vartab.empty);
   1.111  
   1.112  (* Matching of higher-order patterns *)
   1.113  
   1.114 @@ -384,28 +384,27 @@
   1.115            else raise MATCH
   1.116    end;
   1.117  
   1.118 -fun match thy (po as (pat,obj)) =
   1.119 +fun match thy (po as (pat,obj)) envir =
   1.120  let
   1.121    (* Pre: pat and obj have same type *)
   1.122 -  fun mtch binders (env as (iTs,itms),(pat,obj)) =
   1.123 +  fun mtch binders (pat,obj) (env as (iTs,itms)) =
   1.124      case pat of
   1.125        Abs(ns,Ts,ts) =>
   1.126          (case obj of
   1.127 -           Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   1.128 +           Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
   1.129           | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
   1.130 -                in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   1.131 +                in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
   1.132      | _ => (case obj of
   1.133                Abs(nt,Tt,tt) =>
   1.134 -                mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
   1.135 +                mtch((nt,Tt)::binders) ((incr pat)$Bound(0),tt) env
   1.136              | _ => cases(binders,env,pat,obj))
   1.137  
   1.138    and cases(binders,env as (iTs,itms),pat,obj) =
   1.139      let val (ph,pargs) = strip_comb pat
   1.140 -        fun rigrig1(iTs,oargs) =
   1.141 -              Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
   1.142 +        fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
   1.143          fun rigrig2((a:string,Ta),(b,Tb),oargs) =
   1.144                if a <> b then raise MATCH
   1.145 -              else rigrig1(typ_match thy (iTs,(Ta,Tb)), oargs)
   1.146 +              else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
   1.147      in case ph of
   1.148           Var(ixn,T) =>
   1.149             let val is = ints_of pargs
   1.150 @@ -429,15 +428,15 @@
   1.151  
   1.152    val pT = fastype_of pat
   1.153    and oT = fastype_of obj
   1.154 -  val iTs = typ_match thy (Vartab.empty, (pT,oT))
   1.155 -  val insts2 = (iTs, Vartab.empty)
   1.156 -
   1.157 -in mtch [] (insts2, po)
   1.158 -   handle Pattern => fomatch thy insts2 po
   1.159 -end;
   1.160 +  val envir' = apfst (typ_match thy (pT, oT)) envir;
   1.161 +in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
   1.162  
   1.163  (*Predicate: does the pattern match the object?*)
   1.164 -fun matches thy po = (match thy po; true) handle MATCH => false;
   1.165 +fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
   1.166 +
   1.167 +fun matches_list thy pos =
   1.168 +  (fold (match thy) pos (Vartab.empty, Vartab.empty); true) handle MATCH => false;
   1.169 +
   1.170  
   1.171  (* Does pat match a subterm of obj? *)
   1.172  fun matches_subterm thy (pat,obj) =
   1.173 @@ -478,7 +477,7 @@
   1.174  
   1.175      fun match_rew tm (tm1, tm2) =
   1.176        let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 in
   1.177 -        SOME (Envir.subst_vars (match thy (tm1, tm)) rtm, rtm)
   1.178 +        SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
   1.179            handle MATCH => NONE
   1.180        end;
   1.181