Project

General

Profile

Download (7 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 Lustrec.Machine_code_types
15
open Lustrec.Lustre_types
16

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

    
22
module Main =
23
struct
24

    
25
  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
  **)
35
  let pp_main_adb typed_submachines fmt machine =
36
    let statefull = is_machine_statefull machine in
37
    
38
    let pp_package = pp_package_name_with_polymorphic [] machine in
39
    
40
    (* Dependances *)
41
    let text_io = "Ada.Text_IO" in
42
    
43
    (* Locals *)
44
    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 [])
49
    in
50

    
51
    (* Stream instructions *)
52
    let get_basic var = match (Lustrec.Types.repr var.var_type ).Lustrec.Types.tdesc with
53
        Lustrec.Types.Tbasic x -> x | _ -> assert false in
54
    let pp_read fmt var =
55
      match get_basic var with
56
        | Lustrec.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
63
    in
64
    let pp_write fmt var =
65
      match get_basic var with
66
        | Lustrec.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
        | Lustrec.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
        | Lustrec.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
        | Lustrec.Types.Basic.Tstring | Lustrec.Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
79
    in
80

    
81
    (* Loop instructions *)
82
    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
        (Lustrec.Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
86
        pp_call (pp_package_access (pp_package, pp_step_procedure_name), [args])
87
        (Lustrec.Utils.fprintf_list ~sep:";@," pp_write) machine.mstep.step_outputs in
88
    
89
    (* 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)
93
      (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
     @param machine the main machine
106
  **)
107
  let pp_project_configuration_file fmt machine =
108
    fprintf fmt "pragma SPARK_Mode (On);"
109

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

    
118
  let pp_for_single name arg fmt =
119
    fprintf fmt "for %s use \"%s\"" name arg
120

    
121
  let pp_for name args fmt =
122
    fprintf fmt "for %s use (@[%a@])" name
123
      (Lustrec.Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
124
      args
125

    
126
  let pp_content fmt lines =
127
    fprintf fmt "  @[<v>%a%t@]"
128
      (Lustrec.Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
129
      (Lustrec.Utils.pp_final_char_if_non_empty ";" lines)
130

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

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

    
172

    
173
  end
(8-8/12)