lustrec / src / basic_library.ml @ ef8a361a
History | View | Annotate | Download (8.39 KB)
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 arith_funs = ["+";"-";"*";"/";"mod"; "uminus"] |
115 |
let bool_funs = ["&&";"||";"xor";"equi";"impl"; "not"] |
116 |
let rel_funs = ["<";">";"<=";">=";"!=";"="] |
117 |
|
118 |
let internal_funs = arith_funs@bool_funs@rel_funs |
119 |
|
120 |
let rec is_internal_fun x targs = |
121 |
(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*) |
122 |
match targs with |
123 |
| [] -> assert false |
124 |
| t::_ when Types.is_real_type t -> List.mem x internal_funs && not !Options.mpfr |
125 |
| t::_ when Types.is_array_type t -> is_internal_fun x [Types.array_element_type t] |
126 |
| _ -> List.mem x internal_funs |
127 |
|
128 |
let is_expr_internal_fun expr = |
129 |
match expr.expr_desc with |
130 |
| Expr_appl (f, e, _) -> is_internal_fun f (Types.type_list_of_type e.expr_type) |
131 |
| _ -> assert false |
132 |
|
133 |
let is_value_internal_fun v = |
134 |
match v.value_desc with |
135 |
| Fun (f, vl) -> is_internal_fun f (List.map (fun v -> v.value_type) vl) |
136 |
| _ -> assert false |
137 |
|
138 |
let is_numeric_operator x = |
139 |
List.mem x arith_funs |
140 |
|
141 |
let is_homomorphic_fun x = |
142 |
List.mem x internal_funs |
143 |
|
144 |
let is_stateless_fun x = |
145 |
List.mem x internal_funs |
146 |
|
147 |
let pp_c i pp_val fmt vl = |
148 |
match i, vl with |
149 |
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *) |
150 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
151 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v |
152 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
153 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
154 |
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
155 |
| "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2 |
156 |
| "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2 |
157 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
158 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false) |
159 |
|
160 |
let pp_java i pp_val fmt vl = |
161 |
match i, vl with |
162 |
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *) |
163 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
164 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v |
165 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
166 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
167 |
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
168 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
169 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 |
170 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
171 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) |
172 |
|
173 |
let pp_horn i pp_val fmt vl = |
174 |
match i, vl with |
175 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 |
176 |
|
177 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
178 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v |
179 |
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 |
180 |
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 |
181 |
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 |
182 |
| "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 |
183 |
| "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 |
184 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 |
185 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 |
186 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
187 |
| "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
188 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
189 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false) |
190 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
191 |
|
192 |
*) |
193 |
|
194 |
(* Local Variables: *) |
195 |
(* compile-command:"make -C .." *) |
196 |
(* End: *) |