From fffd3e2ad413f00b41f17c3f79edac63ec145760 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 31 Jan 2003 22:20:28 +0000 Subject: Ajout d'un filtrage d'application partielle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3642 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pattern.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'pretyping') diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 0afcbdde7..c921205d1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -238,6 +238,21 @@ let matches_core convert pat c = | PSort (RType _), Sort (Type _) -> sigma + | PApp (PMeta (Some n),args1), App (c2,args2) -> + let p = Array.length args2 - Array.length args1 in + if p>=0 then + let args21, args22 = array_chop p args2 in + let sigma = + let depth = List.length stk in + let c = mkApp(c2,args21) in + let frels = Intset.elements (free_rels c) in + if List.for_all (fun i -> i > depth) frels then + constrain (n,lift (-depth) c) sigma + else + raise PatternMatchingFailure in + array_fold_left2 (sorec stk) sigma args1 args22 + else raise PatternMatchingFailure + | PApp (c1,arg1), App (c2,arg2) -> (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) -- cgit v1.2.3