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