aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/cic.mli13
-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.ml12
-rw-r--r--checker/inductive.ml10
-rw-r--r--checker/modops.ml22
-rw-r--r--checker/reduction.ml24
-rw-r--r--checker/subtyping.ml19
-rw-r--r--checker/typeops.ml7
-rw-r--r--checker/values.ml14
14 files changed, 107 insertions, 115 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 4846a9af8c..17259bb438 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -202,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
@@ -230,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 = {
@@ -254,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 bcb71fe55f..8f11e01c33 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -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 b1edec5568..d15380643f 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -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/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/reduction.ml b/checker/reduction.ml
index 16c7012138..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;
@@ -257,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
@@ -300,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,[]))
@@ -523,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 6d0d6f6c6d..0916d98ddf 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -12,7 +12,6 @@
open Util
open Names
open Cic
-open Term
open Declarations
open Environ
open Reduction
@@ -123,14 +122,6 @@ 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 = check_conv conv_leq env t1 t2 in
let check_packet p1 p2 =
@@ -188,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
@@ -217,7 +208,7 @@ 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 = check_conv conv_leq env t1 t2 in
@@ -281,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/typeops.ml b/checker/typeops.ml
index 19ede4b9a2..138fe8bc95 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -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. *)
diff --git a/checker/values.ml b/checker/values.ml
index 88cdb644db..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 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli
+MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli
*)
@@ -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-04 00:50:26 +0000