Project

General

Profile

Download (11.7 KB) Statistics
| Branch: | Tag: | Revision:
1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
12 a2d97a3e ploc
(* Parts of this file come from the Prelude compiler *)
13 22fe1c93 ploc
14 8446bf03 ploc
(*open LustreSpec*)
15 22fe1c93 ploc
open Type_predef
16
open Clock_predef
17
open Delay_predef
18
open Dimension
19
module TE = Env
20
21 ca7ff3f7 Lélio Brun
let static_op ty = type_static (mkdim_var ()) ty
22 22fe1c93 ploc
23
let type_env =
24 e9b71779 tkahsai
  List.fold_left
25 5c1184ad ploc
    (fun env (op, op_type) -> TE.add_value env op op_type)
26
    TE.initial
27
    [
28 ca7ff3f7 Lélio Brun
      "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 e9b71779 tkahsai
50 22fe1c93 ploc
module CE = Env
51
52
let clock_env =
53
  let init_env = CE.initial in
54 ef34b4ae xthirioux
  let env' =
55 ca7ff3f7 Lélio Brun
    List.fold_right
56
      (fun op env -> CE.add_value env op ck_nullary_univ)
57
      [ "true"; "false" ] init_env
58
  in
59 e9b71779 tkahsai
  let env' =
60 ca7ff3f7 Lélio Brun
    List.fold_right
61
      (fun op env -> CE.add_value env op ck_unary_univ)
62
      [ "uminus"; "not" ] env'
63
  in
64 e9b71779 tkahsai
  let env' =
65 ca7ff3f7 Lélio Brun
    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 22fe1c93 ploc
  env'
88
89
module DE = Env
90
91
let delay_env =
92
  let init_env = DE.initial in
93 ef34b4ae xthirioux
  let env' =
94 ca7ff3f7 Lélio Brun
    List.fold_right
95
      (fun op env -> DE.add_value env op delay_nullary_poly_op)
96
      [ "true"; "false" ] init_env
97
  in
98 ef34b4ae xthirioux
  let env' =
99 ca7ff3f7 Lélio Brun
    List.fold_right
100
      (fun op env -> DE.add_value env op delay_unary_poly_op)
101
      [ "uminus"; "not" ] env'
102
  in
103 e9b71779 tkahsai
  let env' =
104 ca7ff3f7 Lélio Brun
    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 e9b71779 tkahsai
  let env' =
127 ca7ff3f7 Lélio Brun
    List.fold_right
128
      (fun op env -> DE.add_value env op delay_ternary_poly_op)
129
      [] env'
130
  in
131 22fe1c93 ploc
  env'
132
133
module VE = Env
134
135 2d2d89d7 ploc
let eval_dim_env =
136 ca7ff3f7 Lélio Brun
  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 5c1184ad ploc
  in
164 e9b71779 tkahsai
  List.fold_left
165 5c1184ad ploc
    (fun env (op, op_eval) -> VE.add_value env op op_eval)
166 ca7ff3f7 Lélio Brun
    VE.initial defs
167
168
let arith_funs = [ "+"; "-"; "*"; "/"; "mod"; "uminus" ]
169 22fe1c93 ploc
170 ca7ff3f7 Lélio Brun
let bool_funs = [ "&&"; "||"; "xor"; "equi"; "impl"; "not" ]
171
172
let rel_funs = [ "<"; ">"; "<="; ">="; "!="; "=" ]
173
174
let internal_funs = arith_funs @ bool_funs @ rel_funs
175 719f9992 xthirioux
176 04a63d25 xthirioux
let rec is_internal_fun x targs =
177 ca7ff3f7 Lélio Brun
  (*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*)
178 04a63d25 xthirioux
  match targs with
179 ca7ff3f7 Lélio Brun
  | [] ->
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 04a63d25 xthirioux
188
let is_expr_internal_fun expr =
189 8446bf03 ploc
  let open Lustre_types in
190 04a63d25 xthirioux
  match expr.expr_desc with
191 ca7ff3f7 Lélio Brun
  | Expr_appl (f, e, _) ->
192
    is_internal_fun f (Types.type_list_of_type e.expr_type)
193
  | _ ->
194
    assert false
195 04a63d25 xthirioux
196
let is_value_internal_fun v =
197 8446bf03 ploc
  let open Machine_code_types in
198 04a63d25 xthirioux
  match v.value_desc with
199 ca7ff3f7 Lélio Brun
  | Fun (f, vl) ->
200
    is_internal_fun f (List.map (fun v -> v.value_type) vl)
201
  | _ ->
202
    assert false
203 53206908 xthirioux
204 ca7ff3f7 Lélio Brun
let is_numeric_operator x = List.mem x arith_funs
205 04a63d25 xthirioux
206 ca7ff3f7 Lélio Brun
let is_homomorphic_fun x = List.mem x internal_funs
207 22fe1c93 ploc
208 ca7ff3f7 Lélio Brun
let is_stateless_fun x = List.mem x internal_funs
209 ea8f51ae ploc
210
(* let pp_java i pp_val fmt vl = *)
211
(*   match i, vl with *)
212 ca7ff3f7 Lélio Brun
(* (\* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1
213
   pp_val v2 pp_val v3 *\) *)
214 ea8f51ae ploc
(*     | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *)
215
(*     | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *)
216 ca7ff3f7 Lélio Brun
(* | "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 ea8f51ae ploc
225 ca7e8027 Lélio Brun
let partial_eval op e opt =
226 2d2d89d7 ploc
  let open Lustre_types in
227
  let is_zero e =
228
    match e.expr_desc with
229 ca7ff3f7 Lélio Brun
    | Expr_const (Const_int 0) ->
230
      true
231
    | Expr_const (Const_real r) when Real.is_zero r ->
232
      true
233
    | _ ->
234
      false
235 2d2d89d7 ploc
  in
236
  let is_one e =
237
    match e.expr_desc with
238 ca7ff3f7 Lélio Brun
    | Expr_const (Const_int 1) ->
239
      true
240
    | Expr_const (Const_real r) when Real.is_one r ->
241
      true
242
    | _ ->
243
      false
244 2d2d89d7 ploc
  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 ca7ff3f7 Lélio Brun
  let int_arith_op, real_arith_op =
250
    let assoc op =
251 2d2d89d7 ploc
      match op with
252 ca7ff3f7 Lélio Brun
      | "+" ->
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 2d2d89d7 ploc
    in
265 ca7ff3f7 Lélio Brun
    (fun op -> fst (assoc op)), fun op -> snd (assoc op)
266 2d2d89d7 ploc
  in
267
  let int_rel_op, real_rel_op =
268
    let assoc op =
269
      match op with
270 ca7ff3f7 Lélio Brun
      | "<" ->
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 2d2d89d7 ploc
    in
285 ca7ff3f7 Lélio Brun
    (fun op -> fst (assoc op)), fun op -> snd (assoc op)
286 2d2d89d7 ploc
  in
287 ca7ff3f7 Lélio Brun
  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 2d2d89d7 ploc
    let e1, e2 = s2b e1, s2b e2 in
294
    let r =
295
      match op with
296 ca7ff3f7 Lélio Brun
      | "&&" ->
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 2d2d89d7 ploc
    in
309
    if r then Const_tag tag_true else Const_tag tag_false
310
  in
311 ca7ff3f7 Lélio Brun
  let is_const e = match e.expr_desc with Expr_const _ -> true | _ -> false in
312 2d2d89d7 ploc
  let deconst e =
313 ca7ff3f7 Lélio Brun
    match e.expr_desc with Expr_const c -> c | _ -> assert false
314 2d2d89d7 ploc
  in
315 ca7ff3f7 Lélio Brun
  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 2d2d89d7 ploc
      match op, List.map deconst el with
319 ca7ff3f7 Lélio Brun
      | ("+" | "-" | "*" | "/" | "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 2d2d89d7 ploc
    in
353 ca7ff3f7 Lélio Brun
    Expr_const new_cst
354
  | op, el -> (
355
    (* at least one of the arguments is non constant *)
356 2d2d89d7 ploc
    match op, el with
357 ca7ff3f7 Lélio Brun
    | "+", [ 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 2d2d89d7 ploc
    | _ ->
384 ca7ff3f7 Lélio Brun
      Expr_appl (op, e, opt))
385 04a188ec ploc
386 ca7ff3f7 Lélio Brun
(* Local Variables: *)
387
(* compile-command:"make -C .." *)
388
(* End: *)
389 04a188ec ploc
390
let _ =
391
  (* Loading environement *)
392
  Global.type_env := type_env;
393
  Global.clock_env := clock_env