[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
was 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.

This PR just takes care of the serialization, main Python support is
done now in https://github.com/ejgallego/pycoq

Thus, this PR closes #48

.github/workflows/ci.yml

@@ -68,6 +68,7 @@ jobs:
           opam pin add -y -n --kind=path coq-serapi .
           opam install -y --deps-only -j $NJOBS coq-serapi
           opam pin remove coq-serapi
+          opam pin add -y ppx_python https://github.com/ejgallego/ppx_python.git#fixup
       - run: opam list
       - name: Install Coq via git
         if: ${{ matrix.coq-from-git }}
@@ -87,7 +88,9 @@ jobs:
           make install
           popd
       - name: Install extra opam
-        run: opam install --ignore-constraints-on=coq $EXTRA_OPAM
+        run: |
+          opam install --ignore-constraints-on=coq $EXTRA_OPAM
+          opam pin add -y ppx_python https://github.com/ejgallego/ppx_python.git#fixup
       - name: Build SerAPI
         run: |
           set -e

coq-serapi.opam

@@ -34,6 +34,8 @@ depends: [
   "ppx_sexp_conv"       {           >= "v0.13.0" & < "v0.15" }
   "yojson"              {           >= "1.7.0"               }
   "ppx_deriving_yojson" {           >= "3.4"                 }
+# Disabled due to ppx_python >= 0.15 and ppx_import < 2.0 not getting along
+# "ppx_python"          {           >= "v0.15.0"             }
 ]
 
 build: [ "dune" "build" "-p" name "-j" jobs ]

serapi/serapi_protocol.ml

@@ -332,10 +332,12 @@ module ExnInfo = struct
     }
 end
 
+type focus_info = NewTip | Unfocus of Stateid.t
+
 type answer_kind =
     Ack
   | Completed
-  | Added     of Stateid.t * Loc.t * [`NewTip | `Unfocus of Stateid.t ]
+  | Added     of Stateid.t * Loc.t * focus_info
   | Canceled  of Stateid.t list
   | ObjList   of coq_object list
   | CoqExn    of ExnInfo.t
@@ -695,6 +697,10 @@ module ControlUtil = struct
   type doc    = Stateid.t list
   let cur_doc : doc ref = ref [Stateid.of_int 1]
 
+  let convert_foc = function
+    | `NewTip -> NewTip
+    | `Unfocus sid -> Unfocus sid
+
   let pp_doc fmt l =
     let open Serapi_pp in
     Format.fprintf fmt "@[%a@]" (pp_list ~sep:" " pp_stateid) l
@@ -739,6 +745,7 @@ module ControlUtil = struct
         let n_doc, n_st, foc = Stm.add ~doc:!doc ?newtip:opts.newtip ~ontop:!stt opts.verb east in
         doc := n_doc;
         cur_doc := n_st :: !cur_doc;
+        let foc = convert_foc foc in
         acc := (Added (n_st, eloc, foc)) :: !acc;
         stt := n_st;
         incr i

serapi/serapi_protocol.mli

@@ -500,12 +500,14 @@ module ExnInfo : sig
     }
 end
 
+type focus_info = NewTip | Unfocus of Stateid.t
+
 type answer_kind =
   | Ack
   (** The command was received, Coq is processing it. *)
   | Completed
   (** The command was completed. *)
-  | Added     of Stateid.t * Loc.t * [`NewTip | `Unfocus of Stateid.t ]
+  | Added     of Stateid.t * Loc.t * focus_info
   (** A sentence was added, with corresponding sentence id and location. *)
   | Canceled  of Stateid.t list
   (** A set of sentences are not valid anymore. *)

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_deriving_yojson))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_python))
  (libraries coq.stm sexplib))
 

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))
+ (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python))
  (libraries coq.plugins.ltac serlib sexplib))

serlib/plugins/ltac/ser_profile_ltac.ml

@@ -14,9 +14,21 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Serlib.Ppx_python_runtime_serapi
 
-(* XXX: Move to ser_cmap *)
-type 'a cstring_map = 'a CString.Map.t
+module StringSPJ = struct
+  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
+end
+
+module SM = Serlib.Ser_cMap.MakeJP(CString.Map)(StringSPJ)
+
+type 'a cstring_map = 'a SM.t
+  [@@deriving sexp,python]
 
 let from_bindings bl =
   let open CString.Map in
@@ -37,4 +49,4 @@ type treenode =
   [@with CString.Map.t   := cstring_map;
          CString.Map.key := string
   ]]
-  [@@deriving sexp]
+  [@@deriving sexp,python]

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

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"

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

serlib/plugins/ltac/ser_tacexpr.ml

@@ -528,6 +528,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

serlib/plugins/ltac/ser_tacexpr.mli

@@ -270,6 +270,8 @@ val sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexp.t
 type raw_tactic_expr = Tacexpr.raw_tactic_expr
 val raw_tactic_expr_of_sexp : Sexp.t -> raw_tactic_expr
 val sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexp.t
+val raw_tactic_expr_of_python : Py.Object.t -> raw_tactic_expr
+val python_of_raw_tactic_expr : raw_tactic_expr -> Py.Object.t
 
 type raw_atomic_tactic_expr = Tacexpr.raw_atomic_tactic_expr
 val raw_atomic_tactic_expr_of_sexp : Sexp.t -> raw_atomic_tactic_expr

serlib/ppx_python_runtime_serapi.ml

@@ -0,0 +1,6 @@
+include Ppx_python_runtime
+(* To remove in newer ppx_python release *)
+exception Not_found_s = Base.Not_found_s
+
+let python_of_unit _ = Py.Int.of_int 0
+let unit_of_python _ = ()

serlib/serType.ml

@@ -16,6 +16,13 @@ module type SJ = sig
   val to_yojson : t -> Yojson.Safe.t
 end
 
+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 S1 = sig
 
   type 'a t
@@ -33,3 +40,12 @@ module type SJ1 = sig
   val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
 
 end
+
+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

serlib/ser_attributes.ml

@@ -16,15 +16,16 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime_serapi
 
 type vernac_flag_type =
   [%import: Attributes.vernac_flag_type]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 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]
+  [@@deriving sexp,yojson,python]

serlib/ser_cAst.ml

@@ -14,14 +14,15 @@
 (************************************************************************)
 
 open Sexplib.Std
+open Ppx_python_runtime_serapi
 
 module Loc        = Ser_loc
 
 module L = struct
 type 'a t = {
   v   : 'a;
   loc : Loc.t option;
-} [@@deriving sexp,yojson]
+} [@@deriving sexp,yojson,python]
 end
 
 type 'a t = 'a CAst.t = private {
@@ -35,6 +36,9 @@ let sexp_of_t f { CAst.v ; loc } = L.sexp_of_t f { L.v ; loc }
 let of_yojson f json = Ppx_deriving_yojson_runtime.(L.of_yojson f json >|= fun { L.v; loc } -> CAst.make ?loc:loc v)
 let to_yojson f { CAst.v ; loc } = L.to_yojson f { L.v ; loc }
 
+let t_of_python f s = let { L.v ; loc } = L.t_of_python f s in CAst.make ?loc:loc v
+let python_of_t f { CAst.v ; loc } = L.python_of_t f { L.v ; loc }
+
 let omit_att = ref false
 
 let sexp_of_t f x =

serlib/ser_cAst.mli

@@ -26,4 +26,7 @@ val sexp_of_t : ('a -> Sexp.t) -> 'a t -> Sexp.t
 val of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a t, string) Result.result
 val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
 
+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
+
 val omit_att : bool ref

serlib/ser_cEphemeron.ml

@@ -17,3 +17,6 @@ type 'a key = 'a CEphemeron.key
 
 let key_of_sexp f x = CEphemeron.create (f x)
 let sexp_of_key f v = f CEphemeron.(get v)
+
+let key_of_python f x = CEphemeron.create (f x)
+let python_of_key f v = f CEphemeron.(get v)

serlib/ser_cMap.ml

@@ -42,3 +42,69 @@ module Make (M : CSig.MapS) (S : SerType.S with type t := M.key) = struct
       (list_of_sexp (pair_of_sexp S.t_of_sexp f) sexp)
 
 end
+
+module type ExtSJ = sig
+
+  include CSig.MapS
+
+  include SerType.SJ1 with type 'a t := 'a t
+
+end
+
+module MakeJ (M : CSig.MapS) (S : SerType.SJ with type t := M.key) = struct
+
+  include Make(M)(S)
+
+  let tuple_to_yojson f1 f2 (e1, e2) =
+    `List [f1 e1; f2 e2]
+
+  let tuple_of_yojson f1 f2 json =
+    let tlist = Yojson.Safe.Util.to_list json in
+    match tlist with
+    | [e1; e2] ->
+      let open Ppx_deriving_yojson_runtime in
+      f1 e1 >>= (fun r1 ->
+      f2 e2 >>= (fun r2 ->
+      Ok (r1, r2)))
+    | _ ->
+      Error "tuple_of_yojson: incorrect number of tuple elements"
+
+  let to_yojson f cst : Yojson.Safe.t =
+    `List (List.map (tuple_to_yojson S.to_yojson f) (M.bindings cst))
+
+  let of_yojson f json =
+    let open Ppx_deriving_yojson_runtime in
+    Yojson.Safe.Util.to_list json |>
+    List.fold_left
+      (fun e p ->
+         e                               >>= (fun e ->
+         tuple_of_yojson S.of_yojson f p >|= (fun (k,s) ->
+         M.add k s e))) (Ok M.empty)
+
+end
+
+module type ExtSJP = sig
+
+  include CSig.MapS
+
+  include SerType.SJP1 with type 'a t := 'a t
+
+end
+
+module MakeJP (M : CSig.MapS) (S : SerType.SJP with type t := M.key) = struct
+
+  include MakeJ(M)(S)
+
+  let python_of_t f cst =
+    Py.List.of_list_map
+      (fun (key, binding) ->
+         Py.Tuple.of_pair (S.python_of_t key, f binding))
+      (M.bindings cst)
+
+  let t_of_python f py =
+    List.fold_left (fun e (k,s) -> M.add k s e) M.empty
+      (Py.List.to_list_map (fun p ->
+           let key, binding = Py.Tuple.to_pair p in
+           S.t_of_python key, f binding) py)
+
+end

serlib/ser_cMap.mli

@@ -32,3 +32,28 @@ module Make (M : CSig.MapS) (S : SerType.S with type t := M.key)
      and type 'a t = 'a M.t
      (* and module Set := M.Set *)
 
+module type ExtSJ = sig
+
+  include CSig.MapS
+
+  include SerType.SJ1 with type 'a t := 'a t
+
+end
+
+module MakeJ (M : CSig.MapS) (S : SerType.SJ with type t := M.key)
+  : ExtSJ
+    with type key = M.key
+     and type 'a t = 'a M.t
+
+module type ExtSJP = sig
+
+  include CSig.MapS
+
+  include SerType.SJP1 with type 'a t := 'a t
+
+end
+
+module MakeJP (M : CSig.MapS) (S : SerType.SJP with type t := M.key)
+  : ExtSJP
+    with type key = M.key
+     and type 'a t = 'a M.t

serlib/ser_cPrimitives.ml

@@ -18,11 +18,11 @@ open Sexplib.Std
 
 type t =
   [%import: CPrimitives.t]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 type const =
   [%import: CPrimitives.const]
-  [@@deriving sexp,yojson]
+  [@@deriving sexp,yojson,python]
 
 (* XXX: GADTs ... *)
 type 'a prim_type = [%import: 'a CPrimitives.prim_type]
@@ -58,3 +58,6 @@ let op_or_type_of_sexp (x : Sexp.t) : op_or_type =
 (* XXX *)
 let op_or_type_to_yojson = Obj.magic
 let op_or_type_of_yojson = Obj.magic
+
+let python_of_op_or_type = Obj.magic
+let op_or_type_of_python = Obj.magic