aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml2
-rw-r--r--kernel/cemitcodes.ml4
-rw-r--r--kernel/closure.ml12
-rw-r--r--kernel/conv_oracle.ml12
-rw-r--r--kernel/conv_oracle.mli4
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/csymtable.ml8
-rw-r--r--kernel/csymtable.mli4
-rw-r--r--kernel/environ.ml8
-rw-r--r--kernel/mod_typing.ml5
-rw-r--r--kernel/modops.ml5
-rw-r--r--kernel/names.ml16
-rw-r--r--kernel/names.mli18
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/term.ml25
-rw-r--r--kernel/term.mli1
-rw-r--r--kernel/univ.ml2
19 files changed, 82 insertions, 52 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 0d4a246a09..4995547462 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -90,7 +90,7 @@ let rec instruction ppf = function
print_string " bodies = ";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
(* nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_kn id)
+ | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
| Kconst cst ->
fprintf ppf "\tconst"
| Kmakeblock(n, m) ->
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 4219491631..1b93dc4b6a 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -254,7 +254,7 @@ let subst_patch s (ri,pos) =
let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in
(Reloc_annot {a with ci = ci},pos)
| Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (subst_kn s kn), pos)
+ | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos)
let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv
@@ -265,7 +265,7 @@ type body_code =
let subst_body_code s = function
| BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
- | BCallias kn -> BCallias (subst_kn s kn)
+ | BCallias kn -> BCallias (subst_con s kn)
| BCconstant -> BCconstant
type to_patch_substituted = body_code substituted
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 51c355c9a1..2f83657d06 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -51,8 +51,8 @@ let with_stats c =
end else
Lazy.force c
-let all_opaque = (Idpred.empty, KNpred.empty)
-let all_transparent = (Idpred.full, KNpred.full)
+let all_opaque = (Idpred.empty, Cpred.empty)
+let all_transparent = (Idpred.full, Cpred.full)
module type RedFlagsSig = sig
type reds
@@ -107,7 +107,7 @@ module RedFlags = (struct
| DELTA -> { red with r_delta = true; r_const = all_transparent }
| CONST kn ->
let (l1,l2) = red.r_const in
- { red with r_const = l1, KNpred.add kn l2 }
+ { red with r_const = l1, Cpred.add kn l2 }
| IOTA -> { red with r_iota = true }
| ZETA -> { red with r_zeta = true }
| VAR id ->
@@ -119,7 +119,7 @@ module RedFlags = (struct
| DELTA -> { red with r_delta = false }
| CONST kn ->
let (l1,l2) = red.r_const in
- { red with r_const = l1, KNpred.remove kn l2 }
+ { red with r_const = l1, Cpred.remove kn l2 }
| IOTA -> { red with r_iota = false }
| ZETA -> { red with r_zeta = false }
| VAR id ->
@@ -135,7 +135,7 @@ module RedFlags = (struct
| BETA -> incr_cnt red.r_beta beta
| CONST kn ->
let (_,l) = red.r_const in
- let c = KNpred.mem kn l in
+ let c = Cpred.mem kn l in
incr_cnt c delta
| VAR id -> (* En attendant d'avoir des kn pour les Var *)
let (l,_) = red.r_const in
@@ -149,7 +149,7 @@ module RedFlags = (struct
let red_get_const red =
let p1,p2 = red.r_const in
let (b1,l1) = Idpred.elements p1 in
- let (b2,l2) = KNpred.elements p2 in
+ let (b2,l2) = Cpred.elements p2 in
if b1=b2 then
let l1' = List.map (fun x -> EvalVarRef x) l1 in
let l2' = List.map (fun x -> EvalConstRef x) l2 in
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 1504220ac4..d0f5cf63e0 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -11,12 +11,12 @@
open Names
(* Opaque constants *)
-let cst_transp = ref KNpred.full
+let cst_transp = ref Cpred.full
-let set_opaque_const kn = cst_transp := KNpred.remove kn !cst_transp
-let set_transparent_const kn = cst_transp := KNpred.add kn !cst_transp
+let set_opaque_const kn = cst_transp := Cpred.remove kn !cst_transp
+let set_transparent_const kn = cst_transp := Cpred.add kn !cst_transp
-let is_opaque_cst kn = not (KNpred.mem kn !cst_transp)
+let is_opaque_cst kn = not (Cpred.mem kn !cst_transp)
(* Opaque variables *)
let var_transp = ref Idpred.full
@@ -36,7 +36,7 @@ let is_opaque = function
let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1)
(* summary operations *)
-type transparent_state = Idpred.t * KNpred.t
-let init() = (cst_transp := KNpred.full; var_transp := Idpred.full)
+type transparent_state = Idpred.t * Cpred.t
+let init() = (cst_transp := Cpred.full; var_transp := Idpred.full)
let freeze () = (!var_transp, !cst_transp)
let unfreeze (vo,co) = (cst_transp := co; var_transp := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 351df9d86a..7fc3dabcda 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -18,8 +18,8 @@ open Names
val oracle_order : 'a tableKey -> 'a tableKey -> bool
(* Changing the oracle *)
-val set_opaque_const : kernel_name -> unit
-val set_transparent_const : kernel_name -> unit
+val set_opaque_const : constant -> unit
+val set_transparent_const : constant -> unit
val set_opaque_var : identifier -> unit
val set_transparent_var : identifier -> unit
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5c058b4661..9869afcf50 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -102,7 +102,7 @@ let expmod_constr modlist c =
if cb.const_opaque then
errorlabstrm "expmod_constr"
(str"Cannot unfold the value of " ++
- str(string_of_kn kn) ++ spc () ++
+ str(string_of_con kn) ++ spc () ++
str"You cannot declare local lemmas as being opaque" ++ spc () ++
str"and then require that theorems which use them" ++ spc () ++
str"be transparent");
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 402a0fb97b..f9f03e3486 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -55,9 +55,9 @@ let num_boxed = ref 0
let boxed_tbl = Hashtbl.create 53
-let cst_opaque = ref KNpred.full
+let cst_opaque = ref Cpred.full
-let is_opaque kn = KNpred.mem kn !cst_opaque
+let is_opaque kn = Cpred.mem kn !cst_opaque
let set_global_boxed kn v =
let n = !num_boxed in
@@ -163,12 +163,12 @@ and val_of_constr env c =
eval_to_patch env (to_memory ccfv)
let set_transparent_const kn =
- cst_opaque := KNpred.remove kn !cst_opaque;
+ cst_opaque := Cpred.remove kn !cst_opaque;
List.iter (fun n -> (global_boxed()).(n) <- false)
(Hashtbl.find_all boxed_tbl kn)
let set_opaque_const kn =
- cst_opaque := KNpred.add kn !cst_opaque;
+ cst_opaque := Cpred.add kn !cst_opaque;
List.iter (fun n -> (global_boxed()).(n) <- true)
(Hashtbl.find_all boxed_tbl kn)
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 5fafbac49e..4c56fc9478 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -4,5 +4,5 @@ open Environ
val val_of_constr : env -> constr -> values
-val set_opaque_const : kernel_name -> unit
-val set_transparent_const : kernel_name -> unit
+val set_opaque_const : constant -> unit
+val set_transparent_const : constant -> unit
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d9569bca64..a6d7ff65b9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -29,7 +29,7 @@ type constant_key = constant_body * key
type engagement = ImpredicativeSet
type globals = {
- env_constants : constant_key KNmap.t;
+ env_constants : constant_key Cmap.t;
env_inductives : mutual_inductive_body KNmap.t;
env_modules : module_body MPmap.t;
env_modtypes : module_type_body KNmap.t }
@@ -57,7 +57,7 @@ and env = {
let empty_env = {
env_globals = {
- env_constants = KNmap.empty;
+ env_constants = Cmap.empty;
env_inductives = KNmap.empty;
env_modules = MPmap.empty;
env_modtypes = KNmap.empty };
@@ -218,13 +218,13 @@ let set_pos_constant (cb,r) bpos =
else raise AllReadyEvaluated
let lookup_constant_key kn env =
- KNmap.find kn env.env_globals.env_constants
+ Cmap.find kn env.env_globals.env_constants
let lookup_constant kn env = constant_key_body (lookup_constant_key kn env)
let add_constant kn cs env =
let new_constants =
- KNmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in
+ Cmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in
let new_globals =
{ env.env_globals with
env_constants = new_constants } in
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index a3639ef988..9f5a5e9a85 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -143,13 +143,14 @@ and translate_entry_list env msid is_definition sig_e =
let mp = MPself msid in
let do_entry env (l,e) =
let kn = make_kn mp empty_dirpath l in
+ let con = make_con mp empty_dirpath l in
match e with
| SPEconst ce ->
- let cb = translate_constant env kn ce in
+ let cb = translate_constant env con ce in
begin match cb.const_hyps with
| (_::_) -> error_local_context (Some l)
| [] ->
- add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb)
+ add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb)
end
| SPEmind mie ->
let mib = translate_mind env mie in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5a0694cbef..aca663e7c9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -163,8 +163,9 @@ let subst_signature_msid msid mp =
let rec add_signature mp sign env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
+ let con = make_con mp empty_dirpath l in
match elem with
- | SPBconst cb -> Environ.add_constant kn cb env
+ | SPBconst cb -> Environ.add_constant con cb env
| SPBmind mib -> Environ.add_mind kn mib env
| SPBmodule mb ->
add_module (MPdot (mp,l)) (module_body_of_spec mb) env
@@ -189,7 +190,7 @@ let strengthen_const env mp l cb =
| false, Some _ -> cb
| true, Some _
| _, None ->
- let const = mkConst (make_kn mp empty_dirpath l) in
+ let const = mkConst (make_con mp empty_dirpath l) in
let const_subs = Some (Declarations.from_val const) in
{cb with
const_body = const_subs;
diff --git a/kernel/names.ml b/kernel/names.ml
index 8211cf845b..db1b1b6df8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -273,6 +273,9 @@ end
module KNmap = Map.Make(KNord)
module KNpred = Predicate.Make(KNord)
module KNset = Set.Make(KNord)
+module Cmap = KNmap
+module Cpred = KNpred
+module Cset = KNset
let default_module_name = id_of_string "If you see this, it's a bug"
@@ -288,6 +291,15 @@ type mutual_inductive = kernel_name
type inductive = mutual_inductive * int
type constructor = inductive * int
+let constant_of_kn kn = kn
+let make_con mp dir l = (mp,dir,l)
+let repr_con con = con
+let string_of_con = string_of_kn
+let con_label = label
+let pr_con = pr_kn
+let con_modpath = modpath
+let subst_con = subst_kn
+
let ith_mutual_inductive (kn,_) i = (kn,i)
let ith_constructor_of_inductive ind i = (ind,i)
let inductive_of_constructor (ind,i) = ind
@@ -373,12 +385,12 @@ let hcons_names () =
let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in
- (hkn,hdir,hname,hident,hstring)
+ (hkn,hkn,hdir,hname,hident,hstring)
(*******)
-type transparent_state = Idpred.t * KNpred.t
+type transparent_state = Idpred.t * Cpred.t
type 'a tableKey =
| ConstKey of constant
diff --git a/kernel/names.mli b/kernel/names.mli
index a08d1be238..8cda7d958d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -158,13 +158,26 @@ module KNmap : Map.S with type key = kernel_name
(*s Specific paths for declarations *)
type variable = identifier
-type constant = kernel_name
+type constant
type mutual_inductive = kernel_name
(* Beware: first inductive has index 0 *)
type inductive = mutual_inductive * int
(* Beware: first constructor has index 1 *)
type constructor = inductive * int
+module Cmap : Map.S with type key = constant
+module Cpred : Predicate.S with type elt = constant
+module Cset : Set.S with type elt = constant
+
+val constant_of_kn : kernel_name -> constant
+val make_con : module_path -> dir_path -> label -> constant
+val repr_con : constant -> module_path * dir_path * label
+val string_of_con : constant -> string
+val con_label : constant -> label
+val con_modpath : constant -> module_path
+val pr_con : constant -> Pp.std_ppcmds
+val subst_con : substitution -> constant -> constant
+
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
@@ -177,6 +190,7 @@ type evaluable_global_reference =
(* Hash-consing *)
val hcons_names : unit ->
+ (constant -> constant) *
(kernel_name -> kernel_name) * (dir_path -> dir_path) *
(name -> name) * (identifier -> identifier) * (string -> string)
@@ -188,7 +202,7 @@ type 'a tableKey =
| VarKey of identifier
| RelKey of 'a
-type transparent_state = Idpred.t * KNpred.t
+type transparent_state = Idpred.t * Cpred.t
type inv_rel_key = int (* index in the [rel_context] part of environment
starting by the end, {\em inverse}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7e5e919444..737f771841 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -132,7 +132,7 @@ let hcons_constant_body cb =
let add_constant dir l decl senv =
check_label l senv.labset;
- let kn = make_kn senv.modinfo.modpath dir l in
+ let kn = make_con senv.modinfo.modpath dir l in
let cb =
match decl with
| ConstantEntry ce -> translate_constant senv.env kn ce
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f59b5c3756..9b5d78870f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -44,7 +44,7 @@ type global_declaration =
val add_constant :
dir_path -> label -> global_declaration -> safe_environment ->
- kernel_name * safe_environment
+ constant * safe_environment
(* Adding an inductive type *)
val add_mind :
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6bd88c8cd0..2f39dc61a3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -174,7 +174,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
let c2 = Declarations.force lc2 in
let c1 = match cb1.const_body with
| Some lc1 -> Declarations.force lc1
- | None -> mkConst (make_kn (MPself msid1) empty_dirpath l)
+ | None -> mkConst (make_con (MPself msid1) empty_dirpath l)
in
check_conv cst conv env c1 c2
diff --git a/kernel/term.ml b/kernel/term.ml
index 1855858ca0..21ab2ea5d2 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -148,7 +148,7 @@ let comp_term t1 t2 =
& array_for_all2 (==) bl1 bl2
| _ -> false
-let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t =
+let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t =
match t with
| Rel _ -> t
| Meta x -> Meta x
@@ -160,7 +160,7 @@ let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t =
| LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
| App (c,l) -> App (sh_rec c, Array.map sh_rec l)
| Evar (e,l) -> Evar (e, Array.map sh_rec l)
- | Const c -> Const (sh_kn c)
+ | Const c -> Const (sh_con c)
| Ind (kn,i) -> Ind (sh_kn kn,i)
| Construct ((kn,i),j) -> Construct ((sh_kn kn,i),j)
| Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *)
@@ -179,15 +179,16 @@ module Hconstr =
struct
type t = constr
type u = (constr -> constr) *
- ((sorts -> sorts) * (kernel_name -> kernel_name)
- * (name -> name) * (identifier -> identifier))
+ ((sorts -> sorts) * (constant -> constant) *
+ (kernel_name -> kernel_name) * (name -> name) *
+ (identifier -> identifier))
let hash_sub = hash_term
let equal = comp_term
let hash = Hashtbl.hash
end)
-let hcons_term (hsorts,hkn,hname,hident) =
- Hashcons.recursive_hcons Hconstr.f (hsorts,hkn,hname,hident)
+let hcons_term (hsorts,hcon,hkn,hname,hident) =
+ Hashcons.recursive_hcons Hconstr.f (hsorts,hcon,hkn,hname,hident)
(* Constructs a DeBrujin index with number n *)
let rels =
@@ -797,11 +798,11 @@ necessary.
For now, it uses map_constr and is rather ineffective
*)
-let rec map_kn f c =
- let func = map_kn f in
+let rec map_kn f f_con c =
+ let func = map_kn f f_con in
match kind_of_term c with
| Const kn ->
- mkConst (f kn)
+ mkConst (f_con kn)
| Ind (kn,i) ->
mkInd (f kn,i)
| Construct ((kn,i),j) ->
@@ -812,7 +813,7 @@ let rec map_kn f c =
| _ -> map_constr func c
let subst_mps sub =
- map_kn (subst_kn sub)
+ map_kn (subst_kn sub) (subst_con sub)
(*********************)
@@ -1178,9 +1179,9 @@ module Hsorts =
let hsort = Hsorts.f
-let hcons_constr (hkn,hdir,hname,hident,hstr) =
+let hcons_constr (hcon,hkn,hdir,hname,hident,hstr) =
let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
- let hcci = hcons_term (hsortscci,hkn,hname,hident) in
+ let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in
let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
(hcci,htcci)
diff --git a/kernel/term.mli b/kernel/term.mli
index 5ef42f96c1..2b84f79ba5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -512,6 +512,7 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
(*********************************************************************)
val hcons_constr:
+ (constant -> constant) *
(kernel_name -> kernel_name) *
(dir_path -> dir_path) *
(name -> name) *
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9d38c78f55..fb372d2f82 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -465,6 +465,6 @@ module Huniv =
end)
let hcons1_univ u =
- let _,hdir,_,_,_ = Names.hcons_names() in
+ let _,_,hdir,_,_,_ = Names.hcons_names() in
Hashcons.simple_hcons Huniv.f hdir u
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:04:52 +0000