diff options
| -rw-r--r-- | engine/eConstr.ml | 133 | ||||
| -rw-r--r-- | engine/eConstr.mli | 7 | ||||
| -rw-r--r-- | engine/termops.ml | 14 | ||||
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | engine/universes.ml | 41 | ||||
| -rw-r--r-- | engine/universes.mli | 4 | ||||
| -rw-r--r-- | kernel/constr.ml | 113 | ||||
| -rw-r--r-- | kernel/constr.mli | 47 | ||||
| -rw-r--r-- | kernel/names.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 7 | ||||
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | library/globnames.ml | 2 | ||||
| -rw-r--r-- | library/globnames.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 3 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 175 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
| -rw-r--r-- | pretyping/unification.ml | 12 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/6661.v | 259 | ||||
| -rw-r--r-- | test-suite/bugs/closed/6775.v | 43 | ||||
| -rw-r--r-- | test-suite/coqchk/cumulativity.v | 2 | ||||
| -rw-r--r-- | test-suite/success/cumulativity.v | 56 | ||||
| -rw-r--r-- | vernac/obligations.ml | 1 |
24 files changed, 616 insertions, 330 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index b95068ebf..59dc5a221 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -548,39 +548,100 @@ let fold sigma f acc c = match kind sigma c with | CoFix (_,(lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl -let compare_gen k eq_inst eq_sort eq_constr c1 c2 = - (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2 +let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 = + (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2 let eq_constr sigma c1 c2 = let kind c = kind_upto sigma c in - let rec eq_constr c1 c2 = - compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2 + let rec eq_constr nargs c1 c2 = + compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2 in - eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let eq_constr_nounivs sigma c1 c2 = let kind c = kind_upto sigma c in - let rec eq_constr c1 c2 = - compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2 + let rec eq_constr nargs c1 c2 = + compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2 in - eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2) + eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let compare_constr sigma cmp c1 c2 = let kind c = kind_upto sigma c in - let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in - compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2) + let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in + compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) -let test_constr_universes sigma leq m n = +let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = + let open Universes in + if not nargs_ok then enforce_eq_instances_univs false u u' cstrs + else + CArray.fold_left3 + (fun cstrs v u u' -> + let open Univ.Variance in + let u = Univ.Universe.make u in + let u' = Univ.Universe.make u' in + match v with + | Irrelevant -> Constraints.add (u,ULub,u') cstrs + | Covariant -> + (match cv_pb with + | Reduction.CONV -> Constraints.add (u,UEq,u') cstrs + | Reduction.CUMUL -> Constraints.add (u,ULe,u') cstrs) + | Invariant -> Constraints.add (u,UEq,u') cstrs) + cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') + +let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = + let open Universes in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); + cstrs + | Declarations.Polymorphic_ind _ -> + enforce_eq_instances_univs false u1 u2 cstrs + | Declarations.Cumulative_ind cumi -> + let num_param_arity = Reduction.inductive_cumulativity_arguments spec in + let variances = Univ.ACumulativityInfo.variance cumi in + compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs + +let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = + let open Universes in + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + cstrs + | Declarations.Polymorphic_ind _ -> + enforce_eq_instances_univs false u1 u2 cstrs + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in + let variances = Univ.ACumulativityInfo.variance cumi in + compare_cumulative_instances Reduction.CONV (Int.equal num_cnstr_args nargs) variances u1 u2 cstrs + +let eq_universes env sigma cstrs cv_pb ref nargs l l' = + if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true) + else + let l = Evd.normalize_universe_instance sigma l + and l' = Evd.normalize_universe_instance sigma l' in + let open Universes in + match ref with + | VarRef _ -> assert false (* variables don't have instances *) + | ConstRef _ -> + cstrs := enforce_eq_instances_univs true l l' !cstrs; true + | IndRef ind -> + let mind = Environ.lookup_mind (fst ind) env in + cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs; + true + | ConstructRef ((mi,ind),ctor) -> + let mind = Environ.lookup_mind mi env in + cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs; + true + +let test_constr_universes env sigma leq m n = let open Universes in let kind c = kind_upto sigma c in if m == n then Some Constraints.empty - else + else let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - let l = EInstance.kind sigma (EInstance.make l) in - let l' = EInstance.kind sigma (EInstance.make l') in - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = + let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in + let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' + and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in + let eq_sorts s1 s2 = let s1 = ESorts.kind sigma (ESorts.make s1) in let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true @@ -597,24 +658,25 @@ let test_constr_universes sigma leq m n = (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; true) in - let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in + let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in let res = if leq then - let rec compare_leq m n = - Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n + let rec compare_leq nargs m n = + Constr.compare_head_gen_leq_with kind kind leq_universes leq_sorts + eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + compare_leq 0 m n else - Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n + Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None -let eq_constr_universes sigma m n = - test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n) -let leq_constr_universes sigma m n = - test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n) +let eq_constr_universes env sigma m n = + test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n) +let leq_constr_universes env sigma m n = + test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n) -let compare_head_gen_proj env sigma equ eqs eqc' m n = +let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = let kind c = kind_upto sigma c in match kind_upto sigma m, kind_upto sigma n with | Proj (p, c), App (f, args) @@ -624,29 +686,28 @@ let compare_head_gen_proj env sigma equ eqs eqc' m n = let pb = Environ.lookup_projection p env in let npars = pb.Declarations.proj_npars in if Array.length args == npars + 1 then - eqc' c args.(npars) + eqc' 0 c args.(npars) else false | _ -> false) - | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n + | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n let eq_constr_universes_proj env sigma m n = let open Universes in if m == n then Some Constraints.empty else let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = + let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in + let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else (cstrs := Constraints.add (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n in - let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in + let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None let universes_of_constr env sigma c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 36b6093d0..28c9dd3c2 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -198,9 +198,12 @@ val whd_evar : Evd.evar_map -> constr -> constr val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool -val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option -val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option +val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option + +(** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *) val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option + val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) diff --git a/engine/termops.ml b/engine/termops.ml index 35258762a..20b6b3504 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -914,12 +914,9 @@ let vars_of_global_reference env gr = (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) -let dependent_main noevar univs sigma m t = +let dependent_main noevar sigma m t = let open EConstr in - let eqc x y = - if univs then not (Option.is_empty (eq_constr_universes sigma x y)) - else eq_constr_nounivs sigma x y - in + let eqc x y = eq_constr_nounivs sigma x y in let rec deprec m t = if eqc m t then raise Occur @@ -936,11 +933,8 @@ let dependent_main noevar univs sigma m t = in try deprec m t; false with Occur -> true -let dependent sigma c t = dependent_main false false sigma c t -let dependent_no_evar sigma c t = dependent_main true false sigma c t - -let dependent_univs sigma c t = dependent_main false true sigma c t -let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t +let dependent sigma c t = dependent_main false sigma c t +let dependent_no_evar sigma c t = dependent_main true sigma c t let dependent_in_decl sigma a decl = let open NamedDecl in diff --git a/engine/termops.mli b/engine/termops.mli index ef3cb91be..3b0c4bba6 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -108,8 +108,6 @@ val free_rels : Evd.evar_map -> constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) val dependent : Evd.evar_map -> constr -> constr -> bool val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool -val dependent_univs : Evd.evar_map -> constr -> constr -> bool -val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list diff --git a/engine/universes.ml b/engine/universes.ml index c74467405..70ed6311e 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -242,7 +242,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) let cstrs = ref accu in - let eq_universes strict = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -251,45 +251,12 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = | None -> false | Some accu -> cstrs := accu; true in - let rec eq_constr' m n = - Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n in - let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None -let compare_head_gen_proj env equ eqs eqc' m n = - match kind m, kind n with - | Proj (p, c), App (f, args) - | App (f, args), Proj (p, c) -> - (match kind f with - | Const (p', u) when Constant.equal (Projection.constant p) p' -> - let pb = Environ.lookup_projection p env in - let npars = pb.Declarations.proj_npars in - if Array.length args == npars + 1 then - eqc' c args.(npars) - else false - | _ -> false) - | _ -> Constr.compare_head_gen equ eqs eqc' m n - -let eq_constr_universes_proj env m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n - in - let res = eq_constr' m n in - res, !cstrs - (* Generator of levels *) type universe_id = DirPath.t * int diff --git a/engine/universes.mli b/engine/universes.mli index 8e6b8f60c..a86b9779b 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -102,10 +102,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained - (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) diff --git a/kernel/constr.ml b/kernel/constr.ml index 2cbcdd76e..ba7fecadf 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -654,6 +654,11 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = CArray.Fun1.smartmap f l' bl in mkCoFix (ln,(lna,tl',bl')) +type instance_compare_fn = global_reference -> int -> + Univ.Instance.t -> Univ.Instance.t -> bool + +type constr_compare_fn = int -> constr -> constr -> bool + (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose the structure [c2]) using [eq] to compare the immediate subterms of @@ -665,38 +670,42 @@ let map_with_binders g f l c0 = match kind c0 with optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) -let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = +let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = match kind1 t1, kind2 t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1,_,_), _ -> leq c1 t2 - | _, Cast (c2,_,_) -> leq t1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2 - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2 - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2 + | Cast (c1, _, _), _ -> leq nargs c1 t2 + | _, Cast (c2, _, _) -> leq nargs t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2 - | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2)) - | App (c1,l1), App (c2,l2) -> - Int.equal (Array.length l1) (Array.length l2) && - eq c1 c2 && Array.equal_norefl eq l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2 - | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 - | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 - | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 + | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 + | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) + | App (c1, l1), App (c2, l2) -> + let len = Array.length l1 in + Int.equal len (Array.length l2) && + eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 + | Const (c1,u1), Const (c2,u2) -> + (* The args length currently isn't used but may as well pass it. *) + Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2 + | Construct (c1,u1), Construct (c2,u2) -> + eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2 + eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> - Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 - && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 + Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 + && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 + Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ - | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ - | CoFix _), _ -> false + | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ + | CoFix _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -704,8 +713,8 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = application associativity, binders name and Cases annotations are not taken into account *) -let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 = - compare_head_gen_leq_with kind kind eq_universes leq_sorts eq leq t1 t2 +let compare_head_gen_leq leq_universes leq_sorts eq leq t1 t2 = + compare_head_gen_leq_with kind kind leq_universes leq_sorts eq leq t1 t2 (* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to @@ -722,7 +731,7 @@ let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 = let compare_head_gen eq_universes eq_sorts eq t1 t2 = compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2 -let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal +let compare_head = compare_head_gen (fun _ _ -> Univ.Instance.equal) Sorts.equal (*******************************) (* alpha conversion functions *) @@ -730,41 +739,41 @@ let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal (* alpha conversion : ignore print names and casts *) -let rec eq_constr m n = - (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n +let rec eq_constr nargs m n = + (m == n) || compare_head_gen (fun _ _ -> Instance.equal) Sorts.equal eq_constr nargs m n -let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) +let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n - in compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n + in compare_head_gen eq_universes eq_sorts eq_constr' 0 m n let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let rec compare_leq m n = - compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n + let rec compare_leq nargs m n = + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + compare_leq 0 m n let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict = UGraph.check_eq_instances univs in + let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -774,17 +783,17 @@ let eq_constr_univs_infer univs m n = (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in + let res = compare_head_gen eq_universes eq_sorts eq_constr' 0 m n in res, !cstrs let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty else let cstrs = ref Constraint.empty in - let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in + let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else @@ -802,19 +811,17 @@ let leq_constr_univs_infer univs m n = (cstrs := Univ.enforce_leq u1 u2 !cstrs; true) in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n + let rec eq_constr' nargs m n = + m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n in - let rec compare_leq m n = - compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - let res = compare_leq m n in + let rec compare_leq nargs m n = + compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' nargs m n + and leq_constr' nargs m n = m == n || compare_leq nargs m n in + let res = compare_leq 0 m n in res, !cstrs -let always_true _ _ = true - let rec eq_constr_nounivs m n = - (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n + (m == n) || compare_head_gen (fun _ _ _ _ -> true) (fun _ _ -> true) (fun _ -> eq_constr_nounivs) 0 m n let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= diff --git a/kernel/constr.mli b/kernel/constr.mli index f7e4eecba..98c0eaa28 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -402,31 +402,38 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +type constr_compare_fn = int -> constr -> constr -> bool + (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool +val compare_head : constr_compare_fn -> constr_compare_fn + +(** Convert a global reference applied to 2 instances. The int says + how many arguments are given (as we can only use cumulativity for + fully applied inductives/constructors) .*) +type instance_compare_fn = global_reference -> int -> + Univ.Instance.t -> Univ.Instance.t -> bool -(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed, [u] to compare universe - instances (the first boolean tells if they belong to a Constant.t), [s] to - compare sorts; Cast's, binders name and Cases annotations are not taken - into account *) +(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to + compare the immediate subterms of [c1] of [c2] if needed, [u] to + compare universe instances, [s] to compare sorts; Cast's, binders + name and Cases annotations are not taken into account *) -val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn val compare_head_gen_leq_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) @@ -435,10 +442,10 @@ val compare_head_gen_leq_with : val compare_head_gen_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for @@ -447,11 +454,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen_leq : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + constr_compare_fn (** {6 Hashconsing} *) diff --git a/kernel/names.ml b/kernel/names.ml index 6fa44c061..a3aa71f24 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -701,6 +701,12 @@ end module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) +type global_reference = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t diff --git a/kernel/names.mli b/kernel/names.mli index 209826c1f..ffd96781b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -500,6 +500,13 @@ val constructor_user_hash : constructor -> int val constructor_syntactic_ord : constructor -> constructor -> int val constructor_syntactic_hash : constructor -> int +(** {6 Global reference is a kernel side type for all references together } *) +type global_reference = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t diff --git a/kernel/term.mli b/kernel/term.mli index ba521978e..7cb3b662d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -477,7 +477,7 @@ val iter_constr_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit [@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] -val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool +val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool [@@ocaml.deprecated "Alias for [Constr.compare_head]"] type constr = Constr.constr diff --git a/library/globnames.ml b/library/globnames.ml index 8b1a51377..2fa3adba2 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -15,7 +15,7 @@ open Mod_subst open Libnames (*s Global reference is a kernel side type for all references together *) -type global_reference = +type global_reference = Names.global_reference = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) diff --git a/library/globnames.mli b/library/globnames.mli index 017b7386d..f2b88b870 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -14,7 +14,7 @@ open Constr open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) -type global_reference = +type global_reference = Names.global_reference = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 7d43f1986..61632e388 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -859,8 +859,9 @@ END let eq_constr x y = Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes evd x y with + match EConstr.eq_constr_universes env evd x y with | Some _ -> Proofview.tclUNIT () | None -> Tacticals.New.tclFAIL 0 (str "Not equal") end diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index fe2e86a48..130aa8cd7 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -352,10 +352,34 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) -let check_leq_inductives evd cumi u u' = - let u = EConstr.EInstance.kind evd u in - let u' = EConstr.EInstance.kind evd u' in - Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u') +let try_soft evd u u' = + let open Universes in + let make = Univ.Universe.make in + try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u')) + with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd + +(* Add equality constraints for covariant/invariant positions. For + irrelevant positions, unify universes when flexible. *) +let compare_cumulative_instances evd variances u u' = + let cstrs = Univ.Constraint.empty in + let soft = [] in + let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> + let open Univ.Variance in + match v with + | Irrelevant -> cstrs, (u,u')::soft + | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) + (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') + in + match Evd.add_constraints evd cstrs with + | evd -> + Success (List.fold_left (fun evd (u,u') -> try_soft evd u u') evd soft) + | exception Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + +(* We should only compare constructors at convertible types, so this + is only an opportunity to unify universes. *) +let compare_constructor_instances evd u u' = + Array.fold_left2 try_soft + evd (Univ.Instance.to_array u) (Univ.Instance.to_array u') let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in @@ -446,103 +470,56 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let check_strict () = - let univs = EConstr.eq_constr_universes evd term term' in - match univs with - | Some univs -> - begin - let cstrs = Universes.to_constraints (Evd.universes evd) univs in - try Success (Evd.add_constraints evd cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) - end - | None -> - UnifFailure (evd, NotSameHead) + let check_strict evd u u' = + let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) in - let first_try_strict_check cond u u' try_subtyping_constraints = - if cond then - let univs = EConstr.eq_constr_universes evd term term' in - match univs with - | Some univs -> - begin - let cstrs = Universes.to_constraints (Evd.universes evd) univs in - try Success (Evd.add_constraints evd cstrs) - with Univ.UniverseInconsistency p -> try_subtyping_constraints () - end - | None -> - UnifFailure (evd, NotSameHead) - else - UnifFailure (evd, NotSameHead) - in - let compare_heads evd = + let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with - | Const (c, u), Const (c', u') -> - check_strict () - | Ind (ind, u), Ind (ind', u') -> - let check_subtyping_constraints () = - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - begin - let mind = Environ.lookup_mind (fst ind) env in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - UnifFailure (evd, NotSameHead) - | Declarations.Cumulative_ind cumi -> - begin - let num_param_arity = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs - in - if not (num_param_arity = nparamsaplied - && num_param_arity = nparamsaplied') then - UnifFailure (evd, NotSameHead) - else - begin - let evd' = check_leq_inductives evd cumi u u' in - Success (check_leq_inductives evd' cumi u' u) - end - end + | Const (c, u), Const (c', u') when Constant.equal c c' -> + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + check_strict evd u u' + | Const _, Const _ -> UnifFailure (evd, NotSameHead) + | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_universes with + | Monomorphic_ind _ -> assert false + | Polymorphic_ind _ -> check_strict evd u u' + | Cumulative_ind cumi -> + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let needed = Reduction.inductive_cumulativity_arguments (mind,i) in + if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) + then check_strict evd u u' + else + compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u' end - in - first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints - | Construct (cons, u), Construct (cons', u') -> - let check_subtyping_constraints () = - let ind, ind' = fst cons, fst cons' in - let j, j' = snd cons, snd cons' in - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - let mind = Environ.lookup_mind (fst ind) env in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> - UnifFailure (evd, NotSameHead) - | Declarations.Cumulative_ind cumi -> - begin - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs - in - nparamsctxt + - mind.Declarations.mind_packets.(snd ind). - Declarations.mind_consnrealargs.(j - 1) - in - if not (num_cnstr_args = nparamsaplied - && num_cnstr_args = nparamsaplied') then - UnifFailure (evd, NotSameHead) + | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) + | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') + when Names.eq_constructor cons cons' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_universes with + | Monomorphic_ind _ -> assert false + | Polymorphic_ind _ -> check_strict evd u u' + | Cumulative_ind cumi -> + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in + if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) + then check_strict evd u u' else - begin - (** Both constructors should be liftable to the same supertype - at which we compare them, but we don't have access to that type in - untyped unification. We hence try to enforce that one is lower - than the other, also unifying more universes in the process. - If this fails we just leave the universes as is, as in conversion. *) - try Success (check_leq_inductives evd cumi u u') - with Univ.UniverseInconsistency _ -> - try Success (check_leq_inductives evd cumi u' u) - with Univ.UniverseInconsistency e -> Success evd - end - end - in - first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints + Success (compare_constructor_instances evd u u') + end + | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) | _, _ -> anomaly (Pp.str "") in ise_and evd [(fun i -> @@ -789,7 +766,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty allow this identification (first-order unification of universes). Otherwise fallback to unfolding. *) - let univs = EConstr.eq_constr_universes evd term1 term2 in + let univs = EConstr.eq_constr_universes env evd term1 term2 in match univs with | Some univs -> ise_and i [(fun i -> @@ -1096,7 +1073,7 @@ let apply_on_subterm env evdref f c t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) - let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with + let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with | None -> false | Some cstr -> try ignore (Evd.add_universe_constraints !evdref cstr); true diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c9030be2d..96d80741a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1337,7 +1337,7 @@ type conv_fun_bool = let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = let evdref = ref evd in - let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with + let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with | None -> false | Some cstr -> try ignore (Evd.add_universe_constraints !evdref cstr); true diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 44a69d1c1..0a28f1fb8 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -698,7 +698,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> - let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in + let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with | Some csts -> let subst = Universes.Constraints.fold (fun (l,d,r) acc -> @@ -1332,9 +1332,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) let b, sigma = let ans = if pb == Reduction.CUMUL then - EConstr.leq_constr_universes sigma x y + EConstr.leq_constr_universes env sigma x y else - EConstr.eq_constr_universes sigma x y + EConstr.eq_constr_universes env sigma x y in let ans = match ans with | None -> None diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f4269a2c5..1cd8d3940 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -568,10 +568,10 @@ let force_eqs c = Universes.Constraints.add c' acc) c Universes.Constraints.empty -let constr_cmp pb sigma flags t u = +let constr_cmp pb env sigma flags t u = let cstrs = - if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u - else EConstr.leq_constr_universes sigma t u + if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u + else EConstr.leq_constr_universes env sigma t u in match cstrs with | Some cstrs -> @@ -736,7 +736,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Evar (evk,_ as ev), Evar (evk',_) when not (Evar.Set.mem evk flags.frozen_evars) && Evar.equal evk evk' -> - let sigma',b = constr_cmp cv_pb sigma flags cM cN in + let sigma',b = constr_cmp cv_pb env sigma flags cM cN in if b then sigma',metasubst,evarsubst else @@ -918,7 +918,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - let sigma', b = constr_cmp cv_pb sigma flags cM cN in + let sigma', b = constr_cmp cv_pb env sigma flags cM cN in if b then (sigma', metas, evars) else try reduce curenvnb pb opt substn cM cN @@ -1087,7 +1087,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n - | _ -> constr_cmp cv_pb sigma flags m n in + | _ -> constr_cmp cv_pb env sigma flags m n in if b then Some sigma else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with | Some (cv_id, cv_k), (dl_id, dl_k) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 12aef852d..b111fd1ef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4824,9 +4824,9 @@ let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n) is solved by tac *) (** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl evd d1 d2 = +let interpretable_as_section_decl env evd d1 d2 = let open Context.Named.Declaration in - let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes !sigma c1 c2 with + let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with | None -> false | Some cstr -> try ignore (Evd.add_universe_constraints !sigma cstr); true @@ -4890,6 +4890,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let open Tacmach.New in let open Proofview.Notations in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in @@ -4899,7 +4900,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = (fun d (s1,s2) -> let id = NamedDecl.get_id d in if mem_named_context_val id current_sign && - interpretable_as_section_decl evdref (lookup_named_val id current_sign) d + interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in diff --git a/test-suite/bugs/closed/6661.v b/test-suite/bugs/closed/6661.v new file mode 100644 index 000000000..e88a3704d --- /dev/null +++ b/test-suite/bugs/closed/6661.v @@ -0,0 +1,259 @@ +(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *) +(* + The Coq Proof Assistant, version 8.7.1 (January 2018) + compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0 + from commit 391bb5e196901a3a9426295125b8d1c700ab6992 + *) + + +Require Export Coq.Init.Notations. +Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity). +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Reserved Notation "p @ q" (at level 60, right associativity). +Reserved Notation "! p " (at level 50). + +Monomorphic Universe uu. +Monomorphic Universe uu0. +Monomorphic Universe uu1. +Constraint uu0 < uu1. + +Global Set Universe Polymorphism. +Global Set Polymorphic Inductive Cumulativity. +Global Unset Universe Minimization ToSet. + +Notation UU := Type (only parsing). +Notation UU0 := Type@{uu0} (only parsing). + +Global Set Printing Universes. + + Inductive unit : UU0 := tt : unit. + +Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a. +Hint Resolve idpath : core . +Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope. + +Set Primitive Projections. +Set Nonrecursive Elimination Schemes. + +Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i} + := tpair { pr1 : T; pr2 : P pr1 }. + +Arguments tpair {_} _ _ _. +Arguments pr1 {_ _} _. +Arguments pr2 {_ _} _. + +Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..)) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. + induction xy as [x y]. + exact x. +Defined. + +Unset Automatic Introduction. + +Definition idfun (T : UU) := λ t:T, t. + +Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. +Proof. + intros. induction e1. exact e2. +Defined. + +Hint Resolve @pathscomp0 : pathshints. + +Notation "p @ q" := (pathscomp0 p q). + +Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a. +Proof. + intros. induction e. exact (idpath _). +Defined. + +Notation "! p " := (pathsinv0 p). + +Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1} + (e: t1 = t2) : f t1 = f t2. +Proof. + intros. induction e. exact (idpath _). +Defined. + +Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') : + f x y = f x' y'. +Proof. + intros. induction ex. induction ey. exact (idpath _). +Defined. + + +Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X} + (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) : + maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2. +Proof. + intros. induction e1. induction e2. exact (idpath _). +Defined. + +Definition maponpathsinv0 {X Y : UU} (f : X -> Y) + {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e). +Proof. + intros. induction e. exact (idpath _). +Defined. + + + +Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') : + ∑ (f : P x -> P x'), + ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)), + ∏ (pp : P x), maponpaths pr1 (ee pp) = e. +Proof. + intros. induction e. + split with (idfun (P x)). + split with (λ p, idpath _). + unfold maponpaths. simpl. + intro. exact (idpath _). +Defined. + +Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X} + (e : x = x') : P x -> P x' := pr1 (constr1 P e). + +Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2} + (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2. +Proof. + intros. induction p. induction q. exact (idpath _). +Defined. + +Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr. + +Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'. +Proof. + intros. + induction is as [y fe]. + exact (fe x @ !(fe x')). +Defined. + + +Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y). + +Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y} + (x : X) (e : f x = y) : hfiber f y := + tpair _ x e. + +Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t. + +Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t + := tpair _ t' e. + +Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2. +Proof. + intros. + induction c1 as [x0 x]. + induction x. + induction c2 as [x1 y]. + induction y. + exact (idpath _). +Defined. + +Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} := + ∏ y : Y, iscontr (hfiber f y). + +Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'. +Proof. + intros. induction x. induction x'. exact (idpath _). +Defined. + +Lemma unitl0 : tt = tt -> coconustot _ tt. +Proof. + intros e. exact (coconustotpair unit e). +Defined. + +Lemma unitl1: coconustot _ tt -> tt = tt. +Proof. + intro cp. induction cp as [x t]. induction x. exact t. +Defined. + +Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e. +Proof. + intros. unfold unitl0. simpl. exact (idpath _). +Defined. + +Lemma unitl3: ∏ e : tt = tt, e = idpath tt. +Proof. + intros. + + assert (e0 : unitl0 (idpath tt) = unitl0 e). + { simple refine (connectedcoconustot _ _). } + + set (e1 := maponpaths unitl1 e0). + + exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))). +Defined. + +Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x'). +Proof. + intros. + split with (isProofIrrelevantUnit x x'). + intros e'. + induction x. + induction x'. + simpl. + apply unitl3. +Qed. + +Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2. +Proof. + intros. + simple refine (proofirrelevancecontr _ _ _). + exact (iscontrpathsinunit tt tt). +Qed. + +Section isweqcontrtounit. + + Universe i. + + (* To see the bug, run it both with and without this constraint: *) + + (* Constraint uu0 < i. *) + + (* Without this constraint, we get i = uu0 in the next definition *) + Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt). + Proof. + intros. intro y. induction y. + induction is as [c h]. + split with (hfiberpair@{i i i} _ c (idpath tt)). + intros ha. + induction ha as [x e]. + simple refine (two_arg_paths_f (h x) _). + simple refine (ifcontrthenunitl0 _ _). + Defined. + + (* + Explanation of the bug: + + With the constraint uu0 < i above we get: + + |= uu0 <= bug.3 + uu0 <= i + uu1 <= i + i <= bug.3 + + from this print statement: *) + + Print isweqcontrtounit. + + (* + + Without the constraint uu0 < i above we get: + + |= i <= bug.3 + uu0 = i + + Since uu0 = i is not inferred when we impose the constraint uu0 < i, + it is invalid to infer it when we don't. + + *) + + Context (X : Type@{uu1}). + + Check (@isweqcontrtounit X). (* detect a universe inconsistency *) + +End isweqcontrtounit. diff --git a/test-suite/bugs/closed/6775.v b/test-suite/bugs/closed/6775.v new file mode 100644 index 000000000..206df23bc --- /dev/null +++ b/test-suite/bugs/closed/6775.v @@ -0,0 +1,43 @@ +(* Issue caused and fixed during the lifetime of #6775: unification + failing on partially applied cumulative inductives. *) + +Set Universe Polymorphism. + +Set Polymorphic Inductive Cumulativity. + +Unset Elimination Schemes. + +Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Arguments inverse {A x y} p : simpl nomatch. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Arguments concat {A x y z} p q : simpl nomatch. + +Notation "1" := idpath. + +Reserved Notation "p @ q" (at level 20). +Notation "p @ q" := (concat p q). + +Reserved Notation "p ^" (at level 3, format "p '^'"). +Notation "p ^" := (inverse p). + +Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) : + (p @ q^) @ q = p + := + (match q as i return forall p, (p @ i^) @ i = p with + idpath => + fun p => + match p with idpath => 1 end + end) p. diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index d63a3548e..5f4500715 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -25,7 +25,7 @@ Section ListLower. End ListLower. -Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. Proof. reflexivity. Qed. (* I disable these tests because cqochk can't process them when compiled with diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 4dda36042..0394ea340 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -10,40 +10,16 @@ Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. -Section ListLift. - Universe i j. - - Constraint i < j. - - Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. - -End ListLift. +Definition LiftL@{k i j|k <= i, k <= j} {A:Type@{k}} : List@{i} A -> List@{j} A := fun x => x. Lemma LiftL_Lem A (l : List A) : l = LiftL l. Proof. reflexivity. Qed. -Section ListLower. - Universe i j. - - Constraint i < j. - - Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. - -End ListLower. - -Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. -Proof. reflexivity. Qed. - Inductive Tp := tp : Type -> Tp. -Section TpLift. - Universe i j. +Definition LiftTp@{i j|i <= j} : Tp@{i} -> Tp@{j} := fun x => x. - Constraint i < j. - - Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. - -End TpLift. +Fail Definition LowerTp@{i j|j < i} : Tp@{i} -> Tp@{j} := fun x => x. Record Tp' := { tp' : Tp }. @@ -51,22 +27,12 @@ Definition CTp := Tp. (* here we have to reduce a constant to infer the correct subtyping. *) Record Tp'' := { tp'' : CTp }. -Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x. -Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x. +Definition LiftTp'@{i j|i <= j} : Tp'@{i} -> Tp'@{j} := fun x => x. +Definition LiftTp''@{i j|i <= j} : Tp''@{i} -> Tp''@{j} := fun x => x. Lemma LiftC_Lem (t : Tp) : LiftTp t = t. Proof. reflexivity. Qed. -Section TpLower. - Universe i j. - - Constraint i < j. - - Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. - -End TpLower. - - Section subtyping_test. Universe i j. Constraint i < j. @@ -82,14 +48,8 @@ Record B (X : A) : Type := { b : X; }. NonCumulative Inductive NCList (A: Type) := ncnil | nccons : A -> NCList A -> NCList A. -Section NCListLift. - Universe i j. - - Constraint i < j. - - Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x. - -End NCListLift. +Fail Definition LiftNCL@{k i j|k <= i, k <= j} {A:Type@{k}} + : NCList@{i} A -> NCList@{j} A := fun x => x. Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. @@ -114,7 +74,7 @@ Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'} : Arrow@{i j} -> Arrow@{i' j'} := fun x => x. -Definition arrow_lift@{i i' j j' | i' = i, j < j'} +Definition arrow_lift@{i i' j j' | i' = i, j <= j'} : Arrow@{i j} -> Arrow@{i' j'} := fun x => x. diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4f16e1cf6..064e40b9b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1,5 +1,4 @@ open Printf -open Globnames open Libobject open Entries open Decl_kinds |