Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/Ada/ada_backend_adb.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13

  
14 13
open Machine_code_types
15 14
open Lustre_types
16 15
open Corelang
17 16
open Machine_code_common
18

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

  
24
(** Main module for generating packages bodies
25
 **)
26
module Main =
27
struct
28

  
22
(** Main module for generating packages bodies **)
23
module Main = struct
29 24
  (** Printing function for basic assignement [var := value].
30 25

  
31
      @param fmt the formater to print on
32
      @param var_name the name of the variable
33
      @param value the value to be assigned
34
   **)
26
      @param fmt the formater to print on @param var_name the name of the
27
      variable @param value the value to be assigned **)
35 28
  let pp_assign env fmt var value =
36
    fprintf fmt "%a := %a"
37
      (pp_var env) var
38
      (pp_value env) value
29
    fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
39 30

  
40
  (** Printing function for instruction. See
41
      {!type:Machine_code_types.instr_t} for more details on
42
      machine types.
31
  (** Printing function for instruction. See {!type:Machine_code_types.instr_t}
32
      for more details on machine types.
43 33

  
44
      @param typed_submachines list of all typed machine instances of this machine
45
      @param machine the current machine
46
      @param fmt the formater to print on
47
      @param instr the instruction to print
48
   **)
34
      @param typed_submachines list of all typed machine instances of this
35
      machine @param machine the current machine @param fmt the formater to
36
      print on @param instr the instruction to print **)
49 37
  let rec pp_machine_instr typed_submachines env instr fmt =
50 38
    let pp_instr = pp_machine_instr typed_submachines env in
51 39
    (* Print args for a step call *)
......
56 44
    in
57 45
    (* Print a case *)
58 46
    let pp_case fmt (g, hl) =
59
      fprintf fmt "case %a is@,%aend case"
60
        (pp_value env) g
61
        pp_block (List.map pp_when hl)
47
      fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
48
        (List.map pp_when hl)
62 49
    in
63 50
    (* Print a if *)
64 51
    (* If neg is true the we must test for the negation of the condition. It
65 52
       first check that we don't have a negation and a else case, if so it
66
       inverses the two branch and remove the negation doing a recursive
67
       call. *)
53
       inverses the two branch and remove the negation doing a recursive call. *)
68 54
    let pp_if fmt (neg, g, instrs1, instrs2) =
69 55
      let pp_cond =
70
        if neg then
71
          fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
72
        else
73
          pp_value env
56
        if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
57
        else pp_value env
74 58
      in
75
      let pp_else = match instrs2 with
76
        | None -> fun fmt -> fprintf fmt ""
77
        | Some i2 -> fun fmt ->
78
            fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
59
      let pp_else =
60
        match instrs2 with
61
        | None ->
62
          fun fmt -> fprintf fmt ""
63
        | Some i2 ->
64
          fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
79 65
      in
80
      fprintf fmt "if %a then@,%a%tend if"
81
        pp_cond g
82
        pp_block (List.map pp_instr instrs1)
66
      fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
67
        (List.map pp_instr instrs1)
83 68
        pp_else
84 69
    in
85 70
    match get_instr_desc instr with
86
      (* no reset *)
87
      | MNoReset _ -> ()
88
      (* TODO: handle clear_reset *)
89
      | MClearReset -> ()
90
      (* reset  *)
91
      | MSetReset i when List.mem_assoc i typed_submachines ->
92
          let (substitution, submachine) = get_instance i typed_submachines in
93
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
94
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
95
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
96
      | MLocalAssign (ident, value) ->
97
          pp_assign env fmt ident value
98
      | MStateAssign (ident, value) ->
99
          pp_assign env fmt ident value
100
      | MStep ([i0], i, vl) when is_builtin_fun i ->
101
          let value = mk_val (Fun (i, vl)) i0.var_type in
102
            pp_assign env fmt i0 value
103
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
104
          let (substitution, submachine) = get_instance i typed_submachines in
105
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
106
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
107
          let output = List.map pp_var_name il in
108
          let args =
109
            (if is_machine_statefull submachine then [[pp_state i]] else [])
110
              @(if input!=[] then [input] else [])
111
              @(if output!=[] then [output] else [])
112
          in
113
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
114
      | MBranch (_, []) -> assert false
115
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
116
          pp_if fmt (build_if g c1 i1 tl)
117
      | MBranch (g, hl) -> pp_case fmt (g, hl)
118
      | MComment s  ->
119
          let lines = String.split_on_char '\n' s in
120
          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
121
      | _ -> assert false
71
    (* no reset *)
72
    | MNoReset _ ->
73
      ()
74
    (* TODO: handle clear_reset *)
75
    | MClearReset ->
76
      ()
77
    (* reset *)
78
    | MSetReset i when List.mem_assoc i typed_submachines ->
79
      let substitution, submachine = get_instance i typed_submachines in
80
      let pp_package =
81
        pp_package_name_with_polymorphic substitution submachine
82
      in
83
      let args =
84
        if is_machine_statefull submachine then [ [ pp_state i ] ] else []
85
      in
86
      pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
87
    | MLocalAssign (ident, value) ->
88
      pp_assign env fmt ident value
89
    | MStateAssign (ident, value) ->
90
      pp_assign env fmt ident value
91
    | MStep ([ i0 ], i, vl) when is_builtin_fun i ->
92
      let value = mk_val (Fun (i, vl)) i0.var_type in
93
      pp_assign env fmt i0 value
94
    | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
95
      let substitution, submachine = get_instance i typed_submachines in
96
      let pp_package =
97
        pp_package_name_with_polymorphic substitution submachine
98
      in
99
      let input = List.map (fun x fmt -> pp_value env fmt x) vl in
100
      let output = List.map pp_var_name il in
101
      let args =
102
        (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
103
        @ (if input != [] then [ input ] else [])
104
        @ if output != [] then [ output ] else []
105
      in
106
      pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
107
    | MBranch (_, []) ->
108
      assert false
109
    | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
110
      pp_if fmt (build_if g c1 i1 tl)
111
    | MBranch (g, hl) ->
112
      pp_case fmt (g, hl)
113
    | MComment s ->
114
      let lines = String.split_on_char '\n' s in
115
      fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
116
    | _ ->
117
      assert false
122 118

  
123 119
  (** Print the definition of the step procedure from a machine.
124 120

  
125
     @param typed_submachines list of all typed machine instances of this machine
126
     @param fmt the formater to print on
127
     @param machine the machine
128
  **)
121
      @param typed_submachines list of all typed machine instances of this
122
      machine @param fmt the formater to print on @param machine the machine **)
129 123
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
130
    let transform_local_to_state_assign instr = match instr.instr_desc with
131
      | MLocalAssign (ident, value) -> 
124
    let transform_local_to_state_assign instr =
125
      match instr.instr_desc with
126
      | MLocalAssign (ident, value) ->
132 127
        { instr with instr_desc = MStateAssign (ident, value) }
133
      | _ -> instr
128
      | _ ->
129
        instr
134 130
    in
135
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
136
      | None -> [], []
131
    let pp_local_ghost_list, spec_instrs =
132
      match m_spec_opt with
133
      | None ->
134
        [], []
137 135
      | Some m_spec ->
138
          List.map (build_pp_var_decl_local (Some (true, false, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
139
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
136
        ( List.map
137
            (build_pp_var_decl_local (Some (true, false, [], [])))
138
            (List.filter
139
               (fun x -> not (List.mem x.var_id guarantees))
140
               m_spec.mstep.step_locals),
141
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
142
    in
143
    let pp_local_list =
144
      List.map (build_pp_var_decl_local None) m.mstep.step_locals
145
    in
146
    let pp_instr_list =
147
      List.map
148
        (pp_machine_instr typed_submachines env)
149
        (m.mstep.step_instrs @ spec_instrs)
150
    in
151
    let content =
152
      AdaProcedureContent
153
        ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
154
          @ if pp_local_list = [] then [] else [ pp_local_list ]),
155
          pp_instr_list )
140 156
    in
141
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
142
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
143
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
144 157
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
145 158

  
146 159
  (** Print the definition of the reset procedure from a machine.
147 160

  
148
     @param typed_submachines list of all typed machine instances of this machine
149
     @param fmt the formater to print on
150
     @param machine the machine
151
  **)
161
      @param typed_submachines list of all typed machine instances of this
162
      machine @param fmt the formater to print on @param machine the machine **)
152 163
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
153
    let build_assign = function var ->
154
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
164
    let build_assign = function
165
      | var ->
166
        mkinstr (MStateAssign (var, mk_default_value var.var_type))
155 167
    in
156
    let env, memory = match m_spec_opt with
157
      | None -> env, m.mmemory
158
      | Some _ ->
159
          env,
160
          (m.mmemory)
168
    let env, memory =
169
      match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
161 170
    in
162 171
    let assigns = List.map build_assign memory in
163
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
164
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
172
    let pp_instr_list =
173
      List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
174
    in
175
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
176
      (AdaProcedureContent ([], pp_instr_list))
165 177

  
166
  (** Print the package definition(ads) of a machine.
167
    It requires the list of all typed instance.
168
    A typed submachine instance is (ident, type_machine) with ident
169
    the instance name and typed_machine is (substitution, machine) with machine
170
    the machine associated to the instance and substitution the instanciation of
171
    all its polymorphic types.
172
     @param fmt the formater to print on
173
     @param typed_submachines list of all typed machine instances of this machine
174
     @param m the machine
175
  **)
176
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
178
  (** Print the package definition(ads) of a machine. It requires the list of
179
      all typed instance. A typed submachine instance is (ident, type_machine)
180
      with ident the instance name and typed_machine is (substitution, machine)
181
      with machine the machine associated to the instance and substitution the
182
      instanciation of all its polymorphic types. @param fmt the formater to
183
      print on @param typed_submachines list of all typed machine instances of
184
      this machine @param m the machine **)
185
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
186
      =
177 187
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
178 188
    let pp_reset fmt =
179 189
      if is_machine_statefull machine then
180
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
181
      else
182
        fprintf fmt ""
190
        fprintf fmt "%a;@,@,"
191
          (pp_reset_definition env typed_submachines)
192
          (machine, opt_spec_machine)
193
      else fprintf fmt ""
183 194
    in
184 195
    let aux pkgs (id, _) =
185 196
      try
186
        let (pkg, _) = List.assoc id ada_supported_funs in
187
        if List.mem pkg pkgs then
188
          pkgs
189
        else
190
          pkg::pkgs
197
        let pkg, _ = List.assoc id ada_supported_funs in
198
        if List.mem pkg pkgs then pkgs else pkg :: pkgs
191 199
      with Not_found -> pkgs
192 200
    in
193 201
    let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
194 202
    let pp_content fmt =
195
      fprintf fmt "%t%a"
196
        (*Define the reset procedure*)
197
        pp_reset
198
        
203
      fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
199 204
        (*Define the step procedure*)
200
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
205
        (pp_step_definition env typed_submachines)
206
        (machine, opt_spec_machine, guarantees)
201 207
    in
202 208
    fprintf fmt "%a%t%a;@."
203
      
204 209
      (* Include all the required packages*)
205
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
210
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate))
211
      packages
206 212
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
207
      
208 213
      (*Print package*)
209
      (pp_package (pp_package_name machine) [] true ) pp_content
210

  
214
      (pp_package (pp_package_name machine) [] true)
215
      pp_content
211 216
end
212 217

  
213 218
(* Local Variables: *)

Also available in: Unified diff