Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/Ada/ada_backend_common.ml | ||
---|---|---|
1 | 1 |
open Format |
2 |
|
|
3 | 2 |
open Machine_code_types |
4 | 3 |
open Lustre_types |
5 | 4 |
open Machine_code_common |
6 |
|
|
7 | 5 |
open Ada_printer |
8 | 6 |
open Misc_printer |
9 | 7 |
open Misc_lustre_function |
10 | 8 |
|
11 |
(** Exception for unsupported features in Ada backend **) |
|
12 | 9 |
exception Ada_not_supported of string |
10 |
(** Exception for unsupported features in Ada backend **) |
|
13 | 11 |
|
14 |
(** Print the name of the state variable. |
|
15 |
@param fmt the formater to print on |
|
16 |
**) |
|
12 |
(** Print the name of the state variable. @param fmt the formater to print on **) |
|
17 | 13 |
let pp_state_name fmt = fprintf fmt "state" |
18 | 14 |
|
19 |
(** Print the type of the state variable. |
|
20 |
@param fmt the formater to print on |
|
21 |
**) |
|
15 |
(** Print the type of the state variable. @param fmt the formater to print on **) |
|
22 | 16 |
let pp_state_type fmt = fprintf fmt "TState" |
23 | 17 |
|
24 |
(** Print the name of the reset procedure |
|
25 |
@param fmt the formater to print on |
|
26 |
**) |
|
18 |
(** Print the name of the reset procedure @param fmt the formater to print on **) |
|
27 | 19 |
let pp_reset_procedure_name fmt = fprintf fmt "reset" |
28 | 20 |
|
29 |
(** Print the name of the step procedure |
|
30 |
@param fmt the formater to print on |
|
31 |
**) |
|
21 |
(** Print the name of the step procedure @param fmt the formater to print on **) |
|
32 | 22 |
let pp_step_procedure_name fmt = fprintf fmt "step" |
33 | 23 |
|
34 |
(** Print the name of the main procedure. |
|
35 |
@param fmt the formater to print on |
|
36 |
**) |
|
24 |
(** Print the name of the main procedure. @param fmt the formater to print on **) |
|
37 | 25 |
let pp_main_procedure_name fmt = fprintf fmt "ada_main" |
38 | 26 |
|
39 |
(** Print the name of the arrow package. |
|
40 |
@param fmt the formater to print on |
|
41 |
**) |
|
27 |
(** Print the name of the arrow package. @param fmt the formater to print on **) |
|
42 | 28 |
let pp_arrow_package_name fmt = fprintf fmt "Arrow" |
43 | 29 |
|
44 |
(** Print the type of a polymorphic type. |
|
45 |
@param fmt the formater to print on |
|
46 |
@param id the id of the polymorphic type |
|
47 |
**) |
|
30 |
(** Print the type of a polymorphic type. @param fmt the formater to print on |
|
31 |
@param id the id of the polymorphic type **) |
|
48 | 32 |
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id |
49 | 33 |
|
50 | 34 |
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr |
51 | 35 |
|
52 |
|
|
53 |
|
|
54 |
|
|
55 |
|
|
56 |
|
|
57 |
|
|
58 |
|
|
59 |
|
|
60 |
(*TODO Check all this function with unit test, improve this system and |
|
61 |
add support for : "cbrt", "erf", "log10", "pow", "atan2". |
|
62 |
*) |
|
36 |
(*TODO Check all this function with unit test, improve this system and add |
|
37 |
support for : "cbrt", "erf", "log10", "pow", "atan2". *) |
|
63 | 38 |
let ada_supported_funs = |
64 |
[("sqrt", ("Ada.Numerics.Elementary_Functions", "Sqrt"));
|
|
65 |
("log", ("Ada.Numerics.Elementary_Functions", "Log"));
|
|
66 |
("exp", ("Ada.Numerics.Elementary_Functions", "Exp"));
|
|
67 |
("pow", ("Ada.Numerics.Elementary_Functions", "**"));
|
|
68 |
("sin", ("Ada.Numerics.Elementary_Functions", "Sin"));
|
|
69 |
("cos", ("Ada.Numerics.Elementary_Functions", "Cos"));
|
|
70 |
("tan", ("Ada.Numerics.Elementary_Functions", "Tan"));
|
|
71 |
("asin", ("Ada.Numerics.Elementary_Functions", "Arcsin"));
|
|
72 |
("acos", ("Ada.Numerics.Elementary_Functions", "Arccos"));
|
|
73 |
("atan", ("Ada.Numerics.Elementary_Functions", "Arctan"));
|
|
74 |
("sinh", ("Ada.Numerics.Elementary_Functions", "Sinh"));
|
|
75 |
("cosh", ("Ada.Numerics.Elementary_Functions", "Cosh"));
|
|
76 |
("tanh", ("Ada.Numerics.Elementary_Functions", "Tanh"));
|
|
77 |
("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
|
|
78 |
("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
|
|
79 |
("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
|
|
80 |
|
|
81 |
("ceil", ("", "Float'Ceiling"));
|
|
82 |
("floor", ("", "Float'Floor"));
|
|
83 |
("fmod", ("", "Float'Remainder"));
|
|
84 |
("round", ("", "Float'Rounding"));
|
|
85 |
("trunc", ("", "Float'Truncation"));
|
|
86 |
|
|
87 |
("fabs", ("", "abs"));]
|
|
39 |
[ |
|
40 |
"sqrt", ("Ada.Numerics.Elementary_Functions", "Sqrt");
|
|
41 |
"log", ("Ada.Numerics.Elementary_Functions", "Log");
|
|
42 |
"exp", ("Ada.Numerics.Elementary_Functions", "Exp");
|
|
43 |
"pow", ("Ada.Numerics.Elementary_Functions", "**");
|
|
44 |
"sin", ("Ada.Numerics.Elementary_Functions", "Sin");
|
|
45 |
"cos", ("Ada.Numerics.Elementary_Functions", "Cos");
|
|
46 |
"tan", ("Ada.Numerics.Elementary_Functions", "Tan");
|
|
47 |
"asin", ("Ada.Numerics.Elementary_Functions", "Arcsin");
|
|
48 |
"acos", ("Ada.Numerics.Elementary_Functions", "Arccos");
|
|
49 |
"atan", ("Ada.Numerics.Elementary_Functions", "Arctan");
|
|
50 |
"sinh", ("Ada.Numerics.Elementary_Functions", "Sinh");
|
|
51 |
"cosh", ("Ada.Numerics.Elementary_Functions", "Cosh");
|
|
52 |
"tanh", ("Ada.Numerics.Elementary_Functions", "Tanh");
|
|
53 |
"asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh");
|
|
54 |
"acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh");
|
|
55 |
"atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"); |
|
56 |
"ceil", ("", "Float'Ceiling");
|
|
57 |
"floor", ("", "Float'Floor");
|
|
58 |
"fmod", ("", "Float'Remainder");
|
|
59 |
"round", ("", "Float'Rounding");
|
|
60 |
"trunc", ("", "Float'Truncation");
|
|
61 |
"fabs", ("", "abs"); |
|
62 |
] |
|
88 | 63 |
|
89 | 64 |
let is_builtin_fun ident = |
90 |
List.mem ident Basic_library.internal_funs ||
|
|
91 |
List.mem_assoc ident ada_supported_funs
|
|
65 |
List.mem ident Basic_library.internal_funs |
|
66 |
|| List.mem_assoc ident ada_supported_funs
|
|
92 | 67 |
|
93 |
(** Print the name of a package associated to a machine. |
|
94 |
@param fmt the formater to print on |
|
95 |
@param machine the machine |
|
96 |
**) |
|
68 |
(** Print the name of a package associated to a machine. @param fmt the formater |
|
69 |
to print on @param machine the machine **) |
|
97 | 70 |
let pp_package_name machine fmt = |
98 |
if is_arrow machine then |
|
99 |
fprintf fmt "%t" pp_arrow_package_name |
|
100 |
else |
|
101 |
fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id |
|
102 |
|
|
103 |
(** Print a type. |
|
104 |
@param fmt the formater to print on |
|
105 |
@param type the type |
|
106 |
**) |
|
107 |
let pp_type fmt typ = |
|
108 |
(match (Types.repr typ).Types.tdesc with |
|
109 |
| Types.Tbasic Types.Basic.Tint -> pp_integer_type fmt |
|
110 |
| Types.Tbasic Types.Basic.Treal -> pp_float_type fmt |
|
111 |
| Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt |
|
112 |
| Types.Tunivar -> pp_polymorphic_type typ.Types.tid fmt |
|
113 |
| Types.Tbasic _ -> eprintf "Tbasic@."; assert false (*TODO*) |
|
114 |
| Types.Tconst _ -> eprintf "Tconst@."; assert false (*TODO*) |
|
115 |
| Types.Tclock _ -> eprintf "Tclock@."; assert false (*TODO*) |
|
116 |
| Types.Tarrow _ -> eprintf "Tarrow@."; assert false (*TODO*) |
|
117 |
| Types.Ttuple l -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*) |
|
118 |
| Types.Tenum _ -> eprintf "Tenum@."; assert false (*TODO*) |
|
119 |
| Types.Tstruct _ -> eprintf "Tstruct@.";assert false (*TODO*) |
|
120 |
| Types.Tarray _ -> eprintf "Tarray@."; assert false (*TODO*) |
|
121 |
| Types.Tstatic _ -> eprintf "Tstatic@.";assert false (*TODO*) |
|
122 |
| Types.Tlink _ -> eprintf "Tlink@."; assert false (*TODO*) |
|
123 |
| Types.Tvar -> eprintf "Tvar@."; assert false (*TODO*) |
|
124 |
(*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *) |
|
125 |
) |
|
126 |
|
|
127 |
(** Return a default ada constant for a given type. |
|
128 |
@param cst_typ the constant type |
|
129 |
**) |
|
130 |
let default_ada_cst cst_typ = match cst_typ with |
|
131 |
| Types.Basic.Tint -> Const_int 0 |
|
132 |
| Types.Basic.Treal -> Const_real Real.zero |
|
133 |
| Types.Basic.Tbool -> Const_tag tag_false |
|
134 |
| _ -> assert false |
|
135 |
|
|
136 |
(** Make a default value from a given type. |
|
137 |
@param typ the type |
|
138 |
**) |
|
71 |
if is_arrow machine then fprintf fmt "%t" pp_arrow_package_name |
|
72 |
else fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id |
|
73 |
|
|
74 |
(** Print a type. @param fmt the formater to print on @param type the type **) |
|
75 |
let pp_type fmt typ = |
|
76 |
match (Types.repr typ).Types.tdesc with |
|
77 |
| Types.Tbasic Types.Basic.Tint -> |
|
78 |
pp_integer_type fmt |
|
79 |
| Types.Tbasic Types.Basic.Treal -> |
|
80 |
pp_float_type fmt |
|
81 |
| Types.Tbasic Types.Basic.Tbool -> |
|
82 |
pp_boolean_type fmt |
|
83 |
| Types.Tunivar -> |
|
84 |
pp_polymorphic_type typ.Types.tid fmt |
|
85 |
| Types.Tbasic _ -> |
|
86 |
eprintf "Tbasic@."; |
|
87 |
assert false (*TODO*) |
|
88 |
| Types.Tconst _ -> |
|
89 |
eprintf "Tconst@."; |
|
90 |
assert false (*TODO*) |
|
91 |
| Types.Tclock _ -> |
|
92 |
eprintf "Tclock@."; |
|
93 |
assert false (*TODO*) |
|
94 |
| Types.Tarrow _ -> |
|
95 |
eprintf "Tarrow@."; |
|
96 |
assert false (*TODO*) |
|
97 |
| Types.Ttuple l -> |
|
98 |
eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; |
|
99 |
assert false (*TODO*) |
|
100 |
| Types.Tenum _ -> |
|
101 |
eprintf "Tenum@."; |
|
102 |
assert false (*TODO*) |
|
103 |
| Types.Tstruct _ -> |
|
104 |
eprintf "Tstruct@."; |
|
105 |
assert false (*TODO*) |
|
106 |
| Types.Tarray _ -> |
|
107 |
eprintf "Tarray@."; |
|
108 |
assert false (*TODO*) |
|
109 |
| Types.Tstatic _ -> |
|
110 |
eprintf "Tstatic@."; |
|
111 |
assert false (*TODO*) |
|
112 |
| Types.Tlink _ -> |
|
113 |
eprintf "Tlink@."; |
|
114 |
assert false (*TODO*) |
|
115 |
| Types.Tvar -> |
|
116 |
eprintf "Tvar@."; |
|
117 |
assert false |
|
118 |
(*TODO*) |
|
119 |
(*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *) |
|
120 |
|
|
121 |
(** Return a default ada constant for a given type. @param cst_typ the constant |
|
122 |
type **) |
|
123 |
let default_ada_cst cst_typ = |
|
124 |
match cst_typ with |
|
125 |
| Types.Basic.Tint -> |
|
126 |
Const_int 0 |
|
127 |
| Types.Basic.Treal -> |
|
128 |
Const_real Real.zero |
|
129 |
| Types.Basic.Tbool -> |
|
130 |
Const_tag tag_false |
|
131 |
| _ -> |
|
132 |
assert false |
|
133 |
|
|
134 |
(** Make a default value from a given type. @param typ the type **) |
|
139 | 135 |
let mk_default_value typ = |
140 | 136 |
match (Types.repr typ).Types.tdesc with |
141 |
| Types.Tbasic t -> mk_val (Cst (default_ada_cst t)) typ |
|
142 |
| _ -> assert false (*TODO*) |
|
143 |
|
|
144 |
(** Print the type of a variable. |
|
145 |
@param fmt the formater to print on |
|
146 |
@param id the variable |
|
147 |
**) |
|
148 |
let pp_var_type fmt id = |
|
149 |
pp_type fmt id.var_type |
|
150 |
|
|
151 |
(** Print a package name with polymorphic types specified. |
|
152 |
@param substitution correspondance between polymorphic type id and their instantiation |
|
153 |
@param fmt the formater to print on |
|
154 |
@param machine the machine |
|
155 |
**) |
|
137 |
| Types.Tbasic t -> |
|
138 |
mk_val (Cst (default_ada_cst t)) typ |
|
139 |
| _ -> |
|
140 |
assert false |
|
141 |
(*TODO*) |
|
142 |
|
|
143 |
(** Print the type of a variable. @param fmt the formater to print on @param id |
|
144 |
the variable **) |
|
145 |
let pp_var_type fmt id = pp_type fmt id.var_type |
|
146 |
|
|
147 |
(** Print a package name with polymorphic types specified. @param substitution |
|
148 |
correspondance between polymorphic type id and their instantiation @param |
|
149 |
fmt the formater to print on @param machine the machine **) |
|
156 | 150 |
let pp_package_name_with_polymorphic substitution machine fmt = |
157 | 151 |
let polymorphic_types = find_all_polymorphic_type machine in |
158 |
assert(List.length polymorphic_types = List.length substitution); |
|
152 |
assert (List.length polymorphic_types = List.length substitution);
|
|
159 | 153 |
let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in |
160 |
assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2) |
|
161 |
polymorphic_types substituion); |
|
154 |
assert ( |
|
155 |
List.for_all2 |
|
156 |
(fun poly1 (poly2, _) -> poly1 = poly2) |
|
157 |
polymorphic_types substituion); |
|
162 | 158 |
let instantiated_types = snd (List.split substitution) in |
163 |
fprintf fmt "%t%t%a" |
|
164 |
(pp_package_name machine) |
|
159 |
fprintf fmt "%t%t%a" (pp_package_name machine) |
|
165 | 160 |
(Utils.pp_final_char_if_non_empty "_" instantiated_types) |
166 |
(Utils.fprintf_list ~sep:"_" pp_type) instantiated_types |
|
167 |
|
|
168 |
(** Print the name of a variable. |
|
169 |
@param fmt the formater to print on |
|
170 |
@param id the variable |
|
171 |
**) |
|
172 |
let pp_var_name id fmt = |
|
173 |
fprintf fmt "%a" pp_clean_ada_identifier id.var_id |
|
174 |
|
|
175 |
(** Print the complete name of variable. |
|
176 |
@param m the machine to check if it is memory |
|
177 |
@param fmt the formater to print on |
|
178 |
@param var the variable |
|
179 |
**) |
|
161 |
(Utils.fprintf_list ~sep:"_" pp_type) |
|
162 |
instantiated_types |
|
163 |
|
|
164 |
(** Print the name of a variable. @param fmt the formater to print on @param id |
|
165 |
the variable **) |
|
166 |
let pp_var_name id fmt = fprintf fmt "%a" pp_clean_ada_identifier id.var_id |
|
167 |
|
|
168 |
(** Print the complete name of variable. @param m the machine to check if it is |
|
169 |
memory @param fmt the formater to print on @param var the variable **) |
|
180 | 170 |
let pp_var env fmt var = |
181 | 171 |
match List.assoc_opt var.var_id env with |
182 |
| None -> pp_var_name var fmt |
|
183 |
| Some pp_state -> pp_access pp_state (pp_var_name var) fmt |
|
172 |
| None -> |
|
173 |
pp_var_name var fmt |
|
174 |
| Some pp_state -> |
|
175 |
pp_access pp_state (pp_var_name var) fmt |
|
184 | 176 |
|
185 | 177 |
(* Expression print functions *) |
186 | 178 |
|
187 | 179 |
(* Printing functions for basic operations and expressions *) |
188 |
(* TODO: refactor code -> use let rec and for basic pretty printing |
|
189 |
function *) |
|
180 |
(* TODO: refactor code -> use let rec and for basic pretty printing function *)
|
|
181 |
|
|
190 | 182 |
(** Printing function for Ada tags, mainly booleans. |
191 | 183 |
|
192 |
@param fmt the formater to use |
|
193 |
@param t the tag to print |
|
194 |
**) |
|
184 |
@param fmt the formater to use @param t the tag to print **) |
|
195 | 185 |
let pp_ada_tag fmt t = |
196 | 186 |
pp_print_string fmt |
197 | 187 |
(if t = tag_true then "True" else if t = tag_false then "False" else t) |
198 | 188 |
|
199 |
(** Printing function for machine type constants. For the moment, |
|
200 |
arrays are not supported.
|
|
189 |
(** Printing function for machine type constants. For the moment, arrays are not
|
|
190 |
supported. |
|
201 | 191 |
|
202 |
@param fmt the formater to use |
|
203 |
@param c the constant to print |
|
204 |
**) |
|
192 |
@param fmt the formater to use @param c the constant to print **) |
|
205 | 193 |
let pp_ada_const fmt c = |
206 | 194 |
match c with |
207 |
| Const_int i -> pp_print_int fmt i |
|
208 |
| Const_real r -> Real.pp_ada fmt r |
|
209 |
| Const_tag t -> pp_ada_tag fmt t |
|
195 |
| Const_int i -> |
|
196 |
pp_print_int fmt i |
|
197 |
| Const_real r -> |
|
198 |
Real.pp_ada fmt r |
|
199 |
| Const_tag t -> |
|
200 |
pp_ada_tag fmt t |
|
210 | 201 |
| Const_string _ | Const_modeid _ -> |
211 |
(Format.eprintf |
|
212 |
"internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid."; |
|
213 |
assert false) |
|
214 |
| _ -> |
|
215 |
raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not |
|
216 |
support this constant") |
|
217 |
|
|
218 |
(** Printing function for expressions [v1 modulo v2]. Depends |
|
219 |
on option [integer_div_euclidean] to choose between mathematical |
|
220 |
modulo or remainder ([rem] in Ada). |
|
221 |
|
|
222 |
@param pp_value pretty printer for values |
|
223 |
@param v1 the first value in the expression |
|
224 |
@param v2 the second value in the expression |
|
225 |
@param fmt the formater to print on |
|
226 |
**) |
|
202 |
Format.eprintf |
|
203 |
"internal error: Ada_backend_adb.pp_ada_const cannot print string or \ |
|
204 |
modeid."; |
|
205 |
assert false |
|
206 |
| _ -> |
|
207 |
raise |
|
208 |
(Ada_not_supported |
|
209 |
"unsupported: Ada_backend_adb.pp_ada_const does not\n\ |
|
210 |
\ support this constant") |
|
211 |
|
|
212 |
(** Printing function for expressions [v1 modulo v2]. Depends on option |
|
213 |
[integer_div_euclidean] to choose between mathematical modulo or remainder |
|
214 |
([rem] in Ada). |
|
215 |
|
|
216 |
@param pp_value pretty printer for values @param v1 the first value in the |
|
217 |
expression @param v2 the second value in the expression @param fmt the |
|
218 |
formater to print on **) |
|
227 | 219 |
let pp_mod pp_value v1 v2 fmt = |
228 | 220 |
if !Options.integer_div_euclidean then |
229 | 221 |
(* (a rem b) + (a rem b < 0 ? abs(b) : 0) *) |
230 | 222 |
Format.fprintf fmt |
231 |
"((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))" |
|
232 |
pp_value v1 pp_value v2 |
|
233 |
pp_value v1 pp_value v2 |
|
234 |
pp_value v2 |
|
235 |
else (* Ada behavior for rem *) |
|
223 |
"((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))" pp_value v1 |
|
224 |
pp_value v2 pp_value v1 pp_value v2 pp_value v2 |
|
225 |
else |
|
226 |
(* Ada behavior for rem *) |
|
236 | 227 |
Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2 |
237 | 228 |
|
238 |
(** Printing function for expressions [v1 div v2]. Depends on |
|
239 |
option [integer_div_euclidean] to choose between mathematic
|
|
240 |
division or Ada division.
|
|
229 |
(** Printing function for expressions [v1 div v2]. Depends on option
|
|
230 |
[integer_div_euclidean] to choose between mathematic division or Ada
|
|
231 |
division. |
|
241 | 232 |
|
242 |
@param pp_value pretty printer for values |
|
243 |
@param v1 the first value in the expression |
|
244 |
@param v2 the second value in the expression |
|
245 |
@param fmt the formater to print in |
|
246 |
**) |
|
233 |
@param pp_value pretty printer for values @param v1 the first value in the |
|
234 |
expression @param v2 the second value in the expression @param fmt the |
|
235 |
formater to print in **) |
|
247 | 236 |
let pp_div pp_value v1 v2 fmt = |
248 | 237 |
if !Options.integer_div_euclidean then |
249 | 238 |
(* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *) |
250 |
Format.fprintf fmt "(%a - %t) / %a" |
|
251 |
pp_value v1 |
|
252 |
(pp_mod pp_value v1 v2) |
|
239 |
Format.fprintf fmt "(%a - %t) / %a" pp_value v1 (pp_mod pp_value v1 v2) |
|
253 | 240 |
pp_value v2 |
254 |
else (* Ada behavior for / *) |
|
241 |
else |
|
242 |
(* Ada behavior for / *) |
|
255 | 243 |
Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2 |
256 | 244 |
|
257 | 245 |
(** Printing function for basic lib functions. |
258 | 246 |
|
259 |
@param pp_value pretty printer for values |
|
260 |
@param i a string representing the function |
|
261 |
@param fmt the formater to print on |
|
262 |
@param vl the list of operands |
|
263 |
**) |
|
247 |
@param pp_value pretty printer for values @param i a string representing the |
|
248 |
function @param fmt the formater to print on @param vl the list of operands |
|
249 |
**) |
|
264 | 250 |
let pp_basic_lib_fun pp_value ident fmt vl = |
265 | 251 |
match ident, vl with |
266 |
| "uminus", [v] ->
|
|
252 |
| "uminus", [ v ] ->
|
|
267 | 253 |
Format.fprintf fmt "(- %a)" pp_value v |
268 |
| "not", [v] ->
|
|
254 |
| "not", [ v ] ->
|
|
269 | 255 |
Format.fprintf fmt "(not %a)" pp_value v |
270 |
| "impl", [v1; v2] ->
|
|
256 |
| "impl", [ v1; v2 ] ->
|
|
271 | 257 |
Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2 |
272 |
| "=", [v1; v2] ->
|
|
258 |
| "=", [ v1; v2 ] ->
|
|
273 | 259 |
Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2 |
274 |
| "mod", [v1; v2] -> pp_mod pp_value v1 v2 fmt |
|
275 |
| "equi", [v1; v2] -> |
|
260 |
| "mod", [ v1; v2 ] -> |
|
261 |
pp_mod pp_value v1 v2 fmt |
|
262 |
| "equi", [ v1; v2 ] -> |
|
276 | 263 |
Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2 |
277 |
| "xor", [v1; v2] ->
|
|
264 |
| "xor", [ v1; v2 ] ->
|
|
278 | 265 |
Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2 |
279 |
| "/", [v1; v2] -> pp_div pp_value v1 v2 fmt |
|
280 |
| "&&", [v1; v2] -> |
|
266 |
| "/", [ v1; v2 ] -> |
|
267 |
pp_div pp_value v1 v2 fmt |
|
268 |
| "&&", [ v1; v2 ] -> |
|
281 | 269 |
Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2 |
282 |
| "||", [v1; v2] ->
|
|
270 |
| "||", [ v1; v2 ] ->
|
|
283 | 271 |
Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2 |
284 |
| "!=", [v1; v2] ->
|
|
272 |
| "!=", [ v1; v2 ] ->
|
|
285 | 273 |
Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2 |
286 |
| "ite", [v1; v2; v3] -> |
|
287 |
Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3 |
|
288 |
| op, [v1; v2] -> |
|
274 |
| "ite", [ v1; v2; v3 ] -> |
|
275 |
Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 |
|
276 |
pp_value v3 |
|
277 |
| op, [ v1; v2 ] -> |
|
289 | 278 |
Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2 |
290 |
| _, [v1] when List.mem_assoc ident ada_supported_funs -> |
|
291 |
let pkg, name = try List.assoc ident ada_supported_funs |
|
292 |
with Not_found -> assert false in |
|
293 |
let pkg = pkg^(if String.equal pkg "" then "" else ".") in |
|
294 |
Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1 |
|
295 |
| fun_name, _ -> |
|
296 |
(Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false) |
|
279 |
| _, [ v1 ] when List.mem_assoc ident ada_supported_funs -> |
|
280 |
let pkg, name = |
|
281 |
try List.assoc ident ada_supported_funs with Not_found -> assert false |
|
282 |
in |
|
283 |
let pkg = pkg ^ if String.equal pkg "" then "" else "." in |
|
284 |
Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1 |
|
285 |
| fun_name, _ -> |
|
286 |
Format.eprintf "internal compilation error: basic function %s@." fun_name; |
|
287 |
assert false |
|
297 | 288 |
|
298 | 289 |
(** Printing function for values. |
299 | 290 |
|
300 |
@param m the machine to know the state variable |
|
301 |
@param fmt the formater to use |
|
302 |
@param value the value to print. Should be a |
|
303 |
{!type:Machine_code_types.value_t} value |
|
304 |
**) |
|
291 |
@param m the machine to know the state variable @param fmt the formater to |
|
292 |
use @param value the value to print. Should be a |
|
293 |
{!type:Machine_code_types.value_t} value **) |
|
305 | 294 |
let rec pp_value env fmt value = |
306 | 295 |
match value.value_desc with |
307 |
| Cst c -> pp_ada_const fmt c |
|
308 |
| Var var -> pp_var env fmt var (* Find better to test if it is memory or not *) |
|
309 |
| Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl |
|
310 |
| _ -> |
|
311 |
raise (Ada_not_supported |
|
312 |
"unsupported: Ada_backend.adb.pp_value does not support this value type") |
|
313 |
|
|
314 |
|
|
315 |
(** Print the filename of a machine package. |
|
316 |
@param extension the extension to append to the package name |
|
317 |
@param fmt the formatter |
|
318 |
@param machine the machine corresponding to the package |
|
319 |
**) |
|
296 |
| Cst c -> |
|
297 |
pp_ada_const fmt c |
|
298 |
| Var var -> |
|
299 |
pp_var env fmt var (* Find better to test if it is memory or not *) |
|
300 |
| Fun (f_ident, vl) -> |
|
301 |
pp_basic_lib_fun (pp_value env) f_ident fmt vl |
|
302 |
| _ -> |
|
303 |
raise |
|
304 |
(Ada_not_supported |
|
305 |
"unsupported: Ada_backend.adb.pp_value does not support this value \ |
|
306 |
type") |
|
307 |
|
|
308 |
(** Print the filename of a machine package. @param extension the extension to |
|
309 |
append to the package name @param fmt the formatter @param machine the |
|
310 |
machine corresponding to the package **) |
|
320 | 311 |
let pp_machine_filename extension fmt machine = |
321 | 312 |
pp_filename extension fmt (pp_package_name machine) |
322 | 313 |
|
323 | 314 |
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name |
324 | 315 |
|
325 |
|
|
326 | 316 |
(** Print the declaration of a state element of a subinstance of a machine. |
327 |
@param machine the machine |
|
328 |
@param fmt the formater to print on |
|
329 |
@param substitution correspondance between polymorphic type id and their instantiation |
|
330 |
@param ident the identifier of the subinstance |
|
331 |
@param submachine the submachine of the subinstance |
|
332 |
**) |
|
333 |
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) = |
|
317 |
@param machine the machine @param fmt the formater to print on @param |
|
318 |
substitution correspondance between polymorphic type id and their |
|
319 |
instantiation @param ident the identifier of the subinstance @param |
|
320 |
submachine the submachine of the subinstance **) |
|
321 |
let build_pp_state_decl_from_subinstance mode with_statement |
|
322 |
(name, (substitution, machine)) = |
|
334 | 323 |
let pp_package = pp_package_name_with_polymorphic substitution machine in |
335 | 324 |
let pp_type = pp_package_access (pp_package, pp_state_type) in |
336 | 325 |
let pp_name fmt = pp_clean_ada_identifier fmt name in |
337 |
(mode, pp_name, pp_type, with_statement)
|
|
326 |
mode, pp_name, pp_type, with_statement
|
|
338 | 327 |
|
339 |
(** Print variable declaration for a local state variable |
|
340 |
@param fmt the formater to print on |
|
341 |
@param mode input/output mode of the parameter |
|
342 |
**) |
|
328 |
(** Print variable declaration for a local state variable @param fmt the |
|
329 |
formater to print on @param mode input/output mode of the parameter **) |
|
343 | 330 |
let build_pp_state_decl mode with_statement = |
344 |
(mode, pp_state_name, pp_state_type, with_statement)
|
|
331 |
mode, pp_state_name, pp_state_type, with_statement
|
|
345 | 332 |
|
346 | 333 |
let build_pp_var_decl mode with_statement var = |
347 | 334 |
let pp_name = function fmt -> pp_var_name var fmt in |
348 | 335 |
let pp_type = function fmt -> pp_var_type fmt var in |
349 |
(mode, pp_name, pp_type, with_statement)
|
|
336 |
mode, pp_name, pp_type, with_statement
|
|
350 | 337 |
|
351 | 338 |
let build_pp_var_decl_local with_statement var = |
352 | 339 |
AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var) |
353 | 340 |
|
354 | 341 |
let build_pp_var_decl_step_input mode with_statement m = |
355 |
if m.mstep.step_inputs=[] then [] else
|
|
356 |
[List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
|
|
342 |
if m.mstep.step_inputs = [] then []
|
|
343 |
else [ List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs ]
|
|
357 | 344 |
|
358 | 345 |
let build_pp_var_decl_step_output mode with_statement m = |
359 |
if m.mstep.step_outputs=[] then [] else
|
|
360 |
[List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
|
|
346 |
if m.mstep.step_outputs = [] then []
|
|
347 |
else [ List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs ]
|
|
361 | 348 |
|
362 | 349 |
let build_pp_var_decl_static mode with_statement m = |
363 |
if m.mstatic=[] then [] else
|
|
364 |
[List.map (build_pp_var_decl mode with_statement) m.mstatic]
|
|
350 |
if m.mstatic = [] then []
|
|
351 |
else [ List.map (build_pp_var_decl mode with_statement) m.mstatic ]
|
|
365 | 352 |
|
366 | 353 |
let build_pp_arg_step m = |
367 |
(if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else []) |
|
368 |
@ (build_pp_var_decl_step_input AdaIn None m) |
|
369 |
@ (build_pp_var_decl_step_output AdaOut None m) |
|
354 |
(if is_machine_statefull m then [ [ build_pp_state_decl AdaInOut None ] ] |
|
355 |
else []) |
|
356 |
@ build_pp_var_decl_step_input AdaIn None m |
|
357 |
@ build_pp_var_decl_step_output AdaOut None m |
|
370 | 358 |
|
371 | 359 |
let build_pp_arg_reset m = |
372 |
(if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
|
|
373 |
@ (build_pp_var_decl_static AdaIn None m)
|
|
374 |
|
|
360 |
(if is_machine_statefull m then [ [ build_pp_state_decl AdaOut None ] ]
|
|
361 |
else [])
|
|
362 |
@ build_pp_var_decl_static AdaIn None m |
|
375 | 363 |
|
376 | 364 |
(* let build_pp_arg_transition m = |
377 | 365 |
* (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else []) |
Also available in: Unified diff
reformatting