aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/inductiveops.ml43
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--pretyping/namegen.ml28
-rw-r--r--pretyping/namegen.mli1
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/retyping.mli3
6 files changed, 65 insertions, 24 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e180c13465..07dacd0ccc 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -307,7 +307,7 @@ let make_arity_signature env dep indf =
let (arsign,_) = get_arity env indf in
if dep then
(* We need names everywhere *)
- name_context env
+ Namegen.name_context env
((Anonymous,None,build_dependent_inductive env indf)::arsign)
(* Costly: would be better to name once for all at definition time *)
else
@@ -320,7 +320,7 @@ let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
let build_branch_type env dep p cs =
let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
if dep then
- it_mkProd_or_LetIn_name env
+ Namegen.it_mkProd_or_LetIn_name env
(applist (base,[build_dependent_constructor cs]))
cs.cs_args
else
@@ -371,13 +371,28 @@ let find_coinductive env sigma c =
(* find appropriate names for pattern variables. Useful in the Case
and Inversion (case_then_using et case_nodep_then_using) tactics. *)
+let h_based_elimination_names = ref true
+
+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 }
+
let is_predicate_explicitly_dep env pred arsign =
let rec srec env pval arsign =
let pv' = whd_betadeltaiota env Evd.empty pval in
match kind_of_term pv', arsign with
| Lambda (na,t,b), (_,None,_)::arsign ->
srec (push_rel_assum (na,t) env) b arsign
- | Lambda (na,_,_), _ ->
+ | Lambda (na,_,t), _ ->
(* The following code has an impact on the introduction names
given by the tactics "case" and "inversion": when the
@@ -396,10 +411,12 @@ let is_predicate_explicitly_dep env pred arsign =
dependency status (of course, Anonymous implies non
dependent, but not conversely).
- At the end, this is only to preserve the compatibility: a
- check whether the predicate is actually dependent or not
- would indeed be more natural! *)
+ From Coq > 8.2, using or not the the effective dependency of
+ the predicate is parametrable! *)
+ if use_h_based_elimination_names () then
+ dependent (mkRel 1) t
+ else
begin match na with
| Anonymous -> false
| Name _ -> true
@@ -413,11 +430,13 @@ let is_elim_predicate_explicitly_dependent env pred indf =
let arsign,_ = get_arity env indf in
is_predicate_explicitly_dep env pred arsign
-let set_names env n brty =
+let set_names preprocess_names env n brty =
let (ctxt,cl) = decompose_prod_n_assum n brty in
- it_mkProd_or_LetIn_name env cl ctxt
+ let ctxt =
+ if use_h_based_elimination_names () then preprocess_names ctxt else ctxt in
+ Namegen.it_mkProd_or_LetIn_name env cl ctxt
-let set_pattern_names env ind brv =
+let set_pattern_names preprocess_names env ind brv =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let arities =
Array.map
@@ -425,9 +444,9 @@ let set_pattern_names env ind brv =
rel_context_length ((prod_assum c)) -
mib.mind_nparams)
mip.mind_nf_lc in
- Array.map2 (set_names env) arities brv
+ Array.map2 (set_names preprocess_names env) arities brv
-let type_case_branches_with_names env indspec p c =
+let type_case_branches_with_names preprocess_names env indspec p c =
let (ind,args) = indspec in
let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
@@ -437,7 +456,7 @@ let type_case_branches_with_names env indspec p c =
let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
(* Adjust names *)
if is_elim_predicate_explicitly_dependent env p (ind,params) then
- (set_pattern_names env (fst ind) lbrty, conclty)
+ (set_pattern_names preprocess_names env (fst ind) lbrty, conclty)
else (lbrty, conclty)
(* Type of Case predicates *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index fca0c64bf5..1efc29c8fd 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -129,8 +129,8 @@ val arity_of_case_predicate :
env -> inductive_family -> bool -> sorts -> types
val type_case_branches_with_names :
- env -> pinductive * constr list -> constr -> constr ->
- types array * types
+ (rel_context -> rel_context) -> env -> pinductive * constr list -> constr ->
+ constr -> types array * types
(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index c6c21f0259..0581f7283e 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -61,6 +61,20 @@ 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 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 *)
Unicode.lowercase_first_char (Id.to_string id)
@@ -71,11 +85,8 @@ 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
+ | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
+ | Cast (c,_,_) | App (c,_) -> hdrec k c
| Proj (kn,_)
| Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
| Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
@@ -89,13 +100,10 @@ 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"
+ | Meta _ | Evar _ | Case (_, _, _, _) -> "y"
in
hdrec 0 c
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 095c7a59fd..857867f3a9 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -19,6 +19,7 @@ val sort_hdchar : sorts -> string
val hdchar : env -> types -> string
val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
val named_hd : env -> types -> Name.t -> Name.t
+val head_name : types -> Id.t option
val mkProd_name : env -> Name.t * types * types -> types
val mkLambda_name : env -> Name.t * types * constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 0c2bad5c6a..53c2603d8c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -232,3 +232,13 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
(* Makes an unsafe judgment from a constr *)
let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
+
+(* Returns sorts of a context *)
+let sorts_of_context env evc ctxt =
+ let rec aux = function
+ | [] -> env,[]
+ | (_,_,t as d)::ctxt ->
+ let env,sorts = aux ctxt in
+ let s = get_sort_of env evc t in
+ (push_rel d env,s::sorts) in
+ snd (aux ctxt)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index b8b458555a..a694faf4ed 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -8,6 +8,7 @@
open Term
open Evd
+open Context
open Environ
(** This family of functions assumes its constr argument is known to be
@@ -42,3 +43,5 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
val type_of_global_reference_knowing_conclusion :
env -> evar_map -> constr -> types -> evar_map * types
+
+val sorts_of_context : env -> evar_map -> rel_context -> sorts list
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 21:03:09 +0000