aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/cic.mli20
-rw-r--r--checker/closure.ml49
-rw-r--r--checker/closure.mli2
-rw-r--r--checker/declarations.ml16
-rw-r--r--checker/declarations.mli3
-rw-r--r--checker/environ.ml27
-rw-r--r--checker/environ.mli4
-rw-r--r--checker/indtypes.ml22
-rw-r--r--checker/inductive.ml24
-rw-r--r--checker/mod_checking.ml27
-rw-r--r--checker/modops.ml22
-rw-r--r--checker/print.ml4
-rw-r--r--checker/reduction.ml65
-rw-r--r--checker/subtyping.ml102
-rw-r--r--checker/term.ml20
-rw-r--r--checker/typeops.ml21
-rw-r--r--checker/univ.ml42
-rw-r--r--checker/univ.mli2
-rw-r--r--checker/values.ml16
19 files changed, 166 insertions, 322 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index a890f2cef5..17259bb438 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -33,11 +33,10 @@ open Names
(** {6 The sorts of CCI. } *)
-type contents = Pos | Null
-
type sorts =
- | Prop of contents (** Prop and Set *)
- | Type of Univ.universe (** Type *)
+ | Prop
+ | Set
+ | Type of Univ.universe
(** {6 The sorts family of CCI. } *)
@@ -203,16 +202,6 @@ type inline = int option
(** A constant can have no body (axiom/parameter), or a
transparent body, or an opaque one *)
-(** Projections are a particular kind of constant:
- always transparent. *)
-
-type projection_body = {
- proj_ind : inductive;
- proj_npars : int;
- proj_arg : int;
- proj_type : constr; (* Type under params *)
-}
-
type constant_def =
| Undef of inline
| Def of constr_substituted
@@ -231,6 +220,7 @@ type typing_flags = {
points are assumed to be total. *)
check_universes : bool; (** If [false] universe constraints are not checked *)
conv_oracle : oracle; (** Unfolding strategies for conversion *)
+ share_reduction : bool; (** Use by-need reduction algorithm *)
}
type constant_body = {
@@ -255,7 +245,7 @@ type wf_paths = recarg Rtree.t
type record_info =
| NotRecord
| FakeRecord
-| PrimRecord of (Id.t * Constant.t array * projection_body array) array
+| PrimRecord of (Id.t * Label.t array * constr array) array
type regular_inductive_arity = {
mind_user_arity : constr;
diff --git a/checker/closure.ml b/checker/closure.ml
index 2dcc1a9840..5706011607 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -273,7 +273,7 @@ let update v1 (no,t) =
type stack_member =
| Zapp of fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * Projection.t
+ | Zproj of Projection.Repr.t
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -497,8 +497,8 @@ let rec zip m stk =
| ZcaseT(ci,p,br,e)::s ->
let t = FCaseT(ci, p, m, br, e) in
zip {norm=neutr m.norm; term=t} s
- | Zproj (i,j,cst) :: s ->
- zip {norm=neutr m.norm; term=FProj (cst,m)} s
+ | Zproj p :: s ->
+ zip {norm=neutr m.norm; term=FProj (Projection.make p true,m)} s
| Zfix(fx,par)::s ->
zip fx (par @ append_stack [|m|] s)
| Zshift(n)::s ->
@@ -618,21 +618,25 @@ let drop_parameters depth n argstk =
let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
- match mib.mind_record with
- | PrimRecord info when mib.mind_finite <> CoFinite ->
- let (_, projs, pbs) = info.(snd ind) in
- (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
- arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
- let pars = mib.mind_nparams in
- let right = fapp_stack (f, s') in
- let (depth, args, s) = strip_update_shift_app m s in
- (** Try to drop the params, might fail on partially applied constructors. *)
- let argss = try_drop_parameters depth pars args in
- let hstack =
- Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
- term = FProj (Projection.make p false, right) }) projs in
- argss, [Zapp hstack]
- | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+ (* disallow eta-exp for non-primitive records *)
+ if not (mib.mind_finite == BiFinite) then raise Not_found;
+ match Declarations.inductive_make_projections ind mib with
+ | Some projs ->
+ (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+ arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+ let pars = mib.mind_nparams in
+ let right = fapp_stack (f, s') in
+ let (depth, args, s) = strip_update_shift_app m s in
+ (** Try to drop the params, might fail on partially applied constructors. *)
+ let argss = try_drop_parameters depth pars args in
+ let hstack =
+ Array.map (fun p ->
+ { norm = Red; (* right can't be a constructor though *)
+ term = FProj (Projection.make p false, right) })
+ projs
+ in
+ argss, [Zapp hstack]
+ | None -> raise Not_found (* disallow eta-exp for non-primitive records *)
let rec project_nth_arg n argstk =
match argstk with
@@ -669,8 +673,7 @@ let contract_fix_vect fix =
(subs_cons(Array.init nfix make_body, env), thisbody)
let unfold_projection env p =
- let pb = lookup_projection p env in
- Zproj (pb.proj_npars, pb.proj_arg, p)
+ Zproj (Projection.repr p)
(*********************************************************************)
(* A machine that inspects the head of a term until it finds an
@@ -748,9 +751,9 @@ let rec knr info m stk =
let stk' = par @ append_stack [|rarg|] s in
let (fxe,fxbd) = contract_fix_vect fx.term in
knit info fxe fxbd stk'
- | (depth, args, Zproj (n, m, cst)::s) ->
- let rargs = drop_parameters depth n args in
- let rarg = project_nth_arg m rargs in
+ | (depth, args, Zproj p::s) ->
+ let rargs = drop_parameters depth (Projection.Repr.npars p) args in
+ let rarg = project_nth_arg (Projection.Repr.arg p) rargs in
kni info rarg s
| (_,args,s) -> (m,args@s))
| FCoFix _ when red_set info.i_flags fIOTA ->
diff --git a/checker/closure.mli b/checker/closure.mli
index 49b07f730d..cec785699d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -103,7 +103,7 @@ type fterm =
type stack_member =
| Zapp of fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * Projection.t
+ | Zproj of Projection.Repr.t
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index a744a02279..0540227ccb 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -214,11 +214,7 @@ let rec map_kn f f' c =
match c with
| Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
| Proj (p,t) ->
- let p' =
- Projection.map (fun kn ->
- try fst (f' kn Univ.Instance.empty)
- with No_subst -> kn) p
- in
+ let p' = Projection.map f p in
let t' = func t in
if p' == p && t' == t then c
else Proj (p', t')
@@ -495,6 +491,16 @@ let eq_recarg r1 r2 = match r1, r2 with
let eq_wf_paths = Rtree.equal eq_recarg
+let inductive_make_projections ind mib =
+ match mib.mind_record with
+ | NotRecord | FakeRecord -> None
+ | PrimRecord infos ->
+ let projs = Array.mapi (fun proj_arg lab ->
+ Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+ (pi2 infos.(snd ind))
+ in
+ Some projs
+
(**********************************************************************)
(* Representation of mutual inductive types in the kernel *)
(*
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 7458b3e0b0..ce852644ef 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -25,6 +25,9 @@ val dest_subterms : wf_paths -> wf_paths list array
val eq_recarg : recarg -> recarg -> bool
val eq_wf_paths : wf_paths -> wf_paths -> bool
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+ Names.Projection.Repr.t array option
+
(* Modules *)
val empty_delta_resolver : delta_resolver
diff --git a/checker/environ.ml b/checker/environ.ml
index ba1eb0ddb4..74cf237763 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,7 +7,6 @@ open Declarations
type globals = {
env_constants : constant_body Cmap_env.t;
- env_projections : projection_body Cmap_env.t;
env_inductives : mutual_inductive_body Mindmap_env.t;
env_inductives_eq : KerName.t KNmap.t;
env_modules : module_body MPmap.t;
@@ -35,7 +34,6 @@ let empty_oracle = {
let empty_env = {
env_globals =
{ env_constants = Cmap_env.empty;
- env_projections = Cmap_env.empty;
env_inductives = Mindmap_env.empty;
env_inductives_eq = KNmap.empty;
env_modules = MPmap.empty;
@@ -166,9 +164,6 @@ let evaluable_constant cst env =
try let _ = constant_value env (cst, Univ.Instance.empty) in true
with Not_found | NotEvaluableConst _ -> false
-let lookup_projection p env =
- Cmap_env.find (Projection.constant p) env.env_globals.env_projections
-
(* Mutual Inductives *)
let scrape_mind env kn=
try
@@ -191,14 +186,6 @@ let add_mind kn mib env =
Printf.ksprintf anomaly ("Inductive %s is already defined.")
(MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
- let new_projections = match mib.mind_record with
- | NotRecord | FakeRecord -> env.env_globals.env_projections
- | PrimRecord projs ->
- Array.fold_left (fun accu (id, kns, pbs) ->
- Array.fold_left2 (fun accu kn pb ->
- Cmap_env.add kn pb accu) accu kns pbs)
- env.env_globals.env_projections projs
- in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
let new_inds_eq = if KerName.equal kn1 kn2 then
env.env_globals.env_inductives_eq
@@ -207,10 +194,22 @@ let add_mind kn mib env =
let new_globals =
{ env.env_globals with
env_inductives = new_inds;
- env_projections = new_projections;
env_inductives_eq = new_inds_eq} in
{ env with env_globals = new_globals }
+let lookup_projection p env =
+ let mind,i = Projection.inductive p in
+ let mib = lookup_mind mind env in
+ match mib.mind_record with
+ | NotRecord | FakeRecord -> CErrors.anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+ | PrimRecord infos ->
+ let _,labs,typs = infos.(i) in
+ let parg = Projection.arg p in
+ if not (Label.equal labs.(parg) (Projection.label p))
+ then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect label on projection")
+ else if not (Int.equal mib.mind_nparams (Projection.npars p))
+ then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect param number on projection")
+ else typs.(parg)
(* Modules *)
diff --git a/checker/environ.mli b/checker/environ.mli
index acb29d7d2d..af1b2a6228 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -5,7 +5,6 @@ open Cic
type globals = {
env_constants : constant_body Cmap_env.t;
- env_projections : projection_body Cmap_env.t;
env_inductives : mutual_inductive_body Mindmap_env.t;
env_inductives_eq : KerName.t KNmap.t;
env_modules : module_body MPmap.t;
@@ -58,7 +57,8 @@ exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> Constant.t puniverses -> constr
val evaluable_constant : Constant.t -> env -> bool
-val lookup_projection : Projection.t -> env -> projection_body
+(** NB: here in the checker we check the inferred info (npars, label) *)
+val lookup_projection : Projection.t -> env -> constr
(* Inductives *)
val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 916934a81f..8f11e01c33 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t =
(* Prop and Set are small *)
let is_small_sort = function
- | Prop _ -> true
+ | Prop | Set -> true
| _ -> false
let is_logic_sort = function
-| Prop Null -> true
+| Prop -> true
| _ -> false
(* [infos] is a sequence of pair [islogic,issmall] for each type in
@@ -186,10 +186,10 @@ let check_predicativity env s small level =
(* (universes env) in *)
if not (Univ.check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
- | Prop Pos, ImpredicativeSet -> ()
- | Prop Pos, _ ->
+ | Set, ImpredicativeSet -> ()
+ | Set, _ ->
if not small then failwith "impredicative Set inductive type"
- | Prop Null,_ -> ()
+ | Prop,_ -> ()
let sort_of_ind = function
@@ -221,7 +221,7 @@ let allowed_sorts issmall isunit s =
-let compute_elim_sorts env_ar params mib arity lc =
+let compute_elim_sorts env_ar params arity lc =
let inst = extended_rel_list 0 params in
let env_params = push_rel_context params env_ar in
let lc = Array.map
@@ -239,7 +239,7 @@ let compute_elim_sorts env_ar params mib arity lc =
allowed_sorts small unit s
-let typecheck_one_inductive env params mib mip =
+let typecheck_one_inductive env params mip =
(* mind_typename and mind_consnames not checked *)
(* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *)
(* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *)
@@ -256,7 +256,7 @@ let typecheck_one_inductive env params mib mip =
Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
(* mind_kelim: checked by positivity criterion ? *)
let sorts =
- compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in
+ compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in
let reject_sort s = not (List.mem_f family_equal s sorts) in
if List.exists reject_sort mip.mind_kelim then
failwith "elimination not allowed";
@@ -355,7 +355,7 @@ let lambda_implicit_lift n a =
(* This removes global parameters of the inductive types in lc (for
nested inductive types only ) *)
-let abstract_mind_lc env ntyps npars lc =
+let abstract_mind_lc ntyps npars lc =
if npars = 0 then
lc
else
@@ -448,7 +448,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
let auxntyp = mib.mind_ntypes in
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
(* The nested inductive type with parameters removed *)
- let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
+ let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in
(* Extends the environment with a variable corresponding to
the inductive def *)
let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in
@@ -625,7 +625,7 @@ let check_inductive env kn mib =
(* - check arities *)
let env_ar = typecheck_arity env0 params mib.mind_packets in
(* - check constructor types *)
- Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+ Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets;
(* check the inferred subtyping relation *)
let () =
match mib.mind_universes with
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e1c6b135d7..d15380643f 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -101,7 +101,7 @@ let instantiate_params full t u args sign =
substl subs ty
let full_inductive_instantiate mib u params sign =
- let dummy = Prop Null in
+ let dummy = Prop in
let t = mkArity (Term.subst_instance_context u sign,dummy) in
fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
@@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0)
let sort_as_univ = function
| Type u -> u
-| Prop Null -> Univ.type0m_univ
-| Prop Pos -> Univ.type0_univ
+| Prop -> Univ.type0m_univ
+| Set -> Univ.type0_univ
(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
@@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts =
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
- if Univ.is_type0m_univ level then Prop Null
+ if Univ.is_type0m_univ level then Prop
(* Non singleton type not containing types are interpretable in Set *)
- else if Univ.is_type0_univ level then Prop Pos
+ else if Univ.is_type0_univ level then Set
(* This is a Type with constraints *)
else Type level
in
@@ -226,8 +226,8 @@ let type_of_inductive env mip =
(* The max of an array of universes *)
let cumulate_constructor_univ u = function
- | Prop Null -> u
- | Prop Pos -> Univ.sup Univ.type0_univ u
+ | Prop -> u
+ | Set -> Univ.sup Univ.type0_univ u
| Type u' -> Univ.sup u u'
let max_inductive_sort =
@@ -797,7 +797,7 @@ let rec subterm_specif renv stack t =
| Lambda (x,a,b) ->
assert (l=[]);
- let spec,stack' = extract_stack renv a stack in
+ let spec,stack' = extract_stack stack in
subterm_specif (push_var renv (x,a,spec)) stack' b
(* Metas and evars are considered OK *)
@@ -813,7 +813,7 @@ and stack_element_specif = function
|SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
|SArg x -> x
-and extract_stack renv a = function
+and extract_stack = function
| [] -> Lazy.from_val Not_subterm , []
| h::t -> stack_element_specif h, t
@@ -845,7 +845,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
let error_partial_apply renv fx =
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
-let filter_stack_domain env ci p stack =
+let filter_stack_domain env p stack =
let absctx, ar = dest_lam_assum env p in
(* Optimization: if the predicate is not dependent, no restriction is needed
and we avoid building the recargs tree. *)
@@ -925,7 +925,7 @@ let check_one_fix renv recpos trees def =
let case_spec = branches_specif renv
(lazy_subterm_specif renv [] c_0) ci in
let stack' = push_stack_closures renv l stack in
- let stack' = filter_stack_domain renv.env ci p stack' in
+ let stack' = filter_stack_domain renv.env p stack' in
Array.iteri (fun k br' ->
let stack_br = push_stack_args case_spec.(k) stack' in
check_rec_call renv stack_br br') lrest
@@ -968,7 +968,7 @@ let check_one_fix renv recpos trees def =
| Lambda (x,a,b) ->
assert (l = []);
check_rec_call renv [] a ;
- let spec, stack' = extract_stack renv a stack in
+ let spec, stack' = extract_stack stack in
check_rec_call (push_var renv (x,a,spec)) stack' b
| Prod (x,a,b) ->
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ca9581167f..6b2af71f33 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -2,7 +2,6 @@ open Pp
open Util
open Names
open Cic
-open Term
open Reduction
open Typeops
open Indtypes
@@ -13,17 +12,6 @@ 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 ul = Univ.Level.make DirPath.empty 1 in
- let u' = Univ.Universe.make ul in
- let cst = Univ.enforce_leq u u' Univ.empty_constraint in
- let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
- mkArity (ctxt,Prop Null), ctx
- | _ -> ar, Univ.ContextSet.empty
-
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn);
(** Locally set the oracle for further typechecking *)
@@ -37,18 +25,13 @@ let check_constant_declaration env kn cb =
let ctx = Univ.AUContext.repr auctx in
push_context ~strict:false ctx env
in
- let envty, ty =
- let ty = cb.const_type in
- let ty', cu = refresh_arity ty in
- let envty = push_context_set cu env' in
- let _ = infer_type envty ty' in
- envty, ty
- in
- let () =
+ let ty = cb.const_type in
+ let _ = infer_type env' ty in
+ let () =
match body_of_constant cb with
| Some bd ->
- let j = infer envty bd in
- conv_leq envty j ty
+ let j = infer env' bd in
+ conv_leq env' j ty
| None -> ()
in
let env =
diff --git a/checker/modops.ml b/checker/modops.ml
index c7ad0977ac..b92d7bbf1f 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -80,7 +80,7 @@ and add_module mb env =
let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
-let strengthen_const mp_from l cb resolver =
+let strengthen_const mp_from l cb =
match cb.const_body with
| Def _ -> cb
| _ ->
@@ -104,34 +104,34 @@ and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a ge
match mb.mod_type with
| MoreFunctor _ -> mb
| NoFunctor sign ->
- let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
+ let resolve_out,sign_out = strengthen_sig mp_from sign mp_to
in
{ mb with
mod_expr = mk_expr mp_to;
mod_type = NoFunctor sign_out;
mod_delta = resolve_out }
-and strengthen_sig mp_from sign mp_to resolver =
+and strengthen_sig mp_from sign mp_to =
match sign with
| [] -> empty_delta_resolver,[]
| (l,SFBconst cb) :: rest ->
- let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+ let item' = l,SFBconst (strengthen_const mp_from l cb) in
+ let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
resolve_out,item'::rest'
| (_,SFBmind _ as item):: rest ->
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+ let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
resolve_out,item::rest'
| (l,SFBmodule mb) :: rest ->
let mp_from' = MPdot (mp_from,l) in
let mp_to' = MPdot(mp_to,l) in
let mb_out = strengthen_mod mp_from' mp_to' mb in
let item' = l,SFBmodule (mb_out) in
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+ let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
- item':: rest'
- | (l,SFBmodtype mty as item) :: rest ->
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out,item::rest'
+ item':: rest'
+ | (_,SFBmodtype _ as item) :: rest ->
+ let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
+ resolve_out,item::rest'
let strengthen mtb mp =
strengthen_body ignore mtb.mod_mp mp mtb
diff --git a/checker/print.ml b/checker/print.ml
index fc9cd687e8..247c811f80 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -57,8 +57,8 @@ let print_pure_constr fmt csr =
fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
and pp_sort fmt = function
- | Prop(Pos) -> pp_print_string fmt "Set"
- | Prop(Null) -> pp_print_string fmt "Prop"
+ | Set -> pp_print_string fmt "Set"
+ | Prop -> pp_print_string fmt "Prop"
| Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
and pp_name fmt = function
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 4e508dc772..d36c0ef2c9 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -43,7 +43,7 @@ let compare_stack_shape stk1 stk2 =
| (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
| (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
| (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
- | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+ | (Zproj p1::s1, Zproj p2::s2) ->
Int.equal bal 0 && compare_rec 0 s1 s2
| ((ZcaseT(c1,_,_,_))::s1,
(ZcaseT(c2,_,_,_))::s2) ->
@@ -55,7 +55,7 @@ let compare_stack_shape stk1 stk2 =
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
- | Zlproj of Names.Projection.t * lift
+ | Zlproj of Names.Projection.Repr.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -74,8 +74,8 @@ let pure_stack lfts stk =
| (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
| (Zapp a, (l,pstk)) ->
(l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
- | (Zproj (n,m,c), (l,pstk)) ->
- (l, Zlproj (c,l)::pstk)
+ | (Zproj p, (l,pstk)) ->
+ (l, Zlproj (p,l)::pstk)
| (Zfix(fx,a),(l,pstk)) ->
let (lfx,pa) = pure_rec l a in
(l, Zlfix((lfx,fx),pa)::pstk)
@@ -133,7 +133,7 @@ let convert_universes univ u u' =
if Univ.Instance.check_eq univ u u' then ()
else raise NotConvertible
-let compare_stacks f fmind lft1 stk1 lft2 stk2 =
+let compare_stacks f fmind fproj lft1 stk1 lft2 stk2 =
let rec cmp_rec pstk1 pstk2 =
match (pstk1,pstk2) with
| (z1::s1, z2::s2) ->
@@ -143,10 +143,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
f fx1 fx2; cmp_rec a1 a2
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
- if not (Names.Constant.UserOrd.equal
- (Names.Projection.constant c1)
- (Names.Projection.constant c2)) then
- raise NotConvertible
+ if not (fproj c1 c2) then
+ raise NotConvertible
| (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
if not (fmind ci1.ci_ind ci2.ci_ind) then
raise NotConvertible;
@@ -210,29 +208,26 @@ let convert_constructors
let sort_cmp env univ pb s0 s1 =
match (s0,s1) with
- | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
- | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
- | (Prop c1, Type u) ->
+ | Prop, Prop | Set, Set -> ()
+ | Prop, (Set | Type _) | Set, Type _ ->
+ if not (pb = CUMUL) then raise NotConvertible
+ | Type u1, Type u2 ->
+ (** FIXME: handle type-in-type option here *)
+ if (* snd (engagement env) == StratifiedType && *)
+ not
(match pb with
- CUMUL -> ()
- | _ -> raise NotConvertible)
- | (Type u1, Type u2) ->
- (** FIXME: handle type-in-type option here *)
- if (* snd (engagement env) == StratifiedType && *)
- not
- (match pb with
- | CONV -> Univ.check_eq univ u1 u2
- | CUMUL -> Univ.check_leq univ u1 u2)
- then begin
- if !Flags.debug then begin
- let op = match pb with CONV -> "=" | CUMUL -> "<=" in
- Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
- str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
- ++ Univ.pr_universes univ)
- end;
- raise NotConvertible
- end
- | (_, _) -> raise NotConvertible
+ | CONV -> Univ.check_eq univ u1 u2
+ | CUMUL -> Univ.check_leq univ u1 u2)
+ then begin
+ if !Flags.debug then begin
+ let op = match pb with CONV -> "=" | CUMUL -> "<=" in
+ Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+ str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+ ++ Univ.pr_universes univ)
+ end;
+ raise NotConvertible
+ end
+ | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible
let rec no_arg_available = function
| [] -> true
@@ -260,7 +255,7 @@ let rec no_case_available = function
| Zupdate _ :: stk -> no_case_available stk
| Zshift _ :: stk -> no_case_available stk
| Zapp _ :: stk -> no_case_available stk
- | Zproj (_,_,_) :: _ -> false
+ | Zproj _ :: _ -> false
| ZcaseT _ :: _ -> false
| Zfix _ :: _ -> true
@@ -303,6 +298,10 @@ let eq_table_key univ =
Constant.UserOrd.equal c1 c2 &&
Univ.Instance.check_eq univ u1 u2)
+let proj_equiv_infos infos p1 p2 =
+ Int.equal (Projection.Repr.arg p1) (Projection.Repr.arg p2) &&
+ mind_equiv (infos_env infos) (Projection.Repr.inductive p1) (Projection.Repr.inductive p2)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -526,7 +525,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
and convert_stacks univ infos lft1 lft2 stk1 stk2 =
compare_stacks
(fun (l1,t1) (l2,t2) -> ccnv univ CONV infos l1 l2 t1 t2)
- (mind_equiv_infos infos)
+ (mind_equiv_infos infos) (proj_equiv_infos infos)
lft1 stk1 lft2 stk2
and convert_vect univ infos lft1 lft2 v1 v2 =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index a22af4e0f7..0916d98ddf 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -9,11 +9,9 @@
(************************************************************************)
(*i*)
-open CErrors
open Util
open Names
open Cic
-open Term
open Declarations
open Environ
open Reduction
@@ -124,48 +122,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
env, Univ.make_abstract_instance auctx'
| _ -> error ()
in
- let eq_projection_body p1 p2 =
- let check eq f = if not (eq (f p1) (f p2)) then error () in
- check eq_ind (fun x -> x.proj_ind);
- check (==) (fun x -> x.proj_npars);
- check (==) (fun x -> x.proj_arg);
- check (eq_constr) (fun x -> x.proj_type);
- true
- in
- let check_inductive_type t1 t2 =
-
- (* Due to template polymorphism, the conclusions of
- t1 and t2, if in Type, are generated as the least upper bounds
- of the types of the constructors.
-
- By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U
- |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
- universe in the conclusion of t1 has an bounding universe in
- the conclusion of t2, so that we don't need to check the
- subtyping of the conclusions of t1 and t2.
-
- Even if we'd like to recheck it, the inference of constraints
- is not designed to deal with algebraic constraints of the form
- max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
- to recheck it (in short, we would need the actual graph of
- constraints as input while type checking is currently designed
- to output a set of constraints instead) *)
-
- (* So we cheat and replace the subtyping problem on algebraic
- constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
- (that we know are necessary true) by trivial constraints that
- the constraint generator knows how to deal with *)
-
- let (ctx1,s1) = dest_arity env t1 in
- let (ctx2,s2) = dest_arity env t2 in
- let s1,s2 =
- match s1, s2 with
- | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
- | (Prop _, Type _) | (Type _,Prop _) -> error ()
- | _ -> (s1, s2) in
- check_conv conv_leq env
- (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
- in
+ let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
let check_packet p1 p2 =
let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -222,9 +179,9 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
| FakeRecord, FakeRecord -> true
| PrimRecord info1, PrimRecord info2 ->
let check (id1, p1, pb1) (id2, p2, pb2) =
- Id.equal id1 id2 &&
- Array.for_all2 Constant.UserOrd.equal p1 p2 &&
- Array.for_all2 eq_projection_body pb1 pb2
+ (* we don't care about the id, the types are inferred from the inductive
+ (ie checked before now) *)
+ Array.for_all2 Label.equal p1 p2
in
Array.equal check info1 info2
| _, _ -> false
@@ -251,55 +208,10 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets
in ()
-let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
+let check_constant env l info1 cb2 spec2 subst1 subst2 =
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
- let check_type env t1 t2 =
-
- (* If the type of a constant is generated, it may mention
- non-variable algebraic universes that the general conversion
- algorithm is not ready to handle. Anyway, generated types of
- constants are functions of the body of the constant. If the
- bodies are the same in environments that are subtypes one of
- the other, the types are subtypes too (i.e. if Gamma <= Gamma',
- Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
- Hence they don't have to be checked again *)
-
- let t1,t2 =
- if isArity t2 then
- let (ctx2,s2) = destArity t2 in
- match s2 with
- | Type v when not (Univ.is_univ_variable v) ->
- (* The type in the interface is inferred and is made of algebraic
- universes *)
- begin try
- let (ctx1,s1) = dest_arity env t1 in
- match s1 with
- | Type u when not (Univ.is_univ_variable u) ->
- (* Both types are inferred, no need to recheck them. We
- cheat and collapse the types to Prop *)
- mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
- | Prop _ ->
- (* The type in the interface is inferred, it may be the case
- that the type in the implementation is smaller because
- the body is more reduced. We safely collapse the upper
- type to Prop *)
- mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
- | Type _ ->
- (* The type in the interface is inferred and the type in the
- implementation is not inferred or is inferred but from a
- more reduced body so that it is just a variable. Since
- constraints of the form "univ <= max(...)" are not
- expressible in the system of algebraic universes: we fail
- (the user has to use an explicit type in the interface *)
- error ()
- with UserError _ (* "not an arity" *) ->
- error () end
- | _ -> t1,t2
- else
- (t1,t2) in
- check_conv conv_leq env t1 t2
- in
+ let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
match info1 with
| Constant cb1 ->
let cb1 = subst_const_body subst1 cb1 in
@@ -360,7 +272,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
let check_one_body (l,spec2) =
match spec2 with
| SFBconst cb2 ->
- check_constant env mp1 l (get_obj mp1 map1 l)
+ check_constant env l (get_obj mp1 map1 l)
cb2 spec2 subst1 subst2
| SFBmind mib2 ->
check_inductive env mp1 l (get_obj mp1 map1 l)
diff --git a/checker/term.ml b/checker/term.ml
index 509634bdba..d84491b38f 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -20,15 +20,15 @@ open Cic
(* Sorts. *)
let family_of_sort = function
- | Prop Null -> InProp
- | Prop Pos -> InSet
+ | Prop -> InProp
+ | Set -> InSet
| Type _ -> InType
let family_equal = (==)
let sort_of_univ u =
- if Univ.is_type0m_univ u then Prop Null
- else if Univ.is_type0_univ u then Prop Pos
+ if Univ.is_type0m_univ u then Prop
+ else if Univ.is_type0_univ u then Set
else Type u
(********************************************************************)
@@ -356,15 +356,11 @@ let rec isArity c =
(* alpha conversion : ignore print names and casts *)
let compare_sorts s1 s2 = match s1, s2 with
-| Prop c1, Prop c2 ->
- begin match c1, c2 with
- | Pos, Pos | Null, Null -> true
- | Pos, Null -> false
- | Null, Pos -> false
- end
+| Prop, Prop | Set, Set -> true
| Type u1, Type u2 -> Univ.Universe.equal u1 u2
-| Prop _, Type _ -> false
-| Type _, Prop _ -> false
+| Prop, Set | Set, Prop -> false
+| (Prop | Set), Type _ -> false
+| Type _, (Prop | Set) -> false
let eq_puniverses f (c1,u1) (c2,u2) =
Univ.Instance.equal u1 u2 && f c1 c2
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 345ee5b8ff..138fe8bc95 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv =
let sort_of_product env domsort rangsort =
match (domsort, rangsort) with
(* Product rule (s,Prop,Prop) *)
- | (_, Prop Null) -> rangsort
+ | _, Prop -> rangsort
(* Product rule (Prop/Set,Set,Set) *)
- | (Prop _, Prop Pos) -> rangsort
+ | (Prop | Set), Set -> rangsort
(* Product rule (Type,Set,?) *)
- | (Type u1, Prop Pos) ->
+ | Type u1, Set ->
if engagement env = ImpredicativeSet then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
@@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort =
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Univ.sup u1 Univ.type0_univ)
(* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Pos, Type u2) -> Type (Univ.sup Univ.type0_univ u2)
+ | Set, Type u2 -> Type (Univ.sup Univ.type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Null, Type _) -> rangsort
+ | Prop, Type _ -> rangsort
(* Product rule (Type_i,Type_i,Type_i) *)
- | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
+ | Type u1, Type u2 -> Type (Univ.sup u1 u2)
(* Type of a type cast *)
@@ -198,14 +198,13 @@ let judge_of_case env ci pj (c,cj) lfj =
(* Projection. *)
let judge_of_projection env p c ct =
- let pb = lookup_projection p env in
+ let pty = lookup_projection p env in
let (ind,u), args =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (c, ct)
in
- assert(eq_ind pb.proj_ind ind);
- let ty = subst_instance_constr u pb.proj_type in
- substl (c :: List.rev args) ty
+ let ty = subst_instance_constr u pty in
+ substl (c :: List.rev args) ty
(* Fixpoints. *)
@@ -239,7 +238,7 @@ let type_fixpoint env lna lar lbody vdefj =
let rec execute env cstr =
match cstr with
(* Atomic terms *)
- | Sort (Prop _) -> judge_of_prop
+ | Sort (Prop | Set) -> judge_of_prop
| Sort (Type u) -> judge_of_type u
diff --git a/checker/univ.ml b/checker/univ.ml
index 15673736f2..e50e883adf 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -190,13 +190,6 @@ struct
(let (u,n) = x and (v,n') = y in
Int.equal n n' && Level.equal u v)
- let leq (u,n) (v,n') =
- let cmp = Level.compare u v in
- if Int.equal cmp 0 then n <= n'
- else if n <= n' then
- (Level.is_prop u && Level.is_small v)
- else false
-
let successor (u,n) =
if Level.is_prop u then type1
else (u, n + 1)
@@ -833,41 +826,6 @@ type 'a constrained = 'a * constraints
type 'a constraint_function = 'a -> 'a -> constraints -> constraints
-let constraint_add_leq v u c =
- (* We just discard trivial constraints like u<=u *)
- if Expr.equal v u then c
- else
- match v, u with
- | (x,n), (y,m) ->
- let j = m - n in
- if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
- Constraint.add (x,Lt,y) c
- else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
- if Level.equal x y then (* u+(k+1) <= u *)
- raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
- else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
- else if j = 0 then
- Constraint.add (x,Le,y) c
- else (* j >= 1 *) (* m = n + k, u <= v+k *)
- if Level.equal x y then c (* u <= u+k, trivial *)
- else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
- else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
-
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
-
-let check_univ_leq u v =
- Universe.for_all (fun u -> check_univ_leq_one u v) u
-
-let enforce_leq u v c =
- match v with
- | [v] ->
- List.fold_right (fun u -> constraint_add_leq u v) u c
- | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
-
-let enforce_leq u v c =
- if check_univ_leq u v then c
- else enforce_leq u v c
-
let check_constraint g (l,d,r) =
match d with
| Eq -> check_equal g l r
diff --git a/checker/univ.mli b/checker/univ.mli
index 6cd3b36382..3b29b158f2 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints
type 'a constraint_function = 'a -> 'a -> constraints -> constraints
-val enforce_leq : universe constraint_function
-
(** {6 ... } *)
(** Merge of constraints in a universes graph.
The function [merge_constraints] merges a set of constraints in a given
diff --git a/checker/values.ml b/checker/values.ml
index 4f28d6e448..e1b5a949ac 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli
+MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli
*)
@@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
(** kernel/term *)
-let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|]
+let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|]
let v_sortfam = v_enum "sorts_family" 3
let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
@@ -135,7 +135,9 @@ let v_caseinfo =
v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
let v_cast = v_enum "cast_kind" 4
-let v_proj = v_tuple "projection" [|v_cst; v_bool|]
+
+let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
+let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
let rec v_constr =
Sum ("constr",0,[|
@@ -223,12 +225,8 @@ let v_cst_def =
v_sum "constant_def" 0
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
-let v_projbody =
- v_tuple "projection_body"
- [|v_ind;Int;Int;v_constr|]
-
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
+ v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|]
let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
@@ -277,7 +275,7 @@ let v_finite = v_enum "recursivity_kind" 3
let v_record_info =
v_sum "record_info" 2
- [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
+ [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
let v_ind_pack_univs =
v_sum "abstract_inductive_universes" 0
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 22:53:02 +0000