aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml31
-rw-r--r--kernel/cooking.mli4
-rw-r--r--kernel/environ.ml18
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/names.ml253
-rw-r--r--kernel/names.mli45
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/univ.ml18
8 files changed, 157 insertions, 216 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7a06a78968..482be2fb99 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -25,7 +25,7 @@ type modification_action = ABSTRACT | ERASE
type 'a modification =
| NOT_OCCUR
| DO_ABSTRACT of 'a * modification_action list
- | DO_REPLACE
+ | DO_REPLACE of constant_body
type work_list =
(section_path * section_path modification) list
@@ -33,7 +33,7 @@ type work_list =
* (constructor_path * constructor_path modification) list
type recipe = {
- d_from : section_path;
+ d_from : constant_body;
d_abstract : identifier list;
d_modlist : work_list }
@@ -83,7 +83,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun mkMutInd (oper',modif) cl'
- | DO_REPLACE -> assert false)
+ | DO_REPLACE _ -> assert false)
with
| Not_found -> mkMutInd (spi,cl'))
@@ -94,7 +94,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun mkMutConstruct (oper',modif) cl'
- | DO_REPLACE -> assert false)
+ | DO_REPLACE _ -> assert false)
with
| Not_found -> mkMutConstruct (spi,cl'))
@@ -105,7 +105,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
| DO_ABSTRACT (oper',modif) ->
assert (List.length modif <= Array.length cl);
interp_modif absfun mkConst (oper',modif) cl'
- | DO_REPLACE -> substrec (replfun (sp,cl')))
+ | DO_REPLACE cb -> substrec (replfun sp cb cl'))
with
| Not_found -> mkConst (sp,cl'))
@@ -117,17 +117,18 @@ let expmod_constr oldenv modlist c =
let sigma = Evd.empty in
let simpfun =
if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
- let expfun cst =
- try
- constant_value oldenv cst
- with NotEvaluableConst Opaque ->
- let (sp,_) = cst in
+ let expfun sp cb args =
+ if cb.const_opaque then
errorlabstrm "expmod_constr"
[< 'sTR"Cannot unfold the value of ";
- 'sTR(string_of_path sp); 'sPC;
- 'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
- 'sTR"and then require that theorems which use them"; 'sPC;
- 'sTR"be transparent" >];
+ 'sTR(string_of_path sp); 'sPC;
+ 'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
+ 'sTR"and then require that theorems which use them"; 'sPC;
+ 'sTR"be transparent" >];
+ match cb.const_body with
+ | Some body ->
+ instantiate_constr cb.const_hyps body (Array.to_list args)
+ | None -> assert false
in
let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
match kind_of_term c' with
@@ -155,7 +156,7 @@ let abstract_constant ids_to_abs hyps (body,typ) =
(body',typ')
let cook_constant env r =
- let cb = lookup_constant r.d_from env in
+ let cb = r.d_from in
let typ = expmod_type env r.d_modlist cb.const_type in
let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index f295031768..d9b564835b 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -20,7 +20,7 @@ type modification_action = ABSTRACT | ERASE
type 'a modification =
| NOT_OCCUR
| DO_ABSTRACT of 'a * modification_action list
- | DO_REPLACE
+ | DO_REPLACE of constant_body
type work_list =
(section_path * section_path modification) list
@@ -28,7 +28,7 @@ type work_list =
* (constructor_path * constructor_path modification) list
type recipe = {
- d_from : section_path;
+ d_from : constant_body;
d_abstract : identifier list;
d_modlist : work_list }
diff --git a/kernel/environ.ml b/kernel/environ.ml
index db187880ff..77b96d30c9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -20,7 +20,7 @@ open Declarations
type checksum = int
-type import = string * checksum
+type compilation_unit_name = dir_path * checksum
type global = Constant | Inductive
@@ -28,7 +28,7 @@ type globals = {
env_constants : constant_body Spmap.t;
env_inductives : mutual_inductive_body Spmap.t;
env_locals : (global * section_path) list;
- env_imports : import list }
+ env_imports : compilation_unit_name list }
type context = {
env_named_context : named_context;
@@ -366,9 +366,8 @@ let set_transparent env sp =
(*s Modules (i.e. compiled environments). *)
type compiled_env = {
- cenv_id : string;
- cenv_stamp : checksum;
- cenv_needed : import list;
+ cenv_stamped_id : compilation_unit_name;
+ cenv_needed : compilation_unit_name list;
cenv_constants : (section_path * constant_body) list;
cenv_inductives : (section_path * mutual_inductive_body) list }
@@ -382,8 +381,7 @@ let exported_objects env =
let export env id =
let (cst,ind) = exported_objects env in
- { cenv_id = id;
- cenv_stamp = 0;
+ { cenv_stamped_id = (id,0);
cenv_needed = env.env_globals.env_imports;
cenv_constants = cst;
cenv_inductives = ind }
@@ -394,9 +392,9 @@ let check_imports env needed =
try
let actual_stamp = List.assoc id imports in
if stamp <> actual_stamp then
- error ("Inconsistent assumptions over module " ^ id)
+ error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
with Not_found ->
- error ("Reference to unknown module " ^ id)
+ error ("Reference to unknown module " ^ (string_of_dirpath id))
in
List.iter check needed
@@ -415,7 +413,7 @@ let import cenv env =
{ env_constants = add_list gl.env_constants cenv.cenv_constants;
env_inductives = add_list gl.env_inductives cenv.cenv_inductives;
env_locals = gl.env_locals;
- env_imports = (cenv.cenv_id,cenv.cenv_stamp) :: gl.env_imports }
+ env_imports = cenv.cenv_stamped_id :: gl.env_imports }
in
let g = universes env in
let g = List.fold_left
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ca93b84e78..45c2d1130b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -173,7 +173,7 @@ val set_transparent : env -> constant_path -> unit
type compiled_env
-val export : env -> string -> compiled_env
+val export : env -> dir_path -> compiled_env
val import : compiled_env -> env -> env
(*s Unsafe judgments. We introduce here the pre-type of judgments, which is
diff --git a/kernel/names.ml b/kernel/names.ml
index 4965a733c9..c4ced8e999 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -11,101 +11,16 @@
open Pp
open Util
+(*s Identifiers *)
+
(* Utilities *)
let code_of_0 = Char.code '0'
let code_of_9 = Char.code '9'
-(* This checks that a string is acceptable as an ident, i.e. starts
- with a letter and contains only letters, digits or "'" *)
-
-let check_ident_suffix i l s =
- for i=1 to l-1 do
- let c = String.get s i in
- if not (is_letter c or is_digit c or c = '\'') then
- error
- ("Character "^(String.sub s i 1)^" is not allowed in an identifier")
- done
-
-let check_ident s =
- let l = String.length s in
- if l = 0 then error "The empty string is not an identifier";
- let c = String.get s 0 in
- if not (is_letter c) then error "An identifier starts with a letter";
- check_ident_suffix 1 l s
-
-let check_suffix s = check_ident_suffix 0 (String.length s) s
-
-let is_ident s = try check_ident s; true with _ -> false
-
(* Identifiers *)
-(*
-module Ident = struct
-
-type t = {
- atom : string ;
- index : int }
-
-let repr_ident { atom = sa; index = n } =
- if n = -1 then (sa,None) else (sa,Some n)
-
-let make_ident sa = function
- | Some n ->
- let c = Char.code (String.get sa (String.length sa -1)) in
- if c < code_of_0 or c > code_of_9 then { atom = sa; index = n }
- else { atom = sa^"_"; index = n }
- | None -> { atom = sa; index = -1 }
-
-let string_of_id id = match repr_ident id with
- | (s,None) -> s
- | (s,Some n) -> s ^ (string_of_int n)
-
-let id_of_string s =
- let slen = String.length s in
- (* [n'] is the position of the first non nullary digit *)
- let rec numpart n n' =
- if n = 0 then
- failwith
- ("The string " ^ s ^ " is not an identifier: it contains only digits")
- else
- let c = Char.code (String.get s (n-1)) in
- if c = code_of_0 && n <> slen then
- numpart (n-1) n'
- else if code_of_0 <= c && c <= code_of_9 then
- numpart (n-1) (n-1)
- else
- n'
- in
- let numstart = numpart slen slen in
- if numstart = slen then
- { atom = s; index = -1 }
- else
- { atom = String.sub s 0 numstart;
- index = int_of_string (String.sub s numstart (slen - numstart)) }
-
-let first_char id =
- assert (id.atom <> "");
- String.make 1 id.atom.[0]
-
-let id_ord { atom = s1; index = n1 } { atom = s2; index = n2 } =
- let s_bit = Pervasives.compare s1 s2 in
- if s_bit = 0 then n1 - n2 else s_bit
-(* Rem : if an ident starts with toto00 then after successive
- renamings it comes to toto09, then it goes on with toto010 *)
-let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
-let restart_ident id = { id with index = 0 }
-let has_index id = (id.index <> -1)
-
-let hash_sub hstr id = { atom = hstr id.atom; index = id.index }
-let equal id1 id2 = id1.atom == id2.atom && id1.index = id2.index
-
-end (* End of module Ident *)
-*)
-(* Second implementation *)
-module Ident = struct
-
-type t = string
+type identifier = string
let cut_ident s =
let slen = String.length s in
@@ -139,13 +54,7 @@ let make_ident sa = function
let c = Char.code (String.get sa (String.length sa -1)) in
if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
else sa ^ "_" ^ (string_of_int n)
- | None -> sa
-
-let add_suffix id s = check_suffix s; id^s
-let add_prefix s id = check_ident s; s^id
-
-let string_of_id id = id
-let id_of_string s = s
+ | None -> String.copy sa
let first_char id =
assert (id <> "");
@@ -155,7 +64,7 @@ let id_ord = Pervasives.compare
(* Rem: semantics is a bit different, if an ident starts with toto00 then
after successive renamings it comes to toto09, then it goes on with toto10 *)
-let lift_ident id =
+let lift_subscript id =
let len = String.length id in
let rec add carrypos =
let c = id.[carrypos] in
@@ -180,28 +89,52 @@ let lift_ident id =
end
in add (len-1)
-let has_index id = is_digit (id.[String.length id - 1])
+let has_subscript id = is_digit (id.[String.length id - 1])
-let restart_ident id =
+let forget_subscript id =
let len = String.length id in
let numstart = cut_ident id in
let newid = String.make (numstart+1) '0' in
String.blit id 0 newid 0 numstart;
newid
-let hash_sub hstr id = hstr id
-let equal id1 id2 = id1 == id2
+(* This checks that a string is acceptable as an ident, i.e. starts
+ with a letter and contains only letters, digits or "'" *)
+
+let check_ident_suffix i l s =
+ for i=1 to l-1 do
+ let c = String.get s i in
+ if not (is_letter c or is_digit c or c = '\'' or c = '_' or c = '@') then
+ error
+ ("Character "^(String.sub s i 1)^" is not allowed in an identifier")
+ done
+
+let check_ident s =
+ let l = String.length s in
+ if l = 0 then error "The empty string is not an identifier";
+ let c = String.get s 0 in
+ if (is_letter c) or c = '_' or c = '$' then check_ident_suffix 1 l s
+ else error (s^": an identifier starts with a letter")
+
+let is_ident s = try check_ident s; true with _ -> false
-end (* End of module Ident *)
+let check_suffix s = check_ident_suffix 0 (String.length s) s
-type identifier = Ident.t
-let repr_ident = Ident.repr_ident
-let make_ident = Ident.make_ident
let add_suffix id s = check_suffix s; id^s
let add_prefix s id = check_ident s; s^id
-let string_of_id = Ident.string_of_id
-let id_of_string = Ident.id_of_string
-let id_ord = Ident.id_ord
+
+let string_of_id id = String.copy id
+let id_of_string s = check_ident s; String.copy s
+
+(* 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)
module IdOrdered =
struct
@@ -216,18 +149,18 @@ let atompart_of_id id = fst (repr_ident id)
let index_of_id id = snd (repr_ident id)
let pr_id id = [< 'sTR (string_of_id id) >]
-let first_char = Ident.first_char
+let wildcard = id_of_string "_"
(* Fresh names *)
-let lift_ident = Ident.lift_ident
+let lift_ident = lift_subscript
let next_ident_away id avoid =
if List.mem id avoid then
- let id0 = if not (Ident.has_index id) then id else
+ let id0 = if not (has_subscript id) then id else
(* Ce serait sans doute mieux avec quelque chose inspiré de
*** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
- Ident.restart_ident id in
+ forget_subscript id in
let rec name_rec id =
if List.mem id avoid then name_rec (lift_ident id) else id in
name_rec id0
@@ -272,30 +205,25 @@ let kind_of_string = function
| _ -> invalid_arg "kind_of_string"
(*s Directory paths = section names paths *)
-type dir_path = string list
-
-(*s Section paths are absolute names *)
+type module_ident = identifier
+type dir_path = module_ident list
-type section_path = {
- dirpath : dir_path ;
- basename : identifier ;
- kind : path_kind }
+module ModIdOrdered =
+ struct
+ type t = identifier
+ let compare = Pervasives.compare
+ end
-let make_path pa id k = { dirpath = pa; basename = id; kind = k }
-let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+module ModIdmap = Map.Make(ModIdOrdered)
-let kind_of_path sp = sp.kind
-let basename sp = sp.basename
-let dirpath sp = sp.dirpath
+let make_dirpath x = x
+let repr_dirpath x = x
-(* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "." sl
+let dirpath_prefix = function
+ | [] -> anomaly "dirpath_prefix: empty dirpath"
+ | l -> snd (list_sep_last l)
-let string_of_path sp =
- let (sl,id,k) = repr_path sp in
- String.concat ""
- (List.flatten (List.map (fun s -> [s;"."]) sl)
- @ [ string_of_id id ])
+let split_dirpath d = let (b,d) = list_sep_last d in (d,b)
let parse_sp s =
let len = String.length s in
@@ -304,37 +232,60 @@ let parse_sp s =
let pos = String.index_from s n '.' in
let dir = String.sub s n (pos-n) in
let dirs,n' = decoupe_dirs (succ pos) in
- dir::dirs,n'
+ (id_of_string dir)::dirs,n'
with
| Not_found -> [],n
in
if len = 0 then invalid_arg "parse_section_path";
let dirs,n = decoupe_dirs 0 in
let id = String.sub s n (len-n) in
- dirs,id
+ dirs, (id_of_string id)
-let path_of_string s =
+let dirpath_of_string s =
try
let sl,s = parse_sp s in
- make_path sl (id_of_string s) CCI
+ sl @ [s]
with
- | Invalid_argument _ -> invalid_arg "path_of_string"
+ | Invalid_argument _ -> invalid_arg "dirpath_of_string"
-let dirpath_of_string s =
+let string_of_dirpath sl = String.concat "." (List.map string_of_id sl)
+
+let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
+
+(*s Section paths are absolute names *)
+
+type section_path = {
+ dirpath : dir_path ;
+ basename : identifier ;
+ kind : path_kind }
+
+let make_path pa id k = { dirpath = pa; basename = id; kind = k }
+let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+
+let kind_of_path sp = sp.kind
+let basename sp = sp.basename
+let dirpath sp = sp.dirpath
+
+(* parsing and printing of section paths *)
+let string_of_path sp =
+ let (sl,id,k) = repr_path sp in
+ (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+
+let path_of_string s =
try
let sl,s = parse_sp s in
- sl @ [s]
+ make_path sl s CCI
with
- | Invalid_argument _ -> invalid_arg "dirpath_of_string"
+ | Invalid_argument _ -> invalid_arg "path_of_string"
let pr_sp sp = [< 'sTR (string_of_path sp) >]
let sp_of_wd = function
| [] -> invalid_arg "Names.sp_of_wd"
- | l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
+ | l -> let (bn,dp) = list_sep_last l in make_path dp bn OBJ
let wd_of_sp sp =
- let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
+ let (sp,id,_) = repr_path sp in sp @ [id]
let sp_ord sp1 sp2 =
let (p1,id1,k) = repr_path sp1
@@ -346,7 +297,7 @@ let sp_ord sp1 sp2 =
else
ck
-let dirpath_prefix_of = list_prefix_of
+let is_dirpath_prefix_of = list_prefix_of
module SpOrdered =
struct
@@ -366,16 +317,6 @@ type inductive_path = section_path * int
type constructor_path = inductive_path * int
type mutual_inductive_path = section_path
-(* Hash-consing of identifier *)
-module Hident = Hashcons.Make(
- struct
- type t = Ident.t
- type u = string -> string
- let hash_sub = Ident.hash_sub
- let equal = Ident.equal
- let hash = Hashtbl.hash
- end)
-
(* Hash-consing of name objects *)
module Hname = Hashcons.Make(
struct
@@ -395,9 +336,9 @@ module Hname = Hashcons.Make(
module Hsp = Hashcons.Make(
struct
type t = section_path
- type u = (identifier -> identifier) * (string -> string)
- let hash_sub (hident,hstr) sp =
- { dirpath = List.map hstr sp.dirpath;
+ type u = identifier -> identifier
+ let hash_sub hident sp =
+ { dirpath = List.map hident sp.dirpath;
basename = hident sp.basename;
kind = sp.kind }
let equal sp1 sp2 =
@@ -411,6 +352,6 @@ 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 hspcci = Hashcons.simple_hcons Hsp.f (hident,hstring) in
- let hspfw = Hashcons.simple_hcons Hsp.f (hident,hstring) in
+ let hspcci = Hashcons.simple_hcons Hsp.f hident in
+ let hspfw = Hashcons.simple_hcons Hsp.f hident in
(hspcci,hspfw,hname,hident,hstring)
diff --git a/kernel/names.mli b/kernel/names.mli
index 7eb39ff673..58aae5a657 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -32,10 +32,8 @@ val string_of_id : identifier -> string
val id_of_string : string -> identifier
val pr_id : identifier -> std_ppcmds
-(* These checks the validity of an identifier; [check_ident] fails
- with error if invalid *)
-val check_ident : string -> unit
-val is_ident : string -> bool
+(* This is the identifier ["_"] *)
+val wildcard : identifier
(* Deriving ident from other idents *)
val add_suffix : identifier -> string -> identifier
@@ -63,10 +61,24 @@ val string_of_kind : path_kind -> string
val kind_of_string : string -> path_kind
(*s Directory paths = section names paths *)
-type dir_path = string list
+type module_ident = identifier
+type dir_path = module_ident list
+
+module ModIdmap : Map.S with type key = module_ident
+
+val make_dirpath : module_ident list -> dir_path
+val repr_dirpath : dir_path -> module_ident list
+
+(* Give the immediate prefix of a dir_path *)
+val dirpath_prefix : dir_path -> dir_path
+
+(* Give the immediate prefix and basename of a dir_path *)
+val split_dirpath : dir_path -> dir_path * identifier
(* Printing of directory paths as ["coq_root.module.submodule"] *)
val string_of_dirpath : dir_path -> string
+val pr_dirpath : dir_path -> std_ppcmds
+
(*s Section paths are {\em absolute} names *)
type section_path
@@ -80,8 +92,8 @@ val dirpath : section_path -> dir_path
val basename : section_path -> identifier
val kind_of_path : section_path -> path_kind
-val sp_of_wd : string list -> section_path
-val wd_of_sp : section_path -> string list
+val sp_of_wd : module_ident list -> section_path
+val wd_of_sp : section_path -> module_ident list
(* Parsing and printing of section path as ["coq_root.module.id"] *)
val path_of_string : string -> section_path
@@ -89,25 +101,11 @@ val string_of_path : section_path -> string
val pr_sp : section_path -> std_ppcmds
val dirpath_of_string : string -> dir_path
-(*i
-val string_of_path_mind : section_path -> identifier -> string
-val coerce_path : path_kind -> section_path -> section_path
-val fwsp_of : section_path -> section_path
-val ccisp_of : section_path -> section_path
-val objsp_of : section_path -> section_path
-val fwsp_of_ccisp : section_path -> section_path
-val ccisp_of_fwsp : section_path -> section_path
-val append_to_path : section_path -> string -> section_path
-
-val sp_gt : section_path * section_path -> bool
-i*)
val sp_ord : section_path -> section_path -> int
(* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *)
-val dirpath_prefix_of : dir_path -> dir_path -> bool
-(*i
-module Spset : Set.S with type elt = section_path
-i*)
+val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+
module Spmap : Map.S with type key = section_path
(*s Specific paths for declarations *)
@@ -121,4 +119,3 @@ type mutual_inductive_path = section_path
val hcons_names : unit ->
(section_path -> section_path) * (section_path -> section_path) *
(name -> name) * (identifier -> identifier) * (string -> string)
-
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 04fbe21bb1..102fbb228e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -63,7 +63,7 @@ val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
val set_opaque : safe_environment -> section_path -> unit
val set_transparent : safe_environment -> section_path -> unit
-val export : safe_environment -> string -> compiled_env
+val export : safe_environment -> dir_path -> compiled_env
val import : compiled_env -> safe_environment -> safe_environment
val env_of_safe_env : safe_environment -> env
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7c3060820a..5f03e6a36e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -40,9 +40,12 @@ let string_of_univ u =
let pr_uni u =
[< 'sTR (Names.string_of_dirpath u.u_mod) ; 'sTR"." ; 'iNT u.u_num >]
-
-let dummy_univ = { u_mod = ["dummy univ"]; u_num = 0 } (* for prover terms *)
-let implicit_univ = { u_mod = ["implicit univ"]; u_num = 0 }
+let dummy_univ = (* for prover terms *)
+ { u_mod = Names.make_dirpath [Names.id_of_string "dummy_univ"];
+ u_num = 0 }
+let implicit_univ =
+ { u_mod = Names.make_dirpath [Names.id_of_string "implicit_univ"];
+ u_num = 0 }
let current_module = ref []
@@ -83,7 +86,7 @@ let declare_univ u g =
(* The universes of Prop and Set: Type_0, Type_1 and the
resulting graph. *)
let (initial_universes,prop_univ,prop_univ_univ) =
- let prop_sp = ["prop_univ"] in
+ let prop_sp = Names.make_dirpath [Names.id_of_string "prop_univ"] in
let u = { u_mod = prop_sp; u_num = 0 } in
let su = { u_mod = prop_sp; u_num = 1 } in
let g = enter_arc (terminal u) UniverseMap.empty in
@@ -430,7 +433,7 @@ module Huniv =
Hashcons.Make(
struct
type t = universe
- type u = string -> string
+ type u = Names.identifier -> Names.identifier
let hash_sub hstr {u_mod=sp; u_num=n} =
{u_mod=List.map hstr sp; u_num=n}
let equal {u_mod=sp1; u_num=n1} {u_mod=sp2; u_num=n2} =
@@ -441,5 +444,6 @@ module Huniv =
let hcons1_univ u =
- let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
- Hashcons.simple_hcons Huniv.f hstring u
+ let _,_,_,hid,_ = Names.hcons_names () in
+ Hashcons.simple_hcons Huniv.f hid u
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:01:04 +0000