From 3c6117eeba8dac2191418866e452680703167c6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 17 Dec 2024 14:43:49 +0100 Subject: [PATCH] Adapt w.r.t. coq/coq#19943. --- serlib/serType.ml | 32 ++++++++++++++++++++++++++ serlib/serType.mli | 22 ++++++++++++++++++ serlib/ser_declarations.ml | 43 +++++++++++++++++++++++++++++++---- serlib/ser_declarations.mli | 6 +++++ serlib/ser_retroknowledge.ml | 11 +++++---- serlib/ser_retroknowledge.mli | 4 +--- 6 files changed, 106 insertions(+), 12 deletions(-) diff --git a/serlib/serType.ml b/serlib/serType.ml index fb23ba572..89a2fad4f 100644 --- a/serlib/serType.ml +++ b/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 diff --git a/serlib/serType.mli b/serlib/serType.mli index 5adb49804..035db2508 100644 --- a/serlib/serType.mli +++ b/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 *) diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml index 0874cc99c..185cce0e3 100644 --- a/serlib/ser_declarations.ml +++ b/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] diff --git a/serlib/ser_declarations.mli b/serlib/ser_declarations.mli index 815cb1a8b..255f5da18 100644 --- a/serlib/ser_declarations.mli +++ b/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] diff --git a/serlib/ser_retroknowledge.ml b/serlib/ser_retroknowledge.ml index 2716efd6f..bee5c3841 100644 --- a/serlib/ser_retroknowledge.ml +++ b/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] diff --git a/serlib/ser_retroknowledge.mli b/serlib/ser_retroknowledge.mli index 6510dc424..fb74e43e2 100644 --- a/serlib/ser_retroknowledge.mli +++ b/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]