aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/cic.mli20
-rw-r--r--checker/declarations.ml16
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/indtypes.ml28
-rw-r--r--checker/inductive.ml42
-rw-r--r--checker/inductive.mli4
-rw-r--r--checker/mod_checking.ml35
-rw-r--r--checker/term.ml2
-rw-r--r--checker/typeops.ml51
-rw-r--r--checker/typeops.mli6
10 files changed, 88 insertions, 118 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 380093c57e..d2f785abf3 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -163,14 +163,7 @@ type engagement = ImpredicativeSet
(** {6 Representation of constants (Definition/Axiom) } *)
-type polymorphic_arity = {
- poly_param_levels : Univ.universe option list;
- poly_level : Univ.universe;
-}
-
-type constant_type =
- | NonPolymorphicType of constr
- | PolymorphicArity of rel_context * polymorphic_arity
+type constant_type = constr
(** Inlining level of parameters at functor applications.
This is ignored by the checker. *)
@@ -203,15 +196,6 @@ type recarg =
type wf_paths = recarg Rtree.t
-type monomorphic_inductive_arity = {
- mind_user_arity : constr;
- mind_sort : sorts;
-}
-
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-
type one_inductive_body = {
(** {8 Primitive datas } *)
@@ -219,7 +203,7 @@ type one_inductive_body = {
mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
- mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
+ mind_arity : constr; (** Arity sort and original user arity if monomorphic *)
mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index baf2e57db4..4dd814d575 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -433,6 +433,9 @@ let subst_constant_def sub = function
| Def c -> Def (subst_constr_subst sub c)
| OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+(** Local variables and graph *)
+type universe_context = Univ.LSet.t * Univ.constraints
+
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
| Def c -> Some (force_constr c)
@@ -488,9 +491,8 @@ let eq_wf_paths = Rtree.equal eq_recarg
with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
*)
-let subst_arity sub = function
-| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
-| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+let subst_arity sub s = subst_mps sub s
+
(* TODO: should be changed to non-coping after Term.subst_mps *)
(* NB: we leave bytecode and native code fields untouched *)
@@ -499,14 +501,6 @@ let subst_const_body sub cb =
const_body = subst_constant_def sub cb.const_body;
const_type = subst_arity sub cb.const_type }
-let subst_arity sub = function
-| Monomorphic s ->
- Monomorphic {
- mind_user_arity = subst_mps sub s.mind_user_arity;
- mind_sort = s.mind_sort;
- }
-| Polymorphic s as x -> x
-
let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
mind_consnrealdecls = mbp.mind_consnrealdecls;
diff --git a/checker/environ.ml b/checker/environ.ml
index eb084a9105..79234e9e20 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -77,7 +77,7 @@ let push_rec_types (lna,typarray,_) env =
(* Universe constraints *)
let add_constraints c env =
- if c == empty_constraint then
+ if c == Constraint.empty then
env
else
let s = env.env_stratification in
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index a642324429..5927e16338 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -139,14 +139,12 @@ let typecheck_arity env params inds =
let nparamargs = rel_context_nhyps params in
let nparamdecls = rel_context_length params in
let check_arity arctxt = function
- Monomorphic mar ->
- let ar = mar.mind_user_arity in
- let _ = infer_type env ar in
- conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar;
- ar
- | Polymorphic par ->
- check_polymorphic_arity env params par;
- it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in
+ mar ->
+ let _ = infer_type env mar in
+ mar in
+ (* | Polymorphic par -> *)
+ (* check_polymorphic_arity env params par; *)
+ (* it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in *)
let env_arities =
Array.fold_left
(fun env_ar ind ->
@@ -178,11 +176,11 @@ let typecheck_arity env params inds =
let check_predicativity env s small level =
match s, engagement env with
Type u, _ ->
- let u' = fresh_local_univ () in
- let cst =
- merge_constraints (enforce_leq u u' empty_constraint)
- (universes env) in
- if not (check_leq cst level u') then
+ (* let u' = fresh_local_univ () in *)
+ (* let cst = *)
+ (* merge_constraints (enforce_leq u u' empty_constraint) *)
+ (* (universes env) in *)
+ if not (check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
| Prop Pos, Some ImpredicativeSet -> ()
| Prop Pos, _ ->
@@ -191,8 +189,8 @@ let check_predicativity env s small level =
let sort_of_ind = function
- Monomorphic mar -> mar.mind_sort
- | Polymorphic par -> Type par.poly_level
+ mar -> snd (destArity mar)
+ (* | Polymorphic par -> Type par.poly_level *)
let all_sorts = [InProp;InSet;InType]
let small_sorts = [InProp;InSet]
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e6a24f705d..b32379b35e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -161,11 +161,11 @@ let rec make_subst env = function
(* (actualize_decl_level), then to the conclusion of the arity (via *)
(* the substitution) *)
let ctx,subst = make_subst env (sign, exp, []) in
- if polymorphism_on_non_applied_parameters then
- let s = fresh_local_univ () in
- let t = actualize_decl_level env (Type s) t in
- (na,None,t)::ctx, cons_subst u s subst
- else
+ (* if polymorphism_on_non_applied_parameters then *)
+ (* let s = fresh_local_univ () in *)
+ (* let t = actualize_decl_level env (Type s) t in *)
+ (* (na,None,t)::ctx, cons_subst u s subst *)
+ (* else *)
d::ctx, subst
| sign, [], _ ->
(* Uniform parameters are exhausted *)
@@ -173,23 +173,21 @@ let rec make_subst env = function
| [], _, _ ->
assert false
-let instantiate_universes env ctx ar argsorts =
- let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
- let level = subst_large_constraints subst ar.poly_level in
- ctx,
- if is_type0m_univ level then Prop Null
- else if is_type0_univ level then Prop Pos
- else Type level
+(* let instantiate_universes env ctx ar argsorts = *)
+(* let args = Array.to_list argsorts in *)
+(* let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *)
+(* let level = subst_large_constraints subst ar.poly_level in *)
+(* ctx, *)
+(* if is_type0m_univ level then Prop Null *)
+(* else if is_type0_univ level then Prop Pos *)
+(* else Type level *)
let type_of_inductive_knowing_parameters env mip paramtyps =
- match mip.mind_arity with
- | Monomorphic s ->
- s.mind_user_arity
- | Polymorphic ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
- mkArity (List.rev ctx,s)
+ mip.mind_arity
+ (* | Polymorphic ar -> *)
+ (* let ctx = List.rev mip.mind_arity_ctxt in *)
+ (* let ctx,s = instantiate_universes env ctx ar paramtyps in *)
+ (* mkArity (List.rev ctx,s) *)
(* Type of a (non applied) inductive type *)
@@ -236,9 +234,7 @@ let error_elim_expln kp ki =
(* Get type of inductive, with parameters instantiated *)
let inductive_sort_family mip =
- match mip.mind_arity with
- | Monomorphic s -> family_of_sort s.mind_sort
- | Polymorphic _ -> InType
+ family_of_sort (snd (destArity mip.mind_arity))
let mind_arity mip =
mip.mind_arity_ctxt, inductive_sort_family mip
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 0e9b9ccf34..082bdae196 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -54,8 +54,8 @@ val type_of_inductive_knowing_parameters :
val max_inductive_sort : sorts array -> Univ.universe
-val instantiate_universes : env -> rel_context ->
- polymorphic_arity -> constr array -> rel_context * sorts
+(* val instantiate_universes : env -> rel_context -> *)
+(* inductive_arity -> constr array -> rel_context * sorts *)
(***************************************************************)
(* Debug *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index add9935816..4f4cc5560b 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -14,31 +14,30 @@ open Environ
(** {6 Checking constants } *)
-let refresh_arity ar =
- let ctxt, hd = decompose_prod_assum ar in
- match hd with
- Sort (Type u) when not (Univ.is_univ_variable u) ->
- let u' = Univ.fresh_local_univ() in
- mkArity (ctxt,Type u'),
- Univ.enforce_leq u u' Univ.empty_constraint
- | _ -> ar, Univ.empty_constraint
+(* let refresh_arity ar = *)
+(* let ctxt, hd = decompose_prod_assum ar in *)
+(* match hd with *)
+(* Sort (Type u) when not (Univ.is_univ_variable u) -> *)
+(* let u' = Univ.fresh_local_univ() in *)
+(* mkArity (ctxt,Type u'), *)
+(* Univ.enforce_leq u u' Univ.empty_constraint *)
+(* | _ -> ar, Univ.empty_constraint *)
let check_constant_declaration env kn cb =
Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn);
(* let env = add_constraints cb.const_constraints env in*)
(match cb.const_type with
- NonPolymorphicType ty ->
- let ty, cu = refresh_arity ty in
- let envty = add_constraints cu env in
- let _ = infer_type envty ty in
- (match body_of_constant cb with
+ ty ->
+ let env' = add_constraints cb.const_constraints env in
+ let _ = infer_type env' ty in
+ (match body_of_constant cb with
| Some bd ->
- let j = infer env bd in
- conv_leq envty j ty
+ let j = infer env' bd in
+ conv_leq env' j ty
| None -> ())
- | PolymorphicArity(ctxt,par) ->
- let _ = check_ctxt env ctxt in
- check_polymorphic_arity env ctxt par);
+ (* | PolymorphicArity(ctxt,par) -> *)
+ (* let _ = check_ctxt env ctxt in *)
+ (* check_polymorphic_arity env ctxt par *));
add_constant kn cb env
diff --git a/checker/term.ml b/checker/term.ml
index ea81f5dab2..67d3803366 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -347,7 +347,7 @@ let compare_sorts s1 s2 = match s1, s2 with
| Pos, Null -> false
| Null, Pos -> false
end
-| Type u1, Type u2 -> Universe.equal u1 u2
+| Type u1, Type u2 -> Universe.eq u1 u2
| Prop _, Type _ -> false
| Type _, Prop _ -> false
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 95753769df..6a705b1986 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -67,12 +67,11 @@ let judge_of_relative env n =
(* Type of constants *)
let type_of_constant_knowing_parameters env t paramtyps =
- match t with
- | NonPolymorphicType t -> t
- | PolymorphicArity (sign,ar) ->
- let ctx = List.rev sign in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
- mkArity (List.rev ctx,s)
+ t
+ (* | PolymorphicArity (sign,ar) -> *)
+ (* let ctx = List.rev sign in *)
+ (* let ctx,s = instantiate_universes env ctx ar paramtyps in *)
+ (* mkArity (List.rev ctx,s) *)
let type_of_constant_type env t =
type_of_constant_knowing_parameters env t [||]
@@ -220,14 +219,14 @@ let type_fixpoint env lna lar lbody vdefj =
(************************************************************************)
-let refresh_arity env ar =
- let ctxt, hd = decompose_prod_assum ar in
- match hd with
- Sort (Type u) when not (is_univ_variable u) ->
- let u' = fresh_local_univ() in
- let env' = add_constraints (enforce_leq u u' empty_constraint) env in
- env', mkArity (ctxt,Type u')
- | _ -> env, ar
+(* let refresh_arity env ar = *)
+(* let ctxt, hd = decompose_prod_assum ar in *)
+(* match hd with *)
+(* Sort (Type u) when not (is_univ_variable u) -> *)
+(* let u' = fresh_local_univ() in *)
+(* let env' = add_constraints (enforce_leq u u' empty_constraint) env in *)
+(* env', mkArity (ctxt,Type u') *)
+(* | _ -> env, ar *)
(* The typing machine. *)
@@ -282,7 +281,7 @@ let rec execute env cstr =
(* /!\ c2 can be an inferred type => refresh
(but the pushed type is still c2) *)
let _ =
- let env',c2' = refresh_arity env c2 in
+ let env',c2' = (* refresh_arity env *) env, c2 in
let _ = execute_type env' c2' in
judge_of_cast env' (c1,j1) DEFAULTcast c2' in
let env1 = push_rel (name,Some c1,c2) env in
@@ -365,14 +364,14 @@ let check_kind env ar u =
if snd (dest_prod env ar) = Sort(Type u) then ()
else failwith "not the correct sort"
-let check_polymorphic_arity env params par =
- let pl = par.poly_param_levels in
- let rec check_p env pl params =
- match pl, params with
- Some u::pl, (na,None,ty)::params ->
- check_kind env ty u;
- check_p (push_rel (na,None,ty) env) pl params
- | None::pl,d::params -> check_p (push_rel d env) pl params
- | [], _ -> ()
- | _ -> failwith "check_poly: not the right number of params" in
- check_p env pl (List.rev params)
+(* let check_polymorphic_arity env params par = *)
+(* let pl = par.poly_param_levels in *)
+(* let rec check_p env pl params = *)
+(* match pl, params with *)
+(* Some u::pl, (na,None,ty)::params -> *)
+(* check_kind env ty u; *)
+(* check_p (push_rel (na,None,ty) env) pl params *)
+(* | None::pl,d::params -> check_p (push_rel d env) pl params *)
+(* | [], _ -> () *)
+(* | _ -> failwith "check_poly: not the right number of params" in *)
+(* check_p env pl (List.rev params) *)
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 92535606f9..97d79fe54a 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -16,8 +16,8 @@ open Environ
val infer : env -> constr -> constr
val infer_type : env -> constr -> sorts
val check_ctxt : env -> rel_context -> env
-val check_polymorphic_arity :
- env -> rel_context -> polymorphic_arity -> unit
+(* val check_polymorphic_arity : *)
+(* env -> rel_context -> polymorphic_arity -> unit *)
-val type_of_constant_type : env -> constant_type -> constr
+val type_of_constant_type : env -> constr -> constr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-30 08:48:14 +0000