aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/cic.mli16
-rw-r--r--checker/closure.ml3
-rw-r--r--checker/declarations.ml9
-rw-r--r--checker/environ.ml14
-rw-r--r--checker/environ.mli1
-rw-r--r--checker/subtyping.ml23
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/values.ml19
9 files changed, 44 insertions, 44 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index f79ba66e3..139fa765b 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -3,7 +3,6 @@ Coq_config
Analyze
Hook
Terminal
-Canary
Hashset
Hashcons
CSet
diff --git a/checker/cic.mli b/checker/cic.mli
index 27e2a479f..a890f2cef 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -128,7 +128,7 @@ type section_context = unit
(** {6 Substitutions} *)
type delta_hint =
- | Inline of int * constr option
+ | Inline of int * (Univ.AUContext.t * constr) option
| Equiv of KerName.t
type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
@@ -207,12 +207,10 @@ type inline = int option
always transparent. *)
type projection_body = {
- proj_ind : MutInd.t;
+ proj_ind : inductive;
proj_npars : int;
proj_arg : int;
proj_type : constr; (* Type under params *)
- proj_eta : constr * constr; (* Eta-expanded term and type *)
- proj_body : constr; (* For compatibility, the match version *)
}
type constant_def =
@@ -241,7 +239,6 @@ type constant_body = {
const_type : constr;
const_body_code : to_patch_substituted;
const_universes : constant_universes;
- const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags;
}
@@ -255,9 +252,10 @@ type recarg =
type wf_paths = recarg Rtree.t
-type record_body = (Id.t * Constant.t array * projection_body array) option
- (* The body is empty for non-primitive records, otherwise we get its
- binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
type regular_inductive_arity = {
mind_user_arity : constr;
@@ -325,7 +323,7 @@ type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+ mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *)
diff --git a/checker/closure.ml b/checker/closure.ml
index b9ae4daa8..2dcc1a984 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -619,7 +619,8 @@ 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
- | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite ->
+ | 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
diff --git a/checker/declarations.ml b/checker/declarations.ml
index e1d2cf6d1..a744a0227 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -196,7 +196,12 @@ let subst_con0 sub con u =
let dup con = con, Const (con, u) in
let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
match constant_of_delta_with_inline resolve con' with
- | Some t -> con', t
+ | Some (ctx, t) ->
+ (** FIXME: we never typecheck the inlined term, so that it could well
+ be garbage. What environment do we type it in though? The substitution
+ code should be moot in the checker but it **is** used nonetheless. *)
+ let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in
+ con', subst_instance_constr u t
| None ->
let con'' = match side with
| User -> constant_of_delta resolve con'
@@ -340,7 +345,7 @@ let gen_subst_delta_resolver dom subst resolver =
let kkey' = if dom then subst_kn subst kkey else kkey in
let hint' = match hint with
| Equiv kequ -> Equiv (subst_kn_delta subst kequ)
- | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+ | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
| Inline (_,None) -> hint
in
Deltamap.add_kn kkey' hint' rslv
diff --git a/checker/environ.ml b/checker/environ.ml
index 809150cea..ba1eb0ddb 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -166,9 +166,6 @@ let evaluable_constant cst env =
try let _ = constant_value env (cst, Univ.Instance.empty) in true
with Not_found | NotEvaluableConst _ -> false
-let is_projection cst env =
- (lookup_constant cst env).const_proj
-
let lookup_projection p env =
Cmap_env.find (Projection.constant p) env.env_globals.env_projections
@@ -195,11 +192,12 @@ let add_mind kn mib env =
(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
- | None | Some None -> env.env_globals.env_projections
- | Some (Some (id, kns, pbs)) ->
- Array.fold_left2 (fun projs kn pb ->
- Cmap_env.add kn pb projs)
- env.env_globals.env_projections kns pbs
+ | 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
diff --git a/checker/environ.mli b/checker/environ.mli
index 4a7597249..acb29d7d2 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> Constant.t puniverses -> constr
val evaluable_constant : Constant.t -> env -> bool
-val is_projection : Constant.t -> env -> bool
val lookup_projection : Projection.t -> env -> projection_body
(* Inductives *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5c672d04a..a22af4e0f 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -126,13 +126,11 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let eq_projection_body p1 p2 =
let check eq f = if not (eq (f p1) (f p2)) then error () in
- check MutInd.equal (fun x -> x.proj_ind);
+ 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);
- check (eq_constr) (fun x -> fst x.proj_eta);
- check (eq_constr) (fun x -> snd x.proj_eta);
- check (eq_constr) (fun x -> x.proj_body); true
+ true
in
let check_inductive_type t1 t2 =
@@ -220,16 +218,19 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
(* we check that records and their field names are preserved. *)
let record_equal x y =
match x, y with
- | None, None -> true
- | Some None, Some None -> true
- | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
- Id.equal id1 id2 &&
- Array.for_all2 Constant.UserOrd.equal p1 p2 &&
- Array.for_all2 eq_projection_body pb1 pb2
+ | NotRecord, NotRecord -> true
+ | 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
+ in
+ Array.equal check info1 info2
| _, _ -> false
in
check record_equal (fun mib -> mib.mind_record);
- if mib1.mind_record != None then begin
+ if mib1.mind_record != NotRecord then begin
let rec names_prod_letin t = match t with
| Prod(n,_,t) -> n::(names_prod_letin t)
| LetIn(n,_,_,t) -> n::(names_prod_letin t)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0b..345ee5b8f 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -203,7 +203,7 @@ let judge_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (c, ct)
in
- assert(MutInd.equal pb.proj_ind (fst ind));
+ assert(eq_ind pb.proj_ind ind);
let ty = subst_instance_constr u pb.proj_type in
substl (c :: List.rev args) ty
diff --git a/checker/values.ml b/checker/values.ml
index f7ab95fe2..4f28d6e44 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 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli
+MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli
*)
@@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0,
[|[|v_dp|];
[|v_uid|];
[|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
let v_ind = v_tuple "inductive" [|v_cst;Int|]
let v_cons = v_tuple "constructor" [|v_ind;Int|]
@@ -173,7 +173,7 @@ let v_section_ctxt = v_enum "emptylist" 1
(** kernel/mod_subst *)
let v_delta_hint =
- v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|]
+ v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
let v_resolver =
v_tuple "delta_resolver"
@@ -225,9 +225,7 @@ let v_cst_def =
let v_projbody =
v_tuple "projection_body"
- [|v_cst;Int;Int;v_constr;
- v_tuple "proj_eta" [|v_constr;v_constr|];
- v_constr|]
+ [|v_ind;Int;Int;v_constr|]
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
@@ -241,7 +239,6 @@ let v_cb = v_tuple "constant_body"
Any;
v_const_univs;
v_bool;
- v_bool;
v_typing_flags|]
let v_recarg = v_sum "recarg" 1 (* Norec *)
@@ -277,8 +274,10 @@ let v_one_ind = v_tuple "one_inductive_body"
Any|]
let v_finite = v_enum "recursivity_kind" 3
-let v_mind_record = Annot ("mind_record",
- Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
+
+let v_record_info =
+ v_sum "record_info" 2
+ [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
let v_ind_pack_univs =
v_sum "abstract_inductive_universes" 0
@@ -286,7 +285,7 @@ let v_ind_pack_univs =
let v_ind_pack = v_tuple "mutual_inductive_body"
[|Array v_one_ind;
- v_mind_record;
+ v_record_info;
v_finite;
Int;
v_section_ctxt;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 12:51:54 +0000