7 |
7 |
|
8 |
8 |
(** All the pretty print functions common to the ada backend **)
|
9 |
9 |
|
|
10 |
|
|
11 |
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
|
|
12 |
underscore and must not contain a double underscore
|
|
13 |
@param var name to be cleaned*)
|
|
14 |
let print_clean_ada_identifier fmt name =
|
|
15 |
let base_size = String.length name in
|
|
16 |
assert(base_size > 0);
|
|
17 |
let rec remove_double_underscore s = function
|
|
18 |
| i when i == String.length s - 1 -> s
|
|
19 |
| i when String.get s i == '_' && String.get s (i+1) == '_' ->
|
|
20 |
remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
|
|
21 |
| i -> remove_double_underscore s (i+1)
|
|
22 |
in
|
|
23 |
let name = remove_double_underscore name 0 in
|
|
24 |
let prefix = if String.length name != base_size
|
|
25 |
|| String.get name 0 == '_' then
|
|
26 |
"ada"
|
|
27 |
else
|
|
28 |
""
|
|
29 |
in
|
|
30 |
fprintf fmt "%s%s" prefix name
|
|
31 |
|
|
32 |
|
10 |
33 |
(* Package pretty print functions *)
|
11 |
34 |
|
12 |
35 |
(** Print the name of a package associated to a machine.
|
13 |
36 |
@param fmt the formater to print on
|
14 |
37 |
@param machine the machine
|
15 |
|
*)
|
16 |
|
let pp_package_name fmt machine =
|
17 |
|
fprintf fmt "%s" machine.mname.node_id
|
|
38 |
**)
|
|
39 |
let pp_package_name fmt node =
|
|
40 |
fprintf fmt "%a" print_clean_ada_identifier node.node_id
|
18 |
41 |
|
19 |
42 |
(** Print the ada package introduction sentence it can be used for body and
|
20 |
43 |
declaration. Boolean parameter body should be true if it is a body delcaration.
|
21 |
44 |
@param fmt the formater to print on
|
22 |
45 |
@param fmt the formater to print on
|
23 |
46 |
@param machine the machine
|
24 |
|
*)
|
|
47 |
**)
|
25 |
48 |
let pp_begin_package body fmt machine =
|
26 |
|
fprintf fmt "package %s %a is"
|
27 |
|
(if body then "body" else "")
|
28 |
|
pp_package_name machine
|
|
49 |
fprintf fmt "package %s%a is"
|
|
50 |
(if body then "body " else "")
|
|
51 |
pp_package_name machine.mname
|
29 |
52 |
|
30 |
53 |
(** Print the ada package conclusion sentence.
|
31 |
54 |
@param fmt the formater to print on
|
32 |
55 |
@param machine the machine
|
33 |
|
*)
|
|
56 |
**)
|
34 |
57 |
let pp_end_package fmt machine =
|
35 |
|
fprintf fmt "end %a" pp_package_name machine
|
|
58 |
fprintf fmt "end %a" pp_package_name machine.mname
|
36 |
59 |
|
|
60 |
(** Print the access of an item from an other package.
|
|
61 |
@param fmt the formater to print on
|
|
62 |
@param package the package to use
|
|
63 |
@param item the item which is accessed
|
|
64 |
**)
|
|
65 |
let pp_package_access fmt (package, item) =
|
|
66 |
fprintf fmt "%t.%t" package item
|
37 |
67 |
|
38 |
68 |
(* Type pretty print functions *)
|
39 |
69 |
|
... | ... | |
41 |
71 |
@param fmt the formater to print on
|
42 |
72 |
@param pp_name a format printer which print the type name
|
43 |
73 |
@param pp_value a format printer which print the type definition
|
44 |
|
*)
|
|
74 |
**)
|
45 |
75 |
let pp_type_decl fmt (pp_name, pp_definition) =
|
46 |
76 |
fprintf fmt "type %t is %t" pp_name pp_definition
|
47 |
77 |
|
48 |
78 |
(** Print a private type declaration
|
49 |
79 |
@param fmt the formater to print on
|
50 |
80 |
@param pp_name a format printer which print the type name
|
51 |
|
*)
|
|
81 |
**)
|
52 |
82 |
let pp_private_type_decl fmt pp_name =
|
53 |
83 |
let pp_definition fmt = fprintf fmt "private" in
|
54 |
84 |
pp_type_decl fmt (pp_name, pp_definition)
|
55 |
85 |
|
56 |
86 |
(** Print the type of the state variable.
|
57 |
87 |
@param fmt the formater to print on
|
58 |
|
*)
|
|
88 |
**)
|
59 |
89 |
let pp_state_type fmt =
|
|
90 |
(* Type and variable names live in the same environement in Ada so name of
|
|
91 |
this type and of the associated parameter : pp_state_name must be
|
|
92 |
different *)
|
60 |
93 |
fprintf fmt "TState"
|
61 |
94 |
|
|
95 |
(** Print the integer type name.
|
|
96 |
@param fmt the formater to print on
|
|
97 |
**)
|
|
98 |
let pp_integer_type fmt = fprintf fmt "Integer"
|
|
99 |
|
|
100 |
(** Print the float type name.
|
|
101 |
@param fmt the formater to print on
|
|
102 |
**)
|
|
103 |
let pp_float_type fmt = fprintf fmt "Float"
|
|
104 |
|
|
105 |
(** Print the boolean type name.
|
|
106 |
@param fmt the formater to print on
|
|
107 |
**)
|
|
108 |
let pp_boolean_type fmt = fprintf fmt "Boolean"
|
|
109 |
|
62 |
110 |
(** Print the type of a variable.
|
63 |
111 |
@param fmt the formater to print on
|
64 |
112 |
@param id the variable
|
65 |
|
*)
|
66 |
|
let pp_var_type fmt id = fprintf fmt
|
|
113 |
**)
|
|
114 |
let pp_var_type fmt id =
|
67 |
115 |
(match (Types.repr id.var_type).Types.tdesc with
|
68 |
|
| Types.Tbasic Types.Basic.Tint -> "Integer"
|
69 |
|
| Types.Tbasic Types.Basic.Treal -> "Float"
|
70 |
|
| Types.Tbasic Types.Basic.Tbool -> "Boolean"
|
|
116 |
| Types.Tbasic Types.Basic.Tint -> pp_integer_type fmt
|
|
117 |
| Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
|
|
118 |
| Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
|
71 |
119 |
| _ -> eprintf "Type error : %a@." Types.print_ty id.var_type; assert false (*TODO*)
|
72 |
120 |
)
|
73 |
121 |
|
... | ... | |
80 |
128 |
(** Print a parameter_mode.
|
81 |
129 |
@param fmt the formater to print on
|
82 |
130 |
@param mode the modifier
|
83 |
|
*)
|
|
131 |
**)
|
84 |
132 |
let pp_parameter_mode fmt mode =
|
85 |
133 |
fprintf fmt "%s" (match mode with
|
86 |
134 |
| NoMode -> ""
|
... | ... | |
90 |
138 |
|
91 |
139 |
(** Print the name of the state variable.
|
92 |
140 |
@param fmt the formater to print on
|
93 |
|
*)
|
|
141 |
**)
|
94 |
142 |
let pp_state_name fmt =
|
95 |
143 |
fprintf fmt "state"
|
96 |
144 |
|
|
145 |
|
97 |
146 |
(** Print the name of a variable.
|
98 |
147 |
@param fmt the formater to print on
|
99 |
148 |
@param id the variable
|
100 |
|
*)
|
|
149 |
**)
|
101 |
150 |
let pp_var_name fmt id =
|
102 |
|
let base_size = String.length id.var_id in
|
103 |
|
assert(base_size > 0);
|
104 |
|
let rec remove_double_underscore s = function
|
105 |
|
| i when i == String.length s - 1 -> s
|
106 |
|
| i when String.get s i == '_' && String.get s (i+1) == '_' ->
|
107 |
|
remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
|
108 |
|
| i -> remove_double_underscore s (i+1)
|
109 |
|
in
|
110 |
|
let name = remove_double_underscore id.var_id 0 in
|
111 |
|
let prefix = if String.length name == base_size
|
112 |
|
|| String.get id.var_id 0 == '_' then
|
113 |
|
"ada"
|
114 |
|
else
|
115 |
|
""
|
116 |
|
in
|
117 |
|
fprintf fmt "%s%s" prefix name
|
|
151 |
fprintf fmt "%a" print_clean_ada_identifier id.var_id
|
118 |
152 |
|
119 |
153 |
(** Print a variable declaration
|
120 |
154 |
@param mode input/output mode of the parameter
|
... | ... | |
122 |
156 |
@param pp_type a format printer wich print the variable type
|
123 |
157 |
@param fmt the formater to print on
|
124 |
158 |
@param id the variable
|
125 |
|
*)
|
|
159 |
**)
|
126 |
160 |
let pp_var_decl fmt (mode, pp_name, pp_type) =
|
127 |
|
fprintf fmt "%t: %a %t"
|
|
161 |
fprintf fmt "%t: %a%s%t"
|
128 |
162 |
pp_name
|
129 |
163 |
pp_parameter_mode mode
|
|
164 |
(if mode = NoMode then "" else " ")
|
130 |
165 |
pp_type
|
131 |
166 |
|
132 |
167 |
(** Print variable declaration for machine variable
|
133 |
168 |
@param mode input/output mode of the parameter
|
134 |
169 |
@param fmt the formater to print on
|
135 |
170 |
@param id the variable
|
136 |
|
*)
|
|
171 |
**)
|
137 |
172 |
let pp_machine_var_decl mode fmt id =
|
138 |
173 |
let pp_name = function fmt -> pp_var_name fmt id in
|
139 |
174 |
let pp_type = function fmt -> pp_var_type fmt id in
|
... | ... | |
142 |
177 |
(** Print variable declaration for state variable
|
143 |
178 |
@param fmt the formater to print on
|
144 |
179 |
@param mode input/output mode of the parameter
|
145 |
|
*)
|
|
180 |
**)
|
146 |
181 |
let pp_state_var_decl fmt mode =
|
147 |
182 |
let pp_name = pp_state_name in
|
148 |
183 |
let pp_type = pp_state_type in
|
... | ... | |
171 |
206 |
@param state_mode the input/output mode for the state parameter
|
172 |
207 |
@param input list of the input parameter of the procedure
|
173 |
208 |
@param output list of the output parameter of the procedure
|
174 |
|
*)
|
|
209 |
**)
|
175 |
210 |
let pp_simple_prototype fmt (pp_name, state_mode, input, output) =
|
176 |
211 |
fprintf fmt "procedure %t(@[<v>%a%t@[%a@]%t@[%a@])@]"
|
177 |
212 |
pp_name
|
... | ... | |
184 |
219 |
(** Print the prototype of the init procedure of a machine.
|
185 |
220 |
@param fmt the formater to print on
|
186 |
221 |
@param m the machine
|
187 |
|
*)
|
|
222 |
**)
|
188 |
223 |
let pp_init_prototype fmt m =
|
189 |
224 |
pp_simple_prototype fmt (pp_init_procedure_name, Out, m.mstatic, [])
|
190 |
225 |
|
191 |
226 |
(** Print the prototype of the step procedure of a machine.
|
192 |
227 |
@param fmt the formater to print on
|
193 |
228 |
@param m the machine
|
194 |
|
*)
|
|
229 |
**)
|
195 |
230 |
let pp_step_prototype fmt m =
|
196 |
231 |
pp_simple_prototype fmt (pp_step_procedure_name, InOut, m.mstep.step_inputs, m.mstep.step_outputs)
|
197 |
232 |
|
198 |
233 |
(** Print the prototype of the reset procedure of a machine.
|
199 |
234 |
@param fmt the formater to print on
|
200 |
235 |
@param m the machine
|
201 |
|
*)
|
|
236 |
**)
|
202 |
237 |
let pp_reset_prototype fmt m =
|
203 |
238 |
pp_simple_prototype fmt (pp_reset_procedure_name, InOut, m.mstatic, [])
|
204 |
239 |
|
205 |
240 |
(** Print the prototype of the clear procedure of a machine.
|
206 |
241 |
@param fmt the formater to print on
|
207 |
242 |
@param m the machine
|
208 |
|
*)
|
|
243 |
**)
|
209 |
244 |
let pp_clear_prototype fmt m =
|
210 |
245 |
pp_simple_prototype fmt (pp_clear_procedure_name, InOut, m.mstatic, [])
|
Ada: Add to the machine state all its subinstance states. Improve also identifier cleaning