diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-16 10:58:13 +0100 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 17:47:48 +0100 |
commit | fba1f0ed91aff372234b5a95422ee18f1730522f (patch) | |
tree | fa5ca22e0af3ad47067c5908385039e1668f7843 /checker | |
parent | f3a6d9080842899e50a44e9474ac0f9a475d5db1 (diff) |
Update checker/values and cic due to changes in case_info and record_body.
Diffstat (limited to 'checker')
-rw-r--r-- | checker/cic.mli | 8 | ||||
-rw-r--r-- | checker/closure.ml | 3 | ||||
-rw-r--r-- | checker/subtyping.ml | 4 | ||||
-rw-r--r-- | checker/values.ml | 6 |
4 files changed, 13 insertions, 8 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index f00c95705..6ed9a4d25 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -227,6 +227,10 @@ type recarg = type wf_paths = recarg Rtree.t +type record_body = (Id.t * constant 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 regular_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -288,9 +292,7 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : (constant array * projection_body array) option; - (** Whether the inductive type has been declared as a record, - In that case we get its canonical eta-expansion and list of projections. *) + mind_record : record_body option; (** 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 879146284..35c16d2ab 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -731,8 +731,7 @@ let rec get_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 (projs,pbs) when Array.length projs > 0 - && mib.mind_finite <> CoFinite -> + | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite -> (* (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/subtyping.ml b/checker/subtyping.ml index a9a037bce..0144580bc 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -198,7 +198,9 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let record_equal x y = match x, y with | None, None -> true - | Some (p1,pb1), Some (p2,pb2) -> + | Some None, Some None -> true + | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) -> + Id.equal id1 id2 && Array.for_all2 eq_con_chk p1 p2 && Array.for_all2 eq_projection_body pb1 pb2 | _, _ -> false diff --git a/checker/values.ml b/checker/values.ml index b38744cc7..f55cf63fc 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -119,9 +119,11 @@ let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] +let v_boollist = List v_bool + let v_caseinfo = let v_cstyle = v_enum "case_style" 5 in - let v_cprint = v_tuple "case_printing" [|Int;v_cstyle|] in + let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] let v_cast = v_enum "cast_kind" 4 @@ -251,7 +253,7 @@ let v_one_ind = v_tuple "one_inductive_body" let v_finite = v_enum "recursivity_kind" 3 let v_mind_record = Annot ("mind_record", - Opt (v_tuple "record" [| Array v_cst; Array v_projbody |])) + Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]))) let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; |