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 LustreSpec
|
27
|
open Type_predef
|
28
|
open Clock_predef
|
29
|
open Delay_predef
|
30
|
open Dimension
|
31
|
|
32
|
module TE = Env
|
33
|
|
34
|
let static_op ty =
|
35
|
type_static (mkdim_var ()) ty
|
36
|
|
37
|
let type_env =
|
38
|
List.fold_left
|
39
|
(fun env (op, op_type) -> TE.add_value env op op_type)
|
40
|
TE.initial
|
41
|
[
|
42
|
"+", (static_op type_bin_poly_op);
|
43
|
"uminus", (static_op type_unary_poly_op);
|
44
|
"-", (static_op type_bin_poly_op);
|
45
|
"*", (static_op type_bin_poly_op);
|
46
|
"/", (static_op type_bin_poly_op);
|
47
|
"mod", (static_op type_bin_int_op);
|
48
|
"&&", (static_op type_bin_bool_op);
|
49
|
"||", (static_op type_bin_bool_op);
|
50
|
"xor", (static_op type_bin_bool_op);
|
51
|
"impl", (static_op type_bin_bool_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
|
"=", (static_op type_bin_comp_op);
|
58
|
"not", (static_op type_unary_bool_op)
|
59
|
]
|
60
|
|
61
|
module CE = Env
|
62
|
|
63
|
let clock_env =
|
64
|
let init_env = CE.initial in
|
65
|
let env' =
|
66
|
List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
|
67
|
["uminus"; "not"] init_env in
|
68
|
let env' =
|
69
|
List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
|
70
|
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
|
71
|
env'
|
72
|
|
73
|
module DE = Env
|
74
|
|
75
|
let delay_env =
|
76
|
let init_env = DE.initial in
|
77
|
let env' =
|
78
|
List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
|
79
|
["uminus"; "not"] init_env in
|
80
|
let env' =
|
81
|
List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
|
82
|
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
|
83
|
let env' =
|
84
|
List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
|
85
|
[] env' in
|
86
|
env'
|
87
|
|
88
|
module VE = Env
|
89
|
|
90
|
let eval_env =
|
91
|
let defs = [
|
92
|
"uminus", (function [Dint a] -> Dint (-a) | _ -> assert false);
|
93
|
"not", (function [Dbool b] -> Dbool (not 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
|
"/", (function [Dint a; Dint b] -> Dint (a/b) | _ -> assert false);
|
98
|
"mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false);
|
99
|
"&&", (function [Dbool a; Dbool b] -> Dbool (a&&b) | _ -> assert false);
|
100
|
"||", (function [Dbool a; Dbool b] -> Dbool (a||b) | _ -> assert false);
|
101
|
"xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);
|
102
|
"impl", (function [Dbool a; Dbool 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 [Dint a; Dint b] -> Dbool (a>=b) | _ -> assert false);
|
107
|
"!=", (function [a; b] -> Dbool (a<>b) | _ -> assert false);
|
108
|
"=", (function [a; b] -> Dbool (a=b) | _ -> assert false);
|
109
|
]
|
110
|
in
|
111
|
List.fold_left
|
112
|
(fun env (op, op_eval) -> VE.add_value env op op_eval)
|
113
|
VE.initial
|
114
|
defs
|
115
|
|
116
|
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
|
117
|
|
118
|
let is_internal_fun x =
|
119
|
List.mem x internal_funs
|
120
|
|
121
|
(*
|
122
|
let imported_node name inputs outputs sl spec =
|
123
|
mktop_decl Location.dummy_loc
|
124
|
(
|
125
|
ImportedNode
|
126
|
{nodei_id = name;
|
127
|
nodei_type = Types.new_var ();
|
128
|
nodei_clock = Clocks.new_var true;
|
129
|
nodei_inputs = inputs;
|
130
|
nodei_outputs = outputs;
|
131
|
nodei_stateless = sl;
|
132
|
nodei_spec = spec})
|
133
|
|
134
|
let mk_new_var id =
|
135
|
let loc = Location.dummy_loc in
|
136
|
mkvar_decl loc (id, mktyp loc Tydec_any, mkclock loc Ckdec_any, false)
|
137
|
|
138
|
let _ =
|
139
|
let binary_fun id = id, [mk_new_var "x"; mk_new_var "y"], [mk_new_var "z"] in
|
140
|
let unary_fun id = id, [mk_new_var "x"], [mk_new_var "y"] in
|
141
|
(* All following functions are stateless *)
|
142
|
let st = true in
|
143
|
List.iter (fun (n,i,o) -> Hashtbl.add node_table n (imported_node n i o st None))
|
144
|
(
|
145
|
(*("ite", [mk_new_var "g"; mk_new_var "x"; mk_new_var "y"], [mk_new_var "z"])::*)
|
146
|
(List.map binary_fun
|
147
|
["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"="])
|
148
|
@(List.map unary_fun ["uminus";"not"]))
|
149
|
*)
|
150
|
let pp_c i pp_val fmt vl =
|
151
|
match i, vl with
|
152
|
(* | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
|
153
|
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
|
154
|
| "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
|
155
|
| "impl", [v1; v2] -> 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
|
| _ -> assert false
|
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
|
| _ -> assert false
|
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
|
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
|
181
|
| _ -> assert false
|
182
|
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
|
183
|
| "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
|
184
|
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
|
185
|
*)
|
186
|
|
187
|
(* Local Variables: *)
|
188
|
(* compile-command:"make -C .." *)
|
189
|
(* End: *)
|