aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml46
-rw-r--r--kernel/nativeconv.ml23
-rw-r--r--kernel/nativelambda.ml37
-rw-r--r--kernel/nativelambda.mli2
-rw-r--r--kernel/nativelib.ml25
-rw-r--r--kernel/nativelib.mli11
6 files changed, 62 insertions, 82 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2dab14e732..d7ec2ecf72 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -51,7 +51,6 @@ let fresh_lname n =
(** Global names **)
type gname =
| Gind of string * inductive (* prefix, inductive name *)
- | Gconstruct of string * constructor (* prefix, constructor name *)
| Gconstant of string * Constant.t (* prefix, constant name *)
| Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *)
| Gcase of Label.t option * int
@@ -67,8 +66,6 @@ let eq_gname gn1 gn2 =
match gn1, gn2 with
| Gind (s1, ind1), Gind (s2, ind2) ->
String.equal s1 s2 && eq_ind ind1 ind2
- | Gconstruct (s1, c1), Gconstruct (s2, c2) ->
- String.equal s1 s2 && eq_constructor c1 c2
| Gconstant (s1, c1), Gconstant (s2, c2) ->
String.equal s1 s2 && Constant.equal c1 c2
| Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) ->
@@ -88,7 +85,7 @@ let eq_gname gn1 gn2 =
| Ginternal s1, Ginternal s2 -> String.equal s1 s2
| Grel i1, Grel i2 -> Int.equal i1 i2
| Gnamed id1, Gnamed id2 -> Id.equal id1 id2
- | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _
+ | (Gind _| Gconstant _ | Gproj _ | Gcase _ | Gpred _
| Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ ->
false
@@ -100,19 +97,17 @@ open Hashset.Combine
let gname_hash gn = match gn with
| Gind (s, ind) ->
combinesmall 1 (combine (String.hash s) (ind_hash ind))
-| Gconstruct (s, c) ->
- combinesmall 2 (combine (String.hash s) (constructor_hash c))
| Gconstant (s, c) ->
- combinesmall 3 (combine (String.hash s) (Constant.hash c))
-| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i))
-| Ginternal s -> combinesmall 9 (String.hash s)
-| Grel i -> combinesmall 10 (Int.hash i)
-| Gnamed id -> combinesmall 11 (Id.hash id)
-| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i))
+ combinesmall 2 (combine (String.hash s) (Constant.hash c))
+| Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnorm (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnormtbl (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
+| Ginternal s -> combinesmall 8 (String.hash s)
+| Grel i -> combinesmall 9 (Int.hash i)
+| Gnamed id -> combinesmall 10 (Id.hash id)
+| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i))
let case_ctr = ref (-1)
@@ -1280,9 +1275,6 @@ let ml_of_instance instance u =
| Lmakeblock (prefix,(cn,_u),_,args) ->
let args = Array.map (ml_of_lam env l) args in
MLconstruct(prefix,cn,args)
- | Lconstruct (prefix, (cn,u)) ->
- let uargs = ml_of_instance env.env_univ u in
- mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs
| Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
| Lval v ->
let i = push_symbol (SymbValue v) in get_value_code i
@@ -1533,8 +1525,6 @@ let string_of_gname g =
match g with
| Gind (prefix, (mind, i)) ->
Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
- | Gconstruct (prefix, ((mind, i), j)) ->
- Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
| Gconstant (prefix, c) ->
Format.sprintf "%sconst_%s" prefix (string_of_con c)
| Gproj (prefix, (mind, n), i) ->
@@ -1932,16 +1922,6 @@ let compile_mind mb mind stack =
Glet(name, MLapp (MLprimitive Mk_ind, args))
in
let nparams = mb.mind_nparams in
- let params =
- Array.init nparams (fun i -> {lname = param_name; luid = i}) in
- let add_construct j acc (_,arity) =
- let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in
- let c = ind, (j+1) in
- Glet(Gconstruct ("", c),
- mkMLlam (Array.append params args)
- (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
- in
- let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
let add_proj proj_arg acc _pb =
let tbl = ob.mind_reloc_tbl in
(* Building info *)
@@ -1958,7 +1938,7 @@ let compile_mind mb mind stack =
let cargs = Array.init arity
(fun i -> if Int.equal i proj_arg then Some ci_uid else None)
in
- let i = push_symbol (SymbProj (ind, j)) in
+ let i = push_symbol (SymbProj (ind, proj_arg)) in
let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
@@ -1972,7 +1952,7 @@ let compile_mind mb mind stack =
let _, _, _, pbs = info.(i) in
Array.fold_left_i add_proj [] pbs
in
- projs @ constructors @ gtype :: accu :: stack
+ projs @ gtype :: accu :: stack
in
Array.fold_left_i f stack mb.mind_packets
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index baa290367f..d153f84e9c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open CErrors
open Names
open Nativelib
open Reduction
@@ -152,19 +151,15 @@ let native_conv_gen pb sigma env univs t1 t2 =
else
let ml_filename, prefix = get_ml_filename () in
let code, upds = mk_conv_code env sigma prefix t1 t2 in
- match compile ml_filename code ~profile:false with
- | (true, fn) ->
- begin
- if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
- let t0 = Sys.time () in
- call_linker ~fatal:true prefix fn (Some upds);
- let t1 = Sys.time () in
- let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
- if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
- (* TODO change 0 when we can have de Bruijn *)
- fst (conv_val env pb 0 !rt1 !rt2 univs)
- end
- | _ -> anomaly (Pp.str "Compilation failure.")
+ let fn = compile ml_filename code ~profile:false in
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+ let t0 = Sys.time () in
+ call_linker ~fatal:true prefix fn (Some upds);
+ let t1 = Sys.time () in
+ let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+ (* TODO change 0 when we can have de Bruijn *)
+ fst (conv_val env pb 0 !rt1 !rt2 univs)
(* Wrapper for [native_conv] above *)
let native_conv cv_pb sigma env t1 t2 =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index ec3a7b893d..d88be94b39 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -42,8 +42,6 @@ type lambda =
| Lmakeblock of prefix * pconstructor * int * lambda array
(* prefix, constructor Name.t, constructor tag, arguments *)
(* A fully applied constructor *)
- | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *)
- (* A partially applied constructor *)
| Luint of Uint63.t
| Lval of Nativevalues.t
| Lsort of Sorts.t
@@ -121,7 +119,7 @@ let get_const_prefix env c =
let map_lam_with_binders g f n lam =
match lam with
| Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
- | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam
+ | Llazy | Lforce | Lmeta _ -> lam
| Lprod(dom,codom) ->
let dom' = f n dom in
let codom' = f n codom in
@@ -222,7 +220,7 @@ let lam_subst_args subst args =
let can_subst lam =
match lam with
| Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Llam _
- | Lconstruct _ | Lmeta _ | Levar _ -> true
+ | Lmeta _ | Levar _ -> true
| _ -> false
let can_merge_if bt bf =
@@ -337,9 +335,20 @@ let make_args start _end =
Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
(* Translation of constructors *)
+let expand_constructor prefix cstr tag nparams arity =
+ let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+ let ids = Array.make (nparams + arity) anon in
+ let args = make_args arity 1 in
+ Llam(ids, Lmakeblock (prefix, cstr, tag, args))
-let makeblock env cn u tag args =
- if Array.for_all is_value args && Array.length args > 0 then
+(* [nparams] is the number of parameters still expected *)
+let makeblock env cn u tag nparams arity args =
+ let nargs = Array.length args in
+ if nparams > 0 || nargs < arity then
+ let prefix = get_mind_prefix env (fst (fst cn)) in
+ mkLapp (expand_constructor prefix (cn,u) tag nparams arity) args
+ else
+ if Array.for_all is_value args && nargs > 0 then
let args = Array.map get_value args in
Lval (Nativevalues.mk_block tag args)
else
@@ -573,16 +582,12 @@ and lambda_of_app cache env sigma f args =
mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args)
end
| Construct (c,u) ->
- let tag, nparams, arity = Cache.get_construct_info cache env c in
- let expected = nparams + arity in
- let nargs = Array.length args in
- let prefix = get_mind_prefix env (fst (fst c)) in
- if Int.equal nargs expected then
- let args = lambda_of_args cache env sigma nparams args in
- makeblock env c u tag args
- else
- let args = lambda_of_args cache env sigma 0 args in
- mkLapp (Lconstruct (prefix, (c,u))) args
+ let tag, nparams, arity = Cache.get_construct_info cache env c in
+ let nargs = Array.length args in
+ if nparams < nargs then (* got all parameters *)
+ let args = lambda_of_args cache env sigma nparams args in
+ makeblock env c u tag 0 arity args
+ else makeblock env c u tag (nparams - nargs) arity empty_args
| _ ->
let f = lambda_of_constr cache env sigma f in
let args = lambda_of_args cache env sigma 0 args in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index b0de257a27..687789e82b 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -36,8 +36,6 @@ type lambda =
| Lmakeblock of prefix * pconstructor * int * lambda array
(* prefix, constructor Name.t, constructor tag, arguments *)
(* A fully applied constructor *)
- | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *)
- (* A partially applied constructor *)
| Luint of Uint63.t
| Lval of Nativevalues.t
| Lsort of Sorts.t
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 833e4082f0..43c9676f05 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -56,14 +56,15 @@ let write_ml_code fn ?(header=[]) code =
List.iter (pp_global fmt) (header@code);
close_out ch_out
-let warn_native_compiler_failed =
- let print = function
+let error_native_compiler_failed e =
+ let msg = match e with
+ | Inl (Unix.WEXITED 127) -> Pp.(strbrk "The OCaml compiler was not found. Make sure it is installed, together with findlib.")
| Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
| Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
| Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
| Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
in
- CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
+ CErrors.user_err msg
let call_compiler ?profile:(profile=false) ml_filename =
let load_path = !get_load_paths () in
@@ -100,15 +101,12 @@ let call_compiler ?profile:(profile=false) ml_filename =
if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
try
let res = CUnix.sys_command (Envars.ocamlfind ()) args in
- let res = match res with
- | Unix.WEXITED 0 -> true
- | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
- warn_native_compiler_failed (Inl res); false
- in
- res, link_filename
+ match res with
+ | Unix.WEXITED 0 -> link_filename
+ | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
+ error_native_compiler_failed (Inl res)
with Unix.Unix_error (e,_,_) ->
- warn_native_compiler_failed (Inr e);
- false, link_filename
+ error_native_compiler_failed (Inr e)
let compile fn code ~profile:profile =
write_ml_code fn code;
@@ -128,9 +126,8 @@ let compile_library dir code fn =
in
let fn = dirname / basename in
write_ml_code fn ~header code;
- let r = fst (call_compiler fn) in
- if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
- r
+ let _ = call_compiler fn in
+ if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
(* call_linker links dynamically the code for constants in environment or a *)
(* conversion test. *)
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 25adcf224b..e113350368 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,9 +21,14 @@ val load_obj : (string -> unit) ref
val get_ml_filename : unit -> string * string
-val compile : string -> global list -> profile:bool -> bool * string
-
-val compile_library : Names.DirPath.t -> global list -> string -> bool
+(** [compile file code ~profile] will compile native [code] to [file],
+ and return the name of the object file; this name depends on
+ whether are in byte mode or not; file is expected to be .ml file *)
+val compile : string -> global list -> profile:bool -> string
+
+(** [compile_library lib code file] is similar to [compile file code]
+ but will perform some extra tweaks to handle [code] as a Coq lib. *)
+val compile_library : Names.DirPath.t -> global list -> string -> unit
val call_linker :
?fatal:bool -> string -> string -> code_location_updates option -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 21:41:35 +0000