lustrec / src / basic_library.ml @ df647a81
History | View | Annotate | Download (8.69 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
5 |
* |
6 |
* This file is part of Prelude |
7 |
* |
8 |
* Prelude is free software; you can redistribute it and/or |
9 |
* modify it under the terms of the GNU Lesser General Public License |
10 |
* as published by the Free Software Foundation ; either version 2 of |
11 |
* the License, or (at your option) any later version. |
12 |
* |
13 |
* Prelude is distributed in the hope that it will be useful, but |
14 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
15 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
16 |
* Lesser General Public License for more details. |
17 |
* |
18 |
* You should have received a copy of the GNU Lesser General Public |
19 |
* License along with this program ; if not, write to the Free Software |
20 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
21 |
* USA |
22 |
*---------------------------------------------------------------------------- *) |
23 |
|
24 |
(* This module is used for the lustre to C compiler *) |
25 |
|
26 |
open Type_predef |
27 |
open Clock_predef |
28 |
open Delay_predef |
29 |
open Dimension |
30 |
|
31 |
module TE = Env |
32 |
|
33 |
let static_op ty = |
34 |
type_static (mkdim_var ()) ty |
35 |
|
36 |
let type_env = |
37 |
List.fold_left |
38 |
(fun env (op, op_type) -> TE.add_value env op op_type) |
39 |
TE.initial |
40 |
[ |
41 |
"+", (static_op type_bin_poly_op); |
42 |
"uminus", (static_op type_unary_poly_op); |
43 |
"-", (static_op type_bin_poly_op); |
44 |
"*", (static_op type_bin_poly_op); |
45 |
"/", (static_op type_bin_poly_op); |
46 |
"mod", (static_op type_bin_int_op); |
47 |
"&&", (static_op type_bin_bool_op); |
48 |
"||", (static_op type_bin_bool_op); |
49 |
"xor", (static_op type_bin_bool_op); |
50 |
"impl", (static_op type_bin_bool_op); |
51 |
"<", (static_op type_bin_comp_op); |
52 |
"<=", (static_op type_bin_comp_op); |
53 |
">", (static_op type_bin_comp_op); |
54 |
">=", (static_op type_bin_comp_op); |
55 |
"!=", (static_op type_bin_comp_op); |
56 |
"=", (static_op type_bin_comp_op); |
57 |
"not", (static_op type_unary_bool_op) |
58 |
] |
59 |
|
60 |
module CE = Env |
61 |
|
62 |
let clock_env = |
63 |
let init_env = CE.initial in |
64 |
let env' = |
65 |
List.fold_right (fun op env -> CE.add_value env op ck_unary_univ) |
66 |
["uminus"; "not"] init_env in |
67 |
let env' = |
68 |
List.fold_right (fun op env -> CE.add_value env op ck_bin_univ) |
69 |
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
70 |
env' |
71 |
|
72 |
module DE = Env |
73 |
|
74 |
let delay_env = |
75 |
let init_env = DE.initial in |
76 |
let env' = |
77 |
List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op) |
78 |
["uminus"; "not"] init_env in |
79 |
let env' = |
80 |
List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op) |
81 |
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in |
82 |
let env' = |
83 |
List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op) |
84 |
[] env' in |
85 |
env' |
86 |
|
87 |
module VE = Env |
88 |
|
89 |
let eval_env = |
90 |
let defs = [ |
91 |
"uminus", (function [Dint a] -> Dint (-a) | _ -> assert false); |
92 |
"not", (function [Dbool b] -> Dbool (not 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 |
"*", (function [Dint a; Dint b] -> Dint (a*b) | _ -> assert false); |
96 |
"/", (function [Dint a; Dint b] -> Dint (a/b) | _ -> assert false); |
97 |
"mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false); |
98 |
"&&", (function [Dbool a; Dbool b] -> Dbool (a&&b) | _ -> assert false); |
99 |
"||", (function [Dbool a; Dbool b] -> Dbool (a||b) | _ -> assert false); |
100 |
"xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false); |
101 |
"impl", (function [Dbool a; Dbool 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 [Dint a; Dint b] -> Dbool (a>=b) | _ -> assert false); |
106 |
"!=", (function [a; b] -> Dbool (a<>b) | _ -> assert false); |
107 |
"=", (function [a; b] -> Dbool (a=b) | _ -> assert false); |
108 |
] |
109 |
in |
110 |
List.fold_left |
111 |
(fun env (op, op_eval) -> VE.add_value env op op_eval) |
112 |
VE.initial |
113 |
defs |
114 |
|
115 |
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"] |
116 |
|
117 |
let is_internal_fun x = |
118 |
List.mem x internal_funs |
119 |
|
120 |
(* |
121 |
let imported_node name inputs outputs sl spec = |
122 |
mktop_decl Location.dummy_loc |
123 |
( |
124 |
ImportedNode |
125 |
{nodei_id = name; |
126 |
nodei_type = Types.new_var (); |
127 |
nodei_clock = Clocks.new_var true; |
128 |
nodei_inputs = inputs; |
129 |
nodei_outputs = outputs; |
130 |
nodei_stateless = sl; |
131 |
nodei_spec = spec}) |
132 |
|
133 |
let mk_new_var id = |
134 |
let loc = Location.dummy_loc in |
135 |
mkvar_decl loc (id, mktyp loc Tydec_any, mkclock loc Ckdec_any, false) |
136 |
|
137 |
let _ = |
138 |
let binary_fun id = id, [mk_new_var "x"; mk_new_var "y"], [mk_new_var "z"] in |
139 |
let unary_fun id = id, [mk_new_var "x"], [mk_new_var "y"] in |
140 |
(* All following functions are stateless *) |
141 |
let st = true in |
142 |
List.iter (fun (n,i,o) -> Hashtbl.add node_table n (imported_node n i o st None)) |
143 |
( |
144 |
(*("ite", [mk_new_var "g"; mk_new_var "x"; mk_new_var "y"], [mk_new_var "z"])::*) |
145 |
(List.map binary_fun |
146 |
["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"="]) |
147 |
@(List.map unary_fun ["uminus";"not"])) |
148 |
*) |
149 |
let pp_c i get_val_type pp_val fmt vl = |
150 |
match i, vl with |
151 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 |
152 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
153 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v |
154 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
155 |
| "=", [v1; v2] when get_val_type v1 == Types.Tbool-> Format.fprintf fmt "((!!%a) == (!!%a))" pp_val v1 pp_val v2 |
156 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
157 |
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
158 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 |
159 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
160 |
| _ -> raise (Failure ("No C printer for function " ^ i)) |
161 |
|
162 |
let pp_java i pp_val fmt vl = |
163 |
match i, vl with |
164 |
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *) |
165 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
166 |
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v |
167 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
168 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
169 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
170 |
| _ -> raise (Failure ("No Java printer for function " ^ i)) |
171 |
|
172 |
let pp_horn i pp_val fmt vl = |
173 |
match i, vl with |
174 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 |
175 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
176 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v |
177 |
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 |
178 |
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 |
179 |
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 |
180 |
| "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 |
181 |
(* | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 *) |
182 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
183 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
184 |
| _ -> raise (Failure ("No horn printer for function " ^ i)) |
185 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
186 |
|
187 |
*) |
188 |
|
189 |
|
190 |
let pp_acsl i get_val_type pp_val fmt vl = |
191 |
match i, vl with |
192 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 |
193 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
194 |
| "not", [v] -> Format.fprintf fmt "((%a == 0)?1:0)" pp_val v |
195 |
| "impl", [v1; v2] -> Format.fprintf fmt "(%a?(%a?1:0):1)" pp_val v1 pp_val v2 |
196 |
| "=", [v1; v2] when get_val_type v1 == Types.Tbool-> Format.fprintf fmt "(((!!%a) == (!!%a))?1:0)" pp_val v1 pp_val v2 |
197 |
| "=", [v1; v2] -> Format.fprintf fmt "((%a == %a)?1:0)" pp_val v1 pp_val v2 |
198 |
| "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
199 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 |
200 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
201 |
| _ -> raise (Failure ("No ACSL printer for function " ^ i)) |
202 |
|
203 |
(* Local Variables: *) |
204 |
(* compile-command:"make -C .." *) |
205 |
(* End: *) |