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. --- kernel/constr.ml | 113 +++++++++++++++++++++++++++++------------------------- kernel/constr.mli | 47 +++++++++++++---------- kernel/names.ml | 6 +++ kernel/names.mli | 7 ++++ kernel/term.mli | 2 +- 5 files changed, 101 insertions(+), 74 deletions(-) (limited to 'kernel') 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 -- cgit v1.2.3