Revision 826063db
Added by Guillaume DAVY over 3 years ago
src/backends/Ada/ada_backend_adb.ml | ||
---|---|---|
33 | 33 |
(pp_access_var m) var_name |
34 | 34 |
(pp_value m) value |
35 | 35 |
|
36 |
(** Extract from a machine the instance corresponding to the identifier, |
|
37 |
assume that the identifier exists in the instances of the machine. |
|
38 |
|
|
39 |
@param identifier the instance identifier |
|
40 |
@param machine a machine |
|
41 |
@return the instance of machine.minstances corresponding to identifier |
|
42 |
**) |
|
43 |
let get_instance identifier typed_submachines = |
|
44 |
try |
|
45 |
List.assoc identifier typed_submachines |
|
46 |
with Not_found -> assert false |
|
47 |
|
|
48 |
(** Printing a call to a package function |
|
49 |
|
|
50 |
@param typed_submachines list of all typed machine instances of this machine |
|
51 |
@param pp_name printer for the function name |
|
52 |
@param fmt the formater to use |
|
53 |
@param identifier the instance identifier |
|
54 |
@param pp_args_opt optional printer for other arguments |
|
55 |
**) |
|
56 |
let pp_package_call typed_submachines pp_name fmt (identifier, pp_args_opt) = |
|
57 |
let (substitution, submachine) = get_instance identifier typed_submachines in |
|
58 |
let statefull = is_machine_statefull submachine in |
|
59 |
let pp_opt fmt = function |
|
60 |
| Some pp_args when statefull -> fprintf fmt ",@,%t" pp_args |
|
61 |
| Some pp_args -> pp_args fmt |
|
62 |
| None -> fprintf fmt "" |
|
63 |
in |
|
64 |
let pp_state fmt = |
|
65 |
if statefull then |
|
66 |
fprintf fmt "%t.%s" pp_state_name identifier |
|
67 |
else |
|
68 |
fprintf fmt "" |
|
69 |
in |
|
70 |
fprintf fmt "%a.%t(@[<v>%t%a@])" |
|
71 |
(pp_package_name_with_polymorphic substitution) submachine |
|
72 |
pp_name |
|
73 |
pp_state |
|
74 |
pp_opt pp_args_opt |
|
75 |
|
|
76 | 36 |
(** Printing function for instruction. See |
77 | 37 |
{!type:Machine_code_types.instr_t} for more details on |
78 | 38 |
machine types. |
... | ... | |
85 | 45 |
let rec pp_machine_instr typed_submachines machine fmt instr = |
86 | 46 |
let pp_instr = pp_machine_instr typed_submachines machine in |
87 | 47 |
(* Print args for a step call *) |
48 |
let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in |
|
88 | 49 |
let pp_args vl il fmt = |
89 | 50 |
fprintf fmt "@[%a@]%t@[%a@]" |
90 | 51 |
(Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl |
91 | 52 |
(Utils.pp_final_char_if_non_empty ",@," il) |
92 |
(Utils.fprintf_list ~sep:",@ " (pp_access_var machine)) il
|
|
53 |
(Utils.fprintf_list ~sep:",@ " pp_var_name) il
|
|
93 | 54 |
in |
94 | 55 |
(* Print a when branch of a case *) |
95 | 56 |
let pp_when fmt (cond, instrs) = |
... | ... | |
130 | 91 |
(* no reset *) |
131 | 92 |
| MNoReset _ -> () |
132 | 93 |
(* reset *) |
133 |
| MReset i -> |
|
94 |
| MReset i when List.mem_assoc i typed_submachines -> |
|
95 |
let (substitution, submachine) = get_instance i typed_submachines in |
|
134 | 96 |
pp_package_call |
135 |
typed_submachines |
|
136 | 97 |
pp_reset_procedure_name |
137 | 98 |
fmt |
138 |
(i, None) |
|
99 |
(substitution, submachine, pp_state i, None)
|
|
139 | 100 |
| MLocalAssign (ident, value) -> |
140 | 101 |
pp_basic_assign machine fmt ident value |
141 | 102 |
| MStateAssign (ident, value) -> |
... | ... | |
144 | 105 |
let value = mk_val (Fun (i, vl)) i0.var_type in |
145 | 106 |
pp_basic_assign machine fmt i0 value |
146 | 107 |
| MStep (il, i, vl) when List.mem_assoc i typed_submachines -> |
108 |
let (substitution, submachine) = get_instance i typed_submachines in |
|
147 | 109 |
pp_package_call |
148 |
typed_submachines |
|
149 | 110 |
pp_step_procedure_name |
150 | 111 |
fmt |
151 |
(i, Some (pp_args vl il)) |
|
112 |
(substitution, submachine, pp_state i, Some (pp_args vl il))
|
|
152 | 113 |
| MBranch (_, []) -> assert false |
153 | 114 |
| MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true -> |
154 | 115 |
let neg = c1=tag_false in |
Also available in: Unified diff
Ada: Correct ada main to handle statelles top level node