diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
commit | 0413899668e8be15df5065abdaf1d40ad3c2c31b (patch) | |
tree | 5d2c4671737b9d0c9eba68cdf0d16503c6e47608 | |
parent | d7db69dea59cddd3ac81ed469170fad889af4e16 (diff) |
Fix checker to handle projections with eta and universe polymorphism correctly.
-rw-r--r-- | checker/cic.mli | 8 | ||||
-rw-r--r-- | checker/inductive.ml | 10 | ||||
-rw-r--r-- | checker/mod_checking.ml | 11 | ||||
-rw-r--r-- | checker/reduction.ml | 48 | ||||
-rw-r--r-- | checker/term.ml | 1 | ||||
-rw-r--r-- | kernel/reduction.ml | 2 | ||||
-rw-r--r-- | test-suite/success/namedunivs.v | 2 |
7 files changed, 64 insertions, 18 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 2f33c60f5..1313208a3 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -264,14 +264,14 @@ type one_inductive_body = { mind_nf_lc : constr array; (** Head normalized constructor types so that their conclusion is atomic *) - mind_consnrealdecls : int array; - (** Length of the signature of the constructors (with let, w/o params) - (not used in the kernel) *) - mind_consnrealargs : int array; (** Length of the signature of the constructors (w/o let, w/o params) (not used in the kernel) *) + mind_consnrealdecls : int array; + (** Length of the signature of the constructors (with let, w/o params) + (not used in the kernel) *) + mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) (** {8 Datas for bytecode compilation } *) diff --git a/checker/inductive.ml b/checker/inductive.ml index c23b2578b..c95cb7a2e 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -83,7 +83,7 @@ let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in substl s (subst_instance_constr u c) -let instantiate_params full t args sign = +let instantiate_params full t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = @@ -91,7 +91,8 @@ let instantiate_params full t args sign = (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t) + | (Some b,_,LetIn(_,_,_,t)) -> + (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) sign @@ -103,13 +104,12 @@ let instantiate_params full t args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in - subst_instance_context u ar + fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) = let inst_ind = constructor_instantiate mind u mib in (fun t -> - instantiate_params true (inst_ind t) params mib.mind_params_ctxt) + instantiate_params true (inst_ind t) u params mib.mind_params_ctxt) (************************************************************************) (************************************************************************) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 93b136c48..521d9e3ee 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -37,11 +37,16 @@ let check_constant_declaration env kn cb = check_polymorphic_arity env' ctxt par; env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt in - let body = + let () = match body_of_constant cb with | Some bd -> - let j = infer envty bd in - conv_leq envty j ty + (match cb.const_proj with + | None -> let j = infer envty bd in + conv_leq envty j ty + | Some pb -> + let env' = add_constant kn cb env' in + let j = infer env' bd in + conv_leq envty j ty) | None -> () in if cb.const_polymorphic then add_constant kn cb env diff --git a/checker/reduction.ml b/checker/reduction.ml index 403d27779..0bf5ae32f 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -40,6 +40,8 @@ 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) -> + Int.equal bal 0 && compare_rec 0 s1 s2 | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) -> bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> @@ -131,6 +133,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (Zlapp a1,Zlapp a2) -> Array.iter2 f a1 a2 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 + | (Zlproj (c1,l1),Zlproj (c2,l2)) -> + if not (Names.eq_con_chk 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; @@ -238,6 +243,11 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* compute the lifts that apply to the head of the term (hd1 and hd2) *) let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in + let () = Print.print_pure_constr (whd_val infos hd1); + Pp.pp (Pp.str " conv "); + Print.print_pure_constr (whd_val infos hd2); + Pp.ppnl (Pp.str "") + in match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> @@ -265,7 +275,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) - if eq_table_key fl1 fl2 + if eq_table_key fl1 fl2 then convert_stacks univ infos lft1 lft2 v1 v2 else raise NotConvertible with NotConvertible -> @@ -391,6 +401,21 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = convert_stacks univ infos lft1 lft2 v1 v2) else raise NotConvertible + (* Eta expansion of records *) + | (FConstruct ((ind1,j1),u1), _) -> + (try + let v1, v2 = + eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks univ infos lft1 lft2 v1 v2 + with Not_found -> raise NotConvertible) + + | (_, FConstruct ((ind2,j2),u2)) -> + (try + let v2, v1 = + eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks univ infos lft1 lft2 v1 v2 + with Not_found -> raise NotConvertible) + | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> if op1 = op2 then @@ -443,7 +468,19 @@ let clos_fconv cv_pb env t1 t2 = let fconv cv_pb env t1 t2 = if eq_constr t1 t2 then () - else clos_fconv cv_pb env t1 t2 + else + try clos_fconv cv_pb env t1 t2 + with NotConvertible -> + let open Pp in + if !Flags.debug then ( + Pp.ppnl (str " conversion failed: "); + Print.print_pure_constr t1; + Pp.ppnl (str " and "); + Print.print_pure_constr t2); + raise NotConvertible + + + let conv = fconv CONV let conv_leq = fconv CUMUL @@ -483,7 +520,7 @@ let dest_prod env = in decrec env empty_rel_context -(* The same but preserving lets *) +(* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = let rty = whd_betadeltaiota_nolet env ty in @@ -495,7 +532,10 @@ let dest_prod_assum env = let d = (x,Some b,t) in prodec_rec (push_rel d env) (d::l) c | Cast (c,_,_) -> prodec_rec env l c - | _ -> l,rty + | _ -> + let rty' = whd_betadeltaiota env rty in + if Term.eq_constr rty' rty then l, rty + else prodec_rec env l rty' in prodec_rec env empty_rel_context diff --git a/checker/term.ml b/checker/term.ml index 1b8177325..30142c2cd 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -392,6 +392,7 @@ let compare_constr f t1 t2 = Array.equal f tl1 tl2 && Array.equal f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 + | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2 | _ -> false let rec eq_constr m n = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ebba23165..31c338dd9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -468,7 +468,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible - (* Eta expansion of records *) + (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> (try let v1, v2 = diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index 967e13bbc..5c0a3c7f2 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -79,7 +79,7 @@ Proof. Defined. Definition paths_downward_closed_lt (A : Type@{i}) (x y : A) : - @paths (liftlt@{i j} A) x y -> paths x y. + @paths (liftlt@{j i} A) x y -> paths x y. Proof. intros. destruct X. exact (idpath _). Defined. |