aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_gc.h59
-rw-r--r--kernel/byterun/coq_interp.c24
-rw-r--r--kernel/byterun/coq_memory.c5
-rw-r--r--kernel/float64.ml13
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/modops.ml30
-rw-r--r--kernel/reduction.ml8
-rw-r--r--kernel/relevanceops.ml (renamed from kernel/retypeops.ml)0
-rw-r--r--kernel/relevanceops.mli (renamed from kernel/retypeops.mli)0
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--kernel/vars.ml3
-rw-r--r--kernel/vars.mli3
12 files changed, 58 insertions, 91 deletions
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
deleted file mode 100644
index 38eda4d11f..0000000000
--- a/kernel/byterun/coq_gc.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/***********************************************************************/
-/* */
-/* Coq Compiler */
-/* */
-/* Benjamin Gregoire, projets Logical and Cristal */
-/* INRIA Rocquencourt */
-/* */
-/* */
-/***********************************************************************/
-
-#ifndef _COQ_CAML_GC_
-#define _COQ_CAML_GC_
-#include <caml/mlvalues.h>
-#include <caml/alloc.h>
-#include <caml/memory.h>
-
-typedef void (*scanning_action) (value, value *);
-
-
-CAMLextern char *young_ptr;
-CAMLextern char *young_limit;
-CAMLextern void (*scan_roots_hook) (scanning_action);
-CAMLextern void minor_collection (void);
-
-#define Caml_white (0 << 8)
-#define Caml_black (3 << 8)
-
-#ifdef HAS_OCP_MEMPROF
-
-/* This code is necessary to make the OCamlPro memory profiling branch of
- OCaml compile. */
-
-#define Make_header(wosize, tag, color) \
- caml_make_header(wosize, tag, color)
-
-#else
-
-#define Make_header(wosize, tag, color) \
- (((header_t) (((header_t) (wosize) << 10) \
- + (color) \
- + (tag_t) (tag))) \
- )
-#endif
-
-#define Alloc_small(result, wosize, tag) do{ \
- young_ptr -= Bhsize_wosize (wosize); \
- if (young_ptr < young_limit){ \
- young_ptr += Bhsize_wosize (wosize); \
- Setup_for_gc; \
- minor_collection (); \
- Restore_after_gc; \
- young_ptr -= Bhsize_wosize (wosize); \
- } \
- Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \
- (result) = Val_hp (young_ptr); \
- }while(0)
-
-
-#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 606cce0127..7588c1ce07 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,17 +16,37 @@
#include <stdio.h>
#include <signal.h>
#include <stdint.h>
+#include <math.h>
+
+#define CAML_INTERNALS
#include <caml/memory.h>
#include <caml/signals.h>
#include <caml/version.h>
-#include <math.h>
-#include "coq_gc.h"
+
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
#include "coq_values.h"
#include "coq_float64.h"
+#if OCAML_VERSION < 41000
+extern void caml_minor_collection(void);
+
+#undef Alloc_small
+#define Alloc_small(result, wosize, tag) do{ \
+ caml_young_ptr -= Bhsize_wosize(wosize); \
+ if (caml_young_ptr < caml_young_limit) { \
+ caml_young_ptr += Bhsize_wosize(wosize); \
+ Setup_for_gc; \
+ caml_minor_collection(); \
+ Restore_after_gc; \
+ caml_young_ptr -= Bhsize_wosize(wosize); \
+ } \
+ Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black); \
+ (result) = Val_hp(caml_young_ptr); \
+ }while(0)
+#endif
+
#ifdef ARCH_SIXTYFOUR
#include "coq_uint63_native.h"
#else
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 91d6773b1f..6233675c66 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,9 +10,12 @@
#include <stdio.h>
#include <string.h>
+
+#define CAML_INTERNALS
#include <caml/alloc.h>
#include <caml/address_class.h>
-#include "coq_gc.h"
+#include <caml/roots.h>
+
#include "coq_instruct.h"
#include "coq_fix_code.h"
#include "coq_memory.h"
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 299f53e8ab..53fc13b04b 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -21,12 +21,19 @@ let is_neg_infinity f = f = neg_infinity
(* Printing a binary64 float in 17 decimal places and parsing it again
will yield the same float. We assume [to_string_raw] is not given a
- [nan] as input. *)
+ [nan] or an infinity as input. *)
let to_string_raw f = Printf.sprintf "%.17g" f
(* OCaml gives a sign to nan values which should not be displayed as
- all NaNs are considered equal here *)
-let to_string f = if is_nan f then "nan" else to_string_raw f
+ all NaNs are considered equal here.
+ OCaml prints infinities as "inf" (resp. "-inf")
+ but we want "infinity" (resp. "neg_infinity"). *)
+let to_string f =
+ if is_nan f then "nan"
+ else if is_infinity f then "infinity"
+ else if is_neg_infinity f then "neg_infinity"
+ else to_string_raw f
+
let of_string = float_of_string
(* Compiles a float to OCaml code *)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index f1e994b337..cc9da3a2ce 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -27,7 +27,7 @@ Conv_oracle
Environ
Primred
CClosure
-Retypeops
+Relevanceops
Reduction
Clambda
Nativelambda
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5dd5499a26..301af328e4 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -382,21 +382,21 @@ let inline_delta_resolver env inl mp mbid mtb delta =
let rec make_inline delta = function
| [] -> delta
| (lev,kn)::r ->
- let kn = replace_mp_in_kn (MPbound mbid) mp kn in
- let con = constant_of_delta_kn delta kn in
- try
- let constant = lookup_constant con env in
- let l = make_inline delta r in
- match constant.const_body with
- | Undef _ | OpaqueDef _ | Primitive _ -> l
- | Def body ->
- let constr = Mod_subst.force_constr body in
- let ctx = Declareops.constant_polymorphic_context constant in
- let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
- add_inline_delta_resolver kn (lev, Some constr) l
- with Not_found ->
- error_no_such_label_sub (Constant.label con)
- (ModPath.to_string (Constant.modpath con))
+ let kn = replace_mp_in_kn (MPbound mbid) mp kn in
+ let con = constant_of_delta_kn delta kn in
+ if not (Environ.mem_constant con env) then
+ error_no_such_label_sub (Constant.label con)
+ (ModPath.to_string (Constant.modpath con))
+ else
+ let constant = lookup_constant con env in
+ let l = make_inline delta r in
+ match constant.const_body with
+ | Undef _ | OpaqueDef _ | Primitive _ -> l
+ | Def body ->
+ let constr = Mod_subst.force_constr body in
+ let ctx = Declareops.constant_polymorphic_context constant in
+ let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
+ add_inline_delta_resolver kn (lev, Some constr) l
in
make_inline delta constants
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5fbe501169..7574d7b21e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -331,7 +331,7 @@ let skip_pattern infos n c1 c2 =
let is_irrelevant infos lft c =
let env = info_env infos.cnv_inf in
- try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
+ try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -354,7 +354,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(match kind a1, kind a2 with
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
- anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
+ (* May happen because we convert application right to left *)
+ raise NotConvertible;
sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
@@ -471,7 +472,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
- anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
+ (* May happen because we convert application right to left *)
+ raise NotConvertible;
(* Luo's system *)
let el1 = el_stack lft1 v1 in
let el2 = el_stack lft2 v2 in
diff --git a/kernel/retypeops.ml b/kernel/relevanceops.ml
index 3f3e722245..3f3e722245 100644
--- a/kernel/retypeops.ml
+++ b/kernel/relevanceops.ml
diff --git a/kernel/retypeops.mli b/kernel/relevanceops.mli
index 86734e747e..86734e747e 100644
--- a/kernel/retypeops.mli
+++ b/kernel/relevanceops.mli
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0c89d51033..c8c2301171 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -143,7 +143,7 @@ let infer_declaration env (dcl : constant_entry) =
Cooking.cook_body = def;
cook_type = typ;
cook_universes = univs;
- cook_relevance = Retypeops.relevance_of_term env j.uj_val;
+ cook_relevance = Relevanceops.relevance_of_term env j.uj_val;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4c66f1574f..a4465c293b 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -169,9 +169,6 @@ let subst_of_rel_context_instance sign l =
| _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
in aux [] (List.rev sign) l
-let adjust_subst_to_rel_context sign l =
- List.rev (subst_of_rel_context_instance sign l)
-
let adjust_rel_to_rel_context sign n =
let rec aux sign =
let open RelDecl in
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 52a6159f0a..0aac5ed4ce 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -72,9 +72,6 @@ type substl = constr list
[c₁], as if usable for [substl]. *)
val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl
-(** For compatibility: returns the substitution reversed *)
-val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list
-
(** Take an index in an instance of a context and returns its index wrt to
the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:59:53 +0000