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 Misc_printer
|
17
|
open Misc_lustre_function
|
18
|
open Ada_printer
|
19
|
open Ada_backend_common
|
20
|
|
21
|
let build_text_io_package_local typ =
|
22
|
AdaLocalPackage
|
23
|
( (fun fmt -> fprintf fmt "%s_IO" typ),
|
24
|
(fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
|
25
|
[ ((fun fmt -> fprintf fmt "Num"), fun fmt -> fprintf fmt "%s" typ) ] )
|
26
|
|
27
|
(** Print the main file calling in a loop the step function of the main
|
28
|
machine. @param fmt the formater to print on @param machine the main
|
29
|
machine **)
|
30
|
let pp_main_adb fmt machine =
|
31
|
let statefull = is_machine_statefull machine in
|
32
|
|
33
|
let pp_package = pp_package_name_with_polymorphic [] machine in
|
34
|
|
35
|
(* Dependances *)
|
36
|
let text_io = "Ada.Text_IO" in
|
37
|
|
38
|
(* Locals *)
|
39
|
let locals =
|
40
|
[
|
41
|
[
|
42
|
build_text_io_package_local "Integer";
|
43
|
build_text_io_package_local "Float";
|
44
|
];
|
45
|
]
|
46
|
@ (if statefull then
|
47
|
[
|
48
|
[
|
49
|
AdaLocalVar
|
50
|
(build_pp_state_decl_from_subinstance AdaNoMode None
|
51
|
(asprintf "%t" pp_state_name, ([], machine)));
|
52
|
];
|
53
|
]
|
54
|
else [])
|
55
|
@ (if machine.mstep.step_inputs != [] then
|
56
|
[ List.map (build_pp_var_decl_local None) machine.mstep.step_inputs ]
|
57
|
else [])
|
58
|
@
|
59
|
if machine.mstep.step_outputs != [] then
|
60
|
[ List.map (build_pp_var_decl_local None) machine.mstep.step_outputs ]
|
61
|
else []
|
62
|
in
|
63
|
|
64
|
(* Stream instructions *)
|
65
|
let get_type var = Types.repr var.var_type in
|
66
|
let pp_read fmt var =
|
67
|
if Types.is_bool_type (get_type var) then
|
68
|
fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
|
69
|
(pp_var_name var)
|
70
|
else
|
71
|
fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)
|
72
|
pp_var_type var
|
73
|
in
|
74
|
let pp_write fmt var =
|
75
|
let t = get_type var in
|
76
|
if Types.is_bool_type t then
|
77
|
fprintf fmt
|
78
|
"Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \
|
79
|
\"' \")"
|
80
|
(pp_var_name var) (pp_var_name var)
|
81
|
else if Types.is_int_type t then
|
82
|
fprintf fmt
|
83
|
"Ada.Text_IO.Put(\"'%t': '\");@,\
|
84
|
Integer_IO.Put(%t);@,\
|
85
|
Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
|
86
|
else if Types.is_real_type t then
|
87
|
fprintf fmt
|
88
|
"Ada.Text_IO.Put(\"'%t': '\");@,\
|
89
|
Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\
|
90
|
Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
|
91
|
else
|
92
|
assert false
|
93
|
(* Could not be the top level inputs *)
|
94
|
in
|
95
|
|
96
|
(* Loop instructions *)
|
97
|
let pp_loop fmt =
|
98
|
let args =
|
99
|
pp_state_name
|
100
|
::
|
101
|
List.map pp_var_name
|
102
|
(machine.mstep.step_inputs @ machine.mstep.step_outputs)
|
103
|
in
|
104
|
fprintf fmt
|
105
|
"while not Ada.Text_IO.End_Of_File loop@,\
|
106
|
\ @[<v>%a;@,\
|
107
|
%a;@,\
|
108
|
%a;@]@,\
|
109
|
end loop"
|
110
|
(pp_print_list ~pp_sep:pp_print_semicolon pp_read)
|
111
|
machine.mstep.step_inputs pp_call
|
112
|
(pp_package_access (pp_package, pp_step_procedure_name), [ args ])
|
113
|
(pp_print_list ~pp_sep:pp_print_semicolon pp_write)
|
114
|
machine.mstep.step_outputs
|
115
|
in
|
116
|
|
117
|
(* Print the file *)
|
118
|
let instrs =
|
119
|
(if statefull then
|
120
|
[
|
121
|
(fun fmt ->
|
122
|
pp_call fmt
|
123
|
( pp_package_access (pp_package, pp_reset_procedure_name),
|
124
|
[ [ pp_state_name ] ] ));
|
125
|
]
|
126
|
else [])
|
127
|
@ [ pp_loop ]
|
128
|
in
|
129
|
fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
|
130
|
(pp_with AdaPrivate) (pp_package_name machine)
|
131
|
(pp_procedure pp_main_procedure_name [] None)
|
132
|
(AdaProcedureContent (locals, instrs))
|
133
|
|
134
|
(** Print the name of the ada project configuration file. @param fmt the
|
135
|
formater to print on @param main_machine the machine associated to the
|
136
|
main node **)
|
137
|
let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename
|
138
|
|
139
|
(** Print the project configuration file. @param fmt the formater to print on
|
140
|
**)
|
141
|
let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);"
|
142
|
|
143
|
(** Print the name of the ada project file. @param base_name name of the
|
144
|
lustre file @param fmt the formater to print on **)
|
145
|
let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename
|
146
|
|
147
|
let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg
|
148
|
|
149
|
let pp_for name args fmt =
|
150
|
fprintf fmt "for %s use (@[%a@])" name
|
151
|
(pp_comma_list (fun fmt arg -> fprintf fmt "\"%s\"" arg))
|
152
|
args
|
153
|
|
154
|
let pp_content fmt lines =
|
155
|
fprintf fmt " @[<v>%a%a@]"
|
156
|
(pp_print_list ~pp_sep:pp_print_semicolon (fun fmt pp -> fprintf fmt "%t" pp))
|
157
|
lines
|
158
|
(if lines = [] then pp_print_nothing else pp_print_semicolon) ()
|
159
|
|
160
|
let pp_package name lines fmt =
|
161
|
fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name
|
162
|
|
163
|
(** Print the gpr project file, if there is a machine in machine_opt then an
|
164
|
executable project is made else it is a library. @param fmt the formater
|
165
|
to print on @param machine_opt the main machine option **)
|
166
|
let pp_project_file machines basename fmt machine_opt =
|
167
|
let adbs =
|
168
|
List.map (asprintf "%a" (pp_machine_filename "adb")) machines
|
169
|
@
|
170
|
match machine_opt with
|
171
|
| None ->
|
172
|
[]
|
173
|
| Some m ->
|
174
|
[ asprintf "%a" pp_main_filename m ]
|
175
|
in
|
176
|
let project_name =
|
177
|
basename ^ if machine_opt = None then "_lib" else "_exe"
|
178
|
in
|
179
|
fprintf fmt "%sproject %s is@,%a@,end %s;"
|
180
|
(if machine_opt = None then "library " else "")
|
181
|
project_name pp_content
|
182
|
((match machine_opt with
|
183
|
| None ->
|
184
|
[
|
185
|
pp_for_single "Library_Name" basename;
|
186
|
pp_for_single "Library_Dir" "lib";
|
187
|
]
|
188
|
| Some _ ->
|
189
|
[
|
190
|
pp_for "Main" [ asprintf "%t" pp_main_procedure_name ];
|
191
|
pp_for_single "Exec_Dir" "bin";
|
192
|
])
|
193
|
@ [
|
194
|
pp_for_single "Object_Dir" "obj";
|
195
|
pp_for "Source_Files" adbs;
|
196
|
pp_package "Builder"
|
197
|
[
|
198
|
pp_for_single "Global_Configuration_Pragmas"
|
199
|
(asprintf "%a" pp_project_configuration_name basename);
|
200
|
];
|
201
|
pp_package "Prove"
|
202
|
[
|
203
|
pp_for "Switches"
|
204
|
[
|
205
|
"--mode=prove";
|
206
|
"--report=statistics";
|
207
|
"--proof=per_check";
|
208
|
"--warnings=continue";
|
209
|
];
|
210
|
pp_for_single "Proof_Dir" (asprintf "proof");
|
211
|
];
|
212
|
])
|
213
|
project_name
|