From 8bba34395e520ac606fc3efd0a875699fe968e69 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 20 Sep 2015 00:08:35 +0200 Subject: Better debug printers for module paths. Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now. --- kernel/names.ml | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b6389..9e4e8cd61d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -204,7 +204,7 @@ struct DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = - "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" + "<"^DirPath.to_string p ^"#" ^ s ^"#"^ string_of_int i^">" let compare (x : t) (y : t) = if x == y then 0 @@ -282,6 +282,11 @@ module ModPath = struct | MPbound uid -> MBId.to_string uid | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l + let rec debug_to_string = function + | MPfile sl -> DirPath.to_string sl + | MPbound uid -> MBId.debug_to_string uid + | MPdot (mp,l) -> debug_to_string mp ^ "." ^ Label.to_string l + (** we compare labels first if both are MPdots *) let rec compare mp1 mp2 = if mp1 == mp2 then 0 @@ -375,12 +380,16 @@ module KerName = struct let modpath kn = kn.modpath let label kn = kn.knlabel - let to_string kn = + let to_string_gen mp_to_string kn = let dp = if DirPath.is_empty kn.dirpath then "." else "#" ^ DirPath.to_string kn.dirpath ^ "#" in - ModPath.to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel + mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel + + let to_string kn = to_string_gen ModPath.to_string kn + + let debug_to_string kn = to_string_gen ModPath.debug_to_string kn let print kn = str (to_string kn) @@ -500,9 +509,9 @@ module KerPair = struct let print kp = str (to_string kp) let debug_to_string = function - | Same kn -> "(" ^ KerName.to_string kn ^ ")" + | Same kn -> "(" ^ KerName.debug_to_string kn ^ ")" | Dual (knu,knc) -> - "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")" + "(" ^ KerName.debug_to_string knu ^ "," ^ KerName.debug_to_string knc ^ ")" let debug_print kp = str (debug_to_string kp) -- cgit v1.2.3 From e2a67cbbbd17fa262b37903a97b0adf2d109bf06 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 11:00:44 +0100 Subject: COMMENTS: added to the "Names" module. --- kernel/names.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 9e4e8cd61d..0de752c7c5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -23,6 +23,7 @@ open Util (** {6 Identifiers } *) +(** Representation and operations on identifiers. *) module Id = struct type t = string @@ -74,10 +75,12 @@ struct end - +(** Representation and operations on identifiers that are allowed to be anonymous + (i.e. "_" in concrete syntax). *) module Name = struct - type t = Name of Id.t | Anonymous + type t = Anonymous (** anonymous identifier *) + | Name of Id.t (** non-anonymous identifier *) let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 @@ -117,8 +120,8 @@ struct end -type name = Name.t = Name of Id.t | Anonymous (** Alias, to import constructors. *) +type name = Name.t = Anonymous | Name of Id.t (** {6 Various types based on identifiers } *) -- cgit v1.2.3 From 8a4a8758075e09da298762da1a035a5afac4d88b Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 21 Dec 2015 11:37:06 +0100 Subject: COMMENTS: added to the "Names.inductive" and "Names.constructor" types. --- kernel/names.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 0de752c7c5..d1e2c8afee 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -585,11 +585,16 @@ module Mindmap = HMap.Make(MutInd.CanOrd) module Mindset = Mindmap.Set module Mindmap_env = HMap.Make(MutInd.UserOrd) -(** Beware: first inductive has index 0 *) -(** Beware: first constructor has index 1 *) - -type inductive = MutInd.t * int -type constructor = inductive * int +(** Designation of a (particular) inductive type. *) +type inductive = MutInd.t (* the name of the inductive type *) + * int (* the position of this inductive type + within the block of mutually-recursive inductive types. + BEWARE: indexing starts from 0. *) + +(** Designation of a (particular) constructor of a (particular) inductive type. *) +type constructor = inductive (* designates the inductive type *) + * int (* the index of the constructor + BEWARE: indexing starts from 1. *) let ind_modpath (mind,_) = MutInd.modpath mind let constr_modpath (ind,_) = ind_modpath ind -- 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/names.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b6389..f5d954e9ce 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool Names.Name.is_name : Names.Name.t -> bool They enable us to write a more compact code. (example: commit "99633f4" in "relation-extraction" module of "coq-contribs"). --- kernel/names.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 02587bad9b..0aa26fb9cc 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -82,6 +82,12 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let is_anonymous = function + | Anonymous -> true + | Name _ -> false + + let is_name = not % is_anonymous + let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 | Name id1, Name id2 -> Id.compare id1 id2 -- cgit v1.2.3 From 920f1548e9245ddfc8b923c5039a5e09dc0c87d4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:53:21 +0200 Subject: Adding eq/compare/hash for syntactic view at constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same. --- kernel/names.ml | 42 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index f5d954e9ce..e9cb9fd74c 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -477,7 +477,7 @@ module KerPair = struct | Dual (kn,_) -> kn let same kn = Same kn - let make knu knc = if knu == knc then Same knc else Dual (knu,knc) + let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc) let make1 = same let make2 mp l = same (KerName.make2 mp l) @@ -524,6 +524,23 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end + module SyntacticOrd = struct + type t = kernel_pair + let compare x y = match x, y with + | Same knx, Same kny -> KerName.compare knx kny + | Dual (knux,kncx), Dual (knuy,kncy) -> + let c = KerName.compare knux knuy in + if not (Int.equal c 0) then c + else KerName.compare kncx kncy + | Same _, _ -> -1 + | Dual _, _ -> 1 + let equal x y = x == y || compare x y = 0 + let hash = function + | Same kn -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) + end + (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal let hash = CanOrd.hash @@ -590,6 +607,8 @@ let index_of_constructor (ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 +let eq_syntactic_ind (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 let ind_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in @@ -597,15 +616,22 @@ let ind_ord (m1, i1) (m2, i2) = let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c +let ind_syntactic_ord (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c let ind_hash (m, i) = Hashset.Combine.combine (MutInd.hash m) (Int.hash i) let ind_user_hash (m, i) = Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) +let ind_syntactic_hash (m, i) = + Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let eq_user_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_user_ind ind1 ind2 +let eq_syntactic_constructor (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && eq_syntactic_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in @@ -613,11 +639,16 @@ let constructor_ord (ind1, j1) (ind2, j2) = let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c +let constructor_syntactic_ord (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c let constructor_hash (ind, i) = Hashset.Combine.combine (ind_hash ind) (Int.hash i) let constructor_user_hash (ind, i) = Hashset.Combine.combine (ind_user_hash ind) (Int.hash i) +let constructor_syntactic_hash (ind, i) = + Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i) module InductiveOrdered = struct type t = inductive @@ -805,6 +836,15 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c + module SyntacticOrd = struct + type t = constant * bool + let compare (c, b) (c', b') = + if b = b' then Constant.SyntacticOrd.compare c c' else -1 + let equal (c, b as x) (c', b' as x') = + x == x' || b = b' && Constant.SyntacticOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c + end + module Self_Hashcons = struct type _t = t -- 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/names.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index e9cb9fd74c..d8e91cfab7 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -102,7 +102,7 @@ struct let hashcons hident = function | Name id -> Name (hident id) | n -> n - let equal n1 n2 = + let eq n1 n2 = n1 == n2 || match (n1,n2) with | (Name id1, Name id2) -> id1 == id2 @@ -236,7 +236,7 @@ struct type t = _t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) - let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = + let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = hash @@ -327,7 +327,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec equal d1 d2 = + let rec eq d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 @@ -423,7 +423,7 @@ module KerName = struct let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } - let equal kn1 kn2 = + let eq kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel let hash = hash @@ -552,7 +552,7 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let equal x y = (* physical comparison on subterms *) + let eq x y = (* physical comparison on subterms *) x == y || match x,y with | Same x, Same y -> x == y @@ -693,7 +693,7 @@ module Hind = Hashcons.Make( type t = inductive type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) - let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 + let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = ind_hash end) @@ -702,7 +702,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 + let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = constructor_hash end) @@ -851,7 +851,7 @@ struct type t = _t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) - let equal ((c,b) as x) ((c',b') as y) = + let eq ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') let hash = hash end -- cgit v1.2.3