diff options
Diffstat (limited to 'checker')
-rw-r--r-- | checker/check.mllib | 1 | ||||
-rw-r--r-- | checker/cic.mli | 14 | ||||
-rw-r--r-- | checker/closure.ml | 3 | ||||
-rw-r--r-- | checker/environ.ml | 14 | ||||
-rw-r--r-- | checker/environ.mli | 1 | ||||
-rw-r--r-- | checker/subtyping.ml | 23 | ||||
-rw-r--r-- | checker/typeops.ml | 2 | ||||
-rw-r--r-- | checker/values.ml | 17 |
8 files changed, 35 insertions, 40 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 7ec345768..a890f2cef 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -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/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 67032bd1b..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 fb80632357e3ffa988c6bba3fa6ade64 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|] @@ -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; |