diff options
-rw-r--r-- | kernel/closure.ml | 19 | ||||
-rw-r--r-- | kernel/closure.mli | 5 | ||||
-rw-r--r-- | kernel/inductive.ml | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 10 | ||||
-rw-r--r-- | kernel/vconv.ml | 3 | ||||
-rw-r--r-- | pretyping/cases.ml | 8 | ||||
-rw-r--r-- | test-suite/modules/ind.v | 28 |
7 files changed, 53 insertions, 22 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 6bdca4f8f..364475019 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -375,14 +375,17 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) - -let rec mind_equiv info kn1 kn2 = - kn1 = kn2 || - match (lookup_mind kn1 info.i_env).mind_equiv with - Some kn1' -> mind_equiv info kn2 kn1' - | None -> match (lookup_mind kn2 info.i_env).mind_equiv with - Some kn2' -> mind_equiv info kn2' kn1 - | None -> false +let rec mind_equiv env (kn1,i1) (kn2,i2) = + let rec equiv kn1 kn2 = + kn1 = kn2 || + match (lookup_mind kn1 env).mind_equiv with + Some kn1' -> equiv kn2 kn1' + | None -> match (lookup_mind kn2 env).mind_equiv with + Some kn2' -> equiv kn2' kn1 + | None -> false in + i1 = i2 && equiv kn1 kn2 + +let mind_equiv_infos info = mind_equiv info.i_env let create mk_cl flgs env = { i_flags = flgs; diff --git a/kernel/closure.mli b/kernel/closure.mli index 88f9139e6..2a0c1f89e 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -179,8 +179,9 @@ val whd_stack : (* [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> table_key -> fconstr option -(* [mind_equiv] checks whether two mutual inductives are intentionally equal *) -val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool +(* [mind_equiv] checks whether two inductive types are intentionally equal *) +val mind_equiv : env -> inductive -> inductive -> bool +val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2e2bcafce..d62af2e5e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -364,7 +364,7 @@ let inductive_equiv env (kn1,i1) (kn2,i2) = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - (indsp <> ci.ci_ind) or + not (Closure.mind_equiv env indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5b69ac7b6..28176ecc5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -257,14 +257,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd (kn1,i1), FInd (kn2,i2)) -> - if i1 = i2 && mind_equiv infos kn1 kn2 + | (FInd ind1, FInd ind2) -> + if mind_equiv_infos infos ind1 ind2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) -> - if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2 + | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> + if j1 = j2 && mind_equiv_infos infos ind1 ind2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -317,7 +317,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv = and convert_stacks infos lft1 lft2 stk1 stk2 cuniv = compare_stacks (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c) - (fun (mind1,i1) (mind2,i2) -> i1=i2 && mind_equiv infos mind1 mind2) + (mind_equiv_infos infos) lft1 stk1 lft2 stk2 cuniv and convert_vect infos lft1 lft2 v1 v2 cuniv = diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 7115097e4..7c515735d 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -83,7 +83,8 @@ and conv_whd pb k whd1 whd2 cu = and conv_atom pb k a1 stk1 a2 stk2 cu = match a1, a2 with | Aind (kn1,i1), Aind(kn2,i2) -> - if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then + if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 + then conv_stack k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b2c37f7e6..badf8796e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -497,12 +497,12 @@ let rec adjust_local_defs loc = function | [], [] -> [] | _ -> raise NotAdjustable -let check_and_adjust_constructor ind cstrs = function +let check_and_adjust_constructor env ind cstrs = function | PatVar _ as pat -> pat | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in - if ind' = ind then + if Closure.mind_equiv env ind' ind then (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in @@ -1129,7 +1129,7 @@ let first_clause_irrefutable env = function | eqn::mat -> List.for_all (irrefutable env) eqn.patterns | _ -> false -let group_equations pb mind current cstrs mat = +let group_equations pb ind current cstrs mat = let mat = if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in let brs = Array.create (Array.length cstrs) [] in @@ -1139,7 +1139,7 @@ let group_equations pb mind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match check_and_adjust_constructor mind cstrs pat with + match check_and_adjust_constructor pb.env ind cstrs pat with | PatVar (_,name) -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v index a4f9d3a28..a15f390a3 100644 --- a/test-suite/modules/ind.v +++ b/test-suite/modules/ind.v @@ -14,4 +14,30 @@ End M. Module N := M. -Check (N.f M.A).
\ No newline at end of file +Check (N.f M.A). + +(* Check use of equivalence on inductive types (bug #1242) *) + + Module Type ASIG. + Inductive t : Set := a | b : t. + Definition f := fun x => match x with a => true | b => false end. + End ASIG. + + Module Type BSIG. + Declare Module A : ASIG. + Definition f := fun x => match x with A.a => true | A.b => false end. + End BSIG. + + Module C (A : ASIG) (B : BSIG with Module A:=A). + + (* Check equivalence is considered in "case_info" *) + Lemma test : forall x, A.f x = B.f x. + intro x. unfold B.f, A.f. + destruct x; reflexivity. + Qed. + + (* Check equivalence is considered in pattern-matching *) + Definition f (x : A.t) := match x with B.A.a => true | B.A.b => false end. + + End C. + |