Revision a7062da6
Added by LĂ©lio Brun over 3 years ago
src/backends/Ada/ada_backend_wrapper.ml | ||
---|---|---|
9 | 9 |
(* *) |
10 | 10 |
(********************************************************************) |
11 | 11 |
|
12 |
open Utils |
|
12 | 13 |
open Format |
13 | 14 |
open Machine_code_types |
14 | 15 |
open Lustre_types |
... | ... | |
17 | 18 |
open Ada_printer |
18 | 19 |
open Ada_backend_common |
19 | 20 |
|
20 |
module Main = struct |
|
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) ] ) |
|
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 | 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
|
|
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 | 32 |
|
33 |
let pp_package = pp_package_name_with_polymorphic [] machine in
|
|
33 |
let pp_package = pp_package_name_with_polymorphic [] machine in |
|
34 | 34 |
|
35 |
(* Dependances *)
|
|
36 |
let text_io = "Ada.Text_IO" in
|
|
35 |
(* Dependances *) |
|
36 |
let text_io = "Ada.Text_IO" in |
|
37 | 37 |
|
38 |
(* Locals *) |
|
39 |
let locals = |
|
38 |
(* Locals *) |
|
39 |
let locals = |
|
40 |
[ |
|
40 | 41 |
[ |
41 |
[ |
|
42 |
build_text_io_package_local "Integer"; |
|
43 |
build_text_io_package_local "Float"; |
|
44 |
]; |
|
45 |
] |
|
46 |
@ (if statefull then |
|
42 |
build_text_io_package_local "Integer"; |
|
43 |
build_text_io_package_local "Float"; |
|
44 |
]; |
|
45 |
] |
|
46 |
@ (if statefull then |
|
47 | 47 |
[ |
48 | 48 |
[ |
49 | 49 |
AdaLocalVar |
... | ... | |
51 | 51 |
(asprintf "%t" pp_state_name, ([], machine))); |
52 | 52 |
]; |
53 | 53 |
] |
54 |
else [])
|
|
55 |
@ (if machine.mstep.step_inputs != [] then
|
|
54 |
else []) |
|
55 |
@ (if machine.mstep.step_inputs != [] then |
|
56 | 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_basic var = |
|
66 |
match (Types.repr var.var_type).Types.tdesc with |
|
67 |
| Types.Tbasic x -> |
|
68 |
x |
|
69 |
| _ -> |
|
70 |
assert false |
|
71 |
in |
|
72 |
let pp_read fmt var = |
|
73 |
match get_basic var with |
|
74 |
| Types.Basic.Tbool -> |
|
75 |
fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0" |
|
76 |
(pp_var_name var) |
|
77 |
| _ -> |
|
78 |
fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var) |
|
79 |
pp_var_type var |
|
80 |
in |
|
81 |
let pp_write fmt var = |
|
82 |
match get_basic var with |
|
83 |
| Types.Basic.Tbool -> |
|
84 |
fprintf fmt |
|
85 |
"Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \ |
|
86 |
\"' \")" |
|
87 |
(pp_var_name var) (pp_var_name var) |
|
88 |
| Types.Basic.Tint -> |
|
89 |
fprintf fmt |
|
90 |
"Ada.Text_IO.Put(\"'%t': '\");@,\ |
|
91 |
Integer_IO.Put(%t);@,\ |
|
92 |
Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var) |
|
93 |
| Types.Basic.Treal -> |
|
94 |
fprintf fmt |
|
95 |
"Ada.Text_IO.Put(\"'%t': '\");@,\ |
|
96 |
Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\ |
|
97 |
Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var) |
|
98 |
| Types.Basic.Tstring | Types.Basic.Trat -> |
|
99 |
assert false |
|
100 |
(* Could not be the top level inputs *) |
|
101 |
in |
|
102 |
|
|
103 |
(* Loop instructions *) |
|
104 |
let pp_loop fmt = |
|
105 |
let args = |
|
106 |
pp_state_name |
|
107 |
:: |
|
108 |
List.map pp_var_name |
|
109 |
(machine.mstep.step_inputs @ machine.mstep.step_outputs) |
|
110 |
in |
|
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 |
|
111 | 82 |
fprintf fmt |
112 |
"while not Ada.Text_IO.End_Of_File loop@,\ |
|
113 |
\ @[<v>%a;@,\ |
|
114 |
%a;@,\ |
|
115 |
%a;@]@,\ |
|
116 |
end loop" |
|
117 |
(Utils.fprintf_list ~sep:";@," pp_read) |
|
118 |
machine.mstep.step_inputs pp_call |
|
119 |
(pp_package_access (pp_package, pp_step_procedure_name), [ args ]) |
|
120 |
(Utils.fprintf_list ~sep:";@," pp_write) |
|
121 |
machine.mstep.step_outputs |
|
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) |
|
122 | 103 |
in |
123 |
|
|
124 |
(* Print the file *) |
|
125 |
let instrs = |
|
126 |
(if statefull then |
|
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 |
|
127 | 120 |
[ |
128 | 121 |
(fun fmt -> |
129 |
pp_call fmt |
|
130 |
( pp_package_access (pp_package, pp_reset_procedure_name), |
|
131 |
[ [ pp_state_name ] ] )); |
|
122 |
pp_call fmt
|
|
123 |
( pp_package_access (pp_package, pp_reset_procedure_name),
|
|
124 |
[ [ pp_state_name ] ] ));
|
|
132 | 125 |
] |
133 |
else []) |
|
134 |
@ [ pp_loop ] |
|
135 |
in |
|
136 |
fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io) |
|
137 |
(pp_with AdaPrivate) (pp_package_name machine) |
|
138 |
(pp_procedure pp_main_procedure_name [] None) |
|
139 |
(AdaProcedureContent (locals, instrs)) |
|
140 |
|
|
141 |
(** Print the name of the ada project configuration file. @param fmt the |
|
142 |
formater to print on @param main_machine the machine associated to the |
|
143 |
main node **) |
|
144 |
let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename |
|
145 |
|
|
146 |
(** Print the project configuration file. @param fmt the formater to print on |
|
147 |
**) |
|
148 |
let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);" |
|
149 |
|
|
150 |
(** Print the name of the ada project file. @param base_name name of the |
|
151 |
lustre file @param fmt the formater to print on **) |
|
152 |
let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename |
|
153 |
|
|
154 |
let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg |
|
155 |
|
|
156 |
let pp_for name args fmt = |
|
157 |
fprintf fmt "for %s use (@[%a@])" name |
|
158 |
(Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg)) |
|
159 |
args |
|
160 |
|
|
161 |
let pp_content fmt lines = |
|
162 |
fprintf fmt " @[<v>%a%t@]" |
|
163 |
(Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) |
|
164 |
lines |
|
165 |
(Utils.pp_final_char_if_non_empty ";" lines) |
|
166 |
|
|
167 |
let pp_package name lines fmt = |
|
168 |
fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name |
|
169 |
|
|
170 |
(** Print the gpr project file, if there is a machine in machine_opt then an |
|
171 |
executable project is made else it is a library. @param fmt the formater |
|
172 |
to print on @param machine_opt the main machine option **) |
|
173 |
let pp_project_file machines basename fmt machine_opt = |
|
174 |
let adbs = |
|
175 |
List.map (asprintf "%a" (pp_machine_filename "adb")) machines |
|
176 |
@ |
|
177 |
match machine_opt with |
|
178 |
| None -> |
|
179 |
[] |
|
180 |
| Some m -> |
|
181 |
[ asprintf "%a" pp_main_filename m ] |
|
182 |
in |
|
183 |
let project_name = |
|
184 |
basename ^ if machine_opt = None then "_lib" else "_exe" |
|
185 |
in |
|
186 |
fprintf fmt "%sproject %s is@,%a@,end %s;" |
|
187 |
(if machine_opt = None then "library " else "") |
|
188 |
project_name pp_content |
|
189 |
((match machine_opt with |
|
190 |
| None -> |
|
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" |
|
191 | 197 |
[ |
192 |
pp_for_single "Library_Name" basename;
|
|
193 |
pp_for_single "Library_Dir" "lib";
|
|
194 |
] |
|
195 |
| Some _ ->
|
|
198 |
pp_for_single "Global_Configuration_Pragmas"
|
|
199 |
(asprintf "%a" pp_project_configuration_name basename);
|
|
200 |
];
|
|
201 |
pp_package "Prove"
|
|
196 | 202 |
[ |
197 |
pp_for "Main" [ asprintf "%t" pp_main_procedure_name ]; |
|
198 |
pp_for_single "Exec_Dir" "bin"; |
|
199 |
]) |
|
200 |
@ [ |
|
201 |
pp_for_single "Object_Dir" "obj"; |
|
202 |
pp_for "Source_Files" adbs; |
|
203 |
pp_package "Builder" |
|
204 |
[ |
|
205 |
pp_for_single "Global_Configuration_Pragmas" |
|
206 |
(asprintf "%a" pp_project_configuration_name basename); |
|
207 |
]; |
|
208 |
pp_package "Prove" |
|
209 |
[ |
|
210 |
pp_for "Switches" |
|
211 |
[ |
|
212 |
"--mode=prove"; |
|
213 |
"--report=statistics"; |
|
214 |
"--proof=per_check"; |
|
215 |
"--warnings=continue"; |
|
216 |
]; |
|
217 |
pp_for_single "Proof_Dir" (asprintf "proof"); |
|
218 |
]; |
|
219 |
]) |
|
220 |
project_name |
|
221 |
end |
|
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 |
Also available in: Unified diff
another step towards refactoring