1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT - ISAE-SUPAERO *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Format
|
13
|
|
14
|
open Machine_code_types
|
15
|
open Lustre_types
|
16
|
open Corelang
|
17
|
open Machine_code_common
|
18
|
open Ada_backend_common
|
19
|
|
20
|
(** Main module for generating packages bodies
|
21
|
**)
|
22
|
module Main =
|
23
|
struct
|
24
|
|
25
|
(** Printing function for basic assignement [var_name := value].
|
26
|
|
27
|
@param fmt the formater to print on
|
28
|
@param var_name the name of the variable
|
29
|
@param value the value to be assigned
|
30
|
**)
|
31
|
let pp_basic_assign m fmt var_name value =
|
32
|
fprintf fmt "%a := %a"
|
33
|
(pp_access_var m) var_name
|
34
|
(pp_value m) value
|
35
|
|
36
|
(** Extract from a machine the instance corresponding to the identifier,
|
37
|
assume that the identifier exists in the instances of the machine.
|
38
|
|
39
|
@param identifier the instance identifier
|
40
|
@param machine a machine
|
41
|
@return the instance of machine.minstances corresponding to identifier
|
42
|
**)
|
43
|
let get_instance identifier typed_submachines =
|
44
|
try
|
45
|
List.assoc identifier typed_submachines
|
46
|
with Not_found -> assert false
|
47
|
|
48
|
(** Printing a call to a package function
|
49
|
|
50
|
@param typed_submachines list of all typed machine instances of this machine
|
51
|
@param pp_name printer for the function name
|
52
|
@param fmt the formater to use
|
53
|
@param identifier the instance identifier
|
54
|
@param pp_args_opt optional printer for other arguments
|
55
|
**)
|
56
|
let pp_package_call typed_submachines pp_name fmt (identifier, pp_args_opt) =
|
57
|
let (substitution, submachine) = get_instance identifier typed_submachines in
|
58
|
let statefull = is_machine_statefull submachine in
|
59
|
let pp_opt fmt = function
|
60
|
| Some pp_args when statefull -> fprintf fmt ",@,%t" pp_args
|
61
|
| Some pp_args -> pp_args fmt
|
62
|
| None -> fprintf fmt ""
|
63
|
in
|
64
|
let pp_state fmt =
|
65
|
if statefull then
|
66
|
fprintf fmt "%t.%s" pp_state_name identifier
|
67
|
else
|
68
|
fprintf fmt ""
|
69
|
in
|
70
|
fprintf fmt "%a.%t(@[<v>%t%a@])"
|
71
|
(pp_package_name_with_polymorphic substitution) submachine
|
72
|
pp_name
|
73
|
pp_state
|
74
|
pp_opt pp_args_opt
|
75
|
|
76
|
(** Printing function for instruction. See
|
77
|
{!type:Machine_code_types.instr_t} for more details on
|
78
|
machine types.
|
79
|
|
80
|
@param typed_submachines list of all typed machine instances of this machine
|
81
|
@param machine the current machine
|
82
|
@param fmt the formater to print on
|
83
|
@param instr the instruction to print
|
84
|
**)
|
85
|
let rec pp_machine_instr typed_submachines machine fmt instr =
|
86
|
let pp_instr = pp_machine_instr typed_submachines machine in
|
87
|
(* Print args for a step call *)
|
88
|
let pp_args vl il fmt =
|
89
|
fprintf fmt "@[%a@]%t@[%a@]"
|
90
|
(Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl
|
91
|
(Utils.pp_final_char_if_non_empty ",@," il)
|
92
|
(Utils.fprintf_list ~sep:",@ " (pp_access_var machine)) il
|
93
|
in
|
94
|
(* Print a when branch of a case *)
|
95
|
let pp_when fmt (cond, instrs) =
|
96
|
fprintf fmt "when %s =>@,%a" cond (pp_block pp_instr) instrs
|
97
|
in
|
98
|
(* Print a case *)
|
99
|
let pp_case fmt (g, hl) =
|
100
|
fprintf fmt "case %a is@,%aend case"
|
101
|
(pp_value machine) g
|
102
|
(pp_block pp_when) hl
|
103
|
in
|
104
|
(* Print a if *)
|
105
|
(* If neg is true the we must test for the negation of the condition. It
|
106
|
first check that we don't have a negation and a else case, if so it
|
107
|
inverses the two branch and remove the negation doing a recursive
|
108
|
call. *)
|
109
|
let rec pp_if neg fmt (g, instrs1, instrs2) =
|
110
|
match neg, instrs2 with
|
111
|
| true, Some x -> pp_if false fmt (g, x, Some instrs1)
|
112
|
| _ ->
|
113
|
let pp_cond =
|
114
|
if neg then
|
115
|
fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
|
116
|
else
|
117
|
pp_value machine
|
118
|
in
|
119
|
let pp_else = match instrs2 with
|
120
|
| None -> fun fmt -> fprintf fmt ""
|
121
|
| Some i2 -> fun fmt ->
|
122
|
fprintf fmt "else@,%a" (pp_block pp_instr) i2
|
123
|
in
|
124
|
fprintf fmt "if %a then@,%a%tend if"
|
125
|
pp_cond g
|
126
|
(pp_block pp_instr) instrs1
|
127
|
pp_else
|
128
|
in
|
129
|
match get_instr_desc instr with
|
130
|
(* no reset *)
|
131
|
| MNoReset _ -> ()
|
132
|
(* reset *)
|
133
|
| MReset i ->
|
134
|
pp_package_call
|
135
|
typed_submachines
|
136
|
pp_reset_procedure_name
|
137
|
fmt
|
138
|
(i, None)
|
139
|
| MLocalAssign (ident, value) ->
|
140
|
pp_basic_assign machine fmt ident value
|
141
|
| MStateAssign (ident, value) ->
|
142
|
pp_basic_assign machine fmt ident value
|
143
|
| MStep ([i0], i, vl) when is_builtin_fun i ->
|
144
|
let value = mk_val (Fun (i, vl)) i0.var_type in
|
145
|
pp_basic_assign machine fmt i0 value
|
146
|
| MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
|
147
|
pp_package_call
|
148
|
typed_submachines
|
149
|
pp_step_procedure_name
|
150
|
fmt
|
151
|
(i, Some (pp_args vl il))
|
152
|
| MBranch (_, []) -> assert false
|
153
|
| MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
|
154
|
let neg = c1=tag_false in
|
155
|
let other = match tl with
|
156
|
| [] -> None
|
157
|
| [(c2, i2)] -> Some i2
|
158
|
| _ -> assert false
|
159
|
in
|
160
|
pp_if neg fmt (g, i1, other)
|
161
|
| MBranch (g, hl) -> pp_case fmt (g, hl)
|
162
|
| MComment s ->
|
163
|
let lines = String.split_on_char '\n' s in
|
164
|
fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
|
165
|
| _ -> assert false
|
166
|
|
167
|
(** Print the definition of the step procedure from a machine.
|
168
|
|
169
|
@param typed_submachines list of all typed machine instances of this machine
|
170
|
@param fmt the formater to print on
|
171
|
@param machine the machine
|
172
|
**)
|
173
|
let pp_step_definition typed_submachines fmt m =
|
174
|
pp_procedure_definition
|
175
|
pp_step_procedure_name
|
176
|
(pp_step_prototype m)
|
177
|
(pp_machine_var_decl NoMode)
|
178
|
(pp_machine_instr typed_submachines m)
|
179
|
fmt
|
180
|
(m.mstep.step_locals, m.mstep.step_instrs)
|
181
|
|
182
|
(** Print the definition of the reset procedure from a machine.
|
183
|
|
184
|
@param typed_submachines list of all typed machine instances of this machine
|
185
|
@param fmt the formater to print on
|
186
|
@param machine the machine
|
187
|
**)
|
188
|
let pp_reset_definition typed_submachines fmt m =
|
189
|
let build_assign = function var ->
|
190
|
mkinstr (MStateAssign (var, mk_default_value var.var_type))
|
191
|
in
|
192
|
let assigns = List.map build_assign m.mmemory in
|
193
|
pp_procedure_definition
|
194
|
pp_reset_procedure_name
|
195
|
(pp_reset_prototype m)
|
196
|
(pp_machine_var_decl NoMode)
|
197
|
(pp_machine_instr typed_submachines m)
|
198
|
fmt
|
199
|
([], assigns@m.minit)
|
200
|
|
201
|
(** Print the package definition(ads) of a machine.
|
202
|
It requires the list of all typed instance.
|
203
|
A typed submachine instance is (ident, type_machine) with ident
|
204
|
the instance name and typed_machine is (substitution, machine) with machine
|
205
|
the machine associated to the instance and substitution the instanciation of
|
206
|
all its polymorphic types.
|
207
|
@param fmt the formater to print on
|
208
|
@param typed_submachines list of all typed machine instances of this machine
|
209
|
@param m the machine
|
210
|
**)
|
211
|
let pp_file fmt (typed_submachines, machine) =
|
212
|
let pp_reset fmt =
|
213
|
if is_machine_statefull machine then
|
214
|
fprintf fmt "%a;@,@," (pp_reset_definition typed_submachines) machine
|
215
|
else
|
216
|
fprintf fmt ""
|
217
|
in
|
218
|
let aux pkgs (id, _) =
|
219
|
try
|
220
|
let (pkg, _) = List.assoc id ada_supported_funs in
|
221
|
if List.mem pkg pkgs then
|
222
|
pkgs
|
223
|
else
|
224
|
pkg::pkgs
|
225
|
with Not_found -> pkgs
|
226
|
in
|
227
|
let packages = List.fold_left aux [] machine.mcalls in
|
228
|
fprintf fmt "%a%t%a@, @[<v>@,%t%a;@,@]@,%a;@."
|
229
|
|
230
|
(* Include all the required packages*)
|
231
|
(Utils.fprintf_list ~sep:";@," pp_with) packages
|
232
|
(Utils.pp_final_char_if_non_empty ";@,@," packages)
|
233
|
|
234
|
(*Begin the package*)
|
235
|
(pp_begin_package true) machine
|
236
|
|
237
|
(*Define the reset procedure*)
|
238
|
pp_reset
|
239
|
|
240
|
(*Define the step procedure*)
|
241
|
(pp_step_definition typed_submachines) machine
|
242
|
|
243
|
(*End the package*)
|
244
|
pp_end_package machine
|
245
|
|
246
|
end
|
247
|
|
248
|
(* Local Variables: *)
|
249
|
(* compile-command: "make -C ../../.." *)
|
250
|
(* End: *)
|