|
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
|
|
|
20
|
module TE = Env
|
|
21
|
|
|
22
|
let static_op ty =
|
|
23
|
type_static (mkdim_var ()) ty
|
|
24
|
|
|
25
|
let type_env =
|
|
26
|
List.fold_left
|
|
27
|
(fun env (op, op_type) -> TE.add_value env op op_type)
|
|
28
|
TE.initial
|
|
29
|
[
|
|
30
|
"true", (static_op type_bool);
|
|
31
|
"false", (static_op type_bool);
|
|
32
|
"+", (static_op type_bin_poly_op);
|
|
33
|
"uminus", (static_op type_unary_poly_op);
|
|
34
|
"-", (static_op type_bin_poly_op);
|
|
35
|
"*", (static_op type_bin_poly_op);
|
|
36
|
"/", (static_op type_bin_poly_op);
|
|
37
|
"mod", (static_op type_bin_int_op);
|
|
38
|
"&&", (static_op type_bin_bool_op);
|
|
39
|
"||", (static_op type_bin_bool_op);
|
|
40
|
"xor", (static_op type_bin_bool_op);
|
|
41
|
"equi", (static_op type_bin_bool_op);
|
|
42
|
"impl", (static_op type_bin_bool_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
|
"!=", (static_op type_bin_comp_op);
|
|
48
|
"=", (static_op type_bin_comp_op);
|
|
49
|
"not", (static_op type_unary_bool_op)
|
|
50
|
]
|
|
51
|
|
|
52
|
module CE = Env
|
|
53
|
|
|
54
|
let clock_env =
|
|
55
|
let init_env = CE.initial in
|
|
56
|
let env' =
|
|
57
|
List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ)
|
|
58
|
["true"; "false"] init_env in
|
|
59
|
let env' =
|
|
60
|
List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
|
|
61
|
["uminus"; "not"] env' in
|
|
62
|
let env' =
|
|
63
|
List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
|
|
64
|
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
|
|
65
|
env'
|
|
66
|
|
|
67
|
module DE = Env
|
|
68
|
|
|
69
|
let delay_env =
|
|
70
|
let init_env = DE.initial in
|
|
71
|
let env' =
|
|
72
|
List.fold_right (fun op env -> DE.add_value env op delay_nullary_poly_op)
|
|
73
|
["true"; "false"] init_env in
|
|
74
|
let env' =
|
|
75
|
List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
|
|
76
|
["uminus"; "not"] env' in
|
|
77
|
let env' =
|
|
78
|
List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
|
|
79
|
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
|
|
80
|
let env' =
|
|
81
|
List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
|
|
82
|
[] env' in
|
|
83
|
env'
|
|
84
|
|
|
85
|
module VE = Env
|
|
86
|
|
|
87
|
let eval_env =
|
|
88
|
let defs = [
|
|
89
|
"uminus", (function [Dint a] -> Dint (-a) | _ -> assert false);
|
|
90
|
"not", (function [Dbool b] -> Dbool (not b) | _ -> assert false);
|
|
91
|
"+", (function [Dint a; Dint b] -> Dint (a+b) | _ -> assert false);
|
|
92
|
"-", (function [Dint a; Dint b] -> Dint (a-b) | _ -> assert false);
|
|
93
|
"*", (function [Dint a; Dint b] -> Dint (a*b) | _ -> assert false);
|
|
94
|
"/", (function [Dint a; Dint b] -> Dint (a/b) | _ -> assert false);
|
|
95
|
"mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false);
|
|
96
|
"&&", (function [Dbool a; Dbool b] -> Dbool (a&&b) | _ -> assert false);
|
|
97
|
"||", (function [Dbool a; Dbool b] -> Dbool (a||b) | _ -> assert false);
|
|
98
|
"xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);
|
|
99
|
"equi", (function [Dbool a; Dbool b] -> Dbool (a=b) | _ -> assert false);
|
|
100
|
"impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false);
|
|
101
|
"<", (function [Dint a; Dint b] -> Dbool (a<b) | _ -> assert false);
|
|
102
|
">", (function [Dint a; Dint b] -> Dbool (a>b) | _ -> assert false);
|
|
103
|
"<=", (function [Dint a; Dint b] -> Dbool (a<=b) | _ -> assert false);
|
|
104
|
">=", (function [Dint a; Dint b] -> Dbool (a>=b) | _ -> assert false);
|
|
105
|
"!=", (function [a; b] -> Dbool (a<>b) | _ -> assert false);
|
|
106
|
"=", (function [a; b] -> Dbool (a=b) | _ -> assert false);
|
|
107
|
]
|
|
108
|
in
|
|
109
|
List.fold_left
|
|
110
|
(fun env (op, op_eval) -> VE.add_value env op op_eval)
|
|
111
|
VE.initial
|
|
112
|
defs
|
|
113
|
|
|
114
|
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"equi";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
|
|
115
|
|
|
116
|
let is_internal_fun x =
|
|
117
|
List.mem x internal_funs
|
|
118
|
|
|
119
|
let pp_c i pp_val fmt vl =
|
|
120
|
match i, vl with
|
|
121
|
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
|
|
122
|
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
|
|
123
|
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
|
|
124
|
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
|
|
125
|
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
|
|
126
|
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
|
|
127
|
| "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
|
|
128
|
| "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
|
|
129
|
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
|
|
130
|
| _ -> failwith i
|
|
131
|
|
|
132
|
let pp_java i pp_val fmt vl =
|
|
133
|
match i, vl with
|
|
134
|
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
|
|
135
|
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
|
|
136
|
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
|
|
137
|
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
|
|
138
|
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
|
|
139
|
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
|
|
140
|
| "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
|
|
141
|
| "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
|
|
142
|
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
|
|
143
|
| _ -> assert false
|
|
144
|
|
|
145
|
let pp_horn i pp_val fmt vl =
|
|
146
|
match i, vl with
|
|
147
|
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
|
|
148
|
|
|
149
|
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
|
|
150
|
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
|
|
151
|
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
|
|
152
|
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
|
|
153
|
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
|
|
154
|
| "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
|
|
155
|
| "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
|
|
156
|
| "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
|
|
157
|
| "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
|
|
158
|
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
|
|
159
|
| "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
|
|
160
|
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
|
|
161
|
| _ -> assert false
|
|
162
|
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
|
|
163
|
|
|
164
|
*)
|
|
165
|
|
|
166
|
(* Local Variables: *)
|
|
167
|
(* compile-command:"make -C .." *)
|
|
168
|
(* End: *)
|