Merge pull request #389 from ppedrot/vm-split-bytecode

serlib/ser_declarations.ml

@@ -37,6 +37,7 @@ module Vmemitcodes = Ser_vmemitcodes
 module Retroknowledge = Ser_retroknowledge
 module Uint63  = Ser_uint63
 module Float64 = Ser_float64
+module Vmlibrary = Ser_vmlibrary
 
 type template_arity =
   [%import: Declarations.template_arity]
@@ -111,8 +112,8 @@ type typing_flags =
  *   [%import: Declarations.cooking_info]
  *   [@@deriving sexp] *)
 
-type 'a pconstant_body =
-  [%import: 'a Declarations.pconstant_body]
+type ('a, 'b) pconstant_body =
+  [%import: ('a, 'b) Declarations.pconstant_body]
   [@@deriving sexp,yojson,hash,compare]
 
 type constant_body =

serlib/ser_declarations.mli

@@ -75,7 +75,7 @@ type inline = Declarations.inline
  * val sexp_of_cooking_info : cooking_info -> Sexp.t
  * val cooking_info_of_sexp : Sexp.t -> cooking_info *)
 
-type 'a pconstant_body = 'a Declarations.pconstant_body
+type ('a, 'b) pconstant_body = ('a, 'b) Declarations.pconstant_body
   [@@deriving sexp,yojson,hash,compare]
 
 type constant_body = Declarations.constant_body

serlib/ser_environ.ml

@@ -32,6 +32,7 @@ module Opaqueproof    = Ser_opaqueproof
 module Retroknowledge = Ser_retroknowledge
 module UGraph         = Ser_uGraph
 module Declarations   = Ser_declarations
+module Vmlibrary      = Ser_vmlibrary
 
 (* type stratification =
  *   [%import: Environ.stratification]

serlib/ser_safe_typing.ml

@@ -28,6 +28,7 @@ module Declarations = Ser_declarations
 module Entries = Ser_entries
 module Cooking = Ser_cooking
 module Univ = Ser_univ
+module Vmemitcodes = Ser_vmemitcodes
 
 (* Side_effects *)
 type certificate = {
@@ -38,7 +39,7 @@ type certificate = {
 type side_effect = {
   seff_certif : certificate CEphemeron.key;
   seff_constant : Names.Constant.t;
-  seff_body : Constr.t Declarations.pconstant_body;
+  seff_body : (Constr.t, Vmemitcodes.body_code option) Declarations.pconstant_body;
   seff_univs : Univ.ContextSet.t;
 } [@@deriving sexp,yojson,hash,compare]
 

serlib/ser_vmemitcodes.ml

@@ -38,11 +38,23 @@ let hash_fold_array = hash_fold_array_frozen
 type positions = string
  [@@deriving sexp,yojson,hash,compare]
 
-type patches = {
+type _patches = {
   reloc_infos : reloc_info array;
   reloc_positions : positions;
 } [@@deriving sexp,yojson,hash,compare]
 
+module PiercePatches = struct
+
+  type t = [%import: Vmemitcodes.patches]
+  type _t = _patches
+   [@@deriving sexp,yojson,hash,compare]
+
+end
+
+module C = SerType.Pierce(PiercePatches)
+type patches = C.t
+ [@@deriving sexp,yojson,hash,compare]
+
 type emitcodes = string
  [@@deriving sexp,yojson,hash,compare]
 
@@ -51,7 +63,7 @@ type _to_patch = emitcodes * patches
 
 module PierceToPatch = struct
 
-  type t = Vmemitcodes.to_patch
+  type t = [%import: Vmemitcodes.to_patch]
   type _t = _to_patch
    [@@deriving sexp,yojson,hash,compare]
 
@@ -61,6 +73,10 @@ module B = SerType.Pierce(PierceToPatch)
 type to_patch = B.t
  [@@deriving sexp,yojson,hash,compare]
 
+type 'a pbody_code =
+  [%import: 'a Vmemitcodes.pbody_code]
+  [@@deriving sexp,yojson,hash,compare]
+
 type body_code =
   [%import: Vmemitcodes.body_code]
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_vmemitcodes.mli

@@ -16,9 +16,18 @@
 (* Written by: Emilio J. Gallego Arias and others                       *)
 (************************************************************************)
 
+type patches = Vmemitcodes.patches
+ [@@deriving sexp,yojson,hash,compare]
+
+type to_patch = Vmemitcodes.to_patch
+ [@@deriving sexp,yojson,hash,compare]
+
 type body_code = Vmemitcodes.body_code
  [@@deriving sexp,yojson,hash,compare]
 
+type 'a pbody_code = 'a Vmemitcodes.pbody_code
+ [@@deriving sexp,yojson,hash,compare]
+
 (* type to_patch_substituted = Vmemitcodes.to_patch_substituted
  *
  * val sexp_of_to_patch_substituted : to_patch_substituted -> Sexp.t

serlib/ser_vmlibrary.ml

@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq serialization API/Plugin                                         *)
+(* Copyright 2016-2018 MINES ParisTech                                  *)
+(************************************************************************)
+(* Status: Experimental                                                 *)
+(************************************************************************)
+
+open Sexplib.Std
+open Ppx_compare_lib.Builtin
+open Ppx_hash_lib.Std.Hash.Builtin
+
+module Stdlib = Ser_stdlib
+module Names  = Ser_names
+module Vmemitcodes = Ser_vmemitcodes
+
+module Map = Ser_cMap.Make(Int.Map)(Ser_int)
+
+module Delayed =
+struct
+
+type delayed = {
+  del_file : string;
+  del_off : int64;
+  del_digest : string;
+} [@@deriving sexp,yojson,hash,compare]
+
+type 'a node = ToFetch of delayed | Fetched of 'a [@@deriving sexp,yojson,hash,compare]
+
+type 'a t = 'a node Stdlib.ref [@@deriving sexp,yojson,hash,compare]
+
+end
+
+module VmTable =
+struct
+
+type t = {
+  table_len : int;
+  table_dir : Names.DirPath.t;
+  table_val : Vmemitcodes.to_patch Map.t;
+} [@@deriving sexp,yojson,hash,compare]
+
+type index = Names.DirPath.t * int [@@deriving sexp,yojson,hash,compare]
+
+end
+
+module OP = struct
+type t = [%import: Vmlibrary.t]
+type _t = {
+  local : VmTable.t;
+  foreign : VmTable.t Delayed.t Names.DPmap.t;
+}
+[@@deriving sexp,yojson,hash,compare]
+end
+
+module B = SerType.Pierce(OP)
+type t = B.t
+ [@@deriving sexp,yojson,hash,compare]
+
+module OQ = struct
+type t = [%import: Vmlibrary.index]
+type _t = VmTable.index [@@deriving sexp,yojson,hash,compare]
+end
+
+module C = SerType.Pierce(OQ)
+type index = C.t
+ [@@deriving sexp,yojson,hash,compare]
+
+type indirect_code = index Vmemitcodes.pbody_code [@@deriving sexp,yojson,hash,compare]

serlib/ser_vmlibrary.mli

@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq serialization API/Plugin                                         *)
+(* Copyright 2016-2018 MINES ParisTech                                  *)
+(************************************************************************)
+(* Status: Experimental                                                 *)
+(************************************************************************)
+
+type t = Vmlibrary.t
+  [@@deriving sexp,yojson,hash,compare]
+
+type index = Vmlibrary.index
+  [@@deriving sexp,yojson,hash,compare]
+
+type indirect_code = index Vmemitcodes.pbody_code
+  [@@deriving sexp,yojson,hash,compare]