aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/CODEOWNERS1
-rw-r--r--Makefile.build2
-rw-r--r--Makefile.make2
-rw-r--r--dev/vm_printers.ml2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/dune2
-rw-r--r--kernel/genOpcodeFiles.ml6
-rw-r--r--kernel/kernel.mllib12
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/nativelambda.ml4
-rw-r--r--kernel/term_typing.ml8
-rw-r--r--kernel/vconv.ml2
-rw-r--r--kernel/vm.ml2
-rw-r--r--kernel/vmbytecodes.ml (renamed from kernel/cbytecodes.ml)0
-rw-r--r--kernel/vmbytecodes.mli (renamed from kernel/cbytecodes.mli)0
-rw-r--r--kernel/vmbytegen.ml (renamed from kernel/cbytegen.ml)10
-rw-r--r--kernel/vmbytegen.mli (renamed from kernel/cbytegen.mli)4
-rw-r--r--kernel/vmemitcodes.ml (renamed from kernel/cemitcodes.ml)6
-rw-r--r--kernel/vmemitcodes.mli (renamed from kernel/cemitcodes.mli)2
-rw-r--r--kernel/vmlambda.ml (renamed from kernel/clambda.ml)6
-rw-r--r--kernel/vmlambda.mli (renamed from kernel/clambda.mli)0
-rw-r--r--kernel/vmsymtable.ml (renamed from kernel/csymtable.ml)8
-rw-r--r--kernel/vmsymtable.mli (renamed from kernel/csymtable.mli)0
-rw-r--r--pretyping/vnorm.ml2
-rw-r--r--tactics/redexpr.ml4
-rw-r--r--vernac/vernacentries.ml8
28 files changed, 52 insertions, 51 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index bb0beb142a..b7418f54bd 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -106,6 +106,7 @@
/kernel/native* @coq/vm-native-maintainers
/kernel/vm* @coq/vm-native-maintainers
/kernel/vconv.* @coq/vm-native-maintainers
+/kernel/genOpcodefiles.* @coq/vm-native-maintainers
/kernel/sorts.* @coq/universes-maintainers
/kernel/uGraph.* @coq/universes-maintainers
diff --git a/Makefile.build b/Makefile.build
index 7806dce79c..4fb4b12be2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -367,7 +367,7 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe
$(SHOW)'WRITE $@'
$(HIDE)$< jump > $@
-kernel/copcodes.ml: kernel/genOpcodeFiles.exe
+kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe
$(SHOW)'WRITE $@'
$(HIDE)$< copml > $@
diff --git a/Makefile.make b/Makefile.make
index 7191738612..51d6d1c3c1 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES))
GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES?
GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml
GENMLIFILES:=$(GRAMMLIFILES)
GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index ac4972ed0d..1eacfa0fd6 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,7 +1,7 @@
open Format
open Term
open Names
-open Cemitcodes
+open Vmemitcodes
open Vmvalues
let ppripos (ri,pos) =
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7609c1a64d..9c32cd8e0e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -107,7 +107,7 @@ type 'opaque constant_body = {
const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
const_type : types;
const_relevance : Sorts.relevance;
- const_body_code : Cemitcodes.to_patch_substituted option;
+ const_body_code : Vmemitcodes.to_patch_substituted option;
const_universes : universes;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 326bf0d6ad..b9f434f179 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -116,7 +116,7 @@ let subst_const_body sub cb =
const_body = body';
const_type = type';
const_body_code =
- Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
+ Option.map (Vmemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_universes = cb.const_universes;
const_relevance = cb.const_relevance;
const_inline_code = cb.const_inline_code;
diff --git a/kernel/dune b/kernel/dune
index 5f7502ef6b..ce6fdc03df 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -11,7 +11,7 @@
(modules genOpcodeFiles))
(rule
- (targets copcodes.ml)
+ (targets vmopcodes.ml)
(action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml))))
(rule
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 67a672c349..2d74cca44c 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -11,7 +11,7 @@
(** List of opcodes.
It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and
- [copcodes.ml] files.
+ [vmopcodes.ml] files.
If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c
with the arity of the instruction and maybe coq_tcode_of_code.
@@ -196,7 +196,7 @@ let pp_coq_instruct_h fmt =
let pp_coq_jumptbl_h fmt =
pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s")
-let pp_copcodes_ml fmt =
+let pp_vmopcodes_ml fmt =
pp_header true fmt;
Array.iteri (fun n s ->
Format.fprintf fmt "let op%s = %d@.@." s n
@@ -210,7 +210,7 @@ let main () =
match Sys.argv.(1) with
| "enum" -> pp_coq_instruct_h Format.std_formatter
| "jump" -> pp_coq_jumptbl_h Format.std_formatter
- | "copml" -> pp_copcodes_ml Format.std_formatter
+ | "copml" -> pp_vmopcodes_ml Format.std_formatter
| _ -> usage ()
| exception Invalid_argument _ -> usage ()
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 41388d9f17..d4d7150222 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,9 +15,9 @@ Term
CPrimitives
Mod_subst
Vmvalues
-Cbytecodes
-Copcodes
-Cemitcodes
+Vmbytecodes
+Vmopcodes
+Vmemitcodes
Opaqueproof
Declarations
Entries
@@ -30,12 +30,12 @@ Primred
CClosure
Relevanceops
Reduction
-Clambda
+Vmlambda
Nativelambda
-Cbytegen
+Vmbytegen
Nativecode
Nativelib
-Csymtable
+Vmsymtable
Vm
Vconv
Nativeconv
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 44b010204b..5873d1f502 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -124,8 +124,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
{ cb with
const_body = def;
const_universes = univs ;
- const_body_code = Option.map Cemitcodes.from_val
- (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
+ const_body_code = Option.map Vmemitcodes.from_val
+ (Vmbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
else
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 77ef38dfd5..883ad79be5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -328,7 +328,7 @@ let strengthen_const mp_from l cb resolver =
let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
- const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
+ const_body_code = Some (Vmemitcodes.from_val (Vmbytegen.compile_alias con)) }
let rec strengthen_mod mp_from mp_to mb =
if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b00b96018f..99090f0147 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -395,8 +395,8 @@ let rec get_alias env (kn, u as p) =
match tps with
| None -> p
| Some tps ->
- match Cemitcodes.force tps with
- | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
+ match Vmemitcodes.force tps with
+ | Vmemitcodes.BCalias kn' -> get_alias env (kn', u)
| _ -> p
let prim env kn p args =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 48567aa564..24aa4ed771 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -283,8 +283,8 @@ let build_constant_declaration env result =
let univs = result.cook_universes in
let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
let tps =
- let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
- Option.map Cemitcodes.from_val res
+ let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs def in
+ Option.map Vmemitcodes.from_val res
in
{ const_hyps = hyps;
const_body = def;
@@ -343,8 +343,8 @@ let translate_recipe env _kn r =
let open Cooking in
let result = Cooking.cook_constant r in
let univs = result.cook_universes in
- let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
- let tps = Option.map Cemitcodes.from_val res in
+ let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
+ let tps = Option.map Vmemitcodes.from_val res in
let hyps = Option.get result.cook_context in
(* Trust the set of section hypotheses generated by Cooking *)
let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index f78f0d4d1e..cc2c2c0b4b 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -4,7 +4,7 @@ open Environ
open Reduction
open Vm
open Vmvalues
-open Csymtable
+open Vmsymtable
(* Test la structure des piles *)
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d8c66bebd2..76954a83d8 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -44,7 +44,7 @@ external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -
"coq_interprete_byte" "coq_interprete_ml"
let interprete code v env k =
- coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k
+ coq_interprete code v (get_atom_rel ()) (Vmsymtable.get_global_data ()) env k
(* Functions over arguments *)
diff --git a/kernel/cbytecodes.ml b/kernel/vmbytecodes.ml
index 74405a0105..74405a0105 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/vmbytecodes.ml
diff --git a/kernel/cbytecodes.mli b/kernel/vmbytecodes.mli
index b703058fb7..b703058fb7 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/vmbytecodes.mli
diff --git a/kernel/cbytegen.ml b/kernel/vmbytegen.ml
index bacc308e1f..1274e3a867 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -15,9 +15,9 @@
open Util
open Names
open Vmvalues
-open Cbytecodes
-open Cemitcodes
-open Clambda
+open Vmbytecodes
+open Vmemitcodes
+open Vmlambda
open Constr
open Declarations
open Environ
@@ -116,7 +116,7 @@ end
module FvMap = Map.Make(Fv_elem)
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Vmbytegen because I needed then
for the retroknowledge *)
type vm_env = {
size : int; (* longueur de la liste [n] *)
@@ -512,7 +512,7 @@ let rec get_alias env kn =
match tps with
| None -> kn
| Some tps ->
- (match Cemitcodes.force tps with
+ (match Vmemitcodes.force tps with
| BCalias kn' -> get_alias env kn'
| _ -> kn)
diff --git a/kernel/cbytegen.mli b/kernel/vmbytegen.mli
index d5ea2509ef..aef7ac3d6b 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/vmbytegen.mli
@@ -8,8 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Cbytecodes
-open Cemitcodes
+open Vmbytecodes
+open Vmemitcodes
open Constr
open Declarations
open Environ
diff --git a/kernel/cemitcodes.ml b/kernel/vmemitcodes.ml
index ed475dca7e..2dfc9a2941 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -14,8 +14,8 @@
open Names
open Vmvalues
-open Cbytecodes
-open Copcodes
+open Vmbytecodes
+open Vmopcodes
open Mod_subst
open CPrimitives
@@ -350,7 +350,7 @@ let emit_instr env = function
| Ksetfield n ->
if n <= 1 then out env (opSETFIELD0+n)
else (out env opSETFIELD;out_int env n)
- | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+ | Ksequence _ -> invalid_arg "Vmemitcodes.emit_instr"
| Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
| Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
| Kbranch lbl -> out env opBRANCH; out_label env lbl
diff --git a/kernel/cemitcodes.mli b/kernel/vmemitcodes.mli
index c4262f3380..5c0e103143 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/vmemitcodes.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open Names
open Vmvalues
-open Cbytecodes
+open Vmbytecodes
type reloc_info =
| Reloc_annot of annot_switch
diff --git a/kernel/clambda.ml b/kernel/vmlambda.ml
index 6690a379ce..332a331a7a 100644
--- a/kernel/clambda.ml
+++ b/kernel/vmlambda.ml
@@ -559,8 +559,8 @@ let rec get_alias env kn =
match tps with
| None -> kn
| Some tps ->
- (match Cemitcodes.force tps with
- | Cemitcodes.BCalias kn' -> get_alias env kn'
+ (match Vmemitcodes.force tps with
+ | Vmemitcodes.BCalias kn' -> get_alias env kn'
| _ -> kn)
(* Compilation of primitive *)
@@ -681,7 +681,7 @@ open Renv
let rec lambda_of_constr env c =
match Constr.kind c with
- | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
+ | Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta")
| Evar (evk, args) ->
let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
Levar (evk, args)
diff --git a/kernel/clambda.mli b/kernel/vmlambda.mli
index bd11c2667f..bd11c2667f 100644
--- a/kernel/clambda.mli
+++ b/kernel/vmlambda.mli
diff --git a/kernel/csymtable.ml b/kernel/vmsymtable.ml
index 185fb9f5a4..85f7369654 100644
--- a/kernel/csymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -17,11 +17,11 @@
open Util
open Names
open Vmvalues
-open Cemitcodes
-open Cbytecodes
+open Vmemitcodes
+open Vmbytecodes
open Declarations
open Environ
-open Cbytegen
+open Vmbytegen
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
@@ -155,7 +155,7 @@ let rec slot_for_getglobal env kn =
match cb.const_body_code with
| None -> set_global (val_of_constant kn)
| Some code ->
- match Cemitcodes.force code with
+ match Vmemitcodes.force code with
| BCdefined(code,pl,fv) ->
let v = eval_to_patch env (code,pl,fv) in
set_global v
diff --git a/kernel/csymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..e480bfcec1 100644
--- a/kernel/csymtable.mli
+++ b/kernel/vmsymtable.mli
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index e5fa9bada1..900ba0edb9 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -415,7 +415,7 @@ let cbv_vm env sigma c t =
(* This evar-normalizes terms beforehand *)
let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
- let v = Csymtable.val_of_constr env c in
+ let v = Vmsymtable.val_of_constr env c in
EConstr.of_constr (nf_val env sigma v t)
let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index c463c06cd5..a8747e0a7c 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -60,7 +60,7 @@ let set_strategy_one ref l =
Global.set_strategy k l;
match k,l with
ConstKey sp, Conv_oracle.Opaque ->
- Csymtable.set_opaque_const sp
+ Vmsymtable.set_opaque_const sp
| ConstKey sp, _ ->
let cb = Global.lookup_constant sp in
(match cb.const_body with
@@ -69,7 +69,7 @@ let set_strategy_one ref l =
(str "Cannot make" ++ spc () ++
Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.");
- | _ -> Csymtable.set_transparent_const sp)
+ | _ -> Vmsymtable.set_transparent_const sp)
| _ -> ()
let cache_strategy (_,str) =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4e08a40d6b..540e85621a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1516,15 +1516,15 @@ let () =
declare_bool_option
{ optdepr = false;
optkey = ["Dump";"Bytecode"];
- optread = (fun () -> !Cbytegen.dump_bytecode);
- optwrite = (:=) Cbytegen.dump_bytecode }
+ optread = (fun () -> !Vmbytegen.dump_bytecode);
+ optwrite = (:=) Vmbytegen.dump_bytecode }
let () =
declare_bool_option
{ optdepr = false;
optkey = ["Dump";"Lambda"];
- optread = (fun () -> !Clambda.dump_lambda);
- optwrite = (:=) Clambda.dump_lambda }
+ optread = (fun () -> !Vmlambda.dump_lambda);
+ optwrite = (:=) Vmlambda.dump_lambda }
let () =
declare_bool_option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:22:24 +0000