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