From 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 16 Feb 2018 15:44:44 +0100 Subject: Allow using cumulativity without forcing strict constraints. Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible. --- engine/eConstr.ml | 133 +++++++++++++++++++++++++++++++++++++-------------- engine/eConstr.mli | 7 ++- engine/termops.ml | 14 ++---- engine/termops.mli | 2 - engine/universes.ml | 41 ++-------------- engine/universes.mli | 4 -- 6 files changed, 110 insertions(+), 91 deletions(-) (limited to 'engine') 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. *) -- cgit v1.2.3