Évitement des noms de constructeurs dans les motifs de filtrage de "match"

(un peu de doc de termops.mli au passage)


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

3 files changed, 76 insertions, 25 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1fcc6d8b7..8de9e2abe 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -174,17 +174,18 @@ let computable p k =
   let _,ccl = decompose_lam p in 
   noccur_between 1 (k+1) ccl
 
-
+let avoid_flag isgoal = if isgoal then Some true else None
+ 
 let lookup_name_as_renamed env t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
     | Prod (name,_,c') ->
-	(match concrete_name true avoid env_names name c' with
+	(match concrete_name (Some true) avoid env_names name c' with
            | (Name id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-	(match concrete_name true avoid env_names name c' with
+	(match concrete_name (Some true) avoid env_names name c' with
            | (Name id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
@@ -196,11 +197,11 @@ let lookup_name_as_renamed env t s =
 let lookup_index_as_renamed env t n =
   let rec lookup n d c = match kind_of_term c with
     | Prod (name,_,c') ->
-	  (match concrete_name true [] empty_names_context name c' with
+	  (match concrete_name (Some true) [] empty_names_context name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match concrete_name true [] empty_names_context name c' with
+	  (match concrete_name (Some true) [] empty_names_context name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | Cast (c,_,_) -> lookup n d c
@@ -227,7 +228,7 @@ let rec decomp_branch n nal b (avoid,env as e) c =
 	| _ -> 
 	    Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])), 
 	    concrete_name in
-    let na',avoid' = f b avoid env na c in
+    let na',avoid' = f (Some b) avoid env na c in
     decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
 
 let rec build_tree na isgoal e ci cl =
@@ -355,7 +356,7 @@ let detype_sort = function
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let rec detype isgoal avoid env t =
+let rec detype (isgoal:bool) avoid env t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
@@ -484,7 +485,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
     if force_wildcard () & noccurn 1 b then
       PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
     else 
-      let id = next_name_away_with_default "x" x avoid in
+      let id = next_name_away_in_cases_pattern x avoid in
       PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids
   in
   let rec buildrec ids patlist avoid env n b =
@@ -519,9 +520,9 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
 and detype_binder isgoal bk avoid env na ty c =
   let na',avoid' =
     if bk = BLetIn then
-      concrete_let_name isgoal avoid env na c
+      concrete_let_name (avoid_flag isgoal) avoid env na c
     else
-      concrete_name isgoal avoid env na c in
+      concrete_name (avoid_flag isgoal) avoid env na c in
   let r =  detype isgoal avoid' (add_name na' env) c in
   match bk with
   | BProd -> RProd (dl, na',detype isgoal avoid env ty, r)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 08c38f1b1..d3283164b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -834,6 +834,14 @@ let is_global id =
   with Not_found -> 
     false
 
+let is_constructor id =
+  try 
+    match locate (make_short_qualid id) with 
+      | ConstructRef _ as ref -> not (is_imported_ref ref)
+      | _ -> false
+  with Not_found -> 
+    false
+
 let is_section_variable id =
   try let _ = Global.lookup_named id in true
   with Not_found -> false
@@ -898,11 +906,19 @@ let occur_id nenv id0 c =
   with Occur -> true
     | Not_found -> false (* Case when a global is not in the env *)
 
-let next_name_not_occuring is_goal_ccl name l env_names t =
+type avoid_flags = bool option
+
+let next_name_not_occuring avoid_flags name l env_names t =
   let rec next id =
     if List.mem id l or occur_id env_names id t or 
-      (* To be consistent with intro mechanism *)
-      (is_goal_ccl & is_global id & not (is_section_variable id))
+      (* Further restrictions ? *)
+      match avoid_flags with None -> false | Some not_only_cstr ->
+      (if not_only_cstr then
+	(* To be consistent with the intro mechanism *)
+	is_global id & not (is_section_variable id)
+      else
+	(* To avoid constructors in pattern-matchings *)
+	is_constructor id)
     then next (lift_ident id)
     else id
   in 
@@ -996,17 +1012,26 @@ let global_vars_set_of_decl env = function
       Idset.union (global_vars_set env t)
         (global_vars_set env c)
 
+let default_x = id_of_string "x"
+
+let rec next_name_away_in_cases_pattern id avoid =
+  let id = match id with Name id -> id | Anonymous -> default_x in
+  let rec next id =
+    if List.mem id avoid or is_constructor id then next (lift_ident id)
+    else id in
+  next id
+
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name is_goal_ccl l env_names n c =
+let concrete_name avoid_flags l env_names n c =
   if n = Anonymous & noccurn 1 c then
     (Anonymous,l)
   else
-    let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
+    let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
     let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
     (idopt, fresh_id::l)
 
-let concrete_let_name is_goal_ccl l env_names n c =
-  let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
+let concrete_let_name avoid_flags l env_names n c =
+  let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
   (Name fresh_id, fresh_id::l)
 
 let rec rename_bound_var env l c =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d461498d9..37667f741 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -100,6 +100,7 @@ val occur_var_in_decl :
   identifier -> 'a * types option * types -> bool
 val occur_term : constr -> constr -> bool
 val free_rels : constr -> Intset.t
+val dependent : constr -> constr -> bool
 
 (* Substitution of metavariables *)
 type metamap = (metavariable * constr) list 
@@ -108,19 +109,36 @@ val subst_meta : metamap -> constr -> constr
 (* [pop c] lifts by -1 the positive indexes in [c] *)
 val pop : constr -> constr
 
-(* bindings of an arbitrary large term. Uses equality modulo
+(*s Substitution of an arbitrary large term. Uses equality modulo
    reduction of let *)
-val dependent : constr -> constr -> bool
+
+(* [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq]
+   as equality *)
 val subst_term_gen :
   (constr -> constr -> bool) -> constr -> constr -> constr
+
+(* [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
+   as equality *)
 val replace_term_gen :
   (constr -> constr -> bool) ->
     constr -> constr -> constr -> constr
+
+(* [subst_term d c] replaces [Rel 1] by [d] in [c] *)
 val subst_term : constr -> constr -> constr
+
+(* [replace_term d e c] replaces [d] by [e] in [c] *)
 val replace_term : constr -> constr -> constr -> constr
-val subst_term_occ_gen :
-  int list -> int -> constr -> types -> int * types
-val subst_term_occ : int list -> constr -> types -> types
+
+(* [subst_term_occ occl c d] replaces occurrences of [Rel 1] at
+   positions [occl] by [c] in [d] *)
+val subst_term_occ_gen : int list -> int -> constr -> types -> int * types
+
+(* [subst_term_occ occl c d] replaces occurrences of [Rel 1] at
+   positions [occl] by [c] in [d] (see also Note OCC) *)
+val subst_term_occ : int list -> constr -> constr -> constr
+
+(* [subst_term_occ_decl occl c decl] replaces occurrences of [Rel 1] at
+   positions [occl] by [c] in [decl] *)
 val subst_term_occ_decl :
   int list -> constr -> named_declaration -> named_declaration
 
@@ -177,15 +195,22 @@ type used_idents = identifier list
 val occur_rel : int -> name list -> identifier -> bool
 val occur_id : name list -> identifier -> constr -> bool
 
+type avoid_flags = bool option
+ (* Some true = avoid all globals (as in intro); 
+    Some false = avoid only global constructors; None = don't avoid globals *)
+
+val next_name_away_in_cases_pattern : 
+  name -> identifier list -> identifier
 val next_global_ident_away : 
   (*allow section vars:*) bool -> identifier -> identifier list -> identifier
 val next_name_not_occuring :
-  bool -> name -> identifier list -> name list -> constr -> identifier
+  avoid_flags -> name -> identifier list -> name list -> constr -> identifier
 val concrete_name :
-  bool -> identifier list -> name list -> name -> constr -> 
+  avoid_flags -> identifier list -> name list -> name -> constr -> 
     name * identifier list
 val concrete_let_name :
-  bool -> identifier list -> name list -> name -> constr -> name * identifier list
+  avoid_flags -> identifier list -> name list -> name -> constr -> 
+    name * identifier list
 val rename_bound_var : env -> identifier list -> types -> types
 
 (* other signature iterators *)