diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_gc.h | 59 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 24 | ||||
| -rw-r--r-- | kernel/byterun/coq_memory.c | 5 | ||||
| -rw-r--r-- | kernel/modops.ml | 30 |
4 files changed, 41 insertions, 77 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/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 |