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/README
1
This is the Ada Backend generating Ada code from the machine code computed
2
from a Lustre file.
3

  
4
The backend is split in several files described in this README.
5

  
6
=> misc_lustre_function.ml
7
Some fonction on pure Lustre machine code, no printers
8
or anything related to Ada. It just compute information from the Machine Code.
9
It contains mostly the unification code used for polymorphic type. It is
10
important since the Arrow node is polymorphic.
11

  
12
=> misc_printer.ml
13
Some general format printer function, not related at all
14
to Ada but used by this backend.
15

  
16
=> ada_printer.mli
17
=> ada_printer.ml
18
It contains Type representing some part of Ada syntaxe and printers function
19
to generates it. There is nothing specifics to Lustre in this file. It is
20
mostly printers for the declarative part of Ada. The printer functions takes in
21
general directly printer function build by other files(like ada_backend_common.ml)
22
to print instruction and expression contained in the declaration.
23
For example, the printer for the declaration of a variable will take
24
two printer functions as argument:
25
 - pp_type: printing the type
26
 - pp_name: printing the variable name
27
The printer will looks like :
28
--
29
let pp_var_decl pp_type pp_name =
30
  fprintf fmt "%t : %t" pp_type pp_name
31
--
32

  
33
=> ada_backend_common.mli
34
=> ada_backend_common.ml
35
It contains function printing Ada code(instruction and exression) from Machine
36
Code. This functions are used or could be used for ads and/or adb and/or
37
wrappers.
38

  
39
=> ada_backend_ads.ml
40
It contains function printing Ada code(instruction and exression) from Machine
41
Code for the Ads file.
42

  
43
=> ada_backend_adb.ml
44
It contains function printing Ada code(instruction and exression) from Machine
45
Code for the Adb file.
46

  
47
=> ada_backend_wrapper.ml
48
It contains function printing Ada code(instruction and exression) from Machine
49
Code for :
50
  - an adb file witha main function containg a loop calling step.
51
  - a project file
52
  - a configuration file
53

  
54
=> ada_backend.ml
55
It contains the main function of the backend which perform the unification
56
and write all the files using the previsous code.
57

  
58

  
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: *)
src/backends/Ada/ada_backend_adb.ml
15 15
open Lustre_types
16 16
open Corelang
17 17
open Machine_code_common
18

  
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
18 22
open Ada_backend_common
19 23

  
20 24
(** Main module for generating packages bodies
......
42 46
      @param fmt the formater to print on
43 47
      @param instr the instruction to print
44 48
   **)
45
  let rec pp_machine_instr typed_submachines machine fmt instr =
49
  let rec pp_machine_instr typed_submachines machine instr fmt =
46 50
    let pp_instr = pp_machine_instr typed_submachines machine in
47 51
    (* Print args for a step call *)
48 52
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
49
    let pp_args vl il fmt =
50
      fprintf fmt "@[%a@]%t@[%a@]"
51
        (Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl
52
        (Utils.pp_final_char_if_non_empty ",@," il)
53
        (Utils.fprintf_list ~sep:",@ " pp_var_name) il
54
    in
55 53
    (* Print a when branch of a case *)
56
    let pp_when fmt (cond, instrs) =
57
      fprintf fmt "when %s =>@,%a" cond (pp_block pp_instr) instrs
54
    let pp_when (cond, instrs) fmt =
55
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
58 56
    in
59 57
    (* Print a case *)
60 58
    let pp_case fmt (g, hl) =
61 59
      fprintf fmt "case %a is@,%aend case"
62 60
        (pp_value machine) g
63
        (pp_block pp_when) hl
61
        pp_block (List.map pp_when hl)
64 62
    in
65 63
    (* Print a if *)
66 64
    (* If neg is true the we must test for the negation of the condition. It
......
80 78
          let pp_else = match instrs2 with
81 79
            | None -> fun fmt -> fprintf fmt ""
82 80
            | Some i2 -> fun fmt ->
83
                fprintf fmt "else@,%a" (pp_block pp_instr) i2
81
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
84 82
          in
85 83
          fprintf fmt "if %a then@,%a%tend if"
86 84
            pp_cond g
87
            (pp_block pp_instr) instrs1
85
            pp_block (List.map pp_instr instrs1)
88 86
            pp_else
89 87
    in
90 88
    match get_instr_desc instr with
......
93 91
      (* reset  *)
94 92
      | MReset i when List.mem_assoc i typed_submachines ->
95 93
          let (substitution, submachine) = get_instance i typed_submachines in
96
          pp_package_call
97
            pp_reset_procedure_name
98
            fmt
99
            (substitution, submachine, pp_state i, None)
94
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
95
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
96
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
100 97
      | MLocalAssign (ident, value) ->
101 98
          pp_basic_assign machine fmt ident value
102 99
      | MStateAssign (ident, value) ->
......
106 103
          pp_basic_assign machine fmt i0 value
107 104
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
108 105
          let (substitution, submachine) = get_instance i typed_submachines in
109
          pp_package_call
110
            pp_step_procedure_name
111
            fmt
112
            (substitution, submachine, pp_state i, Some (pp_args vl il))
106
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
107
          let input = List.map (fun x fmt -> pp_value machine fmt x) vl in
108
          let output = List.map (fun x fmt -> pp_var_name fmt x) il in
109
          let args =
110
            (if is_machine_statefull submachine then [[pp_state i]] else [])
111
              @(if input!=[] then [input] else [])
112
              @(if output!=[] then [output] else [])
113
          in
114
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
113 115
      | MBranch (_, []) -> assert false
114 116
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
115 117
          let neg = c1=tag_false in
......
131 133
     @param fmt the formater to print on
132 134
     @param machine the machine
133 135
  **)
134
  let pp_step_definition typed_submachines fmt m =
135
    pp_procedure_definition
136
      pp_step_procedure_name
137
      (pp_step_prototype m)
138
      (pp_machine_var_decl NoMode)
139
      (pp_machine_instr typed_submachines m)
140
      fmt
141
      (m.mstep.step_locals, m.mstep.step_instrs)
136
  let pp_step_definition typed_submachines fmt (m, m_spec_opt) =
137
    let spec_instrs = match m_spec_opt with
138
      | None -> []
139
      | Some m -> m.mstep.step_instrs
140
    in
141
    let spec_locals = match m_spec_opt with
142
      | None -> []
143
      | Some m -> m.mstep.step_locals
144
    in
145
    let pp_local_list = List.map build_pp_var_decl_local (m.mstep.step_locals@spec_locals) in
146
    let pp_instr_list = List.map (pp_machine_instr typed_submachines m) (m.mstep.step_instrs@spec_instrs) in
147
    let content = AdaProcedureContent ((if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
148
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
142 149

  
143 150
  (** Print the definition of the reset procedure from a machine.
144 151

  
......
151 158
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
152 159
    in
153 160
    let assigns = List.map build_assign m.mmemory in
154
    pp_procedure_definition
155
      pp_reset_procedure_name
156
      (pp_reset_prototype m)
157
      (pp_machine_var_decl NoMode)
158
      (pp_machine_instr typed_submachines m)
159
      fmt
160
      ([], assigns@m.minit)
161
    let pp_instr_list = List.map (pp_machine_instr typed_submachines m) (assigns@m.minit) in
162
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
161 163

  
162 164
  (** Print the package definition(ads) of a machine.
163 165
    It requires the list of all typed instance.
......
169 171
     @param typed_submachines list of all typed machine instances of this machine
170 172
     @param m the machine
171 173
  **)
172
  let pp_file fmt (typed_submachines, machine) =
174
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
173 175
    let pp_reset fmt =
174 176
      if is_machine_statefull machine then
175 177
        fprintf fmt "%a;@,@," (pp_reset_definition typed_submachines) machine
......
185 187
          pkg::pkgs
186 188
      with Not_found -> pkgs
187 189
    in
188
    let packages = List.fold_left aux [] machine.mcalls in
189
    fprintf fmt "%a%t%a@,  @[<v>@,%t%a;@,@]@,%a;@."
190
    let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
191
    let pp_content fmt =
192
      fprintf fmt "%t%a"
193
        (*Define the reset procedure*)
194
        pp_reset
195
        
196
        (*Define the step procedure*)
197
        (pp_step_definition typed_submachines) (machine, opt_spec_machine)
198
    in
199
    fprintf fmt "%a%t%a;@."
190 200
      
191 201
      (* Include all the required packages*)
192
      (Utils.fprintf_list ~sep:";@," pp_with) packages
202
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) packages
193 203
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
194 204
      
195
      (*Begin the package*)
196
      (pp_begin_package true) machine
197
      
198
      (*Define the reset procedure*)
199
      pp_reset
200
      
201
      (*Define the step procedure*)
202
      (pp_step_definition typed_submachines) machine
203
      
204
      (*End the package*)
205
      pp_end_package machine
205
      (*Print package*)
206
      (pp_package (pp_package_name machine) [] true ) pp_content
206 207

  
207 208
end
208 209

  
src/backends/Ada/ada_backend_ads.ml
16 16
open Corelang
17 17
open Machine_code_common
18 18

  
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
19 22
open Ada_backend_common
20 23

  
21 24
(** Functions printing the .ads file **)
22 25
module Main =
23 26
struct
24 27

  
25
  (** Print the declaration of a state element of a subinstance of a machine.
26
     @param machine the machine
27
     @param fmt the formater to print on
28
     @param substitution correspondance between polymorphic type id and their instantiation
29
     @param ident the identifier of the subinstance
30
     @param submachine the submachine of the subinstance
31
  **)
32
  let pp_machine_subinstance_state_decl fmt (ident, (substitution, submachine)) =
33
    pp_node_state_decl substitution ident fmt submachine
34

  
35
  (** Print the state record for a machine.
36
     @param fmt the formater to print on
37
     @param var_list list of all state var
38
     @param typed_instances list typed instances
39
  **)
40
  let pp_state_record_definition fmt (var_list, typed_instances) =
41
    fprintf fmt "@,  @[<v>record@,  @[<v>%a%t%t%a%t@]@,end record@]"
42
      (Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)
43
      typed_instances
44
      (Utils.pp_final_char_if_non_empty ";" typed_instances)
45
      (fun fmt -> if var_list!=[] && typed_instances!= [] then fprintf fmt "@,@," else fprintf fmt "")
46
      (Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))
47
      var_list
48
      (Utils.pp_final_char_if_non_empty ";" var_list)
49

  
50
  (** Print the declaration for polymorphic types.
51
     @param fmt the formater to print on
52
     @param polymorphic_types all the types to print
53
  **)
54
  let pp_generic fmt polymorphic_types =
55
    let pp_polymorphic_types =
56
      List.map (fun id fmt -> pp_polymorphic_type fmt id) polymorphic_types in
57
    if polymorphic_types != [] then
58
        fprintf fmt "generic@,  @[<v>%a;@]@,"
59
          (Utils.fprintf_list ~sep:";@," pp_private_type_decl)
60
          pp_polymorphic_types
61
    else
62
      fprintf fmt ""
63

  
64
  (** Print instanciation of a generic type in a new statement.
65
     @param fmt the formater to print on
66
     @param id id of the polymorphic type
67
     @param typ the new type
68
  **)
69
  let pp_generic_instanciation fmt (id, typ) =
70
    fprintf fmt "%a => %a" pp_polymorphic_type id pp_type typ
71

  
72 28
  (** Print a new statement instantiating a generic package.
73 29
     @param fmt the formater to print on
74 30
     @param substitutions the instanciation substitution
75 31
     @param machine the machine to instanciate
76 32
  **)
77 33
  let pp_new_package fmt (substitutions, machine) =
78
    fprintf fmt "package %a is new %a @[<v>(%a)@]"
79
      (pp_package_name_with_polymorphic substitutions) machine
80
      pp_package_name machine
81
      (Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions
82

  
83
  let pp_eexpr fmt eexpr = fprintf fmt "true"
34
    let pp_name = pp_package_name machine in
35
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
36
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
37
    pp_package_instanciation pp_new_name pp_name fmt instanciations
84 38

  
85 39
  (** Print a precondition in aspect
86 40
     @param fmt the formater to print on
......
88 42
  **)
89 43
  let pp_pre fmt expr =
90 44
    fprintf fmt "Pre => %a"
91
      pp_eexpr expr
45
      pp_clean_ada_identifier expr
92 46

  
93 47
  (** Print a postcondition in aspect
94 48
     @param fmt the formater to print on
95 49
     @param expr the expession to print as pre
96 50
  **)
97
  let pp_post fmt expr =
51
  let pp_post fmt ident =
98 52
    fprintf fmt "Post => %a"
99
      pp_eexpr expr
53
      pp_clean_ada_identifier ident
100 54

  
101 55
  (** Print the declaration of a procedure with a contract
102 56
     @param pp_prototype the prototype printer
103 57
     @param fmt the formater to print on
104 58
     @param contract the contract for the function to declare
105 59
  **)
106
  let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
107
    match opt_contract with
108
      | None -> pp_prototype fmt
109
      | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
110
      | Some (Contract contract) ->
111
          fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
112
            pp_prototype
113
            (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
114
            (Utils.pp_final_char_if_non_empty ",@," contract.assume)
115
            (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
116

  
117
  (** Print the prototype with a contract of the reset procedure from a machine.
60
  let pp_contract guarantees fmt =
61
    fprintf fmt "@,  @[<v>Global => null%t%a@]"
62
      (Utils.pp_final_char_if_non_empty ",@," guarantees)
63
      (Utils.fprintf_list ~sep:",@," pp_post) guarantees
64

  
65
(*
66
  let pp_transition_name fmt = fprintf fmt "transition"
67
  let pp_state_name_transition suffix fmt = fprintf fmt "%t_%s" pp_state_name suffix
68

  
69
  (** Printing function for basic assignement [var_name := value].
70

  
71
      @param fmt the formater to print on
72
      @param var_name the name of the variable
73
      @param value the value to be assigned
74
   **)
75
  let pp_basic_assign m fmt var_name value =
76
    fprintf fmt "%a = %a"
77
      (pp_access_var m) var_name
78
      (pp_value m) value
79

  
80

  
81
  (** Printing function for instruction. See
82
      {!type:Machine_code_types.instr_t} for more details on
83
      machine types.
84

  
85
      @param typed_submachines list of all typed machine instances of this machine
86
      @param machine the current machine
87
      @param fmt the formater to print on
88
      @param instr the instruction to print
89
   **)
90
  let rec pp_machine_instr typed_submachines machine instr fmt =
91
    let pp_instr = pp_machine_instr typed_submachines machine in
92
    (* Print args for a step call *)
93
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
94
    let pp_args vl il fmt =
95
      fprintf fmt "@[%a@]%t@[%a@]"
96
        (Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl
97
        (Utils.pp_final_char_if_non_empty ",@," il)
98
        (Utils.fprintf_list ~sep:",@ " pp_var_name) il
99
    in
100
    (* Print a when branch of a case *)
101
    let pp_when (cond, instrs) fmt =
102
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
103
    in
104
    (* Print a case *)
105
    let pp_case fmt (g, hl) =
106
      fprintf fmt "case %a is@,%aend case"
107
        (pp_value machine) g
108
        pp_block (List.map pp_when hl)
109
    in
110
    (* Print a if *)
111
    (* If neg is true the we must test for the negation of the condition. It
112
       first check that we don't have a negation and a else case, if so it
113
       inverses the two branch and remove the negation doing a recursive
114
       call. *)
115
    let rec pp_if neg fmt (g, instrs1, instrs2) =
116
      match neg, instrs2 with
117
        | true, Some x -> pp_if false fmt (g, x, Some instrs1)
118
        | _ ->
119
          let pp_cond =
120
            if neg then
121
              fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
122
            else
123
              pp_value machine
124
          in
125
          let pp_else = match instrs2 with
126
            | None -> fun fmt -> fprintf fmt ""
127
            | Some i2 -> fun fmt ->
128
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
129
          in
130
          fprintf fmt "if %a then@,%a%tend if"
131
            pp_cond g
132
            pp_block (List.map pp_instr instrs1)
133
            pp_else
134
    in
135
    match get_instr_desc instr with
136
      (* no reset *)
137
      | MNoReset _ -> ()
138
      (* reset  *)
139
      | MReset i when List.mem_assoc i typed_submachines ->
140
          let (substitution, submachine) = get_instance i typed_submachines in
141
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
142
          pp_call fmt (pp_package_access (pp_package, pp_name), [pp_state i])
143
      | MLocalAssign (ident, value) ->
144
          pp_basic_assign machine fmt ident value
145
      | MStateAssign (ident, value) ->
146
          pp_basic_assign machine fmt ident value
147
      | MStep ([i0], i, vl) when is_builtin_fun i ->
148
          let value = mk_val (Fun (i, vl)) i0.var_type in
149
          pp_basic_assign machine fmt i0 value
150
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
151
          let (substitution, submachine) = get_instance i typed_submachines in
152
          pp_package_call
153
            pp_step_procedure_name
154
            fmt
155
            (substitution, submachine, pp_state i, Some (pp_args vl il))
156
      | MBranch (_, []) -> assert false
157
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
158
          let neg = c1=tag_false in
159
          let other = match tl with
160
            | []         -> None
161
            | [(c2, i2)] -> Some i2
162
            | _          -> assert false
163
          in
164
          pp_if neg fmt (g, i1, other)
165
      | MBranch (g, hl) -> pp_case fmt (g, hl)
166
      | MComment s  ->
167
          let lines = String.split_on_char '\n' s in
168
          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
169
      | _ -> assert false
170

  
171
  (** Print the expression function representing the transition predicate.
118 172
     @param fmt the formater to print on
119 173
     @param machine the machine
120 174
  **)
121
  let pp_step_prototype_contract fmt m =
122
    pp_procedure_prototype_contract
123
      (pp_step_prototype m)
124
      fmt
125
      m.mspec
126
       
175
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
176
    let spec_instrs = match opt_spec_machine with
177
      | None -> []
178
      | Some m -> m.mstep.step_instrs
179
    in
180
    fprintf fmt "function %t (%a; %a) return Boolean is (@,  @[<v>%a@,@]) with Ghost"
181
      pp_transition_name
182
      pp_var_decl_mode (In, pp_state_name_transition "old", pp_state_type)
183
      pp_var_decl_mode (In, pp_state_name_transition "new", pp_state_type)
184
      (Utils.fprintf_list ~sep:" and@," (pp_machine_instr typed_submachines m)) (m.mstep.step_instrs@spec_instrs)*)
127 185
    
128 186
  (** Remove duplicates from a list according to a given predicate.
129 187
     @param eq the predicate defining equality
......
152 210
     @param typed_submachines list of all typed submachines of this machine
153 211
     @param m the machine
154 212
  **)
155
  let pp_file fmt (typed_submachines, m) =
213
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), m)) =
156 214
    let typed_machines = snd (List.split typed_submachines) in
157 215
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
158 216
    
159
    let machines_to_import = snd (List.split typed_machines_set) in
217
    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
160 218

  
161 219
    let polymorphic_types = find_all_polymorphic_type m in
162 220
    
......
164 222
      List.filter (fun (l, _) -> l != []) typed_machines_set in
165 223

  
166 224
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
167
    
168
    let pp_record fmt =
169
      pp_state_record_definition fmt (m.mmemory, typed_instances) in
170 225

  
171
    let pp_state_decl_and_reset fmt = fprintf fmt "%a;@,@,%t;@,@,"
226
    let pp_state_decl_and_reset fmt = fprintf fmt "%t;@,@,%a;@,@,"
172 227
      (*Declare the state type*)
173
      pp_private_limited_type_decl pp_state_type
228
      (pp_type_decl pp_state_type AdaLimitedPrivate)
174 229
      (*Declare the reset procedure*)
175
      (pp_reset_prototype m)
230
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None) AdaNoContent
176 231
    in
177 232

  
178
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,"
233
    let vars = List.map (build_pp_var_decl AdaNoMode) m.mmemory in
234
    let states = List.map build_pp_state_decl_from_subinstance typed_instances in
235
    let var_lists = (if vars = [] then [] else [vars])@(if states = [] then [] else [states]) in
236

  
237
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a"
179 238
      (*Instantiate the polymorphic type that need to be instantiated*)
180 239
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
181 240
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
182 241
      (*Define the state type*)
183
      pp_type_decl (pp_state_type, pp_record)
242
      (pp_record pp_state_type) var_lists
184 243
    in
185 244
    
186 245
    let pp_ifstatefull fmt pp =
......
189 248
      else
190 249
        fprintf fmt ""
191 250
    in
251

  
252
    let pp_content fmt =
253
      let pp_contract_opt = match guarantees with
254
                              | [] -> None
255
                              | _ ->  Some (pp_contract guarantees) in
256
      fprintf fmt "%a%a;@,%a" (* %a;@, *)
257
        pp_ifstatefull pp_state_decl_and_reset
258
        
259
        (*Declare the transition predicate*)
260
        (* pp_transition_predicate typed_submachines) (opt_spec_machine, m) *)
261
        
262
        (*Declare the step procedure*)
263
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
264
        
265
        (*Print the private section*)
266
        pp_ifstatefull pp_private_section
267
    in
192 268
    
193
    fprintf fmt "@[<v>%a%t%a%a@,  @[<v>@,%a%a;@,%a@]@,%a;@.@]"
269
    let pp_poly_types id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
270
    let pp_generics = List.map pp_poly_types polymorphic_types in
271
    
272
    fprintf fmt "@[<v>%a%t%a;@]@."
194 273
      
195 274
      (* Include all the subinstance package*)
196
      (Utils.fprintf_list ~sep:";@," pp_with_machine) machines_to_import
275
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) machines_to_import
197 276
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
198 277
      
199
      pp_generic polymorphic_types
200
      
201 278
      (*Begin the package*)
202
      (pp_begin_package false) m
203

  
204
      pp_ifstatefull pp_state_decl_and_reset
205
      
206
      (*Declare the step procedure*)
207
      pp_step_prototype_contract m
208
      
209
      (*Print the private section*)
210
      pp_ifstatefull pp_private_section
211
      
212
      (*End the package*)
213
      pp_end_package m
279
      (pp_package (pp_package_name m) pp_generics false) pp_content
214 280

  
215 281
end
src/backends/Ada/ada_backend_common.ml
5 5
open Corelang
6 6
open Machine_code_common
7 7

  
8
open Ada_printer
9
open Misc_printer
10
open Misc_lustre_function
11

  
8 12
(** Exception for unsupported features in Ada backend **)
9 13
exception Ada_not_supported of string
10 14

  
11
(** All the pretty print and aux functions common to the ada backend **)
15
(** Print the name of the state variable.
16
   @param fmt the formater to print on
17
**)
18
let pp_state_name fmt = fprintf fmt "state"
19
(** Print the type of the state variable.
20
   @param fmt the formater to print on
21
**)
22
let pp_state_type fmt = fprintf fmt "TState"
23
(** Print the name of the reset procedure
24
   @param fmt the formater to print on
25
**)
26
let pp_reset_procedure_name fmt = fprintf fmt "reset"
27
(** Print the name of the step procedure
28
   @param fmt the formater to print on
29
**)
30
let pp_step_procedure_name fmt = fprintf fmt "step"
31
(** Print the name of the main procedure.
32
   @param fmt the formater to print on
33
**)
34
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
35
(** Print the name of the arrow package.
36
   @param fmt the formater to print on
37
**)
38
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
39
(** Print the type of a polymorphic type.
40
   @param fmt the formater to print on
41
   @param id the id of the polymorphic type
42
**)
43
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
44

  
45

  
46

  
47

  
48

  
49

  
12 50

  
13
(* Misc pretty print functions *)
14 51

  
15
let is_machine_statefull m = not m.mname.node_dec_stateless
16 52

  
17 53
(*TODO Check all this function with unit test, improve this system and
18 54
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
......
47 83
  List.mem ident Basic_library.internal_funs ||
48 84
    List.mem_assoc ident ada_supported_funs
49 85

  
50
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
51
    underscore and must not contain a double underscore
52
   @param var name to be cleaned*)
53
let pp_clean_ada_identifier fmt name =
54
  let reserved_words = ["abort"; "else"; "new"; "return"; "boolean"; "integer";
55
                        "abs"; "elsif"; "not"; "reverse"; "abstract"; "end";
56
                        "null"; "accept"; "entry"; "select"; "access";
57
                        "exception"; "of"; "separate"; "aliased"; "exit";
58
                        "or"; "some"; "all"; "others"; "subtype"; "and";
59
                        "for"; "out"; "synchronized"; "array"; "function";
60
                        "overriding"; "at"; "tagged"; "generic"; "package";
61
                        "task"; "begin"; "goto"; "pragma"; "terminate";
62
                        "body"; "private"; "then"; "if"; "procedure"; "type";
63
                        "case"; "in"; "protected"; "constant"; "interface";
64
                        "until"; "is"; "raise"; "use"; "declare"; "	range";
65
                        "delay"; "limited"; "record"; "when"; "delta"; "loop";
66
                        "rem"; "while"; "digits"; "renames"; "with"; "do";
67
                        "mod"; "requeue"; "xor"; "float"] in
68
  let base_size = String.length name in
69
  assert(base_size > 0);
70
  let rec remove_double_underscore s = function
71
    | i when i == String.length s - 1 -> s
72
    | i when String.get s i == '_' && String.get s (i+1) == '_' ->
73
        remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
74
    | i -> remove_double_underscore s (i+1)
75
  in
76
  let name = if String.get name (base_size-1) == '_' then name^"ada" else name in
77
  let name = remove_double_underscore name 0 in
78
  let prefix = if String.length name != base_size
79
                  || String.get name 0 == '_' 
80
                  || List.exists (String.equal (String.lowercase_ascii name)) reserved_words then
81
                  "ada"
82
               else
83
                  ""
84
  in
85
  fprintf fmt "%s%s" prefix name
86

  
87
(** Encapsulate a pretty print function to lower case its result when applied
88
   @param pp the pretty print function
89
   @param fmt the formatter
90
   @param arg the argument of the pp function
91
**)
92
let pp_lowercase pp fmt =
93
  let str = asprintf "%t" pp in
94
  fprintf fmt "%s" (String. lowercase_ascii str)
95

  
96
(** Print a filename by lowercasing the base and appending an extension.
97
   @param extension the extension to append to the package name
98
   @param fmt the formatter
99
   @param pp_name the file base name printer
100
**)
101
let pp_filename extension fmt pp_name =
102
  fprintf fmt "%t.%s"
103
    (pp_lowercase pp_name)
104
    extension
105

  
106

  
107
(* Package pretty print functions *)
108

  
109
(** Return true if its the arrow machine
110
   @param machine the machine to test
111
*)
112
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
113

  
114
(** Print the name of the arrow package.
115
   @param fmt the formater to print on
116
**)
117
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
118

  
119 86
(** Print the name of a package associated to a machine.
120 87
   @param fmt the formater to print on
121 88
   @param machine the machine
122 89
**)
123
let pp_package_name fmt machine =
90
let pp_package_name machine fmt =
124 91
  if is_arrow machine then
125 92
      fprintf fmt "%t" pp_arrow_package_name
126 93
  else
127 94
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
128 95

  
129
(** Print the ada package introduction sentence it can be used for body and
130
declaration. Boolean parameter body should be true if it is a body delcaration.
131
   @param fmt the formater to print on
132
   @param fmt the formater to print on
133
   @param machine the machine
134
**)
135
let pp_begin_package body fmt machine =
136
  fprintf fmt "package %s%a is"
137
    (if body then "body " else "")
138
    pp_package_name machine
139

  
140
(** Print the ada package conclusion sentence.
141
   @param fmt the formater to print on
142
   @param machine the machine
143
**)
144
let pp_end_package fmt machine =
145
  fprintf fmt "end %a" pp_package_name machine
146

  
147
(** Print the access of an item from an other package.
148
   @param fmt the formater to print on
149
   @param package the package to use
150
   @param item the item which is accessed
151
**)
152
let pp_package_access fmt (package, item) =
153
  fprintf fmt "%t.%t" package item
154

  
155
(** Print the name of the main procedure.
156
   @param fmt the formater to print on
157
**)
158
let pp_main_procedure_name fmt =
159
  fprintf fmt "ada_main"
160

  
161
(** Print a with statement to include a package.
162
   @param fmt the formater to print on
163
   @param pp_pakage_name the package name printer
164
**)
165
let pp_private_with fmt pp_pakage_name =
166
  fprintf fmt "private with %t" pp_pakage_name
167

  
168
(** Print a with statement to include a package.
169
   @param fmt the formater to print on
170
   @param name the package name
171
**)
172
let pp_with fmt name =
173
  fprintf fmt "with %s" name
174

  
175
(** Print a with statement to include a machine.
176
   @param fmt the formater to print on
177
   @param machine the machine
178
**)
179
let pp_with_machine fmt machine =
180
  fprintf fmt "private with %a" pp_package_name machine
181

  
182
(** Extract a node from an instance.
183
   @param instance the instance
184
**)
185
let extract_node instance =
186
  let (_, (node, _)) = instance in
187
  match node.top_decl_desc with
188
    | Node nd         -> nd
189
    | _ -> assert false (*TODO*)
190

  
191
(** Extract from a machine list the one corresponding to the given instance.
192
      assume that the machine is in the list.
193
   @param machines list of all machines
194
   @param instance instance of a machine
195
   @return the machine corresponding to hte given instance
196
**)
197
let get_machine machines instance =
198
    let id = (extract_node instance).node_id in
199
    try
200
      List.find (function m -> m.mname.node_id=id) machines
201
    with
202
      Not_found -> assert false (*TODO*)
203

  
204

  
205
(* Type pretty print functions *)
206

  
207
(** Print a type declaration
208
   @param fmt the formater to print on
209
   @param pp_name a format printer which print the type name
210
   @param pp_value a format printer which print the type definition
211
**)
212
let pp_type_decl fmt (pp_name, pp_definition) =
213
  fprintf fmt "type %t is %t" pp_name pp_definition
214

  
215
(** Print a private type declaration
216
   @param fmt the formater to print on
217
   @param pp_name a format printer which print the type name
218
**)
219
let pp_private_type_decl fmt pp_name =
220
  let pp_definition fmt = fprintf fmt "private" in
221
  pp_type_decl fmt (pp_name, pp_definition)
222

  
223
(** Print a limited private type declaration
224
   @param fmt the formater to print on
225
   @param pp_name a format printer which print the type name
226
**)
227
let pp_private_limited_type_decl fmt pp_name =
228
  let pp_definition fmt = fprintf fmt "limited private" in
229
  pp_type_decl fmt (pp_name, pp_definition)
230

  
231
(** Print the type of the state variable.
232
   @param fmt the formater to print on
233
**)
234
let pp_state_type fmt =
235
  (* Type and variable names live in the same environement in Ada so name of
236
     this type and of the associated parameter : pp_state_name must be
237
     different *)
238
  fprintf fmt "TState"
239 96

  
240 97
(** Print the integer type name.
241 98
   @param fmt the formater to print on
......
252 109
**)
253 110
let pp_boolean_type fmt = fprintf fmt "Boolean"
254 111

  
255
(** Print the type of a polymorphic type.
256
   @param fmt the formater to print on
257
   @param id the id of the polymorphic type
258
**)
259
let pp_polymorphic_type fmt id =
260
  fprintf fmt "T_%i" id
261 112

  
262 113
(** Print a type.
263 114
   @param fmt the formater to print on
......
268 119
    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
269 120
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
270 121
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
271
    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.Types.tid
122
    | Types.Tunivar                  -> pp_polymorphic_type typ.Types.tid fmt
272 123
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
273 124
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
274 125
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
......
300 151
    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
301 152
    | _                              -> assert false (*TODO*)
302 153

  
303
(** Test if two types are the same.
304
   @param typ1 the first type
305
   @param typ2 the second type
306
**)
307
let pp_eq_type typ1 typ2 = 
308
  let get_basic typ = match (Types.repr typ).Types.tdesc with
309
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
310
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
311
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
312
    | _ -> assert false (*TODO*)
313
  in
314
  get_basic typ1 = get_basic typ2
315

  
316

  
317 154
(** Print the type of a variable.
318 155
   @param fmt the formater to print on
319 156
   @param id the variable
......
321 158
let pp_var_type fmt id = 
322 159
  pp_type fmt id.var_type
323 160

  
324
(** Extract all the inputs and outputs.
325
   @param machine the machine
326
   @return a list of all the var_decl of a macine
327
**)
328
let get_all_vars_machine m =
329
  m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
330

  
331
(** Check if a type is polymorphic.
332
   @param typ the type
333
   @return true if its polymorphic
334
**)
335
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
336

  
337
(** Find all polymorphic type : Types.Tunivar in a machine.
338
   @param machine the machine
339
   @return a list of id corresponding to polymorphic type
340
**)
341
let find_all_polymorphic_type m =
342
  let vars = get_all_vars_machine m in
343
  let extract id = id.var_type.tid in
344
  let polymorphic_type_vars =
345
    List.filter (function x-> is_Tunivar x.var_type) vars in
346
  List.sort_uniq (-) (List.map extract polymorphic_type_vars)
347

  
348 161
(** Print a package name with polymorphic types specified.
349 162
   @param substitution correspondance between polymorphic type id and their instantiation
350 163
   @param fmt the formater to print on
351 164
   @param machine the machine
352 165
**)
353
let pp_package_name_with_polymorphic substitution fmt machine =
166
let pp_package_name_with_polymorphic substitution machine fmt =
354 167
  let polymorphic_types = find_all_polymorphic_type machine in
355 168
  assert(List.length polymorphic_types = List.length substitution);
356 169
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
357 170
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
358 171
            polymorphic_types substituion);
359 172
  let instantiated_types = snd (List.split substitution) in
360
  fprintf fmt "%a%t%a"
361
    pp_package_name machine
173
  fprintf fmt "%t%t%a"
174
    (pp_package_name machine)
362 175
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
363 176
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
364 177

  
365

  
366
(* Variable pretty print functions *)
367

  
368
(** Represent the possible mode for a type of a procedure parameter **)
369
type parameter_mode = NoMode | In | Out | InOut
370

  
371
(** Print a parameter_mode.
372
   @param fmt the formater to print on
373
   @param mode the modifier
374
**)
375
let pp_parameter_mode fmt mode =
376
  fprintf fmt "%s" (match mode with
377
                     | NoMode -> ""
378
                     | In     -> "in"
379
                     | Out    -> "out"
380
                     | InOut  -> "in out")
381

  
382
(** Print the name of the state variable.
383
   @param fmt the formater to print on
384
**)
385
let pp_state_name fmt =
386
  fprintf fmt "state"
387

  
388

  
389 178
(** Print the name of a variable.
390 179
   @param fmt the formater to print on
391 180
   @param id the variable
......
404 193
  else
405 194
    pp_var_name fmt var
406 195

  
407
(** Print a variable declaration
408
   @param mode input/output mode of the parameter
409
   @param pp_name a format printer wich print the variable name
410
   @param pp_type a format printer wich print the variable type
411
   @param fmt the formater to print on
412
   @param id the variable
413
**)
414
let pp_var_decl fmt (mode, pp_name, pp_type) =
415
  fprintf fmt "%t: %a%s%t"
416
    pp_name
417
    pp_parameter_mode mode
418
    (if mode = NoMode then "" else " ")
419
    pp_type
420

  
421
(** Print variable declaration for machine variable
422
   @param mode input/output mode of the parameter
423
   @param fmt the formater to print on
424
   @param id the variable
425
**)
426
let pp_machine_var_decl mode fmt id =
427
  let pp_name = function fmt -> pp_var_name fmt id in
428
  let pp_type = function fmt -> pp_var_type fmt id in
429
  pp_var_decl fmt (mode, pp_name, pp_type)
430

  
431
(** Print variable declaration for a local state variable
432
   @param fmt the formater to print on
433
   @param mode input/output mode of the parameter
434
**)
435
let pp_state_var_decl fmt mode =
436
  let pp_name = pp_state_name in
437
  let pp_type = pp_state_type in
438
  pp_var_decl fmt (mode, pp_name, pp_type)
439

  
440
(** Print the declaration of a state element of a machine.
441
   @param substitution correspondance between polymorphic type id and their instantiation
442
   @param name name of the variable
443
   @param fmt the formater to print on
444
   @param machine the machine
445
**)
446
let pp_node_state_decl substitution name fmt machine =
447
  let pp_package fmt = pp_package_name_with_polymorphic substitution fmt machine in
448
  let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
449
  let pp_name fmt = pp_clean_ada_identifier fmt name in
450
  pp_var_decl fmt (NoMode, pp_name, pp_type)
451 196

  
197
(* Expression print functions *)
452 198

  
453
(* Prototype pretty print functions *)
454

  
455
(** Print the name of the reset procedure **)
456
let pp_reset_procedure_name fmt = fprintf fmt "reset"
199
(* Printing functions for basic operations and expressions *)
200
(* TODO: refactor code -> use let rec and for basic pretty printing
201
   function *)
202
(** Printing function for Ada tags, mainly booleans.
457 203

  
458
(** Print the name of the step procedure **)
459
let pp_step_procedure_name fmt = fprintf fmt "step"
204
    @param fmt the formater to use
205
    @param t the tag to print
206
 **)
207
let pp_ada_tag fmt t =
208
  pp_print_string fmt
209
    (if t = tag_true then "True" else if t = tag_false then "False" else t)
460 210

  
461
(** Print the name of the init procedure **)
462
let pp_init_procedure_name fmt = fprintf fmt "init"
211
(** Printing function for machine type constants. For the moment,
212
    arrays are not supported.
463 213

  
464
(** Print the name of the clear procedure **)
465
let pp_clear_procedure_name fmt = fprintf fmt "clear"
214
    @param fmt the formater to use
215
    @param c the constant to print
216
 **)
217
let pp_ada_const fmt c =
218
  match c with
219
  | Const_int i                     -> pp_print_int fmt i
220
  | Const_real (c, e, s)            ->
221
      fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
222
  | Const_tag t                     -> pp_ada_tag fmt t
223
  | Const_string _ | Const_modeid _ ->
224
    (Format.eprintf
225
       "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
226
     assert false)
227
  | _                               ->
228
    raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
229
    support this constant")
230

  
231
(** Printing function for expressions [v1 modulo v2]. Depends
232
    on option [integer_div_euclidean] to choose between mathematical
233
    modulo or remainder ([rem] in Ada).
234

  
235
    @param pp_value pretty printer for values
236
    @param v1 the first value in the expression
237
    @param v2 the second value in the expression
238
    @param fmt the formater to print on
239
 **)
240
let pp_mod pp_value v1 v2 fmt =
241
  if !Options.integer_div_euclidean then
242
    (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
243
    Format.fprintf fmt
244
      "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
245
      pp_value v1 pp_value v2
246
      pp_value v1 pp_value v2
247
      pp_value v2
248
  else (* Ada behavior for rem *)
249
    Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
250

  
251
(** Printing function for expressions [v1 div v2]. Depends on
252
    option [integer_div_euclidean] to choose between mathematic
253
    division or Ada division.
254

  
255
    @param pp_value pretty printer for values
256
    @param v1 the first value in the expression
257
    @param v2 the second value in the expression
258
    @param fmt the formater to print in
259
 **)
260
let pp_div pp_value v1 v2 fmt =
261
  if !Options.integer_div_euclidean then
262
    (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
263
    Format.fprintf fmt "(%a - %t) / %a"
264
      pp_value v1
265
      (pp_mod pp_value v1 v2)
266
      pp_value v2
267
  else (* Ada behavior for / *)
268
    Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
269

  
270
(** Printing function for basic lib functions.
271

  
272
    @param pp_value pretty printer for values
273
    @param i a string representing the function
274
    @param fmt the formater to print on
275
    @param vl the list of operands
276
 **)
277
let pp_basic_lib_fun pp_value ident fmt vl =
278
  match ident, vl with
279
  | "uminus", [v]    ->
280
    Format.fprintf fmt "(- %a)" pp_value v
281
  | "not", [v]       ->
282
    Format.fprintf fmt "(not %a)" pp_value v
283
  | "impl", [v1; v2] ->
284
    Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
285
  | "=", [v1; v2]    ->
286
    Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
287
  | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
288
  | "equi", [v1; v2] ->
289
    Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
290
  | "xor", [v1; v2]  ->
291
    Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
292
  | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
293
  | "&&", [v1; v2]    ->
294
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
295
  | "||", [v1; v2]    ->
296
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
297
  | "!=", [v1; v2]    ->
298
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
299
  | op, [v1; v2]     ->
300
    Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
301
  | op, [v1] when  List.mem_assoc ident ada_supported_funs ->
302
    let pkg, name = try List.assoc ident ada_supported_funs
303
      with Not_found -> assert false in
304
    let pkg = pkg^(if String.equal pkg "" then "" else ".") in
305
      Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1
306
  | fun_name, _      ->
307
    (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
308

  
309
(** Printing function for values.
310

  
311
    @param m the machine to know the state variable
312
    @param fmt the formater to use
313
    @param value the value to print. Should be a
314
           {!type:Machine_code_types.value_t} value
315
 **)
316
let rec pp_value m fmt value =
317
  match value.value_desc with
318
  | Cst c             -> pp_ada_const fmt c
319
  | Var var      -> pp_access_var m fmt var
320
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value m) f_ident fmt vl
321
  | _                 ->
322
    raise (Ada_not_supported
323
             "unsupported: Ada_backend.adb.pp_value does not support this value type")
466 324

  
467
(** Print the prototype of a procedure with non input/outputs
468
   @param fmt the formater to print on
469
   @param name the name of the procedure
470
**)
471
let pp_simple_prototype pp_name fmt =
472
  fprintf fmt "procedure %t" pp_name
473

  
474
(** Print the prototype of a machine procedure. The first parameter is always
475
the state, state_modifier specify the modifier applying to it. The next
476
parameters are inputs and the last parameters are the outputs.
477
   @param state_mode_opt None if no state parameter required and some input/output mode for it else
478
   @param input list of the input parameter of the procedure
479
   @param output list of the output parameter of the procedure
480
   @param fmt the formater to print on
481
   @param name the name of the procedure
482
**)
483
let pp_base_prototype state_mode_opt input output fmt pp_name =
484
  let pp_var_decl_state fmt = match state_mode_opt with
485
    | None -> fprintf fmt ""
486
    | Some state_mode -> fprintf fmt "%a" pp_state_var_decl state_mode
487
  in
488
  fprintf fmt "procedure %t(@[<v>%t%t@[%a@]%t@[%a@])@]"
489
    pp_name
490
    pp_var_decl_state
491
    (fun fmt -> if state_mode_opt != None && input!=[] then
492
      fprintf fmt ";@," else fprintf fmt "")
493
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl In)) input
494
    (fun fmt -> if (state_mode_opt != None || input!=[]) && output != [] then
495
      fprintf fmt ";@," else fprintf fmt "")
496
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl Out)) output
497

  
498
(** Print the prototype of the step procedure of a machine.
499
   @param m the machine
500
   @param fmt the formater to print on
501
   @param pp_name name function printer
502
**)
503
let pp_step_prototype m fmt =
504
  let state_mode = if is_machine_statefull m then Some InOut else None in
505
  pp_base_prototype state_mode m.mstep.step_inputs m.mstep.step_outputs fmt pp_step_procedure_name
506 325

  
507
(** Print the prototype of the reset procedure of a machine.
508
   @param m the machine
509
   @param fmt the formater to print on
510
   @param pp_name name function printer
326
(** Print the filename of a machine package.
327
   @param extension the extension to append to the package name
328
   @param fmt the formatter
329
   @param machine the machine corresponding to the package
511 330
**)
512
let pp_reset_prototype m fmt =
513
  let state_mode = if is_machine_statefull m then Some Out else None in
514
  pp_base_prototype state_mode m.mstatic [] fmt pp_reset_procedure_name
331
let pp_machine_filename extension fmt machine =
332
  pp_filename extension fmt (pp_package_name machine)
515 333

  
516
(** Print the prototype of the init procedure of a machine.
517
   @param m the machine
518
   @param fmt the formater to print on
519
   @param pp_name name function printer
520
**)
521
let pp_init_prototype m fmt =
522
  let state_mode = if is_machine_statefull m then Some Out else None in
523
  pp_base_prototype state_mode m.mstatic [] fmt pp_init_procedure_name
334
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
524 335

  
525
(** Print the prototype of the clear procedure of a machine.
526
   @param m the machine
527
   @param fmt the formater to print on
528
   @param pp_name name function printer
529
**)
530
let pp_clear_prototype m fmt =
531
  let state_mode = if is_machine_statefull m then Some InOut else None in
532
  pp_base_prototype state_mode m.mstatic [] fmt pp_clear_procedure_name
533 336

  
534
(** Print a one line comment with the final new line character to avoid
535
      commenting anything else.
337
(** Print the declaration of a state element of a subinstance of a machine.
338
   @param machine the machine
536 339
   @param fmt the formater to print on
537
   @param s the comment without newline character
538
**)
539
let pp_oneline_comment fmt s =
540
  assert (not (String.contains s '\n'));
541
  fprintf fmt "-- %s@," s
542

  
543

  
544
(* Functions which computes the substitution for polymorphic type *)
545

  
546
(** Check if a submachine is statefull.
547
    @param submachine a submachine
548
    @return true if the submachine is statefull
340
   @param substitution correspondance between polymorphic type id and their instantiation
341
   @param ident the identifier of the subinstance
342
   @param submachine the submachine of the subinstance
549 343
**)
550
let is_submachine_statefull submachine =
551
    not (snd (snd submachine)).mname.node_dec_stateless
344
let build_pp_state_decl_from_subinstance (name, (substitution, machine)) =
345
  let pp_package = pp_package_name_with_polymorphic substitution machine in
346
  let pp_type = pp_package_access (pp_package, pp_state_type) in
347
  let pp_name fmt = pp_clean_ada_identifier fmt name in
348
  (AdaNoMode, pp_name, pp_type)
552 349

  
553
(** Find a submachine step call in a list of instructions.
554
    @param ident submachine instance ident
555
    @param instr_list List of instruction sto search
556
    @return a list of pair containing input types and output types for each step call found
557
**)
558
let rec find_submachine_step_call ident instr_list =
559
  let search_instr instruction = 
560
    match instruction.instr_desc with
561
      | MStep (il, i, vl) when String.equal i ident -> [
562
        (List.map (function x-> x.value_type) vl,
563
            List.map (function x-> x.var_type) il)]
564
      | MBranch (_, l) -> List.flatten
565
          (List.map (function x, y -> find_submachine_step_call ident y) l)
566
      | _ -> []
567
  in
568
  List.flatten (List.map search_instr instr_list)
569

  
570
(** Check that two types are the same.
571
   @param t1 a type
572
   @param t2 an other type
573
   @param return true if the two types are Tbasic or Tunivar and equal
574
**)
575
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
576
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
577
    | Types.Tbasic x, Types.Tbasic y -> x = y
578
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
579
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
580
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
581
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
582
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
583
    | _ -> eprintf "ERROR: %a | %a" pp_type t1 pp_type t2; assert false (* TODO *)
584

  
585
(** Extend a substitution to unify the two given types. Only the
586
  first type can be polymorphic.
587
    @param subsitution the base substitution
588
    @param type_poly the type which can be polymorphic
589
    @param typ the type to match type_poly with
590
**)
591
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =
592
  assert(not (is_Tunivar typ));
593
  (* If type_poly is polymorphic *)
594
  if is_Tunivar type_poly then
595
    (* If a subsitution exists for it *)
596
    if List.mem_assoc type_poly.tid substituion then
597
    begin
598
      (* We check that the type corresponding to type_poly in the subsitution
599
         match typ *)
600
      (try
601
        assert(check_type_equal (List.assoc type_poly.tid substituion) typ)
602
      with
603
        Not_found -> assert false);
604
      (* We return the original substituion, it is already correct *)
605
      substituion
606
    end
607
    (* If type_poly is not in the subsitution *)
608
    else
609
      (* We add it to the substituion *)
610
      (type_poly.tid, typ)::substituion
611
  (* iftype_poly is not polymorphic *)
612
  else
613
  begin
614
    (* We check that type_poly and typ are the same *)
615
    assert(check_type_equal type_poly typ);
616
    (* We return the original substituion, it is already correct *)
617
    substituion
618
  end
619

  
620
(** Check that two calls are equal. A call is
621
  a pair of list of types, the inputs and the outputs.
622
   @param calls a list of pair of list of types
623
   @param return true if the two pairs are equal
624
**)
625
let check_call_equal (i1, o1) (i2, o2) =
626
  (List.for_all2 check_type_equal i1 i2)
627
    && (List.for_all2 check_type_equal i1 i2)
628

  
629
(** Check that all the elements of list of calls are equal to one.
630
  A call is a pair of list of types, the inputs and the outputs.
631
   @param call a pair of list of types
632
   @param calls a list of pair of list of types
633
   @param return true if all the elements are equal
634
**)
635
let check_calls call calls =
636
  List.for_all (check_call_equal call) calls
637

  
638
(** Extract from a subinstance that can have polymorphic type the instantiation
639
    of all its polymorphic type instanciation for a given machine. It searches
640
    the step calls and extract a substitution for all polymorphic type from
641
    it.
642
   @param machine the machine which instantiate the subinstance
643
   @param ident the identifier of the instance which permits to find the step call
644
   @param submachine the machine corresponding to the subinstance
645
   @return the correspondance between polymorphic type id and their instantiation
646
**)
647
let get_substitution machine ident submachine =
648
  (* extract the calls to submachines from the machine *)
649
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in
650
  (* extract the first call  *)
651
  let call = match calls with
652
              (* assume that there is always one call to a subinstance *)
653
              | []    -> assert(false)
654
              | h::t  -> h in
655
  (* assume that all the calls to a subinstance are using the same type *)
656
  assert(check_calls call calls);
657
  (* make a list of all types from input and output vars *)
658
  let call_types = (fst call)@(snd call) in
659
  (* extract all the input and output vars from the submachine *)
660
  let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in
661
  (* keep only the type of vars *)
662
  let machine_types = List.map (function x-> x.var_type) machine_vars in
663
  (* assume that there is the same numer of input and output in the submachine
664
      and the call *)
665
  assert (List.length machine_types = List.length call_types);
666
  (* Unify the two lists of types *)
667
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
668
  (* Assume that our substitution match all the possible
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff