[serlib] Fix some 8.18 piercings

CHANGES.md

@@ -1,3 +1,7 @@
+## Version 0.18.1:
+
+ - [serlib] Fix a few 8.18 piercings (!) (@ejgallego, #)
+
 ## Version 0.18.0:
 
  - [serapi] (!) support for Coq 8.18, thanks to all the developers

serlib/plugins/ssrmatching/ser_ssrmatching.ml

@@ -34,17 +34,9 @@ type ('a, 'b) ssrpattern =
   [%import: ('a, 'b) Ssrmatching_plugin.Ssrmatching.ssrpattern]
   [@@deriving sexp,yojson,hash,compare]
 
-module PierceRPattern = struct
-
-  type t = Ssrmatching_plugin.Ssrmatching.rpattern
-
-  type _t = (cpattern, cpattern) ssrpattern
+type rpattern =
+  [%import: Ssrmatching_plugin.Ssrmatching.rpattern]
   [@@deriving sexp,yojson,hash,compare]
-end
-
-module B_ = SerType.Pierce(PierceRPattern)
-type rpattern = B_.t
- [@@deriving sexp,yojson,hash,compare]
 
 type ssrdir =
   [%import: Ssrmatching_plugin.Ssrmatching.ssrdir]

serlib/ser_declarations.mli

@@ -33,24 +33,19 @@ val sexp_of_declaration_arity :
   ('a, 'b) declaration_arity -> Sexp.t
 
 type recarg = Declarations.recarg
-val recarg_of_sexp : Sexp.t -> recarg
-val sexp_of_recarg : recarg -> Sexp.t
+  [@@deriving sexp,yojson,hash,compare]
 
 type wf_paths = recarg Rtree.t
-val wf_paths_of_sexp : Sexp.t -> wf_paths
-val sexp_of_wf_paths : wf_paths -> Sexp.t
+  [@@deriving sexp,yojson,hash,compare]
 
 type regular_inductive_arity = Declarations.regular_inductive_arity
-val regular_inductive_arity_of_sexp : Sexp.t -> regular_inductive_arity
-val sexp_of_regular_inductive_arity : regular_inductive_arity -> Sexp.t
+  [@@deriving sexp,yojson,hash,compare]
 
 type inductive_arity = Declarations.inductive_arity
-val inductive_arity_of_sexp : Sexp.t -> inductive_arity
-val sexp_of_inductive_arity : inductive_arity -> Sexp.t
+  [@@deriving sexp,yojson,hash,compare]
 
 type one_inductive_body = Declarations.one_inductive_body
-val one_inductive_body_of_sexp : Sexp.t -> one_inductive_body
-val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t
+  [@@deriving sexp,yojson,hash,compare]
 
 (* type set_predicativity = Declarations.set_predicativity
  * val set_predicativity_of_sexp : Sexp.t -> set_predicativity
@@ -61,12 +56,10 @@ val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t
  * val sexp_of_engagement : engagement -> Sexp.t *)
 
 type typing_flags = Declarations.typing_flags
-val typing_flags_of_sexp : Sexp.t -> typing_flags
-val sexp_of_typing_flags : typing_flags -> Sexp.t
+  [@@deriving sexp,yojson,hash,compare]
 
 type inline = Declarations.inline
-val sexp_of_inline : inline -> Sexp.t
-val inline_of_sexp : Sexp.t -> inline
+  [@@deriving sexp,yojson,hash,compare]
 
 (* type work_list = Declarations.work_list *)
 
@@ -80,6 +73,9 @@ val inline_of_sexp : Sexp.t -> 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
+  [@@deriving sexp,yojson,hash,compare]
+
 type constant_body = Declarations.constant_body
   [@@deriving sexp,yojson,hash,compare]
 
@@ -88,17 +84,13 @@ type constant_body = Declarations.constant_body
  * val sexp_of_record_body : record_body -> Sexp.t *)
 
 type recursivity_kind = Declarations.recursivity_kind
-val recursivity_kind_of_sexp : Sexp.t -> recursivity_kind
-val sexp_of_recursivity_kind : recursivity_kind -> Sexp.t
-val recursivity_kind_of_yojson : Yojson.Safe.t -> (recursivity_kind, string) Result.result
-val recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.t
+  [@@deriving sexp,yojson,hash,compare]
 
 type mutual_inductive_body = Declarations.mutual_inductive_body
   [@@deriving sexp,yojson,hash,compare]
 
 type 'a module_alg_expr = 'a Declarations.module_alg_expr
-val sexp_of_module_alg_expr : ('a -> Sexp.t) -> 'a module_alg_expr -> Sexp.t
-val module_alg_expr_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a module_alg_expr
+  [@@deriving sexp,yojson,hash,compare]
 
 type structure_body = Declarations.structure_body
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_safe_typing.ml

@@ -36,9 +36,10 @@ type certificate = {
 } [@@deriving sexp,yojson,hash,compare]
 
 type side_effect = {
-  from_env : certificate CEphemeron.key;
+  seff_certif : certificate CEphemeron.key;
   seff_constant : Names.Constant.t;
-  seff_body : Declarations.constant_body;
+  seff_body : Constr.t Declarations.pconstant_body;
+  seff_univs : Univ.ContextSet.t;
 } [@@deriving sexp,yojson,hash,compare]
 
 module SeffOrd = struct

serlib/ser_sorts.ml

@@ -19,19 +19,6 @@ type family =
   [%import: Sorts.family]
   [@@deriving sexp,yojson,hash,compare]
 
-module PierceSpec = struct
-  type t = Sorts.t
-  type _t =
-    | SProp
-    | Prop
-    | Set
-    | Type of Univ.Universe.t
-  [@@deriving sexp,yojson,hash,compare]
-end
-
-include SerType.Pierce(PierceSpec)
-
-
 module BijectQVar = struct
   open Sexplib.Std
   open Ppx_hash_lib.Std.Hash.Builtin
@@ -44,6 +31,19 @@ end
 
 module QVar = SerType.Biject(BijectQVar)
 
+module PierceSpec = struct
+  type t = Sorts.t
+  type _t =
+    | SProp
+    | Prop
+    | Set
+    | Type of Univ.Universe.t
+    | QSort of QVar.t * Univ.Universe.t
+  [@@deriving sexp,yojson,hash,compare]
+end
+
+include SerType.Pierce(PierceSpec)
+
 type relevance =
   [%import: Sorts.relevance]
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_vmbytecodes.ml

@@ -24,6 +24,10 @@ module Evar = Ser_evar
 
 let hash_fold_array = hash_fold_array_frozen
 
+type caml_prim =
+  [%import: Vmbytecodes.caml_prim]
+  [@@deriving sexp,yojson,hash,compare]
+
 type fv_elem =
   [%import: Vmbytecodes.fv_elem]
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_vmemitcodes.ml

@@ -30,13 +30,17 @@ type reloc_info =
   | Reloc_annot of Vmvalues.annot_switch
   | Reloc_const of Vmvalues.structured_constant
   | Reloc_getglobal of Names.Constant.t
-  | Reloc_caml_prim of CPrimitives.t
+  | Reloc_caml_prim of Vmbytecodes.caml_prim
  [@@deriving sexp,yojson,hash,compare]
 
 let hash_fold_array = hash_fold_array_frozen
 
+type positions = string
+ [@@deriving sexp,yojson,hash,compare]
+
 type patches = {
-  reloc_infos : (reloc_info * int array) array;
+  reloc_infos : reloc_info array;
+  reloc_positions : positions;
 } [@@deriving sexp,yojson,hash,compare]
 
 type emitcodes = string