aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml166
1 files changed, 130 insertions, 36 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index b349ccb009..1f138581cc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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 check_soft x =
+ 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 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)
@@ -48,6 +55,11 @@ struct
let s = String.copy s in
String.hcons s
+ let of_string_soft s =
+ let () = check_soft ~warn:false s in
+ let s = String.copy s in
+ String.hcons s
+
let to_string id = String.copy id
let print id = str id
@@ -69,10 +81,21 @@ 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 mk_name id =
+ Name id
+
+ let is_anonymous = function
+ | Anonymous -> true
+ | Name _ -> false
+
+ let is_name = is_anonymous %> not
let compare n1 n2 = match n1, n2 with
| Anonymous, Anonymous -> 0
@@ -97,7 +120,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
@@ -112,8 +135,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 } *)
@@ -199,7 +222,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
@@ -231,7 +254,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
@@ -277,6 +300,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
@@ -322,7 +350,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
@@ -370,12 +398,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)
@@ -418,7 +450,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
@@ -448,6 +480,9 @@ module KNset = KNmap.Set
- when user and canonical parts differ, we cannot be in a section
anymore, hence the dirpath must be empty
- two pairs with the same user part should have the same canonical part
+ in a given environment (though with backtracking, the hash-table can
+ contains pairs with same user part but different canonical part from
+ a previous state of the session)
Note: since most of the time the canonical and user parts are equal,
we handle this case with a particular constructor to spare some memory *)
@@ -469,7 +504,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)
@@ -492,14 +527,14 @@ 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)
(** For ordering kernel pairs, both user or canonical parts may make
- sense, according to your needs : user for the environments, canonical
+ sense, according to your needs: user for the environments, canonical
for other uses (ex: non-logical things). *)
module UserOrd = struct
@@ -516,16 +551,26 @@ module KerPair = struct
let hash x = KerName.hash (canonical x)
end
- (** Default comparison is on the canonical part *)
- let equal = CanOrd.equal
-
- (** Hash-consing : we discriminate only on the user part, since having
- the same user part implies having the same canonical part
- (invariant of the system). *)
+ 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
- let hash = function
- | Same kn -> KerName.hash kn
- | Dual (kn, _) -> KerName.hash kn
+ (** Default (logical) comparison and hash is on the canonical part *)
+ let equal = CanOrd.equal
+ let hash = CanOrd.hash
module Self_Hashcons =
struct
@@ -534,8 +579,20 @@ module KerPair = struct
let hashcons hkn = function
| Same kn -> Same (hkn kn)
| Dual (knu,knc) -> make (hkn knu) (hkn knc)
- let equal x y = (user x) == (user y)
- let hash = hash
+ let eq x y = (* physical comparison on subterms *)
+ x == y ||
+ match x,y with
+ | Same x, Same y -> x == y
+ | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
+ | (Same _ | Dual _), _ -> false
+ (** Hash-consing (despite having the same user part implies having
+ the same canonical part is a logical invariant of the system, it
+ is not necessarily an invariant in memory, so we treat kernel
+ names as they are syntactically for hash-consing) *)
+ let hash = function
+ | Same kn -> KerName.hash kn
+ | Dual (knu, knc) ->
+ Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
end
module HashKP = Hashcons.Make(Self_Hashcons)
@@ -547,7 +604,13 @@ end
module Constant = KerPair
module Cmap = HMap.Make(Constant.CanOrd)
+(** A map whose keys are constants (values of the {!Constant.t} type).
+ Keys are ordered wrt. "cannonical form" of the constant. *)
+
module Cmap_env = HMap.Make(Constant.UserOrd)
+(** A map whose keys are constants (values of the {!Constant.t} type).
+ Keys are ordered wrt. "user form" of the constant. *)
+
module Cpred = Predicate.Make(Constant.CanOrd)
module Cset = Cmap.Set
module Cset_env = Cmap_env.Set
@@ -560,24 +623,30 @@ 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
let ith_mutual_inductive (mind, _) i = (mind, i)
let ith_constructor_of_inductive ind i = (ind, i)
-let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u)
let inductive_of_constructor (ind, i) = ind
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
@@ -585,15 +654,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
@@ -601,11 +677,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
@@ -650,7 +731,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)
@@ -659,7 +740,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)
@@ -793,13 +874,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
@@ -815,6 +905,10 @@ struct
let map f (c, b as x) =
let c' = f c in
if c' == c then x else (c', b)
+
+ let to_string p = Constant.to_string (constant p)
+ let print p = Constant.print (constant p)
+
end
type projection = Projection.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 11:29:57 +0000