1 |
bdc471f3
|
Guillaume DAVY
|
open Format
|
2 |
|
|
|
3 |
|
|
open Machine_code_types
|
4 |
|
|
open Lustre_types
|
5 |
|
|
open Corelang
|
6 |
|
|
open Machine_code_common
|
7 |
|
|
|
8 |
b12a91e0
|
Guillaume DAVY
|
(** All the pretty print functions common to the ada backend **)
|
9 |
|
|
|
10 |
c203d676
|
Guillaume DAVY
|
|
11 |
fd834769
|
Guillaume DAVY
|
(* Misc pretty print functions *)
|
12 |
7cbb6d8a
|
Guillaume DAVY
|
|
13 |
|
|
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
|
14 |
fd8aeeac
|
Christophe Garion
|
underscore and must not contain a double underscore
|
15 |
7cbb6d8a
|
Guillaume DAVY
|
@param var name to be cleaned*)
|
16 |
fd834769
|
Guillaume DAVY
|
let pp_clean_ada_identifier fmt name =
|
17 |
7cbb6d8a
|
Guillaume DAVY
|
let base_size = String.length name in
|
18 |
|
|
assert(base_size > 0);
|
19 |
|
|
let rec remove_double_underscore s = function
|
20 |
|
|
| i when i == String.length s - 1 -> s
|
21 |
|
|
| i when String.get s i == '_' && String.get s (i+1) == '_' ->
|
22 |
|
|
remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
|
23 |
|
|
| i -> remove_double_underscore s (i+1)
|
24 |
|
|
in
|
25 |
|
|
let name = remove_double_underscore name 0 in
|
26 |
|
|
let prefix = if String.length name != base_size
|
27 |
|
|
|| String.get name 0 == '_' then
|
28 |
|
|
"ada"
|
29 |
|
|
else
|
30 |
|
|
""
|
31 |
|
|
in
|
32 |
|
|
fprintf fmt "%s%s" prefix name
|
33 |
|
|
|
34 |
c203d676
|
Guillaume DAVY
|
|
35 |
b12a91e0
|
Guillaume DAVY
|
(* Package pretty print functions *)
|
36 |
|
|
|
37 |
bdc471f3
|
Guillaume DAVY
|
(** Print the name of a package associated to a machine.
|
38 |
|
|
@param fmt the formater to print on
|
39 |
|
|
@param machine the machine
|
40 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
41 |
|
|
let pp_package_name fmt node =
|
42 |
fd834769
|
Guillaume DAVY
|
fprintf fmt "%a" pp_clean_ada_identifier node.node_id
|
43 |
bdc471f3
|
Guillaume DAVY
|
|
44 |
|
|
(** Print the ada package introduction sentence it can be used for body and
|
45 |
|
|
declaration. Boolean parameter body should be true if it is a body delcaration.
|
46 |
|
|
@param fmt the formater to print on
|
47 |
|
|
@param fmt the formater to print on
|
48 |
|
|
@param machine the machine
|
49 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
50 |
bdc471f3
|
Guillaume DAVY
|
let pp_begin_package body fmt machine =
|
51 |
7cbb6d8a
|
Guillaume DAVY
|
fprintf fmt "package %s%a is"
|
52 |
|
|
(if body then "body " else "")
|
53 |
|
|
pp_package_name machine.mname
|
54 |
bdc471f3
|
Guillaume DAVY
|
|
55 |
|
|
(** Print the ada package conclusion sentence.
|
56 |
|
|
@param fmt the formater to print on
|
57 |
|
|
@param machine the machine
|
58 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
59 |
bdc471f3
|
Guillaume DAVY
|
let pp_end_package fmt machine =
|
60 |
7cbb6d8a
|
Guillaume DAVY
|
fprintf fmt "end %a" pp_package_name machine.mname
|
61 |
b12a91e0
|
Guillaume DAVY
|
|
62 |
7cbb6d8a
|
Guillaume DAVY
|
(** Print the access of an item from an other package.
|
63 |
|
|
@param fmt the formater to print on
|
64 |
|
|
@param package the package to use
|
65 |
|
|
@param item the item which is accessed
|
66 |
|
|
**)
|
67 |
|
|
let pp_package_access fmt (package, item) =
|
68 |
|
|
fprintf fmt "%t.%t" package item
|
69 |
b12a91e0
|
Guillaume DAVY
|
|
70 |
fd834769
|
Guillaume DAVY
|
(** Print the name of the main procedure.
|
71 |
|
|
@param fmt the formater to print on
|
72 |
|
|
@param main_machine the machine associated to the main node
|
73 |
|
|
**)
|
74 |
|
|
let pp_main_procedure_name main_machine fmt =
|
75 |
|
|
fprintf fmt "main"
|
76 |
|
|
|
77 |
|
|
(** Print the name of the main ada file.
|
78 |
|
|
@param fmt the formater to print on
|
79 |
|
|
@param main_machine the machine associated to the main node
|
80 |
|
|
**)
|
81 |
|
|
let pp_main_filename fmt main_machine =
|
82 |
|
|
fprintf fmt "%t.adb" (pp_main_procedure_name main_machine)
|
83 |
|
|
|
84 |
|
|
(** Extract a node from an instance.
|
85 |
|
|
@param instance the instance
|
86 |
|
|
**)
|
87 |
|
|
let extract_node instance =
|
88 |
|
|
let (_, (node, _)) = instance in
|
89 |
fd8aeeac
|
Christophe Garion
|
match node.top_decl_desc with
|
90 |
fd834769
|
Guillaume DAVY
|
| Node nd -> nd
|
91 |
|
|
| _ -> assert false (*TODO*)
|
92 |
|
|
|
93 |
|
|
(** Print a with statement to include a node.
|
94 |
|
|
@param fmt the formater to print on
|
95 |
|
|
@param node the node
|
96 |
|
|
**)
|
97 |
|
|
let pp_with_node fmt node =
|
98 |
|
|
fprintf fmt "private with %a" pp_package_name node
|
99 |
|
|
|
100 |
|
|
|
101 |
c06b3b47
|
Guillaume DAVY
|
(* Type pretty print functions *)
|
102 |
b12a91e0
|
Guillaume DAVY
|
|
103 |
c06b3b47
|
Guillaume DAVY
|
(** Print a type declaration
|
104 |
b12a91e0
|
Guillaume DAVY
|
@param fmt the formater to print on
|
105 |
c06b3b47
|
Guillaume DAVY
|
@param pp_name a format printer which print the type name
|
106 |
|
|
@param pp_value a format printer which print the type definition
|
107 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
108 |
c06b3b47
|
Guillaume DAVY
|
let pp_type_decl fmt (pp_name, pp_definition) =
|
109 |
|
|
fprintf fmt "type %t is %t" pp_name pp_definition
|
110 |
|
|
|
111 |
|
|
(** Print a private type declaration
|
112 |
|
|
@param fmt the formater to print on
|
113 |
|
|
@param pp_name a format printer which print the type name
|
114 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
115 |
c203d676
|
Guillaume DAVY
|
let pp_private_limited_type_decl fmt pp_name =
|
116 |
|
|
let pp_definition fmt = fprintf fmt "limited private" in
|
117 |
c06b3b47
|
Guillaume DAVY
|
pp_type_decl fmt (pp_name, pp_definition)
|
118 |
|
|
|
119 |
|
|
(** Print the type of the state variable.
|
120 |
|
|
@param fmt the formater to print on
|
121 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
122 |
c06b3b47
|
Guillaume DAVY
|
let pp_state_type fmt =
|
123 |
7cbb6d8a
|
Guillaume DAVY
|
(* Type and variable names live in the same environement in Ada so name of
|
124 |
|
|
this type and of the associated parameter : pp_state_name must be
|
125 |
|
|
different *)
|
126 |
c419ca44
|
Guillaume DAVY
|
fprintf fmt "TState"
|
127 |
b12a91e0
|
Guillaume DAVY
|
|
128 |
7cbb6d8a
|
Guillaume DAVY
|
(** Print the integer type name.
|
129 |
|
|
@param fmt the formater to print on
|
130 |
|
|
**)
|
131 |
|
|
let pp_integer_type fmt = fprintf fmt "Integer"
|
132 |
|
|
|
133 |
|
|
(** Print the float type name.
|
134 |
|
|
@param fmt the formater to print on
|
135 |
|
|
**)
|
136 |
|
|
let pp_float_type fmt = fprintf fmt "Float"
|
137 |
|
|
|
138 |
|
|
(** Print the boolean type name.
|
139 |
|
|
@param fmt the formater to print on
|
140 |
|
|
**)
|
141 |
|
|
let pp_boolean_type fmt = fprintf fmt "Boolean"
|
142 |
|
|
|
143 |
b12a91e0
|
Guillaume DAVY
|
(** Print the type of a variable.
|
144 |
|
|
@param fmt the formater to print on
|
145 |
|
|
@param id the variable
|
146 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
147 |
fd8aeeac
|
Christophe Garion
|
let pp_var_type fmt id =
|
148 |
b12a91e0
|
Guillaume DAVY
|
(match (Types.repr id.var_type).Types.tdesc with
|
149 |
7cbb6d8a
|
Guillaume DAVY
|
| Types.Tbasic Types.Basic.Tint -> pp_integer_type fmt
|
150 |
|
|
| Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
|
151 |
|
|
| Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
|
152 |
b12a91e0
|
Guillaume DAVY
|
| _ -> eprintf "Type error : %a@." Types.print_ty id.var_type; assert false (*TODO*)
|
153 |
|
|
)
|
154 |
c203d676
|
Guillaume DAVY
|
|
155 |
b12a91e0
|
Guillaume DAVY
|
|
156 |
c06b3b47
|
Guillaume DAVY
|
(* Variable pretty print functions *)
|
157 |
b12a91e0
|
Guillaume DAVY
|
|
158 |
c06b3b47
|
Guillaume DAVY
|
(** Represent the possible mode for a type of a procedure parameter **)
|
159 |
|
|
type parameter_mode = NoMode | In | Out | InOut
|
160 |
b12a91e0
|
Guillaume DAVY
|
|
161 |
c06b3b47
|
Guillaume DAVY
|
(** Print a parameter_mode.
|
162 |
|
|
@param fmt the formater to print on
|
163 |
|
|
@param mode the modifier
|
164 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
165 |
c06b3b47
|
Guillaume DAVY
|
let pp_parameter_mode fmt mode =
|
166 |
|
|
fprintf fmt "%s" (match mode with
|
167 |
|
|
| NoMode -> ""
|
168 |
|
|
| In -> "in"
|
169 |
|
|
| Out -> "out"
|
170 |
|
|
| InOut -> "in out")
|
171 |
|
|
|
172 |
|
|
(** Print the name of the state variable.
|
173 |
b12a91e0
|
Guillaume DAVY
|
@param fmt the formater to print on
|
174 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
175 |
c06b3b47
|
Guillaume DAVY
|
let pp_state_name fmt =
|
176 |
|
|
fprintf fmt "state"
|
177 |
b12a91e0
|
Guillaume DAVY
|
|
178 |
7cbb6d8a
|
Guillaume DAVY
|
|
179 |
c06b3b47
|
Guillaume DAVY
|
(** Print the name of a variable.
|
180 |
b12a91e0
|
Guillaume DAVY
|
@param fmt the formater to print on
|
181 |
|
|
@param id the variable
|
182 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
183 |
c06b3b47
|
Guillaume DAVY
|
let pp_var_name fmt id =
|
184 |
fd834769
|
Guillaume DAVY
|
fprintf fmt "%a" pp_clean_ada_identifier id.var_id
|
185 |
b12a91e0
|
Guillaume DAVY
|
|
186 |
c06b3b47
|
Guillaume DAVY
|
(** Print a variable declaration
|
187 |
|
|
@param mode input/output mode of the parameter
|
188 |
|
|
@param pp_name a format printer wich print the variable name
|
189 |
|
|
@param pp_type a format printer wich print the variable type
|
190 |
|
|
@param fmt the formater to print on
|
191 |
|
|
@param id the variable
|
192 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
193 |
c06b3b47
|
Guillaume DAVY
|
let pp_var_decl fmt (mode, pp_name, pp_type) =
|
194 |
7cbb6d8a
|
Guillaume DAVY
|
fprintf fmt "%t: %a%s%t"
|
195 |
c06b3b47
|
Guillaume DAVY
|
pp_name
|
196 |
|
|
pp_parameter_mode mode
|
197 |
7cbb6d8a
|
Guillaume DAVY
|
(if mode = NoMode then "" else " ")
|
198 |
c06b3b47
|
Guillaume DAVY
|
pp_type
|
199 |
|
|
|
200 |
|
|
(** Print variable declaration for machine variable
|
201 |
|
|
@param mode input/output mode of the parameter
|
202 |
b12a91e0
|
Guillaume DAVY
|
@param fmt the formater to print on
|
203 |
|
|
@param id the variable
|
204 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
205 |
c06b3b47
|
Guillaume DAVY
|
let pp_machine_var_decl mode fmt id =
|
206 |
|
|
let pp_name = function fmt -> pp_var_name fmt id in
|
207 |
|
|
let pp_type = function fmt -> pp_var_type fmt id in
|
208 |
|
|
pp_var_decl fmt (mode, pp_name, pp_type)
|
209 |
|
|
|
210 |
|
|
(** Print variable declaration for state variable
|
211 |
|
|
@param fmt the formater to print on
|
212 |
|
|
@param mode input/output mode of the parameter
|
213 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
214 |
c06b3b47
|
Guillaume DAVY
|
let pp_state_var_decl fmt mode =
|
215 |
|
|
let pp_name = pp_state_name in
|
216 |
|
|
let pp_type = pp_state_type in
|
217 |
|
|
pp_var_decl fmt (mode, pp_name, pp_type)
|
218 |
|
|
|
219 |
fd834769
|
Guillaume DAVY
|
(** Print the declaration of a state element of node.
|
220 |
|
|
@param instance name of the variable
|
221 |
|
|
@param fmt the formater to print on
|
222 |
|
|
@param instance node
|
223 |
|
|
**)
|
224 |
|
|
let pp_node_state_decl name fmt node =
|
225 |
|
|
let pp_package fmt = pp_package_name fmt node in
|
226 |
|
|
let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
|
227 |
|
|
let pp_name fmt = pp_clean_ada_identifier fmt name in
|
228 |
|
|
pp_var_decl fmt (NoMode, pp_name, pp_type)
|
229 |
c06b3b47
|
Guillaume DAVY
|
|
230 |
c203d676
|
Guillaume DAVY
|
|
231 |
c06b3b47
|
Guillaume DAVY
|
(* Prototype pretty print functions *)
|
232 |
b12a91e0
|
Guillaume DAVY
|
|
233 |
f3e8fc18
|
Christophe Garion
|
(** Print the name of the reset procedure **)
|
234 |
903317e7
|
Guillaume DAVY
|
let pp_reset_procedure_name fmt = fprintf fmt "reset"
|
235 |
3d85297f
|
Guillaume DAVY
|
|
236 |
fd8aeeac
|
Christophe Garion
|
(** Print the name of the step procedure **)
|
237 |
3d85297f
|
Guillaume DAVY
|
let pp_step_procedure_name fmt = fprintf fmt "step"
|
238 |
|
|
|
239 |
903317e7
|
Guillaume DAVY
|
(** Print the name of the init procedure **)
|
240 |
|
|
let pp_init_procedure_name fmt = fprintf fmt "init"
|
241 |
3d85297f
|
Guillaume DAVY
|
|
242 |
fd8aeeac
|
Christophe Garion
|
(** Print the name of the clear procedure **)
|
243 |
3d85297f
|
Guillaume DAVY
|
let pp_clear_procedure_name fmt = fprintf fmt "clear"
|
244 |
|
|
|
245 |
fd834769
|
Guillaume DAVY
|
(** Print the prototype of a procedure with non input/outputs
|
246 |
|
|
@param fmt the formater to print on
|
247 |
|
|
@param name the name of the procedure
|
248 |
|
|
**)
|
249 |
903317e7
|
Guillaume DAVY
|
let pp_simple_prototype pp_name fmt =
|
250 |
fd834769
|
Guillaume DAVY
|
fprintf fmt "procedure %t" pp_name
|
251 |
|
|
|
252 |
c06b3b47
|
Guillaume DAVY
|
(** Print the prototype of a machine procedure. The first parameter is always
|
253 |
|
|
the state, state_modifier specify the modifier applying to it. The next
|
254 |
|
|
parameters are inputs and the last parameters are the outputs.
|
255 |
|
|
@param state_mode the input/output mode for the state parameter
|
256 |
b12a91e0
|
Guillaume DAVY
|
@param input list of the input parameter of the procedure
|
257 |
|
|
@param output list of the output parameter of the procedure
|
258 |
fd834769
|
Guillaume DAVY
|
@param fmt the formater to print on
|
259 |
|
|
@param name the name of the procedure
|
260 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
261 |
fd834769
|
Guillaume DAVY
|
let pp_base_prototype state_mode input output fmt pp_name =
|
262 |
3d85297f
|
Guillaume DAVY
|
fprintf fmt "procedure %t(@[<v>%a%t@[%a@]%t@[%a@])@]"
|
263 |
|
|
pp_name
|
264 |
c06b3b47
|
Guillaume DAVY
|
pp_state_var_decl state_mode
|
265 |
c419ca44
|
Guillaume DAVY
|
(Utils.pp_final_char_if_non_empty ";@," input)
|
266 |
|
|
(Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl In)) input
|
267 |
|
|
(Utils.pp_final_char_if_non_empty ";@," output)
|
268 |
|
|
(Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl Out)) output
|
269 |
b12a91e0
|
Guillaume DAVY
|
|
270 |
903317e7
|
Guillaume DAVY
|
(** Print the prototype of the step procedure of a machine.
|
271 |
b12a91e0
|
Guillaume DAVY
|
@param m the machine
|
272 |
fd834769
|
Guillaume DAVY
|
@param fmt the formater to print on
|
273 |
|
|
@param pp_name name function printer
|
274 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
275 |
903317e7
|
Guillaume DAVY
|
let pp_step_prototype m fmt =
|
276 |
|
|
pp_base_prototype InOut m.mstep.step_inputs m.mstep.step_outputs fmt pp_step_procedure_name
|
277 |
b12a91e0
|
Guillaume DAVY
|
|
278 |
903317e7
|
Guillaume DAVY
|
(** Print the prototype of the reset procedure of a machine.
|
279 |
b12a91e0
|
Guillaume DAVY
|
@param m the machine
|
280 |
fd834769
|
Guillaume DAVY
|
@param fmt the formater to print on
|
281 |
|
|
@param pp_name name function printer
|
282 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
283 |
903317e7
|
Guillaume DAVY
|
let pp_reset_prototype m fmt =
|
284 |
|
|
pp_base_prototype InOut m.mstatic [] fmt pp_reset_procedure_name
|
285 |
b12a91e0
|
Guillaume DAVY
|
|
286 |
903317e7
|
Guillaume DAVY
|
(** Print the prototype of the init procedure of a machine.
|
287 |
b12a91e0
|
Guillaume DAVY
|
@param m the machine
|
288 |
fd834769
|
Guillaume DAVY
|
@param fmt the formater to print on
|
289 |
|
|
@param pp_name name function printer
|
290 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
291 |
903317e7
|
Guillaume DAVY
|
let pp_init_prototype m fmt =
|
292 |
|
|
pp_base_prototype Out m.mstatic [] fmt pp_init_procedure_name
|
293 |
b12a91e0
|
Guillaume DAVY
|
|
294 |
|
|
(** Print the prototype of the clear procedure of a machine.
|
295 |
|
|
@param m the machine
|
296 |
fd834769
|
Guillaume DAVY
|
@param fmt the formater to print on
|
297 |
|
|
@param pp_name name function printer
|
298 |
7cbb6d8a
|
Guillaume DAVY
|
**)
|
299 |
903317e7
|
Guillaume DAVY
|
let pp_clear_prototype m fmt =
|
300 |
|
|
pp_base_prototype InOut m.mstatic [] fmt pp_clear_procedure_name
|
301 |
fd834769
|
Guillaume DAVY
|
|
302 |
|
|
|
303 |
|
|
(* Procedure pretty print functions *)
|
304 |
|
|
|
305 |
|
|
(** Print the definition of a procedure
|
306 |
|
|
@param pp_name the procedure name printer
|
307 |
|
|
@param pp_prototype the prototype printer
|
308 |
|
|
@param pp_instr local var printer
|
309 |
|
|
@param pp_instr instruction printer
|
310 |
|
|
@param fmt the formater to print on
|
311 |
|
|
@param locals locals var list
|
312 |
|
|
@param instrs instructions list
|
313 |
|
|
**)
|
314 |
|
|
let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals, instrs) =
|
315 |
903317e7
|
Guillaume DAVY
|
fprintf fmt "@[<v>%t is%t@[<v>%a%t@]@,begin@, @[<v>%a%t@]@,end %t@]"
|
316 |
|
|
pp_prototype
|
317 |
fd834769
|
Guillaume DAVY
|
(Utils.pp_final_char_if_non_empty "@, " locals)
|
318 |
|
|
(Utils.fprintf_list ~sep:";@," pp_local) locals
|
319 |
|
|
(Utils.pp_final_char_if_non_empty ";" locals)
|
320 |
|
|
(Utils.fprintf_list ~sep:";@," pp_instr) instrs
|
321 |
|
|
(Utils.pp_final_char_if_non_empty ";" instrs)
|
322 |
|
|
pp_name
|