Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_ads.ml @ dda9eb32

History | View | Annotate | Download (6.18 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 (substitution, ident, 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_submachines list of pairs of instantiated types and machine
39
**)
40
let pp_state_record_definition fmt (var_list, typed_submachines) =
41
  fprintf fmt "@,  @[<v>record@,  @[<v>%a%t%a%t@]@,end record@]"
42
    (Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)
43
    typed_submachines
44
    (Utils.pp_final_char_if_non_empty ";@," typed_submachines)
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 ident the name of the instance, useless in this function
75
   @param submachine the submachine to instanciate
76
**)
77
let pp_new_package fmt (substitutions, ident, submachine) =
78
  fprintf fmt "package %a is new %a @[<v>(%a)@]"
79
    (pp_package_name_with_polymorphic substitutions) submachine
80
    pp_package_name submachine
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 contract -> 
110
        fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
111
          pp_prototype
112
          (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
113
          (Utils.pp_final_char_if_non_empty ",@," contract.assume)
114
          (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
115

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

    
125
(** Print the package declaration(ads) of a machine.
126
   @param fmt the formater to print on
127
   @param m the machine
128
**)
129
let pp_file machines fmt m =
130
  let submachines = List.map (get_machine machines) m.minstances in
131
  let names = List.map fst m.minstances in
132
  let var_list = m.mmemory in
133
  let typed_submachines = List.map2
134
    (fun instance submachine ->
135
      let ident = (fst instance) in
136
      get_substitution m ident submachine, ident, submachine)
137
    m.minstances submachines in
138
  let pp_record fmt =
139
    pp_state_record_definition fmt (var_list, typed_submachines) in
140
  let typed_submachines_filtered =
141
    List.filter (function (l, _, _) -> l != []) typed_submachines in
142
  let polymorphic_types = find_all_polymorphic_type m in
143
  fprintf fmt "@[<v>%a%t%a%a@,  @[<v>@,%a;@,@,%t;@,@,%a;@,@,private@,@,%a%t%a;@,@]@,%a;@.@]"
144
    
145
    (* Include all the subinstance*)
146
    (Utils.fprintf_list ~sep:";@," pp_with_machine) submachines
147
    (Utils.pp_final_char_if_non_empty ";@,@," submachines)
148
    
149
    pp_generic polymorphic_types
150
    
151
    (*Begin the package*)
152
    (pp_begin_package false) m
153
    
154
    (*Declare the state type*)
155
    pp_private_limited_type_decl pp_state_type
156
    
157
    (*Declare the reset procedure*)
158
    (pp_reset_prototype m)
159
    
160
    (*Declare the step procedure*)
161
    pp_step_prototype_contract m
162
    
163
    (*Instantiate the polymorphic type that need to be instantiate*)
164
    (Utils.fprintf_list ~sep:";@," pp_new_package) typed_submachines_filtered
165
    (Utils.pp_final_char_if_non_empty ";@,@," typed_submachines_filtered)
166
    
167
    (*Define the state type*)
168
    pp_type_decl (pp_state_type, pp_record)
169
    
170
    (*End the package*)
171
    pp_end_package m
172

    
173
end