src/Pure/pattern.ML
changeset 4820 8f6dbbd8d497
parent 4667 6328d427a339
child 6539 2e7d2fba9f6c
     1.1 --- a/src/Pure/pattern.ML	Tue Apr 21 17:25:19 1998 +0200
     1.2 +++ b/src/Pure/pattern.ML	Wed Apr 22 14:04:35 1998 +0200
     1.3 @@ -24,9 +24,13 @@
     1.4    val eta_contract_atom : term -> term
     1.5    val match             : type_sig -> term * term
     1.6                            -> (indexname*typ)list * (indexname*term)list
     1.7 +  val first_order_match : type_sig -> term * term
     1.8 +                          -> (indexname*typ)list * (indexname*term)list
     1.9    val matches           : type_sig -> term * term -> bool
    1.10    val matches_subterm   : type_sig -> term * term -> bool
    1.11    val unify             : sg * env * (term * term)list -> env
    1.12 +  val first_order       : term -> bool
    1.13 +  val pattern           : term -> bool
    1.14    exception Unif
    1.15    exception MATCH
    1.16    exception Pattern
    1.17 @@ -279,48 +283,6 @@
    1.18    | eta_contract2 t     = eta_contract_atom t;
    1.19  
    1.20  
    1.21 -(* Pattern matching *)
    1.22 -exception MATCH;
    1.23 -
    1.24 -(*First-order matching;  term_match tsig (pattern, object)
    1.25 -    returns a (tyvar,typ)list and (var,term)list.
    1.26 -  The pattern and object may have variables in common.
    1.27 -  Instantiation does not affect the object, so matching ?a with ?a+1 works.
    1.28 -  A Const does not match a Free of the same name! *)
    1.29 -fun fomatch tsig (pat,obj) =
    1.30 -  let fun typ_match args = (Type.typ_match tsig args)
    1.31 -			   handle Type.TYPE_MATCH => raise MATCH;
    1.32 -      fun mtch (tyinsts,insts) = fn
    1.33 -	(Var(ixn,T), t)  =>
    1.34 -	  if loose_bvar(t,0) then raise MATCH
    1.35 -	  else (case assoc_string_int(insts,ixn) of
    1.36 -		  None => (typ_match (tyinsts, (T, fastype_of t)), 
    1.37 -			   (ixn,t)::insts)
    1.38 -		| Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
    1.39 -      | (Free (a,T), Free (b,U)) =>
    1.40 -	  if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    1.41 -      | (Const (a,T), Const (b,U))  =>
    1.42 -	  if  a=b  then (typ_match (tyinsts,(T,U)), insts)  else raise MATCH
    1.43 -      | (Bound i, Bound j)  =>
    1.44 -          if  i=j  then  (tyinsts,insts)  else raise MATCH
    1.45 -      | (Abs(_,T,t), Abs(_,U,u))  =>
    1.46 -	  mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
    1.47 -      | (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u)
    1.48 -      | _ => raise MATCH
    1.49 -  in mtch([],[]) (eta_contract pat, eta_contract obj) end;
    1.50 -
    1.51 -
    1.52 -fun match_bind(itms,binders,ixn,is,t) =
    1.53 -  let val js = loose_bnos t
    1.54 -  in if null is
    1.55 -     then if null js then (ixn,t)::itms else raise MATCH
    1.56 -     else if js subset_int is
    1.57 -          then let val t' = if downto0(is,length binders - 1) then t
    1.58 -                            else mapbnd (idx is) t
    1.59 -               in (ixn, mkabs(binders,is,t')) :: itms end
    1.60 -          else raise MATCH
    1.61 -  end;
    1.62 -
    1.63  (*Tests whether 2 terms are alpha/eta-convertible and have same type.
    1.64    Note that Consts and Vars may have more than one type.*)
    1.65  fun t aeconv u = aconv_aux (eta_contract_atom t, eta_contract_atom u)
    1.66 @@ -333,59 +295,106 @@
    1.67    | aconv_aux _ =  false;
    1.68  
    1.69  
    1.70 +(*** Matching ***)
    1.71 +
    1.72 +exception MATCH;
    1.73 +
    1.74 +fun typ_match tsig args = (Type.typ_match tsig args)
    1.75 +                          handle Type.TYPE_MATCH => raise MATCH;
    1.76 +
    1.77 +(*First-order matching;
    1.78 +  fomatch tsig (pattern, object) returns a (tyvar,typ)list and (var,term)list.
    1.79 +  The pattern and object may have variables in common.
    1.80 +  Instantiation does not affect the object, so matching ?a with ?a+1 works.
    1.81 +  Object is eta-contracted on the fly (by eta-expanding the pattern).
    1.82 +  Precondition: the pattern is already eta-contracted!
    1.83 +  Note: types are matched on the fly *)
    1.84 +fun fomatch tsig =
    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 assoc_string_int(insts,ixn) of
    1.90 +		  None => (typ_match tsig (tyinsts, (T, fastype_of t)), 
    1.91 +			   (ixn,t)::insts)
    1.92 +		| Some u => if t aeconv u then instsp else raise MATCH)
    1.93 +      | (Free (a,T), Free (b,U)) =>
    1.94 +	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
    1.95 +      | (Const (a,T), Const (b,U))  =>
    1.96 +	  if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
    1.97 +      | (Bound i, Bound j)  =>  if  i=j  then  instsp  else raise MATCH
    1.98 +      | (Abs(_,T,t), Abs(_,U,u))  =>
    1.99 +	  mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
   1.100 +      | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
   1.101 +      | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
   1.102 +      | _ => raise MATCH
   1.103 +  in mtch end;
   1.104 +
   1.105 +fun first_order_match tsig = fomatch tsig ([],[]);
   1.106 + 
   1.107 +(* Matching of higher-order patterns *)
   1.108 +
   1.109 +fun match_bind(itms,binders,ixn,is,t) =
   1.110 +  let val js = loose_bnos t
   1.111 +  in if null is
   1.112 +     then if null js then (ixn,t)::itms else raise MATCH
   1.113 +     else if js subset_int is
   1.114 +          then let val t' = if downto0(is,length binders - 1) then t
   1.115 +                            else mapbnd (idx is) t
   1.116 +               in (ixn, mkabs(binders,is,t')) :: itms end
   1.117 +          else raise MATCH
   1.118 +  end;
   1.119 +
   1.120  fun match tsg (po as (pat,obj)) =
   1.121  let
   1.122 -
   1.123 -fun typ_match args = Type.typ_match tsg args
   1.124 -                     handle Type.TYPE_MATCH => raise MATCH;
   1.125 -
   1.126 -(* Pre: pat and obj have same type *)
   1.127 -fun mtch binders (env as (iTs,itms),(pat,obj)) =
   1.128 -      case pat of
   1.129 -        Abs(ns,Ts,ts) =>
   1.130 -          (case obj of
   1.131 -             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   1.132 -           | _ => let val Tt = typ_subst_TVars iTs Ts
   1.133 -                  in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   1.134 -      | _ => (case obj of
   1.135 -                Abs(nt,Tt,tt) =>
   1.136 -                  mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
   1.137 -              | _ => cases(binders,env,pat,obj))
   1.138 +  (* Pre: pat and obj have same type *)
   1.139 +  fun mtch binders (env as (iTs,itms),(pat,obj)) =
   1.140 +    case pat of
   1.141 +      Abs(ns,Ts,ts) =>
   1.142 +        (case obj of
   1.143 +           Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   1.144 +         | _ => let val Tt = typ_subst_TVars iTs Ts
   1.145 +                in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   1.146 +    | _ => (case obj of
   1.147 +              Abs(nt,Tt,tt) =>
   1.148 +                mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
   1.149 +            | _ => cases(binders,env,pat,obj))
   1.150  
   1.151 -and cases(binders,env as (iTs,itms),pat,obj) =
   1.152 -      let val (ph,pargs) = strip_comb pat
   1.153 -          fun rigrig1(iTs,oargs) =
   1.154 -                foldl (mtch binders) ((iTs,itms), pargs~~oargs)
   1.155 -          fun rigrig2((a,Ta),(b,Tb),oargs) =
   1.156 -                if a<> b then raise MATCH
   1.157 -                else rigrig1(typ_match(iTs,(Ta,Tb)), oargs)
   1.158 -      in case ph of
   1.159 -           Var(ixn,_) =>
   1.160 -             let val is = ints_of pargs
   1.161 -             in case assoc_string_int(itms,ixn) of
   1.162 -                  None => (iTs,match_bind(itms,binders,ixn,is,obj))
   1.163 -                | Some u => if obj aeconv (red u is []) then env
   1.164 -                            else raise MATCH
   1.165 -             end
   1.166 -         | _ =>
   1.167 -             let val (oh,oargs) = strip_comb obj
   1.168 -             in case (ph,oh) of
   1.169 -                  (Const c,Const d) => rigrig2(c,d,oargs)
   1.170 -                | (Free f,Free g)   => rigrig2(f,g,oargs)
   1.171 -                | (Bound i,Bound j) => if i<>j then raise MATCH
   1.172 -                                       else rigrig1(iTs,oargs)
   1.173 -                | (Abs _, _)        => raise Pattern
   1.174 -                | (_, Abs _)        => raise Pattern
   1.175 -                | _                 => raise MATCH
   1.176 -             end
   1.177 -      end;
   1.178 +  and cases(binders,env as (iTs,itms),pat,obj) =
   1.179 +    let val (ph,pargs) = strip_comb pat
   1.180 +        fun rigrig1(iTs,oargs) =
   1.181 +              foldl (mtch binders) ((iTs,itms), pargs~~oargs)
   1.182 +        fun rigrig2((a,Ta),(b,Tb),oargs) =
   1.183 +              if a<> b then raise MATCH
   1.184 +              else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
   1.185 +    in case ph of
   1.186 +         Var(ixn,_) =>
   1.187 +           let val is = ints_of pargs
   1.188 +           in case assoc_string_int(itms,ixn) of
   1.189 +                None => (iTs,match_bind(itms,binders,ixn,is,obj))
   1.190 +              | Some u => if obj aeconv (red u is []) then env
   1.191 +                          else raise MATCH
   1.192 +           end
   1.193 +       | _ =>
   1.194 +           let val (oh,oargs) = strip_comb obj
   1.195 +           in case (ph,oh) of
   1.196 +                (Const c,Const d) => rigrig2(c,d,oargs)
   1.197 +              | (Free f,Free g)   => rigrig2(f,g,oargs)
   1.198 +              | (Bound i,Bound j) => if i<>j then raise MATCH
   1.199 +                                     else rigrig1(iTs,oargs)
   1.200 +              | (Abs _, _)        => raise Pattern
   1.201 +              | (_, Abs _)        => raise Pattern
   1.202 +              | _                 => raise MATCH
   1.203 +           end
   1.204 +    end;
   1.205  
   1.206 -val pT = fastype_of pat
   1.207 -and oT = fastype_of obj
   1.208 -val iTs = typ_match ([],(pT,oT))
   1.209 +  val pT = fastype_of pat
   1.210 +  and oT = fastype_of obj
   1.211 +  val iTs = typ_match tsg ([],(pT,oT))
   1.212 +  val insts2 = (iTs,[])
   1.213  
   1.214 -in mtch [] ((iTs,[]), po)
   1.215 -   handle Pattern => fomatch tsg po
   1.216 +in mtch [] (insts2, po)
   1.217 +   handle Pattern => fomatch tsg insts2 po
   1.218  end;
   1.219  
   1.220  (*Predicate: does the pattern match the object?*)
   1.221 @@ -402,4 +411,17 @@
   1.222              | _ => false
   1.223    in msub([],obj) end;
   1.224  
   1.225 +fun first_order(Abs(_,_,t)) = first_order t
   1.226 +  | first_order(t $ u) = first_order t andalso first_order u andalso
   1.227 +                         not(is_Var t)
   1.228 +  | first_order _ = true;
   1.229 +
   1.230 +fun pattern(Abs(_,_,t)) = pattern t
   1.231 +  | pattern(t) = let val (head,args) = strip_comb t
   1.232 +                 in if is_Var head
   1.233 +                    then let val _ = ints_of args in true end
   1.234 +                         handle Pattern => false
   1.235 +                    else forall pattern args
   1.236 +                 end;
   1.237 +
   1.238  end;