1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
type token =
| Open_scope of string
| Close_scope
| Symbol of Smtml.Symbol.t
type t = token list
let symbol s tl : t = Symbol s :: tl
let open_scope name tl = Open_scope name :: tl
let close_scope tl = Close_scope :: tl
let empty = []
let of_expressions exprs =
List.fold_left
(fun acc cur -> Symbol cur :: acc)
[]
(Smtml.Expr.Set.get_symbols exprs)
let of_symbol sym = [ Symbol sym ]
let pp_token fmt token =
match token with
| Open_scope name -> Fmt.pf fmt "open %s" name
| Close_scope -> Fmt.pf fmt "close"
| Symbol s -> Fmt.pf fmt "symbol %a" Smtml.Symbol.pp s
let pp fmt tokens =
Fmt.list ~sep:(fun fmt () -> Fmt.pf fmt " ; ") pp_token fmt tokens
let only_symbols tokens =
List.filter_map
(function Symbol s -> Some s | Open_scope _ | Close_scope -> None)
tokens
let get_value model sym =
match Smtml.Model.evaluate model sym with
| Some value -> value
| None -> assert false
let to_scfg ~no_value model scope_tokens =
let open Scfg.Types in
let open Smtml in
let symbol_to_scfg symbol =
let p0 = Symbol.to_string symbol in
let p1 = Symbol.type_of symbol |> Ty.string_of_type in
let params =
if no_value then [ p0; p1 ]
else
let value = get_value model symbol in
let p2 = Value.to_string value in
[ p0; p1; p2 ]
in
{ name = "symbol"; params; children = [] }
in
let rec process_scope name tokens =
let rec collect_items acc tokens =
match tokens with
| [] ->
Logs.err (fun m -> m "Reached end without closing scope: %s" name);
assert false
| Close_scope :: rest -> (List.rev acc, rest)
| Open_scope name :: rest ->
let content, remaining = process_scope name rest in
let scope =
match content with
| sym :: [] ->
{ name = sym.name; params = sym.params @ [ name ]; children = [] }
| children -> { name = "scope"; params = [ name ]; children }
in
collect_items (scope :: acc) remaining
| Symbol s :: rest -> collect_items (symbol_to_scfg s :: acc) rest
in
collect_items [] tokens
in
let rec process_tokens tokens acc =
match tokens with
| [] -> List.rev acc
| Open_scope name :: rest ->
let content, remaining = process_scope name rest in
let scope =
match content with
| sym :: [] ->
{ name = sym.name; params = sym.params @ [ name ]; children = [] }
| _ as children -> { name = "scope"; params = [ name ]; children }
in
process_tokens remaining (scope :: acc)
| Symbol s :: rest -> process_tokens rest (symbol_to_scfg s :: acc)
| Close_scope :: _ -> assert false
in
let rev_scope_tokens = List.rev scope_tokens in
Logs.debug (fun m -> m "Current scope tokens: [%a]" pp rev_scope_tokens);
let children = process_tokens rev_scope_tokens [] in
[ { name = "model"; params = []; children } ]
let to_json ~no_value model scope_tokens =
let open Smtml in
let module Json = Yojson.Basic in
let symbol_to_json sym =
let name = ("symbol", `String (Symbol.to_string sym)) in
let ty = ("type", `String (Fmt.str "%a" Ty.pp sym.ty)) in
if no_value then `Assoc [ name; ty ]
else
let value = ("value", Value.to_json @@ get_value model sym) in
`Assoc [ name; ty; value ]
in
let rec process_scope scope_name tokens =
let rec collect_items acc tokens =
match tokens with
| [] ->
Logs.err (fun m -> m "Reached end without closing scope: %s" scope_name);
assert false
| Open_scope scope_name :: rest ->
(* Nested scope *)
let content, remaining = process_scope scope_name rest in
let json =
match content with
| `Assoc pairs :: [] ->
let obj = `Assoc pairs in
let scope_json = `Assoc [ ("scope", `String scope_name) ] in
Json.Util.combine obj scope_json
| _ ->
`Assoc [ ("scope", `String scope_name); ("content", `List content) ]
in
collect_items (json :: acc) remaining
| Symbol sym :: rest -> collect_items (symbol_to_json sym :: acc) rest
| Close_scope :: rest -> (List.rev acc, rest)
in
let content, rest = collect_items [] tokens in
(content, rest)
in
let rec process_tokens tokens acc =
match tokens with
| [] -> List.rev acc
| Open_scope scope_name :: rest -> (
let content, remaining = process_scope scope_name rest in
match content with
| `Assoc pairs :: [] ->
let obj = `Assoc pairs in
let scope_json = `Assoc [ ("scope", `String scope_name) ] in
process_tokens remaining (Json.Util.combine obj scope_json :: acc)
| _ ->
let json =
`Assoc [ ("scope", `String scope_name); ("content", `List content) ]
in
process_tokens remaining (json :: acc) )
| Symbol s :: rest -> process_tokens rest (symbol_to_json s :: acc)
| Close_scope :: _ ->
Log.err (fun m ->
m "Called close_scope without a corresponding open_scope" );
assert false
in
let rev_scope_tokens = List.rev scope_tokens in
Logs.debug (fun m -> m "Current scope tokens: [%a]" pp rev_scope_tokens);
let result = process_tokens rev_scope_tokens [] in
`Assoc [ ("model", `List result) ]
let model_of_json json_str =
let open Yojson.Basic in
let open Syntax in
let tbl = Hashtbl.create 16 in
let* json =
try Ok (from_string json_str)
with _ -> Fmt.error_msg "Invalid json string: %s" json_str
in
let rec process_json json =
match json with
| `Assoc obj :: rest when List.mem_assoc "symbol" obj ->
let obj = `Assoc obj in
let ty = Util.member "type" obj |> Util.to_string in
let* ty = Smtml.Ty.of_string ty in
let value =
match Util.member "value" obj with
| `Bool x -> Bool.to_string x
| `Float x -> Float.to_string x
| `Int x -> Int.to_string x
| `String x -> x
| _ -> assert false
in
let* value = Smtml.Value.of_string ty value in
let sym_name = Util.member "symbol" obj |> Util.to_string in
let key = Smtml.Symbol.make ty sym_name in
Hashtbl.add tbl key value;
process_json rest
| `Assoc obj :: rest when List.mem_assoc "scope" obj ->
let content = Util.member "content" (`Assoc obj) |> Util.to_list in
let* () = process_json content in
process_json rest
| _ :: _ -> assert false
| [] -> Ok ()
in
match json with
| `Assoc root -> (
match List.assoc_opt "model" root with
| Some items ->
let+ () = process_json (Util.to_list items) in
tbl
| None -> Fmt.error_msg "JSON does not contain model field" )
| _ ->
Fmt.error_msg "Invalid JSON format for symbol scope:@. %a"
(Yojson.Basic.pretty_print ~std:true)
json
let model_of_scfg scfg =
let open Scfg in
let open Syntax in
let tbl = Hashtbl.create 16 in
let rec process_dirs (dirs : Types.directive list) =
match dirs with
| dir :: rest when String.compare dir.name "symbol" = 0 ->
let* name = Scfg.Query.get_param 0 dir in
let* ty = Scfg.Query.get_param 1 dir in
let* ty = Smtml.Ty.of_string ty in
let* value = Scfg.Query.get_param 2 dir in
let* value = Smtml.Value.of_string ty value in
let key = Smtml.Symbol.make ty name in
Hashtbl.add tbl key value;
process_dirs rest
| dir :: rest when String.compare dir.name "scope" = 0 ->
let* () = process_dirs dir.children in
process_dirs rest
| _ :: rest -> process_dirs rest (* not scope or symbol *)
| [] -> Ok ()
in
let* scfg = Scfg.Parse.from_string scfg in
match Query.get_dir "model" scfg with
| Some model ->
let+ () = process_dirs model.children in
tbl
| None ->
Fmt.error_msg "Could not find the directive `model` in the scfg config"