Project

General

Profile

Download (7.42 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 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 fmt machine =
52
    let pp_str str fmt = fprintf fmt "%s" str in
53
    (* Dependances *)
54
    let text_io = "Ada.Text_IO" in
55
    let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
56
    let integer_io = "package Integer_IO is new Ada.Text_IO.Integer_IO(Integer)" in
57
    
58
    (* Locals *)
59
    let stateVar = "state" in
60
    let step_parameters = machine.mstep.step_inputs@machine.mstep.step_outputs in
61
    let pp_local_state_var_decl fmt = pp_node_state_decl [] stateVar fmt machine in
62
    let apply_pp_var_decl var fmt = pp_machine_var_decl NoMode fmt var in
63
    let locals = List.map apply_pp_var_decl step_parameters in
64
    let locals = (pp_str integer_io)::(pp_str float_io)::pp_local_state_var_decl::locals in
65

    
66
    (* Node instructions *)
67
    let pp_reset fmt =
68
      fprintf fmt "%a.reset(%s)"
69
        pp_package_name machine
70
        stateVar in
71
    let pp_step fmt =
72
      fprintf fmt "%a.step(@[%s,@ %a@])"
73
        pp_package_name machine
74
        stateVar
75
        (Utils.fprintf_list ~sep:",@ " pp_var_name) step_parameters in
76

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

    
107
    (* Loop instructions *)
108
    let pp_loop fmt =
109
      fprintf fmt "while not Ada.Text_IO.End_Of_File loop@,  @[<v>%a;@,%t;@,%a;@]@,end loop"
110
        (Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
111
        pp_step
112
        (Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
113
    
114
    (* Print the file *)
115
    let instrs = [ pp_reset;
116
                   pp_loop] in
117
    fprintf fmt "@[<v>%a;@,%a;@,@,%a;@]"
118
      pp_private_with (pp_str text_io)
119
      pp_with_machine machine
120
      (pp_main_procedure_definition machine) (locals, instrs)
121

    
122
  (** Print the name of the ada project configuration file.
123
     @param fmt the formater to print on
124
     @param main_machine the machine associated to the main node
125
  **)
126
  let pp_project_configuration_name fmt basename =
127
    fprintf fmt "%s.adc" basename
128

    
129
  (** Print the project configuration file.
130
     @param fmt the formater to print on
131
     @param machine the main machine
132
  **)
133
  let pp_project_configuration_file fmt machine =
134
    fprintf fmt "pragma SPARK_Mode (On);"
135

    
136
  (** Print the name of the ada project file.
137
     @param base_name name of the lustre file
138
     @param fmt the formater to print on
139
     @param machine_opt the main machine option
140
  **)
141
  let pp_project_name basename fmt machine_opt =
142
    fprintf fmt "%s.gpr" basename
143

    
144
  let pp_for_single name arg fmt =
145
    fprintf fmt "for %s use \"%s\"" name arg
146

    
147
  let pp_for name args fmt =
148
    fprintf fmt "for %s use (@[%a@])" name
149
      (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
150
      args
151

    
152
  let pp_content fmt lines =
153
    fprintf fmt "  @[<v>%a%t@]"
154
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
155
      (Utils.pp_final_char_if_non_empty ";" lines)
156

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

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

    
197

    
198
  end
(6-6/6)