Export/Import lpo

lambdapi.opam

@@ -41,6 +41,7 @@ depends: [
   "lwt_ppx" {>= "1"}
   "uri" {>= "1.1"}
   "ppx_inline_test"
+  "ppx_deriving_yojson" { >= "3.7.0"}
 ]
 build: [
   ["dune" "subst"] {dev}

src/common/dune

@@ -1,6 +1,7 @@
 (library
  (name common)
  (public_name lambdapi.common)
+ (preprocess (pps ppx_deriving_yojson))
  (modules :standard)
  (libraries camlp-streams str timed lambdapi.lplib)
  (flags -w +3))

src/common/path.ml

@@ -5,7 +5,7 @@ open Lplib open Base
 module Path =
   struct
     (** Representation of a module name (roughly, a file path). *)
-    type t = string list
+    type t = string list [@@deriving yojson]
 
     (** [pp ppf p] prints path [p] on the formatter [ppf]. Remark: to be used
        in Common only as it does not escape identifiers that need to be
@@ -15,6 +15,12 @@ module Path =
     (** [compare] is a standard comparison function on paths. *)
     let compare : t cmp = Stdlib.compare
 
+    let make (s : string) : t =
+      if s = "" then []
+      else
+        s
+        |> String.split_on_char '.'
+        |> List.filter (fun x -> x <> "")
   end
 
 include Path

src/common/pos.ml

@@ -14,7 +14,7 @@ type pos =
   ; end_col      : int (** Column number (utf8) of the ending point.   *)
   ; end_offset   : int (** Number of chars since the beginning of the document
                            for the ending point *)
-  }
+  } [@@deriving yojson]
 
 (** Total comparison function on pos. *)
 let cmp : pos cmp = fun p1 p2 ->
@@ -77,7 +77,7 @@ let to_string : ?print_dirname:bool -> ?print_fname:bool -> pos -> string =
 
 
 (** Type of optional positions. *)
-type popt = pos option
+type popt = pos option [@@deriving yojson]
 
 (** [equal p1 p2] tells whether [p1] and [p2] denote the same position. *)
 let equal : popt -> popt -> bool = fun p1 p2 ->

src/core/dune

@@ -9,5 +9,8 @@
  (name core)
  (public_name lambdapi.core)
  (synopsis "LambdaPi interactive theorem prover [core]")
+ (inline_tests)
+;  (preprocess (pps ))
+ (preprocess (pps ppx_inline_test ppx_deriving_yojson))
  (modules :standard)
- (libraries lambdapi.common lambdapi.lplib pratter why3 unix))
+ (libraries yojson lambdapi.common lambdapi.lplib pratter why3 unix))