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_lustre_function
|
17
|
open Ada_printer
|
18
|
open Ada_backend_common
|
19
|
|
20
|
(** Functions printing the .ads file **)
|
21
|
|
22
|
let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
|
23
|
(*should be replaced by the init of list from ocaml std lib*)
|
24
|
|
25
|
let suffixOld = "_old"
|
26
|
|
27
|
let suffixNew = "_new"
|
28
|
|
29
|
let pp_invariant_name fmt = fprintf fmt "inv"
|
30
|
|
31
|
let pp_transition_name fmt = fprintf fmt "transition"
|
32
|
|
33
|
let pp_init_name fmt = fprintf fmt "init"
|
34
|
|
35
|
let pp_state_name_predicate suffix fmt =
|
36
|
fprintf fmt "%t%s" pp_state_name suffix
|
37
|
|
38
|
let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
|
39
|
|
40
|
(** Print the expression function representing the transition predicate.
|
41
|
@param fmt the formater to print on **)
|
42
|
let pp_init_predicate fmt () =
|
43
|
let new_state =
|
44
|
AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
|
45
|
in
|
46
|
pp_predicate pp_init_name [ [ new_state ] ] true fmt None
|
47
|
|
48
|
(** Print the expression function representing the transition predicate.
|
49
|
@param fmt the formater to print on @param machine the machine **)
|
50
|
let pp_transition_predicate fmt (_, m) =
|
51
|
let old_state =
|
52
|
AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None
|
53
|
in
|
54
|
let new_state =
|
55
|
AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None
|
56
|
in
|
57
|
let inputs = build_pp_var_decl_step_input AdaIn None m in
|
58
|
let outputs = build_pp_var_decl_step_output AdaIn None m in
|
59
|
pp_predicate pp_transition_name
|
60
|
([ [ old_state; new_state ] ] @ inputs @ outputs)
|
61
|
true fmt None
|
62
|
|
63
|
let pp_invariant_predicate fmt () =
|
64
|
pp_predicate pp_invariant_name
|
65
|
[ [ build_pp_state_decl AdaIn None ] ]
|
66
|
true fmt None
|
67
|
|
68
|
(** Print a new statement instantiating a generic package. @param fmt the
|
69
|
formater to print on @param substitutions the instanciation substitution
|
70
|
@param machine the machine to instanciate **)
|
71
|
let pp_new_package fmt (substitutions, machine) =
|
72
|
let pp_name = pp_package_name machine in
|
73
|
let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
|
74
|
let instanciations =
|
75
|
List.map
|
76
|
(fun (id, typ) -> pp_polymorphic_type id, fun fmt -> pp_type fmt typ)
|
77
|
substitutions
|
78
|
in
|
79
|
pp_package_instanciation pp_new_name pp_name fmt instanciations
|
80
|
|
81
|
(** Remove duplicates from a list according to a given predicate. @param eq
|
82
|
the predicate defining equality @param l the list to parse **)
|
83
|
let remove_duplicates eq l =
|
84
|
let aux l x = if List.exists (eq x) l then l else x :: l in
|
85
|
List.fold_left aux [] l
|
86
|
|
87
|
(** Compare two typed machines. **)
|
88
|
let eq_typed_machine (subst1, machine1) (subst2, machine2) =
|
89
|
String.equal machine1.mname.node_id machine2.mname.node_id
|
90
|
&& List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
|
91
|
|
92
|
(** Print the package declaration(ads) of a machine. It requires the list of
|
93
|
all typed instance. A typed submachine is a (ident, typed_machine) with -
|
94
|
ident: the name - typed_machine: a (substitution, machine) with - machine:
|
95
|
the submachine struct - substitution the instanciation of all its
|
96
|
polymorphic types. @param fmt the formater to print on @param
|
97
|
typed_submachines list of all typed submachines of this machine @param m
|
98
|
the machine **)
|
99
|
let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
|
100
|
let typed_machines = snd (List.split typed_submachines) in
|
101
|
let typed_machines_set =
|
102
|
remove_duplicates eq_typed_machine typed_machines
|
103
|
in
|
104
|
|
105
|
let machines_to_import =
|
106
|
List.map pp_package_name (snd (List.split typed_machines_set))
|
107
|
in
|
108
|
|
109
|
let polymorphic_types = find_all_polymorphic_type m in
|
110
|
|
111
|
let typed_machines_to_instanciate =
|
112
|
List.filter (fun (l, _) -> l != []) typed_machines_set
|
113
|
in
|
114
|
|
115
|
let typed_instances =
|
116
|
List.filter is_submachine_statefull typed_submachines
|
117
|
in
|
118
|
|
119
|
let memories =
|
120
|
match m_spec_opt with
|
121
|
| None ->
|
122
|
[]
|
123
|
| Some m ->
|
124
|
List.map
|
125
|
(fun x ->
|
126
|
pp_var_decl
|
127
|
(build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
|
128
|
m.mmemory
|
129
|
in
|
130
|
let ghost_private = memories in
|
131
|
(* Commented since not used. Could be reinjected in the code let vars_spec =
|
132
|
match m_spec_opt with | None -> [] | Some m_spec -> List.map
|
133
|
(build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
|
134
|
(m_spec.mmemory) in *)
|
135
|
let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
|
136
|
let states =
|
137
|
List.map
|
138
|
(build_pp_state_decl_from_subinstance AdaNoMode None)
|
139
|
typed_instances
|
140
|
in
|
141
|
let var_lists =
|
142
|
(if states = [] then [] else [ states ])
|
143
|
@ if vars = [] then [] else [ vars ]
|
144
|
in
|
145
|
|
146
|
let pp_ifstatefull fmt pp =
|
147
|
if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
|
148
|
in
|
149
|
|
150
|
let pp_state_decl_and_reset fmt =
|
151
|
let init fmt =
|
152
|
pp_call fmt
|
153
|
( pp_access pp_axiomatize_package_name pp_init_name,
|
154
|
[ [ pp_state_name ] ] )
|
155
|
in
|
156
|
let contract = Some (false, false, [], [ init ]) in
|
157
|
fprintf fmt "%t;@,@,%a;@,@,"
|
158
|
(*Declare the state type*)
|
159
|
(pp_type_decl pp_state_type AdaPrivate)
|
160
|
(*Declare the reset procedure*)
|
161
|
(pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
|
162
|
AdaNoContent
|
163
|
in
|
164
|
|
165
|
let pp_private_section fmt =
|
166
|
fprintf fmt "@,private@,@,%a%a%a"
|
167
|
(*Instantiate the polymorphic type that need to be instantiated*)
|
168
|
(pp_print_list
|
169
|
~pp_sep:pp_print_semicolon
|
170
|
~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
|
171
|
pp_new_package)
|
172
|
typed_machines_to_instanciate
|
173
|
(*Define the state type*)
|
174
|
pp_ifstatefull
|
175
|
(fun fmt -> pp_record pp_state_type fmt var_lists)
|
176
|
(pp_print_list
|
177
|
~pp_sep:pp_print_semicolon
|
178
|
~pp_prologue:(fun fmt () -> fprintf fmt ";@,@,")
|
179
|
(fun fmt pp -> pp fmt))
|
180
|
ghost_private
|
181
|
in
|
182
|
|
183
|
let pp_content fmt =
|
184
|
let pp_contract_opt =
|
185
|
let pp_var x fmt = pp_clean_ada_identifier fmt x in
|
186
|
let guarantee_post_conditions = List.map pp_var guarantees in
|
187
|
let state_pre_conditions, state_post_conditions =
|
188
|
if is_machine_statefull m then
|
189
|
let input = List.map pp_var_name m.mstep.step_inputs in
|
190
|
let output = List.map pp_var_name m.mstep.step_outputs in
|
191
|
let args =
|
192
|
[ [ pp_old pp_state_name; pp_state_name ] ]
|
193
|
@ (if input != [] then [ input ] else [])
|
194
|
@ if output != [] then [ output ] else []
|
195
|
in
|
196
|
let transition fmt =
|
197
|
pp_call fmt
|
198
|
(pp_access pp_axiomatize_package_name pp_transition_name, args)
|
199
|
in
|
200
|
let invariant fmt =
|
201
|
pp_call fmt
|
202
|
( pp_access pp_axiomatize_package_name pp_invariant_name,
|
203
|
[ [ pp_state_name ] ] )
|
204
|
in
|
205
|
[ invariant ], [ transition; invariant ]
|
206
|
else [], []
|
207
|
in
|
208
|
let post_conditions =
|
209
|
state_post_conditions @ guarantee_post_conditions
|
210
|
in
|
211
|
let pre_conditions = state_pre_conditions in
|
212
|
if post_conditions = [] && pre_conditions = [] then None
|
213
|
else Some (false, false, pre_conditions, post_conditions)
|
214
|
in
|
215
|
let pp_guarantee name =
|
216
|
pp_var_decl
|
217
|
( AdaNoMode,
|
218
|
(fun fmt -> pp_clean_ada_identifier fmt name),
|
219
|
pp_boolean_type,
|
220
|
Some (true, false, [], []) )
|
221
|
in
|
222
|
let ghost_public = List.map pp_guarantee guarantees in
|
223
|
fprintf fmt "@,%a%a%a%a@,@,%a;@,@,%t"
|
224
|
(pp_print_list
|
225
|
~pp_sep:pp_print_semicolon
|
226
|
~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
|
227
|
(fun fmt pp -> pp fmt))
|
228
|
ghost_public
|
229
|
pp_ifstatefull pp_state_decl_and_reset
|
230
|
(*Declare the step procedure*)
|
231
|
(pp_procedure pp_step_procedure_name (build_pp_arg_step m)
|
232
|
pp_contract_opt)
|
233
|
AdaNoContent pp_ifstatefull
|
234
|
(fun fmt -> fprintf fmt ";@,")
|
235
|
(pp_package pp_axiomatize_package_name [] false)
|
236
|
(fun fmt ->
|
237
|
fprintf fmt
|
238
|
"pragma Annotate (GNATProve, External_Axiomatization);@,\
|
239
|
@,\
|
240
|
%a;@,\
|
241
|
%a;@,\
|
242
|
%a"
|
243
|
(*Declare the init predicate*)
|
244
|
pp_init_predicate ()
|
245
|
(*Declare the transition predicate*)
|
246
|
pp_transition_predicate (m_spec_opt, m)
|
247
|
(*Declare the invariant predicate*)
|
248
|
pp_invariant_predicate ())
|
249
|
(*Print the private section*)
|
250
|
pp_private_section
|
251
|
in
|
252
|
|
253
|
let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
|
254
|
let pp_generics = List.map pp_poly_type polymorphic_types in
|
255
|
|
256
|
fprintf fmt "@[<v>%a%a;@]@."
|
257
|
(* Include all the subinstance package*)
|
258
|
(pp_print_list
|
259
|
~pp_sep:pp_print_semicolon
|
260
|
~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
|
261
|
(pp_with AdaNoVisibility))
|
262
|
machines_to_import
|
263
|
(*Begin the package*)
|
264
|
(pp_package (pp_package_name m) pp_generics false)
|
265
|
pp_content
|