Project

General

Profile

Download (6.85 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
open Machine_code_types
14
open Misc_lustre_function
15
open Ada_backend_common
16

    
17
let indent_size = 2
18

    
19
(** Log at level 2 a string message with some indentation. @param indent the
20
    indentation level @param info the message **)
21
let log_str_level_two indent info =
22
  let str_indent = String.make (indent * indent_size) ' ' in
23
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
24
  Log.report ~level:2 pp_message;
25
  Format.pp_print_flush Format.err_formatter ()
26

    
27
(** Write a new file with formatter @param destname folder where the file shoudl
28
    be created @param pp_filename function printing the filename @param pp_file
29
    function wich pretty print the file @param arg will be given to pp_filename
30
    and pp_file **)
31
let write_file destname pp_filename pp_file arg =
32
  let path = asprintf "%s%a" destname pp_filename arg in
33
  let out = open_out path in
34
  let fmt = formatter_of_out_channel out in
35
  log_str_level_two 2 ("generating " ^ path);
36
  pp_file fmt arg;
37
  pp_print_flush fmt ();
38
  close_out out
39

    
40
exception CheckFailed of string
41
(** Exception raised when a machine contains a feature not supported by the Ada
42
    backend*)
43

    
44
(** Check that a machine match the requirement for an Ada compilation : - No
45
    constants. @param machine the machine to test **)
46
let check machine =
47
  match machine.mconst with
48
  | [] ->
49
    ()
50
  | _ ->
51
    raise (CheckFailed "machine.mconst should be void")
52

    
53
let get_typed_submachines machines m =
54
  let instances =
55
    List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls
56
  in
57
  let submachines = List.map (get_machine machines) instances in
58
  List.map2
59
    (fun instance submachine ->
60
      let ident = fst instance in
61
      ident, (get_substitution m ident submachine, submachine))
62
    instances
63
    submachines
64

    
65
let extract_contract machines m =
66
  let rec find_submachine_from_ident ident = function
67
    | [] ->
68
      raise Not_found
69
    | h :: _ when h.mname.node_id = ident ->
70
      h
71
    | _ :: t ->
72
      find_submachine_from_ident ident t
73
  in
74
  let extract_ident eexpr =
75
    match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
76
    | Expr_ident ident ->
77
      ident
78
    | _ ->
79
      assert false
80
    (* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false |
81
       Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1,
82
       expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false |
83
       Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert
84
       false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> assert
85
       false | Expr_when (expr,ident,label) -> assert false | Expr_merge (ident,
86
       l) -> assert false | Expr_appl call -> assert false *)
87
  in
88
  match m.mspec.mnode_spec with
89
  | Some (NodeSpec ident) ->
90
    let machine_spec = find_submachine_from_ident ident machines in
91
    let guarantees =
92
      match machine_spec.mspec.mnode_spec with
93
      | Some (Contract contract) ->
94
        (* assert (contract.consts = []);
95
         * assert (contract.locals = []);
96
         * assert (contract.stmts = []);
97
         * assert (contract.assume = []);
98
         * List.map extract_ident contract.guarantees *)
99
        (* TODO *)
100
        assert false
101
      | _ ->
102
        assert false
103
    in
104
    let opt_machine_spec =
105
      match machine_spec.mstep.step_instrs with
106
      | [] ->
107
        None
108
      | _ ->
109
        Some machine_spec
110
    in
111
    opt_machine_spec, guarantees
112
  | _ ->
113
    None, []
114

    
115
(** Main function of the Ada backend. It calls all the subfunction creating all
116
    the file and fill them with Ada code representing the machines list given.
117
    @param basename name of the lustre file @param prog list of machines to
118
    translate **)
119
let translate_to_ada basename machines =
120
  (* let module Ads = Ada_backend_ads.Main in
121
   * let module Adb = Ada_backend_adb.Main in
122
   * let module Wrapper = Ada_backend_wrapper.Main in *)
123
  let is_real_machine m =
124
    match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
125
  in
126

    
127
  let filtered_machines = List.filter is_real_machine machines in
128

    
129
  let typed_submachines =
130
    List.map (get_typed_submachines machines) filtered_machines
131
  in
132

    
133
  let contracts = List.map (extract_contract machines) filtered_machines in
134

    
135
  let _machines = List.combine contracts filtered_machines in
136

    
137
  let _machines = List.combine typed_submachines _machines in
138

    
139
  let _pp_filename ext fmt (_, (_, machine)) =
140
    pp_machine_filename ext fmt machine
141
  in
142

    
143
  (* Extract the main machine if there is one *)
144
  let main_machine =
145
    match !Options.main_node with
146
    | "" ->
147
      None
148
    | main_node -> (
149
      match Machine_code_common.get_machine_opt filtered_machines main_node with
150
      | None ->
151
        Format.eprintf
152
          "Ada Code generation error: %a@."
153
          Error.pp
154
          Error.Main_not_found;
155
        raise (Error.Error (Location.dummy, Error.Main_not_found))
156
      | Some m ->
157
        Some m)
158
  in
159

    
160
  let destname = !Options.dest_dir ^ "/" in
161

    
162
  log_str_level_two 1 "Checking machines";
163
  List.iter check machines;
164

    
165
  log_str_level_two 1 "Generating ads";
166
  List.iter
167
    (write_file destname (_pp_filename "ads") Ada_backend_ads.pp_file)
168
    _machines;
169

    
170
  log_str_level_two 1 "Generating adb";
171
  List.iter
172
    (write_file destname (_pp_filename "adb") Ada_backend_adb.pp_file)
173
    _machines;
174

    
175
  (* If a main node is given we generate a main adb file and a project file *)
176
  log_str_level_two 1 "Generating wrapper files";
177
  (match main_machine with
178
  | None ->
179
    ()
180
  | Some machine ->
181
    write_file
182
      destname
183
      pp_main_filename
184
      Ada_backend_wrapper.pp_main_adb
185
      (*get_typed_submachines filtered_machines machine*)
186
      machine;
187
    write_file
188
      destname
189
      (fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_exe") fmt)
190
      (Ada_backend_wrapper.pp_project_file filtered_machines basename)
191
      main_machine);
192
  write_file
193
    destname
194
    Ada_backend_wrapper.pp_project_configuration_name
195
    (fun fmt _ -> Ada_backend_wrapper.pp_project_configuration_file fmt)
196
    basename;
197
  write_file
198
    destname
199
    (fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_lib") fmt)
200
    (Ada_backend_wrapper.pp_project_file filtered_machines basename)
201
    None
202

    
203
(* Local Variables: *)
204
(* compile-command:"make -C ../../.." *)
205
(* End: *)
(2-2/17)