From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/constr.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index e2b1d3fd9c..753d188455 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -545,8 +545,8 @@ let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true else - let eq_universes _ = Univ.Instance.check_eq univs in - let eq_sorts s1 s2 = s1 == s2 || Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) 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 @@ -554,11 +554,11 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true else - let eq_universes _ = Univ.Instance.check_eq univs in + let eq_universes _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || - Univ.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let leq_sorts s1 s2 = s1 == s2 || - Univ.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in + 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 in @@ -571,12 +571,12 @@ 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 = Univ.Instance.check_eq univs in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) @@ -591,12 +591,12 @@ 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' = Univ.Instance.check_eq univs l l' in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true + if UGraph.check_eq univs u1 u2 then true else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in @@ -604,7 +604,7 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true + if UGraph.check_leq univs u1 u2 then true else (cstrs := Univ.enforce_leq u1 u2 !cstrs; true) -- cgit v1.2.3 From b88929d9d8de179a7e356cf9cbe2afef76f905a3 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 18 Dec 2015 10:07:53 +0100 Subject: COMMENTS: added to the "Constr.case_info" type. --- kernel/constr.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index 753d188455..c3aebada26 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -42,11 +42,15 @@ type case_printing = cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *) style : case_style } type case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*) - ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *) - ci_pp_info : case_printing (* not interpreted by the kernel *) + { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) + ci_npar : int; (* number of parameters of the above inductive type *) + ci_cstr_ndecls : int array; (* number of arguments of individual constructors + (numbers of parameters of the inductive type are excluded from the count) + (with let's) *) + ci_cstr_nargs : int array; (* number of arguments of individual constructors + (numbers of parameters of the inductive type are excluded from the count) + (w/o let's) *) + ci_pp_info : case_printing (* not interpreted by the kernel *) } (********************************************************************) -- cgit v1.2.3 From f8eb2ed4ddbe2199187696f51c42734014f4d9d0 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 21 Dec 2015 13:32:57 +0100 Subject: COMMENTS: of "Constr.case_info" type were updated. --- kernel/constr.ml | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index c3aebada26..3e7d888ede 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -41,15 +41,23 @@ type case_printing = { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *) style : case_style } + +(* INVARIANT: + * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs + * - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)), + * ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i) + *) type case_info = { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) ci_npar : int; (* number of parameters of the above inductive type *) - ci_cstr_ndecls : int array; (* number of arguments of individual constructors - (numbers of parameters of the inductive type are excluded from the count) - (with let's) *) - ci_cstr_nargs : int array; (* number of arguments of individual constructors - (numbers of parameters of the inductive type are excluded from the count) - (w/o let's) *) + ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines + the number of values that can be bound in a match-construct. + NOTE: parameters of the inductive type are therefore excluded from the count *) + ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines + the number of values that can be applied to the constructor, + in addition to the parameters of the related inductive type + NOTE: "lets" are therefore excluded from the count + NOTE: parameters of the inductive type are also excluded from the count *) ci_pp_info : case_printing (* not interpreted by the kernel *) } -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/constr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index e2b1d3fd9c..7e103b1dab 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* c1 == c2 && array_eqeq l1 l2 | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 - | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 - | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> - sp1 == sp2 && Int.equal i1 i2 && u1 == u2 - | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) -> - sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2 + | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 + | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> @@ -815,19 +813,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in - (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc)) + (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu)) - | Ind ((kn,i) as ind,u) -> + (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) + | Ind (ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_hash ind) hu)) - | Construct ((((kn,i),j) as c,u))-> + combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + | Construct (c,u) -> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_hash c) hu)) + combinesmall 11 (combine (constructor_syntactic_hash c) hu)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in -- cgit v1.2.3 From 2e557589920156fe84335e72c5e765347bcc7c9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 14:45:24 +0200 Subject: A patch renaming equal into eq in the module dealing with hash-consing, so as to avoid having too many kinds of equalities with same name. --- kernel/constr.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index 2a80cf2016..db457f28ce 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -755,10 +755,10 @@ let hasheq t1 t2 = once and for all the table we'll use for hash-consing all constr *) module HashsetTerm = - Hashset.Make(struct type t = constr let equal = hasheq end) + Hashset.Make(struct type t = constr let eq = hasheq end) module HashsetTermArray = - Hashset.Make(struct type t = constr array let equal = array_eqeq end) + Hashset.Make(struct type t = constr array let eq = array_eqeq end) let term_table = HashsetTerm.create 19991 (* The associative table to hashcons terms. *) @@ -928,7 +928,7 @@ struct List.equal (==) info1.ind_tags info2.ind_tags && Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags && info1.style == info2.style - let equal ci ci' = + let eq ci ci' = ci.ci_ind == ci'.ci_ind && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) @@ -970,7 +970,7 @@ module Hsorts = let hashcons huniv = function Prop c -> Prop c | Type u -> Type (huniv u) - let equal s1 s2 = + let eq s1 s2 = s1 == s2 || match (s1,s2) with (Prop c1, Prop c2) -> c1 == c2 -- cgit v1.2.3