Project

General

Profile

Download (7.33 KB) Statistics
| Branch: | Tag: | Revision:
1 f20d8ac7 Christophe Garion
(********************************************************************)
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 fd834769 Guillaume DAVY
open Format
13
open Machine_code_types
14 379715f7 Guillaume DAVY
open Lustre_types
15 230b168e Guillaume DAVY
open Misc_printer
16
open Misc_lustre_function
17
open Ada_printer
18
open Ada_backend_common
19
20 ca7ff3f7 Lélio Brun
module Main = struct
21 230b168e Guillaume DAVY
  let build_text_io_package_local typ =
22 ca7ff3f7 Lélio Brun
    AdaLocalPackage
23
      ( (fun fmt -> fprintf fmt "%s_IO" typ),
24
        (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
25
        [ ((fun fmt -> fprintf fmt "Num"), fun fmt -> fprintf fmt "%s" typ) ] )
26
27
  (** Print the main file calling in a loop the step function of the main
28
      machine. @param fmt the formater to print on @param machine the main
29
      machine **)
30 ca7e8027 Lélio Brun
  let pp_main_adb fmt machine =
31 826063db Guillaume DAVY
    let statefull = is_machine_statefull machine in
32 ca7ff3f7 Lélio Brun
33 230b168e Guillaume DAVY
    let pp_package = pp_package_name_with_polymorphic [] machine in
34 ca7ff3f7 Lélio Brun
35 8d22ea35 Guillaume DAVY
    (* Dependances *)
36
    let text_io = "Ada.Text_IO" in
37 ca7ff3f7 Lélio Brun
38 8d22ea35 Guillaume DAVY
    (* Locals *)
39 230b168e Guillaume DAVY
    let locals =
40 ca7ff3f7 Lélio Brun
      [
41
        [
42
          build_text_io_package_local "Integer";
43
          build_text_io_package_local "Float";
44
        ];
45
      ]
46
      @ (if statefull then
47
         [
48
           [
49
             AdaLocalVar
50
               (build_pp_state_decl_from_subinstance AdaNoMode None
51
                  (asprintf "%t" pp_state_name, ([], machine)));
52
           ];
53
         ]
54
        else [])
55
      @ (if machine.mstep.step_inputs != [] then
56
         [ List.map (build_pp_var_decl_local None) machine.mstep.step_inputs ]
57
        else [])
58
      @
59
      if machine.mstep.step_outputs != [] then
60
        [ List.map (build_pp_var_decl_local None) machine.mstep.step_outputs ]
61
      else []
62 826063db Guillaume DAVY
    in
63 8d22ea35 Guillaume DAVY
64
    (* Stream instructions *)
65 ca7ff3f7 Lélio Brun
    let get_basic var =
66
      match (Types.repr var.var_type).Types.tdesc with
67
      | Types.Tbasic x ->
68
        x
69
      | _ ->
70
        assert false
71
    in
72 8d22ea35 Guillaume DAVY
    let pp_read fmt var =
73 379715f7 Guillaume DAVY
      match get_basic var with
74 ca7ff3f7 Lélio Brun
      | Types.Basic.Tbool ->
75
        fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
76
          (pp_var_name var)
77
      | _ ->
78
        fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)
79
          pp_var_type var
80 379715f7 Guillaume DAVY
    in
81 8d22ea35 Guillaume DAVY
    let pp_write fmt var =
82 379715f7 Guillaume DAVY
      match get_basic var with
83 ca7ff3f7 Lélio Brun
      | Types.Basic.Tbool ->
84
        fprintf fmt
85
          "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \
86
           \"' \")"
87
          (pp_var_name var) (pp_var_name var)
88
      | Types.Basic.Tint ->
89
        fprintf fmt
90
          "Ada.Text_IO.Put(\"'%t': '\");@,\
91
           Integer_IO.Put(%t);@,\
92
           Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
93
      | Types.Basic.Treal ->
94
        fprintf fmt
95
          "Ada.Text_IO.Put(\"'%t': '\");@,\
96
           Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\
97
           Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
98
      | Types.Basic.Tstring | Types.Basic.Trat ->
99
        assert false
100
      (* Could not be the top level inputs *)
101 379715f7 Guillaume DAVY
    in
102 8d22ea35 Guillaume DAVY
103
    (* Loop instructions *)
104
    let pp_loop fmt =
105 ca7ff3f7 Lélio Brun
      let args =
106
        pp_state_name
107
        ::
108
        List.map pp_var_name
109
          (machine.mstep.step_inputs @ machine.mstep.step_outputs)
110
      in
111
      fprintf fmt
112
        "while not Ada.Text_IO.End_Of_File loop@,\
113
        \  @[<v>%a;@,\
114
         %a;@,\
115
         %a;@]@,\
116
         end loop"
117
        (Utils.fprintf_list ~sep:";@," pp_read)
118
        machine.mstep.step_inputs pp_call
119
        (pp_package_access (pp_package, pp_step_procedure_name), [ args ])
120
        (Utils.fprintf_list ~sep:";@," pp_write)
121
        machine.mstep.step_outputs
122
    in
123
124 8d22ea35 Guillaume DAVY
    (* Print the file *)
125 ca7ff3f7 Lélio Brun
    let instrs =
126
      (if statefull then
127
       [
128
         (fun fmt ->
129
           pp_call fmt
130
             ( pp_package_access (pp_package, pp_reset_procedure_name),
131
               [ [ pp_state_name ] ] ));
132
       ]
133
      else [])
134
      @ [ pp_loop ]
135
    in
136
    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
137 230b168e Guillaume DAVY
      (pp_with AdaPrivate) (pp_package_name machine)
138 ca7ff3f7 Lélio Brun
      (pp_procedure pp_main_procedure_name [] None)
139
      (AdaProcedureContent (locals, instrs))
140
141
  (** Print the name of the ada project configuration file. @param fmt the
142
      formater to print on @param main_machine the machine associated to the
143
      main node **)
144
  let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename
145
146
  (** Print the project configuration file. @param fmt the formater to print on
147
      **)
148
  let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);"
149
150
  (** Print the name of the ada project file. @param base_name name of the
151
      lustre file @param fmt the formater to print on **)
152
  let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename
153
154
  let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg
155 61e0c3c4 Guillaume DAVY
156
  let pp_for name args fmt =
157
    fprintf fmt "for %s use (@[%a@])" name
158
      (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
159
      args
160
161
  let pp_content fmt lines =
162
    fprintf fmt "  @[<v>%a%t@]"
163 ca7ff3f7 Lélio Brun
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp))
164
      lines
165 61e0c3c4 Guillaume DAVY
      (Utils.pp_final_char_if_non_empty ";" lines)
166
167
  let pp_package name lines fmt =
168 ca7ff3f7 Lélio Brun
    fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name
169
170
  (** Print the gpr project file, if there is a machine in machine_opt then an
171
      executable project is made else it is a library. @param fmt the formater
172
      to print on @param machine_opt the main machine option **)
173 61e0c3c4 Guillaume DAVY
  let pp_project_file machines basename fmt machine_opt =
174 ca7ff3f7 Lélio Brun
    let adbs =
175
      List.map (asprintf "%a" (pp_machine_filename "adb")) machines
176
      @
177
      match machine_opt with
178
      | None ->
179
        []
180
      | Some m ->
181
        [ asprintf "%a" pp_main_filename m ]
182
    in
183
    let project_name =
184
      basename ^ if machine_opt = None then "_lib" else "_exe"
185
    in
186
    fprintf fmt "%sproject %s is@,%a@,end %s;"
187
      (if machine_opt = None then "library " else "")
188
      project_name pp_content
189
      ((match machine_opt with
190
       | None ->
191
         [
192
           pp_for_single "Library_Name" basename;
193
           pp_for_single "Library_Dir" "lib";
194
         ]
195
       | Some _ ->
196
         [
197
           pp_for "Main" [ asprintf "%t" pp_main_procedure_name ];
198
           pp_for_single "Exec_Dir" "bin";
199
         ])
200
      @ [
201
          pp_for_single "Object_Dir" "obj";
202
          pp_for "Source_Files" adbs;
203
          pp_package "Builder"
204
            [
205
              pp_for_single "Global_Configuration_Pragmas"
206
                (asprintf "%a" pp_project_configuration_name basename);
207
            ];
208
          pp_package "Prove"
209
            [
210
              pp_for "Switches"
211
                [
212
                  "--mode=prove";
213
                  "--report=statistics";
214
                  "--proof=per_check";
215
                  "--warnings=continue";
216
                ];
217
              pp_for_single "Proof_Dir" (asprintf "proof");
218
            ];
219 61e0c3c4 Guillaume DAVY
        ])
220 ca7ff3f7 Lélio Brun
      project_name
221
end