From e6260a918531caff33221de4a5d693a124f43468 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 3 Nov 2020 05:52:00 +0100 Subject: [PATCH] [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 https://github.com/janestreet/ppx_python/issues/4 , but fortunately it was easy to work around. Thanks to the `ppx_python` team for their quick resolution of issue https://github.com/janestreet/ppx_python/issues/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 | 5 +- coq-serapi.opam | 2 + serapi/serapi_protocol.ml | 9 +- serapi/serapi_protocol.mli | 4 +- serlib/dune | 2 +- serlib/plugins/ltac/dune | 2 +- serlib/plugins/ltac/ser_profile_ltac.ml | 18 +- serlib/plugins/ltac/ser_profile_ltac.mli | 3 + serlib/plugins/ltac/ser_tacenv.ml | 5 + serlib/plugins/ltac/ser_tacenv.mli | 3 + serlib/plugins/ltac/ser_tacexpr.ml | 6 + serlib/plugins/ltac/ser_tacexpr.mli | 2 + serlib/ppx_python_runtime_serapi.ml | 6 + serlib/serType.ml | 16 ++ serlib/ser_attributes.ml | 5 +- serlib/ser_cAst.ml | 6 +- serlib/ser_cAst.mli | 3 + serlib/ser_cEphemeron.ml | 3 + serlib/ser_cMap.ml | 66 +++++ serlib/ser_cMap.mli | 25 ++ serlib/ser_cPrimitives.ml | 7 +- serlib/ser_cSet.ml | 20 ++ serlib/ser_cSet.mli | 13 + serlib/ser_cUnix.ml | 3 +- serlib/ser_constr.ml | 59 +++-- serlib/ser_constr.mli | 19 ++ serlib/ser_constrexpr.ml | 58 ++--- serlib/ser_constrexpr.mli | 35 +++ serlib/ser_context.ml | 16 +- serlib/ser_context.mli | 18 ++ serlib/ser_conv_oracle.ml | 10 +- serlib/ser_conv_oracle.mli | 5 + serlib/ser_declarations.ml | 70 +++--- serlib/ser_declarations.mli | 14 ++ serlib/ser_declaremods.ml | 5 +- serlib/ser_declaremods.mli | 4 + serlib/ser_decls.ml | 8 +- serlib/ser_environ.ml | 23 +- serlib/ser_environ.mli | 6 +- serlib/ser_evar.ml | 6 +- serlib/ser_evar.mli | 4 +- serlib/ser_evar_kinds.ml | 13 +- serlib/ser_evar_kinds.mli | 2 +- serlib/ser_extend.ml | 17 +- serlib/ser_extend.mli | 10 + serlib/ser_feedback.ml | 7 +- serlib/ser_feedback.mli | 6 + serlib/ser_float64.ml | 7 +- serlib/ser_future.ml | 3 + serlib/ser_genarg.ml | 25 +- serlib/ser_genarg.mli | 2 + serlib/ser_genredexpr.ml | 13 +- serlib/ser_genredexpr.mli | 2 + serlib/ser_glob_term.ml | 13 +- serlib/ser_glob_term.mli | 10 + serlib/ser_globnames.ml | 4 +- serlib/ser_goal.ml | 2 +- serlib/ser_goal.mli | 2 + serlib/ser_goal_select.ml | 3 +- serlib/ser_goptions.ml | 11 +- serlib/ser_goptions.mli | 6 + serlib/ser_gramlib.ml | 2 +- serlib/ser_hints.ml | 5 +- serlib/ser_hints.mli | 4 + serlib/ser_impargs.ml | 25 +- serlib/ser_impargs.mli | 3 + serlib/ser_int.ml | 3 +- serlib/ser_int.mli | 4 + serlib/ser_libnames.ml | 7 +- serlib/ser_libnames.mli | 2 + serlib/ser_loadpath.ml | 6 +- serlib/ser_loc.ml | 9 +- serlib/ser_loc.mli | 10 +- serlib/ser_locus.ml | 9 +- serlib/ser_locus.mli | 2 + serlib/ser_mod_subst.ml | 15 +- serlib/ser_mod_subst.mli | 6 + serlib/ser_namegen.ml | 2 +- serlib/ser_names.ml | 79 ++++-- serlib/ser_names.mli | 87 ++++--- serlib/ser_nativevalues.ml | 7 +- serlib/ser_notation.ml | 3 +- serlib/ser_notation.mli | 2 + serlib/ser_notation_gram.ml | 7 +- serlib/ser_notation_gram.mli | 2 + serlib/ser_notation_term.ml | 2 +- serlib/ser_notation_term.mli | 2 + serlib/ser_numTok.ml | 13 +- serlib/ser_opaqueproof.ml | 17 +- serlib/ser_opaqueproof.mli | 4 + serlib/ser_pattern.ml | 2 +- serlib/ser_pattern.mli | 2 + serlib/ser_pp.ml | 12 +- serlib/ser_pp.mli | 4 + serlib/ser_ppextend.ml | 13 +- serlib/ser_ppextend.mli | 4 + serlib/ser_printer.ml | 2 +- serlib/ser_proof_bullet.ml | 3 +- serlib/ser_range.ml | 2 + serlib/ser_retroknowledge.ml | 2 + serlib/ser_retroknowledge.mli | 4 +- serlib/ser_rtree.ml | 6 +- serlib/ser_sorts.ml | 9 +- serlib/ser_sorts.mli | 7 +- serlib/ser_stateid.ml | 9 +- serlib/ser_stateid.mli | 4 +- serlib/ser_stdlib.ml | 5 + serlib/ser_stm.ml | 5 +- serlib/ser_stm.mli | 2 + serlib/ser_tok.ml | 10 +- serlib/ser_tok.mli | 5 +- serlib/ser_typeclasses.ml | 3 +- serlib/ser_typeclasses.mli | 2 + serlib/ser_uGraph.ml | 5 +- serlib/ser_uGraph.mli | 5 + serlib/ser_uState.ml | 3 +- serlib/ser_uint63.ml | 6 +- serlib/ser_univ.ml | 56 +++-- serlib/ser_univ.mli | 19 +- serlib/ser_univNames.ml | 3 +- serlib/ser_util.ml | 2 +- serlib/ser_util.mli | 2 + serlib/ser_vernacexpr.ml | 178 ++++++++----- serlib/ser_vernacexpr.mli | 2 + serlib/ser_vmemitcodes.ml | 5 + serlib/ser_vmemitcodes.mli | 2 + serlib/ser_vmvalues.ml | 5 +- serlib/ser_vmvalues.mli | 4 + serlib/serlib_base.ml | 10 + serlib/serlib_base.mli | 3 + sertop/dune | 6 +- sertop/sertop_pyser.ml | 305 +++++++++++++++++++++++ sertop/sertop_ser.ml | 4 + 133 files changed, 1410 insertions(+), 423 deletions(-) create mode 100644 serlib/ppx_python_runtime_serapi.ml create mode 100644 sertop/sertop_pyser.ml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0291cdd4..40465cb1 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/coq-serapi.opam b/coq-serapi.opam index e970211f..05ce4059 100644 --- a/coq-serapi.opam +++ b/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 ] diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index 1aa52ecd..2e273b41 100644 --- a/serapi/serapi_protocol.ml +++ b/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 diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli index 2fee755b..288cbf96 100644 --- a/serapi/serapi_protocol.mli +++ b/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. *) diff --git a/serlib/dune b/serlib/dune index 3e538340..e70fe0c7 100644 --- 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_deriving_yojson)) + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_python)) (libraries coq.stm sexplib)) diff --git a/serlib/plugins/ltac/dune b/serlib/plugins/ltac/dune index 2e25c0a0..e1ab7dda 100644 --- 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)) + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python)) (libraries coq.plugins.ltac serlib sexplib)) diff --git a/serlib/plugins/ltac/ser_profile_ltac.ml b/serlib/plugins/ltac/ser_profile_ltac.ml index cb325573..c360058e 100644 --- a/serlib/plugins/ltac/ser_profile_ltac.ml +++ b/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] diff --git a/serlib/plugins/ltac/ser_profile_ltac.mli b/serlib/plugins/ltac/ser_profile_ltac.mli index 2dc8b7eb..75ecb7b2 100644 --- 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 index 94ba91f0..3d77631c 100644 --- 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 index 7cca6039..9353dd37 100644 --- 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 index 2ac9712a..e1be5b93 100644 --- a/serlib/plugins/ltac/ser_tacexpr.ml +++ b/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 diff --git a/serlib/plugins/ltac/ser_tacexpr.mli b/serlib/plugins/ltac/ser_tacexpr.mli index 3d86de48..454d65f0 100644 --- a/serlib/plugins/ltac/ser_tacexpr.mli +++ b/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 diff --git a/serlib/ppx_python_runtime_serapi.ml b/serlib/ppx_python_runtime_serapi.ml new file mode 100644 index 00000000..9dbe8fdf --- /dev/null +++ b/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 _ = () diff --git a/serlib/serType.ml b/serlib/serType.ml index 221590d9..9938592e 100644 --- a/serlib/serType.ml +++ b/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 diff --git a/serlib/ser_attributes.ml b/serlib/ser_attributes.ml index 5f16f639..64fd1094 100644 --- a/serlib/ser_attributes.ml +++ b/serlib/ser_attributes.ml @@ -16,10 +16,11 @@ (************************************************************************) 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] @@ -27,4 +28,4 @@ and vernac_flag_value = [%import: Attributes.vernac_flag_value] and vernac_flags = [%import: Attributes.vernac_flags] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_cAst.ml b/serlib/ser_cAst.ml index 2c7f8061..a35f2b1c 100644 --- a/serlib/ser_cAst.ml +++ b/serlib/ser_cAst.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Loc = Ser_loc @@ -21,7 +22,7 @@ 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 = diff --git a/serlib/ser_cAst.mli b/serlib/ser_cAst.mli index 2005b7ce..2c337f40 100644 --- a/serlib/ser_cAst.mli +++ b/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 diff --git a/serlib/ser_cEphemeron.ml b/serlib/ser_cEphemeron.ml index 9ef69f40..a33a4d54 100644 --- a/serlib/ser_cEphemeron.ml +++ b/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) diff --git a/serlib/ser_cMap.ml b/serlib/ser_cMap.ml index 86be007c..a23af19a 100644 --- a/serlib/ser_cMap.ml +++ b/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 diff --git a/serlib/ser_cMap.mli b/serlib/ser_cMap.mli index e042f1b9..a71a554c 100644 --- a/serlib/ser_cMap.mli +++ b/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 diff --git a/serlib/ser_cPrimitives.ml b/serlib/ser_cPrimitives.ml index a3859b55..3456dcd6 100644 --- a/serlib/ser_cPrimitives.ml +++ b/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 diff --git a/serlib/ser_cSet.ml b/serlib/ser_cSet.ml index e71a819c..ce19bcd8 100644 --- a/serlib/ser_cSet.ml +++ b/serlib/ser_cSet.ml @@ -61,3 +61,23 @@ module MakeJ (M : CSig.SetS) (S : SerType.SJ with type t := M.elt) = struct map_bind S.of_yojson [] json >|= from_list end + +module type ExtSJP = sig + + include CSig.SetS + + include SerType.SJP with type t := t + +end + +module MakeJP (M : CSig.SetS) (S : SerType.SJP with type t := M.elt) = struct + + include MakeJ(M)(S) + + let python_of_t cst = + Py.List.of_list_map S.python_of_t (M.elements cst) + + let t_of_python py = + Py.List.to_list_map S.t_of_python py |> from_list + +end diff --git a/serlib/ser_cSet.mli b/serlib/ser_cSet.mli index cda713dd..d1a7b610 100644 --- a/serlib/ser_cSet.mli +++ b/serlib/ser_cSet.mli @@ -42,3 +42,16 @@ module MakeJ (M : CSig.SetS) (S : SerType.SJ with type t := M.elt) with type t = M.t and type elt = M.elt +module type ExtSJP = sig + + include CSig.SetS + + include SerType.SJP with type t := t + +end + +module MakeJP (M : CSig.SetS) (S : SerType.SJP with type t := M.elt) + : ExtSJP + with type t = M.t + and type elt = M.elt + diff --git a/serlib/ser_cUnix.ml b/serlib/ser_cUnix.ml index d63fd4c0..5b998628 100644 --- a/serlib/ser_cUnix.ml +++ b/serlib/ser_cUnix.ml @@ -14,7 +14,8 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi type physical_path = [%import: CUnix.physical_path] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_constr.ml b/serlib/ser_constr.ml index eb018ccd..b2cd7c0f 100644 --- a/serlib/ser_constr.ml +++ b/serlib/ser_constr.ml @@ -21,6 +21,8 @@ need to recurse throu the constr to build the clone. *) +open Ppx_python_runtime_serapi + open Sexplib open Sexplib.Std @@ -34,58 +36,58 @@ module Float64 = Ser_float64 type metavariable = [%import: Constr.metavariable] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type pconstant = [%import: Constr.pconstant] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type pinductive = [%import: Constr.pinductive] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type pconstructor = [%import: Constr.pconstructor] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type cast_kind = [%import: Constr.cast_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type case_style = [%import: Constr.case_style] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type case_printing = [%import: Constr.case_printing] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type case_info = [%import: Constr.case_info] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'constr pexistential = [%import: 'constr Constr.pexistential] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type ('constr, 'types) prec_declaration = [%import: ('constr, 'types) Constr.prec_declaration] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type ('constr, 'types) pfixpoint = [%import: ('constr, 'types) Constr.pfixpoint] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type ('constr, 'types) pcofixpoint = [%import: ('constr, 'types) Constr.pcofixpoint] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type constr = Constr.constr type types = Constr.constr type ('constr, 'univs) case_invert = [%import: ('constr, 'univs) Constr.case_invert] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let map_case_invert f = function | NoInvert -> NoInvert @@ -98,10 +100,10 @@ type _constr = | Meta of int | Evar of _constr pexistential | Sort of Sorts.t - | Cast of _constr * cast_kind * _types - | Prod of Names.Name.t Context.binder_annot * _types * _types - | Lambda of Names.Name.t Context.binder_annot * _types * _constr - | LetIn of Names.Name.t Context.binder_annot * _constr * _types * _constr + | Cast of _constr * cast_kind * _constr + | Prod of Names.Name.t Context.binder_annot * _constr * _constr + | Lambda of Names.Name.t Context.binder_annot * _constr * _constr + | LetIn of Names.Name.t Context.binder_annot * _constr * _constr * _constr | App of _constr * _constr array | Const of pconstant | Ind of pinductive @@ -113,9 +115,8 @@ type _constr = | Int of Uint63.t | Float of Float64.t | Array of Univ.Instance.t * _constr array * _constr * _types -[@@deriving sexp,yojson] and _types = _constr -[@@deriving sexp,yojson] +[@@deriving sexp,yojson,python] let rec _constr_put (c : constr) : _constr = let cr = _constr_put in @@ -183,12 +184,21 @@ let sexp_of_constr (c : constr) : Sexp.t = let constr_of_yojson json = Ppx_deriving_yojson_runtime.(_constr_of_yojson json >|= _constr_get) let constr_to_yojson level = _constr_to_yojson (_constr_put level) +let constr_of_python (c : Py.Object.t) : constr = + _constr_get (_constr_of_python c) + +let python_of_constr (c : constr) : Py.Object.t = + python_of__constr (_constr_put c) + let types_of_sexp = constr_of_sexp let sexp_of_types = sexp_of_constr let types_of_yojson = constr_of_yojson let types_to_yojson = constr_to_yojson +let types_of_python = constr_of_python +let python_of_types = python_of_constr + type t = constr let t_of_sexp = constr_of_sexp @@ -197,6 +207,9 @@ let sexp_of_t = sexp_of_constr let of_yojson = constr_of_yojson let to_yojson = constr_to_yojson +let t_of_python = constr_of_python +let python_of_t = python_of_constr + type rec_declaration = [%import: Constr.rec_declaration] [@@deriving sexp] @@ -219,16 +232,16 @@ let sexp_of_sorts_family = Sorts.sexp_of_family type named_declaration = [%import: Constr.named_declaration] - [@@deriving sexp] + [@@deriving sexp, python] type named_context = [%import: Constr.named_context] - [@@deriving sexp] + [@@deriving sexp, python] type rel_declaration = [%import: Constr.rel_declaration] - [@@deriving sexp] + [@@deriving sexp, python] type rel_context = [%import: Constr.rel_context] - [@@deriving sexp] + [@@deriving sexp, python] diff --git a/serlib/ser_constr.mli b/serlib/ser_constr.mli index 2349c5d6..0188ff0c 100644 --- a/serlib/ser_constr.mli +++ b/serlib/ser_constr.mli @@ -46,6 +46,8 @@ val case_style_of_sexp : Sexp.t -> case_style val sexp_of_case_style : case_style -> Sexp.t val case_style_of_yojson : Yojson.Safe.t -> (case_style, string) Result.result val case_style_to_yojson : case_style -> Yojson.Safe.t +val case_style_of_python : Py.Object.t -> case_style +val python_of_case_style : case_style -> Py.Object.t type case_printing = Constr.case_printing @@ -114,6 +116,9 @@ val sexp_of_t : t -> Sexp.t val of_yojson : Yojson.Safe.t -> (t, string) Result.result val to_yojson : t -> Yojson.Safe.t +val t_of_python : Py.Object.t -> t +val python_of_t : t -> Py.Object.t + type constr = t val constr_of_sexp : Sexp.t -> constr @@ -122,6 +127,9 @@ val sexp_of_constr : constr -> Sexp.t val constr_of_yojson : Yojson.Safe.t -> (constr, string) Result.result val constr_to_yojson : constr -> Yojson.Safe.t +val constr_of_python : Py.Object.t -> constr +val python_of_constr : constr -> Py.Object.t + type types = constr val types_of_sexp : Sexp.t -> types val sexp_of_types : types -> Sexp.t @@ -129,6 +137,9 @@ val sexp_of_types : types -> Sexp.t val types_of_yojson : Yojson.Safe.t -> (types, string) Result.result val types_to_yojson : types -> Yojson.Safe.t +val types_of_python : Py.Object.t -> types +val python_of_types : types -> Py.Object.t + type existential = Constr.existential val existential_of_sexp : Sexp.t -> existential val sexp_of_existential : existential -> Sexp.t @@ -140,15 +151,23 @@ val sexp_of_sorts_family : sorts_family -> Sexp.t type named_declaration = Constr.named_declaration val named_declaration_of_sexp : Sexp.t -> named_declaration val sexp_of_named_declaration : named_declaration -> Sexp.t +val named_declaration_of_python : Py.Object.t -> named_declaration +val python_of_named_declaration : named_declaration -> Py.Object.t type named_context = Constr.named_context val named_context_of_sexp : Sexp.t -> named_context val sexp_of_named_context : named_context -> Sexp.t +val named_context_of_python : Py.Object.t -> named_context +val python_of_named_context : named_context -> Py.Object.t type rel_declaration = Constr.rel_declaration val rel_declaration_of_sexp : Sexp.t -> rel_declaration val sexp_of_rel_declaration : rel_declaration -> Sexp.t +val rel_declaration_of_python : Py.Object.t -> rel_declaration +val python_of_rel_declaration : rel_declaration -> Py.Object.t type rel_context = Constr.rel_context val rel_context_of_sexp : Sexp.t -> rel_context val sexp_of_rel_context : rel_context -> Sexp.t +val rel_context_of_python : Py.Object.t -> rel_context +val python_of_rel_context : rel_context -> Py.Object.t diff --git a/serlib/ser_constrexpr.ml b/serlib/ser_constrexpr.ml index bb6f3bed..28616b12 100644 --- a/serlib/ser_constrexpr.ml +++ b/serlib/ser_constrexpr.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Loc = Ser_loc module CAst = Ser_cAst @@ -31,63 +32,63 @@ module Univ = Ser_univ type sort_name_expr = [%import: Constrexpr.sort_name_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type univ_level_expr = [%import: Constrexpr.univ_level_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type sort_expr = [%import: Constrexpr.sort_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type univ_constraint_expr = [%import: Constrexpr.univ_constraint_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type instance_expr = [%import: Constrexpr.instance_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a or_by_notation_r = [%import: 'a Constrexpr.or_by_notation_r] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a or_by_notation = [%import: 'a Constrexpr.or_by_notation] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type universe_decl_expr = [%import: Constrexpr.universe_decl_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type ident_decl = [%import: Constrexpr.ident_decl] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type cumul_univ_decl_expr = [%import: Constrexpr.cumul_univ_decl_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type cumul_ident_decl = [%import: Constrexpr.cumul_ident_decl] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type name_decl = [%import: Constrexpr.name_decl] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type notation_entry = [%import: Constrexpr.notation_entry] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type entry_level = [%import: Constrexpr.entry_level] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type entry_relative_level = [%import: Constrexpr.entry_relative_level] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type notation_entry_level = [%import: Constrexpr.notation_entry_level] @@ -95,22 +96,22 @@ type notation_entry_level = type notation_key = [%import: Constrexpr.notation_key] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type notation = [%import: Constrexpr.notation] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type explicitation = [%import: Constrexpr.explicitation] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type binder_kind = [%import: Constrexpr.binder_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type abstraction_kind = [%import: Constrexpr.abstraction_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type proj_flag = [%import: Constrexpr.proj_flag] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type raw_numeral = [%import: Constrexpr.raw_numeral] * [@@deriving sexp,yojson] *) @@ -119,11 +120,11 @@ type proj_flag = [%import: Constrexpr.proj_flag] * [@@deriving sexp,yojson] *) type prim_token = [%import: Constrexpr.prim_token] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type notation_with_optional_scope = [%import: Constrexpr.notation_with_optional_scope] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type cases_pattern_expr_r = [%import: Constrexpr.cases_pattern_expr_r] and cases_pattern_expr = [%import: Constrexpr.cases_pattern_expr] @@ -140,16 +141,17 @@ and recursion_order_expr_r = [%import: Constrexpr.recursion_order_expr_r] and recursion_order_expr = [%import: Constrexpr.recursion_order_expr] and local_binder_expr = [%import: Constrexpr.local_binder_expr] and constr_notation_substitution = [%import: Constrexpr.constr_notation_substitution] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type constr_pattern_expr = [%import: Constrexpr.constr_pattern_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type with_declaration_ast = [%import: Constrexpr.with_declaration_ast] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] -type module_ast_r = [%import: Constrexpr.module_ast_r] +type module_ast_r = + [%import: Constrexpr.module_ast_r] and module_ast = [%import: Constrexpr.module_ast] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_constrexpr.mli b/serlib/ser_constrexpr.mli index 0c40a63a..831f9c33 100644 --- a/serlib/ser_constrexpr.mli +++ b/serlib/ser_constrexpr.mli @@ -20,18 +20,24 @@ val or_by_notation_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a or_by_notation val sexp_of_or_by_notation : ('a -> Sexp.t) -> 'a or_by_notation -> Sexp.t val or_by_notation_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a or_by_notation, string) Result.result val or_by_notation_to_yojson : ('a -> Yojson.Safe.t) -> 'a or_by_notation -> Yojson.Safe.t +val or_by_notation_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a or_by_notation +val python_of_or_by_notation : ('a -> Py.Object.t) -> 'a or_by_notation -> Py.Object.t type notation_entry = Constrexpr.notation_entry val notation_entry_of_sexp : Sexp.t -> notation_entry val sexp_of_notation_entry : notation_entry -> Sexp.t val notation_entry_of_yojson : Yojson.Safe.t -> (notation_entry, string) Result.result val notation_entry_to_yojson : notation_entry -> Yojson.Safe.t +val notation_entry_of_python : Py.Object.t -> notation_entry +val python_of_notation_entry : notation_entry -> Py.Object.t type entry_level = Constrexpr.entry_level val entry_level_of_sexp : Sexp.t -> entry_level val sexp_of_entry_level : entry_level -> Sexp.t val entry_level_of_yojson : Yojson.Safe.t -> (entry_level, string) Result.result val entry_level_to_yojson : entry_level -> Yojson.Safe.t +val entry_level_of_python : Py.Object.t -> entry_level +val python_of_entry_level : entry_level -> Py.Object.t type notation_entry_level = Constrexpr.notation_entry_level val notation_entry_level_of_sexp : Sexp.t -> notation_entry_level @@ -44,47 +50,64 @@ val entry_relative_level_of_sexp : Sexp.t -> entry_relative_level val sexp_of_entry_relative_level : entry_relative_level -> Sexp.t val entry_relative_level_of_yojson : Yojson.Safe.t -> (entry_relative_level, string) Result.result val entry_relative_level_to_yojson : entry_relative_level -> Yojson.Safe.t +val entry_relative_level_of_python : Py.Object.t -> entry_relative_level +val python_of_entry_relative_level : entry_relative_level -> Py.Object.t type universe_decl_expr = Constrexpr.universe_decl_expr val universe_decl_expr_of_sexp : Sexp.t -> universe_decl_expr val sexp_of_universe_decl_expr : universe_decl_expr -> Sexp.t val universe_decl_expr_of_yojson : Yojson.Safe.t -> (universe_decl_expr, string) Result.result val universe_decl_expr_to_yojson : universe_decl_expr -> Yojson.Safe.t +val universe_decl_expr_of_python : Py.Object.t -> universe_decl_expr +val python_of_universe_decl_expr : universe_decl_expr -> Py.Object.t type ident_decl = Constrexpr.ident_decl val ident_decl_of_sexp : Sexp.t -> ident_decl val sexp_of_ident_decl : ident_decl -> Sexp.t val ident_decl_of_yojson : Yojson.Safe.t -> (ident_decl, string) Result.result val ident_decl_to_yojson : ident_decl -> Yojson.Safe.t +val ident_decl_of_python : Py.Object.t -> ident_decl +val python_of_ident_decl : ident_decl -> Py.Object.t type cumul_ident_decl = Constrexpr.cumul_ident_decl val cumul_ident_decl_of_sexp : Sexp.t -> cumul_ident_decl val sexp_of_cumul_ident_decl : cumul_ident_decl -> Sexp.t val cumul_ident_decl_of_yojson : Yojson.Safe.t -> (cumul_ident_decl, string) Result.result val cumul_ident_decl_to_yojson : cumul_ident_decl -> Yojson.Safe.t +val cumul_ident_decl_of_python : Py.Object.t -> cumul_ident_decl +val python_of_cumul_ident_decl : cumul_ident_decl -> Py.Object.t type univ_constraint_expr = Constrexpr.univ_constraint_expr val univ_constraint_expr_of_sexp : Sexp.t -> univ_constraint_expr val sexp_of_univ_constraint_expr : univ_constraint_expr -> Sexp.t val univ_constraint_expr_of_yojson : Yojson.Safe.t -> (univ_constraint_expr, string) Result.result val univ_constraint_expr_to_yojson : univ_constraint_expr -> Yojson.Safe.t +val univ_constraint_expr_of_python : Py.Object.t -> univ_constraint_expr +val python_of_univ_constraint_expr : univ_constraint_expr -> Py.Object.t type name_decl = Constrexpr.name_decl val name_decl_of_sexp : Sexp.t -> name_decl val sexp_of_name_decl : name_decl -> Sexp.t val name_decl_of_yojson : Yojson.Safe.t -> (name_decl, string) Result.result val name_decl_to_yojson : name_decl -> Yojson.Safe.t +val name_decl_of_python : Py.Object.t -> name_decl +val python_of_name_decl : name_decl -> Py.Object.t type notation = Constrexpr.notation val notation_of_sexp : Sexp.t -> notation val sexp_of_notation : notation -> Sexp.t +val notation_of_python : Py.Object.t -> notation +val python_of_notation : notation -> Py.Object.t type explicitation = Constrexpr.explicitation val explicitation_of_sexp : Sexp.t -> explicitation val sexp_of_explicitation : explicitation -> Sexp.t +val explicitation_of_python : Py.Object.t -> explicitation +val python_of_explicitation : explicitation -> Py.Object.t + type binder_kind = Constrexpr.binder_kind val binder_kind_of_sexp : Sexp.t -> binder_kind @@ -130,6 +153,8 @@ and local_binder_expr = Constrexpr.local_binder_expr and constr_notation_substitution = Constrexpr.constr_notation_substitution val constr_expr_of_sexp : Sexp.t -> constr_expr +val constr_expr_of_python : Py.Object.t -> constr_expr + val case_expr_of_sexp : Sexp.t -> case_expr val branch_expr_of_sexp : Sexp.t -> branch_expr (* val binder_expr_of_sexp : Sexp.t -> binder_expr *) @@ -138,6 +163,8 @@ val cofix_expr_of_sexp : Sexp.t -> cofix_expr val constr_notation_substitution_of_sexp : Sexp.t -> constr_notation_substitution val sexp_of_constr_expr : constr_expr -> Sexp.t +val python_of_constr_expr : constr_expr -> Py.Object.t + val sexp_of_case_expr : case_expr -> Sexp.t val sexp_of_branch_expr : branch_expr -> Sexp.t (* val sexp_of_binder_expr : binder_expr -> Sexp.t *) @@ -149,11 +176,15 @@ val recursion_order_expr_of_sexp : Sexp.t -> recursion_order_expr val sexp_of_recursion_order_expr : recursion_order_expr -> Sexp.t val recursion_order_expr_of_yojson : Yojson.Safe.t -> (recursion_order_expr, string) Result.result val recursion_order_expr_to_yojson : recursion_order_expr -> Yojson.Safe.t +val recursion_order_expr_of_python : Py.Object.t -> recursion_order_expr +val python_of_recursion_order_expr : recursion_order_expr -> Py.Object.t val sexp_of_local_binder_expr : local_binder_expr -> Sexp.t val local_binder_expr_of_sexp : Sexp.t -> local_binder_expr val local_binder_expr_of_yojson : Yojson.Safe.t -> (local_binder_expr, string) Result.result val local_binder_expr_to_yojson : local_binder_expr -> Yojson.Safe.t +val python_of_local_binder_expr : local_binder_expr -> Py.Object.t +val local_binder_expr_of_python : Py.Object.t -> local_binder_expr val constr_expr_of_yojson : Yojson.Safe.t -> (constr_expr, string) Result.result val constr_expr_to_yojson : constr_expr -> Yojson.Safe.t @@ -163,6 +194,8 @@ val constr_pattern_expr_of_sexp : Sexp.t -> constr_pattern_expr val sexp_of_constr_pattern_expr : constr_pattern_expr -> Sexp.t val constr_pattern_expr_of_yojson : Yojson.Safe.t -> (constr_pattern_expr, string) Result.result val constr_pattern_expr_to_yojson : constr_pattern_expr -> Yojson.Safe.t +val constr_pattern_expr_of_python : Py.Object.t -> constr_pattern_expr +val python_of_constr_pattern_expr : constr_pattern_expr -> Py.Object.t type with_declaration_ast = Constrexpr.with_declaration_ast @@ -177,3 +210,5 @@ val module_ast_of_sexp : Sexp.t -> module_ast val sexp_of_module_ast : module_ast -> Sexp.t val module_ast_of_yojson : Yojson.Safe.t -> (module_ast, string) Result.result val module_ast_to_yojson : module_ast -> Yojson.Safe.t +val module_ast_of_python : Py.Object.t -> module_ast +val python_of_module_ast : module_ast -> Py.Object.t diff --git a/serlib/ser_context.ml b/serlib/ser_context.ml index a791d321..0e7b0cb5 100644 --- a/serlib/ser_context.ml +++ b/serlib/ser_context.ml @@ -19,9 +19,11 @@ open Sexplib.Conv module Names = Ser_names module Sorts = Ser_sorts +open Ppx_python_runtime_serapi + type 'a binder_annot = [%import: 'a Context.binder_annot] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] module Rel = struct @@ -29,13 +31,13 @@ module Rel = struct type ('constr, 'types) pt = [%import: ('constr, 'types) Context.Rel.Declaration.pt] - [@@deriving sexp] + [@@deriving sexp,python] end type ('constr, 'types) pt = [%import: ('constr, 'types) Context.Rel.pt] - [@@deriving sexp] + [@@deriving sexp,python] end @@ -45,13 +47,13 @@ module Named = struct type ('constr, 'types) pt = [%import: ('constr, 'types) Context.Named.Declaration.pt] - [@@deriving sexp] + [@@deriving sexp,python] end type ('constr, 'types) pt = [%import: ('constr, 'types) Context.Named.pt] - [@@deriving sexp] + [@@deriving sexp,python] end @@ -61,13 +63,13 @@ module Compacted = struct type ('constr, 'types) pt = [%import: ('constr, 'types) Context.Compacted.Declaration.pt] - [@@deriving sexp] + [@@deriving sexp,python] end type ('constr, 'types) pt = [%import: ('constr, 'types) Context.Compacted.pt] - [@@deriving sexp] + [@@deriving sexp,python] end diff --git a/serlib/ser_context.mli b/serlib/ser_context.mli index 5712f43e..00f6a40f 100644 --- a/serlib/ser_context.mli +++ b/serlib/ser_context.mli @@ -23,20 +23,30 @@ val sexp_of_binder_annot : ('a -> Sexp.t) -> 'a binder_annot -> Sexp.t val binder_annot_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a binder_annot, string) Result.result val binder_annot_to_yojson : ('a -> Yojson.Safe.t) -> 'a binder_annot -> Yojson.Safe.t +val binder_annot_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a binder_annot +val python_of_binder_annot : ('a -> Py.Object.t) -> 'a binder_annot -> Py.Object.t module Rel : sig module Declaration : sig type ('c,'t) pt = ('c,'t) Context.Rel.Declaration.pt + val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> Sexp.t -> ('c,'t) pt val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('c,'t) pt -> Sexp.t + val pt_of_python : (Py.Object.t -> 'c) -> (Py.Object.t -> 't) -> Py.Object.t -> ('c,'t) pt + val python_of_pt : ('c -> Py.Object.t) -> ('t -> Py.Object.t) -> ('c,'t) pt -> Py.Object.t + end type ('c, 't) pt = ('c,'t) Context.Rel.pt + val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> Sexp.t -> ('c,'t) pt val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('c,'t) pt -> Sexp.t + val pt_of_python : (Py.Object.t -> 'c) -> (Py.Object.t -> 't) -> Py.Object.t -> ('c,'t) pt + val python_of_pt : ('c -> Py.Object.t) -> ('t -> Py.Object.t) -> ('c,'t) pt -> Py.Object.t + end module Named : sig @@ -44,15 +54,23 @@ module Named : sig module Declaration : sig type ('c, 't) pt = ('c, 't) Context.Named.Declaration.pt + val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> Sexp.t -> ('c,'t) pt val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('c,'t) pt -> Sexp.t + val pt_of_python : (Py.Object.t -> 'c) -> (Py.Object.t -> 't) -> Py.Object.t -> ('c,'t) pt + val python_of_pt : ('c -> Py.Object.t) -> ('t -> Py.Object.t) -> ('c,'t) pt -> Py.Object.t + end type ('c, 't) pt = ('c, 't) Context.Named.pt + val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> Sexp.t -> ('c,'t) pt val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('c,'t) pt -> Sexp.t + val pt_of_python : (Py.Object.t -> 'c) -> (Py.Object.t -> 't) -> Py.Object.t -> ('c,'t) pt + val python_of_pt : ('c -> Py.Object.t) -> ('t -> Py.Object.t) -> ('c,'t) pt -> Py.Object.t + end module Compacted : sig diff --git a/serlib/ser_conv_oracle.ml b/serlib/ser_conv_oracle.ml index ed087db3..0e0c0492 100644 --- a/serlib/ser_conv_oracle.ml +++ b/serlib/ser_conv_oracle.ml @@ -14,16 +14,18 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime type level = [%import: Conv_oracle.level] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* XXX: Fixme *) type oracle = [%import: Conv_oracle.oracle] -let sexp_of_oracle _ = - Sexplib.Sexp.(Atom "[Conv_oracle.oracle: Abstract]") - +let sexp_of_oracle = Serlib_base.sexp_of_opaque ~typ:"Conv_oracle.oracle" let oracle_of_sexp _ = Conv_oracle.empty + +let python_of_oracle = Serlib_base.python_of_opaque ~typ:"Conv_oracle.oracle" +let oracle_of_python _ = Conv_oracle.empty diff --git a/serlib/ser_conv_oracle.mli b/serlib/ser_conv_oracle.mli index 11a35781..97ca35bd 100644 --- a/serlib/ser_conv_oracle.mli +++ b/serlib/ser_conv_oracle.mli @@ -20,7 +20,12 @@ val level_of_sexp : Sexp.t -> level val sexp_of_level : level -> Sexp.t val level_of_yojson : Yojson.Safe.t -> (level, string) Result.result val level_to_yojson : level -> Yojson.Safe.t +val level_of_python : Py.Object.t -> level +val python_of_level : level -> Py.Object.t type oracle = Conv_oracle.oracle val oracle_of_sexp : Sexp.t -> oracle val sexp_of_oracle : oracle -> Sexp.t +val oracle_of_python : Py.Object.t -> oracle +val python_of_oracle : oracle -> Py.Object.t + diff --git a/serlib/ser_declarations.ml b/serlib/ser_declarations.ml index 7195f86c..dd063633 100644 --- a/serlib/ser_declarations.ml +++ b/serlib/ser_declarations.ml @@ -15,6 +15,8 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi + open Declarations module Rtree = Ser_rtree @@ -33,64 +35,64 @@ module Retroknowledge = Ser_retroknowledge type template_arity = [%import: Declarations.template_arity] - [@@deriving sexp] + [@@deriving sexp,python] type ('a, 'b) declaration_arity = [%import: ('a, 'b) Declarations.declaration_arity] - [@@deriving sexp] + [@@deriving sexp,python] type nested_type = [%import: Declarations.nested_type] - [@@deriving sexp] + [@@deriving sexp,python] type recarg = [%import: Declarations.recarg] - [@@deriving sexp] + [@@deriving sexp,python] type wf_paths = [%import: Declarations.wf_paths] - [@@deriving sexp] + [@@deriving sexp,python] type regular_inductive_arity = [%import: Declarations.regular_inductive_arity [@with Term.sorts := Sorts.t;]] - [@@deriving sexp] + [@@deriving sexp,python] type inductive_arity = [%import: Declarations.inductive_arity] - [@@deriving sexp] + [@@deriving sexp,python] type one_inductive_body = [%import: Declarations.one_inductive_body] - [@@deriving sexp] + [@@deriving sexp,python] type set_predicativity = [%import: Declarations.set_predicativity] - [@@deriving sexp] + [@@deriving sexp,python] type engagement = [%import: Declarations.engagement] - [@@deriving sexp] + [@@deriving sexp,python] type inline = [%import: Declarations.inline] - [@@deriving sexp] + [@@deriving sexp,python] type universes = [%import: Declarations.universes] - [@@deriving sexp] + [@@deriving sexp,python] type ('a, 'b) constant_def = [%import: ('a, 'b) Declarations.constant_def] - [@@deriving sexp] + [@@deriving sexp,python] type typing_flags = [%import: Declarations.typing_flags] - [@@deriving sexp] + [@@deriving sexp,python] type 'a constant_body = [%import: 'a Declarations.constant_body] - [@@deriving sexp] + [@@deriving sexp,python] let sexp_of_constant_body f e = (* We cannot handle VM values *) @@ -103,67 +105,77 @@ let sexp_of_module_retroknowledge _ = let module_retroknowledge_of_sexp _ = Serlib_base.opaque_of_sexp ~typ:"Declarations.module_retroknowledge" +let _python_of_module_retroknowledge _ = + Serlib_base.python_of_opaque ~typ:"Declarations.module_retroknowledge" + +let _module_retroknowledge_of_python _ = + Serlib_base.opaque_of_python ~typ:"Declarations.module_retroknowledge" + (* type abstract_inductive_universes = * [%import: Declarations.abstract_inductive_universes] * [@@deriving sexp] *) type recursivity_kind = [%import: Declarations.recursivity_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type record_info = [%import: Declarations.record_info] - [@@deriving sexp] + [@@deriving sexp,python] type template_universes = [%import: Declarations.template_universes] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type mutual_inductive_body = [%import: Declarations.mutual_inductive_body [@with Context.section_context := Context.Named.t;]] - [@@deriving sexp] + [@@deriving sexp,python] type ('ty,'a) functorize = [%import: ('ty, 'a) Declarations.functorize] - [@@deriving sexp] + [@@deriving sexp,python] type with_declaration = [%import: Declarations.with_declaration] - [@@deriving sexp] + [@@deriving sexp,python] type module_alg_expr = [%import: Declarations.module_alg_expr] - [@@deriving sexp] + [@@deriving sexp,python] type structure_field_body = [%import: Declarations.structure_field_body] - [@@deriving sexp] and structure_body = [%import: Declarations.structure_body] - [@@deriving sexp] and module_signature = [%import: Declarations.module_signature] - [@@deriving sexp] and module_expression = [%import: Declarations.module_expression] - [@@deriving sexp] and module_implementation = [%import: Declarations.module_implementation] - [@@deriving sexp] and 'a generic_module_body = [%import: 'a Declarations.generic_module_body] - [@@deriving sexp] and module_body = [%import: Declarations.module_body] - [@@deriving sexp] and module_type_body = [%import: Declarations.module_type_body] [@@deriving sexp] +(* Strange error, need to recheck what is going on *) +(* [@@deriving sexp,python] *) + +let python_of_module_body = + Serlib_base.python_of_opaque ~typ:"module_body" +let module_body_of_python = + Serlib_base.opaque_of_python ~typ:"module_body" +let python_of_module_type_body = + Serlib_base.python_of_opaque ~typ:"module_type_body" +let module_type_body_of_python = + Serlib_base.opaque_of_python ~typ:"module_type_body" diff --git a/serlib/ser_declarations.mli b/serlib/ser_declarations.mli index 7944c7bb..b98823ca 100644 --- a/serlib/ser_declarations.mli +++ b/serlib/ser_declarations.mli @@ -55,14 +55,20 @@ val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t type set_predicativity = Declarations.set_predicativity val set_predicativity_of_sexp : Sexp.t -> set_predicativity val sexp_of_set_predicativity : set_predicativity -> Sexp.t +val set_predicativity_of_python : Py.Object.t -> set_predicativity +val python_of_set_predicativity : set_predicativity -> Py.Object.t type engagement = Declarations.engagement val engagement_of_sexp : Sexp.t -> engagement val sexp_of_engagement : engagement -> Sexp.t +val engagement_of_python : Py.Object.t -> engagement +val python_of_engagement : engagement -> Py.Object.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 +val typing_flags_of_python : Py.Object.t -> typing_flags +val python_of_typing_flags : typing_flags -> Py.Object.t type inline = Declarations.inline val sexp_of_inline : inline -> Sexp.t @@ -71,6 +77,8 @@ val inline_of_sexp : Sexp.t -> inline type 'opaque constant_body = 'opaque Declarations.constant_body val sexp_of_constant_body : ('opaque -> Sexp.t) -> 'opaque constant_body -> Sexp.t val constant_body_of_sexp : (Sexp.t -> 'opaque) -> Sexp.t -> 'opaque constant_body +val python_of_constant_body : ('opaque -> Py.Object.t) -> 'opaque constant_body -> Py.Object.t +val constant_body_of_python : (Py.Object.t -> 'opaque) -> Py.Object.t -> 'opaque constant_body (* type record_body = Declarations.record_body * val record_body_of_sexp : Sexp.t -> record_body @@ -85,6 +93,8 @@ val recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.t type mutual_inductive_body = Declarations.mutual_inductive_body val mutual_inductive_body_of_sexp : Sexp.t -> mutual_inductive_body val sexp_of_mutual_inductive_body : mutual_inductive_body -> Sexp.t +val mutual_inductive_body_of_python : Py.Object.t -> mutual_inductive_body +val python_of_mutual_inductive_body : mutual_inductive_body -> Py.Object.t type module_alg_expr = Declarations.module_alg_expr val sexp_of_module_alg_expr : module_alg_expr -> Sexp.t @@ -97,7 +107,11 @@ val structure_body_of_sexp : Sexp.t -> structure_body type module_body = Declarations.module_body val sexp_of_module_body : module_body -> Sexp.t val module_body_of_sexp : Sexp.t -> module_body +val python_of_module_body : module_body -> Py.Object.t +val module_body_of_python : Py.Object.t -> module_body type module_type_body = Declarations.module_type_body val sexp_of_module_type_body : module_type_body -> Sexp.t val module_type_body_of_sexp : Sexp.t -> module_type_body +val python_of_module_type_body : module_type_body -> Py.Object.t +val module_type_body_of_python : Py.Object.t -> module_type_body diff --git a/serlib/ser_declaremods.ml b/serlib/ser_declaremods.ml index 16c55f3c..f880c8c3 100644 --- a/serlib/ser_declaremods.ml +++ b/serlib/ser_declaremods.ml @@ -16,11 +16,12 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi type 'a module_signature = [%import: 'a Declaremods.module_signature] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type inline = [%import: Declaremods.inline] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_declaremods.mli b/serlib/ser_declaremods.mli index 3cface39..3b3e0802 100644 --- a/serlib/ser_declaremods.mli +++ b/serlib/ser_declaremods.mli @@ -23,9 +23,13 @@ val module_signature_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a module_signature val sexp_of_module_signature : ('a -> Sexp.t) -> 'a module_signature -> Sexp.t val module_signature_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a module_signature, string) Result.result val module_signature_to_yojson : ('a -> Yojson.Safe.t) -> 'a module_signature -> Yojson.Safe.t +val module_signature_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a module_signature +val python_of_module_signature : ('a -> Py.Object.t) -> 'a module_signature -> Py.Object.t type inline = Declaremods.inline val inline_of_sexp : Sexp.t -> inline val sexp_of_inline : inline -> Sexp.t val inline_of_yojson : Yojson.Safe.t -> (inline, string) Result.result val inline_to_yojson : inline -> Yojson.Safe.t +val inline_of_python : Py.Object.t -> inline +val python_of_inline : inline -> Py.Object.t diff --git a/serlib/ser_decls.ml b/serlib/ser_decls.ml index 2850fadf..389b607b 100644 --- a/serlib/ser_decls.ml +++ b/serlib/ser_decls.ml @@ -15,16 +15,16 @@ type definition_object_kind = [%import: Decls.definition_object_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type theorem_kind = [%import: Decls.theorem_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type assumption_object_kind = [%import: Decls.assumption_object_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type logical_kind = [%import: Decls.logical_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_environ.ml b/serlib/ser_environ.ml index 940a6a6b..d5ee8faf 100644 --- a/serlib/ser_environ.ml +++ b/serlib/ser_environ.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module Stdlib = Ser_stdlib module CEphemeron = Ser_cEphemeron @@ -29,34 +30,35 @@ module Declarations = Ser_declarations type lazy_val = [%import: Environ.lazy_val] let sexp_of_lazy_val = Serlib_base.sexp_of_opaque ~typ:"Environ.lazy_val" +let python_of_lazy_val = Serlib_base.python_of_opaque ~typ:"Environ.lazy_val" type stratification = [%import: Environ.stratification] - [@@deriving sexp_of] + [@@deriving sexp_of,python_of] type rel_context_val = [%import: Environ.rel_context_val] - [@@deriving sexp_of] + [@@deriving sexp_of,python_of] type named_context_val = [%import: Environ.named_context_val] - [@@deriving sexp_of] + [@@deriving sexp_of,python_of] type link_info = [%import: Environ.link_info] - [@@deriving sexp] + [@@deriving sexp,python] type key = [%import: Environ.key] - [@@deriving sexp] + [@@deriving sexp,python] type constant_key = [%import: Environ.constant_key] - [@@deriving sexp] + [@@deriving sexp,python] type mind_key = [%import: Environ.mind_key] - [@@deriving sexp] + [@@deriving sexp,python] module Globals = struct @@ -64,17 +66,20 @@ module Globals = struct type _t = [%import: Environ.Globals.view] - [@@deriving sexp] + [@@deriving sexp,python] let sexp_of_t g = sexp_of__t (Obj.magic g) let _t_of_sexp s = Obj.magic (_t_of_sexp s) + let python_of_t g = python_of__t (Obj.magic g) + let _t_of_python s = Obj.magic (_t_of_python s) end type env = [%import: Environ.env] - [@@deriving sexp_of] + [@@deriving sexp_of, python_of] let env_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Environ.env" +let env_of_python = Serlib_base.opaque_of_python ~typ:"Environ.env" let abstract_env = ref false let sexp_of_env env = diff --git a/serlib/ser_environ.mli b/serlib/ser_environ.mli index ace7c296..594779a8 100644 --- a/serlib/ser_environ.mli +++ b/serlib/ser_environ.mli @@ -24,8 +24,10 @@ type env = Environ.env val env_of_sexp : Sexp.t -> env val sexp_of_env : env -> Sexp.t -type ('constr, 'types) punsafe_judgment = ('constr, 'types) - Environ.punsafe_judgment +val env_of_python : Py.Object.t -> env +val python_of_env : env -> Py.Object.t + +type ('constr, 'types) punsafe_judgment = ('constr, 'types) Environ.punsafe_judgment val punsafe_judgment_of_sexp : (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> Sexp.t -> ('constr, 'types) punsafe_judgment val diff --git a/serlib/ser_evar.ml b/serlib/ser_evar.ml index 956bac20..b70cdace 100644 --- a/serlib/ser_evar.ml +++ b/serlib/ser_evar.ml @@ -15,12 +15,13 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime (* Private *) module Self = struct type t = [%import: Evar.t] -type _t = Ser_Evar of int [@@deriving sexp,yojson] +type _t = Ser_Evar of int [@@deriving sexp,yojson,python] let _t_put evar = Ser_Evar (Evar.repr evar) let _t_get (Ser_Evar evar) = Evar.unsafe_of_int evar @@ -30,6 +31,9 @@ let sexp_of_t evar = sexp_of__t (_t_put evar) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) +let t_of_python python = _t_get (_t_of_python python) +let python_of_t evar = python_of__t (_t_put evar) + end include Self diff --git a/serlib/ser_evar.mli b/serlib/ser_evar.mli index 301ae7fc..3c56d3ff 100644 --- a/serlib/ser_evar.mli +++ b/serlib/ser_evar.mli @@ -14,8 +14,6 @@ (* Status: Very Experimental *) (************************************************************************) -module Self : SerType.SJ with type t = Evar.t - -include module type of Self +include SerType.SJP with type t = Evar.t module Set : SerType.S with type t = Evar.Set.t diff --git a/serlib/ser_evar_kinds.ml b/serlib/ser_evar_kinds.ml index 03225ebc..5becdc7d 100644 --- a/serlib/ser_evar_kinds.ml +++ b/serlib/ser_evar_kinds.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Names = Ser_names module Evar = Ser_evar @@ -25,25 +26,25 @@ module Constr = Ser_constr type matching_var_kind = [%import: Evar_kinds.matching_var_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type obligation_definition_status = [%import: Evar_kinds.obligation_definition_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type record_field = [%import: Evar_kinds.record_field] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type question_mark = [%import: Evar_kinds.question_mark] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type subevar_kind = [%import: Evar_kinds.subevar_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type t = [%import: Evar_kinds.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_evar_kinds.mli b/serlib/ser_evar_kinds.mli index 70709c88..937d5d51 100644 --- a/serlib/ser_evar_kinds.mli +++ b/serlib/ser_evar_kinds.mli @@ -28,4 +28,4 @@ type obligation_definition_status = Evar_kinds.obligation_definition_status val obligation_definition_status_of_sexp : Sexp.t -> obligation_definition_status val sexp_of_obligation_definition_status : obligation_definition_status -> Sexp.t -include SerType.SJ with type t = Evar_kinds.t +include SerType.SJP with type t = Evar_kinds.t diff --git a/serlib/ser_extend.ml b/serlib/ser_extend.ml index 9ea7e4aa..25697a59 100644 --- a/serlib/ser_extend.ml +++ b/serlib/ser_extend.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Tok = Ser_tok module Notation_term = Ser_notation_term @@ -22,33 +23,33 @@ module Gramlib = Ser_gramlib type side = [%import: Extend.side] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type production_position = [%import: Extend.production_position] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type production_level = [%import: Extend.production_level] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type binder_entry_kind = [%import: Extend.binder_entry_kind] - [@@deriving sexp] + [@@deriving sexp,python] type 'lev constr_entry_key_gen = [%import: 'lev Extend.constr_entry_key_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type constr_entry_key = [%import: Extend.constr_entry_key] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type constr_prod_entry_key = [%import: Extend.constr_prod_entry_key] - [@@deriving sexp] + [@@deriving sexp,python] type simple_constr_prod_entry_key = [%import: Extend.simple_constr_prod_entry_key] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_extend.mli b/serlib/ser_extend.mli index 26bb9dc6..d3645211 100644 --- a/serlib/ser_extend.mli +++ b/serlib/ser_extend.mli @@ -18,6 +18,8 @@ open Sexplib type side = Extend.side val side_of_sexp : Sexp.t -> side val sexp_of_side : side -> Sexp.t +val side_of_python : Py.Object.t -> side +val python_of_side : side -> Py.Object.t type production_position = Extend.production_position val production_position_of_sexp : Sexp.t -> production_position @@ -28,6 +30,8 @@ val production_level_of_sexp : Sexp.t -> production_level val sexp_of_production_level : production_level -> Sexp.t val production_level_of_yojson : Yojson.Safe.t -> (production_level, string) Result.result val production_level_to_yojson : production_level -> Yojson.Safe.t +val production_level_of_python : Py.Object.t -> production_level +val python_of_production_level : production_level -> Py.Object.t type binder_entry_kind = Extend.binder_entry_kind val binder_entry_kind_of_sexp : Sexp.t -> binder_entry_kind @@ -42,10 +46,14 @@ val sexp_of_constr_entry_key_gen : ('lev -> Sexp.t) -> type constr_entry_key = Extend.constr_entry_key val constr_entry_key_of_sexp : Sexp.t -> constr_entry_key val sexp_of_constr_entry_key : constr_entry_key -> Sexp.t +val constr_entry_key_of_python : Py.Object.t -> constr_entry_key +val python_of_constr_entry_key : constr_entry_key -> Py.Object.t type constr_prod_entry_key = Extend.constr_prod_entry_key val constr_prod_entry_key_of_sexp : Sexp.t -> constr_prod_entry_key val sexp_of_constr_prod_entry_key : constr_prod_entry_key -> Sexp.t +val constr_prod_entry_key_of_python : Py.Object.t -> constr_prod_entry_key +val python_of_constr_prod_entry_key : constr_prod_entry_key -> Py.Object.t type simple_constr_prod_entry_key = Extend.simple_constr_prod_entry_key @@ -53,4 +61,6 @@ val simple_constr_prod_entry_key_of_sexp : Sexp.t -> simple_constr_prod_entry_ke val sexp_of_simple_constr_prod_entry_key : simple_constr_prod_entry_key -> Sexp.t val simple_constr_prod_entry_key_of_yojson : Yojson.Safe.t -> (simple_constr_prod_entry_key, string) Result.result val simple_constr_prod_entry_key_to_yojson : simple_constr_prod_entry_key -> Yojson.Safe.t +val simple_constr_prod_entry_key_of_python : Py.Object.t -> simple_constr_prod_entry_key +val python_of_simple_constr_prod_entry_key : simple_constr_prod_entry_key -> Py.Object.t diff --git a/serlib/ser_feedback.ml b/serlib/ser_feedback.ml index a1df41ba..0719de76 100644 --- a/serlib/ser_feedback.ml +++ b/serlib/ser_feedback.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime module Loc = Ser_loc @@ -23,15 +24,15 @@ module Stateid = Ser_stateid type level = [%import: Feedback.level] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type route_id = [%import: Feedback.route_id] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type doc_id = [%import: Feedback.doc_id] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type feedback_content = [%import: Feedback.feedback_content] diff --git a/serlib/ser_feedback.mli b/serlib/ser_feedback.mli index 18169f60..dd3024d7 100644 --- a/serlib/ser_feedback.mli +++ b/serlib/ser_feedback.mli @@ -21,6 +21,8 @@ val doc_id_of_sexp : Sexp.t -> doc_id val sexp_of_doc_id : doc_id -> Sexp.t val doc_id_of_yojson : Yojson.Safe.t -> (doc_id, string) Result.result val doc_id_to_yojson : doc_id -> Yojson.Safe.t +val doc_id_of_python : Py.Object.t -> doc_id +val python_of_doc_id : doc_id -> Py.Object.t type level = Feedback.level @@ -28,12 +30,16 @@ val level_of_sexp : Sexp.t -> level val sexp_of_level : level -> Sexp.t val level_of_yojson : Yojson.Safe.t -> (level, string) Result.result val level_to_yojson : level -> Yojson.Safe.t +val level_of_python : Py.Object.t -> level +val python_of_level : level -> Py.Object.t type route_id = Feedback.route_id val route_id_of_sexp : Sexp.t -> route_id val sexp_of_route_id : route_id -> Sexp.t val route_id_of_yojson : Yojson.Safe.t -> (route_id, string) Result.result val route_id_to_yojson : route_id -> Yojson.Safe.t +val route_id_of_python : Py.Object.t -> route_id +val python_of_route_id : route_id -> Py.Object.t type feedback_content = Feedback.feedback_content diff --git a/serlib/ser_float64.ml b/serlib/ser_float64.ml index 82f652e4..acda0dcb 100644 --- a/serlib/ser_float64.ml +++ b/serlib/ser_float64.ml @@ -19,7 +19,9 @@ type t = Float64.t open Sexplib.Std -type _t = float [@@deriving sexp, yojson] +open Ppx_python_runtime + +type _t = float [@@deriving sexp, yojson, python] let _t_get = Obj.magic let _t_put = Obj.magic @@ -29,3 +31,6 @@ let sexp_of_t t = sexp_of__t (_t_get t) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) + +let t_of_python t = _t_put (_t_of_python t) +let python_of_t t = python_of__t (_t_get t) diff --git a/serlib/ser_future.ml b/serlib/ser_future.ml index 605e1aca..a1ea3f6b 100644 --- a/serlib/ser_future.ml +++ b/serlib/ser_future.ml @@ -2,3 +2,6 @@ type 'a computation = 'a Future.computation let computation_of_sexp f x = Future.from_val (f x) let sexp_of_computation f x = f Future.(force x) +let computation_of_python f x = Future.from_val (f x) +let python_of_computation f x = f Future.(force x) + diff --git a/serlib/ser_genarg.ml b/serlib/ser_genarg.ml index 9556e835..955ab056 100644 --- a/serlib/ser_genarg.ml +++ b/serlib/ser_genarg.ml @@ -31,6 +31,14 @@ type tlevel = [%import: Genarg.tlevel] [@@deriving sexp,yojson] +(* XXX: fix ppx_python *) +let python_of_rlevel _ = Py.String.of_string "rlevel" +let rlevel_of_python _ = `rlevel +let python_of_glevel _ = Py.String.of_string "glevel" +let glevel_of_python _ = `glevel +let python_of_tlevel _ = Py.String.of_string "tlevel" +let tlevel_of_python _ = `tlevel + open Sexp let rec sexp_of_genarg_type : type a b c. (a, b, c) genarg_type -> t = fun gt -> @@ -193,22 +201,29 @@ let generic_argument_of_sexp _lvl sexp : 'a Genarg.generic_argument = let (RG ga) = gen_abstype_of_sexp sexp in Obj.magic ga -let generic_argument_of_yojson _lvl _json = Error "not supported generic_argument_of_yojson" -let generic_argument_to_yojson _lvl _g = `String "foo" +let generic_argument_of_yojson _lvl _json = + Error "not supported generic_argument_of_yojson" +let generic_argument_to_yojson _lvl _g = + `String "foo" + +let generic_argument_of_python _ = + Serlib_base.opaque_of_python ~typ:"generic_argument" +let python_of_generic_argument _ = + Serlib_base.python_of_opaque ~typ:"generic_argument" type 'a generic_argument = 'a Genarg.generic_argument type glob_generic_argument = [%import: Genarg.glob_generic_argument] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type raw_generic_argument = [%import: Genarg.raw_generic_argument] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type typed_generic_argument = [%import: Genarg.typed_generic_argument] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let mk_uniform pin pout = { raw_ser = pin; diff --git a/serlib/ser_genarg.mli b/serlib/ser_genarg.mli index 0f6096a5..1e9b38d0 100644 --- a/serlib/ser_genarg.mli +++ b/serlib/ser_genarg.mli @@ -50,6 +50,8 @@ val raw_generic_argument_of_sexp : Sexp.t -> Genarg.raw_generic_argument val sexp_of_raw_generic_argument : Genarg.raw_generic_argument -> Sexp.t val raw_generic_argument_of_yojson : Yojson.Safe.t -> (raw_generic_argument, string) Result.result val raw_generic_argument_to_yojson : raw_generic_argument -> Yojson.Safe.t +val raw_generic_argument_of_python : Py.Object.t -> Genarg.raw_generic_argument +val python_of_raw_generic_argument : Genarg.raw_generic_argument -> Py.Object.t type typed_generic_argument = Genarg.typed_generic_argument val typed_generic_argument_of_sexp : Sexp.t -> Genarg.typed_generic_argument diff --git a/serlib/ser_genredexpr.ml b/serlib/ser_genredexpr.ml index 997df14c..7fdf8871 100644 --- a/serlib/ser_genredexpr.ml +++ b/serlib/ser_genredexpr.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Loc = Ser_loc module Names = Ser_names @@ -28,11 +29,11 @@ type 'a red_atom = type 'a glob_red_flag = [%import: 'a Genredexpr.glob_red_flag] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type ('a,'b,'c) red_expr_gen = [%import: ('a,'b,'c) Genredexpr.red_expr_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type ('a,'b,'c) may_eval = [%import: ('a,'b,'c) Genredexpr.may_eval] @@ -41,19 +42,19 @@ type ('a,'b,'c) may_eval = (* Helpers for raw_red_expr *) type r_trm = [%import: Genredexpr.r_trm] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type r_cst = [%import: Genredexpr.r_cst] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type r_pat = [%import: Genredexpr.r_pat] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type raw_red_expr = [%import: Genredexpr.raw_red_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a and_short_name = [%import: 'a Genredexpr.and_short_name] diff --git a/serlib/ser_genredexpr.mli b/serlib/ser_genredexpr.mli index fd00bb33..1712aca4 100644 --- a/serlib/ser_genredexpr.mli +++ b/serlib/ser_genredexpr.mli @@ -53,6 +53,8 @@ val raw_red_expr_of_sexp : Sexp.t -> raw_red_expr val sexp_of_raw_red_expr : raw_red_expr -> Sexp.t val raw_red_expr_of_yojson : Yojson.Safe.t -> (raw_red_expr, string) Result.result val raw_red_expr_to_yojson : raw_red_expr -> Yojson.Safe.t +val raw_red_expr_of_python : Py.Object.t -> raw_red_expr +val python_of_raw_red_expr : raw_red_expr -> Py.Object.t type r_cst = Genredexpr.r_cst val r_cst_of_sexp : Sexp.t -> r_cst diff --git a/serlib/ser_glob_term.ml b/serlib/ser_glob_term.ml index f851cd50..2e95d90f 100644 --- a/serlib/ser_glob_term.ml +++ b/serlib/ser_glob_term.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Loc = Ser_loc module CAst = Ser_cAst @@ -34,7 +35,7 @@ module Namegen = Ser_namegen type binding_kind = [%import: Glob_term.binding_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type 'a universe_kind = * [%import: 'a Glob_term.universe_kind] @@ -46,11 +47,11 @@ type binding_kind = type glob_sort_name = [%import: Glob_term.glob_sort_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a glob_sort_gen = [%import: 'a Glob_term.glob_sort_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type 'a glob_sort_expr = * [%import: 'a Glob_term.glob_sort_expr] @@ -62,7 +63,7 @@ type glob_level = type glob_constraint = [%import: Glob_term.glob_constraint] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type sort_info = * [%import: Glob_term.sort_info] @@ -74,11 +75,11 @@ type glob_sort = type 'a cast_type = [%import: 'a Glob_term.cast_type] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type existential_name = [%import: Glob_term.existential_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a cases_pattern_r = [%import: 'a Glob_term.cases_pattern_r] and 'a cases_pattern_g = [%import: 'a Glob_term.cases_pattern_g] diff --git a/serlib/ser_glob_term.mli b/serlib/ser_glob_term.mli index 1f26cb4e..2da01ab6 100644 --- a/serlib/ser_glob_term.mli +++ b/serlib/ser_glob_term.mli @@ -20,12 +20,16 @@ val binding_kind_of_sexp : Sexp.t -> Glob_term.binding_kind val sexp_of_binding_kind : Glob_term.binding_kind -> Sexp.t val binding_kind_of_yojson : Yojson.Safe.t -> (binding_kind,string) result val binding_kind_to_yojson : Glob_term.binding_kind -> Yojson.Safe.t +val binding_kind_of_python : Py.Object.t -> Glob_term.binding_kind +val python_of_binding_kind : Glob_term.binding_kind -> Py.Object.t type 'a glob_sort_gen = 'a Glob_term.glob_sort_gen val glob_sort_gen_of_sexp : (Sexp.t -> 'a) ->Sexp.t -> 'a Glob_term.glob_sort_gen val sexp_of_glob_sort_gen : ('a -> Sexp.t) -> 'a Glob_term.glob_sort_gen -> Sexp.t val glob_sort_gen_of_yojson : (Yojson.Safe.t -> ('a,string) result ) -> Yojson.Safe.t -> ('a glob_sort_gen, string) result val glob_sort_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a Glob_term.glob_sort_gen -> Yojson.Safe.t +val glob_sort_gen_of_python : (Py.Object.t -> 'a) ->Py.Object.t -> 'a Glob_term.glob_sort_gen +val python_of_glob_sort_gen : ('a -> Py.Object.t) -> 'a Glob_term.glob_sort_gen -> Py.Object.t type glob_level = Glob_term.glob_level val glob_level_of_sexp : Sexp.t -> Glob_term.glob_level @@ -45,12 +49,16 @@ val cast_type_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a Glob_term.cast_type val sexp_of_cast_type : ('a -> Sexp.t) -> 'a Glob_term.cast_type -> Sexp.t val cast_type_of_yojson : (Yojson.Safe.t -> ('a,string) result ) -> Yojson.Safe.t -> ('a cast_type, string) Result.result val cast_type_to_yojson : ('a -> Yojson.Safe.t) -> 'a cast_type -> Yojson.Safe.t +val cast_type_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a Glob_term.cast_type +val python_of_cast_type : ('a -> Py.Object.t) -> 'a Glob_term.cast_type -> Py.Object.t type glob_constraint = Glob_term.glob_constraint val glob_constraint_of_sexp : Sexp.t -> Glob_term.glob_constraint val sexp_of_glob_constraint : Glob_term.glob_constraint -> Sexp.t val glob_constraint_of_yojson : Yojson.Safe.t -> (glob_constraint, string) Result.result val glob_constraint_to_yojson : glob_constraint -> Yojson.Safe.t +val glob_constraint_of_python : Py.Object.t -> Glob_term.glob_constraint +val python_of_glob_constraint : Glob_term.glob_constraint -> Py.Object.t type existential_name = Glob_term.existential_name @@ -68,6 +76,8 @@ val existential_name_of_sexp : Sexp.t -> Glob_term.existential_name val sexp_of_existential_name : Glob_term.existential_name -> Sexp.t val existential_name_of_yojson : Yojson.Safe.t -> (existential_name, string) Result.result val existential_name_to_yojson : existential_name -> Yojson.Safe.t +val existential_name_of_python : Py.Object.t -> Glob_term.existential_name +val python_of_existential_name : Glob_term.existential_name -> Py.Object.t val cases_pattern_of_sexp : Sexp.t -> cases_pattern val sexp_of_cases_pattern : cases_pattern -> Sexp.t diff --git a/serlib/ser_globnames.ml b/serlib/ser_globnames.ml index 7a69e15e..862b188d 100644 --- a/serlib/ser_globnames.ml +++ b/serlib/ser_globnames.ml @@ -17,8 +17,8 @@ module Names = Ser_names type syndef_name = [%import: Globnames.syndef_name] - [@@deriving sexp] + [@@deriving sexp,python] type extended_global_reference = [%import: Globnames.extended_global_reference] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_goal.ml b/serlib/ser_goal.ml index c7ed3aef..f2cff0cc 100644 --- a/serlib/ser_goal.ml +++ b/serlib/ser_goal.ml @@ -17,4 +17,4 @@ module Evar = Ser_evar type goal = [%import: Goal.goal] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_goal.mli b/serlib/ser_goal.mli index 895a7b20..08bf2fab 100644 --- a/serlib/ser_goal.mli +++ b/serlib/ser_goal.mli @@ -19,3 +19,5 @@ type goal = Goal.goal val goal_of_sexp : Sexp.t -> goal val sexp_of_goal : goal -> Sexp.t +val goal_of_python : Py.Object.t -> goal +val python_of_goal : goal -> Py.Object.t diff --git a/serlib/ser_goal_select.ml b/serlib/ser_goal_select.ml index 2577f608..c1c24412 100644 --- a/serlib/ser_goal_select.ml +++ b/serlib/ser_goal_select.ml @@ -20,9 +20,10 @@ * val sexp_of_goal_selector : goal_selector -> Sexp.t *) open Sexplib.Conv +open Ppx_python_runtime_serapi module Names = Ser_names type t = [%import: Goal_select.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_goptions.ml b/serlib/ser_goptions.ml index e65a81a3..968d8add 100644 --- a/serlib/ser_goptions.ml +++ b/serlib/ser_goptions.ml @@ -16,26 +16,27 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Libnames = Ser_libnames type option_locality = [%import: Goptions.option_locality] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type option_name = [%import: Goptions.option_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type option_value = [%import: Goptions.option_value] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type option_state = [%import: Goptions.option_state] - [@@deriving sexp] + [@@deriving sexp,python] type table_value = [%import: Goptions.table_value] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_goptions.mli b/serlib/ser_goptions.mli index e1d5361a..bd1a498d 100644 --- a/serlib/ser_goptions.mli +++ b/serlib/ser_goptions.mli @@ -28,6 +28,8 @@ val option_name_of_sexp : Sexp.t -> option_name val sexp_of_option_name : option_name -> Sexp.t val option_name_of_yojson : Yojson.Safe.t -> (option_name, string) Result.result val option_name_to_yojson : option_name -> Yojson.Safe.t +val option_name_of_python : Py.Object.t -> option_name +val python_of_option_name : option_name -> Py.Object.t type option_value = Goptions.option_value @@ -40,6 +42,8 @@ type option_state = Goptions.option_state val option_state_of_sexp : Sexp.t -> option_state val sexp_of_option_state : option_state -> Sexp.t +val option_state_of_python : Py.Object.t -> option_state +val python_of_option_state : option_state -> Py.Object.t type table_value = Goptions.table_value @@ -47,3 +51,5 @@ val table_value_of_sexp : Sexp.t -> table_value val sexp_of_table_value : table_value -> Sexp.t val table_value_of_yojson : Yojson.Safe.t -> (table_value, string) Result.result val table_value_to_yojson : table_value -> Yojson.Safe.t +val table_value_of_python : Py.Object.t -> table_value +val python_of_table_value : table_value -> Py.Object.t diff --git a/serlib/ser_gramlib.ml b/serlib/ser_gramlib.ml index a9fdd575..828282cb 100644 --- a/serlib/ser_gramlib.ml +++ b/serlib/ser_gramlib.ml @@ -16,5 +16,5 @@ module Gramext = struct type g_assoc = [%import: Gramlib.Gramext.g_assoc] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end diff --git a/serlib/ser_hints.ml b/serlib/ser_hints.ml index d04294c9..a0e5bd43 100644 --- a/serlib/ser_hints.ml +++ b/serlib/ser_hints.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module Names = Ser_names module Libnames = Ser_libnames @@ -45,7 +46,7 @@ type reference_or_constr = type hint_mode = [%import: Hints.hint_mode] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type hint_info_expr = @@ -55,7 +56,7 @@ type hint_info_expr = type 'a hints_transparency_target = [%import: 'a Hints.hints_transparency_target] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type hints_expr = diff --git a/serlib/ser_hints.mli b/serlib/ser_hints.mli index 2ca31c91..32d234cd 100644 --- a/serlib/ser_hints.mli +++ b/serlib/ser_hints.mli @@ -44,6 +44,8 @@ val hints_transparency_target_of_yojson : val hints_transparency_target_to_yojson : ('a -> Yojson.Safe.t) -> 'a hints_transparency_target -> Yojson.Safe.t +val hints_transparency_target_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a hints_transparency_target +val python_of_hints_transparency_target : ('a -> Py.Object.t) -> 'a hints_transparency_target -> Py.Object.t (* type hint_info_expr = Hints.hint_info_expr @@ -58,6 +60,8 @@ val hint_mode_of_sexp : Sexp.t -> hint_mode val sexp_of_hint_mode : hint_mode -> Sexp.t val hint_mode_of_yojson : Yojson.Safe.t -> (hint_mode, string) Result.result val hint_mode_to_yojson : hint_mode -> Yojson.Safe.t +val hint_mode_of_python : Py.Object.t -> hint_mode +val python_of_hint_mode : hint_mode -> Py.Object.t (* type hints_expr = Hints.hints_expr diff --git a/serlib/ser_impargs.ml b/serlib/ser_impargs.ml index 764a7362..6e11e741 100644 --- a/serlib/ser_impargs.ml +++ b/serlib/ser_impargs.ml @@ -15,29 +15,30 @@ open Sexplib open Sexplib.Std +open Ppx_python_runtime_serapi module Names = Ser_names module Constrexpr = Ser_constrexpr type argument_position = [%import: Impargs.argument_position] - [@@deriving sexp] + [@@deriving sexp,python] type implicit_explanation = [%import: Impargs.implicit_explanation] - [@@deriving sexp] + [@@deriving sexp,python] type maximal_insertion = [%import: Impargs.maximal_insertion] - [@@deriving sexp] + [@@deriving sexp,python] type force_inference = [%import: Impargs.force_inference] - [@@deriving sexp] + [@@deriving sexp,python] (* XXX: Careful here, we break abstraction, so this must be kept in sync with Coq. *) type _implicit_side_condition = DefaultImpArgs | LessArgsThan of int - [@@deriving sexp] + [@@deriving sexp,python] type implicit_side_condition = Impargs.implicit_side_condition @@ -47,14 +48,16 @@ let implicit_side_condition_of_sexp (sexp : Sexp.t) : implicit_side_condition = let sexp_of_implicit_side_condition (isc : implicit_side_condition) : Sexp.t = sexp_of__implicit_side_condition (Obj.magic isc) +let implicit_side_condition_of_python (python : Py.Object.t) : implicit_side_condition = + Obj.magic (_implicit_side_condition_of_python python) + +let python_of_implicit_side_condition (isc : implicit_side_condition) : Py.Object.t = + python_of__implicit_side_condition (Obj.magic isc) + type implicit_status = [%import: Impargs.implicit_status] - [@@deriving sexp] + [@@deriving sexp,python] type implicits_list = [%import: Impargs.implicits_list] - [@@deriving sexp] - - - - + [@@deriving sexp,python] diff --git a/serlib/ser_impargs.mli b/serlib/ser_impargs.mli index 6b02454b..2bb90a48 100644 --- a/serlib/ser_impargs.mli +++ b/serlib/ser_impargs.mli @@ -49,3 +49,6 @@ type implicits_list = Impargs.implicits_list val implicits_list_of_sexp : Sexp.t -> implicits_list val sexp_of_implicits_list : implicits_list -> Sexp.t + +val implicits_list_of_python : Py.Object.t -> implicits_list +val python_of_implicits_list : implicits_list -> Py.Object.t diff --git a/serlib/ser_int.ml b/serlib/ser_int.ml index b09c68fb..854fec63 100644 --- a/serlib/ser_int.ml +++ b/serlib/ser_int.ml @@ -15,8 +15,9 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi type t = [%import: Int.t] - [@@deriving sexp] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_int.mli b/serlib/ser_int.mli index 33a65752..90b72c86 100644 --- a/serlib/ser_int.mli +++ b/serlib/ser_int.mli @@ -20,3 +20,7 @@ type t = Int.t val t_of_sexp : Sexp.t -> t val sexp_of_t : t -> Sexp.t +val of_yojson : Yojson.Safe.t -> (t, string) Result.result +val to_yojson : t -> Yojson.Safe.t +val t_of_python : Py.Object.t -> t +val python_of_t : t -> Py.Object.t diff --git a/serlib/ser_libnames.ml b/serlib/ser_libnames.ml index 1955ccdc..e16f2c6d 100644 --- a/serlib/ser_libnames.ml +++ b/serlib/ser_libnames.ml @@ -23,7 +23,7 @@ module Names = Ser_names type _t = Ser_Qualid of Names.DirPath.t * Names.Id.t - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let _t_put qid = let (dp, id) = Libnames.repr_qualid (cmake qid) in @@ -40,10 +40,13 @@ let sexp_of_qualid_r qid = sexp_of__t (_t_put qid) let qualid_r_of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let qualid_r_to_yojson level = _t_to_yojson (_t_put level) +let qualid_r_of_python python = _t_get (_t_of_python python) +let python_of_qualid_r qid = python_of__t (_t_put qid) + (* qualid: private *) type qualid = [%import: Libnames.qualid] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] module FP = struct type _t = diff --git a/serlib/ser_libnames.mli b/serlib/ser_libnames.mli index e6baef3d..c01115af 100644 --- a/serlib/ser_libnames.mli +++ b/serlib/ser_libnames.mli @@ -21,6 +21,8 @@ val qualid_of_sexp : Sexp.t -> Libnames.qualid val sexp_of_qualid : Libnames.qualid -> Sexp.t val qualid_of_yojson : Yojson.Safe.t -> (qualid, string) Result.result val qualid_to_yojson : qualid -> Yojson.Safe.t +val qualid_of_python : Py.Object.t -> Libnames.qualid +val python_of_qualid : Libnames.qualid -> Py.Object.t type full_path = Libnames.full_path diff --git a/serlib/ser_loadpath.ml b/serlib/ser_loadpath.ml index d2689e42..12b503ff 100644 --- a/serlib/ser_loadpath.ml +++ b/serlib/ser_loadpath.ml @@ -16,12 +16,14 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi + module Names = Ser_names type library_location = [%import: Loadpath.library_location] - [@@deriving sexp] + [@@deriving sexp,python] type vo_path = [%import: Loadpath.vo_path] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_loc.ml b/serlib/ser_loc.ml index 705b99bf..cbe9f18b 100644 --- a/serlib/ser_loc.ml +++ b/serlib/ser_loc.ml @@ -17,15 +17,16 @@ (* Loc.mli *) (**********************************************************************) -open Sexplib.Std +open! Base +open Ppx_python_runtime type source = [%import: Loc.source] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type t = [%import: Loc.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let omit_loc = ref false let sexp_of_t x = @@ -34,4 +35,4 @@ let sexp_of_t x = (* located: public *) type 'a located = [%import: 'a Loc.located] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_loc.mli b/serlib/ser_loc.mli index 7a25ac1e..05050167 100644 --- a/serlib/ser_loc.mli +++ b/serlib/ser_loc.mli @@ -19,13 +19,7 @@ open Sexplib -type t = Loc.t - -val t_of_sexp : Sexp.t -> Loc.t -val sexp_of_t : Loc.t -> Sexp.t - -val of_yojson : Yojson.Safe.t -> (t, string) Result.result -val to_yojson : t -> Yojson.Safe.t +include SerType.SJP with type t = Loc.t (* Don't print locations. Global-flag Hack. *) val omit_loc : bool ref @@ -35,3 +29,5 @@ val located_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a Loc.located val sexp_of_located : ('a -> Sexp.t) -> 'a Loc.located -> Sexp.t val located_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a located, string) Result.result val located_to_yojson : ('a -> Yojson.Safe.t) -> 'a located -> Yojson.Safe.t +val located_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a Loc.located +val python_of_located : ('a -> Py.Object.t) -> 'a Loc.located -> Py.Object.t diff --git a/serlib/ser_locus.ml b/serlib/ser_locus.ml index 1f74ebc8..ce286704 100644 --- a/serlib/ser_locus.ml +++ b/serlib/ser_locus.ml @@ -14,24 +14,25 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Names = Ser_names type 'a or_var = [%import: 'a Locus.or_var] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a occurrences_gen = [%import: 'a Locus.occurrences_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type occurrences_expr = [%import: Locus.occurrences_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a with_occurrences = [%import: 'a Locus.with_occurrences] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type occurrences = [%import: Locus.occurrences] diff --git a/serlib/ser_locus.mli b/serlib/ser_locus.mli index bc2e36b7..e9a95cbd 100644 --- a/serlib/ser_locus.mli +++ b/serlib/ser_locus.mli @@ -36,6 +36,8 @@ val with_occurrences_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a with_occurrences val sexp_of_with_occurrences : ('a -> Sexp.t) -> 'a with_occurrences -> Sexp.t val with_occurrences_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a with_occurrences, string) Result.result val with_occurrences_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_occurrences -> Yojson.Safe.t +val with_occurrences_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a with_occurrences +val python_of_with_occurrences : ('a -> Py.Object.t) -> 'a with_occurrences -> Py.Object.t type occurrences = Locus.occurrences val occurrences_of_sexp : Sexp.t -> occurrences diff --git a/serlib/ser_mod_subst.ml b/serlib/ser_mod_subst.ml index a6025208..5a9c5705 100644 --- a/serlib/ser_mod_subst.ml +++ b/serlib/ser_mod_subst.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Names = Ser_names @@ -26,6 +27,12 @@ let sexp_of_delta_resolver = let delta_resolver_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Mod_subst.delta_resolver" +let python_of_delta_resolver = + Serlib_base.python_of_opaque ~typ:"Mod_subst.delta_resolver" + +let delta_resolver_of_python = + Serlib_base.opaque_of_python ~typ:"Mod_subst.delta_resolver" + (* type substitution = (Names.ModPath.t * delta_resolver) Names.Umap.t * [@@deriving sexp] *) @@ -35,13 +42,19 @@ type substitution = let sexp_of_substitution = Serlib_base.sexp_of_opaque ~typ:"Mod_subst.substitution" let substitution_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Mod_subst.substitution" +let python_of_substitution = Serlib_base.python_of_opaque ~typ:"Mod_subst.substitution" +let substitution_of_python = Serlib_base.opaque_of_python ~typ:"Mod_subst.substitution" + type 'a _substituted = { mutable subst_value : 'a; mutable subst_subst : substitution list; -} [@@deriving sexp] +} [@@deriving sexp,python] type 'a substituted = [%import: 'a Mod_subst.substituted] let sexp_of_substituted f x = sexp_of__substituted f (Obj.magic x) let substituted_of_sexp f x = Obj.magic (_substituted_of_sexp f x) + +let python_of_substituted f x = python_of__substituted f (Obj.magic x) +let substituted_of_python f x = Obj.magic (_substituted_of_python f x) diff --git a/serlib/ser_mod_subst.mli b/serlib/ser_mod_subst.mli index 381801fc..c1b74b16 100644 --- a/serlib/ser_mod_subst.mli +++ b/serlib/ser_mod_subst.mli @@ -18,11 +18,17 @@ open Sexplib type delta_resolver = Mod_subst.delta_resolver val sexp_of_delta_resolver : delta_resolver -> Sexp.t val delta_resolver_of_sexp : Sexp.t -> delta_resolver +val python_of_delta_resolver : delta_resolver -> Py.Object.t +val delta_resolver_of_python : Py.Object.t -> delta_resolver type substitution = Mod_subst.substitution val sexp_of_substitution : substitution -> Sexp.t val substitution_of_sexp : Sexp.t -> substitution +val python_of_substitution : substitution -> Py.Object.t +val substitution_of_python : Py.Object.t -> substitution type 'a substituted = 'a Mod_subst.substituted val sexp_of_substituted : ('a -> Sexp.t) -> 'a substituted -> Sexp.t val substituted_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a substituted +val python_of_substituted : ('a -> Py.Object.t) -> 'a substituted -> Py.Object.t +val substituted_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a substituted diff --git a/serlib/ser_namegen.ml b/serlib/ser_namegen.ml index 46bbc135..39a18ad6 100644 --- a/serlib/ser_namegen.ml +++ b/serlib/ser_namegen.ml @@ -19,4 +19,4 @@ module Names = Ser_names type intro_pattern_naming_expr = [%import: Namegen.intro_pattern_naming_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_names.ml b/serlib/ser_names.ml index e62a5871..bf8e1799 100644 --- a/serlib/ser_names.ml +++ b/serlib/ser_names.ml @@ -17,6 +17,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi open Names @@ -33,7 +34,7 @@ module Id = struct module Self = struct type t = [%import: Names.Id.t] -type _t = Id of string [@@deriving sexp, yojson] +type _t = Id of string [@@deriving sexp, yojson, python] let _t_put id = Id (Id.to_string id) let _t_get (Id id) = Id.of_string_soft id @@ -43,12 +44,15 @@ let sexp_of_t id = sexp_of__t (_t_put id) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) +let t_of_python sexp = _t_get (_t_of_python sexp) +let python_of_t id = python_of__t (_t_put id) + end include Self -module Set = Ser_cSet.Make(Names.Id.Set)(Self) -module Map = Ser_cMap.Make(Names.Id.Map)(Self) +module Set = Ser_cSet.MakeJP(Names.Id.Set)(Self) +module Map = Ser_cMap.MakeJP(Names.Id.Map)(Self) end @@ -57,7 +61,7 @@ module Name = struct (* Name.t: public *) type t = [%import: Names.Name.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end @@ -67,7 +71,7 @@ module DirPath = struct type t = [%import: Names.DirPath.t] type _t = DirPath of Id.t list - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let _t_put dp = DirPath (DirPath.repr dp) let _t_get (DirPath dpl) = DirPath.make dpl @@ -78,9 +82,12 @@ let sexp_of_t dp = sexp_of__t (_t_put dp) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) +let t_of_python sexp = _t_get (_t_of_python sexp) +let python_of_t dp = python_of__t (_t_put dp) + end -module DPmap = Ser_cMap.Make(DPmap)(DirPath) +module DPmap = Ser_cMap.MakeJP(DPmap)(DirPath) module Label = struct @@ -94,6 +101,9 @@ let sexp_of_t label = Id.sexp_of_t (Label.to_id label) let of_yojson json = Ppx_deriving_yojson_runtime.(Id.of_yojson json >|= Label.of_id) let to_yojson level = Id.to_yojson (Label.to_id level) +let t_of_python python = Label.of_id (Id.t_of_python python) +let python_of_t label = Id.python_of_t (Label.to_id label) + end module MBId = struct @@ -102,7 +112,7 @@ module MBId = struct type t = [%import: Names.MBId.t] type _t = Mbid of int * Id.t * DirPath.t - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let _t_put dp = let i, n, dp = MBId.repr dp in Mbid (i,n,dp) @@ -114,17 +124,20 @@ let sexp_of_t dp = sexp_of__t (_t_put dp) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) +let t_of_python python = _t_get (_t_of_python python) +let python_of_t dp = python_of__t (_t_put dp) + end module ModPath = struct (* ModPath.t: public *) type t = [%import: Names.ModPath.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end -module MPmap = Ser_cMap.Make(MPmap)(ModPath) +module MPmap = Ser_cMap.MakeJP(MPmap)(ModPath) (* KerName: private *) module KerName = struct @@ -132,7 +145,7 @@ module KerName = struct type t = [%import: Names.KerName.t] type _kername = KerName of ModPath.t * Label.t - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let _kername_put kn = let mp, l = KerName.repr kn in KerName (mp,l) @@ -144,6 +157,9 @@ let sexp_of_t kn = sexp_of__kername (_kername_put kn) let of_yojson json = Ppx_deriving_yojson_runtime.(_kername_of_yojson json >|= _kername_get) let to_yojson kn = _kername_to_yojson (_kername_put kn) +let t_of_python python = _kername_get (_kername_of_python python) +let python_of_t dp = python_of__kername (_kername_put dp) + end module Constant = struct @@ -152,7 +168,7 @@ module Constant = struct type t = [%import: Names.Constant.t] type _t = Constant of ModPath.t * Label.t - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let _t_put cs = let mp, l = Constant.repr2 cs in Constant (mp,l) let _t_get (Constant (mp,l)) = Constant.make2 mp l @@ -163,10 +179,13 @@ let sexp_of_t dp = sexp_of__t (_t_put dp) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) +let t_of_python python = _t_get (_t_of_python python) +let python_of_t dp = python_of__t (_t_put dp) + end -module Cmap = Ser_cMap.Make(Cmap)(Constant) -module Cmap_env = Ser_cMap.Make(Cmap_env)(Constant) +module Cmap = Ser_cMap.MakeJP(Cmap)(Constant) +module Cmap_env = Ser_cMap.MakeJP(Cmap_env)(Constant) module MutInd = struct @@ -174,7 +193,7 @@ module MutInd = struct type t = [%import: Names.MutInd.t] type _t = MutInd of ModPath.t * Label.t - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] let _t_put cs = let mp, l = MutInd.repr2 cs in MutInd (mp,l) @@ -186,10 +205,13 @@ let sexp_of_t dp = sexp_of__t (_t_put dp) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) +let t_of_python python = _t_get (_t_of_python python) +let python_of_t dp = python_of__t (_t_put dp) + end -module Mindmap = Ser_cMap.Make(Mindmap)(MutInd) -module Mindmap_env = Ser_cMap.Make(Mindmap_env)(MutInd) +module Mindmap = Ser_cMap.MakeJP(Mindmap)(MutInd) +module Mindmap_env = Ser_cMap.MakeJP(Mindmap_env)(MutInd) type 'a tableKey = [%import: 'a Names.tableKey] @@ -197,28 +219,28 @@ type 'a tableKey = type variable = [%import: Names.variable] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* Inductive and constructor = public *) module Ind = struct type t = [%import: Names.Ind.t] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,python] end type inductive = [%import: Names.inductive] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] module Construct = struct type t = [%import: Names.Construct.t] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,python] end type constructor = [%import: Names.constructor] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,python] (* Projection: private *) module Projection = struct @@ -229,11 +251,11 @@ module Projection = struct proj_npars : int; proj_arg : int; proj_name : Label.t; } - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end type _t = Repr.t * bool - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type t = [%import: Names.Projection.t] @@ -242,12 +264,15 @@ module Projection = struct let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic) let to_yojson level = _t_to_yojson (Obj.magic level) + + let t_of_python se = Obj.magic (_t_of_python se) + let python_of_t dp = python_of__t (Obj.magic dp) end module GlobRef = struct type t = [%import: Names.GlobRef.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end @@ -258,12 +283,12 @@ type evaluable_global_reference = type lident = [%import: Names.lident] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type lname = [%import: Names.lname] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type lstring = [%import: Names.lstring] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_names.mli b/serlib/ser_names.mli index 2a986a58..0d5232fc 100644 --- a/serlib/ser_names.mli +++ b/serlib/ser_names.mli @@ -20,44 +20,74 @@ open Names open Sexplib module Id : sig - include SerType.SJ with type t = Id.t + include SerType.SJP with type t = Id.t - module Set : SerType.S with type t = Id.Set.t - module Map : SerType.S1 with type 'a t = 'a Id.Map.t + module Set : SerType.SJP with type t = Id.Set.t + module Map : SerType.SJP1 with type 'a t = 'a Id.Map.t end -module Name : SerType.SJ with type t = Name.t -module DirPath : SerType.SJ with type t = DirPath.t +module Name : SerType.SJP with type t = Name.t +module DirPath : SerType.SJP with type t = DirPath.t module DPmap : Ser_cMap.ExtS with type key = DirPath.t and type 'a t = 'a DPmap.t -module Label : SerType.SJ with type t = Label.t -module MBId : SerType.SJ with type t = MBId.t -module ModPath : SerType.SJ with type t = ModPath.t -module MPmap : Ser_cMap.ExtS with type key = ModPath.t and type 'a t = 'a MPmap.t +module Label : SerType.SJP with type t = Label.t +module MBId : SerType.SJP with type t = MBId.t +module ModPath : SerType.SJP with type t = ModPath.t +module MPmap : Ser_cMap.ExtSJP with type key = ModPath.t and type 'a t = 'a MPmap.t -module KerName : SerType.SJ with type t = KerName.t -module Constant : SerType.SJ with type t = Constant.t +module KerName : SerType.SJP with type t = KerName.t +module Constant : SerType.SJP with type t = Constant.t -module Cmap : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Cmap.t -module Cmap_env : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Cmap_env.t +module Cmap : Ser_cMap.ExtSJP with type key = Constant.t and type 'a t = 'a Cmap.t +module Cmap_env : Ser_cMap.ExtSJP with type key = Constant.t and type 'a t = 'a Cmap_env.t -module MutInd : SerType.S with type t = MutInd.t +module MutInd : SerType.SJP with type t = MutInd.t -module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap.t -module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Mindmap_env.t +module Mindmap : Ser_cMap.ExtSJP with type key = MutInd.t and type 'a t = 'a Mindmap.t +module Mindmap_env : Ser_cMap.ExtSJP with type key = MutInd.t and type 'a t = 'a Mindmap_env.t type 'a tableKey = 'a Names.tableKey val tableKey_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a tableKey val sexp_of_tableKey : ('a -> Sexp.t) -> 'a tableKey -> Sexp.t +(* -- modularize -- *) type variable = Names.variable + +val variable_of_sexp : Sexp.t -> variable +val sexp_of_variable : variable -> Sexp.t +(* -- end modularize -- *) + +(* -- modularize -- *) type inductive = Names.inductive + +val inductive_of_sexp : Sexp.t -> inductive +val sexp_of_inductive : inductive -> Sexp.t + +val inductive_of_yojson : Yojson.Safe.t -> (inductive, string) Result.result +val inductive_to_yojson : inductive -> Yojson.Safe.t + +val inductive_of_python : Py.Object.t -> inductive +val python_of_inductive : inductive -> Py.Object.t +(* -- end modularize -- *) + +(* -- modularize -- *) type constructor = Names.constructor +val constructor_of_sexp : Sexp.t -> constructor +val sexp_of_constructor : constructor -> Sexp.t + +val constructor_of_yojson : Yojson.Safe.t -> (constructor, string) Result.result +val constructor_to_yojson : constructor -> Yojson.Safe.t + +val constructor_of_python : Py.Object.t -> constructor +val python_of_constructor : constructor -> Py.Object.t + +(* -- end modularize -- *) + module Projection : sig - include SerType.SJ with type t = Projection.t + include SerType.SJP with type t = Projection.t module Repr : sig type t = @@ -69,22 +99,7 @@ module Projection : sig end -module GlobRef : SerType.SJ with type t = Names.GlobRef.t - -val variable_of_sexp : Sexp.t -> variable -val sexp_of_variable : variable -> Sexp.t - -val inductive_of_sexp : Sexp.t -> inductive -val sexp_of_inductive : inductive -> Sexp.t - -val inductive_of_yojson : Yojson.Safe.t -> (inductive, string) Result.result -val inductive_to_yojson : inductive -> Yojson.Safe.t - -val constructor_of_sexp : Sexp.t -> constructor -val sexp_of_constructor : constructor -> Sexp.t - -val constructor_of_yojson : Yojson.Safe.t -> (constructor, string) Result.result -val constructor_to_yojson : constructor -> Yojson.Safe.t +module GlobRef : SerType.SJP with type t = Names.GlobRef.t type evaluable_global_reference = Names.evaluable_global_reference val evaluable_global_reference_of_sexp : Sexp.t -> evaluable_global_reference @@ -95,15 +110,21 @@ val lident_of_sexp : Sexp.t -> lident val sexp_of_lident : lident -> Sexp.t val lident_of_yojson : Yojson.Safe.t -> (lident, string) Result.result val lident_to_yojson : lident -> Yojson.Safe.t +val lident_of_python : Py.Object.t -> lident +val python_of_lident : lident -> Py.Object.t type lname = Names.lname val lname_of_sexp : Sexp.t -> lname val sexp_of_lname : lname -> Sexp.t val lname_of_yojson : Yojson.Safe.t -> (lname, string) Result.result val lname_to_yojson : lname -> Yojson.Safe.t +val lname_of_python : Py.Object.t -> lname +val python_of_lname : lname -> Py.Object.t type lstring = Names.lstring val lstring_of_sexp : Sexp.t -> lstring val sexp_of_lstring : lstring -> Sexp.t val lstring_of_yojson : Yojson.Safe.t -> (lstring, string) Result.result val lstring_to_yojson : lstring -> Yojson.Safe.t +val lstring_of_python : Py.Object.t -> lstring +val python_of_lstring : lstring -> Py.Object.t diff --git a/serlib/ser_nativevalues.ml b/serlib/ser_nativevalues.ml index 780709ee..97327e44 100644 --- a/serlib/ser_nativevalues.ml +++ b/serlib/ser_nativevalues.ml @@ -16,6 +16,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime module Names = Ser_names module Evar = Ser_evar @@ -29,15 +30,15 @@ type t = type tag = [%import: Nativevalues.tag] - [@@deriving sexp] + [@@deriving sexp,python] type arity = [%import: Nativevalues.arity] - [@@deriving sexp] + [@@deriving sexp,python] type reloc_table = [%import: Nativevalues.reloc_table] - [@@deriving sexp] + [@@deriving sexp,python] type annot_sw = [%import: Nativevalues.annot_sw] diff --git a/serlib/ser_notation.ml b/serlib/ser_notation.ml index 7b0885e5..35da2813 100644 --- a/serlib/ser_notation.ml +++ b/serlib/ser_notation.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi (* module Ppextend = Ser_ppextend * module Notation_term = Ser_notation_term *) @@ -22,6 +23,6 @@ module Constrexpr = Ser_constrexpr type level = [%import: Notation.level] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_notation.mli b/serlib/ser_notation.mli index df562d86..cfd5a87f 100644 --- a/serlib/ser_notation.mli +++ b/serlib/ser_notation.mli @@ -18,3 +18,5 @@ open Sexplib type level = Notation.level val level_of_sexp : Sexp.t -> level val sexp_of_level : level -> Sexp.t +val level_of_python : Py.Object.t -> level +val python_of_level : level -> Py.Object.t diff --git a/serlib/ser_notation_gram.ml b/serlib/ser_notation_gram.ml index 9c51d661..b94e2ed8 100644 --- a/serlib/ser_notation_gram.ml +++ b/serlib/ser_notation_gram.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module Names = Ser_names module Constrexpr = Ser_constrexpr @@ -36,12 +37,12 @@ module Notation = Ser_notation type grammar_constr_prod_item = [%import: Notation_gram.grammar_constr_prod_item] - [@@deriving sexp] + [@@deriving sexp,python] type one_notation_grammar = [%import: Notation_gram.one_notation_grammar] - [@@deriving sexp] + [@@deriving sexp,python] type notation_grammar = [%import: Notation_gram.notation_grammar] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_notation_gram.mli b/serlib/ser_notation_gram.mli index a08ad5ab..ca4f3ce2 100644 --- a/serlib/ser_notation_gram.mli +++ b/serlib/ser_notation_gram.mli @@ -37,4 +37,6 @@ val sexp_of_grammar_constr_prod_item : grammar_constr_prod_item -> Sexp.t type notation_grammar = Notation_gram.notation_grammar val notation_grammar_of_sexp : Sexp.t -> notation_grammar val sexp_of_notation_grammar : notation_grammar -> Sexp.t +val notation_grammar_of_python : Py.Object.t -> notation_grammar +val python_of_notation_grammar : notation_grammar -> Py.Object.t diff --git a/serlib/ser_notation_term.ml b/serlib/ser_notation_term.ml index a7f97321..1d5dadf2 100644 --- a/serlib/ser_notation_term.ml +++ b/serlib/ser_notation_term.ml @@ -43,7 +43,7 @@ type subscopes = type constr_as_binder_kind = [%import: Notation_term.constr_as_binder_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type notation_var_internalization_type = [%import: Notation_term.notation_var_internalization_type] diff --git a/serlib/ser_notation_term.mli b/serlib/ser_notation_term.mli index 8dcae23d..96a71890 100644 --- a/serlib/ser_notation_term.mli +++ b/serlib/ser_notation_term.mli @@ -24,6 +24,8 @@ val constr_as_binder_kind_of_sexp : Sexp.t -> constr_as_binder_kind val sexp_of_constr_as_binder_kind : constr_as_binder_kind -> Sexp.t val constr_as_binder_kind_of_yojson : Yojson.Safe.t -> (constr_as_binder_kind, string) Result.result val constr_as_binder_kind_to_yojson : constr_as_binder_kind -> Yojson.Safe.t +val constr_as_binder_kind_of_python : Py.Object.t -> constr_as_binder_kind +val python_of_constr_as_binder_kind : constr_as_binder_kind -> Py.Object.t type notation_var_internalization_type = Notation_term.notation_var_internalization_type val notation_var_internalization_type_of_sexp : Sexp.t -> notation_var_internalization_type diff --git a/serlib/ser_numTok.ml b/serlib/ser_numTok.ml index 2e1bcc49..46f611fe 100644 --- a/serlib/ser_numTok.ml +++ b/serlib/ser_numTok.ml @@ -14,18 +14,19 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi type sign = [%import: NumTok.sign] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type num_class = [%import: NumTok.num_class] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a exp = [%import: 'a NumTok.exp] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] module Unsigned = struct @@ -33,13 +34,15 @@ module Unsigned = struct int : string; frac : string; exp : string - } [@@deriving sexp,yojson] + } [@@deriving sexp,yojson,python] type t = NumTok.Unsigned.t let t_of_sexp s = Obj.magic (_t_of_sexp s) let sexp_of_t s = sexp_of__t (Obj.magic s) let of_yojson s = Obj.magic (_t_of_yojson s) let to_yojson s = _t_to_yojson (Obj.magic s) + let t_of_python s = Obj.magic (_t_of_python s) + let python_of_t s = python_of__t (Obj.magic s) end @@ -47,6 +50,6 @@ module Signed = struct type t = [%import: NumTok.Signed.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end diff --git a/serlib/ser_opaqueproof.ml b/serlib/ser_opaqueproof.ml index 5db1b60e..6c51895d 100644 --- a/serlib/ser_opaqueproof.ml +++ b/serlib/ser_opaqueproof.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module Future = Ser_future module Names = Ser_names @@ -22,35 +23,39 @@ module Constr = Ser_constr module Mod_subst = Ser_mod_subst type proofterm = (Constr.constr * Univ.ContextSet.t) Future.computation - [@@deriving sexp] + [@@deriving sexp,python] type work_list = [%import: Opaqueproof.work_list] - [@@deriving sexp] + [@@deriving sexp,python] type cooking_info = [%import: Opaqueproof.cooking_info] - [@@deriving sexp] + [@@deriving sexp,python] type _opaque = | Indirect of Mod_subst.substitution list * cooking_info list * Names.DirPath.t * int (* subst, discharge, lib, index *) - [@@deriving sexp] + [@@deriving sexp,python] type opaque = [%import: Opaqueproof.opaque] let sexp_of_opaque x = sexp_of__opaque (Obj.magic x) let opaque_of_sexp x = Obj.magic (_opaque_of_sexp x) +let python_of_opaque x = python_of__opaque (Obj.magic x) +let opaque_of_python x = Obj.magic (_opaque_of_python x) -module Map = Ser_cMap.Make(Int.Map)(Ser_int) +module Map = Ser_cMap.MakeJP(Int.Map)(Ser_int) type _opaquetab = { opaque_val : proofterm Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) opaque_dir : Names.DirPath.t; -} [@@deriving sexp] +} [@@deriving sexp,python] type opaquetab = [%import: Opaqueproof.opaquetab] let sexp_of_opaquetab x = sexp_of__opaquetab (Obj.magic x) let opaquetab_of_sexp x = Obj.magic (_opaquetab_of_sexp x) +let python_of_opaquetab x = python_of__opaquetab (Obj.magic x) +let opaquetab_of_python x = Obj.magic (_opaquetab_of_python x) diff --git a/serlib/ser_opaqueproof.mli b/serlib/ser_opaqueproof.mli index dff146d2..2f130d37 100644 --- a/serlib/ser_opaqueproof.mli +++ b/serlib/ser_opaqueproof.mli @@ -26,7 +26,11 @@ val cooking_info_of_sexp : Sexp.t -> cooking_info type opaque = Opaqueproof.opaque val sexp_of_opaque : opaque -> Sexp.t val opaque_of_sexp : Sexp.t -> opaque +val python_of_opaque : opaque -> Py.Object.t +val opaque_of_python : Py.Object.t -> opaque type opaquetab = Opaqueproof.opaquetab val sexp_of_opaquetab : opaquetab -> Sexp.t val opaquetab_of_sexp : Sexp.t -> opaquetab +val python_of_opaquetab : opaquetab -> Py.Object.t +val opaquetab_of_python : Py.Object.t -> opaquetab diff --git a/serlib/ser_pattern.ml b/serlib/ser_pattern.ml index a2f5a998..882e2841 100644 --- a/serlib/ser_pattern.ml +++ b/serlib/ser_pattern.ml @@ -26,7 +26,7 @@ module Glob_term = Ser_glob_term type patvar = [%import: Pattern.patvar] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type case_info_pattern = [%import: Pattern.case_info_pattern] diff --git a/serlib/ser_pattern.mli b/serlib/ser_pattern.mli index b72fe5d5..fffbef60 100644 --- a/serlib/ser_pattern.mli +++ b/serlib/ser_pattern.mli @@ -21,6 +21,8 @@ val patvar_of_sexp : Sexp.t -> patvar val sexp_of_patvar : patvar -> Sexp.t val patvar_of_yojson : Yojson.Safe.t -> (patvar, string) Result.result val patvar_to_yojson : patvar -> Yojson.Safe.t +val patvar_of_python : Py.Object.t -> patvar +val python_of_patvar : patvar -> Py.Object.t type case_info_pattern = Pattern.case_info_pattern diff --git a/serlib/ser_pp.ml b/serlib/ser_pp.ml index 9078a176..7e612af0 100644 --- a/serlib/ser_pp.ml +++ b/serlib/ser_pp.ml @@ -14,14 +14,15 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime type pp_tag = [%import: Pp.pp_tag] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type block_type = [%import: Pp.block_type] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] module P = struct type _t = @@ -34,7 +35,7 @@ module P = struct | Pp_print_break of int * int | Pp_force_newline | Pp_comment of string list - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] open Pp @@ -67,6 +68,9 @@ let sexp_of_t d = P.(sexp_of__t (from_t d)) let of_yojson json = Ppx_deriving_yojson_runtime.(P.(_t_of_yojson json >|= to_t)) let to_yojson level = P.(_t_to_yojson (from_t level)) +let t_of_python s = P.(to_t (_t_of_python s)) +let python_of_t d = P.(python_of__t (from_t d)) + type doc_view = [%import: Pp.doc_view] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] diff --git a/serlib/ser_pp.mli b/serlib/ser_pp.mli index cf9073af..31cd83ee 100644 --- a/serlib/ser_pp.mli +++ b/serlib/ser_pp.mli @@ -22,8 +22,12 @@ val t_of_sexp : Sexp.t -> t val sexp_of_t : t -> Sexp.t val of_yojson : Yojson.Safe.t -> (t, string) Result.result val to_yojson : t -> Yojson.Safe.t +val t_of_python : Py.Object.t -> t +val python_of_t : t -> Py.Object.t val doc_view_of_sexp : Sexp.t -> doc_view val sexp_of_doc_view : doc_view -> Sexp.t val doc_view_of_yojson : Yojson.Safe.t -> (doc_view, string) Result.result val doc_view_to_yojson : doc_view -> Yojson.Safe.t +val doc_view_of_python : Py.Object.t -> doc_view +val python_of_doc_view : doc_view -> Py.Object.t diff --git a/serlib/ser_ppextend.ml b/serlib/ser_ppextend.ml index ae154e3e..e2dce4bf 100644 --- a/serlib/ser_ppextend.ml +++ b/serlib/ser_ppextend.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi module Loc = Ser_loc module Notation_term = Ser_notation_term @@ -23,24 +24,24 @@ module Extend = Ser_extend type ppbox = [%import: Ppextend.ppbox] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,python] type ppcut = [%import: Ppextend.ppcut] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,python] type pattern_quote_style = [%import: Ppextend.pattern_quote_style] - [@@deriving sexp, yojson] + [@@deriving sexp,yojson,python] type unparsing = [%import: Ppextend.unparsing] - [@@deriving sexp] + [@@deriving sexp,python] type unparsing_rule = [%import: Ppextend.unparsing_rule] - [@@deriving sexp] + [@@deriving sexp,python] type extra_unparsing_rules = [%import: Ppextend.extra_unparsing_rules] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_ppextend.mli b/serlib/ser_ppextend.mli index 482be919..b67b69df 100644 --- a/serlib/ser_ppextend.mli +++ b/serlib/ser_ppextend.mli @@ -32,7 +32,11 @@ val sexp_of_ppcut : ppcut -> Sexp.t type unparsing_rule = Ppextend.unparsing_rule val unparsing_rule_of_sexp : Sexp.t -> unparsing_rule val sexp_of_unparsing_rule : unparsing_rule -> Sexp.t +val unparsing_rule_of_python : Py.Object.t -> unparsing_rule +val python_of_unparsing_rule : unparsing_rule -> Py.Object.t type extra_unparsing_rules = Ppextend.extra_unparsing_rules val extra_unparsing_rules_of_sexp : Sexp.t -> extra_unparsing_rules val sexp_of_extra_unparsing_rules : extra_unparsing_rules -> Sexp.t +val extra_unparsing_rules_of_python : Py.Object.t -> extra_unparsing_rules +val python_of_extra_unparsing_rules : extra_unparsing_rules -> Py.Object.t diff --git a/serlib/ser_printer.ml b/serlib/ser_printer.ml index 0c1ab9cc..d4ecaf11 100644 --- a/serlib/ser_printer.ml +++ b/serlib/ser_printer.ml @@ -19,4 +19,4 @@ module Names = Ser_names type axiom = [%import: Printer.axiom] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_proof_bullet.ml b/serlib/ser_proof_bullet.ml index 35d5c110..dcc41ab3 100644 --- a/serlib/ser_proof_bullet.ml +++ b/serlib/ser_proof_bullet.ml @@ -16,7 +16,8 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi type t = [%import: Proof_bullet.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_range.ml b/serlib/ser_range.ml index 60ab0986..d9614e2d 100644 --- a/serlib/ser_range.ml +++ b/serlib/ser_range.ml @@ -16,3 +16,5 @@ type 'a t = 'a Range.t let sexp_of_t _ = Serlib_base.sexp_of_opaque ~typ:"Range.t" let t_of_sexp _ = Serlib_base.opaque_of_sexp ~typ:"Range.t" +let python_of_t _ = Serlib_base.python_of_opaque ~typ:"Range.t" +let t_of_python _ = Serlib_base.opaque_of_python ~typ:"Range.t" diff --git a/serlib/ser_retroknowledge.ml b/serlib/ser_retroknowledge.ml index da7a3043..d0a63add 100644 --- a/serlib/ser_retroknowledge.ml +++ b/serlib/ser_retroknowledge.ml @@ -18,6 +18,8 @@ type retroknowledge = let sexp_of_retroknowledge = Serlib_base.sexp_of_opaque ~typ:"Retroknowledge.retroknowledge" let retroknowledge_of_sexp = Serlib_base.opaque_of_sexp ~typ:"Retroknowledge.retroknowledge" +let python_of_retroknowledge = Serlib_base.python_of_opaque ~typ:"Retroknowledge.retroknowledge" +let retroknowledge_of_python = Serlib_base.opaque_of_python ~typ:"Retroknowledge.retroknowledge" (* type entry = * [%import: Retroknowledge.entry] *) diff --git a/serlib/ser_retroknowledge.mli b/serlib/ser_retroknowledge.mli index d0f515cb..84e2391f 100644 --- a/serlib/ser_retroknowledge.mli +++ b/serlib/ser_retroknowledge.mli @@ -18,8 +18,10 @@ type retroknowledge = Retroknowledge.retroknowledge val sexp_of_retroknowledge : retroknowledge -> Sexp.t val retroknowledge_of_sexp : Sexp.t -> retroknowledge +val python_of_retroknowledge : retroknowledge -> Py.Object.t +val retroknowledge_of_python : Py.Object.t -> retroknowledge type action = Retroknowledge.action val sexp_of_action : action -> Sexp.t -val action_of_sexp : Sexp.t -> action \ No newline at end of file +val action_of_sexp : Sexp.t -> action diff --git a/serlib/ser_rtree.ml b/serlib/ser_rtree.ml index 7352c2ad..a945f20a 100644 --- a/serlib/ser_rtree.ml +++ b/serlib/ser_rtree.ml @@ -15,14 +15,18 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime type 'a _t = Param of int * int | Node of 'a * 'a _t array | Rec of int * 'a _t array -[@@deriving sexp] +[@@deriving sexp,python] type 'a t = 'a Rtree.t let sexp_of_t f r = sexp_of__t f (Obj.magic r) let t_of_sexp f r = Obj.magic (_t_of_sexp f r) + +let python_of_t f r = python_of__t f (Obj.magic r) +let t_of_python f r = Obj.magic (_t_of_python f r) diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml index 08a95e7b..66f54c1b 100644 --- a/serlib/ser_sorts.ml +++ b/serlib/ser_sorts.ml @@ -17,22 +17,23 @@ module Univ = Ser_univ type family = [%import: Sorts.family] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type _t = | SProp | Prop | Set | Type of Univ.Universe.t - [@@deriving of_sexp,yojson] + [@@deriving sexp,yojson,python] type t = [%import: Sorts.t] - [@@deriving sexp_of,to_yojson] + [@@deriving sexp_of,to_yojson,python_of] let t_of_sexp x = Obj.magic (_t_of_sexp x) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic) +let t_of_python x = Obj.magic (_t_of_python x) type relevance = [%import: Sorts.relevance] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_sorts.mli b/serlib/ser_sorts.mli index 47b81a27..33e361cb 100644 --- a/serlib/ser_sorts.mli +++ b/serlib/ser_sorts.mli @@ -22,10 +22,15 @@ val sexp_of_family : family -> Sexp.t val family_of_yojson : Yojson.Safe.t -> (family, string) Result.result val family_to_yojson : family -> Yojson.Safe.t -include SerType.SJ with type t = Sorts.t +val family_of_python : Py.Object.t -> family +val python_of_family : family -> Py.Object.t + +include SerType.SJP with type t = Sorts.t type relevance = Sorts.relevance val relevance_of_sexp : Sexp.t -> relevance val sexp_of_relevance : relevance -> Sexp.t val relevance_of_yojson : Yojson.Safe.t -> (relevance, string) Result.result val relevance_to_yojson : relevance -> Yojson.Safe.t +val relevance_of_python : Py.Object.t -> relevance +val python_of_relevance : relevance -> Py.Object.t diff --git a/serlib/ser_stateid.ml b/serlib/ser_stateid.ml index c50f004e..a0fc906d 100644 --- a/serlib/ser_stateid.ml +++ b/serlib/ser_stateid.ml @@ -14,13 +14,12 @@ (************************************************************************) open Sexplib.Std - -module Self = struct +open Ppx_python_runtime type t = [%import: Stateid.t] -type _t = int [@@deriving sexp, yojson] +type _t = int [@@deriving sexp, yojson, python] let _t_put stateid = (Stateid.to_int stateid) let _t_get stateid = Stateid.of_int stateid @@ -30,6 +29,6 @@ let sexp_of_t stateid = sexp_of__t (_t_put stateid) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) -end -include Self +let t_of_python python = _t_get (_t_of_python python) +let python_of_t stateid = python_of__t (_t_put stateid) diff --git a/serlib/ser_stateid.mli b/serlib/ser_stateid.mli index baaf010f..eb5c3401 100644 --- a/serlib/ser_stateid.mli +++ b/serlib/ser_stateid.mli @@ -13,6 +13,4 @@ (* Status: Very Experimental *) (************************************************************************) -module Self : SerType.SJ with type t = Stateid.t - -include module type of Self +include SerType.SJP with type t = Stateid.t diff --git a/serlib/ser_stdlib.ml b/serlib/ser_stdlib.ml index fdb17208..73643f77 100644 --- a/serlib/ser_stdlib.ml +++ b/serlib/ser_stdlib.ml @@ -20,6 +20,11 @@ type nonrec 'a ref = 'a ref let ref_of_sexp = ref_of_sexp let sexp_of_ref = sexp_of_ref +let python_of_ref f (x : 'a ref) = + match x with | { contents } -> f contents + +let ref_of_python f x = ref (f x) + module Lazy = struct type 'a t = 'a lazy_t [@@deriving sexp] diff --git a/serlib/ser_stm.ml b/serlib/ser_stm.ml index f85fe70a..44b1e319 100644 --- a/serlib/ser_stm.ml +++ b/serlib/ser_stm.ml @@ -14,17 +14,18 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module Stateid = Ser_stateid module Names = Ser_names type interactive_top = [%import: Stm.interactive_top] - [@@deriving sexp] + [@@deriving sexp,python] type focus = [%import: Stm.focus] - [@@deriving sexp] + [@@deriving sexp,python] (* { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } *) diff --git a/serlib/ser_stm.mli b/serlib/ser_stm.mli index 5358092a..6ff80e78 100644 --- a/serlib/ser_stm.mli +++ b/serlib/ser_stm.mli @@ -19,6 +19,8 @@ type interactive_top = Stm.interactive_top val sexp_of_interactive_top : Stm.interactive_top -> Sexp.t val interactive_top_of_sexp : Sexp.t -> Stm.interactive_top +val python_of_interactive_top : Stm.interactive_top -> Py.Object.t +val interactive_top_of_python : Py.Object.t -> Stm.interactive_top type focus = Stm.focus diff --git a/serlib/ser_tok.ml b/serlib/ser_tok.ml index 9c859208..1ccff409 100644 --- a/serlib/ser_tok.ml +++ b/serlib/ser_tok.ml @@ -14,12 +14,13 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime -module NumTok = Ser_numTok +module NumTok = Ser_numTok type t = [%import: Tok.t] - [@@deriving sexp] + [@@deriving sexp,yojson,python] type 'c p = [%import: 'c Tok.p] @@ -37,6 +38,9 @@ type 'c _p = | PBULLET of string option | PQUOTATION of string | PEOI - [@@deriving of_sexp] + [@@deriving of_sexp,python] let p_of_sexp f x = Obj.magic (_p_of_sexp f x) + +let p_of_python f x = Obj.magic (_p_of_python f x) +let python_of_p f x = python_of__p f (Obj.magic x) diff --git a/serlib/ser_tok.mli b/serlib/ser_tok.mli index b584293c..e07a456d 100644 --- a/serlib/ser_tok.mli +++ b/serlib/ser_tok.mli @@ -15,7 +15,7 @@ open Sexplib -type t = Tok.t +include SerType.SJP with type t = Tok.t val t_of_sexp : Sexp.t -> t val sexp_of_t : t -> Sexp.t @@ -23,3 +23,6 @@ val sexp_of_t : t -> Sexp.t type 'c p = 'c Tok.p val p_of_sexp : (Sexp.t -> 'c) -> Sexp.t -> 'c p val sexp_of_p : ('c -> Sexp.t) -> 'c p -> Sexp.t + +val p_of_python : (Py.Object.t -> 'c) -> Py.Object.t -> 'c p +val python_of_p : ('c -> Py.Object.t) -> 'c p -> Py.Object.t diff --git a/serlib/ser_typeclasses.ml b/serlib/ser_typeclasses.ml index e9e50717..22b14703 100644 --- a/serlib/ser_typeclasses.ml +++ b/serlib/ser_typeclasses.ml @@ -16,7 +16,8 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi type 'a hint_info_gen = [%import: 'a Typeclasses.hint_info_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_typeclasses.mli b/serlib/ser_typeclasses.mli index 3d6ac7b5..b988b458 100644 --- a/serlib/ser_typeclasses.mli +++ b/serlib/ser_typeclasses.mli @@ -23,3 +23,5 @@ val sexp_of_hint_info_gen : ('a -> Sexp.t) -> 'a hint_info_gen -> Sexp.t val hint_info_gen_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a hint_info_gen val hint_info_gen_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a hint_info_gen, string) Result.result val hint_info_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a hint_info_gen -> Yojson.Safe.t +val python_of_hint_info_gen : ('a -> Py.Object.t) -> 'a hint_info_gen -> Py.Object.t +val hint_info_gen_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a hint_info_gen diff --git a/serlib/ser_uGraph.ml b/serlib/ser_uGraph.ml index a326d49e..fc40ad43 100644 --- a/serlib/ser_uGraph.ml +++ b/serlib/ser_uGraph.ml @@ -15,10 +15,13 @@ module Bound = struct type t = [%import: UGraph.Bound.t] - [@@deriving sexp] + [@@deriving sexp,python] end type t = [%import: UGraph.t] let sexp_of_t = Serlib_base.sexp_of_opaque ~typ:"UGraph.t" let t_of_sexp = Serlib_base.opaque_of_sexp ~typ:"UGraph.t" +let python_of_t = Serlib_base.python_of_opaque ~typ:"UGraph.t" +let t_of_python = Serlib_base.opaque_of_python ~typ:"UGraph.t" + diff --git a/serlib/ser_uGraph.mli b/serlib/ser_uGraph.mli index de40f0d5..d4c16c14 100644 --- a/serlib/ser_uGraph.mli +++ b/serlib/ser_uGraph.mli @@ -15,14 +15,19 @@ open Sexplib +(* Use utils PJ *) module Bound : sig type t = UGraph.Bound.t val sexp_of_t : t -> Sexp.t val t_of_sexp : Sexp.t -> t + val python_of_t : t -> Py.Object.t + val t_of_python : Py.Object.t -> t end type t = UGraph.t val sexp_of_t : t -> Sexp.t val t_of_sexp : Sexp.t -> t +val python_of_t : t -> Py.Object.t +val t_of_python : Py.Object.t -> t diff --git a/serlib/ser_uState.ml b/serlib/ser_uState.ml index 47af040c..e6ac9bb6 100644 --- a/serlib/ser_uState.ml +++ b/serlib/ser_uState.ml @@ -14,7 +14,8 @@ (************************************************************************) open Sexplib.Std +open Ppx_python_runtime_serapi type ('a,'b) gen_universe_decl = [%import: ('a,'b) UState.gen_universe_decl] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_uint63.ml b/serlib/ser_uint63.ml index 8cf8aef8..07fdd6b1 100644 --- a/serlib/ser_uint63.ml +++ b/serlib/ser_uint63.ml @@ -15,8 +15,9 @@ (************************************************************************) open Sexplib +open Ppx_python_runtime -type _t = string [@@deriving yojson] +type _t = string [@@deriving yojson,python] let _t_put = Uint63.to_string let _t_get x = Uint63.of_int64 (Int64.of_string x) @@ -27,3 +28,6 @@ let sexp_of_t (x : Uint63.t) : Sexp.t = Conv.sexp_of_string (_t_put x) let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _t_get) let to_yojson level = _t_to_yojson (_t_put level) + +let t_of_python (x : Py.Object.t) : Uint63.t = _t_get (_t_of_python x) +let python_of_t (x : Uint63.t) : Py.Object.t = python_of__t (_t_put x) diff --git a/serlib/ser_univ.ml b/serlib/ser_univ.ml index 84bd6f8a..92b87033 100644 --- a/serlib/ser_univ.ml +++ b/serlib/ser_univ.ml @@ -15,6 +15,7 @@ open Sexplib open Sexplib.Conv +open Ppx_python_runtime module Stdlib = Ser_stdlib module Names = Ser_names @@ -23,7 +24,7 @@ module RawLevel = struct module UGlobal = struct type t = Names.DirPath.t * int - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] end type t = @@ -32,37 +33,41 @@ module RawLevel = struct | Set | Level of UGlobal.t | Var of int - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] end module Level = struct + open Base type _t = { hash : int ; data : RawLevel.t } - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type t = Univ.Level.t - let t_of_sexp sexp = Obj.magic (_t_of_sexp sexp) - let sexp_of_t level = sexp_of__t (Obj.magic level) + let t_of_sexp sexp = Caml.Obj.magic (_t_of_sexp sexp) + let sexp_of_t level = sexp_of__t (Caml.Obj.magic level) let of_yojson json = - Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic) - let to_yojson level = _t_to_yojson (Obj.magic level) + Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Caml.Obj.magic) + let to_yojson level = _t_to_yojson (Caml.Obj.magic level) + + let t_of_python python = Caml.Obj.magic (_t_of_python python) + let python_of_t level = python_of__t (Caml.Obj.magic level) end -module LSet = Ser_cSet.MakeJ(Univ.LSet)(Level) +module LSet = Ser_cSet.MakeJP(Univ.LSet)(Level) (* XXX: Think what to do with this *) module Universe = struct type t = [%import: Univ.Universe.t] type _t = (Level.t * int) list - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] let t_of_sexp sexp = Obj.magic (_t_of_sexp sexp) let sexp_of_t universe = sexp_of__t (Obj.magic universe) @@ -70,6 +75,9 @@ module Universe = struct let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic) let to_yojson level = _t_to_yojson (Obj.magic level) + + let t_of_python python = Obj.magic (_t_of_python python) + let python_of_t universe = python_of__t (Obj.magic universe) end (*************************************************************************) @@ -78,7 +86,7 @@ module Variance = struct type t = [%import: Univ.Variance.t] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] end @@ -88,7 +96,7 @@ type t = [%import: Univ.Instance.t] type _t = Instance of Level.t array - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] let _instance_put instance = Instance (Univ.Instance.to_array instance) let _instance_get (Instance instance) = Univ.Instance.of_array instance @@ -100,26 +108,31 @@ let of_yojson json = Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _instance_get) let to_yojson level = _t_to_yojson (_instance_put level) +let t_of_python python = _instance_get (_t_of_python python) +let python_of_t instance = python_of__t (_instance_put instance) + end type constraint_type = [%import: Univ.constraint_type] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson,python] type univ_constraint = [%import: Univ.univ_constraint] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson,python] -module Constraint = Ser_cSet.MakeJ(Univ.Constraint)(struct +module Constraint = Ser_cSet.MakeJP(Univ.Constraint)(struct let t_of_sexp = univ_constraint_of_sexp let sexp_of_t = sexp_of_univ_constraint let of_yojson = univ_constraint_of_yojson let to_yojson = univ_constraint_to_yojson + let t_of_python = univ_constraint_of_python + let python_of_t = python_of_univ_constraint end) type 'a constrained = [%import: 'a Univ.constrained] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] module UContext = struct @@ -133,19 +146,26 @@ end module AUContext = struct type _t = Names.Name.t array constrained - [@@deriving sexp] + [@@deriving sexp,yojson,python] type t = Univ.AUContext.t (* XXX: Opaque, so check they are the same *) let t_of_sexp x = Obj.magic (_t_of_sexp x) let sexp_of_t c = sexp_of__t (Obj.magic c) + let of_yojson json = + Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic) + let to_yojson level = _t_to_yojson (Obj.magic level) + + let t_of_python x = Obj.magic (_t_of_python x) + let python_of_t c = python_of__t (Obj.magic c) + end module ContextSet = struct type t = [%import: Univ.ContextSet.t] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] end type 'a in_universe_context = @@ -158,7 +178,7 @@ type 'a in_universe_context_set = type 'a puniverses = [%import: 'a Univ.puniverses] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type explanation = [%import: Univ.explanation] diff --git a/serlib/ser_univ.mli b/serlib/ser_univ.mli index 6a8900f3..21169235 100644 --- a/serlib/ser_univ.mli +++ b/serlib/ser_univ.mli @@ -15,11 +15,11 @@ open Sexplib -module Level : SerType.SJ with type t = Univ.Level.t -module Universe : SerType.SJ with type t = Univ.Universe.t +module Level : SerType.SJP with type t = Univ.Level.t +module Universe : SerType.SJP with type t = Univ.Universe.t -module Variance : SerType.SJ with type t = Univ.Variance.t -module Instance : SerType.SJ with type t = Univ.Instance.t +module Variance : SerType.SJP with type t = Univ.Variance.t +module Instance : SerType.SJP with type t = Univ.Instance.t type constraint_type = Univ.constraint_type @@ -27,6 +27,8 @@ val constraint_type_of_sexp : Sexp.t -> constraint_type val sexp_of_constraint_type : constraint_type -> Sexp.t val constraint_type_of_yojson : Yojson.Safe.t -> (constraint_type, string) Result.result val constraint_type_to_yojson : constraint_type -> Yojson.Safe.t +val constraint_type_of_python : Py.Object.t -> constraint_type +val python_of_constraint_type : constraint_type -> Py.Object.t type univ_constraint = Univ.univ_constraint @@ -35,10 +37,8 @@ val sexp_of_univ_constraint : univ_constraint -> Sexp.t module Constraint : SerType.SJ with type t = Univ.Constraint.t module UContext : SerType.S with type t = Univ.UContext.t - -module AUContext : SerType.S with type t = Univ.AUContext.t - -module ContextSet : SerType.SJ with type t = Univ.ContextSet.t +module AUContext : SerType.SJP with type t = Univ.AUContext.t +module ContextSet : SerType.SJP with type t = Univ.ContextSet.t (** A value in a universe context (resp. context set). *) type 'a in_universe_context = 'a Univ.in_universe_context @@ -57,6 +57,9 @@ val sexp_of_puniverses : ('a -> Sexp.t) -> 'a puniverses -> Sexp.t val puniverses_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> Yojson.Safe.t -> ('a puniverses, string) Result.result val puniverses_to_yojson : ('a -> Yojson.Safe.t) -> 'a puniverses -> Yojson.Safe.t +val puniverses_of_python : (Py.Object.t -> 'a) -> Py.Object.t -> 'a puniverses +val python_of_puniverses : ('a -> Py.Object.t) -> 'a puniverses -> Py.Object.t + type explanation = Univ.explanation val explanation_of_sexp : Sexp.t -> explanation diff --git a/serlib/ser_univNames.ml b/serlib/ser_univNames.ml index ae7aab69..b35b31d2 100644 --- a/serlib/ser_univNames.ml +++ b/serlib/ser_univNames.ml @@ -14,9 +14,10 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module Names = Ser_names type univ_name_list = [%import: UnivNames.univ_name_list] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_util.ml b/serlib/ser_util.ml index addd45da..a461b67f 100644 --- a/serlib/ser_util.ml +++ b/serlib/ser_util.ml @@ -15,4 +15,4 @@ type ('a,'b) union = [%import: ('a,'b) Util.union] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] diff --git a/serlib/ser_util.mli b/serlib/ser_util.mli index 52061610..e8c412e9 100644 --- a/serlib/ser_util.mli +++ b/serlib/ser_util.mli @@ -21,3 +21,5 @@ val union_of_sexp : (Sexp.t -> 'a) -> (Sexp.t -> 'b) -> Sexp.t -> ('a, 'b) union val sexp_of_union : ('a -> Sexp.t) -> ('b -> Sexp.t) -> ('a, 'b) union -> Sexp.t val union_of_yojson : (Yojson.Safe.t -> ('a, string) Result.result) -> (Yojson.Safe.t -> ('b, string) Result.result) -> Yojson.Safe.t -> (('a, 'b) union, string) Result.result val union_to_yojson : ('a -> Yojson.Safe.t) -> ('b -> Yojson.Safe.t) -> ('a,'b) union -> Yojson.Safe.t +val union_of_python : (Py.Object.t -> 'a) -> (Py.Object.t -> 'b) -> Py.Object.t -> ('a, 'b) union +val python_of_union : ('a -> Py.Object.t) -> ('b -> Py.Object.t) -> ('a, 'b) union -> Py.Object.t diff --git a/serlib/ser_vernacexpr.ml b/serlib/ser_vernacexpr.ml index c8e2f929..2dd228e2 100644 --- a/serlib/ser_vernacexpr.ml +++ b/serlib/ser_vernacexpr.ml @@ -14,6 +14,7 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime_serapi module CUnix = Ser_cUnix module Loc = Ser_loc @@ -47,72 +48,72 @@ module Impargs = Ser_impargs module Typeclasses = Ser_typeclasses type class_rawexpr = [%import: Vernacexpr.class_rawexpr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type goal_identifier = [%import: Vernacexpr.goal_identifier] [@@deriving sexp] type scope_name = [%import: Vernacexpr.scope_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type goal_reference = [%import: Vernacexpr.goal_reference] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type printable = [%import: Vernacexpr.printable] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type vernac_cumulative = * [%import: Vernacexpr.vernac_cumulative] - * [@@deriving sexp,yojson] *) + * [@@deriving sexp,yojson,python] *) type glob_search_where = [%import: Vernacexpr.glob_search_where] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type search_item = [%import: Vernacexpr.search_item] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type search_request = [%import: Vernacexpr.search_request] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type searchable = [%import: Vernacexpr.searchable] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type locatable = [%import: Vernacexpr.locatable] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type showable = [%import: Vernacexpr.showable] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type comment = [%import: Vernacexpr.comment] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type search_restriction = [%import: Vernacexpr.search_restriction] - [@@deriving sexp,yojson] - -(* type rec_flag = [%import: Vernacexpr.rec_flag ] [@@deriving sexp,yojson] *) -type verbose_flag = [%import: Vernacexpr.verbose_flag ] [@@deriving sexp,yojson] -type coercion_flag = [%import: Vernacexpr.coercion_flag ] [@@deriving sexp,yojson] -(* type inductive_flag = [%import: Vernacexpr.inductive_flag ] [@@deriving sexp,yojson] *) -type instance_flag = [%import: Vernacexpr.instance_flag ] [@@deriving sexp,yojson] -type export_flag = [%import: Vernacexpr.export_flag ] [@@deriving sexp,yojson] -type onlyparsing_flag = [%import: Vernacexpr.onlyparsing_flag ] [@@deriving sexp,yojson] -type locality_flag = [%import: Vernacexpr.locality_flag ] [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] + +(* type rec_flag = [%import: Vernacexpr.rec_flag ] [@@deriving sexp,yojson,python] *) +type verbose_flag = [%import: Vernacexpr.verbose_flag ] [@@deriving sexp,yojson,python] +type coercion_flag = [%import: Vernacexpr.coercion_flag ] [@@deriving sexp,yojson,python] +(* type inductive_flag = [%import: Vernacexpr.inductive_flag ] [@@deriving sexp,yojson,python] *) +type instance_flag = [%import: Vernacexpr.instance_flag ] [@@deriving sexp,yojson,python] +type export_flag = [%import: Vernacexpr.export_flag ] [@@deriving sexp,yojson,python] +type onlyparsing_flag = [%import: Vernacexpr.onlyparsing_flag ] [@@deriving sexp,yojson,python] +type locality_flag = [%import: Vernacexpr.locality_flag ] [@@deriving sexp,yojson,python] (* type obsolete_locality = [%import: Vernacexpr.obsolete_locality ] [@@deriving sexp] *) type option_setting = [%import: Vernacexpr.option_setting] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type option_ref_value = * [%import: Vernacexpr.option_ref_value] - * [@@deriving sexp,yojson] *) + * [@@deriving sexp,yojson,python] *) (* type plident = * [%import: Vernacexpr.plident ] @@ -124,172 +125,217 @@ type option_setting = type definition_expr = [%import: Vernacexpr.definition_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type syntax_modifier = [%import: Vernacexpr.syntax_modifier] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type decl_notation = [%import: Vernacexpr.decl_notation] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a fix_expr_gen = [%import: 'a Vernacexpr.fix_expr_gen] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type fixpoint_expr = [%import: Vernacexpr.fixpoint_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type cofixpoint_expr = [%import: Vernacexpr.cofixpoint_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type local_decl_expr = [%import: Vernacexpr.local_decl_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type inductive_kind = [%import: Vernacexpr.inductive_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type simple_binder = [%import: Vernacexpr.simple_binder] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type class_binder = [%import: Vernacexpr.class_binder] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type 'a with_coercion = [%import: 'a Vernacexpr.with_coercion] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] (* type 'a with_instance = * [%import: 'a Vernacexpr.with_instance] - * [@@deriving sexp,yojson] *) + * [@@deriving sexp,yojson,python] *) (* type 'a with_notation = * [%import: 'a Vernacexpr.with_notation] - * [@@deriving sexp,yojson] *) + * [@@deriving sexp,yojson,python] *) (* type 'a with_priority = * [%import: 'a Vernacexpr.with_priority] - * [@@deriving sexp,yojson] *) + * [@@deriving sexp,yojson,python] *) type constructor_expr = [%import: Vernacexpr.constructor_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type record_field_attr = [%import: Vernacexpr.record_field_attr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type constructor_list_or_record_decl_expr = [%import: Vernacexpr.constructor_list_or_record_decl_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type inductive_params_expr = [%import: Vernacexpr.inductive_params_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type inductive_expr = [%import: Vernacexpr.inductive_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type one_inductive_expr = [%import: Vernacexpr.one_inductive_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type proof_expr = [%import: Vernacexpr.proof_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type opacity_flag = [%import: Vernacexpr.opacity_flag] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type proof_end = [%import: Vernacexpr.proof_end] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type one_import_filter_name = [%import: Vernacexpr.one_import_filter_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type import_filter_expr = [%import: Vernacexpr.import_filter_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type scheme = [%import: Vernacexpr.scheme] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type section_subset_expr = [%import: Vernacexpr.section_subset_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type extend_name = [%import: Vernacexpr.extend_name] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type register_kind = [%import: Vernacexpr.register_kind] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type module_ast_inl = [%import: Vernacexpr.module_ast_inl] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type module_binder = [%import: Vernacexpr.module_binder] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type typeclass_constraint = [%import: Vernacexpr.typeclass_constraint] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type discharge = [%import: Vernacexpr.discharge] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] + +module AM = struct + type _t = + | Assert + | ClearBidiHint + | ClearImplicits + | ClearScopes + | DefaultImplicits + | ExtraScopes + | ReductionDontExposeCase + | ReductionNeverUnfold + | Rename + [@@deriving python] + + type t = Vernacexpr.arguments_modifier + + let _to (x : t) : _t = match x with + | `Assert -> Assert + | `ClearBidiHint -> ClearBidiHint + | `ClearImplicits -> ClearImplicits + | `ClearScopes -> ClearScopes + | `DefaultImplicits -> DefaultImplicits + | `ExtraScopes -> ExtraScopes + | `ReductionDontExposeCase -> ReductionDontExposeCase + | `ReductionNeverUnfold -> ReductionNeverUnfold + | `Rename -> Rename + + let _of (x : _t) : t = match x with + | Assert -> `Assert + | ClearBidiHint -> `ClearBidiHint + | ClearImplicits -> `ClearImplicits + | ClearScopes -> `ClearScopes + | DefaultImplicits -> `DefaultImplicits + | ExtraScopes -> `ExtraScopes + | ReductionDontExposeCase -> `ReductionDontExposeCase + | ReductionNeverUnfold -> `ReductionNeverUnfold + | Rename -> `Rename + + let t_of_python x = _of (_t_of_python x) + let python_of_t x = python_of__t (_to x) + +end type arguments_modifier = [%import: Vernacexpr.arguments_modifier] [@@deriving sexp,yojson] +let arguments_modifier_of_python = AM.t_of_python +let python_of_arguments_modifier = AM.python_of_t + type vernac_one_argument_status = [%import: Vernacexpr.vernac_one_argument_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type vernac_argument_status = [%import: Vernacexpr.vernac_argument_status] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type hint_info_expr = [%import: Vernacexpr.hint_info_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type reference_or_constr = [%import: Vernacexpr.reference_or_constr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type hints_expr = [%import: Vernacexpr.hints_expr] - [@@deriving sexp,yojson] + [@@deriving sexp,yojson,python] type vernac_expr = [%import: Vernacexpr.vernac_expr] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type control_flag = [%import: Vernacexpr.control_flag] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type vernac_control_r = [%import: Vernacexpr.vernac_control_r] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] type vernac_control = [%import: Vernacexpr.vernac_control] - [@@deriving sexp, yojson] + [@@deriving sexp, yojson, python] diff --git a/serlib/ser_vernacexpr.mli b/serlib/ser_vernacexpr.mli index 35ff1b98..9aff437d 100644 --- a/serlib/ser_vernacexpr.mli +++ b/serlib/ser_vernacexpr.mli @@ -234,3 +234,5 @@ val vernac_control_of_sexp : Sexp.t -> vernac_control val sexp_of_vernac_control : vernac_control -> Sexp.t val vernac_control_of_yojson : Yojson.Safe.t -> (vernac_control, string) Result.result val vernac_control_to_yojson : vernac_control -> Yojson.Safe.t +val vernac_control_of_python : Py.Object.t -> vernac_control +val python_of_vernac_control : vernac_control -> Py.Object.t diff --git a/serlib/ser_vmemitcodes.ml b/serlib/ser_vmemitcodes.ml index a8bae3ef..2edc8bc8 100644 --- a/serlib/ser_vmemitcodes.ml +++ b/serlib/ser_vmemitcodes.ml @@ -54,3 +54,8 @@ let sexp_of_to_patch_substituted = let to_patch_substituted_of_sexp _ = Obj.magic PBCconstant (* Serlib_base.opaque_of_sexp ~typ:"Cemitcodes.to_patch_substituted" *) + +let python_of_to_patch_substituted = + Serlib_base.python_of_opaque ~typ:"Cemitcodes.to_patch_substituted" + +let to_patch_substituted_of_python _ = Obj.magic PBCconstant diff --git a/serlib/ser_vmemitcodes.mli b/serlib/ser_vmemitcodes.mli index 7636044d..a1f8da80 100644 --- a/serlib/ser_vmemitcodes.mli +++ b/serlib/ser_vmemitcodes.mli @@ -26,3 +26,5 @@ type to_patch_substituted = Vmemitcodes.to_patch_substituted val sexp_of_to_patch_substituted : to_patch_substituted -> Sexp.t val to_patch_substituted_of_sexp : Sexp.t -> to_patch_substituted +val python_of_to_patch_substituted : to_patch_substituted -> Py.Object.t +val to_patch_substituted_of_python : Py.Object.t -> to_patch_substituted diff --git a/serlib/ser_vmvalues.ml b/serlib/ser_vmvalues.ml index 4dd13916..dbe991b7 100644 --- a/serlib/ser_vmvalues.ml +++ b/serlib/ser_vmvalues.ml @@ -15,11 +15,12 @@ (************************************************************************) open Sexplib.Conv +open Ppx_python_runtime type tag = [%import: Vmvalues.tag] - [@@deriving sexp] + [@@deriving sexp,python] type reloc_table = [%import: Vmvalues.reloc_table] - [@@deriving sexp] + [@@deriving sexp,python] diff --git a/serlib/ser_vmvalues.mli b/serlib/ser_vmvalues.mli index 741fc5be..eadbf171 100644 --- a/serlib/ser_vmvalues.mli +++ b/serlib/ser_vmvalues.mli @@ -22,5 +22,9 @@ val tag_of_sexp : Sexp.t -> tag val sexp_of_tag : tag -> Sexp.t type reloc_table = Vmvalues.reloc_table + val reloc_table_of_sexp : Sexp.t -> reloc_table val sexp_of_reloc_table : reloc_table -> Sexp.t + +val reloc_table_of_python : Py.Object.t -> reloc_table +val python_of_reloc_table : reloc_table -> Py.Object.t diff --git a/serlib/serlib_base.ml b/serlib/serlib_base.ml index 36c3171b..cbca10df 100644 --- a/serlib/serlib_base.ml +++ b/serlib/serlib_base.ml @@ -32,3 +32,13 @@ let sexp_of_opaque ~typ _exp = raise (Ser_error msg) else Sexplib.Sexp.Atom ("["^typ^": ABSTRACT]") + +let opaque_of_python ~typ _obj = + raise (Ser_error ("["^typ^": ABSTRACT / cannot deserialize]")) + +let python_of_opaque ~typ _obj = + let msg = "["^typ^": ABSTRACT]" in + if !exn_on_opaque then + raise (Ser_error msg) + else + Py.String.of_string ("["^typ^": ABSTRACT]") diff --git a/serlib/serlib_base.mli b/serlib/serlib_base.mli index 5824a0ab..d28415a9 100644 --- a/serlib/serlib_base.mli +++ b/serlib/serlib_base.mli @@ -21,3 +21,6 @@ val exn_on_opaque : bool ref val sexp_of_opaque : typ:string -> 'a -> Sexp.t val opaque_of_sexp : typ:string -> Sexp.t -> 'a + +val python_of_opaque : typ:string -> 'a -> Py.Object.t +val opaque_of_python : typ:string -> Py.Object.t -> 'a diff --git a/sertop/dune b/sertop/dune index 971d1990..5290cda0 100644 --- a/sertop/dune +++ b/sertop/dune @@ -2,14 +2,14 @@ (name sertop) (public_name coq-serapi.sertop_v8_12) (modules :standard \ sertop_bin sercomp sertok sername sertop_js sertop_async) - (preprocess (staged_pps ppx_import ppx_sexp_conv)) + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python)) (libraries findlib.dynload cmdliner serapi serlib serlib_ltac)) (executables (public_names sertop sercomp sertok sername) (names sertop_bin sercomp sertok sername) (modules sertop_bin sercomp sertok sername) - (preprocess (staged_pps ppx_import ppx_sexp_conv)) + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python)) (link_flags -linkall) (libraries sertop)) @@ -17,7 +17,7 @@ (name sertop_js) (modules sertop_async sertop_js) (modes js) - (preprocess (staged_pps ppx_import ppx_sexp_conv)) + (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python)) (js_of_ocaml (javascript_files ../jscoq/coq-libjs/mutex.js diff --git a/sertop/sertop_pyser.ml b/sertop/sertop_pyser.ml new file mode 100644 index 00000000..3a81d8d7 --- /dev/null +++ b/sertop/sertop_pyser.ml @@ -0,0 +1,305 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Sertop_util.pp_sertop + | SP_Mach -> Sexplib.Sexp.pp + | SP_Human -> Sexplib.Sexp.pp_hum + +module SP = Serapi.Serapi_protocol + +(******************************************************************************) +(* Exception Registration *) +(******************************************************************************) + +(* We play slow for now *) +let _ = + (* XXX Finish this *) + let open Sexplib in + let open Sexplib.Conv in + let open Sexplib.Sexp in + let sexp_of_std_ppcmds pp = Atom (Pp.string_of_ppcmds pp) in + Conv.Exn_converter.add [%extension_constructor SP.NoSuchState] (function + (* Own things *) + | SP.NoSuchState sid -> + List [Atom "NoSuchState"; Ser_stateid.sexp_of_t sid] + | _ -> assert false); + Conv.Exn_converter.add [%extension_constructor CErrors.UserError] (function + (* Errors *) + | CErrors.UserError(hdr,msg) -> + let hdr = Option.default "" hdr in + List [Atom "CErrors.UserError"; List [Atom hdr; sexp_of_std_ppcmds msg]] + | _ -> assert false); + Conv.Exn_converter.add [%extension_constructor DeclareUniv.AlreadyDeclared] (function + | DeclareUniv.AlreadyDeclared (msg, id) -> + List [Atom "Declare.AlreadyDeclared"; List [sexp_of_option sexp_of_string msg; Ser_names.Id.sexp_of_t id]] + | _ -> assert false); + Conv.Exn_converter.add [%extension_constructor Pretype_errors.PretypeError] (function + (* Pretype Errors XXX what to do with _env, _envmap *) + | Pretype_errors.PretypeError(_env, _evmap, pterr) -> + List [Atom "Pretype_errors.PretypeError"; + List [Ser_pretype_errors.sexp_of_pretype_error pterr]] + | _ -> assert false); + (* Conv.Exn_converter.add [%extension_constructor Proof_global.NoCurrentProof] (function + * | Proof_global.NoCurrentProof -> + * Atom "NoCurrentProof" + * | _ -> assert false) *) +(* Private... request Coq devs to make them public? + | Errors.Anomaly(msgo, pp) -> + Some (List [Atom "Anomaly"; sexp_of_option sexp_of_string msgo; sexp_of_std_ppcmds pp]) +*) + +(******************************************************************************) +(* Serialization of the Protocol *) +(******************************************************************************) + +module Loc = Ser_loc +module CAst = Ser_cAst +module Pp = Ser_pp +module Names = Ser_names +module Environ = Ser_environ +module Goptions = Ser_goptions +module Stateid = Ser_stateid +module Evar = Ser_evar +module Context = Ser_context +module Feedback = Ser_feedback +module Libnames = Ser_libnames +module Globnames = Ser_globnames +module Impargs = Ser_impargs +module Constr = Ser_constr +module Constrexpr = Ser_constrexpr +module Proof = Ser_proof +module Goal = Ser_goal +module Tok = Ser_tok +module Ppextend = Ser_ppextend +module Notation_gram = Ser_notation_gram +module Genarg = Ser_genarg +module Loadpath = Ser_loadpath +module Printer = Ser_printer + +(* Alias fails due to the [@@default in protocol] *) +(* module Stm = Ser_stm *) +module Ser_stm = Ser_stm + +module Ltac_plugin = struct + module Tacenv = Serlib_ltac.Ser_tacenv + module Profile_ltac = Serlib_ltac.Ser_profile_ltac + module Tacexpr = Serlib_ltac.Ser_tacexpr +end + +module Notation = Ser_notation +module Xml_datatype = Ser_xml_datatype +module Notation_term = Ser_notation_term +module Vernacexpr = Ser_vernacexpr +module Declarations = Ser_declarations +(* module Richpp = Ser_richpp *) + +(* XXX: hack!! *) +[@@@ocaml.warning "-38"] +exception Not_found_s = Base.Not_found_s +(* XXX: end hack!! *) + +module Serapi = struct +module Serapi_goals = struct + + type 'a hyp = + [%import: 'a Serapi.Serapi_goals.hyp] + [@@deriving python] + + type info = + [%import: Serapi.Serapi_goals.info] + [@@deriving python] + + type 'a reified_goal = + [%import: 'a Serapi.Serapi_goals.reified_goal] + [@@deriving python] + + type 'a ser_goals = + [%import: 'a Serapi.Serapi_goals.ser_goals] + [@@deriving python] + +end + +module Serapi_assumptions = struct +type ax_ctx = + [%import: Serapi.Serapi_assumptions.ax_ctx] + [@@deriving python] + +type t = + [%import: Serapi.Serapi_assumptions.t] + [@@deriving python] + +end + +module Serapi_protocol = Serapi.Serapi_protocol + +end + +(* Serialization to sexp *) +type coq_object = + [%import: Serapi.Serapi_protocol.coq_object] + [@@deriving python] + +exception AnswerExn of Py.Object.t +let exn_of_python sexp = AnswerExn sexp +let python_of_exn _ = Py.none + +type print_format = + [%import: Serapi.Serapi_protocol.print_format] + [@@deriving python] + +type format_opt = + [%import: Serapi.Serapi_protocol.format_opt] + [@@deriving python] + +type print_opt = + [%import: Serapi.Serapi_protocol.print_opt] + [@@deriving python] + +type query_pred = + [%import: Serapi.Serapi_protocol.query_pred] + [@@deriving python] + +type query_opt = + [%import: Serapi.Serapi_protocol.query_opt + [@with + Sexplib.Conv.sexp_list := sexp_list; + Sexplib.Conv.sexp_option := sexp_option; + ]] + [@@deriving python] + +type query_cmd = + [%import: Serapi.Serapi_protocol.query_cmd] + [@@deriving python] + +type cmd_tag = + [%import: Serapi.Serapi_protocol.cmd_tag] + [@@deriving python] + +type location = + [%import: Printexc.location] + [@@deriving python] + +type raw_backtrace = Printexc.raw_backtrace +let raw_backtrace_of_python _ = Printexc.get_raw_backtrace () + +type slot_rep = { + slot_loc : location option; + slot_idx : int; + slot_str : string option; +} [@@deriving python] + +let to_slot_rep idx bs = { + slot_loc = Printexc.Slot.location bs; + slot_idx = idx; + slot_str = Printexc.Slot.format idx bs; +} + +let python_of_backtrace_slot idx bs = + python_of_slot_rep (to_slot_rep idx bs) + +(* +let sexp_of_raw_backtrace (bt : Printexc.raw_backtrace) : Sexp.t = + let bt = Printexc.backtrace_slots bt in + let bt = Option.map Array.(mapi sexp_of_backtrace_slot) bt in + let bt = sexp_of_option (sexp_of_array (fun x -> x)) bt in + Sexp.(List [Atom "Backtrace"; bt]) +*) + +let python_of_raw_backtrace (_bt : Printexc.raw_backtrace) : Py.Object.t = + Ppx_python_runtime.python_of_bool false + +module ExnInfo = struct + type t = + [%import: Serapi.Serapi_protocol.ExnInfo.t + [@with + Stm.focus := Ser_stm.focus; + Printexc.raw_backtrace := raw_backtrace; + Stdlib.Printexc.raw_backtrace := raw_backtrace; + ]] + [@@deriving python] +end + +type focus_info = + [%import: Serapi.Serapi_protocol.focus_info] + [@@deriving python] + +type answer_kind = + [%import: Serapi.Serapi_protocol.answer_kind + [@with Exninfo.t := Exninfo.t; + ]] + [@@deriving python] + +type feedback_content = + [%import: Serapi.Serapi_protocol.feedback_content] + [@@deriving python] + +type feedback = + [%import: Serapi.Serapi_protocol.feedback] + [@@deriving python] + +type answer = + [%import: Serapi.Serapi_protocol.answer] + [@@deriving python] + +type add_opts = + [%import: Serapi.Serapi_protocol.add_opts + [@with + Sexplib.Conv.sexp_option := sexp_option; + ]] + [@@deriving python] + +type newdoc_opts = + [%import: Serapi.Serapi_protocol.newdoc_opts + [@with + Stm.interactive_top := Ser_stm.interactive_top; + Sexplib.Conv.sexp_list := sexp_list; + Sexplib.Conv.sexp_option := sexp_option; + ]] + [@@deriving python] + +type save_opts = + [%import: Serapi.Serapi_protocol.save_opts] + [@@deriving python] + +type parse_opt = + [%import: Serapi.Serapi_protocol.parse_opt + [@with + Sexplib.Conv.sexp_option := sexp_option; + ]] + [@@deriving python] + +type cmd = + [%import: Serapi.Serapi_protocol.cmd] + [@@deriving python] + +type tagged_cmd = + [%import: Serapi.Serapi_protocol.tagged_cmd] + [@@deriving python] + +type sentence = Sentence of Tok.t CAst.t list + [@@deriving python] diff --git a/sertop/sertop_ser.ml b/sertop/sertop_ser.ml index 9ecafc11..f4310c82 100644 --- a/sertop/sertop_ser.ml +++ b/sertop/sertop_ser.ml @@ -231,6 +231,10 @@ module ExnInfo = struct [@@deriving sexp] end +type focus_info = + [%import: Serapi.Serapi_protocol.focus_info] + [@@deriving sexp] + type answer_kind = [%import: Serapi.Serapi_protocol.answer_kind [@with Exninfo.t := Exninfo.t;