Add parsing utilities to Value

Adds `Value.of_string` and `Num.of_string` to retrieve values from
serialized models and adds test for scfg model parsing.

src/ast/num.ml

@@ -14,6 +14,14 @@ type printer =
   | `Hexadecimal
   ]
 
+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 compare n1 n2 =
   match (n1, n2) with
   | I8 i1, I8 i2 -> Int.compare i1 i2
@@ -62,12 +70,22 @@ let pp fmt v = !printer fmt v
 
 let to_string (n : t) : string = Fmt.str "%a" pp n
 
-let to_json (n : t) : Yojson.Basic.t = `String (to_string n)
+let of_string (cast : Ty.t) value =
+  match cast with
+  | Ty_bitv 8 -> (
+    match int_of_string value with
+    | None -> Error "invalid value, expected 8-bit bitv"
+    | Some n -> Ok (I8 n) )
+  | Ty_bitv 32 -> Ok (I32 (Int32.of_string value))
+  | Ty_bitv 64 -> Ok (I64 (Int64.of_string value))
+  | Ty_fp 32 -> (
+    match float_of_string value with
+    | None -> Error "invalid value, expected float"
+    | Some n -> Ok (I32 (Int32.bits_of_float n)) )
+  | Ty_fp 64 -> (
+    match float_of_string value with
+    | None -> Error "invalid value, expected float"
+    | Some n -> Ok (I64 (Int64.bits_of_float n)) )
+  | _ -> Error "invalid value, expected num"
 
-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 to_json (n : t) : Yojson.Basic.t = `String (to_string n)

src/ast/num.mli

@@ -14,6 +14,8 @@ type printer =
   | `Hexadecimal
   ]
 
+val type_of : t -> Ty.t
+
 val compare : t -> t -> int
 
 val equal : t -> t -> bool
@@ -26,6 +28,6 @@ val pp : t Fmt.t
 
 val to_string : t -> string
 
-val to_json : t -> Yojson.Basic.t
+val of_string : Ty.t -> string -> (t, string) result
 
-val type_of : t -> Ty.t
+val to_json : t -> Yojson.Basic.t

src/ast/value.ml

@@ -16,6 +16,18 @@ type t =
   | App : [> `Op of string ] * t list -> t
   | Nothing
 
+let type_of (v : t) : Ty.t =
+  match v with
+  | True | False -> Ty_bool
+  | Unit -> Ty_unit
+  | Int _ -> Ty_int
+  | Real _ -> Ty_real
+  | Str _ -> Ty_str
+  | Num n -> Num.type_of n
+  | List _ -> Ty_list
+  | App _ -> Ty_app
+  | Nothing -> Ty_none
+
 let rec compare (v1 : t) (v2 : t) : int =
   match (v1, v2) with
   | True, True | False, False | Unit, Unit | Nothing, Nothing -> 0
@@ -69,6 +81,29 @@ let rec pp fmt = function
 
 let to_string (v : t) : string = Fmt.str "%a" pp v
 
+let of_string (cast : Ty.t) v =
+  let open Result in
+  match cast with
+  | Ty_bitv _ | Ty_fp _ ->
+    let+ n = Num.of_string cast v in
+    Num n
+  | Ty_bool -> (
+    match v with
+    | "true" -> Ok True
+    | "false" -> Ok False
+    | _ -> Error "invalid value, expected boolean" )
+  | Ty_int -> (
+    match int_of_string v with
+    | None -> Error "invalid value, expected integer"
+    | Some n -> Ok (Int n) )
+  | Ty_real -> (
+    match float_of_string v with
+    | None -> Error "invalid value, expected real"
+    | Some n -> Ok (Real n) )
+  | Ty_str -> Ok (Str v)
+  | Ty_app | Ty_list | Ty_none | Ty_unit | Ty_regexp ->
+    Error (Fmt.str "unsupported parsing values of type %a" Ty.pp cast)
+
 let rec to_json (v : t) : Yojson.Basic.t =
   match v with
   | True -> `Bool true
@@ -81,15 +116,3 @@ let rec to_json (v : t) : Yojson.Basic.t =
   | List l -> `List (List.map to_json l)
   | Nothing -> `Null
   | App _ -> assert false
-
-let type_of (v : t) : Ty.t =
-  match v with
-  | True | False -> Ty_bool
-  | Unit -> Ty_unit
-  | Int _ -> Ty_int
-  | Real _ -> Ty_real
-  | Str _ -> Ty_str
-  | Num n -> Num.type_of n
-  | List _ -> Ty_list
-  | App _ -> Ty_app
-  | Nothing -> Ty_none

src/ast/value.mli

@@ -14,6 +14,8 @@ type t =
   | App : [> `Op of string ] * t list -> t
   | Nothing
 
+val type_of : t -> Ty.t
+
 val compare : t -> t -> int
 
 val equal : t -> t -> bool
@@ -26,6 +28,6 @@ val pp : t Fmt.t
 
 val to_string : t -> string
 
-val to_json : t -> Yojson.Basic.t
+val of_string : Ty.t -> string -> (t, string) result
 
-val type_of : t -> Ty.t
+val to_json : t -> Yojson.Basic.t

src/solvers/model.ml

@@ -49,6 +49,17 @@ let to_json (model : t) : Yojson.t =
   let model :> Yojson.t = Hashtbl.fold add_assignment model (`Assoc []) in
   `Assoc [ ("model", model) ]
 
+(** {b Example}: Model in the json format:
+
+    {@json[
+      {
+        "model" : {
+          "x_0" : { "ty" : "int", "value" : 42 },
+          "x_1" : { "ty" : "bool", "value" : true },
+          "x_2" : { "ty" : "f32", "value" : 42.42 }
+        }
+      }
+    ]} *)
 let to_json_string model =
   let model = to_json model in
   Fmt.str "%a" Yojson.pp model
@@ -68,18 +79,30 @@ let to_scfg model =
   in
   [ { name = "model"; params = []; children } ]
 
+(** {b Example}: Model in the scfg format:
+
+    {@scfg[
+      model {
+        symbol x_0 int 42
+        symbol x_1 bool true
+        symbol x_2 f32 42.42
+      }
+    ]} *)
 let to_scfg_string model =
   let model = to_scfg model in
   Fmt.str "%a" Scfg.Pp.config model
 
 let to_smtlib _model = assert false
 
+(** {b Example}: TODO *)
 let to_smtlib_string model =
   let _model = to_smtlib model in
   assert false
 
 module Parse = struct
   module Json = struct
+
+
     let from_string _s = assert false
 
     let from_channel _chan = assert false
@@ -88,7 +111,7 @@ module Parse = struct
   end
 
   module Scfg = struct
-    let ( let* ) = Result.bind
+    open Result
 
     let from_scfg v =
       match Scfg.Query.get_dir "model" v with
@@ -98,27 +121,16 @@ module Parse = struct
         let symbols = Scfg.Query.get_dirs "symbol" model.children in
         let tbl = Hashtbl.create 16 in
         let* () =
-          List.fold_left
-            (fun acc symbol ->
-              let* () = acc in
+          Result.list_iter
+            (fun symbol ->
               let* name = Scfg.Query.get_param 0 symbol in
               let* ty = Scfg.Query.get_param 1 symbol in
               let* ty = Ty.of_string ty in
               let* value = Scfg.Query.get_param 2 symbol in
-              let* value =
-                (* TODO: expose a Value.of_string : ty -> s -> Value.t instead ? *)
-                match ty with
-                | Ty_bitv _n -> begin
-                  match int_of_string value with
-                  | None -> Error "invalid symbol value, expected integer"
-                  | Some n -> Ok (Value.Int n)
-                end
-                | _ -> assert false
-              in
+              let+ value = Value.of_string ty value in
               let key = Symbol.make ty name in
-              Hashtbl.add tbl key value;
-              Ok () )
-            (Ok ()) symbols
+              Hashtbl.add tbl key value )
+            symbols
         in
         Ok tbl
 

test/unit/test_model.ml

@@ -1,6 +1,6 @@
 open Smtml
 
-(** Test Model.to_json *)
+(* Test Model.to_json *)
 let () =
   let x = Symbol.make Ty_int "x" in
   let y = Symbol.make Ty_real "y" in
@@ -15,3 +15,20 @@ let () =
   in
   let model_to_json = Model.to_json model in
   Format.printf "%a@." (Yojson.pretty_print ~std:true) model_to_json
+
+(* Parsing *)
+
+(* scfg *)
+let () =
+  let open Result in
+  let model_str =
+    {|
+      model {
+        symbol x_0 int 42
+        symbol x_1 bool true
+        symbol x_2 f32 42.42
+      }
+    |}
+  in
+  let model = Model.Parse.Scfg.from_string model_str in
+  assert (match model with Ok _ -> true | _ -> false)