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