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 Ada_backend_common
|
16
|
open Lustre_types
|
17
|
|
18
|
module Main =
|
19
|
struct
|
20
|
|
21
|
(** Print the main procedure
|
22
|
@param fmt the formater to print on
|
23
|
@param machine the main machine
|
24
|
@param locals list of local variable printers
|
25
|
@param instrs list of instructions printer
|
26
|
**)
|
27
|
let pp_main_procedure_definition machine fmt (locals, instrs) =
|
28
|
pp_procedure_definition
|
29
|
pp_main_procedure_name
|
30
|
(pp_simple_prototype pp_main_procedure_name)
|
31
|
(fun fmt local -> fprintf fmt "%t" local)
|
32
|
(fun fmt instr -> fprintf fmt "%t" instr)
|
33
|
fmt
|
34
|
(locals, instrs)
|
35
|
|
36
|
(** Print call to machine procedure on state.
|
37
|
@param instance name of the variable
|
38
|
@param fmt the formater to print on
|
39
|
@param instance node
|
40
|
**)
|
41
|
let pp_node_reset_call name fmt node =
|
42
|
let pp_package fmt = pp_package_name fmt node in
|
43
|
let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
|
44
|
let pp_name fmt = pp_clean_ada_identifier fmt name in
|
45
|
pp_var_decl fmt (NoMode, pp_name, pp_type)
|
46
|
|
47
|
(** Print the main file calling in a loop the step function of the main machine.
|
48
|
@param fmt the formater to print on
|
49
|
@param machine the main machine
|
50
|
**)
|
51
|
let pp_main_adb fmt machine =
|
52
|
let pp_str str fmt = fprintf fmt "%s" str in
|
53
|
(* Dependances *)
|
54
|
let text_io = "Ada.Text_IO" in
|
55
|
let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
|
56
|
let integer_io = "package Integer_IO is new Ada.Text_IO.Integer_IO(Integer)" in
|
57
|
|
58
|
(* Locals *)
|
59
|
let stateVar = "state" in
|
60
|
let step_parameters = machine.mstep.step_inputs@machine.mstep.step_outputs in
|
61
|
let pp_local_state_var_decl fmt = pp_node_state_decl [] stateVar fmt machine in
|
62
|
let apply_pp_var_decl var fmt = pp_machine_var_decl NoMode fmt var in
|
63
|
let locals = List.map apply_pp_var_decl step_parameters in
|
64
|
let locals = (pp_str integer_io)::(pp_str float_io)::pp_local_state_var_decl::locals in
|
65
|
|
66
|
(* Node instructions *)
|
67
|
let pp_reset fmt =
|
68
|
fprintf fmt "%a.reset(%s)"
|
69
|
pp_package_name machine
|
70
|
stateVar in
|
71
|
let pp_step fmt =
|
72
|
fprintf fmt "%a.step(@[%s,@ %a@])"
|
73
|
pp_package_name machine
|
74
|
stateVar
|
75
|
(Utils.fprintf_list ~sep:",@ " pp_var_name) step_parameters in
|
76
|
|
77
|
(* Stream instructions *)
|
78
|
let get_basic var = match (Types.repr var.var_type ).Types.tdesc with
|
79
|
Types.Tbasic x -> x | _ -> assert false in
|
80
|
let pp_read fmt var =
|
81
|
match get_basic var with
|
82
|
| Types.Basic.Tbool ->
|
83
|
fprintf fmt "%a := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
|
84
|
pp_var_name var
|
85
|
| _ ->
|
86
|
fprintf fmt "%a := %a'Value(Ada.Text_IO.Get_Line)"
|
87
|
pp_var_name var
|
88
|
pp_var_type var
|
89
|
in
|
90
|
let pp_write fmt var =
|
91
|
match get_basic var with
|
92
|
| Types.Basic.Tbool ->
|
93
|
fprintf fmt "Ada.Text_IO.Put_Line(\"'%a': '\" & (if %a then \"1\" else \"0\") & \"' \")"
|
94
|
pp_var_name var
|
95
|
pp_var_name var
|
96
|
| Types.Basic.Tint ->
|
97
|
fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Integer_IO.Put(%a);@,Ada.Text_IO.Put_Line(\"' \")"
|
98
|
pp_var_name var
|
99
|
pp_var_name var
|
100
|
| Types.Basic.Treal ->
|
101
|
fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Float_IO.Put(%a, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
|
102
|
pp_var_name var
|
103
|
pp_var_name var
|
104
|
| Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
|
105
|
in
|
106
|
|
107
|
(* Loop instructions *)
|
108
|
let pp_loop fmt =
|
109
|
fprintf fmt "while not Ada.Text_IO.End_Of_File loop@, @[<v>%a;@,%t;@,%a;@]@,end loop"
|
110
|
(Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
|
111
|
pp_step
|
112
|
(Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
|
113
|
|
114
|
(* Print the file *)
|
115
|
let instrs = [ pp_reset;
|
116
|
pp_loop] in
|
117
|
fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]"
|
118
|
pp_private_with (pp_str text_io)
|
119
|
pp_with_machine machine
|
120
|
(pp_main_procedure_definition machine) (locals, instrs)
|
121
|
|
122
|
(** Print the name of the ada project configuration file.
|
123
|
@param fmt the formater to print on
|
124
|
@param main_machine the machine associated to the main node
|
125
|
**)
|
126
|
let pp_project_configuration_name fmt basename =
|
127
|
fprintf fmt "%s.adc" basename
|
128
|
|
129
|
(** Print the project configuration file.
|
130
|
@param fmt the formater to print on
|
131
|
@param machine the main machine
|
132
|
**)
|
133
|
let pp_project_configuration_file fmt machine =
|
134
|
fprintf fmt "pragma SPARK_Mode (On);"
|
135
|
|
136
|
(** Print the name of the ada project file.
|
137
|
@param base_name name of the lustre file
|
138
|
@param fmt the formater to print on
|
139
|
@param machine_opt the main machine option
|
140
|
**)
|
141
|
let pp_project_name basename fmt machine_opt =
|
142
|
fprintf fmt "%s.gpr" basename
|
143
|
|
144
|
let pp_for_single name arg fmt =
|
145
|
fprintf fmt "for %s use \"%s\"" name arg
|
146
|
|
147
|
let pp_for name args fmt =
|
148
|
fprintf fmt "for %s use (@[%a@])" name
|
149
|
(Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
|
150
|
args
|
151
|
|
152
|
let pp_content fmt lines =
|
153
|
fprintf fmt " @[<v>%a%t@]"
|
154
|
(Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
|
155
|
(Utils.pp_final_char_if_non_empty ";" lines)
|
156
|
|
157
|
let pp_package name lines fmt =
|
158
|
fprintf fmt "package %s is@,%a@,end %s"
|
159
|
name
|
160
|
pp_content lines
|
161
|
name
|
162
|
|
163
|
(** Print the gpr project file, if there is a machine in machine_opt then
|
164
|
an executable project is made else it is a library.
|
165
|
@param fmt the formater to print on
|
166
|
@param machine_opt the main machine option
|
167
|
**)
|
168
|
let pp_project_file machines basename fmt machine_opt =
|
169
|
let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
|
170
|
@(match machine_opt with
|
171
|
| None -> []
|
172
|
| Some m -> [asprintf "%a" pp_main_filename m]) in
|
173
|
let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
|
174
|
fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
|
175
|
pp_content
|
176
|
((match machine_opt with
|
177
|
| None -> [
|
178
|
pp_for_single "Library_Name" basename;
|
179
|
pp_for_single "Library_Dir" "lib";
|
180
|
]
|
181
|
| Some machine -> [
|
182
|
pp_for "Main" [asprintf "%t" pp_main_procedure_name];
|
183
|
pp_for_single "Exec_Dir" "bin";
|
184
|
])
|
185
|
@[
|
186
|
pp_for_single "Object_Dir" "obj";
|
187
|
pp_for "Source_Files" adbs;
|
188
|
pp_package "Builder" [
|
189
|
pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
|
190
|
];
|
191
|
pp_package "Prove" [
|
192
|
pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
|
193
|
]
|
194
|
])
|
195
|
project_name
|
196
|
|
197
|
|
198
|
end
|