Project

General

Profile

Download (6.66 KB) Statistics
| Branch: | Tag: | Revision:
1 f20d8ac7 Christophe Garion
(********************************************************************)
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 48a6309c Guillaume DAVY
open Machine_code_types
14
15 230b168e Guillaume DAVY
open Misc_lustre_function
16
open Ada_printer
17 fd834769 Guillaume DAVY
open Ada_backend_common
18
19
let indent_size = 2
20
21
(** Log at level 2 a string message with some indentation.
22
   @param indent the indentation level
23
   @param info the message
24
**)
25
let log_str_level_two indent info =
26
  let str_indent = String.make (indent*indent_size) ' ' in
27
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
28 e6492c59 Guillaume DAVY
  Log.report ~level:2 pp_message;
29
  Format.pp_print_flush Format.err_formatter ()
30 fd834769 Guillaume DAVY
31
(** Write a new file with formatter
32
   @param destname folder where the file shoudl be created
33
   @param pp_filename function printing the filename
34
   @param pp_file function wich pretty print the file
35
   @param arg will be given to pp_filename and pp_file
36
**)
37
let write_file destname pp_filename pp_file arg =
38
  let path = asprintf "%s%a" destname pp_filename arg in
39 48a6309c Guillaume DAVY
  let out = open_out path in
40
  let fmt = formatter_of_out_channel out in
41 e6492c59 Guillaume DAVY
  log_str_level_two 2 ("generating "^path);
42 fd834769 Guillaume DAVY
  pp_file fmt arg;
43
  pp_print_flush fmt ();
44 e6492c59 Guillaume DAVY
  close_out out
45 fd834769 Guillaume DAVY
46 f20d8ac7 Christophe Garion
47 fd834769 Guillaume DAVY
(** Exception raised when a machine contains a feature not supported by the
48
  Ada backend*)
49 c419ca44 Guillaume DAVY
exception CheckFailed of string
50
51 fd834769 Guillaume DAVY
52
(** Check that a machine match the requirement for an Ada compilation :
53
      - No constants.
54
   @param machine the machine to test
55
**)
56 c419ca44 Guillaume DAVY
let check machine =
57
  match machine.mconst with
58
    | [] -> ()
59
    | _ -> raise (CheckFailed "machine.mconst should be void")
60
61 3de9f6e4 Guillaume DAVY
62 09d7b39f Guillaume DAVY
let get_typed_submachines machines m =
63
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
64
  let submachines = List.map (get_machine machines) instances in
65 3de9f6e4 Guillaume DAVY
  List.map2
66
    (fun instance submachine ->
67
      let ident = (fst instance) in
68
      ident, (get_substitution m ident submachine, submachine))
69 09d7b39f Guillaume DAVY
    instances submachines
70 3de9f6e4 Guillaume DAVY
71 230b168e Guillaume DAVY
let extract_contract machines m =
72
  let rec find_submachine_from_ident ident = function
73
    | [] -> raise Not_found
74
    | h::t when h.mname.node_id = ident -> h
75
    | _::t -> find_submachine_from_ident ident t
76
  in
77
  let extract_ident eexpr =
78
    match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
79
      | Expr_ident ident -> ident
80
      | _ -> assert false
81
      (*
82
      | Expr_const cst -> assert false
83
      | Expr_tuple exprs -> assert false
84
      | Expr_ite (expr1, expr2, expr3) -> assert false
85
      | Expr_arrow (expr1, expr2)  -> assert false
86
      | Expr_fby (expr1, expr2) -> assert false
87
      | Expr_array exprs -> assert false
88
      | Expr_access (expr1, dim) -> assert false
89
      | Expr_power (expr1, dim) -> assert false
90
      | Expr_pre expr -> assert false
91
      | Expr_when (expr,ident,label) -> assert false
92
      | Expr_merge (ident, l) -> assert false
93
      | Expr_appl call -> assert false
94
      *)
95
  in
96
  match m.mspec with
97
    | Some (NodeSpec ident) ->
98
      begin
99
        let machine_spec = find_submachine_from_ident ident machines in
100
        let guarantees =
101
          match machine_spec.mspec with
102
            | Some (Contract contract) ->
103
                assert (contract.consts=[]);
104
                assert (contract.locals=[]);
105
                assert (contract.stmts=[]);
106
                assert (contract.assume=[]);
107
                List.map extract_ident contract.guarantees
108
            | _ -> assert false
109
        in
110
        let opt_machine_spec =
111
          match machine_spec.mstep.step_instrs with
112
            | [] -> None
113
            | _ -> Some machine_spec
114
        in
115 173a2a8f Guillaume DAVY
        (opt_machine_spec, guarantees, 4)
116 230b168e Guillaume DAVY
      end
117 173a2a8f Guillaume DAVY
    | _ -> None, [], 0
118 230b168e Guillaume DAVY
119 fd834769 Guillaume DAVY
(** Main function of the Ada backend. It calls all the subfunction creating all
120
the file and fill them with Ada code representing the machines list given.
121 61e0c3c4 Guillaume DAVY
   @param basename name of the lustre file
122 fd834769 Guillaume DAVY
   @param prog useless
123
   @param prog list of machines to translate
124
   @param dependencies useless
125
**)
126 f20d8ac7 Christophe Garion
let translate_to_ada basename prog machines dependencies =
127
  let module Ads = Ada_backend_ads.Main in
128
  let module Adb = Ada_backend_adb.Main in
129
  let module Wrapper = Ada_backend_wrapper.Main in
130 48a6309c Guillaume DAVY
131 230b168e Guillaume DAVY
  let is_real_machine m =
132
    match m.mspec with
133
      | Some (Contract x) -> false
134
      | _ -> true
135
  in
136
137
  let filtered_machines = List.filter is_real_machine machines in
138
139 09d7b39f Guillaume DAVY
  let typed_submachines =
140 230b168e Guillaume DAVY
    List.map (get_typed_submachines machines) filtered_machines in
141
  
142
  let contracts = List.map (extract_contract machines) filtered_machines in
143
144
  let _machines = List.combine contracts filtered_machines in
145 3de9f6e4 Guillaume DAVY
146 230b168e Guillaume DAVY
  let _machines = List.combine typed_submachines _machines in
147 3de9f6e4 Guillaume DAVY
148 230b168e Guillaume DAVY
  let _pp_filename ext fmt (_, (_, machine)) =
149 3de9f6e4 Guillaume DAVY
    pp_machine_filename ext fmt machine in
150
151 fd834769 Guillaume DAVY
  (* Extract the main machine if there is one *)
152
  let main_machine = (match !Options.main_node with
153
  | "" -> None
154
  | main_node -> (
155 230b168e Guillaume DAVY
    match Machine_code_common.get_machine_opt filtered_machines main_node with
156 fd834769 Guillaume DAVY
    | None -> begin
157
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
158
      raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
159
    end
160
    | Some m -> Some m
161
  )) in
162 c419ca44 Guillaume DAVY
163 fd834769 Guillaume DAVY
  let destname = !Options.dest_dir ^ "/" in
164 c419ca44 Guillaume DAVY
165 fd834769 Guillaume DAVY
  log_str_level_two 1 "Checking machines";
166 c419ca44 Guillaume DAVY
  List.iter check machines;
167 48a6309c Guillaume DAVY
168 fd834769 Guillaume DAVY
  log_str_level_two 1 "Generating ads";
169 3de9f6e4 Guillaume DAVY
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
170 48a6309c Guillaume DAVY
171 fd834769 Guillaume DAVY
  log_str_level_two 1 "Generating adb";
172 3de9f6e4 Guillaume DAVY
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
173 48a6309c Guillaume DAVY
174 fd834769 Guillaume DAVY
  (* If a main node is given we generate a main adb file and a project file *)
175
  log_str_level_two 1 "Generating wrapper files";
176 61e0c3c4 Guillaume DAVY
  (match main_machine with
177
    | None -> ()
178 9e5f8085 Guillaume DAVY
    | Some machine ->
179 230b168e Guillaume DAVY
        write_file destname pp_main_filename (Wrapper.pp_main_adb (get_typed_submachines filtered_machines machine)) machine;
180
        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file filtered_machines basename) main_machine);
181 61e0c3c4 Guillaume DAVY
  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
182 230b168e Guillaume DAVY
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file filtered_machines basename) None;
183 48a6309c Guillaume DAVY
184 f20d8ac7 Christophe Garion
185
(* Local Variables: *)
186
(* compile-command:"make -C ../../.." *)
187
(* End: *)