Source file socExecEvalPredef.ml
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
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
open SocExecValue
open Data
open Soc
let type_error v1 v2 =
Printf.eprintf "Runtime error: '%s' and '%s' have different types.\n"
(Data.val_to_string string_of_float v1) (Data.val_to_string string_of_float v2);
flush stderr;
exit 2
let type_error1 v1 str =
Printf.eprintf "Runtime error: '%s' is not a '%s'\n"
(Data.val_to_string string_of_float v1) str;
flush stderr;
exit 2
let type_error2 v1 v2 str =
Printf.eprintf "Runtime error: '%s' and/or '%s' are/is not a %s\n"
(Data.val_to_string string_of_float v1) (Data.val_to_string string_of_float v2) str;
flush stderr;
exit 2
let (lustre_plus : ctx -> ctx) =
fun ctx ->
let l = [get_val "i1" ctx; get_val "i2" ctx] in
let (vn,vv) =
match l with
| [I x1; I x2] -> "out"::ctx.cpath,I(x1+x2)
| [F i1; F i2] -> "out"::ctx.cpath,F(i1+.i2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_times ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [I x1; I x2] -> "out"::ctx.cpath,I(x1 * x2)
| [F x1; F x2] -> "out"::ctx.cpath,F(x1 *. x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_div ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [I x1; I x2] -> "out"::ctx.cpath,I(x1 / x2)
| [F x1; F x2] -> "out"::ctx.cpath,F(x1 /. x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_slash ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [I x1; I x2] -> "out"::ctx.cpath,I(x1 / x2)
| [F x1; F x2] -> "out"::ctx.cpath,F(x1 /. x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_minus ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [I x1; I x2] -> "out"::ctx.cpath,I(x1 - x2)
| [F x1; F x2] -> "out"::ctx.cpath,F(x1 -. x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_mod ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [I x1; I x2] -> "out"::ctx.cpath,I(x1 mod x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_eq ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [x1; x2] -> "out"::ctx.cpath,B(x1 = x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_uminus ctx =
let (vn,vv) =
match ([get_val "i1" ctx]) with
| [I x1] -> "out"::ctx.cpath,I(- x1)
| [F x1] -> "out"::ctx.cpath,F(-. x1)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1] -> type_error1 v1 "numeric"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_real2int ctx =
let (vn,vv) =
match ([get_val "i1" ctx]) with
| [F x1] -> "out"::ctx.cpath,I(int_of_float x1)
| [U] -> "out"::ctx.cpath,U
| [v1] -> type_error1 v1 "real"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_int2real ctx =
let (vn,vv) =
match ([get_val "i1" ctx]) with
| [I x1] -> "out"::ctx.cpath,F(float_of_int x1)
| [U] -> "out"::ctx.cpath,U
| [v1] -> type_error1 v1 "int"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_not ctx =
let (vn,vv) =
match ([get_val "i1" ctx]) with
| [B x1] -> "out"::ctx.cpath,B(not x1)
| [U] -> "out"::ctx.cpath,U
| [v1] -> type_error1 v1 "bool"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_lt ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [x1; x2] -> "out"::ctx.cpath,B(x1 < x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_gt ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [x1; x2] -> "out"::ctx.cpath,B(x1 > x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_lte ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [x1; x2] -> "out"::ctx.cpath,B(x1 <= x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_gte ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [x1; x2] -> "out"::ctx.cpath,B(x1 >= x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_and ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [B x1; B x2] -> "out"::ctx.cpath,B(x1 && x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_xor ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [B x1; B x2] -> "out"::ctx.cpath,B(x1 <> x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_neq ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [x1; x2] -> "out"::ctx.cpath,B(x1 <> x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_or ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [B x1; B x2] -> "out"::ctx.cpath,B(x1 || x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_impl ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [B x1; B x2] -> "out"::ctx.cpath,B(not x1 || x2)
| [U; _] | [_;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error2 v1 v2 "bool"
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_if ctx =
let (vn,vv) =
match ([get_val "cond" ctx; get_val "xthen" ctx; get_val "xelse" ctx]) with
| [B c; v1; v2] -> "out"::ctx.cpath, if c then v1 else v2
| [U;_; _] | [_;U;U] -> "out"::ctx.cpath,U
| [v1;v2] -> type_error v1 v2
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let make_names str start stop =
let res = ref [] in
for k=stop downto start do
res:= (str^(string_of_int k)) :: !res;
done;
!res
let lustre_array tl ctx =
let _t,size = match List.hd (List.rev tl) with
| Data.Array(t,i) -> t,i
| _ -> assert false
in
let inames = make_names "i" 1 size in
let l = List.map (fun name -> get_val name ctx) inames in
let a = Array.of_list l in
{ ctx with s = sadd ctx.s ("out"::ctx.cpath) (A a) }
let lustre_slice tl si_opt ctx =
let _t,size = match List.hd (List.rev tl) with
| Data.Array(t,i) -> t,i
| _ -> assert false
in
let (vn,vv) =
match ([get_val "i1" ctx], si_opt) with
| [A a],Slic(b,e,step) ->
let a_res = Array.make size a.(0) in
let j=ref 0 in
for i = b to e do
if (i-b) mod step = 0 then (
a_res.(!j) <- a.(i);
incr j
);
done;
"out"::ctx.cpath, A (a_res)
| [U],_ -> "out"::ctx.cpath, U
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_concat ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx]) with
| [A a1; A a2] -> "out"::ctx.cpath, A (Array.append a1 a2)
| [U;_] | [_;U] -> "out"::ctx.cpath, U
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let lustre_arrow ctx =
let (vn,vv) =
match ([get_val "i1" ctx; get_val "i2" ctx;
get_val "_memory" { ctx with cpath=ctx.cpath}])
with
| [v1;v2; fs] -> "out"::ctx.cpath, if fs=B false then v2 else v1
| _ -> assert false
in
let ctx = { ctx with s = sadd ctx.s vn vv } in
let ctx = { ctx with s = sadd ctx.s ("_memory"::ctx.cpath) (B false) } in
ctx
let lustre_hat tl ctx =
let i = match tl with
| [_;Data.Array(_,i)] -> i
| _ -> assert false
in
let (vn,vv) =
match ([get_val "i1" ctx]) with
| [U] -> "out"::ctx.cpath,U
| [v] -> "out"::ctx.cpath,A(Array.make i v)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
let (get: Soc.key -> (ctx -> ctx)) =
fun (n,tl,si_opt) ->
match n with
| "Lustre::rplus"
| "Lustre::iplus"
| "Lustre::plus" -> lustre_plus
| "Lustre::itimes"
| "Lustre::rtimes"
| "Lustre::times"-> lustre_times
| "Lustre::idiv"
| "Lustre::rdiv"
| "Lustre::div" -> lustre_div
| "Lustre::slash" | "Lustre::islash" | "Lustre::rslash" -> lustre_slash
| "Lustre::iminus"
| "Lustre::rminus"
| "Lustre::minus"-> lustre_minus
| "Lustre::mod" -> lustre_mod
| "Lustre::iuminus"
| "Lustre::ruminus"
| "Lustre::uminus" -> lustre_uminus
| "Lustre::not" -> lustre_not
| "Lustre::real2int" -> lustre_real2int
| "Lustre::int2real" -> lustre_int2real
| "Lustre::lt"| "Lustre::rlt" | "Lustre::ilt" -> lustre_lt
| "Lustre::gt"| "Lustre::rgt" | "Lustre::igt" -> lustre_gt
| "Lustre::lte"| "Lustre::rlte" | "Lustre::ilte" -> lustre_lte
| "Lustre::gte"| "Lustre::rgte"| "Lustre::igte" -> lustre_gte
| "Lustre::xor" -> lustre_xor
| "Lustre::and" -> lustre_and
| "Lustre::eq" -> lustre_eq
| "Lustre::neq" -> lustre_neq
| "Lustre::or" -> lustre_or
| "Lustre::impl" -> lustre_impl
| "Lustre::if"| "Lustre::rif"| "Lustre::iif" -> lustre_if
| "Lustre::hat" -> lustre_hat tl
| "Lustre::array" -> lustre_array tl
| "Lustre::concat" -> lustre_concat
| "Lustre::arrow" -> lustre_arrow
| "Lustre::current" -> assert false
| "Lustre::array_slice" -> lustre_slice tl si_opt
| "Lustre::nor" -> assert false
| "Lustre::diese" -> assert false
| _ -> raise Not_found