aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.mli2
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/evarsolve.ml8
-rw-r--r--pretyping/inductiveops.ml5
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/pretype_errors.mli4
-rw-r--r--pretyping/pretyping.ml26
-rw-r--r--pretyping/reductionops.ml1
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/retyping.ml8
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/tacred.mli4
-rw-r--r--pretyping/typing.ml58
-rw-r--r--pretyping/typing.mli2
14 files changed, 81 insertions, 47 deletions
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index 6a776dc961..6d1b6eefd4 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -17,6 +17,8 @@ val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit
(** [Not_found] is raised if no names are defined for [r] *)
val arguments_names : GlobRef.t -> Name.t list
+val rename_type : types -> GlobRef.t -> types
+
val rename_type_of_constant : env -> pconstant -> types
val rename_type_of_inductive : env -> pinductive -> types
val rename_type_of_constructor : env -> pconstructor -> types
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e15c00f7dc..e21c2fda85 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -104,6 +104,7 @@ let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env ev
Evar_kinds.qm_name=na;
}) in
let evd, v = Evarutil.new_evar env !evdref ~src c in
+ let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in
evdref := evd;
v
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 674f6846ae..96213af9c6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
(** Refresh the types of evars under template polymorphic references *)
let rec refresh_term_evars ~onevars ~top t =
match EConstr.kind !evdref t with
- | App (f, args) when is_template_polymorphic env !evdref f ->
+ | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
let pos = get_polymorphic_positions !evdref f in
refresh_polymorphic_positions args pos; t
| App (f, args) when top && isEvar !evdref f ->
@@ -1240,9 +1240,9 @@ let check_evar_instance evd evk1 body conv_algo =
let update_evar_info ev1 ev2 evd =
(* We update the source of obligation evars during evar-evar unifications. *)
- let loc, evs2 = evar_source ev2 evd in
- let evi = Evd.find evd ev1 in
- Evd.add evd ev1 {evi with evar_source = loc, evs2}
+ let loc, evs1 = evar_source ev1 evd in
+ let evi = Evd.find evd ev2 in
+ Evd.add evd ev2 {evi with evar_source = loc, evs1}
let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
try
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ea222397a8..14358dd02a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -746,8 +746,11 @@ let type_of_projection_knowing_arg env sigma p c ty =
syntactic conditions *)
let control_only_guard env sigma c =
+ let c = Evarutil.nf_evar sigma c in
let check_fix_cofix e c =
- match kind (EConstr.to_constr sigma c) with
+ (** [c] has already been normalized upfront *)
+ let c = EConstr.Unsafe.to_constr c in
+ match kind c with
| CoFix (_,(_,_,_) as cofix) ->
Inductive.check_cofix e cofix
| Fix (_,(_,_,_) as fix) ->
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 856894d9a6..01b0d96f98 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -164,8 +164,8 @@ let error_not_product ?loc env sigma c =
(*s Error in conversion from AST to glob_constr *)
-let error_var_not_found ?loc s =
- raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
+let error_var_not_found ?loc env sigma s =
+ raise_pretype_error ?loc (env, sigma, VarNotFound s)
(*s Typeclass errors *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6f14d025c7..054f0c76a9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -150,9 +150,7 @@ val error_unexpected_type :
val error_not_product :
?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
-(** {6 Error in conversion from AST to glob_constr } *)
-
-val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
+val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
(** {6 Typeclass errors } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 37afcf75e1..cba1533da5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let pretype_id pretype k0 loc env sigma id =
sigma, { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
with Not_found ->
(* [id] not found, standard error message *)
- error_var_not_found ?loc id
+ error_var_not_found ?loc !!env sigma id
(*************************************************************************)
(* Main pretyping function *)
@@ -436,7 +436,7 @@ let pretype_ref ?loc sigma env ref us =
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
variables *)
- Pretype_errors.error_var_not_found ?loc id)
+ Pretype_errors.error_var_not_found ?loc !!env sigma id)
| ref ->
let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
let ty = unsafe_type_of !!env sigma c in
@@ -457,6 +457,15 @@ let pretype_sort ?loc sigma = function
let new_type_evar env sigma loc =
new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
+let mark_obligation_evar sigma k evc =
+ if Flags.is_program_mode () then
+ match k with
+ | Evar_kinds.QuestionMark _
+ | Evar_kinds.ImplicitArg (_, _, false) ->
+ Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+ | _ -> sigma
+ else sigma
+
(* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [sigma] and *)
(* the type constraint tycon *)
@@ -510,15 +519,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
| Some ty -> sigma, ty
| None -> new_type_evar env sigma loc in
let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
- let sigma =
- if Flags.is_program_mode () then
- match k with
- | Evar_kinds.QuestionMark _
- | Evar_kinds.ImplicitArg (_, _, false) ->
- Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val))
- | _ -> sigma
- else sigma
- in
+ let sigma = mark_obligation_evar sigma k uj_val in
sigma, { uj_val; uj_type = ty }
| GHole (k, _naming, Some arg) ->
@@ -691,7 +692,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
let sigma, resj =
match EConstr.kind sigma resj.uj_val with
| App (f,args) ->
- if is_template_polymorphic !!env sigma f then
+ if Termops.is_template_polymorphic_ind !!env sigma f then
(* Special case for inductive type applications that must be
refreshed right away. *)
let c = mkApp (f, args) in
@@ -1039,6 +1040,7 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
| None ->
let sigma, s = new_sort_variable univ_flexible_alg sigma in
let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
+ let sigma = mark_obligation_evar sigma knd utj_val in
sigma, { utj_val; utj_type = s})
| _ ->
let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 367a48cb5e..aced97e910 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,6 +1251,7 @@ let clos_whd_flags flgs env sigma t =
let nf_beta = clos_norm_flags CClosure.beta
let nf_betaiota = clos_norm_flags CClosure.betaiota
let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
+let nf_zeta = clos_norm_flags CClosure.zeta
let nf_all env sigma =
clos_norm_flags CClosure.all env sigma
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c0ff6723f6..41de779414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -171,6 +171,7 @@ val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
val nf_beta : reduction_function
val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
+val nf_zeta : reduction_function
val nf_all : reduction_function
val nf_evar : evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 7e43c5e41d..62ad296ecb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma =
subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
| Fix ((_,i),(_,tys,_)) -> tys.(i)
| CoFix (i,(_,tys,_)) -> tys.(i)
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
| App(f,args) ->
@@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma =
let dom = sort_of env t in
let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
Typeops.sort_of_product env dom rang
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
| App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t =
let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
if not (is_impredicative_set env) &&
s2 == InSet && sort_family_of env t == InType then InType else s2
- | App(f,args) when is_template_polymorphic env sigma f ->
+ | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
if truncation_style then InType else
let t = type_of_global_reference_knowing_parameters env f args in
Sorts.family (sort_of_atomic_type env sigma t args)
| App(f,args) ->
Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ -> retype_error NotAType
- | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType
+ | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType
| _ ->
Sorts.family (decomp_sort env sigma (type_of env t))
in sort_family_of env t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8911a2f343..4ec8569dd8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1135,8 +1135,8 @@ let fold_commands cl env sigma c =
let cbv_norm_flags flags env sigma t =
cbv_norm (create_cbv_infos flags env sigma) t
-let cbv_beta = cbv_norm_flags beta empty_env
-let cbv_betaiota = cbv_norm_flags betaiota empty_env
+let cbv_beta = cbv_norm_flags beta
+let cbv_betaiota = cbv_norm_flags betaiota
let cbv_betadeltaiota env sigma = cbv_norm_flags all env sigma
let compute = cbv_betadeltaiota
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index bf38c30a1f..0887d0efd3 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -69,8 +69,8 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function
(** Call by value strategy (uses Closures) *)
val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function
- val cbv_beta : local_reduction_function
- val cbv_betaiota : local_reduction_function
+ val cbv_beta : reduction_function
+ val cbv_betaiota : reduction_function
val cbv_betadeltaiota : reduction_function
val compute : reduction_function (** = [cbv_betadeltaiota] *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index dc3f042431..b5729d7574 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -218,9 +218,6 @@ let judge_of_cast env sigma cj k tj =
sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
uj_type = expected_type }
-let enrich_env env sigma =
- set_universes env @@ Evd.universes sigma
-
let check_fix env sigma pfix =
let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let (idx, (ids, cs, ts)) = pfix in
@@ -277,6 +274,38 @@ let judge_of_letin env name defj typj j =
{ uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
uj_type = subst1 defj.uj_val j.uj_type }
+let check_hyps_inclusion env sigma f x hyps =
+ let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
+ let f x = EConstr.Unsafe.to_constr (f x) in
+ Typeops.check_hyps_inclusion env ~evars f x hyps
+
+let type_of_constant env sigma (c,u) =
+ let open Declarations in
+ let cb = Environ.lookup_constant c env in
+ let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in
+ let u = EInstance.kind sigma u in
+ let ty, csts = Environ.constant_type env (c,u) in
+ let sigma = Evd.add_constraints sigma csts in
+ sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c)))
+
+let type_of_inductive env sigma (ind,u) =
+ let open Declarations in
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let u = EInstance.kind sigma u in
+ let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
+ let sigma = Evd.add_constraints sigma csts in
+ sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind)))
+
+let type_of_constructor env sigma ((ind,_ as ctor),u) =
+ let open Declarations in
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let u = EInstance.kind sigma u in
+ let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
+ let sigma = Evd.add_constraints sigma csts in
+ sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
+
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
let rec execute env sigma cstr =
@@ -297,17 +326,17 @@ let rec execute env sigma cstr =
| Var id ->
sigma, judge_of_variable env id
- | Const (c, u) ->
- let u = EInstance.kind sigma u in
- sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
+ | Const c ->
+ let sigma, ty = type_of_constant env sigma c in
+ sigma, make_judge cstr ty
- | Ind (ind, u) ->
- let u = EInstance.kind sigma u in
- sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
+ | Ind ind ->
+ let sigma, ty = type_of_inductive env sigma ind in
+ sigma, make_judge cstr ty
- | Construct (cstruct, u) ->
- let u = EInstance.kind sigma u in
- sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
+ | Construct ctor ->
+ let sigma, ty = type_of_constructor env sigma ctor in
+ sigma, make_judge cstr ty
| Case (ci,p,c,lf) ->
let sigma, cj = execute env sigma c in
@@ -391,7 +420,6 @@ and execute_recdef env sigma (names,lar,vdef) =
and execute_array env = Array.fold_left_map (execute env)
let check env sigma c t =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
match Evarconv.cumul env sigma j.uj_type t with
| None ->
@@ -401,14 +429,12 @@ let check env sigma c t =
(* Type of a constr *)
let unsafe_type_of env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
j.uj_type
(* Sort of a type *)
let sort_of env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
let sigma, a = type_judgment env sigma j in
sigma, a.utj_type
@@ -416,7 +442,6 @@ let sort_of env sigma c =
(* Try to solve the existential variables by typing *)
let type_of ?(refresh=false) env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
if refresh then
@@ -424,7 +449,6 @@ let type_of ?(refresh=false) env sigma c =
else sigma, j.uj_type
let solve_evars env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
sigma, nf_evar sigma j.uj_val
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index b8830ff4a2..366af0772f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -48,6 +48,8 @@ val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ->
val judge_of_prop : unsafe_judgment
val judge_of_set : unsafe_judgment
+val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array ->
+ evar_map * unsafe_judgment
val judge_of_abstraction : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
val judge_of_product : Environ.env -> Name.t ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:11:32 +0000