Added support for referring to subterms of the goal by pattern.

Tactics set/remember and destruct/induction take benefit of it.

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

2 files changed, 88 insertions, 51 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9e8d22a877..452b395ddb 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -661,6 +661,11 @@ let replace_term = replace_term_gen eq_constr
    occurrence except the ones in l and b=false, means all occurrences
    except the ones in l *)
 
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
 type occurrences = bool * int list
 let all_occurrences = (false,[])
 let no_occurrences_in_set = (true,[])
@@ -671,17 +676,24 @@ let error_invalid_occurrence l =
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
      prlist_with_sep spc int l ++ str ".")
 
-let error_cannot_unify_occurrences pos (nowhere_except_in,locs) =
-(*
-  let l = List.filter ((>) !pos) locs in
-  let l =
-    if nowhere_except_in then list_subtract (interval 1 (!pos-1)) l else l in
-  errorlabstrm "" (str "Cannot unify occurrence at position " ++ int pos ++
-    plural n " with occurrence" ++ plural n " at position" ++
-    spc() ++ pr_enum l ++ str".")
-*)
-  errorlabstrm "" (str "Cannot unify occurrence at position " ++ int pos ++
-    strbrk " in a way compatible with the other unifications found for the given term.")
+let pr_position (cl,pos) =
+  let clpos = match cl with
+    | None -> str " of the goal"
+    | Some (id,InHyp) -> str " of hypothesis " ++ pr_id id
+    | Some (id,InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
+    | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
+  int pos ++ clpos
+
+let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_except_in,locs) =
+  let s = if nested then "Found nested occurrences of the pattern"
+    else "Found incompatible occurrences of the pattern" in
+  errorlabstrm ""
+    (str s ++ str ":" ++
+     spc () ++ str "Matched term " ++ quote (print_constr t2) ++
+     strbrk " at position " ++ pr_position (cl2,pos2) ++ 
+     strbrk " is not compatible with matched term " ++
+     quote (print_constr t1) ++ strbrk " at position " ++ 
+     pr_position (cl1,pos1) ++ str ".")
 
 let is_selected pos (nowhere_except_in,locs) =
   nowhere_except_in && List.mem pos locs ||
@@ -689,25 +701,43 @@ let is_selected pos (nowhere_except_in,locs) =
 
 exception NotUnifiable
 
-let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) 
-    match_fun merge_fun substs occ t =
+type 'a testing_function = {
+  match_fun : constr -> 'a;
+  merge_fun : 'a -> 'a -> 'a;
+  mutable testing_state : 'a;
+  mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+}
+
+let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl occ t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
-  let substs = ref substs in
-  let add_subst subst =
-    try substs := merge_fun subst !substs
-    with NotUnifiable -> error_cannot_unify_occurrences !pos plocs in
+  let nested = ref false in
+  let add_subst t subst =
+    try
+      test.testing_state <- test.merge_fun subst test.testing_state;
+      test.last_found <- Some (cl,!pos,t)
+    with NotUnifiable ->
+      let lastpos = Option.get test.last_found in
+      error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos plocs in
   let rec substrec k t =
     if nowhere_except_in & !pos > maxocc then t else
     try
-      let subst = match_fun t in
-      let r = if is_selected !pos plocs then (add_subst subst; mkRel k) else t
-      in incr pos; r
-    with _ ->
-      map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+      let subst = test.match_fun t in
+      if is_selected !pos plocs then
+        (add_subst t subst; incr pos;
+         (* Check nested matching subterms *)
+         nested := true; ignore (subst_below k t); nested := false;
+         (* Do the effective substitution *)
+         mkRel k)
+      else
+        (incr pos; subst_below k t)
+    with NotUnifiable ->
+      subst_below k t
+  and subst_below k t =
+    map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
   in
   let t' = substrec 1 t in
-  (!substs,!pos, t')
+  (!pos, t')
 
 let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] 
 
@@ -724,22 +754,26 @@ let proceed_with_occurrences f plocs x =
     x
   end
 
+let make_eq_test c = {
+  match_fun = (fun c' -> if eq_constr c c' then () else raise NotUnifiable);
+  merge_fun = (fun () () -> ());
+  testing_state = ();
+  last_found = None
+} 
+
 let subst_closed_term_occ_gen plocs pos c t =
-  let (_,pos,t) = subst_closed_term_occ_gen_modulo plocs 
-    (fun c' -> if eq_constr c c' then () else raise Exit)
-    (fun () () -> ()) () pos t in
-  (pos,t)
+  subst_closed_term_occ_gen_modulo plocs (make_eq_test c) None pos t
 
 let subst_closed_term_occ plocs c t =
   proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c)
     plocs t
 
-type hyp_location_flag = (* To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
+let subst_closed_term_occ_modulo plocs test cl t =
+  proceed_with_occurrences
+    (subst_closed_term_occ_gen_modulo plocs test cl) plocs t
 
 let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
+  let f = f (Some (id,hyploc)) in
   match bodyopt,hyploc with
   | None, InHypValueOnly ->
       errorlabstrm "" (pr_id id ++ str " has no value.")
@@ -755,19 +789,13 @@ let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
 let subst_closed_term_occ_decl (plocs,hyploc) c d =
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d
+       (fun _ occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d
 
-let subst_closed_term_occ_decl_modulo (plocs,hyploc)
-    match_fun merge_fun substs d =
-  let subst = ref substs in
+let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d =
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-        (fun occ t ->
-          let (substs,occ,t) =
-            subst_closed_term_occ_gen_modulo plocs
-              match_fun merge_fun !subst occ t
-          in subst := substs; (occ,t))
-        hyploc)
+       (subst_closed_term_occ_gen_modulo plocs test)
+       hyploc)
     plocs d
 
 let vars_of_env env =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 2e202bf073..2028e5acac 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -153,17 +153,31 @@ val no_occurrences_in_set : occurrences
 val subst_closed_term_occ_gen :
   occurrences -> int -> constr -> types -> int * types
 
-(** [subst_closed_term_occ_gen_modulo] looks for subterm modulo a
+(** [subst_closed_term_occ_modulo] looks for subterm modulo a
     testing function returning a substitution of type ['a] (or failing
     with NotUnifiable); a function for merging substitution (possibly
     failing with NotUnifiable) and an initial substitution are
     required too *)
 
+type hyp_location_flag = (** To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
+type 'a testing_function = {
+  match_fun : constr -> 'a;
+  merge_fun : 'a -> 'a -> 'a;
+  mutable testing_state : 'a;
+  mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+}
+
+val make_eq_test : constr -> unit testing_function
+
 exception NotUnifiable
 
-val subst_closed_term_occ_gen_modulo :
-  occurrences -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
-  int -> constr -> 'a * int * types
+val subst_closed_term_occ_modulo :
+  occurrences -> 'a testing_function -> (identifier * hyp_location_flag) option
+  -> constr -> types
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at
    positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
@@ -172,17 +186,12 @@ val subst_closed_term_occ : occurrences -> constr -> constr -> constr
 (** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c]
    at positions [occl] by [Rel 1] in [decl] *)
 
-type hyp_location_flag = (** To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
-
 val subst_closed_term_occ_decl :
   occurrences * hyp_location_flag -> constr -> named_declaration ->
       named_declaration
 
 val subst_closed_term_occ_decl_modulo :
-  occurrences * hyp_location_flag -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a ->
+  occurrences * hyp_location_flag -> 'a testing_function ->
   named_declaration -> named_declaration
 
 val error_invalid_occurrence : int list -> 'a