Project

General

Profile

« Previous | Next » 

Revision a7062da6

Added by LĂ©lio Brun over 3 years ago

another step towards refactoring

View differences:

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

  
12
open Utils
12 13
open Format
13 14
open Machine_code_types
14 15
open Lustre_types
......
17 18
open Ada_printer
18 19
open Ada_backend_common
19 20

  
20
module Main = struct
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) ] )
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 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
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 32

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

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

  
38
    (* Locals *)
39
    let locals =
38
  (* Locals *)
39
  let locals =
40
    [
40 41
      [
41
        [
42
          build_text_io_package_local "Integer";
43
          build_text_io_package_local "Float";
44
        ];
45
      ]
46
      @ (if statefull then
42
        build_text_io_package_local "Integer";
43
        build_text_io_package_local "Float";
44
      ];
45
    ]
46
    @ (if statefull then
47 47
         [
48 48
           [
49 49
             AdaLocalVar
......
51 51
                  (asprintf "%t" pp_state_name, ([], machine)));
52 52
           ];
53 53
         ]
54
        else [])
55
      @ (if machine.mstep.step_inputs != [] then
54
       else [])
55
    @ (if machine.mstep.step_inputs != [] then
56 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_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
    let pp_read fmt var =
73
      match get_basic var with
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
80
    in
81
    let pp_write fmt var =
82
      match get_basic var with
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 *)
101
    in
102

  
103
    (* Loop instructions *)
104
    let pp_loop fmt =
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
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
111 82
      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
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)
122 103
    in
123

  
124
    (* Print the file *)
125
    let instrs =
126
      (if statefull then
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
127 120
       [
128 121
         (fun fmt ->
129
           pp_call fmt
130
             ( pp_package_access (pp_package, pp_reset_procedure_name),
131
               [ [ pp_state_name ] ] ));
122
            pp_call fmt
123
              ( pp_package_access (pp_package, pp_reset_procedure_name),
124
                [ [ pp_state_name ] ] ));
132 125
       ]
133
      else [])
134
      @ [ pp_loop ]
135
    in
136
    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]" (pp_with AdaPrivate) (pp_str text_io)
137
      (pp_with AdaPrivate) (pp_package_name machine)
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
155

  
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
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp))
164
      lines
165
      (Utils.pp_final_char_if_non_empty ";" lines)
166

  
167
  let pp_package name lines fmt =
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 **)
173
  let pp_project_file machines basename fmt machine_opt =
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 ->
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"
191 197
         [
192
           pp_for_single "Library_Name" basename;
193
           pp_for_single "Library_Dir" "lib";
194
         ]
195
       | Some _ ->
198
           pp_for_single "Global_Configuration_Pragmas"
199
             (asprintf "%a" pp_project_configuration_name basename);
200
         ];
201
       pp_package "Prove"
196 202
         [
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
        ])
220
      project_name
221
end
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

Also available in: Unified diff