- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


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

7 files changed, 112 insertions, 166 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index fe48cd4fa..79708e9fb 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -335,7 +335,14 @@ let all_flags =
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 
-type 'a with_occurrences = int or_var list * 'a
+type occurrences_expr = bool * int or_var list
+
+let all_occurrences_expr_but l = (false,l)
+let no_occurrences_expr_but l = (true,l)
+let all_occurrences_expr = (false,[])
+let no_occurrences_expr = (true,[])
+
+type 'a with_occurrences = occurrences_expr * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index ab67a0922..0eee3e73a 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -146,7 +146,14 @@ val all_flags : 'a raw_red_flag
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 
-type 'a with_occurrences = int or_var list * 'a
+type occurrences_expr = bool * int or_var list
+
+val all_occurrences_expr_but : int or_var list -> occurrences_expr
+val no_occurrences_expr_but : int or_var list -> occurrences_expr
+val all_occurrences_expr : occurrences_expr
+val no_occurrences_expr : occurrences_expr
+
+type 'a with_occurrences = occurrences_expr * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 05d108673..47bc132ac 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -35,16 +35,23 @@ exception ReductionTacticError of reduction_tactic_error
 exception Elimconst
 exception Redelimination
 
-let is_evaluable env ref =
-  match ref with
-      EvalConstRef kn ->
-        is_transparent (ConstKey kn) &&
-        let cb = Environ.lookup_constant kn env in
-        cb.const_body <> None & not cb.const_opaque
-    | EvalVarRef id ->
-        is_transparent (VarKey id) &&
-        let (_,value,_) = Environ.lookup_named id env in
-        value <> None
+let is_evaluable env = function
+  | EvalConstRef kn ->
+      is_transparent (ConstKey kn) &&
+      let cb = Environ.lookup_constant kn env in
+      cb.const_body <> None & not cb.const_opaque
+  | EvalVarRef id ->
+      is_transparent (VarKey id) &&
+      let (_,value,_) = Environ.lookup_named id env in
+      value <> None
+
+let value_of_evaluable_ref env = function
+  | EvalConstRef con -> constant_value env con
+  | EvalVarRef id -> Option.get (pi2 (lookup_named id env))
+
+let constr_of_evaluable_ref = function
+  | EvalConstRef con -> mkConst con
+  | EvalVarRef id -> mkVar id
 
 type evaluable_reference =
   | EvalConst of constant
@@ -627,20 +634,16 @@ let is_head c t =
     | App (f,_) -> f = c
     | _ -> false
 
-let contextually byhead (locs,c) f env sigma t =
+let contextually byhead ((nowhere_except_in,locs),c) f env sigma t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
-  let except = List.exists (fun n -> n<0) locs in
-  if except & (List.exists (fun n -> n>=0) locs) 
-  then error "mixing of positive and negative occurences"
-  else
-   let rec traverse (env,c as envc) t =
-    if locs <> [] & (not except) & (!pos > maxocc) then t
+  let rec traverse (env,c as envc) t =
+    if nowhere_except_in & (!pos > maxocc) then t
     else
     if (not byhead & eq_constr c t) or (byhead & is_head c t) then
       let ok = 
-	if except then not (List.mem (- !pos) locs)
-	else (locs = [] or List.mem !pos locs) in
+	if nowhere_except_in then List.mem !pos locs
+	else not (List.mem !pos locs) in
       incr pos;
       if ok then
 	f env sigma t
@@ -656,112 +659,34 @@ let contextually byhead (locs,c) f env sigma t =
         traverse envc t
   in
   let t' = traverse (env,c) t in
-  if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then
-    error_invalid_occurrence locs;
+  if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
   t'
 
 (* linear bindings (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
-let rec substlin env name n ol c =
-  match kind_of_term c with
-    | Const kn when EvalConstRef kn = name ->
-        if List.hd ol = n then
-          try 
-	    (n+1, List.tl ol, constant_value env kn)
-          with
-	      NotEvaluableConst _ ->
-		errorlabstrm "substlin"
-		  (pr_con kn ++ str " is not a defined constant")
-        else 
-	  ((n+1), ol, c)
-
-    | Var id when EvalVarRef id = name ->
-        if List.hd ol = n then
-          match lookup_named id env with
-	    | (_,Some c,_) -> (n+1, List.tl ol, c)
-	    | _ -> 
-		errorlabstrm "substlin"
-		  (pr_id id ++ str " is not a defined constant")
-        else 
-	  ((n+1), ol, c)
-
-    (* INEFFICIENT: OPTIMIZE *)
-    | App (c1,cl) ->
-        Array.fold_left 
-	  (fun (n1,ol1,c1') c2 ->
-	     (match ol1 with 
-                | [] -> (n1,[],applist(c1',[c2]))
-                | _  ->
-                    let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-                    (n2,ol2,applist(c1',[c2']))))
-          (substlin env name n ol c1) cl
-
-    | Lambda (na,c1,c2) ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkLambda (na,c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkLambda (na,c1',c2')))
-
-    | LetIn (na,c1,t,c2) ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkLetIn (na,c1',t,c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkLetIn (na,c1',t,c2')))
-
-    | Prod (na,c1,c2) ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkProd (na,c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkProd (na,c1',c2')))
-	
-    | Case (ci,p,d,llf) ->
-        let rec substlist nn oll = function
-          | []     -> (nn,oll,[])
-          | f::lfe ->
-              let (nn1,oll1,f') = substlin env name nn oll f in
-              (match oll1 with
-                 | [] -> (nn1,[],f'::lfe)
-                 | _  ->
-                     let (nn2,oll2,lfe') = substlist nn1 oll1 lfe in
-                     (nn2,oll2,f'::lfe'))
-	in
-	(* p is printed after d in v8 syntax *)
-	let (n1,ol1,d') = substlin env name n ol d in
-        (match ol1 with
-           | [] -> (n1,[],mkCase (ci, p, d', llf))
-           | _  ->
-               let (n2,ol2,p') = substlin env name n1 ol1 p in
-               (match ol2 with
-		  | [] -> (n2,[],mkCase (ci, p', d', llf))
-		  | _  -> 
-	              let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
-                      in (n3,ol3,mkCase (ci, p', d', Array.of_list lf'))))
-        
-    | Cast (c1,k,c2)   ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkCast (c1',k,c2))
-           | _  -> 
-	       let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkCast (c1',k,c2')))
-
-    | Fix _ -> 
-        (Flags.if_verbose
-	  warning "do not consider occurrences inside fixpoints"; (n,ol,c))
-	
-    | CoFix _ -> 
-        (Flags.if_verbose
-	  warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
 
-    | (Rel _|Meta _|Var _|Sort _
-      |Evar _|Const _|Ind _|Construct _) -> (n,ol,c)
+let substlin env evalref n (nowhere_except_in,locs) c =
+  let maxocc = List.fold_right max locs 0 in
+  let pos = ref n in
+  assert (List.for_all (fun x -> x >= 0) locs);
+  let value = value_of_evaluable_ref env evalref in
+  let term = constr_of_evaluable_ref evalref in
+  let rec substrec () c =
+    if nowhere_except_in & !pos > maxocc then c
+    else if c = term then
+      let ok = 
+	if nowhere_except_in then List.mem !pos locs
+	else not (List.mem !pos locs) in
+      incr pos;
+      if ok then value else c
+    else
+      map_constr_with_binders_left_to_right
+	(fun _ () -> ())
+        substrec () c
+  in
+  let t' = substrec () c in
+  (!pos, t')
 
 let string_of_evaluable_ref env = function
   | EvalVarRef id -> string_of_id id
@@ -779,16 +704,15 @@ let unfold env sigma name =
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
-let unfoldoccs env sigma (occl,name) c =
-  match occl with
-    | []  -> unfold env sigma name c
-    | l -> 
-        match substlin env name 1 (Sort.list (<) l) c with
-          | (_,[],uc) -> nf_betaiota uc
-          | (1,_,_) ->
-              error ((string_of_evaluable_ref env name)^" does not occur")
-          | (_,l,_) ->
-	      error_invalid_occurrence l
+let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
+  if locs = [] then if nowhere_except_in then c else unfold env sigma name c
+  else
+    let (nbocc,uc) = substlin env name 1 plocs c in
+    if nbocc = 1 then 
+      error ((string_of_evaluable_ref env name)^" does not occur");
+    let rest = List.filter (fun o -> o >= nbocc) locs in
+    if rest <> [] then error_invalid_occurrence rest;
+    nf_betaiota uc
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c = 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 0ff5154f6..1516a2bd6 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -16,6 +16,7 @@ open Evd
 open Reductionops
 open Closure
 open Rawterm
+open Termops
 (*i*)
 
 type reduction_tactic_error = 
@@ -47,13 +48,13 @@ val hnf_constr : reduction_function
 
 (* Unfold *)
 val unfoldn : 
-  (int list * evaluable_global_reference) list ->  reduction_function
+  (occurrences * evaluable_global_reference) list ->  reduction_function
 
 (* Fold *)
 val fold_commands : constr list ->  reduction_function
 
 (* Pattern *)
-val pattern_occs : (int list * constr) list ->  reduction_function
+val pattern_occs : (occurrences * constr) list ->  reduction_function
 (* Rem: Lazy strategies are defined in Reduction *)
 
 (* Call by value strategy (uses Closures) *)
@@ -81,7 +82,7 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-val contextually : bool -> int list * constr -> reduction_function
+val contextually : bool -> occurrences * constr -> reduction_function
   -> reduction_function
 
 (* Compatibility *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9a9e25c59..aa6c37491 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -621,32 +621,33 @@ let subst_term = subst_term_gen eq_constr
 
 let replace_term = replace_term_gen eq_constr
 
-(* Substitute only a list of locations locs, the empty list is
-   interpreted as substitute all, if 0 is in the list then no
-   bindings is done. The list may contain only negative occurrences
-   that will not be substituted. *)
+(* Substitute only at a list of locations or excluding a list of
+   locations; in the occurrences list (b,l), b=true means no
+   occurrence except the ones in l and b=false, means all occurrences
+   except the ones in l *)
+
+type occurrences = bool * int list
+let all_occurrences = (false,[])
+let no_occurrences_in_set = (true,[])
 
 let error_invalid_occurrence l =
   errorlabstrm ""
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ 
      prlist_with_sep spc int l)
 
-let subst_term_occ_gen locs occ c t =
+let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
-  let except = List.exists (fun n -> n<0) locs in
-  if except & (List.exists (fun n -> n>=0) locs) 
-  then error "mixing of positive and negative occurences"
-  else
-   let rec substrec (k,c as kc) t =
-    if (not except) & (!pos > maxocc) then t
+  assert (List.for_all (fun x -> x >= 0) locs);
+  let rec substrec (k,c as kc) t =
+    if nowhere_except_in & !pos > maxocc then t
     else
     if eq_constr c t then
       let r = 
-	if except then 
-	  if List.mem (- !pos) locs then t else (mkRel k)
-	else 
+	if nowhere_except_in then
 	  if List.mem !pos locs then (mkRel k) else t
+	else 
+	  if List.mem !pos locs then t else (mkRel k)
       in incr pos; r
     else
       map_constr_with_binders_left_to_right
@@ -656,28 +657,27 @@ let subst_term_occ_gen locs occ c t =
   let t' = substrec (1,c) t in
   (!pos, t')
 
-let subst_term_occ locs c t = 
-  if locs = [] then subst_term c t
-  else if List.mem 0 locs then 
-    t
+let subst_term_occ (nowhere_except_in,locs as plocs) c t = 
+  if locs = [] then if nowhere_except_in then t else subst_term c t
   else 
-    let (nbocc,t') = subst_term_occ_gen locs 1 c t in
-    let rest = List.filter (fun o -> o >= nbocc or o <= -nbocc) locs in
+    let (nbocc,t') = subst_term_occ_gen plocs 1 c t in
+    let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
     t'
 
-let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
+let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) =
   match bodyopt with
-    | None -> (id,None,subst_term_occ locs c typ)
+    | None -> (id,None,subst_term_occ plocs c typ)
     | Some body -> 
 	if locs = [] then
-	  (id,Some (subst_term c body),subst_term c typ)
-	else if List.mem 0 locs then 
-	  d
+	  if nowhere_except_in then
+	    (id,Some (subst_term c body),subst_term c typ)
+	  else
+	    d
 	else 
-	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
-	  let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in
-	  let rest = List.filter (fun o -> o >= nbocc' or o <= -nbocc') locs in
+	  let (nbocc,body') = subst_term_occ_gen plocs 1 c body in
+	  let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in
+	  let rest = List.filter (fun o -> o >= nbocc') locs in
 	  if rest <> [] then error_invalid_occurrence rest;
 	  (id,Some body',t')
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index bc483cfc3..f80deab10 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -131,18 +131,24 @@ val subst_term : constr -> constr -> constr
 (* [replace_term d e c] replaces [d] by [e] in [c] *)
 val replace_term : constr -> constr -> constr -> constr
 
+(* In occurrences sets, false = everywhere except and true = nowhere except *)
+type occurrences = bool * int list
+val all_occurrences : occurrences
+val no_occurrences_in_set : occurrences
+
 (* [subst_term_occ_gen occl n c d] replaces occurrences of [c] at
    positions [occl], counting from [n], by [Rel 1] in [d] *)
-val subst_term_occ_gen : int list -> int -> constr -> types -> int * types
+val subst_term_occ_gen : 
+  occurrences -> int -> constr -> types -> int * types
 
 (* [subst_term_occ occl c d] replaces occurrences of [c] at
    positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
-val subst_term_occ : int list -> constr -> constr -> constr
+val subst_term_occ : occurrences -> constr -> constr -> constr
 
 (* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
    positions [occl] by [Rel 1] in [decl] *)
 val subst_term_occ_decl :
-  int list -> constr -> named_declaration -> named_declaration
+  occurrences -> constr -> named_declaration -> named_declaration
 
 val error_invalid_occurrence : int list -> 'a
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ca1be55bb..41d6ff4c1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -44,7 +44,8 @@ let abstract_scheme env c l lname_typ =
 
 let abstract_list_all env evd typ c l =
   let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in
-  let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in 
+  let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
+  let p = abstract_scheme env c l_with_all_occs ctxt in 
   try 
     if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p
     else error "abstract_list_all"