Adapt w.r.t. rocq-prover/rocq#19943.

Author: ppedrot

serlib/serType.ml

@@ -24,6 +24,10 @@ module type SJHC1 = sig
   type 'a t [@@deriving sexp,yojson,hash,compare]
 end
 
+module type SJHC2 = sig
+  type ('a, 'b) t [@@deriving sexp,yojson,hash,compare]
+end
+
 (* Bijection with serializable types *)
 module type Bijectable = sig
 
@@ -85,6 +89,34 @@ module Biject1(M : Bijectable1) : SJHC1 with type 'a t = 'a M.t = struct
   let compare f x1 x2 = M.compare__t f (M.of_t x1) (M.of_t x2)
 end
 
+module type Bijectable2 = sig
+
+  (* Base Type *)
+  type ('a, 'b) t
+
+  (* Representation type *)
+  type ('a, 'b) _t [@@deriving sexp,yojson,hash,compare]
+
+  (* Need to be bijetive *)
+  val to_t : ('a, 'b) _t -> ('a, 'b) t
+  val of_t : ('a, 'b) t -> ('a, 'b) _t
+end
+
+module Biject2(M : Bijectable2) : SJHC2 with type ('a, 'b) t = ('a, 'b) M.t = struct
+
+  type ('a, 'b) t = ('a, 'b) M.t
+
+  let sexp_of_t f g x = M.sexp_of__t f g (M.of_t x)
+  let t_of_sexp f g s = M.to_t (M._t_of_sexp f g s)
+
+  let to_yojson f g p = M._t_to_yojson f g (M.of_t p)
+  let of_yojson f g p = M._t_of_yojson f g p |> Result.map M.to_t
+
+  let hash_fold_t f g st x = M.hash_fold__t f g st (M.of_t x)
+
+  let compare f g x1 x2 = M.compare__t f g (M.of_t x1) (M.of_t x2)
+end
+
 (* We do our own alias as to have better control *)
 let _sercast = Obj.magic
 

serlib/serType.mli

@@ -28,6 +28,12 @@ module type SJHC1 = sig
 
 end
 
+module type SJHC2 = sig
+
+  type ('a, 'b) t [@@deriving sexp,yojson,hash,compare]
+
+end
+
 (** Bijection with serializable types *)
 module type Bijectable = sig
 
@@ -62,6 +68,22 @@ end
 
 module Biject1(M : Bijectable1) : SJHC1 with type 'a t = 'a M.t
 
+module type Bijectable2 = sig
+
+  (* Base Type *)
+  type ('a, 'b) t
+
+  (* Representation type *)
+  type ('a, 'b) _t [@@deriving sexp,yojson,hash,compare]
+
+  (* Need to be bijetive *)
+  val to_t : ('a, 'b) _t -> ('a, 'b) t
+  val of_t : ('a, 'b) t -> ('a, 'b) _t
+end
+
+module Biject2(M : Bijectable2) : SJHC2 with type ('a, 'b) t = ('a, 'b) M.t
+
+
 module type Pierceable = sig
 
   (** Type to pierce *)

serlib/ser_declarations.ml

@@ -125,14 +125,19 @@ let sexp_of_constant_body e =
   (* We cannot handle VM values *)
   sexp_of_constant_body { e with const_body_code = None }
 
+(*
+module Retroknowledge =
+struct
 module MRK = struct
-  type 'a t = 'a Declarations.module_retroknowledge
-  let name = "Declarations.module_retroknowledge"
+  type t = Retroknowledge.action
+  let name = "Retroknowledge.action"
 end
 
-module B_ = SerType.Opaque1(MRK)
-type 'a module_retroknowledge = 'a B_.t
- [@@deriving sexp,yojson,hash,compare]
+module B_ = SerType.Opaque(MRK)
+type action = B_.t
+  [@@deriving sexp,yojson,hash,compare]
+end
+*)
 
 type recursivity_kind =
   [%import: Declarations.recursivity_kind]
@@ -188,6 +193,34 @@ type 'a with_declaration =
   [%import: 'a Declarations.with_declaration]
   [@@deriving sexp,yojson,hash,compare]
 
+type mod_body =
+  [%import: Declarations.mod_body]
+  [@@deriving sexp,yojson,hash,compare]
+
+type mod_type =
+  [%import: Declarations.mod_type]
+  [@@deriving sexp,yojson,hash,compare]
+
+module WMBBiject = struct
+  type ('a, 'b) t = ('a, 'b) Declarations.when_mod_body
+
+  type ('a, 'b) _t = 'b option
+    [@@deriving sexp,yojson,hash,compare]
+
+  let to_t (type a b) (x : b option) : (a, b) Declarations.when_mod_body = match x with
+  | Some x -> Obj.magic @@ Declarations.ModBodyVal x
+  | None -> Obj.magic @@ Declarations.ModTypeNul
+
+  let of_t (type a) (type b) (x : (a, b) Declarations.when_mod_body) : b option = match x with
+  | Declarations.ModBodyVal x -> Some x
+  | Declarations.ModTypeNul -> None
+end
+
+module WMB = SerType.Biject2(WMBBiject)
+
+ type ('a, 'b) when_mod_body = ('a, 'b) WMB.t
+  [@@deriving sexp,yojson,hash,compare]
+
 type 'a module_alg_expr =
   [%import: 'a Declarations.module_alg_expr]
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_declarations.mli

@@ -94,6 +94,12 @@ type mutual_inductive_body = Declarations.mutual_inductive_body
 type rewrite_rule = Declarations.rewrite_rule
   [@@deriving sexp,yojson,hash,compare]
 
+type mod_body = Declarations.mod_body
+type mod_type = Declarations.mod_type
+
+type ('a, 'v) when_mod_body = ('a, 'v) Declarations.when_mod_body
+  [@@deriving sexp,yojson,hash,compare]
+
 type 'a module_alg_expr = 'a Declarations.module_alg_expr
   [@@deriving sexp,yojson,hash,compare]
 

serlib/ser_retroknowledge.ml

@@ -25,8 +25,11 @@ let retroknowledge_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Retroknowledge.ret
 (* type entry = 
  *   [%import: Retroknowledge.entry] *)
 
-type action = 
-  [%import: Retroknowledge.action]
+module MRK = struct
+  type t = Retroknowledge.action
+  let name = "Retroknowledge.action"
+end
 
-let sexp_of_action = Serlib_base.sexp_of_opaque ~typ:"Retroknowledge.action"
-let action_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Retroknowledge.action"
+module B_ = SerType.Opaque(MRK)
+type action = B_.t
+  [@@deriving sexp,yojson,hash,compare]

serlib/ser_retroknowledge.mli

@@ -24,6 +24,4 @@ val sexp_of_retroknowledge : retroknowledge -> Sexp.t
 val retroknowledge_of_sexp : Sexp.t -> retroknowledge
 
 type action = Retroknowledge.action
-
-val sexp_of_action : action -> Sexp.t
-val action_of_sexp : Sexp.t -> action
+  [@@deriving sexp,yojson,hash,compare]