1 |
f20d8ac7
|
Christophe Garion
|
(********************************************************************)
|
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 |
48a6309c
|
Guillaume DAVY
|
open Format
|
13 |
bdc471f3
|
Guillaume DAVY
|
|
14 |
48a6309c
|
Guillaume DAVY
|
open Machine_code_types
|
15 |
|
|
open Lustre_types
|
16 |
|
|
open Corelang
|
17 |
|
|
open Machine_code_common
|
18 |
230b168e
|
Guillaume DAVY
|
|
19 |
|
|
open Misc_printer
|
20 |
|
|
open Misc_lustre_function
|
21 |
|
|
open Ada_printer
|
22 |
bdc471f3
|
Guillaume DAVY
|
open Ada_backend_common
|
23 |
|
|
|
24 |
768f60f0
|
Christophe Garion
|
(** Main module for generating packages bodies
|
25 |
|
|
**)
|
26 |
f20d8ac7
|
Christophe Garion
|
module Main =
|
27 |
|
|
struct
|
28 |
48a6309c
|
Guillaume DAVY
|
|
29 |
b5b745fb
|
Guillaume DAVY
|
(** Printing function for basic assignement [var := value].
|
30 |
768f60f0
|
Christophe Garion
|
|
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 |
b5b745fb
|
Guillaume DAVY
|
let pp_assign env fmt var value =
|
36 |
c85c2e3d
|
Christophe Garion
|
fprintf fmt "%a := %a"
|
37 |
b5b745fb
|
Guillaume DAVY
|
(pp_var env) var
|
38 |
|
|
(pp_value env) value
|
39 |
768f60f0
|
Christophe Garion
|
|
40 |
|
|
(** Printing function for instruction. See
|
41 |
|
|
{!type:Machine_code_types.instr_t} for more details on
|
42 |
|
|
machine types.
|
43 |
|
|
|
44 |
09d7b39f
|
Guillaume DAVY
|
@param typed_submachines list of all typed machine instances of this machine
|
45 |
768f60f0
|
Christophe Garion
|
@param machine the current machine
|
46 |
|
|
@param fmt the formater to print on
|
47 |
|
|
@param instr the instruction to print
|
48 |
|
|
**)
|
49 |
b5b745fb
|
Guillaume DAVY
|
let rec pp_machine_instr typed_submachines env instr fmt =
|
50 |
|
|
let pp_instr = pp_machine_instr typed_submachines env in
|
51 |
6e3cdaf6
|
Guillaume DAVY
|
(* Print args for a step call *)
|
52 |
826063db
|
Guillaume DAVY
|
let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
|
53 |
6e3cdaf6
|
Guillaume DAVY
|
(* Print a when branch of a case *)
|
54 |
230b168e
|
Guillaume DAVY
|
let pp_when (cond, instrs) fmt =
|
55 |
|
|
fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
|
56 |
6e3cdaf6
|
Guillaume DAVY
|
in
|
57 |
|
|
(* Print a case *)
|
58 |
525eebd1
|
Guillaume DAVY
|
let pp_case fmt (g, hl) =
|
59 |
|
|
fprintf fmt "case %a is@,%aend case"
|
60 |
b5b745fb
|
Guillaume DAVY
|
(pp_value env) g
|
61 |
230b168e
|
Guillaume DAVY
|
pp_block (List.map pp_when hl)
|
62 |
525eebd1
|
Guillaume DAVY
|
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 |
b5b745fb
|
Guillaume DAVY
|
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 |
6e3cdaf6
|
Guillaume DAVY
|
in
|
85 |
768f60f0
|
Christophe Garion
|
match get_instr_desc instr with
|
86 |
3de9f6e4
|
Guillaume DAVY
|
(* no reset *)
|
87 |
|
|
| MNoReset _ -> ()
|
88 |
|
|
(* reset *)
|
89 |
826063db
|
Guillaume DAVY
|
| MReset i when List.mem_assoc i typed_submachines ->
|
90 |
|
|
let (substitution, submachine) = get_instance i typed_submachines in
|
91 |
230b168e
|
Guillaume DAVY
|
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 |
3de9f6e4
|
Guillaume DAVY
|
| MLocalAssign (ident, value) ->
|
95 |
b5b745fb
|
Guillaume DAVY
|
pp_assign env fmt ident value
|
96 |
3de9f6e4
|
Guillaume DAVY
|
| MStateAssign (ident, value) ->
|
97 |
b5b745fb
|
Guillaume DAVY
|
pp_assign env fmt ident value
|
98 |
09d7b39f
|
Guillaume DAVY
|
| MStep ([i0], i, vl) when is_builtin_fun i ->
|
99 |
3de9f6e4
|
Guillaume DAVY
|
let value = mk_val (Fun (i, vl)) i0.var_type in
|
100 |
b5b745fb
|
Guillaume DAVY
|
pp_assign env fmt i0 value
|
101 |
09d7b39f
|
Guillaume DAVY
|
| MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
|
102 |
826063db
|
Guillaume DAVY
|
let (substitution, submachine) = get_instance i typed_submachines in
|
103 |
230b168e
|
Guillaume DAVY
|
let pp_package = pp_package_name_with_polymorphic substitution submachine in
|
104 |
b5b745fb
|
Guillaume DAVY
|
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 |
230b168e
|
Guillaume DAVY
|
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 |
6e3cdaf6
|
Guillaume DAVY
|
| MBranch (_, []) -> assert false
|
113 |
525eebd1
|
Guillaume DAVY
|
| MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
|
114 |
b5b745fb
|
Guillaume DAVY
|
pp_if fmt (build_if g c1 i1 tl)
|
115 |
6e3cdaf6
|
Guillaume DAVY
|
| MBranch (g, hl) -> pp_case fmt (g, hl)
|
116 |
3de9f6e4
|
Guillaume DAVY
|
| MComment s ->
|
117 |
6e3cdaf6
|
Guillaume DAVY
|
let lines = String.split_on_char '\n' s in
|
118 |
|
|
fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
|
119 |
09d7b39f
|
Guillaume DAVY
|
| _ -> assert false
|
120 |
3d85297f
|
Guillaume DAVY
|
|
121 |
8d22ea35
|
Guillaume DAVY
|
(** 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 |
173a2a8f
|
Guillaume DAVY
|
let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
|
128 |
b5b745fb
|
Guillaume DAVY
|
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 |
230b168e
|
Guillaume DAVY
|
in
|
134 |
173a2a8f
|
Guillaume DAVY
|
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, [], []))) (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 |
230b168e
|
Guillaume DAVY
|
in
|
140 |
b5b745fb
|
Guillaume DAVY
|
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 |
173a2a8f
|
Guillaume DAVY
|
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 |
230b168e
|
Guillaume DAVY
|
pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
|
144 |
8d22ea35
|
Guillaume DAVY
|
|
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 |
173a2a8f
|
Guillaume DAVY
|
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
|
152 |
61e0c3c4
|
Guillaume DAVY
|
let build_assign = function var ->
|
153 |
|
|
mkinstr (MStateAssign (var, mk_default_value var.var_type))
|
154 |
|
|
in
|
155 |
173a2a8f
|
Guillaume DAVY
|
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 |
b5b745fb
|
Guillaume DAVY
|
let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
|
163 |
230b168e
|
Guillaume DAVY
|
pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
|
164 |
8d22ea35
|
Guillaume DAVY
|
|
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 |
173a2a8f
|
Guillaume DAVY
|
let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees, past_size), machine)) =
|
176 |
b5b745fb
|
Guillaume DAVY
|
let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
|
177 |
8d22ea35
|
Guillaume DAVY
|
let pp_reset fmt =
|
178 |
|
|
if is_machine_statefull machine then
|
179 |
173a2a8f
|
Guillaume DAVY
|
fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
|
180 |
09d7b39f
|
Guillaume DAVY
|
else
|
181 |
8d22ea35
|
Guillaume DAVY
|
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 |
230b168e
|
Guillaume DAVY
|
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 |
173a2a8f
|
Guillaume DAVY
|
(pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
|
200 |
230b168e
|
Guillaume DAVY
|
in
|
201 |
|
|
fprintf fmt "%a%t%a;@."
|
202 |
8d22ea35
|
Guillaume DAVY
|
|
203 |
|
|
(* Include all the required packages*)
|
204 |
173a2a8f
|
Guillaume DAVY
|
(Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
|
205 |
8d22ea35
|
Guillaume DAVY
|
(Utils.pp_final_char_if_non_empty ";@,@," packages)
|
206 |
|
|
|
207 |
230b168e
|
Guillaume DAVY
|
(*Print package*)
|
208 |
|
|
(pp_package (pp_package_name machine) [] true ) pp_content
|
209 |
48a6309c
|
Guillaume DAVY
|
|
210 |
f20d8ac7
|
Christophe Garion
|
end
|
211 |
768f60f0
|
Christophe Garion
|
|
212 |
|
|
(* Local Variables: *)
|
213 |
|
|
(* compile-command: "make -C ../../.." *)
|
214 |
|
|
(* End: *)
|