Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_ads.ml @ 3de9f6e4

History | View | Annotate | Download (6.83 KB)

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%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
    (Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))
46
    var_list
47
    (Utils.pp_final_char_if_non_empty ";" var_list)
48

    
49
(** Print the declaration for polymorphic types.
50
   @param fmt the formater to print on
51
   @param polymorphic_types all the types to print
52
**)
53
let pp_generic fmt polymorphic_types =
54
  let pp_polymorphic_types =
55
    List.map (fun id fmt -> pp_polymorphic_type fmt id) polymorphic_types in
56
  if polymorphic_types != [] then
57
      fprintf fmt "generic@,  @[<v>%a;@]@,"
58
        (Utils.fprintf_list ~sep:";@," pp_private_limited_type_decl)
59
        pp_polymorphic_types
60
  else
61
    fprintf fmt ""
62

    
63
(** Print instanciation of a generic type in a new statement.
64
   @param fmt the formater to print on
65
   @param id id of the polymorphic type
66
   @param typ the new type
67
**)
68
let pp_generic_instanciation fmt (id, typ) =
69
  fprintf fmt "%a => %a" pp_polymorphic_type id pp_type typ
70

    
71
(** Print a new statement instantiating a generic package.
72
   @param fmt the formater to print on
73
   @param substitutions the instanciation substitution
74
   @param machine the machine to instanciate
75
**)
76
let pp_new_package fmt (substitutions, machine) =
77
  fprintf fmt "package %a is new %a @[<v>(%a)@]"
78
    (pp_package_name_with_polymorphic substitutions) machine
79
    pp_package_name machine
80
    (Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions
81

    
82
let pp_eexpr fmt eexpr = fprintf fmt "true"
83

    
84
(** Print a precondition in aspect
85
   @param fmt the formater to print on
86
   @param expr the expession to print as pre
87
**)
88
let pp_pre fmt expr =
89
  fprintf fmt "Pre => %a"
90
    pp_eexpr expr
91

    
92
(** Print a postcondition in aspect
93
   @param fmt the formater to print on
94
   @param expr the expession to print as pre
95
**)
96
let pp_post fmt expr =
97
  fprintf fmt "Post => %a"
98
    pp_eexpr expr
99

    
100
(** Print the declaration of a procedure with a contract
101
   @param pp_prototype the prototype printer
102
   @param fmt the formater to print on
103
   @param contract the contract for the function to declare
104
**)
105
let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
106
  match opt_contract with
107
    | None -> pp_prototype fmt
108
    | Some contract -> 
109
        fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
110
          pp_prototype
111
          (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
112
          (Utils.pp_final_char_if_non_empty ",@," contract.assume)
113
          (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
114

    
115
(** Print the prototype with a contract of the reset procedure from a machine.
116
   @param fmt the formater to print on
117
   @param machine the machine
118
**)
119
let pp_step_prototype_contract fmt m = pp_procedure_prototype_contract
120
      (pp_step_prototype m)
121
      fmt
122
      m.mspec
123

    
124
(** Remove duplicates from a list according to a given predicate.
125
   @param eq the predicate defining equality
126
   @param l the list to parse
127
**)
128
let remove_duplicates eq l =
129
  let aux l x = if List.exists (eq x) l then l else x::l in
130
  List.fold_left aux [] l
131

    
132

    
133
(** Compare two typed machines.
134
**)
135
let eq_typed_machine (subst1, machine1) (subst2, machine2) =
136
  (String.equal machine1.mname.node_id machine2.mname.node_id) &&
137
  (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
138

    
139

    
140
(** Print the package declaration(ads) of a machine.
141
  It requires the list of all typed instance.
142
  A typed submachine instance is (ident, type_machine) with ident
143
  the instance name and typed_machine is (substitution, machine) with machine
144
  the machine associated to the instance and substitution the instanciation of
145
  all its polymorphic types.
146
   @param fmt the formater to print on
147
   @param typed_instances list of all typed machine instances of this machine
148
   @param m the machine
149
**)
150
let pp_file fmt (typed_instances, m) =
151
  let typed_machines = snd (List.split typed_instances) in
152
  let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
153
  
154
  let machines_to_import = snd (List.split typed_machines_set) in
155

    
156
  let polymorphic_types = find_all_polymorphic_type m in
157
  
158
  let typed_machines_to_instanciate =
159
    List.filter (fun (l, _) -> l != []) typed_machines_set in
160
  
161
  let pp_record fmt =
162
    pp_state_record_definition fmt (m.mmemory, typed_instances) in
163
  
164
  
165
  fprintf fmt "@[<v>%a%t%a%a@,  @[<v>@,%a;@,@,%t;@,@,%a;@,@,private@,@,%a%t%a;@,@]@,%a;@.@]"
166
    
167
    (* Include all the subinstance*)
168
    (Utils.fprintf_list ~sep:";@," pp_with_machine) machines_to_import
169
    (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
170
    
171
    pp_generic polymorphic_types
172
    
173
    (*Begin the package*)
174
    (pp_begin_package false) m
175
    
176
    (*Declare the state type*)
177
    pp_private_limited_type_decl pp_state_type
178
    
179
    (*Declare the reset procedure*)
180
    (pp_reset_prototype m)
181
    
182
    (*Declare the step procedure*)
183
    pp_step_prototype_contract m
184
    
185
    (*Instantiate the polymorphic type that need to be instantiated*)
186
    (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
187
    (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
188
    
189
    (*Define the state type*)
190
    pp_type_decl (pp_state_type, pp_record)
191
    
192
    (*End the package*)
193
    pp_end_package m
194

    
195
end