added matches_seq (left-to-right matching, intermediate beta-normalization);
authorwenzelm
Mon Jun 05 21:54:22 2006 +0200 (2006-06-05)
changeset 19776a8c02d8b8b40
parent 19775 06cb6743adf6
child 19777 77929c3d2b74
added matches_seq (left-to-right matching, intermediate beta-normalization);
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Mon Jun 05 21:54:21 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Mon Jun 05 21:54:22 2006 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    val first_order_match: theory -> term * term
     1.5      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
     1.6    val matches: theory -> term * term -> bool
     1.7 -  val matches_list: theory -> (term * term) list -> bool
     1.8 +  val matches_seq: theory -> term list -> term list -> bool
     1.9    val matches_subterm: theory -> term * term -> bool
    1.10    val unify: theory -> term * term -> Envir.env -> Envir.env
    1.11    val first_order: term -> bool
    1.12 @@ -404,11 +404,15 @@
    1.13    val envir' = apfst (typ_match thy (pT, oT)) envir;
    1.14  in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
    1.15  
    1.16 -(*Predicate: does the pattern match the object?*)
    1.17  fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    1.18  
    1.19 -fun matches_list thy pos =
    1.20 -  (fold (match thy) pos (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    1.21 +fun matches_seq thy ps os =
    1.22 +  let
    1.23 +    fun mtch (pat :: pats) (obj :: objs) env =
    1.24 +          mtch pats objs (match thy (pairself Envir.beta_norm (Envir.subst_vars env pat, obj)) env)
    1.25 +      | mtch [] [] env = env
    1.26 +      | mtch _ _ _ = raise MATCH;
    1.27 +  in (mtch ps os (Vartab.empty, Vartab.empty); true) handle MATCH => false end;
    1.28  
    1.29  
    1.30  (* Does pat match a subterm of obj? *)