Using ezjsonm

proofs/psnj_toolbox/bin/qfo.ml

@@ -59,7 +59,12 @@ let new_sig_state (mp : Path.t) : Sig_state.t =
 
 let translate (config : string) (mapfile : string) (eval : string list) : unit =
   (* Get symbol mappings *)
-  let mapping = PsnjQfo.Mappings.of_file mapfile in
+  let mapping =
+    let ic = open_in mapfile in
+    let ret = PsnjQfo.Mappings.of_channel ic in
+    close_in ic;
+    ret
+  in
   let pvs_cert, pvs_connectives, propositional_connectives =
     let f s =
       try StrMap.find s mapping

proofs/psnj_toolbox/lib/qfo/dune

 (library
  (public_name personoj.qfo)
  (libraries
-  yojson
+  ezjsonm
   lambdapi.common
   lambdapi.lplib
   lambdapi.parsing

proofs/psnj_toolbox/lib/qfo/mappings.ml

@@ -2,7 +2,6 @@
      to work on. A symbol mapping specify which symbol of a Dedukti
      encoding implements such symbol. *)
 
-module J = Yojson.Basic
 open Lplib
 open Extra
 
@@ -10,14 +9,15 @@ type t = (string * string) list StrMap.t
 
 (** [parse obj] parses json object [obj] into a map from module names
     (as strings) to symbol mappings (as assoc list of strings). *)
-let parse (obj : J.t) : t =
-  let f (modl, map) =
-    let map =
-      J.Util.to_assoc map |> List.map (fun (x, y) -> (x, J.Util.to_string y))
+let parse (obj : Ezjsonm.t) : t =
+  let f (modl, builtins) =
+    let dict =
+      Ezjsonm.get_dict builtins
+      |> List.map (fun (k, v) -> (k, Ezjsonm.get_string v))
     in
-    StrMap.add modl map
+    StrMap.add modl dict
   in
-  List.fold_right f (J.Util.to_assoc obj) StrMap.empty
+  List.fold_right f Ezjsonm.(get_dict (value obj)) StrMap.empty
 
-(** [of_file src] parses the json object in file [src]. *)
-let of_file (src : string) : t = J.from_file src |> parse
+(** [of_file ic] parses the json object from channel [ic]. *)
+let of_channel (ic : in_channel) : t = Ezjsonm.from_channel ic |> parse

proofs/psnj_toolbox/lib/qfo/mappings.mli

@@ -6,5 +6,5 @@ type t = (string * string) list StrMap.t
     ["propositional_connectives"]) to association from label
     (e.g. "truth") to a symbol name. See the manual page. *)
 
-val of_file : string -> t
-(** [of_file f] create a mapping from a file [f]. *)
+val of_channel : in_channel -> t
+(** [of_channel ic] create a mapping from channel [ic]. *)

proofs/psnj_toolbox/personoj.opam.locked

@@ -17,10 +17,14 @@ depends: [
   "conf-pkg-config" {= "2"}
   "cppo" {= "1.6.8"}
   "csexp" {= "1.5.1"}
+  "cstruct" {= "6.0.1"}
   "dune" {= "2.9.1"}
   "dune-configurator" {= "2.9.1"}
   "easy-format" {= "1.3.2"}
+  "ezjsonm" {= "1.3.0"}
   "gen" {= "0.5.3"}
+  "hex" {= "1.4.0"}
+  "jsonm" {= "1.0.1"}
   "lambdapi" {= "1.0"}
   "menhir" {= "20211128"}
   "menhirLib" {= "20211128"}
@@ -44,7 +48,9 @@ depends: [
   "sexplib0" {= "v0.14.0"}
   "stdlib-shims" {= "0.3.0"}
   "timed" {= "1.0"}
+  "topkg" {= "1.0.4"}
   "uchar" {= "0.0.2"}
+  "uutf" {= "1.0.2"}
   "why3" {= "1.4.0"}
   "yojson" {= "1.7.0"}
 ]