Project

General

Profile

Download (7.74 KB) Statistics
| Branch: | Tag: | Revision:
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
(4-4/6)