summaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /kernel/names.ml
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml285
1 files changed, 172 insertions, 113 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 642f5562..8c228404 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1,35 +1,34 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: names.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting
+ parts of file initial.ml from CoC V4.8, Dec 1988, by Gérard Huet,
+ Thierry Coquand and Christine Paulin *)
+(* Hash-consing by Bruno Barras in Feb 1998 *)
+(* Extra functions for splitting/generation of identifiers by Hugo Herbelin *)
+(* Restructuration by Jacek Chrzaszcz as part of the implementation of
+ the module system, Aug 2002 *)
+(* Abstraction over the type of constant for module inlining by Claudio
+ Sacerdoti, Nov 2004 *)
+(* Miscellaneous features or improvements by Hugo Herbelin,
+ Élie Soubiran, ... *)
open Pp
open Util
-(*s Identifiers *)
+(** {6 Identifiers } *)
type identifier = string
-let id_ord = Pervasives.compare
-
let id_of_string s = check_ident_soft s; String.copy s
-
let string_of_id id = String.copy id
-(* Hash-consing of identifier *)
-module Hident = Hashcons.Make(
- struct
- type t = string
- type u = string -> string
- let hash_sub hstr id = hstr id
- let equal id1 id2 = id1 == id2
- let hash = Hashtbl.hash
- end)
+let id_ord = Pervasives.compare
module IdOrdered =
struct
@@ -38,15 +37,27 @@ module IdOrdered =
end
module Idset = Set.Make(IdOrdered)
-module Idmap = Map.Make(IdOrdered)
+module Idmap =
+struct
+ include Map.Make(IdOrdered)
+ exception Finded
+ let exists f m =
+ try iter (fun a b -> if f a b then raise Finded) m ; false
+ with |Finded -> true
+ let singleton k v = add k v empty
+end
module Idpred = Predicate.Make(IdOrdered)
-(* Names *)
+(** {6 Various types based on identifiers } *)
type name = Name of identifier | Anonymous
+type variable = identifier
-(* Dirpaths are lists of module identifiers. The actual representation
- is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *)
+(** {6 Directory paths = section names paths } *)
+
+(** Dirpaths are lists of module identifiers.
+ The actual representation is reversed to optimise sharing:
+ Coq.A.B is ["B";"A";"Coq"] *)
type module_ident = identifier
type dir_path = module_ident list
@@ -58,14 +69,17 @@ let repr_dirpath x = x
let empty_dirpath = []
+(** Printing of directory paths as ["coq_root.module.submodule"] *)
+
let string_of_dirpath = function
| [] -> "<>"
| sl -> String.concat "." (List.map string_of_id (List.rev sl))
+(** {6 Unique names for bound modules } *)
let u_number = ref 0
-type uniq_ident = int * string * dir_path
-let make_uid dir s = incr u_number;(!u_number,String.copy s,dir)
+type uniq_ident = int * identifier * dir_path
+let make_uid dir s = incr u_number;(!u_number,s,dir)
let debug_string_of_uid (i,s,p) =
"<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
let string_of_uid (i,s,p) =
@@ -76,30 +90,31 @@ module Umap = Map.Make(struct
let compare = Pervasives.compare
end)
-type label = string
-
type mod_bound_id = uniq_ident
let make_mbid = make_uid
let repr_mbid (n, id, dp) = (n, id, dp)
let debug_string_of_mbid = debug_string_of_uid
let string_of_mbid = string_of_uid
let id_of_mbid (_,s,_) = s
-let label_of_mbid (_,s,_) = s
+(** {6 Names of structure elements } *)
-let mk_label l = l
-let string_of_label = string_of_id
+type label = identifier
+let mk_label = id_of_string
+let string_of_label = string_of_id
+let pr_label l = str (string_of_label l)
let id_of_label l = l
let label_of_id id = id
module Labset = Idset
module Labmap = Idmap
+(** {6 The module part of the kernel name } *)
+
type module_path =
| MPfile of dir_path
| MPbound of mod_bound_id
- (* | MPapp of module_path * module_path *)
| MPdot of module_path * label
let rec check_bound_mp = function
@@ -110,12 +125,9 @@ let rec check_bound_mp = function
let rec string_of_mp = function
| MPfile sl -> string_of_dirpath sl
| MPbound uid -> string_of_uid uid
- (* | MPapp (mp1,mp2) ->
- "("^string_of_mp mp ^ " " ^
- string_of_mp mp^")"*)
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
-(* we compare labels first if both are MPdots *)
+(** we compare labels first if both are MPdots *)
let rec mp_ord mp1 mp2 = match (mp1,mp2) with
MPdot(mp1,l1), MPdot(mp2,l2) ->
let c = Pervasives.compare l1 l2 in
@@ -133,7 +145,12 @@ end
module MPset = Set.Make(MPord)
module MPmap = Map.Make(MPord)
-(* Kernel names *)
+let default_module_name = "If you see this, it's a bug"
+
+let initial_dir = make_dirpath [default_module_name]
+let initial_path = MPfile initial_dir
+
+(** {6 Kernel names } *)
type kernel_name = module_path * dir_path * label
@@ -147,11 +164,12 @@ let label kn =
let _,_,l = repr_kn kn in l
let string_of_kn (mp,dir,l) =
- string_of_mp mp ^ "#" ^ string_of_dirpath dir ^ "#" ^ string_of_label l
+ let str_dir = if dir = [] then "." else "#" ^ string_of_dirpath dir ^ "#"
+ in
+ string_of_mp mp ^ str_dir ^ string_of_label l
let pr_kn kn = str (string_of_kn kn)
-
let kn_ord kn1 kn2 =
let mp1,dir1,l1 = kn1 in
let mp2,dir2,l2 = kn2 in
@@ -165,100 +183,104 @@ let kn_ord kn1 kn2 =
else
MPord.compare mp1 mp2
-(* a constant name is a kernel name couple (kn1,kn2)
+module KNord = struct
+ type t = kernel_name
+ let compare = kn_ord
+end
+
+module KNmap = Map.Make(KNord)
+module KNpred = Predicate.Make(KNord)
+module KNset = Set.Make(KNord)
+
+(** {6 Constant names } *)
+
+(** a constant name is a kernel name couple (kn1,kn2)
where kn1 corresponds to the name used at toplevel
- (i.e. what the user see)
- and kn2 corresponds to the canonical kernel name
- i.e. in the environment we have
+ (i.e. what the user see)
+ and kn2 corresponds to the canonical kernel name
+ i.e. in the environment we have
kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t *)
type constant = kernel_name*kernel_name
-(* For the environment we distinguish constants by their
- user part*)
+let constant_of_kn kn = (kn,kn)
+let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
+let make_con mp dir l = constant_of_kn (mp,dir,l)
+let make_con_equiv mp1 mp2 dir l =
+ if mp1 == mp2 then make_con mp1 dir l
+ else ((mp1,dir,l),(mp2,dir,l))
+let canonical_con con = snd con
+let user_con con = fst con
+let repr_con con = fst con
+
+let eq_constant (_,kn1) (_,kn2) = kn1=kn2
+
+let con_label con = label (fst con)
+let con_modpath con = modpath (fst con)
+
+let string_of_con con = string_of_kn (fst con)
+let pr_con con = str (string_of_con con)
+let debug_string_of_con con =
+ "(" ^ string_of_kn (fst con) ^ "," ^ string_of_kn (snd con) ^ ")"
+let debug_pr_con con = str (debug_string_of_con con)
+
+let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
+ if lbl = l1 && lbl = l2 then con
+ else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+
+(** For the environment we distinguish constants by their user part*)
module User_ord = struct
type t = kernel_name*kernel_name
let compare x y= kn_ord (fst x) (fst y)
end
-(* For other uses (ex: non-logical things) it is enough
- to deal with the canonical part *)
+(** For other uses (ex: non-logical things) it is enough
+ to deal with the canonical part *)
module Canonical_ord = struct
type t = kernel_name*kernel_name
let compare x y= kn_ord (snd x) (snd y)
end
-
-module KNord = struct
- type t = kernel_name
- let compare =kn_ord
-end
-
-module KNmap = Map.Make(KNord)
-module KNpred = Predicate.Make(KNord)
-module KNset = Set.Make(KNord)
-
module Cmap = Map.Make(Canonical_ord)
module Cmap_env = Map.Make(User_ord)
module Cpred = Predicate.Make(Canonical_ord)
module Cset = Set.Make(Canonical_ord)
module Cset_env = Set.Make(User_ord)
-module Mindmap = Map.Make(Canonical_ord)
-module Mindset = Set.Make(Canonical_ord)
-module Mindmap_env = Map.Make(User_ord)
-
-let default_module_name = "If you see this, it's a bug"
-let initial_dir = make_dirpath [default_module_name]
-let initial_path = MPfile initial_dir
+(** {6 Names of mutual inductive types } *)
-type variable = identifier
+(** The same thing is done for mutual inductive names
+ it replaces also the old mind_equiv field of mutual
+ inductive types *)
+(** Beware: first inductive has index 0 *)
+(** Beware: first constructor has index 1 *)
-(* The same thing is done for mutual inductive names
- it replaces also the old mind_equiv field of mutual
- inductive types*)
type mutual_inductive = kernel_name*kernel_name
type inductive = mutual_inductive * int
type constructor = inductive * int
-let constant_of_kn kn = (kn,kn)
-let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = constant_of_kn (mp,dir,l)
-let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
-let canonical_con con = snd con
-let user_con con = fst con
-let repr_con con = fst con
-let string_of_con con = string_of_kn (fst con)
-let con_label con = label (fst con)
-let pr_con con = pr_kn (fst con)
-let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ str ")"
-let eq_constant (_,kn1) (_,kn2) = kn1=kn2
-let debug_string_of_con con = string_of_kn (fst con)^"'"^string_of_kn (snd con)
-
-let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
- if lbl = l1 && lbl = l2 then con
- else ((mp1,dp1,lbl),(mp2,dp2,lbl))
-
-let con_modpath con = modpath (fst con)
-
let mind_modpath mind = modpath (fst mind)
let ind_modpath ind = mind_modpath (fst ind)
let constr_modpath c = ind_modpath (fst c)
-
let mind_of_kn kn = (kn,kn)
let mind_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_mind mp dir l = ((mp,dir,l),(mp,dir,l))
-let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
+let make_mind mp dir l = mind_of_kn (mp,dir,l)
+let make_mind_equiv mp1 mp2 dir l =
+ if mp1 == mp2 then make_mind mp1 dir l
+ else ((mp1,dir,l),(mp2,dir,l))
let canonical_mind mind = snd mind
let user_mind mind = fst mind
let repr_mind mind = fst mind
-let string_of_mind mind = string_of_kn (fst mind)
let mind_label mind= label (fst mind)
-let pr_mind mind = pr_kn (fst mind)
-let debug_pr_mind mind = str "("++ pr_kn (fst mind) ++ str ","++ pr_kn (snd mind)++ str ")"
+
let eq_mind (_,kn1) (_,kn2) = kn1=kn2
-let debug_string_of_mind mind = string_of_kn (fst mind)^"'"^string_of_kn (snd mind)
+
+let string_of_mind mind = string_of_kn (fst mind)
+let pr_mind mind = str (string_of_mind mind)
+let debug_string_of_mind mind =
+ "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")"
+let debug_pr_mind con = str (debug_string_of_mind con)
let ith_mutual_inductive (kn,_) i = (kn,i)
let ith_constructor_of_inductive ind i = (ind,i)
@@ -267,6 +289,10 @@ let index_of_constructor (ind,i) = i
let eq_ind (kn1,i1) (kn2,i2) = i1=i2&&eq_mind kn1 kn2
let eq_constructor (kn1,i1) (kn2,i2) = i1=i2&&eq_ind kn1 kn2
+module Mindmap = Map.Make(Canonical_ord)
+module Mindset = Set.Make(Canonical_ord)
+module Mindmap_env = Map.Make(User_ord)
+
module InductiveOrdered = struct
type t = inductive
let compare (spx,ix) (spy,iy) =
@@ -306,7 +332,8 @@ let eq_egr e1 e2 = match e1,e2 with
EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
| _,_ -> e1 = e2
-(* Hash-consing of name objects *)
+(** {6 Hash-consing of name objects } *)
+
module Hname = Hashcons.Make(
struct
type t = name
@@ -326,7 +353,7 @@ module Hdir = Hashcons.Make(
struct
type t = dir_path
type u = identifier -> identifier
- let hash_sub hident d = List.map hident d
+ let hash_sub hident d = list_smartmap hident d
let rec equal d1 d2 = match (d1,d2) with
| [],[] -> true
| id1::d1,id2::d2 -> id1 == id2 & equal d1 d2
@@ -337,9 +364,9 @@ module Hdir = Hashcons.Make(
module Huniqid = Hashcons.Make(
struct
type t = uniq_ident
- type u = (string -> string) * (dir_path -> dir_path)
- let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir)
- let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 & s1 = s2 & dir1 == dir2
+ type u = (identifier -> identifier) * (dir_path -> dir_path)
+ let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
+ let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 && s1 == s2 && dir1 == dir2
let hash = Hashtbl.hash
end)
@@ -355,34 +382,66 @@ module Hmod = Hashcons.Make(
let rec equal d1 d2 = match (d1,d2) with
| MPfile dir1, MPfile dir2 -> dir1 == dir2
| MPbound m1, MPbound m2 -> m1 == m2
- | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2
+ | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2
| _ -> false
let hash = Hashtbl.hash
end)
-
-module Hcn = Hashcons.Make(
- struct
- type t = kernel_name*kernel_name
+module Hkn = Hashcons.Make(
+ struct
+ type t = kernel_name
type u = (module_path -> module_path)
* (dir_path -> dir_path) * (string -> string)
- let hash_sub (hmod,hdir,hstr) ((md,dir,l),(mde,dire,le)) =
- ((hmod md, hdir dir, hstr l),(hmod mde, hdir dire, hstr le))
- let equal ((mod1,dir1,l1),_) ((mod2,dir2,l2),_) =
+ let hash_sub (hmod,hdir,hstr) (md,dir,l) =
+ (hmod md, hdir dir, hstr l)
+ let equal (mod1,dir1,l1) (mod2,dir2,l2) =
mod1 == mod2 && dir1 == dir2 && l1 == l2
let hash = Hashtbl.hash
end)
-let hcons_names () =
- let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
- let hident = Hashcons.simple_hcons Hident.f hstring in
- let hname = Hashcons.simple_hcons Hname.f hident in
- let hdir = Hashcons.simple_hcons Hdir.f hident in
- let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
- let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
- let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
- let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
- (hcn,hmind,hdir,hname,hident,hstring)
+(** For [constant] and [mutual_inductive], we discriminate only on
+ the user part : having the same user part implies having the
+ same canonical part (invariant of the system). *)
+
+module Hcn = Hashcons.Make(
+ struct
+ type t = kernel_name*kernel_name
+ type u = kernel_name -> kernel_name
+ let hash_sub hkn (user,can) = (hkn user, hkn can)
+ let equal (user1,_) (user2,_) = user1 == user2
+ let hash (user,_) = Hashtbl.hash user
+ end)
+
+module Hind = Hashcons.Make(
+ struct
+ type t = inductive
+ type u = mutual_inductive -> mutual_inductive
+ let hash_sub hmind (mind, i) = (hmind mind, i)
+ let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2
+ let hash = Hashtbl.hash
+ end)
+
+module Hconstruct = Hashcons.Make(
+ struct
+ type t = constructor
+ type u = inductive -> inductive
+ let hash_sub hind (ind, j) = (hind ind, j)
+ let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
+ let hash = Hashtbl.hash
+ end)
+
+let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.f ()
+let hcons_ident = hcons_string
+let hcons_name = Hashcons.simple_hcons Hname.f hcons_ident
+let hcons_dirpath = Hashcons.simple_hcons Hdir.f hcons_ident
+let hcons_uid = Hashcons.simple_hcons Huniqid.f (hcons_ident,hcons_dirpath)
+let hcons_mp =
+ Hashcons.simple_hcons Hmod.f (hcons_dirpath,hcons_uid,hcons_string)
+let hcons_kn = Hashcons.simple_hcons Hkn.f (hcons_mp,hcons_dirpath,hcons_string)
+let hcons_con = Hashcons.simple_hcons Hcn.f hcons_kn
+let hcons_mind = Hashcons.simple_hcons Hcn.f hcons_kn
+let hcons_ind = Hashcons.simple_hcons Hind.f hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.f hcons_ind
(*******)