Fixing #1225: we now skip the canonically built binding contexts of

the return clause and of the branches in a "match", computing them
automatically when using the "at" clause of pattern, destruct, ...

In principle, this is a source of incompatibilities in the numbering,
since the internal binders of a "match" are now skipped. We shall deal
with that later on.

3 files changed, 71 insertions, 28 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 95a6ba79db..c8d90fffea 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -14,6 +14,8 @@ open Locus
 open Term
 open Nameops
 open Termops
+open Environ
+open Inductiveops
 open Pretype_errors
 
 (** Processing occurrences *)
@@ -73,6 +75,17 @@ let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
       let acc,typ = f acc typ in
       acc,(id,Some body,typ)
 
+let rec process_under_binders f envk sign p =
+  let rec aux (env,k) sign p =
+    match (sign,kind_of_term p) with
+    | [], _ -> f (env,k) p
+    | (_,None,t as d)::sign, Lambda (na,_,p) ->
+      mkLambda (na,t,aux (push_rel d env,k+1) sign p)
+    | (_,(Some c),t as d)::sign, LetIn (na,_,_,p) ->
+      mkLetIn (na,c,t,aux (push_rel d env,k+1) sign p)
+    | _ -> assert false
+  in aux envk (List.rev sign) p
+
 (** Finding a subterm up to some testing function *)
 
 exception SubtermUnificationError of subterm_unification_error
@@ -82,6 +95,7 @@ exception NotUnifiable of (constr * constr * unification_error) option
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
+  get_evars : 'a -> Evd.evar_map;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
 }
@@ -91,7 +105,7 @@ type 'a testing_function = {
    (b,l), b=true means no occurrence except the ones in l and b=false,
    means all occurrences except the ones in l *)
 
-let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
+let replace_term_occ_gen_modulo occs like_first test bywhat env cl occ t =
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
@@ -103,9 +117,9 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
     with NotUnifiable e when not like_first ->
       let lastpos = Option.get test.last_found in
      raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
-  let rec substrec k t =
+  let rec substrec (env,k) t =
     if nowhere_except_in && !pos > maxocc then t else
-    if not (Vars.closed0 t) then subst_below k t else
+    if not (Vars.closed0 t) then subst_below (env,k) t else
     try
       let subst = test.match_fun test.testing_state t in
       if Locusops.is_selected !pos occs then
@@ -118,31 +132,51 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
          add_subst t subst; incr pos;
          (* Check nested matching subterms *)
          if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then
-           begin nested := true; ignore (subst_below k t); nested := false end;
+           begin nested := true; ignore (subst_below (env,k) t); nested := false end;
          (* Do the effective substitution *)
          Vars.lift k (bywhat ()))
       else
-        (incr pos; subst_below k t)
+        (incr pos; subst_below (env,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 0 t in
+      subst_below (env,k) t
+  and subst_below (env,k) t =
+    match kind_of_term t with
+    | Case (ci,p,c,br) ->
+      let c = substrec (env,k) c in
+      let sigma = test.get_evars test.testing_state in
+      let t = Retyping.get_type_of env sigma c in
+      let IndType (indf,_) = find_rectype env sigma t in
+      let p = subst_cases_predicate (env,k) indf p in
+      let cstrs = get_constructors env indf in
+      let br = Array.map2 (subst_cases_branch (env,k) indf) br cstrs in
+      mkCase (ci,p,c,br)
+    | _ ->
+      map_constr_with_binders_left_to_right (fun d (env,k) -> (push_rel d env,k+1))
+        substrec (env,k) t
+  and subst_cases_predicate (env,k) indf p =
+    let arsign,_ = get_arity env indf in
+    let nrealargs = List.length arsign in
+    let (ind,params) = dest_ind_family indf in
+    let mind = applist (mkIndU ind,
+       (List.map (Vars.lift nrealargs) params)@(extended_rel_list 0 arsign)) in
+    process_under_binders substrec (env,k) ((Anonymous,None,mind)::arsign) p
+  and subst_cases_branch (env,k) indf b cstr =
+    process_under_binders substrec (env,k) cstr.cs_args b in
+  let t' = substrec (env,0) t in
   (!pos, t')
 
-let replace_term_occ_modulo occs test bywhat t =
+let replace_term_occ_modulo occs test bywhat env t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
   proceed_with_occurrences
-    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
+    (replace_term_occ_gen_modulo occs' like_first test bywhat env None) occs' t
 
-let replace_term_occ_decl_modulo occs test bywhat d =
+let replace_term_occ_decl_modulo occs test bywhat env d =
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (replace_term_occ_gen_modulo plocs like_first test bywhat)
+       (replace_term_occ_gen_modulo plocs like_first test bywhat env)
        hyploc)
     plocs d
 
@@ -156,23 +190,30 @@ let make_eq_univs_test env evd c =
 	with Evd.UniversesDiffer -> raise (NotUnifiable None)
       else raise (NotUnifiable None));
   merge_fun = (fun evd _ -> evd);
+  get_evars = (fun evd -> evd);
   testing_state = evd;
   last_found = None
 } 
 
-let subst_closed_term_occ env evd occs c t =
-  let test = make_eq_univs_test env evd c in
+let subst_closed_term_occ env sigma occs c t =
+  let test = make_eq_univs_test env sigma c in
   let bywhat () = mkRel 1 in
-  let t' = replace_term_occ_modulo occs test bywhat t in
+  let typ = Retyping.get_type_of env sigma c in
+  assert (rel_context env == []);
+  let env = push_rel (Anonymous,Some c,typ) env in
+  let t' = replace_term_occ_modulo occs test bywhat env t in
     t', test.testing_state
 
-let subst_closed_term_occ_decl env evd occs c d =
-  let test = make_eq_univs_test env evd c in
+let subst_closed_term_occ_decl env sigma occs c d =
+  let test = make_eq_univs_test env sigma c in
   let (plocs,hyploc),like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
   let bywhat () = mkRel 1 in
+  let typ = Retyping.get_type_of env sigma c in
+  assert (rel_context env == []);
+  let env = push_rel (Anonymous,Some c,typ) env in
   proceed_with_occurrences
     (map_named_declaration_with_hyploc
-       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
+       (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat env None)
        hyploc) plocs d,
   test.testing_state
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 47d9654e57..23d7ed9498 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -29,6 +29,7 @@ exception SubtermUnificationError of subterm_unification_error
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
+  get_evars : 'a -> evar_map;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
 }
@@ -43,14 +44,14 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
 val replace_term_occ_modulo : occurrences or_like_first ->
-  'a testing_function -> (unit -> constr) -> constr -> constr
+  'a testing_function -> (unit -> constr) -> env -> constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> constr) ->
-  named_declaration -> named_declaration
+  env -> named_declaration -> named_declaration
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 269c723e30..002fd0c025 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1530,6 +1530,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     | None, Some _ -> c2
     | None, None -> None in
   { match_fun = matching_fun; merge_fun = merge_fun;
+    get_evars = (function None -> sigma | Some (evd,_,_) -> evd);
     testing_state = None; last_found = None },
   (fun test -> match test.testing_state with
   | None -> None
@@ -1545,8 +1546,8 @@ let make_eq_test env evd c =
   (make_eq_univs_test env evd c, out)
 
 let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
+  let t = match ty with Some t -> t | None -> get_type_of env sigma c in
   let id =
-    let t = match ty with Some t -> t | None -> get_type_of env sigma c in
     let x = id_of_name_using_hdchar (Global.env()) t name in
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
@@ -1554,8 +1555,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       errorlabstrm "Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
-      x
-  in
+      x in
+  let env' = push_named (id, Some c, t) env in
   let likefirst = clause_with_generic_occurrences occs in
   let mkvarid () = mkVar id in
   let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) =
@@ -1571,7 +1572,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val d sign,depdecls)
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
-        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo occ test mkvarid env' d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
         then
@@ -1582,7 +1583,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
           (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
         (* There are specific occurrences, hence not like first *)
-        let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid env' d in
         (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
     let sign,depdecls =
@@ -1592,7 +1593,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          replace_term_occ_modulo occ test mkvarid concl
+          replace_term_occ_modulo occ test mkvarid env' concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in