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 Lustre_types
|
16
|
open Corelang
|
17
|
open Machine_code_common
|
18
|
|
19
|
open Ada_backend_common
|
20
|
|
21
|
(** Functions printing the .ads file **)
|
22
|
module Main =
|
23
|
struct
|
24
|
|
25
|
(** Print the declaration of a state element of a subinstance of a machine.
|
26
|
@param machine the machine
|
27
|
@param fmt the formater to print on
|
28
|
@param substitution correspondance between polymorphic type id and their instantiation
|
29
|
@param ident the identifier of the subinstance
|
30
|
@param submachine the submachine of the subinstance
|
31
|
**)
|
32
|
let pp_machine_subinstance_state_decl fmt (ident, (substitution, submachine)) =
|
33
|
pp_node_state_decl substitution ident fmt submachine
|
34
|
|
35
|
(** Print the state record for a machine.
|
36
|
@param fmt the formater to print on
|
37
|
@param var_list list of all state var
|
38
|
@param typed_instances list typed instances
|
39
|
**)
|
40
|
let pp_state_record_definition fmt (var_list, typed_instances) =
|
41
|
fprintf fmt "@, @[<v>record@, @[<v>%a%t%t%a%t@]@,end record@]"
|
42
|
(Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)
|
43
|
typed_instances
|
44
|
(Utils.pp_final_char_if_non_empty ";" typed_instances)
|
45
|
(fun fmt -> if var_list!=[] && typed_instances!= [] then fprintf fmt "@,@," else fprintf fmt "")
|
46
|
(Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))
|
47
|
var_list
|
48
|
(Utils.pp_final_char_if_non_empty ";" var_list)
|
49
|
|
50
|
(** Print the declaration for polymorphic types.
|
51
|
@param fmt the formater to print on
|
52
|
@param polymorphic_types all the types to print
|
53
|
**)
|
54
|
let pp_generic fmt polymorphic_types =
|
55
|
let pp_polymorphic_types =
|
56
|
List.map (fun id fmt -> pp_polymorphic_type fmt id) polymorphic_types in
|
57
|
if polymorphic_types != [] then
|
58
|
fprintf fmt "generic@, @[<v>%a;@]@,"
|
59
|
(Utils.fprintf_list ~sep:";@," pp_private_type_decl)
|
60
|
pp_polymorphic_types
|
61
|
else
|
62
|
fprintf fmt ""
|
63
|
|
64
|
(** Print instanciation of a generic type in a new statement.
|
65
|
@param fmt the formater to print on
|
66
|
@param id id of the polymorphic type
|
67
|
@param typ the new type
|
68
|
**)
|
69
|
let pp_generic_instanciation fmt (id, typ) =
|
70
|
fprintf fmt "%a => %a" pp_polymorphic_type id pp_type typ
|
71
|
|
72
|
(** Print a new statement instantiating a generic package.
|
73
|
@param fmt the formater to print on
|
74
|
@param substitutions the instanciation substitution
|
75
|
@param machine the machine to instanciate
|
76
|
**)
|
77
|
let pp_new_package fmt (substitutions, machine) =
|
78
|
fprintf fmt "package %a is new %a @[<v>(%a)@]"
|
79
|
(pp_package_name_with_polymorphic substitutions) machine
|
80
|
pp_package_name machine
|
81
|
(Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions
|
82
|
|
83
|
let pp_eexpr fmt eexpr = fprintf fmt "true"
|
84
|
|
85
|
(** Print a precondition in aspect
|
86
|
@param fmt the formater to print on
|
87
|
@param expr the expession to print as pre
|
88
|
**)
|
89
|
let pp_pre fmt expr =
|
90
|
fprintf fmt "Pre => %a"
|
91
|
pp_eexpr expr
|
92
|
|
93
|
(** Print a postcondition in aspect
|
94
|
@param fmt the formater to print on
|
95
|
@param expr the expession to print as pre
|
96
|
**)
|
97
|
let pp_post fmt expr =
|
98
|
fprintf fmt "Post => %a"
|
99
|
pp_eexpr expr
|
100
|
|
101
|
(** Print the declaration of a procedure with a contract
|
102
|
@param pp_prototype the prototype printer
|
103
|
@param fmt the formater to print on
|
104
|
@param contract the contract for the function to declare
|
105
|
**)
|
106
|
let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
|
107
|
match opt_contract with
|
108
|
| None -> pp_prototype fmt
|
109
|
| Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
|
110
|
| Some (Contract contract) ->
|
111
|
fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
|
112
|
pp_prototype
|
113
|
(Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
|
114
|
(Utils.pp_final_char_if_non_empty ",@," contract.assume)
|
115
|
(Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
|
116
|
|
117
|
(** Print the prototype with a contract of the reset procedure from a machine.
|
118
|
@param fmt the formater to print on
|
119
|
@param machine the machine
|
120
|
**)
|
121
|
let pp_step_prototype_contract fmt m =
|
122
|
pp_procedure_prototype_contract
|
123
|
(pp_step_prototype m)
|
124
|
fmt
|
125
|
m.mspec
|
126
|
|
127
|
|
128
|
(** Remove duplicates from a list according to a given predicate.
|
129
|
@param eq the predicate defining equality
|
130
|
@param l the list to parse
|
131
|
**)
|
132
|
let remove_duplicates eq l =
|
133
|
let aux l x = if List.exists (eq x) l then l else x::l in
|
134
|
List.fold_left aux [] l
|
135
|
|
136
|
|
137
|
(** Compare two typed machines.
|
138
|
**)
|
139
|
let eq_typed_machine (subst1, machine1) (subst2, machine2) =
|
140
|
(String.equal machine1.mname.node_id machine2.mname.node_id) &&
|
141
|
(List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
|
142
|
|
143
|
|
144
|
(** Print the package declaration(ads) of a machine.
|
145
|
It requires the list of all typed instance.
|
146
|
A typed submachine is a (ident, typed_machine) with
|
147
|
- ident: the name
|
148
|
- typed_machine: a (substitution, machine) with
|
149
|
- machine: the submachine struct
|
150
|
- substitution the instanciation of all its polymorphic types.
|
151
|
@param fmt the formater to print on
|
152
|
@param typed_submachines list of all typed submachines of this machine
|
153
|
@param m the machine
|
154
|
**)
|
155
|
let pp_file fmt (typed_submachines, m) =
|
156
|
let typed_machines = snd (List.split typed_submachines) in
|
157
|
let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
|
158
|
|
159
|
let machines_to_import = snd (List.split typed_machines_set) in
|
160
|
|
161
|
let polymorphic_types = find_all_polymorphic_type m in
|
162
|
|
163
|
let typed_machines_to_instanciate =
|
164
|
List.filter (fun (l, _) -> l != []) typed_machines_set in
|
165
|
|
166
|
let typed_instances = List.filter is_submachine_statefull typed_submachines in
|
167
|
|
168
|
let pp_record fmt =
|
169
|
pp_state_record_definition fmt (m.mmemory, typed_instances) in
|
170
|
|
171
|
let pp_state_decl_and_reset fmt = fprintf fmt "%a;@,@,%t;@,@,"
|
172
|
(*Declare the state type*)
|
173
|
pp_private_limited_type_decl pp_state_type
|
174
|
(*Declare the reset procedure*)
|
175
|
(pp_reset_prototype m)
|
176
|
in
|
177
|
|
178
|
let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,"
|
179
|
(*Instantiate the polymorphic type that need to be instantiated*)
|
180
|
(Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
|
181
|
(Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
|
182
|
(*Define the state type*)
|
183
|
pp_type_decl (pp_state_type, pp_record)
|
184
|
in
|
185
|
|
186
|
let pp_ifstatefull fmt pp =
|
187
|
if is_machine_statefull m then
|
188
|
fprintf fmt "%t" pp
|
189
|
else
|
190
|
fprintf fmt ""
|
191
|
in
|
192
|
|
193
|
fprintf fmt "@[<v>%a%t%a%a@, @[<v>@,%a%a;@,%a@]@,%a;@.@]"
|
194
|
|
195
|
(* Include all the subinstance package*)
|
196
|
(Utils.fprintf_list ~sep:";@," pp_with_machine) machines_to_import
|
197
|
(Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
|
198
|
|
199
|
pp_generic polymorphic_types
|
200
|
|
201
|
(*Begin the package*)
|
202
|
(pp_begin_package false) m
|
203
|
|
204
|
pp_ifstatefull pp_state_decl_and_reset
|
205
|
|
206
|
(*Declare the step procedure*)
|
207
|
pp_step_prototype_contract m
|
208
|
|
209
|
(*Print the private section*)
|
210
|
pp_ifstatefull pp_private_section
|
211
|
|
212
|
(*End the package*)
|
213
|
pp_end_package m
|
214
|
|
215
|
end
|