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 Utils
|
13
|
open Format
|
14
|
open Machine_code_types
|
15
|
open Lustre_types
|
16
|
open Corelang
|
17
|
open Machine_code_common
|
18
|
open Misc_printer
|
19
|
open Misc_lustre_function
|
20
|
open Ada_printer
|
21
|
open Ada_backend_common
|
22
|
|
23
|
(** Main module for generating packages bodies **)
|
24
|
|
25
|
(** Printing function for basic assignement [var := value].
|
26
|
|
27
|
@param fmt the formater to print on @param var_name the name of the
|
28
|
variable @param value the value to be assigned **)
|
29
|
let pp_assign env fmt var value =
|
30
|
fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
|
31
|
|
32
|
(** Printing function for instruction. See {!type:Machine_code_types.instr_t}
|
33
|
for more details on machine types.
|
34
|
|
35
|
@param typed_submachines list of all typed machine instances of this
|
36
|
machine @param machine the current machine @param fmt the formater to
|
37
|
print on @param instr the instruction to print **)
|
38
|
let rec pp_machine_instr typed_submachines env instr fmt =
|
39
|
let pp_instr = pp_machine_instr typed_submachines env in
|
40
|
(* Print args for a step call *)
|
41
|
let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
|
42
|
(* Print a when branch of a case *)
|
43
|
let pp_when (cond, instrs) fmt =
|
44
|
fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
|
45
|
in
|
46
|
(* Print a case *)
|
47
|
let pp_case fmt (g, hl) =
|
48
|
fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
|
49
|
(List.map pp_when hl)
|
50
|
in
|
51
|
(* Print a if *)
|
52
|
(* If neg is true the we must test for the negation of the condition. It
|
53
|
first check that we don't have a negation and a else case, if so it
|
54
|
inverses the two branch and remove the negation doing a recursive call. *)
|
55
|
let pp_if fmt (neg, g, instrs1, instrs2) =
|
56
|
let pp_cond =
|
57
|
if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
|
58
|
else pp_value env
|
59
|
in
|
60
|
let pp_else =
|
61
|
match instrs2 with
|
62
|
| None ->
|
63
|
fun fmt -> fprintf fmt ""
|
64
|
| Some i2 ->
|
65
|
fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
|
66
|
in
|
67
|
fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
|
68
|
(List.map pp_instr instrs1)
|
69
|
pp_else
|
70
|
in
|
71
|
match get_instr_desc instr with
|
72
|
(* no reset *)
|
73
|
| MNoReset _ ->
|
74
|
()
|
75
|
(* TODO: handle clear_reset *)
|
76
|
| MClearReset ->
|
77
|
()
|
78
|
(* reset *)
|
79
|
| MSetReset i when List.mem_assoc i typed_submachines ->
|
80
|
let substitution, submachine = get_instance i typed_submachines in
|
81
|
let pp_package =
|
82
|
pp_package_name_with_polymorphic substitution submachine
|
83
|
in
|
84
|
let args =
|
85
|
if is_machine_statefull submachine then [ [ pp_state i ] ] else []
|
86
|
in
|
87
|
pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
|
88
|
| MLocalAssign (ident, value) ->
|
89
|
pp_assign env fmt ident value
|
90
|
| MStateAssign (ident, value) ->
|
91
|
pp_assign env fmt ident value
|
92
|
| MStep ([ i0 ], i, vl) when is_builtin_fun i ->
|
93
|
let value = mk_val (Fun (i, vl)) i0.var_type in
|
94
|
pp_assign env fmt i0 value
|
95
|
| MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
|
96
|
let substitution, submachine = get_instance i typed_submachines in
|
97
|
let pp_package =
|
98
|
pp_package_name_with_polymorphic substitution submachine
|
99
|
in
|
100
|
let input = List.map (fun x fmt -> pp_value env fmt x) vl in
|
101
|
let output = List.map pp_var_name il in
|
102
|
let args =
|
103
|
(if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
|
104
|
@ (if input != [] then [ input ] else [])
|
105
|
@ if output != [] then [ output ] else []
|
106
|
in
|
107
|
pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
|
108
|
| MBranch (_, []) ->
|
109
|
assert false
|
110
|
| MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
|
111
|
pp_if fmt (build_if g c1 i1 tl)
|
112
|
| MBranch (g, hl) ->
|
113
|
pp_case fmt (g, hl)
|
114
|
| MComment s ->
|
115
|
let lines = String.split_on_char '\n' s in
|
116
|
fprintf fmt "%a" (pp_print_list ~pp_sep:pp_print_nothing pp_oneline_comment) lines
|
117
|
| _ ->
|
118
|
assert false
|
119
|
|
120
|
(** Print the definition of the step procedure from a machine.
|
121
|
|
122
|
@param typed_submachines list of all typed machine instances of this
|
123
|
machine @param fmt the formater to print on @param machine the machine **)
|
124
|
let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
|
125
|
let transform_local_to_state_assign instr =
|
126
|
match instr.instr_desc with
|
127
|
| MLocalAssign (ident, value) ->
|
128
|
{ instr with instr_desc = MStateAssign (ident, value) }
|
129
|
| _ ->
|
130
|
instr
|
131
|
in
|
132
|
let pp_local_ghost_list, spec_instrs =
|
133
|
match m_spec_opt with
|
134
|
| None ->
|
135
|
[], []
|
136
|
| Some m_spec ->
|
137
|
( List.map
|
138
|
(build_pp_var_decl_local (Some (true, false, [], [])))
|
139
|
(List.filter
|
140
|
(fun x -> not (List.mem x.var_id guarantees))
|
141
|
m_spec.mstep.step_locals),
|
142
|
List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
|
143
|
in
|
144
|
let pp_local_list =
|
145
|
List.map (build_pp_var_decl_local None) m.mstep.step_locals
|
146
|
in
|
147
|
let pp_instr_list =
|
148
|
List.map
|
149
|
(pp_machine_instr typed_submachines env)
|
150
|
(m.mstep.step_instrs @ spec_instrs)
|
151
|
in
|
152
|
let content =
|
153
|
AdaProcedureContent
|
154
|
( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
|
155
|
@ if pp_local_list = [] then [] else [ pp_local_list ]),
|
156
|
pp_instr_list )
|
157
|
in
|
158
|
pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
|
159
|
|
160
|
(** Print the definition of the reset procedure from a machine.
|
161
|
|
162
|
@param typed_submachines list of all typed machine instances of this
|
163
|
machine @param fmt the formater to print on @param machine the machine **)
|
164
|
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
|
165
|
let build_assign = function
|
166
|
| var ->
|
167
|
mkinstr (MStateAssign (var, mk_default_value var.var_type))
|
168
|
in
|
169
|
let env, memory =
|
170
|
match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
|
171
|
in
|
172
|
let assigns = List.map build_assign memory in
|
173
|
let pp_instr_list =
|
174
|
List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
|
175
|
in
|
176
|
pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
|
177
|
(AdaProcedureContent ([], pp_instr_list))
|
178
|
|
179
|
(** Print the package definition(ads) of a machine. It requires the list of
|
180
|
all typed instance. A typed submachine instance is (ident, type_machine)
|
181
|
with ident the instance name and typed_machine is (substitution, machine)
|
182
|
with machine the machine associated to the instance and substitution the
|
183
|
instanciation of all its polymorphic types. @param fmt the formater to
|
184
|
print on @param typed_submachines list of all typed machine instances of
|
185
|
this machine @param m the machine **)
|
186
|
let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
|
187
|
=
|
188
|
let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
|
189
|
let pp_reset fmt =
|
190
|
if is_machine_statefull machine then
|
191
|
fprintf fmt "%a;@,@,"
|
192
|
(pp_reset_definition env typed_submachines)
|
193
|
(machine, opt_spec_machine)
|
194
|
else fprintf fmt ""
|
195
|
in
|
196
|
let aux pkgs (id, _) =
|
197
|
try
|
198
|
let pkg, _ = List.assoc id ada_supported_funs in
|
199
|
if List.mem pkg pkgs then pkgs else pkg :: pkgs
|
200
|
with Not_found -> pkgs
|
201
|
in
|
202
|
let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
|
203
|
let pp_content fmt =
|
204
|
fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
|
205
|
(*Define the step procedure*)
|
206
|
(pp_step_definition env typed_submachines)
|
207
|
(machine, opt_spec_machine, guarantees)
|
208
|
in
|
209
|
fprintf fmt "%a%a;@."
|
210
|
(* Include all the required packages*)
|
211
|
(pp_print_list
|
212
|
~pp_sep:pp_print_semicolon
|
213
|
~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
|
214
|
(pp_with AdaPrivate))
|
215
|
packages
|
216
|
(*Print package*)
|
217
|
(pp_package (pp_package_name machine) [] true)
|
218
|
pp_content
|
219
|
|
220
|
(* Local Variables: *)
|
221
|
(* compile-command: "make -C ../../.." *)
|
222
|
(* End: *)
|