Revision 09d7b39f
Added by Guillaume DAVY about 4 years ago
| src/backends/Ada/ada_backend_adb.ml | ||
|---|---|---|
| 50 | 50 |
@param machine a machine |
| 51 | 51 |
@return the instance of machine.minstances corresponding to identifier |
| 52 | 52 |
**) |
| 53 |
let get_instance identifier typed_instances =
|
|
| 53 |
let get_instance identifier typed_submachines =
|
|
| 54 | 54 |
try |
| 55 |
List.assoc identifier typed_instances
|
|
| 55 |
List.assoc identifier typed_submachines
|
|
| 56 | 56 |
with Not_found -> assert false |
| 57 | 57 |
|
| 58 |
(** Printing the reset function. call
|
|
| 58 |
(** Printing a call to a package function
|
|
| 59 | 59 |
|
| 60 |
@param typed_instances list of all typed machine instances of this machine |
|
| 61 |
@param machine the current machine |
|
| 62 |
@param instance the considered instance |
|
| 60 |
@param typed_submachines list of all typed machine instances of this machine |
|
| 61 |
@param pp_name printer for the function name |
|
| 63 | 62 |
@param fmt the formater to use |
| 63 |
@param identifier the instance identifier |
|
| 64 |
@param pp_args_opt optional printer for other arguments |
|
| 64 | 65 |
**) |
| 65 |
let pp_machine_reset typed_instances (machine: machine_t) fmt identifier = |
|
| 66 |
let (substitution, submachine) = get_instance identifier typed_instances in |
|
| 67 |
fprintf fmt "%a.%t(%t.%s)" |
|
| 66 |
let pp_package_call typed_submachines pp_name fmt (identifier, pp_args_opt) = |
|
| 67 |
let (substitution, submachine) = get_instance identifier typed_submachines in |
|
| 68 |
let statefull = is_machine_statefull submachine in |
|
| 69 |
let pp_opt fmt = function |
|
| 70 |
| Some pp_args when statefull -> fprintf fmt ",@,%t" pp_args |
|
| 71 |
| Some pp_args -> pp_args fmt |
|
| 72 |
| None -> fprintf fmt "" |
|
| 73 |
in |
|
| 74 |
let pp_state fmt = |
|
| 75 |
if statefull then |
|
| 76 |
fprintf fmt "%t.%s" pp_state_name identifier |
|
| 77 |
else |
|
| 78 |
fprintf fmt "" |
|
| 79 |
in |
|
| 80 |
fprintf fmt "%a.%t(@[<v>%t%a@])" |
|
| 68 | 81 |
(pp_package_name_with_polymorphic substitution) submachine |
| 69 |
pp_reset_procedure_name
|
|
| 70 |
pp_state_name
|
|
| 71 |
identifier
|
|
| 82 |
pp_name |
|
| 83 |
pp_state |
|
| 84 |
pp_opt pp_args_opt
|
|
| 72 | 85 |
|
| 73 | 86 |
(** Printing function for instruction. See |
| 74 | 87 |
{!type:Machine_code_types.instr_t} for more details on
|
| 75 | 88 |
machine types. |
| 76 | 89 |
|
| 77 |
@param typed_instances list of all typed machine instances of this machine
|
|
| 90 |
@param typed_submachines list of all typed machine instances of this machine
|
|
| 78 | 91 |
@param machine the current machine |
| 79 | 92 |
@param fmt the formater to print on |
| 80 | 93 |
@param instr the instruction to print |
| 81 | 94 |
**) |
| 82 |
let pp_machine_instr typed_instances machine fmt instr =
|
|
| 95 |
let pp_machine_instr typed_submachines machine fmt instr =
|
|
| 83 | 96 |
match get_instr_desc instr with |
| 84 | 97 |
(* no reset *) |
| 85 | 98 |
| MNoReset _ -> () |
| 86 | 99 |
(* reset *) |
| 87 |
| MReset ident ->
|
|
| 88 |
pp_machine_reset typed_instances machine fmt ident
|
|
| 100 |
| MReset i -> |
|
| 101 |
pp_package_call typed_submachines pp_reset_procedure_name fmt (i, None)
|
|
| 89 | 102 |
| MLocalAssign (ident, value) -> |
| 90 | 103 |
pp_basic_assign machine fmt ident value |
| 91 | 104 |
| MStateAssign (ident, value) -> |
| 92 | 105 |
pp_basic_assign machine fmt ident value |
| 93 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i |
|
| 94 |
(List.map (fun v -> v.value_type) vl) -> |
|
| 106 |
| MStep ([i0], i, vl) when is_builtin_fun i -> |
|
| 95 | 107 |
let value = mk_val (Fun (i, vl)) i0.var_type in |
| 96 | 108 |
pp_basic_assign machine fmt i0 value |
| 97 |
| MStep (il, i, vl) -> fprintf fmt "Null" |
|
| 98 |
(* pp_basic_instance_call m self fmt i vl il *) |
|
| 109 |
| MStep (il, i, vl) when List.mem_assoc i typed_submachines -> |
|
| 110 |
let pp_args fmt = fprintf fmt "@[%a@]%t@[%a@]" |
|
| 111 |
(Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl |
|
| 112 |
(Utils.pp_final_char_if_non_empty ",@," il) |
|
| 113 |
(Utils.fprintf_list ~sep:",@ " (pp_access_var machine)) il |
|
| 114 |
in |
|
| 115 |
pp_package_call typed_submachines pp_step_procedure_name fmt (i, Some pp_args) |
|
| 99 | 116 |
| MBranch (_, []) -> fprintf fmt "Null" |
| 100 | 117 |
|
| 101 | 118 |
(* (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false) *) |
| ... | ... | |
| 114 | 131 |
| MComment s -> |
| 115 | 132 |
let lines = String.split_on_char '\n' s in |
| 116 | 133 |
fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines |
| 134 |
| _ -> assert false |
|
| 117 | 135 |
|
| 118 | 136 |
(** Print the definition of the step procedure from a machine. |
| 119 | 137 |
|
| 120 |
@param typed_instances list of all typed machine instances of this machine
|
|
| 138 |
@param typed_submachines list of all typed machine instances of this machine
|
|
| 121 | 139 |
@param fmt the formater to print on |
| 122 | 140 |
@param machine the machine |
| 123 | 141 |
**) |
| 124 |
let pp_step_definition typed_instances fmt m = pp_procedure_definition
|
|
| 142 |
let pp_step_definition typed_submachines fmt m = pp_procedure_definition
|
|
| 125 | 143 |
pp_step_procedure_name |
| 126 | 144 |
(pp_step_prototype m) |
| 127 | 145 |
(pp_machine_var_decl NoMode) |
| 128 |
(pp_machine_instr typed_instances m)
|
|
| 146 |
(pp_machine_instr typed_submachines m)
|
|
| 129 | 147 |
fmt |
| 130 | 148 |
(m.mstep.step_locals, m.mstep.step_instrs) |
| 131 | 149 |
|
| 132 | 150 |
(** Print the definition of the reset procedure from a machine. |
| 133 | 151 |
|
| 134 |
@param typed_instances list of all typed machine instances of this machine
|
|
| 152 |
@param typed_submachines list of all typed machine instances of this machine
|
|
| 135 | 153 |
@param fmt the formater to print on |
| 136 | 154 |
@param machine the machine |
| 137 | 155 |
**) |
| 138 |
let pp_reset_definition typed_instances fmt m = pp_procedure_definition
|
|
| 156 |
let pp_reset_definition typed_submachines fmt m = pp_procedure_definition
|
|
| 139 | 157 |
pp_reset_procedure_name |
| 140 | 158 |
(pp_reset_prototype m) |
| 141 | 159 |
(pp_machine_var_decl NoMode) |
| 142 |
(pp_machine_instr typed_instances m)
|
|
| 160 |
(pp_machine_instr typed_submachines m)
|
|
| 143 | 161 |
fmt |
| 144 | 162 |
([], m.minit) |
| 145 | 163 |
|
| ... | ... | |
| 150 | 168 |
the machine associated to the instance and substitution the instanciation of |
| 151 | 169 |
all its polymorphic types. |
| 152 | 170 |
@param fmt the formater to print on |
| 153 |
@param typed_instances list of all typed machine instances of this machine
|
|
| 171 |
@param typed_submachines list of all typed machine instances of this machine
|
|
| 154 | 172 |
@param m the machine |
| 155 | 173 |
**) |
| 156 |
let pp_file fmt (typed_instances, machine) = |
|
| 157 |
fprintf fmt "%a@, @[<v>@,%a;@,@,%a;@,@]@,%a;@." |
|
| 158 |
(pp_begin_package true) machine (*Begin the package*) |
|
| 159 |
(pp_reset_definition typed_instances) machine (*Define the reset procedure*) |
|
| 160 |
(pp_step_definition typed_instances) machine (*Define the step procedure*) |
|
| 161 |
pp_end_package machine (*End the package*) |
|
| 174 |
let pp_file fmt (typed_submachines, machine) = |
|
| 175 |
let pp_reset fmt = |
|
| 176 |
if is_machine_statefull machine then |
|
| 177 |
fprintf fmt "%a;@,@," (pp_reset_definition typed_submachines) machine |
|
| 178 |
else |
|
| 179 |
fprintf fmt "" |
|
| 180 |
in |
|
| 181 |
let aux pkgs (id, _) = |
|
| 182 |
try |
|
| 183 |
let (pkg, _) = List.assoc id ada_supported_funs in |
|
| 184 |
if List.mem pkg pkgs then |
|
| 185 |
pkgs |
|
| 186 |
else |
|
| 187 |
pkg::pkgs |
|
| 188 |
with Not_found -> pkgs |
|
| 189 |
in |
|
| 190 |
let packages = List.fold_left aux [] machine.mcalls in |
|
| 191 |
fprintf fmt "%a%t%a@, @[<v>@,%t%a;@,@]@,%a;@." |
|
| 192 |
|
|
| 193 |
(* Include all the required packages*) |
|
| 194 |
(Utils.fprintf_list ~sep:";@," pp_with) packages |
|
| 195 |
(Utils.pp_final_char_if_non_empty ";@,@," packages) |
|
| 196 |
|
|
| 197 |
(*Begin the package*) |
|
| 198 |
(pp_begin_package true) machine |
|
| 199 |
|
|
| 200 |
(*Define the reset procedure*) |
|
| 201 |
pp_reset |
|
| 202 |
|
|
| 203 |
(*Define the step procedure*) |
|
| 204 |
(pp_step_definition typed_submachines) machine |
|
| 205 |
|
|
| 206 |
(*End the package*) |
|
| 207 |
pp_end_package machine |
|
| 162 | 208 |
|
| 163 | 209 |
end |
| 164 | 210 |
|
Also available in: Unified diff
Ada: Add generation of step calls and refactor prototypes and ads printing to handle staless
instance.