Matching patterns: fixed allow_partial_app which was not working on

unnamed Metas; also added matching an applicative prefix (with
non-meta head) of a term against a pattern, to be used by "Search"
(i.e. SearchHead).

This allows "Search" and "SearchPattern" to behave as in 8.4.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16422 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 52 insertions, 5 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index e25312e41c..5460d8ba1f 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -181,12 +181,15 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
       | PApp (PApp (h, a1), a2), _ ->
           sorec stk subst (PApp(h,Array.append a1 a2)) t
 
-      | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
+      | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
           let p = Array.length args2 - Array.length args1 in
           if p >= 0 then
             let args21, args22 = Array.chop p args2 in
 	    let c = mkApp(c2,args21) in
-            let subst = merge_binding allow_bound_rels stk n c subst in
+            let subst =
+              match meta with
+              | None -> subst
+              | Some n -> merge_binding allow_bound_rels stk n c subst in
             Array.fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
@@ -257,7 +260,7 @@ let matches_core_closed convert allow_partial_app pat c =
 
 let extended_matches = matches_core None true true
 
-let matches c p = snd (matches_core_closed None true c p)
+let matches pat c = snd (matches_core_closed None true pat c)
 
 let special_meta = (-1)
 
@@ -268,6 +271,19 @@ type 'a matching_result =
 
 let mkresult s c n = { m_sub=s; m_ctx=c; m_nxt=n }
 
+let isPMeta = function PMeta _ -> true | _ -> false
+
+let matches_head pat c =
+  let head =
+    match pat, kind_of_term c with
+    | PApp (c1,arg1), App (c2,arg2) ->
+        if isPMeta c1 then c else
+        let n1 = Array.length arg1 in
+        if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c
+    | c1, App (c2,arg2) when not (isPMeta c1) -> c2
+    | _ -> c in
+  matches pat head
+
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ partial_app closed pat c mk_ctx next =
   try
@@ -356,6 +372,10 @@ let is_matching pat c =
   try let _ = matches pat c in true
   with PatternMatchingFailure -> false
 
+let is_matching_head pat c =
+  try let _ = matches_head pat c in true
+  with PatternMatchingFailure -> false
+
 let is_matching_appsubterm ?(closed=true) pat c =
   try let _ = sub_match ~partial_app:true ~closed pat c in true
   with PatternMatchingFailure -> false
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 05e01e2e26..5ba68f26bf 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -33,6 +33,10 @@ type bound_ident_map = (Id.t * Id.t) list
    numbers given in the pattern *)
 val matches : constr_pattern -> constr -> patvar_map
 
+(** [matches_head pat c] does the same as |matches pat c] but accepts
+    [pat] to match an applicative prefix of [c] *)
+val matches_head : constr_pattern -> constr -> patvar_map
+
 (** [extended_matches pat c] also returns the names of bound variables
    in [c] that matches the bound variables in [pat]; if several bound
    variables or metavariables have the same name, the metavariable,
@@ -43,6 +47,10 @@ val extended_matches :
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
 val is_matching : constr_pattern -> constr -> bool
 
+(** [is_matching_head pat c] just tells if [c] or an applicative
+    prefix of it matches against [pat] *)
+val is_matching_head : constr_pattern -> constr -> bool
+
 (** [matches_conv env sigma] matches up to conversion in environment
    [(env,sigma)] when constants in pattern are concerned; it raises
    [PatternMatchingFailure] if not matchable; bindings are given in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 3a8faaa8db..9e61bc7fb7 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -120,6 +120,14 @@ let rec pattern_filter pat ref env typ =
   | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
   | _ -> false
 
+let rec head_filter pat ref env typ =
+  let typ = strip_outer_cast typ in
+  if Matching.is_matching_head pat typ then true
+  else match kind_of_term typ with
+  | Prod (_, _, typ)
+  | LetIn (_, _, _, typ) -> head_filter pat ref env typ
+  | _ -> false
+
 let full_name_of_reference ref =
   let (dir,id) = repr_path (path_of_global ref) in
   DirPath.to_string dir ^ "." ^ Id.to_string id
@@ -195,8 +203,19 @@ let search_rewrite pat mods =
 
 (** Search *)
 
-let search_by_head = search_pattern
-(** Now search_by_head is the same as search_pattern... *)
+let search_by_head pat mods =
+  let ans = ref [] in
+  let filter ref env typ =
+    let f_module = module_filter mods ref env typ in
+    let f_blacklist = blacklist_filter ref env typ in
+    let f_pattern () = head_filter pat ref env typ in
+    f_module && f_pattern () && f_blacklist
+  in
+  let iter ref env typ =
+    if filter ref env typ then plain_display ans ref env typ
+  in
+  let () = generic_search iter in
+  format_display !ans
 
 (** SearchAbout *)