summaryrefslogtreecommitdiff
path: root/pretyping/namegen.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /pretyping/namegen.ml
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'pretyping/namegen.ml')
-rw-r--r--pretyping/namegen.ml204
1 files changed, 134 insertions, 70 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 76b9bd8a..5aca11ae 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -15,25 +15,42 @@
open Util
open Names
open Term
+open Vars
open Nametab
open Nameops
open Libnames
+open Globnames
open Environ
open Termops
(**********************************************************************)
+(* Conventional names *)
+
+let default_prop_string = "H"
+let default_prop_ident = Id.of_string default_prop_string
+
+let default_small_string = "H"
+let default_small_ident = Id.of_string default_small_string
+
+let default_type_string = "X"
+let default_type_ident = Id.of_string default_type_string
+
+let default_non_dependent_string = "H"
+let default_non_dependent_ident = Id.of_string default_non_dependent_string
+
+let default_dependent_ident = Id.of_string "x"
+
+(**********************************************************************)
(* Globality of identifiers *)
-let rec is_imported_modpath mp =
- let current_mp,_ = Lib.current_prefix() in
- match mp with
- | MPfile dp ->
- let rec find_prefix = function
- |MPfile dp1 -> not (dp1=dp)
- |MPdot(mp,_) -> find_prefix mp
- |MPbound(_) -> false
- in find_prefix current_mp
- | p -> false
+let is_imported_modpath = function
+ | MPfile dp ->
+ let rec find_prefix = function
+ |MPfile dp1 -> not (DirPath.equal dp1 dp)
+ |MPdot(mp,_) -> find_prefix mp
+ |MPbound(_) -> false
+ in find_prefix (Lib.current_mp ())
+ | _ -> false
let is_imported_ref = function
| VarRef _ -> false
@@ -61,8 +78,22 @@ let is_constructor id =
(**********************************************************************)
(* Generating "intuitive" names from its type *)
+let head_name c = (* Find the head constant of a constr if any *)
+ let rec hdrec c =
+ match kind_of_term c with
+ | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
+ | Cast (c,_,_) | App (c,_) -> hdrec c
+ | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
+ | Const _ | Ind _ | Construct _ | Var _ ->
+ Some (basename_of_global (global_of_constr c))
+ | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
+ Some (match lna.(i) with Name id -> id | _ -> assert false)
+ | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
+ in
+ hdrec c
+
let lowercase_first_char id = (* First character of a constr *)
- lowercase_first_char_utf8 (string_of_id id)
+ Unicode.lowercase_first_char (Id.to_string id)
let sort_hdchar = function
| Prop(_) -> "P"
@@ -71,14 +102,12 @@ let sort_hdchar = function
let hdchar env c =
let rec hdrec k c =
match kind_of_term c with
- | Prod (_,_,c) -> hdrec (k+1) c
- | Lambda (_,_,c) -> hdrec (k+1) c
- | LetIn (_,_,_,c) -> hdrec (k+1) c
- | Cast (c,_,_) -> hdrec k c
- | App (f,l) -> hdrec k f
- | Const kn -> lowercase_first_char (id_of_label (con_label kn))
- | Ind x -> lowercase_first_char (basename_of_global (IndRef x))
- | Construct x -> lowercase_first_char (basename_of_global (ConstructRef x))
+ | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
+ | Cast (c,_,_) | App (c,_) -> hdrec k c
+ | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
+ | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
+ | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
+ | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
| Var id -> lowercase_first_char id
| Sort s -> sort_hdchar s
| Rel n ->
@@ -88,22 +117,20 @@ let hdchar env c =
| (Name id,_,_) -> lowercase_first_char id
| (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
with Not_found -> "y")
- | Fix ((_,i),(lna,_,_)) ->
- let id = match lna.(i) with Name id -> id | _ -> assert false in
- lowercase_first_char id
- | CoFix (i,(lna,_,_)) ->
+ | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
let id = match lna.(i) with Name id -> id | _ -> assert false in
lowercase_first_char id
- | Meta _|Evar _|Case (_, _, _, _) -> "y"
+ | Evar _ (* We could do better... *)
+ | Meta _ | Case (_, _, _, _) -> "y"
in
hdrec 0 c
let id_of_name_using_hdchar env a = function
- | Anonymous -> id_of_string (hdchar env a)
+ | Anonymous -> Id.of_string (hdchar env a)
| Name id -> id
let named_hd env a = function
- | Anonymous -> Name (id_of_string (hdchar env a))
+ | Anonymous -> Name (Id.of_string (hdchar env a))
| x -> x
let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b)
@@ -138,8 +165,6 @@ let it_mkLambda_or_LetIn_name env b hyps =
(**********************************************************************)
(* Fresh names *)
-let default_x = id_of_string "x"
-
(* Looks for next "good" name by lifting subscript *)
let next_ident_away_from id bad =
@@ -151,17 +176,46 @@ let next_ident_away_from id bad =
let restart_subscript id =
if not (has_subscript id) then id else
- (* Ce serait sans doute mieux avec quelque chose inspiré de
- *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+ (* It would probably be better with something in the spirit of
+ *** make_ident id (Some 0) *** but compatibility would be lost... *)
forget_subscript id
+let rec to_avoid id = function
+| [] -> false
+| id' :: avoid -> Id.equal id id' || to_avoid id avoid
+
+let occur_rel p env id =
+ try
+ let name = lookup_name_of_rel p env in
+ begin match name with
+ | Name id' -> Id.equal id' id
+ | Anonymous -> false
+ end
+ with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+ let rec occur n c = match kind_of_term c with
+ | Const _ | Ind _ | Construct _ | Var _
+ when
+ let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in
+ qualid_eq short (qualid_of_ident id) ->
+ raise Occur
+ | Rel p when p>n && occur_rel (p-n) nenv id -> raise Occur
+ | _ -> iter_constr_with_binders succ occur n c
+ in
+ try occur 1 c; false
+ with Occur -> true
+ | Not_found -> false (* Happens when a global is not in the env *)
+
(* Now, there are different renaming strategies... *)
(* 1- Looks for a fresh name for printing in cases pattern *)
-let next_name_away_in_cases_pattern na avoid =
- let id = match na with Name id -> id | Anonymous -> default_x in
- next_ident_away_from id (fun id -> List.mem id avoid or is_constructor id)
+let next_name_away_in_cases_pattern env_t na avoid =
+ let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
+ let bad id = to_avoid id avoid || is_constructor id
+ || visibly_occur_id id env_t in
+ next_ident_away_from id bad
(* 2- Looks for a fresh name for introduction in goal *)
@@ -173,12 +227,14 @@ let next_name_away_in_cases_pattern na avoid =
name is taken by finding a free subscript starting from 0 *)
let next_ident_away_in_goal id avoid =
- let id = if List.mem id avoid then restart_subscript id else id in
- let bad id = List.mem id avoid || (is_global id & not (is_section_variable id)) in
+ let id = if to_avoid id avoid then restart_subscript id else id in
+ let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in
next_ident_away_from id bad
let next_name_away_in_goal na avoid =
- let id = match na with Name id -> id | Anonymous -> id_of_string "H" in
+ let id = match na with
+ | Name id -> id
+ | Anonymous -> default_non_dependent_ident in
next_ident_away_in_goal id avoid
(* 3- Looks for next fresh name outside a list that is moreover valid
@@ -189,20 +245,20 @@ let next_name_away_in_goal na avoid =
beyond the current subscript *)
let next_global_ident_away id avoid =
- let id = if List.mem id avoid then restart_subscript id else id in
- let bad id = List.mem id avoid || is_global id in
+ let id = if to_avoid id avoid then restart_subscript id else id in
+ let bad id = to_avoid id avoid || is_global id in
next_ident_away_from id bad
(* 4- Looks for next fresh name outside a list; if name already used,
looks for same name with lower available subscript *)
let next_ident_away id avoid =
- if List.mem id avoid then
- next_ident_away_from (restart_subscript id) (fun id -> List.mem id avoid)
+ if to_avoid id avoid then
+ next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid)
else id
let next_name_away_with_default default na avoid =
- let id = match na with Name id -> id | Anonymous -> id_of_string default in
+ let id = match na with Name id -> id | Anonymous -> Id.of_string default in
next_ident_away id avoid
let reserved_type_name = ref (fun t -> Anonymous)
@@ -213,10 +269,10 @@ let next_name_away_with_default_using_types default na avoid t =
| Name id -> id
| Anonymous -> match !reserved_type_name t with
| Name id -> id
- | Anonymous -> id_of_string default in
+ | Anonymous -> Id.of_string default in
next_ident_away id avoid
-let next_name_away = next_name_away_with_default "H"
+let next_name_away = next_name_away_with_default default_non_dependent_string
let make_all_name_different env =
let avoid = ref (ids_of_named_context (named_context env)) in
@@ -232,24 +288,8 @@ let make_all_name_different env =
looks for name of same base with lower available subscript beyond current
subscript *)
-let occur_rel p env id =
- try lookup_name_of_rel p env = Name id
- with Not_found -> false (* Unbound indice : may happen in debug *)
-
-let visibly_occur_id id (nenv,c) =
- let rec occur n c = match kind_of_term c with
- | Const _ | Ind _ | Construct _ | Var _
- when shortest_qualid_of_global Idset.empty (global_of_constr c)
- = qualid_of_ident id -> raise Occur
- | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
- | _ -> iter_constr_with_binders succ occur n c
- in
- try occur 1 c; false
- with Occur -> true
- | Not_found -> false (* Happens when a global is not in the env *)
-
let next_ident_away_for_default_printing env_t id avoid =
- let bad id = List.mem id avoid or visibly_occur_id id env_t in
+ let bad id = to_avoid id avoid || visibly_occur_id id env_t in
next_ident_away_from id bad
let next_name_away_for_default_printing env_t na avoid =
@@ -259,7 +299,7 @@ let next_name_away_for_default_printing env_t na avoid =
(* In principle, an anonymous name is not dependent and will not be *)
(* taken into account by the function compute_displayed_name_in; *)
(* just in case, invent a valid name *)
- id_of_string "H" in
+ default_non_dependent_ident in
next_ident_away_for_default_printing env_t id avoid
(**********************************************************************)
@@ -281,29 +321,31 @@ let next_name_away_for_default_printing env_t na avoid =
*)
type renaming_flags =
- | RenamingForCasesPattern
+ | RenamingForCasesPattern of (Name.t list * constr)
| RenamingForGoal
- | RenamingElsewhereFor of (name list * constr)
+ | RenamingElsewhereFor of (Name.t list * constr)
let next_name_for_display flags =
match flags with
- | RenamingForCasesPattern -> next_name_away_in_cases_pattern
+ | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t
| RenamingForGoal -> next_name_away_in_goal
| RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
(* Remark: Anonymous var may be dependent in Evar's contexts *)
let compute_displayed_name_in flags avoid na c =
- if na = Anonymous & noccurn 1 c then
+ match na with
+ | Anonymous when noccurn 1 c ->
(Anonymous,avoid)
- else
+ | _ ->
let fresh_id = next_name_for_display flags na avoid in
let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
(idopt, fresh_id::avoid)
let compute_and_force_displayed_name_in flags avoid na c =
- if na = Anonymous & noccurn 1 c then
+ match na with
+ | Anonymous when noccurn 1 c ->
(Anonymous,avoid)
- else
+ | _ ->
let fresh_id = next_name_for_display flags na avoid in
(Name fresh_id, fresh_id::avoid)
@@ -311,7 +353,7 @@ let compute_displayed_let_name_in flags avoid na c =
let fresh_id = next_name_for_display flags na avoid in
(Name fresh_id, fresh_id::avoid)
-let rec rename_bound_vars_as_displayed avoid env c =
+let rename_bound_vars_as_displayed avoid env c =
let rec rename avoid env c =
match kind_of_term c with
| Prod (na,c1,c2) ->
@@ -328,3 +370,25 @@ let rec rename_bound_vars_as_displayed avoid env c =
| _ -> c
in
rename avoid env c
+
+(**********************************************************************)
+(* "H"-based naming strategy introduced June 2014 for hypotheses in
+ Prop produced by case/elim/destruct/induction, in place of the
+ strategy that was using the first letter of the type, leading to
+ inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar
+ types *)
+
+let h_based_elimination_names = ref false
+
+let use_h_based_elimination_names () =
+ !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4
+
+open Goptions
+
+let _ = declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "use of \"H\"-based proposition names in elimination tactics";
+ optkey = ["Standard";"Proposition";"Elimination";"Names"];
+ optread = (fun () -> !h_based_elimination_names);
+ optwrite = (:=) h_based_elimination_names }