Adds Model.to_json (Closes #168)

dune-project

@@ -54,6 +54,7 @@
    (and
     :build
     (>= "20220210")))
+  yojson
   (odoc
    :with-doc)
   (bisect_ppx

lib/dune

@@ -45,6 +45,7 @@
  (libraries
   hc
   ocaml_intrinsics
+  yojson
   (select
    colibri2_mappings.ml
    from

lib/model.ml

@@ -18,36 +18,46 @@
 
 type t = (Symbol.t, Value.t) Hashtbl.t
 
+
+let iter f model = Hashtbl.iter (fun a b -> f (a, b)) model
+
 let get_symbols (model : t) : Symbol.t List.t =
   Hashtbl.to_seq_keys model |> List.of_seq |> List.sort Symbol.compare
 
 let compare_bindings (s1, v1) (s2, v2) =
   let compare_symbol = Symbol.compare s1 s2 in
   if compare_symbol = 0 then Value.compare v1 v2 else compare_symbol
 
-let get_bindings (model : t) : (Symbol.t * Value.t) List.t =
+let get_bindings (model : t) : (Symbol.t * Value.t) list =
   Hashtbl.to_seq model |> List.of_seq |> List.sort compare_bindings
 
-let evaluate (model : t) (symb : Symbol.t) : Value.t Option.t =
+let evaluate (model : t) (symb : Symbol.t) : Value.t option =
   Hashtbl.find_opt model symb
 
-let pp_print_hashtbl ~pp_sep pp_v fmt v =
-  let l = Hashtbl.to_seq v |> List.of_seq |> List.sort compare_bindings in
-  Format.pp_print_list ~pp_sep pp_v fmt l
-
 let pp_bindings fmt ?(no_values = false) model =
-  pp_print_hashtbl
+  Format.pp_print_list
     ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
     (fun fmt (key, data) ->
       if not no_values then
         Format.fprintf fmt "(%a %a)" Symbol.pp key Value.pp data
       else
         let t = Symbol.type_of key in
         Format.fprintf fmt "(%a %a)" Symbol.pp key Ty.pp t )
-    fmt model
+    fmt (get_bindings model)
 
 let pp fmt ?(no_values = false) model =
   Format.fprintf fmt "(model@\n  @[<v>%a@])" (pp_bindings ~no_values) model
 
-let to_string (model : t) : String.t =
+let to_string (model : t) : string =
   Format.asprintf "%a" (pp ~no_values:false) model
+
+let to_json (model : t) : Yojson.t =
+  let model :> Yojson.t list =
+    Hashtbl.fold
+      (fun s v acc ->
+        let s = Symbol.to_json s in
+        let v = `Assoc [ ("value", Value.to_json v) ] in
+        Yojson.Basic.Util.combine s v :: acc )
+      model []
+  in
+  `Assoc [ ("model", `List model) ]

lib/model.mli

@@ -18,12 +18,17 @@
 
 type t = (Symbol.t, Value.t) Hashtbl.t
 
-val get_symbols : t -> Symbol.t List.t
+val iter : (Symbol.t * Value.t -> unit) -> t -> unit
 
-val get_bindings : t -> (Symbol.t * Value.t) List.t
+val get_symbols : t -> Symbol.t list
 
-val evaluate : t -> Symbol.t -> Value.t Option.t
+(** bindings are sorted by symbol *)
+val get_bindings : t -> (Symbol.t * Value.t) list
 
-val pp : Format.formatter -> ?no_values:bool -> t -> Unit.t
+val evaluate : t -> Symbol.t -> Value.t option
 
-val to_string : t -> String.t
+val pp : Format.formatter -> ?no_values:bool -> t -> unit
+
+val to_string : t -> string
+
+val to_json : t -> Yojson.t

lib/num.ml

@@ -23,15 +23,6 @@ type t =
   | F32 of int32
   | F64 of int64
 
-let equal (n1 : t) (n2 : t) : bool =
-  match (n1, n2) with
-  | I8 i1, I8 i2 -> i1 = i2
-  | I32 i1, I32 i2 -> i1 = i2
-  | I64 i1, I64 i2 -> i1 = i2
-  | F32 i1, F32 i2 -> Int32.float_of_bits i1 = Int32.float_of_bits i2
-  | F64 i1, F64 i2 -> Int64.float_of_bits i1 = Int64.float_of_bits i2
-  | I8 _, _ | I32 _, _ | I64 _, _ | F32 _, _ | F64 _, _ -> false
-
 let compare n1 n2 =
   match (n1, n2) with
   | I8 i1, I8 i2 -> compare i1 i2
@@ -45,13 +36,16 @@ let compare n1 n2 =
   *)
   | I8 _, _ | I32 _, _ | I64 _, _ | F32 _, _ | F64 _, _ -> compare n1 n2
 
-let type_of (n : t) =
-  match n with
-  | I8 _ -> Ty.(Ty_bitv 8)
-  | I32 _ -> Ty.(Ty_bitv 32)
-  | I64 _ -> Ty.(Ty_bitv 64)
-  | F32 _ -> Ty.(Ty_fp 32)
-  | F64 _ -> Ty.(Ty_fp 64)
+let equal (n1 : t) (n2 : t) : bool =
+  match (n1, n2) with
+  | I8 i1, I8 i2 -> i1 = i2
+  | I32 i1, I32 i2 -> i1 = i2
+  | I64 i1, I64 i2 -> i1 = i2
+  | F32 i1, F32 i2 -> Int32.float_of_bits i1 = Int32.float_of_bits i2
+  | F64 i1, F64 i2 -> Int64.float_of_bits i1 = Int64.float_of_bits i2
+  | I8 _, _ | I32 _, _ | I64 _, _ | F32 _, _ | F64 _, _ -> false
+
+let num_of_bool (b : bool) : t = I32 (if b then 1l else 0l)
 
 let pp fmt (n : t) =
   match n with
@@ -63,4 +57,12 @@ let pp fmt (n : t) =
 
 let to_string (n : t) : string = Format.asprintf "%a" pp n
 
-let num_of_bool (b : bool) : t = I32 (if b then 1l else 0l)
+let to_json (n : t) : Yojson.Basic.t = `String (to_string n)
+
+let type_of (n : t) =
+  match n with
+  | I8 _ -> Ty.(Ty_bitv 8)
+  | I32 _ -> Ty.(Ty_bitv 32)
+  | I64 _ -> Ty.(Ty_bitv 64)
+  | F32 _ -> Ty.(Ty_fp 32)
+  | F64 _ -> Ty.(Ty_fp 64)

lib/num.mli

@@ -23,14 +23,16 @@ type t =
   | F32 of int32
   | F64 of int64
 
-val equal : t -> t -> bool
-
 val compare : t -> t -> int
 
-val type_of : t -> Ty.t
+val equal : t -> t -> bool
+
+val num_of_bool : bool -> t
 
 val pp : Format.formatter -> t -> unit
 
 val to_string : t -> string
 
-val num_of_bool : bool -> t
+val to_json : t -> Yojson.Basic.t
+
+val type_of : t -> Ty.t

lib/symbol.ml

@@ -23,22 +23,26 @@ type t =
 
 let ( @: ) (name : string) (ty : Ty.t) : t = { name; ty }
 
-let make (ty : Ty.t) (name : string) : t = name @: ty
-
-let mk_symbol (ty : Ty.t) (name : string) : t = name @: ty
-
-let equal (s1 : t) (s2 : t) : bool =
-  Ty.equal s1.ty s2.ty && String.equal s1.name s2.name
-
 let compare (t1 : t) (t2 : t) : int =
   let compare_name = compare t1.name t2.name in
   if compare_name = 0 then compare t1.ty t2.ty else compare_name
 
-let rename (symbol : t) (name : string) : t = { symbol with name }
+let equal (s1 : t) (s2 : t) : bool =
+  Ty.equal s1.ty s2.ty && String.equal s1.name s2.name
 
-let type_of ({ ty; _ } : t) : Ty.t = ty
+let make (ty : Ty.t) (name : string) : t = name @: ty
+
+let mk_symbol (ty : Ty.t) (name : string) : t = name @: ty
 
 let pp (fmt : Format.formatter) ({ name; _ } : t) : unit =
   Format.pp_print_string fmt name
 
+let rename (symbol : t) (name : string) : t = { symbol with name }
+
 let to_string ({ name; _ } : t) : string = name
+
+let to_json ({ name; ty } : t) : Yojson.Basic.t =
+  `Assoc
+    [ ("name", `String name); ("ty", `String (Format.asprintf "%a" Ty.pp ty)) ]
+
+let type_of ({ ty; _ } : t) : Ty.t = ty

lib/symbol.mli

@@ -23,18 +23,20 @@ type t =
 
 val ( @: ) : string -> Ty.t -> t
 
+val compare : t -> t -> int
+
+val equal : t -> t -> Bool.t
+
 val make : Ty.t -> string -> t
 
 val mk_symbol : Ty.t -> string -> t [@@deprecated "Please use 'make' instead"]
 
-val equal : t -> t -> Bool.t
+val pp : Format.formatter -> t -> unit
 
 val rename : t -> string -> t
 
-val type_of : t -> Ty.t
-
 val to_string : t -> string
 
-val compare : t -> t -> int
+val to_json : t -> Yojson.Basic.t
 
-val pp : Format.formatter -> t -> unit
+val type_of : t -> Ty.t

lib/value.ml

@@ -28,19 +28,7 @@ type t =
   | List of t list
   | App : [> `Op of string ] * t list -> t
 
-let rec equal (v1 : t) (v2 : t) : Bool.t =
-  match (v1, v2) with
-  | True, True | False, False -> true
-  | Int x1, Int x2 -> Int.equal x1 x2
-  | Real x1, Real x2 -> x1 = x2
-  | Str x1, Str x2 -> String.equal x1 x2
-  | Num x1, Num x2 -> Num.equal x1 x2
-  | List l1, List l2 -> List.equal equal l1 l2
-  | App (`Op op1, vs1), App (`Op op2, vs2) ->
-    String.equal op1 op2 && List.equal equal vs1 vs2
-  | _ -> false
-
-let rec compare v1 v2 =
+let rec compare (v1 : t) (v2 : t) : int =
   match (v1, v2) with
   | True, True | False, False -> 0
   | False, True -> -1
@@ -55,17 +43,19 @@ let rec compare v1 v2 =
     if c = 0 then List.compare compare vs1 vs2 else c
   | _ -> compare v1 v2
 
-let type_of (v : t) : Ty.t =
-  match v with
-  | True | False -> Ty_bool
-  | Int _ -> Ty_int
-  | Real _ -> Ty_real
-  | Str _ -> Ty_str
-  | Num n -> Num.type_of n
-  | List _ -> Ty_list
-  | App _ -> Ty_app
+let rec equal (v1 : t) (v2 : t) : bool =
+  match (v1, v2) with
+  | True, True | False, False -> true
+  | Int x1, Int x2 -> Int.equal x1 x2
+  | Real x1, Real x2 -> x1 = x2
+  | Str x1, Str x2 -> String.equal x1 x2
+  | Num x1, Num x2 -> Num.equal x1 x2
+  | List l1, List l2 -> List.equal equal l1 l2
+  | App (`Op op1, vs1), App (`Op op2, vs2) ->
+    String.equal op1 op2 && List.equal equal vs1 vs2
+  | _ -> false
 
-let rec pp fmt (v : t) =
+let rec pp (fmt : Format.formatter) (v : t) : unit =
   let open Format in
   match v with
   | True -> pp_print_string fmt "true"
@@ -84,4 +74,25 @@ let rec pp fmt (v : t) =
       vs
   | _ -> assert false
 
-let to_string v = Format.asprintf "%a" pp v
+let to_string (v : t) : string = Format.asprintf "%a" pp v
+
+let rec to_json (v : t) : Yojson.Basic.t =
+  match v with
+  | True -> `Bool true
+  | False -> `Bool false
+  | Int int -> `Int int
+  | Real real -> `Float real
+  | Str str -> `String str
+  | Num n -> Num.to_json n
+  | List l -> `List (List.map to_json l)
+  | App _ -> assert false
+
+let type_of (v : t) : Ty.t =
+  match v with
+  | True | False -> Ty_bool
+  | Int _ -> Ty_int
+  | Real _ -> Ty_real
+  | Str _ -> Ty_str
+  | Num n -> Num.type_of n
+  | List _ -> Ty_list
+  | App _ -> Ty_app

lib/value.mli

@@ -26,12 +26,14 @@ type t =
   | List of t list
   | App : [> `Op of string ] * t list -> t
 
-val equal : t -> t -> bool
-
 val compare : t -> t -> int
 
-val type_of : t -> Ty.t
+val equal : t -> t -> bool
 
 val pp : Format.formatter -> t -> unit
 
 val to_string : t -> string
+
+val to_json : t -> Yojson.Basic.t
+
+val type_of : t -> Ty.t

smtml.opam

@@ -16,6 +16,7 @@ depends: [
   "zarith" {>= "1.5"}
   "hc" {>= "0.3"}
   "menhir" {build & >= "20220210"}
+  "yojson"
   "odoc" {with-doc}
   "bisect_ppx" {with-test & >= "2.5.0"}
 ]

test/unit/dune

@@ -7,5 +7,6 @@
   test_triop
   test_relop
   test_cvtop
-  test_naryop)
- (libraries smtml))
+  test_naryop
+  test_model)
+ (libraries smtml yojson))

test/unit/test_model.expected

@@ -0,0 +1,8 @@
+{
+  "model": [
+    { "name": "u", "ty": "str", "value": "abc" },
+    { "name": "z", "ty": "bool", "value": true },
+    { "name": "x", "ty": "int", "value": 1 },
+    { "name": "y", "ty": "real", "value": 2.0 }
+  ]
+}

test/unit/test_model.ml

@@ -0,0 +1,17 @@
+open Smtml
+
+(** Test Model.to_json *)
+let () =
+  let x = Symbol.make Ty_int "x" in
+  let y = Symbol.make Ty_real "y" in
+  let z = Symbol.make Ty_bool "z" in
+  let u = Symbol.make Ty_str "u" in
+  let model : Model.t =
+    let tbl = Hashtbl.create 16 in
+    List.iter
+      (fun ((s, v) : Symbol.t * Value.t) -> Hashtbl.replace tbl s v)
+      [ (x, Int 1); (y, Real 2.0); (z, True); (u, Str "abc") ];
+    tbl
+  in
+  let model_to_json = Model.to_json model in
+  Format.printf "%a@." (Yojson.pretty_print ~std:true) model_to_json