1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
(* Parts of this file come from the Prelude compiler *)
|
13
|
|
14
|
(*open LustreSpec*)
|
15
|
open Type_predef
|
16
|
open Clock_predef
|
17
|
open Delay_predef
|
18
|
open Dimension
|
19
|
module TE = Env
|
20
|
|
21
|
let static_op ty = type_static (mkdim_var ()) ty
|
22
|
|
23
|
let type_env =
|
24
|
List.fold_left
|
25
|
(fun env (op, op_type) -> TE.add_value env op op_type)
|
26
|
TE.initial
|
27
|
[
|
28
|
"true", static_op type_bool;
|
29
|
"false", static_op type_bool;
|
30
|
"+", static_op type_bin_poly_op;
|
31
|
"uminus", static_op type_unary_poly_op;
|
32
|
"-", static_op type_bin_poly_op;
|
33
|
"*", static_op type_bin_poly_op;
|
34
|
"/", static_op type_bin_poly_op;
|
35
|
"mod", static_op type_bin_int_op;
|
36
|
"&&", static_op type_bin_bool_op;
|
37
|
"||", static_op type_bin_bool_op;
|
38
|
"xor", static_op type_bin_bool_op;
|
39
|
"equi", static_op type_bin_bool_op;
|
40
|
"impl", static_op type_bin_bool_op;
|
41
|
"<", static_op type_bin_comp_op;
|
42
|
"<=", static_op type_bin_comp_op;
|
43
|
">", static_op type_bin_comp_op;
|
44
|
">=", static_op type_bin_comp_op;
|
45
|
"!=", static_op type_bin_comp_op;
|
46
|
"=", static_op type_bin_comp_op;
|
47
|
"not", static_op type_unary_bool_op;
|
48
|
]
|
49
|
|
50
|
module CE = Env
|
51
|
|
52
|
let clock_env =
|
53
|
let init_env = CE.initial in
|
54
|
let env' =
|
55
|
List.fold_right
|
56
|
(fun op env -> CE.add_value env op ck_nullary_univ)
|
57
|
[ "true"; "false" ] init_env
|
58
|
in
|
59
|
let env' =
|
60
|
List.fold_right
|
61
|
(fun op env -> CE.add_value env op ck_unary_univ)
|
62
|
[ "uminus"; "not" ] env'
|
63
|
in
|
64
|
let env' =
|
65
|
List.fold_right
|
66
|
(fun op env -> CE.add_value env op ck_bin_univ)
|
67
|
[
|
68
|
"+";
|
69
|
"-";
|
70
|
"*";
|
71
|
"/";
|
72
|
"mod";
|
73
|
"&&";
|
74
|
"||";
|
75
|
"xor";
|
76
|
"equi";
|
77
|
"impl";
|
78
|
"<";
|
79
|
"<=";
|
80
|
">";
|
81
|
">=";
|
82
|
"!=";
|
83
|
"=";
|
84
|
]
|
85
|
env'
|
86
|
in
|
87
|
env'
|
88
|
|
89
|
module DE = Env
|
90
|
|
91
|
let delay_env =
|
92
|
let init_env = DE.initial in
|
93
|
let env' =
|
94
|
List.fold_right
|
95
|
(fun op env -> DE.add_value env op delay_nullary_poly_op)
|
96
|
[ "true"; "false" ] init_env
|
97
|
in
|
98
|
let env' =
|
99
|
List.fold_right
|
100
|
(fun op env -> DE.add_value env op delay_unary_poly_op)
|
101
|
[ "uminus"; "not" ] env'
|
102
|
in
|
103
|
let env' =
|
104
|
List.fold_right
|
105
|
(fun op env -> DE.add_value env op delay_binary_poly_op)
|
106
|
[
|
107
|
"+";
|
108
|
"-";
|
109
|
"*";
|
110
|
"/";
|
111
|
"mod";
|
112
|
"&&";
|
113
|
"||";
|
114
|
"xor";
|
115
|
"equi";
|
116
|
"impl";
|
117
|
"<";
|
118
|
"<=";
|
119
|
">";
|
120
|
">=";
|
121
|
"!=";
|
122
|
"=";
|
123
|
]
|
124
|
env'
|
125
|
in
|
126
|
let env' =
|
127
|
List.fold_right
|
128
|
(fun op env -> DE.add_value env op delay_ternary_poly_op)
|
129
|
[] env'
|
130
|
in
|
131
|
env'
|
132
|
|
133
|
module VE = Env
|
134
|
|
135
|
let eval_dim_env =
|
136
|
let defs =
|
137
|
[
|
138
|
("uminus", function [ Dint a ] -> Dint (-a) | _ -> assert false);
|
139
|
("not", function [ Dbool b ] -> Dbool (not b) | _ -> assert false);
|
140
|
("+", function [ Dint a; Dint b ] -> Dint (a + b) | _ -> assert false);
|
141
|
("-", function [ Dint a; Dint b ] -> Dint (a - b) | _ -> assert false);
|
142
|
("*", function [ Dint a; Dint b ] -> Dint (a * b) | _ -> assert false);
|
143
|
("/", function [ Dint a; Dint b ] -> Dint (a / b) | _ -> assert false);
|
144
|
( "mod",
|
145
|
function [ Dint a; Dint b ] -> Dint (a mod b) | _ -> assert false );
|
146
|
( "&&",
|
147
|
function [ Dbool a; Dbool b ] -> Dbool (a && b) | _ -> assert false );
|
148
|
( "||",
|
149
|
function [ Dbool a; Dbool b ] -> Dbool (a || b) | _ -> assert false );
|
150
|
( "xor",
|
151
|
function [ Dbool a; Dbool b ] -> Dbool (a <> b) | _ -> assert false );
|
152
|
( "equi",
|
153
|
function [ Dbool a; Dbool b ] -> Dbool (a = b) | _ -> assert false );
|
154
|
( "impl",
|
155
|
function [ Dbool a; Dbool b ] -> Dbool (a <= b) | _ -> assert false );
|
156
|
("<", function [ Dint a; Dint b ] -> Dbool (a < b) | _ -> assert false);
|
157
|
(">", function [ Dint a; Dint b ] -> Dbool (a > b) | _ -> assert false);
|
158
|
("<=", function [ Dint a; Dint b ] -> Dbool (a <= b) | _ -> assert false);
|
159
|
(">=", function [ Dint a; Dint b ] -> Dbool (a >= b) | _ -> assert false);
|
160
|
("!=", function [ a; b ] -> Dbool (a <> b) | _ -> assert false);
|
161
|
("=", function [ a; b ] -> Dbool (a = b) | _ -> assert false);
|
162
|
]
|
163
|
in
|
164
|
List.fold_left
|
165
|
(fun env (op, op_eval) -> VE.add_value env op op_eval)
|
166
|
VE.initial defs
|
167
|
|
168
|
let arith_funs = [ "+"; "-"; "*"; "/"; "mod"; "uminus" ]
|
169
|
|
170
|
let bool_funs = [ "&&"; "||"; "xor"; "equi"; "impl"; "not" ]
|
171
|
|
172
|
let rel_funs = [ "<"; ">"; "<="; ">="; "!="; "=" ]
|
173
|
|
174
|
let internal_funs = arith_funs @ bool_funs @ rel_funs
|
175
|
|
176
|
let rec is_internal_fun x targs =
|
177
|
(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*)
|
178
|
match targs with
|
179
|
| [] ->
|
180
|
assert false
|
181
|
| t :: _ when Types.is_real_type t ->
|
182
|
List.mem x internal_funs && not !Options.mpfr
|
183
|
| t :: _ when Types.is_array_type t ->
|
184
|
is_internal_fun x [ Types.array_element_type t ]
|
185
|
| _ ->
|
186
|
List.mem x internal_funs
|
187
|
|
188
|
let is_expr_internal_fun expr =
|
189
|
let open Lustre_types in
|
190
|
match expr.expr_desc with
|
191
|
| Expr_appl (f, e, _) ->
|
192
|
is_internal_fun f (Types.type_list_of_type e.expr_type)
|
193
|
| _ ->
|
194
|
assert false
|
195
|
|
196
|
let is_value_internal_fun v =
|
197
|
let open Machine_code_types in
|
198
|
match v.value_desc with
|
199
|
| Fun (f, vl) ->
|
200
|
is_internal_fun f (List.map (fun v -> v.value_type) vl)
|
201
|
| _ ->
|
202
|
assert false
|
203
|
|
204
|
let is_numeric_operator x = List.mem x arith_funs
|
205
|
|
206
|
let is_homomorphic_fun x = List.mem x internal_funs
|
207
|
|
208
|
let is_stateless_fun x = List.mem x internal_funs
|
209
|
|
210
|
(* let pp_java i pp_val fmt vl = *)
|
211
|
(* match i, vl with *)
|
212
|
(* (\* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1
|
213
|
pp_val v2 pp_val v3 *\) *)
|
214
|
(* | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *)
|
215
|
(* | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *)
|
216
|
(* | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *)
|
217
|
(* | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
|
218
|
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *)
|
219
|
(* | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
|
220
|
(* | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *)
|
221
|
(* | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *)
|
222
|
(* | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert
|
223
|
false) *)
|
224
|
|
225
|
let partial_eval op e opt =
|
226
|
let open Lustre_types in
|
227
|
let is_zero e =
|
228
|
match e.expr_desc with
|
229
|
| Expr_const (Const_int 0) ->
|
230
|
true
|
231
|
| Expr_const (Const_real r) when Real.is_zero r ->
|
232
|
true
|
233
|
| _ ->
|
234
|
false
|
235
|
in
|
236
|
let is_one e =
|
237
|
match e.expr_desc with
|
238
|
| Expr_const (Const_int 1) ->
|
239
|
true
|
240
|
| Expr_const (Const_real r) when Real.is_one r ->
|
241
|
true
|
242
|
| _ ->
|
243
|
false
|
244
|
in
|
245
|
let is_true, is_false =
|
246
|
let is_tag t e = e.expr_desc = Expr_const (Const_tag t) in
|
247
|
is_tag tag_true, is_tag tag_false
|
248
|
in
|
249
|
let int_arith_op, real_arith_op =
|
250
|
let assoc op =
|
251
|
match op with
|
252
|
| "+" ->
|
253
|
( + ), Real.add
|
254
|
| "-" ->
|
255
|
( - ), Real.minus
|
256
|
| "*" ->
|
257
|
( * ), Real.times
|
258
|
| "/" ->
|
259
|
( / ), Real.div
|
260
|
| "mod" ->
|
261
|
( mod ), fun _ _ -> assert false
|
262
|
| _ ->
|
263
|
assert false
|
264
|
in
|
265
|
(fun op -> fst (assoc op)), fun op -> snd (assoc op)
|
266
|
in
|
267
|
let int_rel_op, real_rel_op =
|
268
|
let assoc op =
|
269
|
match op with
|
270
|
| "<" ->
|
271
|
( < ), Real.lt
|
272
|
| ">" ->
|
273
|
( > ), Real.gt
|
274
|
| "<=" ->
|
275
|
( <= ), Real.le
|
276
|
| ">=" ->
|
277
|
( >= ), Real.ge
|
278
|
| "!=" ->
|
279
|
( != ), Real.diseq
|
280
|
| "=" ->
|
281
|
( = ), Real.eq
|
282
|
| _ ->
|
283
|
assert false
|
284
|
in
|
285
|
(fun op -> fst (assoc op)), fun op -> snd (assoc op)
|
286
|
in
|
287
|
let eval_bool_fun op e1 e2 =
|
288
|
let s2b s =
|
289
|
if s = tag_true then true
|
290
|
else if s = tag_false then false
|
291
|
else assert false
|
292
|
in
|
293
|
let e1, e2 = s2b e1, s2b e2 in
|
294
|
let r =
|
295
|
match op with
|
296
|
| "&&" ->
|
297
|
e1 && e2
|
298
|
| "||" ->
|
299
|
e1 || e2
|
300
|
| "xor" ->
|
301
|
(e1 && e2) || ((not e1) && not e2)
|
302
|
| "impl" ->
|
303
|
(not e1) || e2
|
304
|
| "equi" ->
|
305
|
((not e1) || e2) && ((not e2) || e1)
|
306
|
| _ ->
|
307
|
assert false
|
308
|
in
|
309
|
if r then Const_tag tag_true else Const_tag tag_false
|
310
|
in
|
311
|
let is_const e = match e.expr_desc with Expr_const _ -> true | _ -> false in
|
312
|
let deconst e =
|
313
|
match e.expr_desc with Expr_const c -> c | _ -> assert false
|
314
|
in
|
315
|
match op, match e.expr_desc with Expr_tuple el -> el | _ -> [ e ] with
|
316
|
| _, el when List.for_all is_const el ->
|
317
|
let new_cst =
|
318
|
match op, List.map deconst el with
|
319
|
| ("+" | "-" | "*" | "/" | "mod"), [ Const_int c1; Const_int c2 ] ->
|
320
|
Const_int (int_arith_op op c1 c2)
|
321
|
| ("+" | "-" | "*" | "/"), [ Const_real c1; Const_real c2 ] ->
|
322
|
Const_real (real_arith_op op c1 c2)
|
323
|
| "uminus", [ Const_int c ] ->
|
324
|
Const_int (-c)
|
325
|
| "uminus", [ Const_real c ] ->
|
326
|
Const_real (Real.uminus c)
|
327
|
| rel_fun, [ Const_int c1; Const_int c2 ] when List.mem rel_fun rel_funs
|
328
|
->
|
329
|
if int_rel_op op c1 c2 then Const_tag tag_true else Const_tag tag_false
|
330
|
| rel_fun, [ Const_real c1; Const_real c2 ] when List.mem rel_fun rel_funs
|
331
|
->
|
332
|
if real_rel_op op c1 c2 then Const_tag tag_true else Const_tag tag_false
|
333
|
| "=", [ Const_tag t1; Const_tag t2 ] ->
|
334
|
if t1 = t2 then Const_tag tag_true else Const_tag tag_false
|
335
|
| "!=", [ Const_tag t1; Const_tag t2 ] ->
|
336
|
if t1 = t2 then Const_tag tag_false else Const_tag tag_true
|
337
|
| "not", [ Const_tag c ] ->
|
338
|
Const_tag
|
339
|
(if c = tag_true then tag_false
|
340
|
else if c = tag_false then tag_true
|
341
|
else assert false)
|
342
|
| bool_fun, [ Const_tag c1; Const_tag c2 ]
|
343
|
when List.mem bool_fun bool_funs ->
|
344
|
eval_bool_fun bool_fun c1 c2
|
345
|
| _ ->
|
346
|
let loc = e.expr_loc in
|
347
|
let err =
|
348
|
Error.Unbound_symbol
|
349
|
(op ^ string_of_bool (List.mem op rel_funs) ^ " in basic library")
|
350
|
in
|
351
|
raise (Error.Error (loc, err))
|
352
|
in
|
353
|
Expr_const new_cst
|
354
|
| op, el -> (
|
355
|
(* at least one of the arguments is non constant *)
|
356
|
match op, el with
|
357
|
| "+", [ e0; e ] when is_zero e0 ->
|
358
|
e.expr_desc
|
359
|
| "+", [ e; e0 ] when is_zero e0 ->
|
360
|
e.expr_desc
|
361
|
| "-", [ e; e0 ] when is_zero e0 ->
|
362
|
e.expr_desc
|
363
|
| "-", [ e0; e ] when is_zero e0 ->
|
364
|
Expr_appl ("uminus", e, None)
|
365
|
| ("*" | "/"), [ e0; _ ] when is_zero e0 ->
|
366
|
e0.expr_desc
|
367
|
| "*", [ _; e0 ] when is_zero e0 ->
|
368
|
e0.expr_desc
|
369
|
| "*", [ e1; e ] when is_one e1 ->
|
370
|
e.expr_desc
|
371
|
| "/", [ e; e1 ] when is_one e1 ->
|
372
|
e.expr_desc
|
373
|
| "&&", [ efalse; _ ] when is_false efalse ->
|
374
|
Expr_const (Const_tag tag_false)
|
375
|
| "&&", [ _; efalse ] when is_false efalse ->
|
376
|
Expr_const (Const_tag tag_false)
|
377
|
| "||", [ etrue; _ ] when is_true etrue ->
|
378
|
Expr_const (Const_tag tag_true)
|
379
|
| "||", [ _; etrue ] when is_true etrue ->
|
380
|
Expr_const (Const_tag tag_true)
|
381
|
| "impl", [ efalse; _ ] when is_false efalse ->
|
382
|
Expr_const (Const_tag tag_true)
|
383
|
| _ ->
|
384
|
Expr_appl (op, e, opt))
|
385
|
|
386
|
(* Local Variables: *)
|
387
|
(* compile-command:"make -C .." *)
|
388
|
(* End: *)
|
389
|
|
390
|
let _ =
|
391
|
(* Loading environement *)
|
392
|
Global.type_env := type_env;
|
393
|
Global.clock_env := clock_env
|