Project

General

Profile

Download (6.93 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 Utils
13
open Format
14
open Machine_code_types
15
open Lustre_types
16
open Misc_printer
17
open Misc_lustre_function
18
open Ada_printer
19
open Ada_backend_common
20

    
21
let build_text_io_package_local typ =
22
  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
let pp_main_adb fmt machine =
31
  let statefull = is_machine_statefull machine in
32

    
33
  let pp_package = pp_package_name_with_polymorphic [] machine in
34

    
35
  (* Dependances *)
36
  let text_io = "Ada.Text_IO" in
37

    
38
  (* Locals *)
39
  let locals =
40
    [
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
  in
63

    
64
  (* Stream instructions *)
65
  let get_type var = Types.repr var.var_type in
66
  let pp_read fmt var =
67
    if Types.is_bool_type (get_type var) then
68
      fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
69
        (pp_var_name var)
70
    else
71
      fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)" (pp_var_name var)
72
        pp_var_type var
73
  in
74
  let pp_write fmt var =
75
    let t = get_type var in
76
    if Types.is_bool_type t then
77
      fprintf fmt
78
        "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \
79
         \"' \")"
80
        (pp_var_name var) (pp_var_name var)
81
    else if Types.is_int_type t then
82
      fprintf fmt
83
        "Ada.Text_IO.Put(\"'%t': '\");@,\
84
         Integer_IO.Put(%t);@,\
85
         Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
86
    else if Types.is_real_type t then
87
      fprintf fmt
88
        "Ada.Text_IO.Put(\"'%t': '\");@,\
89
         Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,\
90
         Ada.Text_IO.Put_Line(\"' \")" (pp_var_name var) (pp_var_name var)
91
    else
92
      assert false
93
      (* Could not be the top level inputs *)
94
  in
95

    
96
  (* Loop instructions *)
97
  let pp_loop fmt =
98
    let args =
99
      pp_state_name
100
      ::
101
      List.map pp_var_name
102
        (machine.mstep.step_inputs @ machine.mstep.step_outputs)
103
    in
104
    fprintf fmt
105
      "while not Ada.Text_IO.End_Of_File loop@,\
106
      \  @[<v>%a;@,\
107
       %a;@,\
108
       %a;@]@,\
109
       end loop"
110
      (pp_print_list ~pp_sep:pp_print_semicolon pp_read)
111
      machine.mstep.step_inputs pp_call
112
      (pp_package_access (pp_package, pp_step_procedure_name), [ args ])
113
      (pp_print_list ~pp_sep:pp_print_semicolon pp_write)
114
      machine.mstep.step_outputs
115
  in
116

    
117
  (* Print the file *)
118
  let instrs =
119
    (if statefull then
120
       [
121
         (fun fmt ->
122
            pp_call fmt
123
              ( pp_package_access (pp_package, pp_reset_procedure_name),
124
                [ [ pp_state_name ] ] ));
125
       ]
126
     else [])
127
    @ [ pp_loop ]
128
  in
129
  fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
130
    (pp_with AdaPrivate) (pp_package_name machine)
131
    (pp_procedure pp_main_procedure_name [] None)
132
    (AdaProcedureContent (locals, instrs))
133

    
134
(** Print the name of the ada project configuration file. @param fmt the
135
    formater to print on @param main_machine the machine associated to the
136
    main node **)
137
let pp_project_configuration_name fmt basename = fprintf fmt "%s.adc" basename
138

    
139
(** Print the project configuration file. @param fmt the formater to print on
140
    **)
141
let pp_project_configuration_file fmt = fprintf fmt "pragma SPARK_Mode (On);"
142

    
143
(** Print the name of the ada project file. @param base_name name of the
144
    lustre file @param fmt the formater to print on **)
145
let pp_project_name basename fmt = fprintf fmt "%s.gpr" basename
146

    
147
let pp_for_single name arg fmt = fprintf fmt "for %s use \"%s\"" name arg
148

    
149
let pp_for name args fmt =
150
  fprintf fmt "for %s use (@[%a@])" name
151
    (pp_comma_list (fun fmt arg -> fprintf fmt "\"%s\"" arg))
152
    args
153

    
154
let pp_content fmt lines =
155
  fprintf fmt "  @[<v>%a%a@]"
156
    (pp_print_list ~pp_sep:pp_print_semicolon (fun fmt pp -> fprintf fmt "%t" pp))
157
    lines
158
    (if lines = [] then pp_print_nothing else pp_print_semicolon) ()
159

    
160
let pp_package name lines fmt =
161
  fprintf fmt "package %s is@,%a@,end %s" name pp_content lines name
162

    
163
(** Print the gpr project file, if there is a machine in machine_opt then an
164
    executable project is made else it is a library. @param fmt the formater
165
    to print on @param machine_opt the main machine option **)
166
let pp_project_file machines basename fmt machine_opt =
167
  let adbs =
168
    List.map (asprintf "%a" (pp_machine_filename "adb")) machines
169
    @
170
    match machine_opt with
171
    | None ->
172
      []
173
    | Some m ->
174
      [ asprintf "%a" pp_main_filename m ]
175
  in
176
  let project_name =
177
    basename ^ if machine_opt = None then "_lib" else "_exe"
178
  in
179
  fprintf fmt "%sproject %s is@,%a@,end %s;"
180
    (if machine_opt = None then "library " else "")
181
    project_name pp_content
182
    ((match machine_opt with
183
        | None ->
184
          [
185
            pp_for_single "Library_Name" basename;
186
            pp_for_single "Library_Dir" "lib";
187
          ]
188
        | Some _ ->
189
          [
190
            pp_for "Main" [ asprintf "%t" pp_main_procedure_name ];
191
            pp_for_single "Exec_Dir" "bin";
192
          ])
193
     @ [
194
       pp_for_single "Object_Dir" "obj";
195
       pp_for "Source_Files" adbs;
196
       pp_package "Builder"
197
         [
198
           pp_for_single "Global_Configuration_Pragmas"
199
             (asprintf "%a" pp_project_configuration_name basename);
200
         ];
201
       pp_package "Prove"
202
         [
203
           pp_for "Switches"
204
             [
205
               "--mode=prove";
206
               "--report=statistics";
207
               "--proof=per_check";
208
               "--warnings=continue";
209
             ];
210
           pp_for_single "Proof_Dir" (asprintf "proof");
211
         ];
212
     ])
213
    project_name
(10-10/17)