[serlib] Add ppx_python serialization.

We add Python serialization for the complete protocol, modulo the existing issues the current setup seems to work well! Main hiccup was the lack of variants support janestreet/ppx_python#4 , but fortunately it is easy to work around. Thanks to the `ppx_python` team for their quick resolution of issue janestreet/ppx_python#1 which was essential to get this commit working.
rocq-archive · Aug 9, 2022 · a3a62e2 · a3a62e2
1 parent c2f9aa9
commit a3a62e2
Show file tree

Hide file tree

Showing 145 changed files with 1,292 additions and 869 deletions.
diff --git a/coq-serapi.opam b/coq-serapi.opam
@@ -36,6 +36,7 @@ depends: [
   "ppx_hash"            {           >= "v0.13.0" & < "v0.16" }
   "yojson"              {           >= "1.7.0"               }
   "ppx_deriving_yojson" {           >= "3.4"                 }
+  "ppx_python"          {           >= "v0.15.0"             }
 ]
 
 build: [ "dune" "build" "-p" name "-j" jobs ]
diff --git a/serlib/dune b/serlib/dune
@@ -2,6 +2,6 @@
  (name serlib)
  (public_name coq-serapi.serlib)
  (synopsis "Serialization Library for Coq")
- (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson ppx_python))
  (libraries coq-core.stm sexplib))
 
diff --git a/serlib/plugins/ltac/dune b/serlib/plugins/ltac/dune
@@ -2,5 +2,5 @@
  (name serlib_ltac)
  (public_name coq-serapi.serlib.ltac)
  (synopsis "Serialization Library for Coq [LTAC plugin]")
- (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare ppx_python))
  (libraries coq-core.plugins.ltac serlib sexplib))
diff --git a/serlib/plugins/ltac/ser_profile_ltac.ml b/serlib/plugins/ltac/ser_profile_ltac.ml
@@ -14,9 +14,25 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 
-(* XXX: Move to ser_cmap *)
-type 'a cstring_map = 'a CString.Map.t
+module String = struct
+  type t = string
+  let t_of_sexp = string_of_sexp
+  let sexp_of_t = sexp_of_string
+  let of_yojson s = Ok (Yojson.Safe.Util.to_string s)
+  let to_yojson s = `String s
+  let t_of_python = Py.String.to_string
+  let python_of_t = Py.String.of_string
+  let hash = Ppx_hash_lib.Std.Hash.Builtin.hash_string
+  let hash_fold_t = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_string
+  let compare = String.compare
+end
+
+module SM = Serlib.Ser_cMap.Make(CString.Map)(String)
+
+type 'a cstring_map = 'a SM.t
+  [@@deriving sexp,python]
 
 let from_bindings bl =
   let open CString.Map in
@@ -37,4 +53,4 @@ type treenode =
   [@with CString.Map.t   := cstring_map;
          CString.Map.key := string
   ]]
-  [@@deriving sexp]
+  [@@deriving sexp,python]
diff --git a/serlib/plugins/ltac/ser_profile_ltac.mli b/serlib/plugins/ltac/ser_profile_ltac.mli
@@ -21,3 +21,6 @@ type treenode = Profile_ltac.treenode
 
 val treenode_of_sexp : Sexp.t -> treenode
 val sexp_of_treenode : treenode -> Sexp.t
+
+val treenode_of_python : Py.Object.t -> treenode
+val python_of_treenode : treenode -> Py.Object.t
diff --git a/serlib/plugins/ltac/ser_tacenv.ml b/serlib/plugins/ltac/ser_tacenv.ml
@@ -32,3 +32,8 @@ type ltac_entry =
   [%import: Ltac_plugin.Tacenv.ltac_entry]
   [@@deriving sexp]
 
+let ltac_entry_of_python =
+  Serlib_base.opaque_of_python ~typ:"ltac_entry"
+
+let python_of_ltac_entry =
+  Serlib_base.python_of_opaque ~typ:"ltac_entry"
diff --git a/serlib/plugins/ltac/ser_tacenv.mli b/serlib/plugins/ltac/ser_tacenv.mli
@@ -23,3 +23,6 @@ type ltac_entry = Tacenv.ltac_entry
 
 val ltac_entry_of_sexp : Sexp.t -> ltac_entry
 val sexp_of_ltac_entry : ltac_entry -> Sexp.t
+
+val ltac_entry_of_python : Py.Object.t -> ltac_entry
+val python_of_ltac_entry : ltac_entry -> Py.Object.t
diff --git a/serlib/plugins/ltac/ser_tacexpr.ml b/serlib/plugins/ltac/ser_tacexpr.ml
@@ -678,6 +678,12 @@ and raw_atomic_tactic_expr_of_sexp tac =
     raw_tactic_expr_of_sexp
     Genarg.rlevel_of_sexp
 
+let python_of_raw_tactic_expr =
+  Serlib_base.python_of_opaque ~typ:"raw_tactic_expr"
+
+let raw_tactic_expr_of_python =
+  Serlib_base.opaque_of_python ~typ:"raw_tactic_expr"
+
 let rec sexp_of_raw_tactic_expr (tac : raw_tactic_expr) =
   sexp_of_gen_tactic_expr
     Constrexpr.sexp_of_constr_expr

diff --git a/serlib/plugins/ltac/ser_tacexpr.mli b/serlib/plugins/ltac/ser_tacexpr.mli
@@ -259,7 +259,7 @@ type glob_atomic_tactic_expr = Tacexpr.glob_atomic_tactic_expr
   [@@deriving sexp,yojson,hash,compare]
 
 type raw_tactic_expr = Tacexpr.raw_tactic_expr
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,hash,compare,python]
 
 type raw_atomic_tactic_expr = Tacexpr.raw_atomic_tactic_expr
   [@@deriving sexp,yojson,hash,compare]

diff --git a/serlib/plugins/ssrmatching/dune b/serlib/plugins/ssrmatching/dune
@@ -2,5 +2,5 @@
  (name serlib_ssrmatching)
  (public_name coq-serapi.serlib.ssrmatching)
  (synopsis "Serialization Library for Coq [SSR Matching plugin]")
- (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python ppx_deriving_yojson ppx_hash ppx_compare))
  (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib))
diff --git a/serlib/plugins/ssrmatching/ser_ssrmatching.ml b/serlib/plugins/ssrmatching/ser_ssrmatching.ml
@@ -14,6 +14,7 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
 
@@ -24,22 +25,22 @@ module Geninterp = Ser_geninterp
 
 type ssrtermkind =
   [%import: Ssrmatching_plugin.Ssrmatching.ssrtermkind]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type cpattern =
   [%import: Ssrmatching_plugin.Ssrmatching.cpattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type ('a, 'b) ssrpattern =
   [%import: ('a, 'b) Ssrmatching_plugin.Ssrmatching.ssrpattern]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 module PierceRPattern = struct
 
   type t = Ssrmatching_plugin.Ssrmatching.rpattern
 
   type _t = (cpattern, cpattern) ssrpattern
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module B_ = SerType.Pierce(PierceRPattern)

diff --git a/serlib/serType.ml b/serlib/serType.ml
@@ -16,15 +16,23 @@ module type SJ = sig
   val to_yojson : t -> Yojson.Safe.t
 end
 
-module type SJH = sig
+module type SJP = sig
 
   include SJ
+  val t_of_python : Py.Object.t -> t
+  val python_of_t : t -> Py.Object.t
+
+end
+
+module type SJPH = sig
+
+  include SJP
   val hash : t -> int
   val hash_fold_t : Ppx_hash_lib.Std.Hash.state -> t -> Ppx_hash_lib.Std.Hash.state
 end
 
-module type SJHC = sig
-  include SJH
+module type SJPHC = sig
+  include SJPH
   val compare : t -> t -> int
 end
 
@@ -46,19 +54,27 @@ module type SJ1 = sig
 
 end
 
-module type SJH1 = sig
+module type SJP1 = sig
 
   include SJ1
 
+  val t_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a t
+  val python_of_t : ('a -> Py.Object.t) -> 'a t -> Py.Object.t
+end
+
+module type SJPH1 = sig
+
+  include SJP1
+
   open Ppx_hash_lib.Std.Hash
 
   val hash_fold_t : 'a folder -> 'a t folder
 
 end
 
-module type SJHC1 = sig
+module type SJPHC1 = sig
 
-  include SJH1
+  include SJPH1
 
   open Ppx_compare_lib
 
@@ -73,21 +89,24 @@ module type Bijectable = sig
   type t
 
   (* Representation type *)
-  type _t [@@deriving sexp,yojson,hash,compare]
+  type _t [@@deriving sexp,yojson,python,hash,compare]
 
   (* Need to be bijetive *)
   val to_t : _t -> t
   val of_t : t -> _t
 
 end
 
-module Biject(M : Bijectable) : SJHC with type t = M.t = struct
+module Biject(M : Bijectable) : SJPHC with type t = M.t = struct
 
   type t = M.t
 
   let sexp_of_t x = M.sexp_of__t (M.of_t x)
   let t_of_sexp s = M.to_t (M._t_of_sexp s)
 
+  let python_of_t x = M.python_of__t (M.of_t x)
+  let t_of_python x = M.to_t (M._t_of_python x)
+
   let to_yojson p = M._t_to_yojson (M.of_t p)
   let of_yojson p = M._t_of_yojson p |> Result.map M.to_t
 
@@ -104,21 +123,24 @@ module type Bijectable1 = sig
   type 'a t
 
   (* Representation type *)
-  type 'a _t [@@deriving sexp,yojson,hash,compare]
+  type 'a _t [@@deriving sexp,yojson,python,hash,compare]
 
   (* Need to be bijetive *)
   val to_t : 'a _t -> 'a t
   val of_t : 'a t -> 'a _t
 
 end
 
-module Biject1(M : Bijectable1) : SJHC1 with type 'a t = 'a M.t = struct
+module Biject1(M : Bijectable1) : SJPHC1 with type 'a t = 'a M.t = struct
 
   type 'a t = 'a M.t
 
   let sexp_of_t f x = M.sexp_of__t f (M.of_t x)
   let t_of_sexp f s = M.to_t (M._t_of_sexp f s)
 
+  let python_of_t f x = M.python_of__t f (M.of_t x)
+  let t_of_python f x = M.to_t (M._t_of_python f x)
+
   let to_yojson f p = M._t_to_yojson f (M.of_t p)
   let of_yojson f p = M._t_of_yojson f p |> Result.map M.to_t
 
@@ -137,7 +159,7 @@ module type Pierceable = sig
   type t
 
   (* Representation type *)
-  type _t [@@deriving sexp,yojson,hash,compare]
+  type _t [@@deriving sexp,yojson,python,hash,compare]
 end
 
 module type Pierceable1 = sig
@@ -146,16 +168,19 @@ module type Pierceable1 = sig
   type 'a t
 
   (* Representation type *)
-  type 'a _t [@@deriving sexp,yojson,hash,compare]
+  type 'a _t [@@deriving sexp,yojson,python,hash,compare]
 end
 
-module Pierce(M : Pierceable) : SJHC with type t = M.t = struct
+module Pierce(M : Pierceable) : SJPHC with type t = M.t = struct
 
   type t = M.t
 
   let sexp_of_t x = M.sexp_of__t (_sercast x)
   let t_of_sexp s = _sercast (M._t_of_sexp s)
 
+  let python_of_t x = M.python_of__t (_sercast x)
+  let t_of_python s = _sercast (M._t_of_python s)
+
   let to_yojson p = M._t_to_yojson (_sercast p)
   let of_yojson p = M._t_of_yojson p |> Result.map _sercast
 
@@ -166,13 +191,16 @@ module Pierce(M : Pierceable) : SJHC with type t = M.t = struct
 
 end
 
-module Pierce1(M : Pierceable1) : SJHC1 with type 'a t = 'a M.t = struct
+module Pierce1(M : Pierceable1) : SJPHC1 with type 'a t = 'a M.t = struct
 
   type 'a t = 'a M.t
 
   let sexp_of_t f x = M.sexp_of__t f (_sercast x)
   let t_of_sexp f s = _sercast (M._t_of_sexp f s)
 
+  let python_of_t f x = M.python_of__t f (_sercast x)
+  let t_of_python f s = _sercast (M._t_of_python f s)
+
   let to_yojson f p = M._t_to_yojson f (_sercast p)
   let of_yojson f p = M._t_of_yojson f p |> Result.map _sercast
 
@@ -186,11 +214,14 @@ end
 (* Unfortunately this doesn't really work for types that are named as
    the functions would have to be sexp_of_name etc... Maybe fixme in
    the future *)
-module PierceAlt(M : Pierceable) : SJHC with type t := M.t = struct
+module PierceAlt(M : Pierceable) : SJPHC with type t := M.t = struct
 
   let sexp_of_t x = M.sexp_of__t (_sercast x)
   let t_of_sexp s = _sercast (M._t_of_sexp s)
 
+  let python_of_t x = M.python_of__t (_sercast x)
+  let t_of_python s = _sercast (M._t_of_python s)
+
   let to_yojson p = M._t_to_yojson (_sercast p)
   let of_yojson p = M._t_of_yojson p |> Result.map _sercast
 
@@ -203,14 +234,17 @@ end
 
 module type OpaqueDesc = sig type t val name : string end
 
-module Opaque(M : OpaqueDesc) : SJHC with type t = M.t = struct
+module Opaque(M : OpaqueDesc) : SJPHC with type t = M.t = struct
 
   type t = M.t
   let typ = M.name
 
   let sexp_of_t x = Serlib_base.sexp_of_opaque ~typ x
   let t_of_sexp s = Serlib_base.opaque_of_sexp ~typ s
 
+  let python_of_t x = Serlib_base.python_of_opaque ~typ x
+  let t_of_python s = Serlib_base.opaque_of_python ~typ s
+
   let to_yojson p = Serlib_base.opaque_to_yojson ~typ p
   let of_yojson p = Serlib_base.opaque_of_yojson ~typ p
 
@@ -223,14 +257,17 @@ end
 
 module type OpaqueDesc1 = sig type 'a t val name : string end
 
-module Opaque1(M : OpaqueDesc1) : SJHC1 with type 'a t = 'a M.t = struct
+module Opaque1(M : OpaqueDesc1) : SJPHC1 with type 'a t = 'a M.t = struct
 
   type 'a  t = 'a M.t
   let typ = M.name
 
   let sexp_of_t _ x = Serlib_base.sexp_of_opaque ~typ x
   let t_of_sexp _ s = Serlib_base.opaque_of_sexp ~typ s
 
+  let python_of_t _ x = Serlib_base.python_of_opaque ~typ x
+  let t_of_python _ s = Serlib_base.opaque_of_python ~typ s
+
   let to_yojson _ p = Serlib_base.opaque_to_yojson ~typ p
   let of_yojson _ p = Serlib_base.opaque_of_yojson ~typ p
 

diff --git a/serlib/ser_attributes.ml b/serlib/ser_attributes.ml
@@ -15,20 +15,21 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
+open Sexplib.Std
+open Ppx_python_runtime
 open Ppx_hash_lib.Std.Hash.Builtin
 open Ppx_compare_lib.Builtin
-open Sexplib.Std
 
 module CAst = Ser_cAst
 
 type vernac_flag_type =
   [%import: Attributes.vernac_flag_type]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]
 
 type vernac_flag =
   [%import: Attributes.vernac_flag]
 and vernac_flag_value =
   [%import: Attributes.vernac_flag_value]
 and vernac_flags =
   [%import: Attributes.vernac_flags]
-  [@@deriving sexp,yojson,hash,compare]
+  [@@deriving sexp,yojson,python,hash,compare]