Project

General

Profile

Download (6.72 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

    
15
open Misc_lustre_function
16
open Ada_backend_common
17

    
18
let indent_size = 2
19

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

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

    
45

    
46
(** Exception raised when a machine contains a feature not supported by the
47
  Ada backend*)
48
exception CheckFailed of string
49

    
50

    
51
(** Check that a machine match the requirement for an Ada compilation :
52
      - No constants.
53
   @param machine the machine to test
54
**)
55
let check machine =
56
  match machine.mconst with
57
    | [] -> ()
58
    | _ -> raise (CheckFailed "machine.mconst should be void")
59

    
60

    
61
let get_typed_submachines machines m =
62
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
63
  let submachines = List.map (get_machine machines) instances in
64
  List.map2
65
    (fun instance submachine ->
66
      let ident = (fst instance) in
67
      ident, (get_substitution m ident submachine, submachine))
68
    instances submachines
69

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

    
118
(** Main function of the Ada backend. It calls all the subfunction creating all
119
the file and fill them with Ada code representing the machines list given.
120
   @param basename name of the lustre file
121
   @param prog list of machines to translate
122
**)
123
let translate_to_ada basename machines =
124
  let module Ads = Ada_backend_ads.Main in
125
  let module Adb = Ada_backend_adb.Main in
126
  let module Wrapper = Ada_backend_wrapper.Main in
127

    
128
  let is_real_machine m =
129
    match m.mspec.mnode_spec with
130
      | Some (Contract _) -> false
131
      | _ -> true
132
  in
133

    
134
  let filtered_machines = List.filter is_real_machine machines in
135

    
136
  let typed_submachines =
137
    List.map (get_typed_submachines machines) filtered_machines in
138
  
139
  let contracts = List.map (extract_contract machines) filtered_machines in
140

    
141
  let _machines = List.combine contracts filtered_machines in
142

    
143
  let _machines = List.combine typed_submachines _machines in
144

    
145
  let _pp_filename ext fmt (_, (_, machine)) =
146
    pp_machine_filename ext fmt machine in
147

    
148
  (* Extract the main machine if there is one *)
149
  let main_machine = (match !Options.main_node with
150
  | "" -> None
151
  | main_node -> (
152
    match Machine_code_common.get_machine_opt filtered_machines main_node with
153
    | None -> begin
154
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
155
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
156
    end
157
    | Some m -> 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 (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
167

    
168
  log_str_level_two 1 "Generating adb";
169
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
170

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

    
193

    
194
(* Local Variables: *)
195
(* compile-command:"make -C ../../.." *)
196
(* End: *)
(2-2/11)