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.ml2
-rw-r--r--pretyping/inductiveops.ml5
-rw-r--r--pretyping/pretyping.ml22
-rw-r--r--pretyping/retyping.ml8
-rw-r--r--pretyping/typing.ml58
-rw-r--r--pretyping/typing.mli2
8 files changed, 67 insertions, 33 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 dd38ec6f64..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 ->
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/pretyping.ml b/pretyping/pretyping.ml
index 55817f1b76..cba1533da5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -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/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/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-02 05:20:36 +0000