Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/Ada/ada_backend_wrapper.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13

  
14 13
open Machine_code_types
15 14
open Lustre_types
16

  
17 15
open Misc_printer
18 16
open Misc_lustre_function
19 17
open Ada_printer
20 18
open Ada_backend_common
21 19

  
22
module Main =
23
struct
24

  
20
module Main = struct
25 21
  let build_text_io_package_local typ =
26
    AdaLocalPackage (
27
      (fun fmt -> fprintf fmt "%s_IO" typ),
28
      (fun fmt -> fprintf fmt "Ada.Text_IO.%s_IO" typ),
29
      [((fun fmt -> fprintf fmt "Num"), (fun fmt -> fprintf fmt "%s" typ))])
30

  
31
  (** Print the main file calling in a loop the step function of the main machine.
32
     @param fmt the formater to print on
33
     @param machine the main machine
34
  **)
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 **)
35 30
  let pp_main_adb fmt machine =
36 31
    let statefull = is_machine_statefull machine in
37
    
32

  
38 33
    let pp_package = pp_package_name_with_polymorphic [] machine in
39
    
34

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

  
43 38
    (* Locals *)
44 39
    let locals =
45
      [[build_text_io_package_local "Integer";build_text_io_package_local "Float"]]
46
      @(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance AdaNoMode None (asprintf "%t" pp_state_name, ([], machine)))]] else [])
47
      @(if machine.mstep.step_inputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_inputs] else [])
48
      @(if machine.mstep.step_outputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_outputs] else [])
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 []
49 62
    in
50 63

  
51 64
    (* Stream instructions *)
52
    let get_basic var = match (Types.repr var.var_type ).Types.tdesc with
53
        Types.Tbasic x -> x | _ -> assert false in
65
    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
54 72
    let pp_read fmt var =
55 73
      match get_basic var with
56
        | Types.Basic.Tbool ->
57
            fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
58
              (pp_var_name var)
59
        | _ ->
60
            fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)"
61
              (pp_var_name var)
62
              pp_var_type var
74
      | 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
63 80
    in
64 81
    let pp_write fmt var =
65 82
      match get_basic var with
66
        | Types.Basic.Tbool ->
67
            fprintf fmt "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \"' \")"
68
              (pp_var_name var)
69
              (pp_var_name var)
70
        | Types.Basic.Tint ->
71
            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Integer_IO.Put(%t);@,Ada.Text_IO.Put_Line(\"' \")"
72
              (pp_var_name var)
73
              (pp_var_name var)
74
        | Types.Basic.Treal ->
75
            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
76
              (pp_var_name var)
77
              (pp_var_name var)
78
        | Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
83
      | 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 *)
79 101
    in
80 102

  
81 103
    (* Loop instructions *)
82 104
    let pp_loop fmt =
83
      let args = pp_state_name::(List.map pp_var_name (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
84
      fprintf fmt "while not Ada.Text_IO.End_Of_File loop@,  @[<v>%a;@,%a;@,%a;@]@,end loop"
85
        (Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
86
        pp_call (pp_package_access (pp_package, pp_step_procedure_name), [args])
87
        (Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
88
    
105
      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

  
89 124
    (* Print the file *)
90
    let instrs = (if statefull then [fun fmt -> pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), [[pp_state_name]])] else [])@[pp_loop] in
91
    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]"
92
      (pp_with AdaPrivate) (pp_str text_io)
125
    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)
93 137
      (pp_with AdaPrivate) (pp_package_name machine)
94
      (pp_procedure pp_main_procedure_name [] None) (AdaProcedureContent (locals, instrs))
95

  
96
  (** Print the name of the ada project configuration file.
97
     @param fmt the formater to print on
98
     @param main_machine the machine associated to the main node
99
  **)
100
  let pp_project_configuration_name fmt basename =
101
    fprintf fmt "%s.adc" basename
102

  
103
  (** Print the project configuration file.
104
     @param fmt the formater to print on
105
  **)
106
  let pp_project_configuration_file fmt =
107
    fprintf fmt "pragma SPARK_Mode (On);"
108

  
109
  (** Print the name of the ada project file.
110
     @param base_name name of the lustre file
111
     @param fmt the formater to print on
112
  **)
113
  let pp_project_name basename fmt =
114
    fprintf fmt "%s.gpr" basename
115

  
116
  let pp_for_single name arg fmt =
117
    fprintf fmt "for %s use \"%s\"" name arg
138
      (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
118 155

  
119 156
  let pp_for name args fmt =
120 157
    fprintf fmt "for %s use (@[%a@])" name
......
123 160

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

  
129 167
  let pp_package name lines fmt =
130
    fprintf fmt "package %s is@,%a@,end %s"
131
      name
132
      pp_content lines
133
      name
134

  
135
  (** Print the gpr project file, if there is a machine in machine_opt then
136
        an executable project is made else it is a library.
137
     @param fmt the formater to print on
138
     @param machine_opt the main machine option
139
  **)
168
    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 **)
140 173
  let pp_project_file machines basename fmt machine_opt =
141
    let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
142
                  @(match machine_opt with
143
                    | None -> []
144
                    | Some m -> [asprintf "%a" pp_main_filename m]) in
145
    let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
146
    fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
147
    pp_content
148
    ((match machine_opt with
149
      | None -> [
150
          pp_for_single "Library_Name" basename;
151
          pp_for_single "Library_Dir" "lib";
152
        ]
153
      | Some _ -> [
154
          pp_for "Main" [asprintf "%t" pp_main_procedure_name];
155
          pp_for_single "Exec_Dir" "bin";
174
    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
            ];
156 219
        ])
157
    @[
158
      pp_for_single "Object_Dir" "obj";
159
      pp_for "Source_Files" adbs;
160
      pp_package "Builder" [
161
        pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
162
      ];
163
      pp_package "Prove" [
164
        pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
165
        pp_for_single "Proof_Dir" (asprintf "proof");
166
      ]
167
    ])
168
    project_name
169

  
170

  
171
  end
220
      project_name
221
end

Also available in: Unified diff