Project

General

Profile

« Previous | Next » 

Revision 230b168e

Added by Guillaume DAVY almost 3 years ago

Ada: Refactor Ada Backend to reduce redundancy, make it more modular and
more simple.

View differences:

src/backends/Ada/ada_backend.ml
12 12
open Format
13 13
open Machine_code_types
14 14

  
15
open Misc_lustre_function
16
open Ada_printer
15 17
open Ada_backend_common
16 18

  
17 19
let indent_size = 2
......
66 68
      ident, (get_substitution m ident submachine, submachine))
67 69
    instances submachines
68 70

  
71
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
        None, [] (*(opt_machine_spec, guarantees)*)
116
      end
117
    | _ -> None, []
118

  
69 119
(** Main function of the Ada backend. It calls all the subfunction creating all
70 120
the file and fill them with Ada code representing the machines list given.
71 121
   @param basename name of the lustre file
......
78 128
  let module Adb = Ada_backend_adb.Main in
79 129
  let module Wrapper = Ada_backend_wrapper.Main in
80 130

  
131
  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

  
81 139
  let typed_submachines =
82
    List.map (get_typed_submachines machines) machines in
140
    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
83 145

  
84
  let _machines = List.combine typed_submachines machines in
146
  let _machines = List.combine typed_submachines _machines in
85 147

  
86
  let _pp_filename ext fmt (typed_submachine, machine) =
148
  let _pp_filename ext fmt (_, (_, machine)) =
87 149
    pp_machine_filename ext fmt machine in
88 150

  
89 151
  (* Extract the main machine if there is one *)
90 152
  let main_machine = (match !Options.main_node with
91 153
  | "" -> None
92 154
  | main_node -> (
93
    match Machine_code_common.get_machine_opt machines main_node with
155
    match Machine_code_common.get_machine_opt filtered_machines main_node with
94 156
    | None -> begin
95 157
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
96 158
      raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))
......
114 176
  (match main_machine with
115 177
    | None -> ()
116 178
    | Some machine ->
117
        write_file destname pp_main_filename (Wrapper.pp_main_adb (get_typed_submachines machines machine)) machine;
118
        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file machines basename) main_machine);
179
        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);
119 181
  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
120
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file machines basename) None;
182
  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file filtered_machines basename) None;
121 183

  
122 184

  
123 185
(* Local Variables: *)

Also available in: Unified diff