Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/Ada/ada_backend.ml
11 11

  
12 12
open Format
13 13
open Machine_code_types
14

  
15 14
open Misc_lustre_function
16 15
open Ada_backend_common
17 16

  
18 17
let indent_size = 2
19 18

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

  
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
**)
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 **)
36 31
let write_file destname pp_filename pp_file arg =
37 32
  let path = asprintf "%s%a" destname pp_filename arg in
38 33
  let out = open_out path in
39 34
  let fmt = formatter_of_out_channel out in
40
  log_str_level_two 2 ("generating "^path);
35
  log_str_level_two 2 ("generating " ^ path);
41 36
  pp_file fmt arg;
42 37
  pp_print_flush fmt ();
43 38
  close_out out
44 39

  
45

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

  
50

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

  
48
  | [] ->
49
    ()
50
  | _ ->
51
    raise (CheckFailed "machine.mconst should be void")
60 52

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

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

  
118 112
(** 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
**)
113
    the file and fill them with Ada code representing the machines list given.
114
    @param basename name of the lustre file @param prog list of machines to
115
    translate **)
123 116
let translate_to_ada basename machines =
124 117
  let module Ads = Ada_backend_ads.Main in
125 118
  let module Adb = Ada_backend_adb.Main in
126 119
  let module Wrapper = Ada_backend_wrapper.Main in
127

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

  
134 124
  let filtered_machines = List.filter is_real_machine machines in
135 125

  
136 126
  let typed_submachines =
137
    List.map (get_typed_submachines machines) filtered_machines in
138
  
127
    List.map (get_typed_submachines machines) filtered_machines
128
  in
129

  
139 130
  let contracts = List.map (extract_contract machines) filtered_machines in
140 131

  
141 132
  let _machines = List.combine contracts filtered_machines in
......
143 134
  let _machines = List.combine typed_submachines _machines in
144 135

  
145 136
  let _pp_filename ext fmt (_, (_, machine)) =
146
    pp_machine_filename ext fmt machine in
137
    pp_machine_filename ext fmt machine
138
  in
147 139

  
148 140
  (* 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
141
  let main_machine =
142
    match !Options.main_node with
143
    | "" ->
144
      None
145
    | main_node -> (
146
      match Machine_code_common.get_machine_opt filtered_machines main_node with
147
      | None ->
148
        Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg
149
          Error.Main_not_found;
150
        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
151
      | Some m ->
152
        Some m)
153
  in
159 154

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

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

  
185
    None
193 186

  
194 187
(* Local Variables: *)
195 188
(* compile-command:"make -C ../../.." *)

Also available in: Unified diff