aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/fast_typeops.ml36
-rw-r--r--kernel/inductive.ml5
-rw-r--r--kernel/inductive.mli5
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/typeops.ml34
-rw-r--r--pretyping/pretyping.ml15
-rw-r--r--pretyping/retyping.ml6
-rw-r--r--pretyping/termops.ml5
-rw-r--r--pretyping/unification.ml17
9 files changed, 89 insertions, 36 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 8b7230c3b..a68888c8c 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -132,11 +132,10 @@ let type_of_constant_in env cst =
let ar = constant_type_in env cst in
type_of_constant_knowing_parameters_arity env ar [||]
-let judge_of_constant_knowing_parameters env (kn,u as cst) jl =
+let judge_of_constant_knowing_parameters env (kn,u as cst) args =
let cb = lookup_constant kn env in
let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
- let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
- let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
+ let ty, cu = type_of_constant_knowing_parameters env cst args in
let () = check_constraints cu env in
ty
@@ -278,13 +277,14 @@ let judge_of_cast env c ct k expected_type =
the App case of execute; from this constraints, the expected
dynamic constraints of the form u<=v are enforced *)
-(* let judge_of_inductive_knowing_parameters env ind jl = *)
-(* let c = mkInd ind in *)
-(* let (mib,mip) = lookup_mind_specif env ind in *)
-(* check_args env c mib.mind_hyps; *)
-(* let paramstyp = Array.map (fun j -> j.uj_type) jl in *)
-(* let t = in *)
-(* make_judge c t *)
+let judge_of_inductive_knowing_parameters env (ind,u as indu) args =
+ let (mib,mip) as spec = lookup_mind_specif env ind in
+ check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+ let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
+ env (spec,u) args
+ in
+ check_constraints cst env;
+ t
let judge_of_inductive env (ind,u as indu) =
let (mib,mip) = lookup_mind_specif env ind in
@@ -382,7 +382,21 @@ let rec execute env cstr =
(* Lambda calculus operators *)
| App (f,args) ->
let argst = execute_array env args in
- let ft = execute env f in
+ let ft =
+ match kind_of_term f with
+ | Ind ind ->
+ (* Sort-polymorphism of inductive types *)
+ let args = Array.map (fun t -> lazy t) argst in
+ judge_of_inductive_knowing_parameters env ind args
+ | Const cst ->
+ (* Sort-polymorphism of constant *)
+ let args = Array.map (fun t -> lazy t) argst in
+ judge_of_constant_knowing_parameters env cst args
+ | _ ->
+ (* No sort-polymorphism *)
+ execute env f
+ in
+
judge_of_apply env f ft args argst
| Lambda (name,c1,c2) ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9862ffd3e..64a6f1e17 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -237,6 +237,11 @@ let constrained_type_of_inductive env ((mib,mip),u as pind) =
let cst = instantiate_inductive_constraints mib subst in
(ty, cst)
+let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
+ let ty, subst = type_of_inductive_gen env pind args in
+ let cst = instantiate_inductive_constraints mib subst in
+ (ty, cst)
+
let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args =
fst (type_of_inductive_gen env mip args)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a403003e2..a23d170f5 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -44,10 +44,13 @@ val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context
val instantiate_inductive_constraints : mutual_inductive_body -> universe_subst -> constraints
val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
+val constrained_type_of_inductive_knowing_parameters :
+ env -> mind_specif puniverses -> types Lazy.t array -> types constrained
val type_of_inductive : env -> mind_specif puniverses -> types
-val type_of_inductive_knowing_parameters : env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
+val type_of_inductive_knowing_parameters :
+ env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
val elim_sorts : mind_specif -> sorts_family list
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 63bd40681..0a89a0bfd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -632,7 +632,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
let b =
- if cv_pb = CUMUL then leq_constr_univs univs t1 t2
+ if cv_pb == CUMUL then leq_constr_univs univs t1 t2
else eq_constr_univs univs t1 t2
in
if b then Constraint.empty
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09e2fb1d5..9428ace38 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -314,19 +314,21 @@ let judge_of_cast env cj k tj =
the App case of execute; from this constraints, the expected
dynamic constraints of the form u<=v are enforced *)
-(* let judge_of_inductive_knowing_parameters env ind jl = *)
-(* let c = mkInd ind in *)
-(* let (mib,mip) = lookup_mind_specif env ind in *)
-(* check_args env c mib.mind_hyps; *)
-(* let paramstyp = Array.map (fun j -> j.uj_type) jl in *)
-(* let t = in *)
-(* make_judge c t *)
+let judge_of_inductive_knowing_parameters env (ind,u as indu) args =
+ let c = mkIndU indu in
+ let (mib,mip) as spec = lookup_mind_specif env ind in
+ check_hyps_inclusion env c mib.mind_hyps;
+ let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
+ env (spec,u) args
+ in
+ check_constraints cst env;
+ make_judge c t
let judge_of_inductive env (ind,u as indu) =
let c = mkIndU indu in
- let (mib,mip) = lookup_mind_specif env ind in
+ let (mib,mip) as spec = lookup_mind_specif env ind in
check_hyps_inclusion env c mib.mind_hyps;
- let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in
+ let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in
check_constraints cst env;
(make_judge c t)
@@ -424,7 +426,19 @@ let rec execute env cstr =
(* Lambda calculus operators *)
| App (f,args) ->
let jl = execute_array env args in
- let j = execute env f in
+ let j =
+ match kind_of_term f with
+ | Ind ind ->
+ (* Sort-polymorphism of inductive types *)
+ let args = Array.map (fun j -> lazy j.uj_type) jl in
+ judge_of_inductive_knowing_parameters env ind args
+ | Const cst ->
+ (* Sort-polymorphism of constant *)
+ judge_of_constant_knowing_parameters env cst jl
+ | _ ->
+ (* No sort-polymorphism *)
+ execute env f
+ in
judge_of_apply env j jl
| Lambda (name,c1,c2) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7777de514..0ef8d3f3c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -545,6 +545,21 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
resj [hj]
in
let resj = apply_rec env 1 fj candargs args in
+ let resj =
+ match evar_kind_of_term !evdref resj.uj_val with
+ | App (f,args) ->
+ let f = whd_evar !evdref f in
+ begin match kind_of_term f with
+ | Ind _ | Const _
+ when isInd f || has_polymorphic_type (fst (destConst f))
+ ->
+ let sigma = !evdref in
+ let c = mkApp (f,Array.map (whd_evar sigma) args) in
+ let t = Retyping.get_type_of env sigma c in
+ make_judge c (* use this for keeping evars: resj.uj_val *) t
+ | _ -> resj end
+ | _ -> resj
+ in
inh_conv_coerce_to_tycon loc env evdref resj tycon
| GLambda(loc,name,bk,c1,c2) ->
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ccb9420fd..9aecd2d1f 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -154,9 +154,9 @@ let retype ?(polyprop=true) sigma =
| Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
| Prop Null, (Type _ as s) -> s
| Type u1, Type u2 -> Type (Univ.sup u1 u2))
- (* | App(f,args) when isGlobalRef f -> *)
- (* let t = type_of_global_reference_knowing_parameters env f args in *)
- (* sort_of_atomic_type env sigma t args *)
+ | App(f,args) when isGlobalRef 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
| Lambda _ | Fix _ | Construct _ -> retype_error NotAType
| _ -> decomp_sort env sigma (type_of env t)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b3fa53eee..ee7538b22 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -868,7 +868,10 @@ let isGlobalRef c =
| Const _ | Ind _ | Construct _ | Var _ -> true
| _ -> false
-let has_polymorphic_type c = (Global.lookup_constant c).Declarations.const_polymorphic
+let has_polymorphic_type c =
+ match (Global.lookup_constant c).Declarations.const_type with
+ | Declarations.TemplateArity _ -> true
+ | _ -> false
let base_sort_cmp pb s0 s1 =
match (s0,s1) with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f7379b4a0..dbd83bb42 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -734,21 +734,20 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- let evd = sigma in
let res =
- if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n
+ if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
|| subterm_restriction conv_at_top flags then None
else
let sigma, b = match flags.modulo_conv_on_closed_terms with
- | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
- | _ -> constr_cmp cv_pb sigma flags m n in
+ | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
+ | _ -> constr_cmp cv_pb sigma flags m n in
if b then Some sigma
else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
- | Some (cv_id, cv_k), (dl_id, dl_k) ->
- Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
- | None,(dl_id, dl_k) ->
- Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
- then error_cannot_unify env sigma (m, n) else None
+ | Some (cv_id, cv_k), (dl_id, dl_k) ->
+ Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+ | None,(dl_id, dl_k) ->
+ Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
+ then error_cannot_unify env sigma (m, n) else None
in
match res with
| Some sigma -> sigma, ms, es
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:53:06 +0000