Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_wrapper.ml @ 826063db

History | View | Annotate | Download (7.67 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 Ada_backend_common
16
open Lustre_types
17

    
18
module Main =
19
struct
20

    
21
  (** Print the main procedure
22
     @param fmt the formater to print on
23
     @param machine the main machine
24
     @param locals list of local variable printers
25
     @param instrs list of instructions printer
26
  **)
27
  let pp_main_procedure_definition machine fmt (locals, instrs) =
28
      pp_procedure_definition
29
        pp_main_procedure_name
30
        (pp_simple_prototype pp_main_procedure_name)
31
        (fun fmt local -> fprintf fmt "%t" local)
32
        (fun fmt instr -> fprintf fmt "%t" instr)
33
        fmt
34
        (locals, instrs)
35

    
36
  (** Print call to machine procedure on state.
37
     @param instance name of the variable
38
     @param fmt the formater to print on
39
     @param instance node
40
  **)
41
  let pp_node_reset_call name fmt node =
42
    let pp_package fmt = pp_package_name fmt node in
43
    let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
44
    let pp_name fmt = pp_clean_ada_identifier fmt name in
45
    pp_var_decl fmt (NoMode, pp_name, pp_type)
46

    
47
  (** Print the main file calling in a loop the step function of the main machine.
48
     @param fmt the formater to print on
49
     @param machine the main machine
50
  **)
51
  let pp_main_adb typed_submachines fmt machine =
52
    let statefull = is_machine_statefull machine in
53
    let pp_str str fmt = fprintf fmt "%s" str in
54
    
55
    (* Dependances *)
56
    let text_io = "Ada.Text_IO" in
57
    let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
58
    let integer_io = "package Integer_IO is new Ada.Text_IO.Integer_IO(Integer)" in
59
    
60
    (* Locals *)
61
    let stateVar = asprintf "%t" pp_state_name in
62
    let pp_local_state_var_decl fmt = pp_node_state_decl [] stateVar fmt machine in
63
    let apply_pp_var_decl var fmt = pp_machine_var_decl NoMode fmt var in
64
    let step_parameters = machine.mstep.step_inputs@machine.mstep.step_outputs in
65
    let locals = List.map apply_pp_var_decl step_parameters in
66
    let locals = [pp_str integer_io;pp_str float_io]@(if statefull then [pp_local_state_var_decl] else [])@locals in
67

    
68
    (* Node instructions *)
69
    let pp_reset fmt =
70
      pp_package_call
71
        pp_reset_procedure_name
72
        fmt
73
        ([], machine, pp_state_name, None)
74
    in
75
    let pp_args fmt =
76
      fprintf fmt "@[%a@]"
77
        (Utils.fprintf_list ~sep:",@ " pp_var_name) step_parameters
78
    in
79
    let pp_step fmt =
80
          pp_package_call
81
            pp_step_procedure_name
82
            fmt
83
            ([], machine, pp_state_name, Some pp_args)
84
    in
85

    
86
    (* Stream instructions *)
87
    let get_basic var = match (Types.repr var.var_type ).Types.tdesc with
88
        Types.Tbasic x -> x | _ -> assert false in
89
    let pp_read fmt var =
90
      match get_basic var with
91
        | Types.Basic.Tbool ->
92
            fprintf fmt "%a := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
93
              pp_var_name var
94
        | _ ->
95
            fprintf fmt "%a := %a'Value(Ada.Text_IO.Get_Line)"
96
              pp_var_name var
97
              pp_var_type var
98
    in
99
    let pp_write fmt var =
100
      match get_basic var with
101
        | Types.Basic.Tbool ->
102
            fprintf fmt "Ada.Text_IO.Put_Line(\"'%a': '\" & (if %a then \"1\" else \"0\") & \"' \")"
103
              pp_var_name var
104
              pp_var_name var
105
        | Types.Basic.Tint ->
106
            fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Integer_IO.Put(%a);@,Ada.Text_IO.Put_Line(\"' \")"
107
              pp_var_name var
108
              pp_var_name var
109
        | Types.Basic.Treal ->
110
            fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Float_IO.Put(%a, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
111
              pp_var_name var
112
              pp_var_name var
113
        | Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
114
    in
115

    
116
    (* Loop instructions *)
117
    let pp_loop fmt =
118
      fprintf fmt "while not Ada.Text_IO.End_Of_File loop@,  @[<v>%a;@,%t;@,%a;@]@,end loop"
119
        (Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
120
        pp_step
121
        (Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
122
    
123
    (* Print the file *)
124
    let instrs = (if statefull then [pp_reset] else [])@[pp_loop] in
125
    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]"
126
      pp_private_with (pp_str text_io)
127
      pp_with_machine machine
128
      (pp_main_procedure_definition machine) (locals, instrs)
129

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

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

    
144
  (** Print the name of the ada project file.
145
     @param base_name name of the lustre file
146
     @param fmt the formater to print on
147
     @param machine_opt the main machine option
148
  **)
149
  let pp_project_name basename fmt machine_opt =
150
    fprintf fmt "%s.gpr" basename
151

    
152
  let pp_for_single name arg fmt =
153
    fprintf fmt "for %s use \"%s\"" name arg
154

    
155
  let pp_for name args fmt =
156
    fprintf fmt "for %s use (@[%a@])" name
157
      (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
158
      args
159

    
160
  let pp_content fmt lines =
161
    fprintf fmt "  @[<v>%a%t@]"
162
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
163
      (Utils.pp_final_char_if_non_empty ";" lines)
164

    
165
  let pp_package name lines fmt =
166
    fprintf fmt "package %s is@,%a@,end %s"
167
      name
168
      pp_content lines
169
      name
170

    
171
  (** Print the gpr project file, if there is a machine in machine_opt then
172
        an executable project is made else it is a library.
173
     @param fmt the formater to print on
174
     @param machine_opt the main machine option
175
  **)
176
  let pp_project_file machines basename fmt machine_opt =
177
    let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
178
                  @(match machine_opt with
179
                    | None -> []
180
                    | Some m -> [asprintf "%a" pp_main_filename m]) in
181
    let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
182
    fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
183
    pp_content
184
    ((match machine_opt with
185
      | None -> [
186
          pp_for_single "Library_Name" basename;
187
          pp_for_single "Library_Dir" "lib";
188
        ]
189
      | Some machine -> [
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
        pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
198
      ];
199
      pp_package "Prove" [
200
        pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
201
      ]
202
    ])
203
    project_name
204

    
205

    
206
  end