aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c10
-rw-r--r--kernel/cbytegen.ml4
-rw-r--r--kernel/closure.ml3
-rw-r--r--kernel/closure.mli3
-rw-r--r--kernel/constr.mli3
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/names.mli16
-rw-r--r--kernel/nativecode.ml13
-rw-r--r--kernel/nativeconv.ml6
-rw-r--r--kernel/nativelib.ml16
-rw-r--r--kernel/nativelibrary.ml10
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/term_typing.ml6
-rw-r--r--kernel/vconv.ml2
15 files changed, 60 insertions, 37 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index bf383a33ac..df5fdce755 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -903,10 +903,12 @@ value coq_interprete
Alloc_small(block, 2, ATOM_PROJ_TAG);
Field(block, 0) = Field(coq_global_data, *pc);
Field(block, 1) = accu;
- /* Create accumulator */
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu, 1) = block;
+ accu = block;
+ /* Create accumulator */
+ Alloc_small(block, 2, Accu_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = accu;
+ accu = block;
} else {
accu = Field(accu, *pc++);
}
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 77eac9ee93..431c914c08 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -904,10 +904,10 @@ let compile fail_on_error ?universes:(universes=0) env c =
in
let fv = List.rev (!(reloc.in_env).fv_rev) in
(if !Flags.dump_bytecode then
- Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+ Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive tname ->
- let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+ let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in
(Pp.(fn
(str "Cannot compile code for virtual machine as it uses inductive " ++
Id.print tname ++ str str_max_constructors));
diff --git a/kernel/closure.ml b/kernel/closure.ml
index bf3801e547..960bdb649a 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -45,7 +45,7 @@ let reset () =
prune := 0
let stop() =
- msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+ Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++
str"]")
@@ -363,6 +363,7 @@ let set_norm v = v.norm <- Norm
let is_val v = match v.norm with Norm -> true | _ -> false
let mk_atom c = {norm=Norm;term=FAtom c}
+let mk_red f = {norm=Red;term=f}
(* Could issue a warning if no is still Red, pointing out that we loose
sharing. *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 07176cb7de..8e172290fb 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -164,6 +164,9 @@ val inject : constr -> fconstr
(** mk_atom: prevents a term from being evaluated *)
val mk_atom : constr -> fconstr
+(** mk_red: makes a reducible term (used in newring) *)
+val mk_red : fterm -> fconstr
+
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> constr
val destFLambda :
diff --git a/kernel/constr.mli b/kernel/constr.mli
index f76b5ae4f0..42d298e3b9 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -6,6 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file defines the most important datatype of Coq, namely kernel terms,
+ as well as a handful of generic manipulation functions. *)
+
open Names
(** {6 Value under universe substitution } *)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index f7220c94a1..1e132e3ab2 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,7 +15,6 @@ Copcodes
Cemitcodes
Nativevalues
Primitives
-Nativeinstr
Opaqueproof
Declareops
Retroknowledge
diff --git a/kernel/names.ml b/kernel/names.ml
index e8226d3d32..9abc9842a8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -36,7 +36,7 @@ struct
let check_soft ?(warn = true) x =
let iter (fatal, x) =
- if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
+ if fatal then Errors.error x else if warn then Feedback.msg_warning (str x)
in
Option.iter iter (Unicode.ident_refutation x)
diff --git a/kernel/names.mli b/kernel/names.mli
index 1dfdd82903..feaedc775c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,6 +6,20 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file defines a lot of different notions of names used pervasively in
+ the kernel as well as in other places. The essential datatypes exported by
+ this API are:
+
+ - Id.t is the type of identifiers, that is morally a subset of strings which
+ only contains Unicode characters of the Letter kind (and a few more).
+ - Name.t is an ad-hoc variant of Id.t option allowing to handle optionally
+ named objects.
+ - DirPath.t represents generic paths as sequences of identifiers.
+ - Label.t is an equivalent of Id.t made distinct for semantical purposes.
+ - ModPath.t are module paths.
+ - KerName.t are absolute names of objects in Coq.
+*)
+
open Util
(** {6 Identifiers } *)
@@ -766,7 +780,7 @@ val mind_of_kn : KerName.t -> mutual_inductive
(** @deprecated Same as [MutInd.make1] *)
val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make2] *)
+(** @deprecated Same as [MutInd.make] *)
val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
(** @deprecated Same as [MutInd.make3] *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index dabe905dee..44cf21cff0 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1486,8 +1486,8 @@ let optimize_stk stk =
(** Printing to ocaml **)
(* Redefine a bunch of functions in module Names to generate names
acceptable to OCaml. *)
-let string_of_id s = Unicode.ascii_of_ident (string_of_id s)
-let string_of_label l = Unicode.ascii_of_ident (string_of_label l)
+let string_of_id s = Unicode.ascii_of_ident (Id.to_string s)
+let string_of_label l = string_of_id (Label.to_id l)
let string_of_dirpath = function
| [] -> "_"
@@ -1560,8 +1560,7 @@ let pp_gname fmt g =
Format.fprintf fmt "%s" (string_of_gname g)
let pp_lname fmt ln =
- let s = Unicode.ascii_of_ident (string_of_name ln.lname) in
- Format.fprintf fmt "x_%s_%i" s ln.luid
+ Format.fprintf fmt "x_%s_%i" (string_of_name ln.lname) ln.luid
let pp_ldecls fmt ids =
let len = Array.length ids in
@@ -1864,7 +1863,7 @@ let compile_constant env sigma prefix ~interactive con cb =
| Def t ->
let t = Mod_subst.force_constr t in
let code = lambda_of_constr env sigma t in
- if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
let is_lazy = is_lazy prefix t in
let code = if is_lazy then mk_lazy code else code in
let name =
@@ -1879,11 +1878,11 @@ let compile_constant env sigma prefix ~interactive con cb =
let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
(auxdefs,mkMLlam [|univ|] code)
in
- if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
let code =
optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs)
in
- if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
code, name
| _ ->
let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 4ed926f1fe..a0ff9e123a 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -134,12 +134,12 @@ let native_conv_gen pb sigma env univs t1 t2 =
match compile ml_filename code with
| (true, fn) ->
begin
- if !Flags.debug then Pp.msg_debug (Pp.str "Running test...");
+ 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 Pp.msg_debug (Pp.str time_info);
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
(* TODO change 0 when we can have deBruijn *)
fst (conv_val env pb 0 !rt1 !rt2 univs)
end
@@ -149,7 +149,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
let native_conv cv_pb sigma env t1 t2 =
if Coq_config.no_native_compiler then begin
let msg = "Native compiler is disabled, falling back to VM conversion test." in
- Pp.msg_warning (Pp.str msg);
+ Feedback.msg_warning (Pp.str msg);
vm_conv cv_pb env t1 t2
end
else
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4296b73abe..5b92e9554f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -73,20 +73,20 @@ let call_compiler ml_filename =
::"-w"::"a"
::include_dirs
@ ["-impl"; ml_filename] in
- if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+ if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
try
let res = CUnix.sys_command (ocamlfind ()) args in
let res = match res with
| Unix.WEXITED 0 -> true
| Unix.WEXITED n ->
- Pp.(msg_warning (str "command exited with status " ++ int n)); false
+ Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
| Unix.WSIGNALED n ->
- Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+ Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
| Unix.WSTOPPED n ->
- Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+ Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
res, link_filename
with Unix.Unix_error (e,_,_) ->
- Pp.(msg_warning (str (Unix.error_message e)));
+ Feedback.msg_warning Pp.(str (Unix.error_message e));
false, link_filename
let compile fn code =
@@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds =
begin
let msg = "Cannot find native compiler file " ^ f in
if fatal then Errors.error msg
- else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+ else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
end
else
(try
@@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds =
with Dynlink.Error e as exn ->
let exn = Errors.push exn in
let msg = "Dynlink error, " ^ Dynlink.error_message e in
- if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
- else if !Flags.debug then Pp.msg_debug (Pp.str msg));
+ if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
+ else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
match upds with Some upds -> update_locations upds | _ -> ()
let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 9d159be64c..246b00da40 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -29,13 +29,13 @@ and translate_field prefix mp env acc (l,x) =
let con = make_con mp empty_dirpath l in
(if !Flags.debug then
let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
- Pp.msg_debug (Pp.str msg));
+ Feedback.msg_debug (Pp.str msg));
compile_constant_field (pre_env env) prefix con acc cb
| SFBmind mb ->
(if !Flags.debug then
let id = mb.mind_packets.(0).mind_typename in
let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
- Pp.msg_debug (Pp.str msg));
+ Feedback.msg_debug (Pp.str msg));
compile_mind_field prefix mp l acc mb
| SFBmodule md ->
let mp = md.mod_mp in
@@ -43,7 +43,7 @@ and translate_field prefix mp env acc (l,x) =
let msg =
Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
in
- Pp.msg_debug (Pp.str msg));
+ Feedback.msg_debug (Pp.str msg));
translate_mod prefix mp env md.mod_type acc
| SFBmodtype mdtyp ->
let mp = mdtyp.mod_mp in
@@ -51,11 +51,11 @@ and translate_field prefix mp env acc (l,x) =
let msg =
Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
in
- Pp.msg_debug (Pp.str msg));
+ Feedback.msg_debug (Pp.str msg));
translate_mod prefix mp env mdtyp.mod_type acc
let dump_library mp dp env mod_expr =
- if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
match mod_expr with
| NoFunctor struc ->
let env = add_structure mp struc empty_delta_resolver env in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5bf369441f..30a346c910 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -681,7 +681,7 @@ let vm_conv cv_pb env t1 t2 =
try
!vm_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
- Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+ Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
gen_conv cv_pb env t1 t2
let default_conv cv_pb ?(l2r=false) env t1 t2 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3839135a86..6bfd2457a8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -167,8 +167,10 @@ let hcons_j j =
{ uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type}
let feedback_completion_typecheck =
- Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
+ let open Feedback in
+ Option.iter (fun state_id ->
+ feedback ~id:(State state_id) Feedback.Complete)
+
let infer_declaration ~trust env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 89e833254a..53db6f5bee 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,7 +185,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
let v2 = val_of_constr env t2 in
fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
with Not_found | Invalid_argument _ ->
- (Pp.msg_warning
+ (Feedback.msg_warning
(Pp.str "Bytecode compilation failed, falling back to default conversion");
Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
full_transparent_state env univs t1 t2)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 07:55:24 +0000