Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY almost 3 years ago

Ada: First support for transition predicate generation.

View differences:

src/backends/Ada/ada_backend_common.ml
93 93
  else
94 94
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
95 95

  
96

  
97
(** Print the integer type name.
98
   @param fmt the formater to print on
99
**)
100
let pp_integer_type fmt = fprintf fmt "Integer"
101

  
102
(** Print the float type name.
103
   @param fmt the formater to print on
104
**)
105
let pp_float_type fmt = fprintf fmt "Float"
106

  
107
(** Print the boolean type name.
108
   @param fmt the formater to print on
109
**)
110
let pp_boolean_type fmt = fprintf fmt "Boolean"
111

  
112

  
113 96
(** Print a type.
114 97
   @param fmt the formater to print on
115 98
   @param type the type
......
179 162
   @param fmt the formater to print on
180 163
   @param id the variable
181 164
**)
182
let pp_var_name fmt id =
165
let pp_var_name id fmt =
183 166
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
184 167

  
185 168
(** Print the complete name of variable.
......
187 170
   @param fmt the formater to print on
188 171
   @param var the variable
189 172
**)
190
let pp_access_var m fmt var =
191
  if is_memory m var then
192
    fprintf fmt "%t.%a" pp_state_name pp_var_name var
193
  else
194
    pp_var_name fmt var
195

  
173
let pp_var env fmt var =
174
  match List.assoc_opt var.var_id env with
175
    | None -> pp_var_name var fmt
176
    | Some pp_state -> pp_access pp_state (pp_var_name var) fmt
196 177

  
197 178
(* Expression print functions *)
198 179

  
......
296 277
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
297 278
  | "!=", [v1; v2]    ->
298 279
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
280
  | "ite", [v1; v2; v3]    ->
281
    Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
299 282
  | op, [v1; v2]     ->
300 283
    Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
301 284
  | op, [v1] when  List.mem_assoc ident ada_supported_funs ->
......
313 296
    @param value the value to print. Should be a
314 297
           {!type:Machine_code_types.value_t} value
315 298
 **)
316
let rec pp_value m fmt value =
299
let rec pp_value env fmt value =
317 300
  match value.value_desc with
318 301
  | 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
302
  | Var var      -> pp_var env fmt var (* Find better to test if it is memory or not *)
303
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl
321 304
  | _                 ->
322 305
    raise (Ada_not_supported
323 306
             "unsupported: Ada_backend.adb.pp_value does not support this value type")
......
341 324
   @param ident the identifier of the subinstance
342 325
   @param submachine the submachine of the subinstance
343 326
**)
344
let build_pp_state_decl_from_subinstance (name, (substitution, machine)) =
327
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =
345 328
  let pp_package = pp_package_name_with_polymorphic substitution machine in
346 329
  let pp_type = pp_package_access (pp_package, pp_state_type) in
347 330
  let pp_name fmt = pp_clean_ada_identifier fmt name in
348
  (AdaNoMode, pp_name, pp_type)
331
  (mode, pp_name, pp_type, with_statement)
349 332

  
350 333
(** Print variable declaration for a local state variable
351 334
   @param fmt the formater to print on
352 335
   @param mode input/output mode of the parameter
353 336
**)
354
let build_pp_state_decl mode =
355
  (mode, pp_state_name, pp_state_type)
337
let build_pp_state_decl mode with_statement =
338
  (mode, pp_state_name, pp_state_type, with_statement)
356 339

  
357
let build_pp_var_decl mode var =
358
  let pp_name = function fmt -> pp_var_name fmt var in
340
let build_pp_var_decl mode with_statement var =
341
  let pp_name = function fmt -> pp_var_name var fmt in
359 342
  let pp_type = function fmt -> pp_var_type fmt var in
360
  (mode, pp_name, pp_type)
343
  (mode, pp_name, pp_type, with_statement)
361 344

  
362
let build_pp_var_decl_local var =
363
  AdaLocalVar (build_pp_var_decl AdaNoMode var)
345
let build_pp_var_decl_local with_statement var =
346
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
364 347

  
365
let build_pp_var_decl_step_input mode m =
348
let build_pp_var_decl_step_input mode with_statement m =
366 349
  if m.mstep.step_inputs=[] then [] else
367
    [List.map (build_pp_var_decl mode) m.mstep.step_inputs]
350
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
368 351

  
369
let build_pp_var_decl_step_output mode m =
352
let build_pp_var_decl_step_output mode with_statement m =
370 353
  if m.mstep.step_outputs=[] then [] else
371
    [List.map (build_pp_var_decl mode) m.mstep.step_outputs]
354
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
372 355

  
373
let build_pp_var_decl_static mode m =
356
let build_pp_var_decl_static mode with_statement m =
374 357
  if m.mstatic=[] then [] else
375
    [List.map (build_pp_var_decl mode) m.mstatic]
358
    [List.map (build_pp_var_decl mode with_statement) m.mstatic]
376 359

  
377 360
let build_pp_arg_step m =
378
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut]] else [])
379
    @ (build_pp_var_decl_step_input AdaIn m)
380
    @ (build_pp_var_decl_step_output AdaOut m)
361
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
362
    @ (build_pp_var_decl_step_input AdaIn None m)
363
    @ (build_pp_var_decl_step_output AdaOut None m)
381 364

  
382 365
let build_pp_arg_reset m =
383
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut]] else [])
384
    @ (build_pp_var_decl_static AdaIn m)
366
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
367
    @ (build_pp_var_decl_static AdaIn None m)
368

  
369

  
370
let build_pp_arg_transition m =
371
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
372
    @ (build_pp_var_decl_step_input AdaIn None m)
373
    @ (build_pp_var_decl_step_output AdaOut None m)
374

  

Also available in: Unified diff