Project

General

Profile

Download (6.85 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 (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 extract_identifier (subst, _, submachine) =
139
    submachine.mname.node_id^"####"^(String.concat "####" (List.map (function (_, typ) -> (asprintf "%a" pp_type typ)) subst))
140
  in
141
  let identifiers = List.map extract_identifier typed_submachines in
142
  let typed_submachines_identified = List.combine identifiers typed_submachines in
143
  let typed_submachines_identified_set = List.fold_left (fun l x -> if List.mem_assoc (fst x) l then l else x::l) [] typed_submachines_identified in
144
  let submachines_set = List.map (function (_, (_, _, machine)) -> machine) typed_submachines_identified_set in
145
  let typed_submachines_set = snd (List.split typed_submachines_identified_set) in
146
  let pp_record fmt =
147
    pp_state_record_definition fmt (var_list, typed_submachines) in
148
  let typed_submachines_filtered =
149
    List.filter (function (l, _, _) -> l != []) typed_submachines_set in
150
  let polymorphic_types = find_all_polymorphic_type m in
151
  fprintf fmt "@[<v>%a%t%a%a@,  @[<v>@,%a;@,@,%t;@,@,%a;@,@,private@,@,%a%t%a;@,@]@,%a;@.@]"
152
    
153
    (* Include all the subinstance*)
154
    (Utils.fprintf_list ~sep:";@," pp_with_machine) submachines_set
155
    (Utils.pp_final_char_if_non_empty ";@,@," submachines_set)
156
    
157
    pp_generic polymorphic_types
158
    
159
    (*Begin the package*)
160
    (pp_begin_package false) m
161
    
162
    (*Declare the state type*)
163
    pp_private_limited_type_decl pp_state_type
164
    
165
    (*Declare the reset procedure*)
166
    (pp_reset_prototype m)
167
    
168
    (*Declare the step procedure*)
169
    pp_step_prototype_contract m
170
    
171
    (*Instantiate the polymorphic type that need to be instantiate*)
172
    (Utils.fprintf_list ~sep:";@," pp_new_package) typed_submachines_filtered
173
    (Utils.pp_final_char_if_non_empty ";@,@," typed_submachines_filtered)
174
    
175
    (*Define the state type*)
176
    pp_type_decl (pp_state_type, pp_record)
177
    
178
    (*End the package*)
179
    pp_end_package m
180

    
181
end
(4-4/6)