aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/cic.mli15
-rw-r--r--checker/closure.ml49
-rw-r--r--checker/closure.mli2
-rw-r--r--checker/declarations.ml51
-rw-r--r--checker/declarations.mli3
-rw-r--r--checker/dune26
-rw-r--r--checker/environ.ml29
-rw-r--r--checker/environ.mli4
-rw-r--r--checker/indtypes.ml6
-rw-r--r--checker/reduction.ml24
-rw-r--r--checker/subtyping.ml15
-rw-r--r--checker/typeops.ml11
-rw-r--r--checker/values.ml19
13 files changed, 130 insertions, 124 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 4846a9af8c..4162903b04 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -132,7 +132,7 @@ type delta_hint =
type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
-type 'a umap_t = 'a MPmap.t * 'a MBImap.t
+type 'a umap_t = 'a MPmap.t
type substitution = (ModPath.t * delta_resolver) umap_t
(** {6 Delayed constr} *)
@@ -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..03fee1ab51 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -28,18 +28,13 @@ let empty_delta_resolver = Deltamap.empty
module Umap = struct
[@@@ocaml.warning "-32-34"]
type 'a t = 'a umap_t
- let empty = MPmap.empty, MBImap.empty
- let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
- let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
- let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
- let find_mp mp map = MPmap.find mp (fst map)
- let find_mbi mbi map = MBImap.find mbi (snd map)
- let mem_mp mp map = MPmap.mem mp (fst map)
- let mem_mbi mbi map = MBImap.mem mbi (snd map)
- let iter_mbi f map = MBImap.iter f (snd map)
- let fold fmp fmbi (m1,m2) i =
- MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
- let join map1 map2 = fold add_mp add_mbi map1 map2
+ let empty = MPmap.empty
+ let is_empty m = MPmap.is_empty m
+ let add_mbi mbi x m = MPmap.add (MPbound mbi) x m
+ let add_mp mp x m = MPmap.add mp x m
+ let find = MPmap.find
+ let fold = MPmap.fold
+ let join map1 map2 = fold add_mp map1 map2
end
type 'a subst_fun = substitution -> 'a -> 'a
@@ -117,15 +112,10 @@ let constant_of_delta_with_inline resolve con =
let subst_mp0 sub mp = (* 's like subst *)
let rec aux mp =
match mp with
- | MPfile sid -> Umap.find_mp mp sub
- | MPbound bid ->
- begin
- try Umap.find_mbi bid sub
- with Not_found -> Umap.find_mp mp sub
- end
+ | MPfile _ | MPbound _ -> Umap.find mp sub
| MPdot (mp1,l) as mp2 ->
begin
- try Umap.find_mp mp2 sub
+ try Umap.find mp2 sub
with Not_found ->
let mp1',resolve = aux mp1 in
MPdot (mp1',l),resolve
@@ -214,11 +204,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')
@@ -386,9 +372,7 @@ let substition_prefixed_by k mp subst =
Umap.add_mp new_key (mp_to,reso) sub
else sub
in
- let mbi_prefixmp mbi _ sub = sub
- in
- Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst
+ Umap.fold mp_prefixmp subst empty_subst
let join subst1 subst2 =
let apply_subst mpk add (mp,resolve) res =
@@ -408,8 +392,7 @@ let join subst1 subst2 =
Umap.join prefixed_subst (add (mp',resolve'') res)
in
let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in
- let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in
- let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
+ let subst = Umap.fold mp_apply_subst subst1 empty_subst in
Umap.join subst2 subst
let from_val x = { subst_value = x; subst_subst = []; }
@@ -495,6 +478,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/dune b/checker/dune
new file mode 100644
index 0000000000..d918f853dd
--- /dev/null
+++ b/checker/dune
@@ -0,0 +1,26 @@
+(rule (copy %{project_root}/kernel/names.ml names.ml))
+(rule (copy %{project_root}/kernel/names.mli names.mli))
+(rule (copy %{project_root}/kernel/esubst.ml esubst.ml))
+(rule (copy %{project_root}/kernel/esubst.mli esubst.mli))
+
+(library
+ (name checker)
+ (public_name coq.checker)
+ (synopsis "Coq's Standalone Proof Checker")
+ (modules values analyze names esubst)
+ (wrapped false)
+ (libraries coq.lib))
+
+(executable
+ (name main)
+ (public_name coqchk)
+ (modules :standard \ votour values analyze names esubst)
+ (modules_without_implementation cic)
+ (libraries coq.checker))
+
+(executable
+ (name votour)
+ (public_name votour)
+ (modules votour)
+ (libraries coq.checker))
+
diff --git a/checker/environ.ml b/checker/environ.ml
index ba1eb0ddb4..b172acb126 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
@@ -188,17 +183,9 @@ let lookup_mind kn env =
let add_mind kn mib env =
if Mindmap_env.mem kn env.env_globals.env_inductives then
- Printf.ksprintf anomaly ("Inductive %s is already defined.")
+ Printf.ksprintf anomaly ("Mutual inductive block %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 8f11e01c33..1fd86bc368 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -595,8 +595,12 @@ let check_subtyping cumi paramsctxt env inds =
(************************************************************************)
(************************************************************************)
+let print_mutind ind =
+ let kn = MutInd.user ind in
+ str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn))
+
let check_inductive env kn mib =
- Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
+ Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ print_mutind kn);
(* check mind_constraints: should be consistent with env *)
let env0 =
match mib.mind_universes with
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 3f7f844704..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
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 19ede4b9a2..e4c3f4ae4b 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
let specif =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+ failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
in
type_of_inductive_knowing_parameters env (specif,u) paramstyp
@@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) =
let specif =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+ failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
in
type_of_constructor (c,u) specif
@@ -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 d81b0f474a..35027d5bfb 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 a127e0c2322c7846914bbca9921309c7 checker/cic.mli
*)
@@ -142,7 +142,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,[|
@@ -190,10 +192,7 @@ let v_resolver =
let v_mp_resolver = v_tuple "" [|v_mp;v_resolver|]
let v_subst =
- v_tuple "substitution"
- [|v_map v_mp v_mp_resolver;
- v_map v_uid v_mp_resolver|]
-
+ Annot ("substitution", v_map v_mp v_mp_resolver)
(** kernel/lazyconstr *)
@@ -230,12 +229,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|]|]
@@ -284,7 +279,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 23:29:50 +0000