aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cPrimitives.ml (renamed from kernel/primitives.ml)0
-rw-r--r--kernel/cPrimitives.mli (renamed from kernel/primitives.mli)0
-rw-r--r--kernel/environ.ml34
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/nativecode.ml16
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/nativeinstr.mli2
-rw-r--r--kernel/nativelambda.mli2
-rw-r--r--kernel/nativelib.ml32
-rw-r--r--kernel/nativelib.mli2
-rw-r--r--kernel/pre_env.ml2
11 files changed, 53 insertions, 41 deletions
diff --git a/kernel/primitives.ml b/kernel/cPrimitives.ml
index 14c11bf107..14c11bf107 100644
--- a/kernel/primitives.ml
+++ b/kernel/cPrimitives.ml
diff --git a/kernel/primitives.mli b/kernel/cPrimitives.mli
index 8cdffb6702..8cdffb6702 100644
--- a/kernel/primitives.mli
+++ b/kernel/cPrimitives.mli
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d2c737ab0c..621a9931de 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -624,39 +624,39 @@ fun rk value field ->
native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
}
| KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
- Primitives.Int31add
+ CPrimitives.Int31add
| KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
- Primitives.Int31addc
+ CPrimitives.Int31addc
| KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
- Primitives.Int31addcarryc
+ CPrimitives.Int31addcarryc
| KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
- Primitives.Int31sub
+ CPrimitives.Int31sub
| KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
- Primitives.Int31subc
+ CPrimitives.Int31subc
| KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
- Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc
+ Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
| KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
- Primitives.Int31mul
+ CPrimitives.Int31mul
| KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
- Primitives.Int31mulc
+ CPrimitives.Int31mulc
| KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
- Primitives.Int31div21
+ CPrimitives.Int31div21
| KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
- Primitives.Int31diveucl
+ CPrimitives.Int31diveucl
| KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
- Primitives.Int31addmuldiv
+ CPrimitives.Int31addmuldiv
| KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
- Primitives.Int31compare
+ CPrimitives.Int31compare
| KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
- Primitives.Int31head0
+ CPrimitives.Int31head0
| KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
- Primitives.Int31tail0
+ CPrimitives.Int31tail0
| KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
- Primitives.Int31lor
+ CPrimitives.Int31lor
| KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
- Primitives.Int31land
+ CPrimitives.Int31land
| KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
- Primitives.Int31lxor
+ CPrimitives.Int31lxor
| _ -> empty_reactive_info
let _ = Hook.set Retroknowledge.dispatch_hook dispatch
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 9946348541..917e4f6f14 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -17,7 +17,7 @@ Opaqueproof
Declarations
Entries
Nativevalues
-Primitives
+CPrimitives
Declareops
Retroknowledge
Conv_oracle
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index da7fcd6f23..e08d913bc6 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -296,7 +296,7 @@ type primitive =
| MLmagic
| MLarrayget
| Mk_empty_instance
- | Coq_primitive of Primitives.t * (prefix * constant) option
+ | Coq_primitive of CPrimitives.t * (prefix * constant) option
let eq_primitive p1 p2 =
match p1, p2 with
@@ -361,9 +361,9 @@ let primitive_hash = function
| MLsub -> 33
| MLmul -> 34
| MLmagic -> 35
- | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim)
+ | Coq_primitive (prim, None) -> combinesmall 36 (CPrimitives.hash prim)
| Coq_primitive (prim, Some (prefix,kn)) ->
- combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim))
+ combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim))
| Mk_proj -> 38
| MLarrayget -> 39
| Mk_empty_instance -> 40
@@ -921,7 +921,7 @@ let merge_branches t =
type prim_aux =
- | PAprim of string * constant * Primitives.t * prim_aux array
+ | PAprim of string * constant * CPrimitives.t * prim_aux array
| PAml of mllambda
let add_check cond args =
@@ -988,11 +988,11 @@ let compile_prim decl cond paux =
| Int31lt ->
if Sys.word_size = 64 then
app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|]
- else app_prim (Coq_primitive (Primitives.Int31lt,None)) args
+ else app_prim (Coq_primitive (CPrimitives.Int31lt,None)) args
| Int31le ->
if Sys.word_size = 64 then
app_prim Mk_bool [|(app_prim MLle (args_to_int args))|]
- else app_prim (Coq_primitive (Primitives.Int31le, None)) args
+ else app_prim (Coq_primitive (CPrimitives.Int31le, None)) args
| Int31lsl -> of_int (mk_lsl (args_to_int args))
| Int31lsr -> of_int (mk_lsr (args_to_int args))
| Int31land -> of_int (mk_land (args_to_int args))
@@ -1752,9 +1752,9 @@ let pp_mllam fmt l =
| MLarrayget -> Format.fprintf fmt "Array.get"
| Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty"
| Coq_primitive (op,None) ->
- Format.fprintf fmt "no_check_%s" (Primitives.to_string op)
+ Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op)
| Coq_primitive (op, Some (prefix,kn)) ->
- Format.fprintf fmt "%s %a" (Primitives.to_string op)
+ Format.fprintf fmt "%s %a" (CPrimitives.to_string op)
pp_mllam (MLglobal (Gconstant (prefix, kn)))
in
Format.fprintf fmt "@[%a@]" pp_mllam l
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index d2f050d3bc..a62a079da9 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -132,7 +132,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
let penv = Environ.pre_env env in
let ml_filename, prefix = get_ml_filename () in
let code, upds = mk_conv_code penv sigma prefix t1 t2 in
- match compile ml_filename code with
+ match compile ml_filename code ~profile:false with
| (true, fn) ->
begin
if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index cb79877e8b..2353470f01 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -30,7 +30,7 @@ and lambda =
| Lapp of lambda * lambda array
| Lconst of prefix * pconstant
| Lproj of prefix * constant (* prefix, projection name *)
- | Lprim of prefix * constant * Primitives.t * lambda array
+ | Lprim of prefix * constant * CPrimitives.t * lambda array
| Lcase of annot_sw * lambda * lambda * lam_branches
(* annotations, term being matched, accu, branches *)
| Lif of lambda * lambda * lambda
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index bfa3bf9418..156e4f834a 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda ->
lambda
-val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array ->
+val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array ->
lambda
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 02e02b031a..665ddf7a65 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -64,7 +64,7 @@ let warn_native_compiler_failed =
in
CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
-let call_compiler ml_filename =
+let call_compiler ?profile:(profile=false) ml_filename =
let load_path = !get_load_paths () in
let load_path = List.map (fun dn -> dn / output_dir) load_path in
let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in
@@ -74,14 +74,26 @@ let call_compiler ml_filename =
let remove f = if Sys.file_exists f then Sys.remove f in
remove link_filename;
remove (f ^ ".cmi");
+ let initial_args =
+ if Dynlink.is_native then
+ ["opt"; "-shared"]
+ else
+ ["ocamlc"; "-c"]
+ in
+ let profile_args =
+ if profile then
+ ["-g"]
+ else
+ []
+ in
let args =
- (if Dynlink.is_native then "opt" else "ocamlc")
- ::(if Dynlink.is_native then "-shared" else "-c")
- ::"-o"::link_filename
- ::"-rectypes"
- ::"-w"::"a"
- ::include_dirs
- @ ["-impl"; ml_filename] in
+ initial_args @
+ profile_args @
+ ("-o"::link_filename
+ ::"-rectypes"
+ ::"-w"::"a"
+ ::include_dirs) @
+ ["-impl"; ml_filename] in
if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
try
let res = CUnix.sys_command (ocamlfind ()) args in
@@ -95,9 +107,9 @@ let call_compiler ml_filename =
warn_native_compiler_failed (Inr e);
false, link_filename
-let compile fn code =
+let compile fn code ~profile:profile =
write_ml_code fn code;
- let r = call_compiler fn in
+ let r = call_compiler ~profile fn in
if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
r
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index e8b51dc366..a262a9f58a 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -19,7 +19,7 @@ val load_obj : (string -> unit) ref
val get_ml_filename : unit -> string * string
-val compile : string -> global list -> bool * string
+val compile : string -> global list -> profile:bool -> bool * string
val compile_library : Names.dir_path -> global list -> string -> bool
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 7b4fb4e869..94738d6186 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -156,7 +156,7 @@ let map_named_val f ctxt =
in
(accu, d')
in
- let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
+ let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
if map == ctxt.env_named_map then ctxt
else { env_named_ctx = ctx; env_named_map = map }
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:28:10 +0000