From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- kernel/names.ml | 113 +++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 91 insertions(+), 22 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index f5d954e9..1eb9a317 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 @@ -33,9 +34,15 @@ struct let hash = String.hash + let warn_invalid_identifier = + CWarnings.create ~name:"invalid-identifier" ~category:"parsing" + ~default:CWarnings.Disabled + (fun s -> str s) + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else if warn then Pp.msg_warning (str x) + if fatal then CErrors.error x else + if warn then warn_invalid_identifier x in Option.iter iter (Unicode.ident_refutation x) @@ -74,10 +81,18 @@ 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 is_anonymous = function + | Anonymous -> true + | Name _ -> false + + let is_name = not % is_anonymous let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 @@ -102,7 +117,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 @@ -117,8 +132,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 } *) @@ -204,7 +219,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 @@ -236,7 +251,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 @@ -282,6 +297,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 @@ -327,7 +347,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 eq d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 @@ -375,12 +395,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) @@ -423,7 +447,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 @@ -477,7 +501,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) @@ -500,9 +524,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) @@ -524,6 +548,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 @@ -535,7 +576,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 @@ -573,11 +614,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 *) +(** 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. *) -type inductive = MutInd.t * int -type constructor = inductive * int +(** 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 @@ -590,6 +636,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 +645,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 +668,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 @@ -662,7 +722,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) @@ -671,7 +731,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) @@ -805,13 +865,22 @@ 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 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