Revision 768f60f0
Added by Christophe Garion over 4 years ago
src/backends/Ada/ada_backend_adb.ml | ||
---|---|---|
15 | 15 |
open Lustre_types |
16 | 16 |
open Corelang |
17 | 17 |
open Machine_code_common |
18 |
|
|
19 | 18 |
open Ada_backend_common |
20 | 19 |
|
20 |
(** Main module for generating packages bodies |
|
21 |
**) |
|
21 | 22 |
module Main = |
22 | 23 |
struct |
23 | 24 |
|
24 |
let pp_machine_instr machine fmt instr = |
|
25 |
fprintf fmt "NULL" |
|
25 |
(* Printing functions for basic operations *) |
|
26 |
|
|
27 |
(** Printing function for expressions [v1 modulo v2]. Depends |
|
28 |
on option [integer_div_euclidean] to choose between mathematical |
|
29 |
modulo or remainder ([rem] in Ada). |
|
30 |
|
|
31 |
@param pp_val pretty printer for values |
|
32 |
@param v1 the first value in the expression |
|
33 |
@param v2 the second value in the expression |
|
34 |
@param fmt the formater to print on |
|
35 |
**) |
|
36 |
let pp_mod pp_val v1 v2 fmt = |
|
37 |
if !Options.integer_div_euclidean then |
|
38 |
(* (a rem b) + (a rem b < 0 ? abs(b) : 0) *) |
|
39 |
Format.fprintf fmt |
|
40 |
"((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))" |
|
41 |
pp_val v1 pp_val v2 |
|
42 |
pp_val v1 pp_val v2 |
|
43 |
pp_val v2 |
|
44 |
else (* Ada behavior for rem *) |
|
45 |
Format.fprintf fmt "(%a rem %a)" pp_val v1 pp_val v2 |
|
46 |
|
|
47 |
(** Printing function for expressions [v1 div v2]. Depends on |
|
48 |
option [integer_div_euclidean] to choose between mathematic |
|
49 |
division or Ada division. |
|
50 |
|
|
51 |
@param pp_val pretty printer for values |
|
52 |
@param v1 the first value in the expression |
|
53 |
@param v2 the second value in the expression |
|
54 |
@param fmt the formater to print in |
|
55 |
**) |
|
56 |
let pp_div pp_val v1 v2 fmt = |
|
57 |
if !Options.integer_div_euclidean then |
|
58 |
(* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *) |
|
59 |
Format.fprintf fmt "(%a - %t) / %a" |
|
60 |
pp_val v1 |
|
61 |
(pp_mod pp_val v1 v2) |
|
62 |
pp_val v2 |
|
63 |
else (* Ada behovior for / *) |
|
64 |
Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2 |
|
65 |
|
|
66 |
(** Printing function for basic lib functions. |
|
67 |
|
|
68 |
@param is_int boolean to choose between integer |
|
69 |
division (resp. remainder) or Ada division |
|
70 |
(resp. remainder) |
|
71 |
@param i a string representing the function |
|
72 |
@param pp_val the pretty printer for values |
|
73 |
@param fmt the formater to print on |
|
74 |
@param vl the list of operands |
|
75 |
**) |
|
76 |
let pp_basic_lib_fun is_int i pp_val fmt vl = |
|
77 |
match i, vl with |
|
78 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
|
79 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v |
|
80 |
| "impl", [v1; v2] -> Format.fprintf fmt "(not %a or else %a)" pp_val v1 pp_val v2 |
|
81 |
| "=", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 |
|
82 |
| "mod", [v1; v2] -> |
|
83 |
if is_int then |
|
84 |
pp_mod pp_val v1 v2 fmt |
|
85 |
else |
|
86 |
Format.fprintf fmt "(%a rem %a)" pp_val v1 pp_val v2 |
|
87 |
| "equi", [v1; v2] -> Format.fprintf fmt "((not %a) = (not %a))" pp_val v1 pp_val v2 |
|
88 |
| "xor", [v1; v2] -> Format.fprintf fmt "((not %a) \\= (not %a))" pp_val v1 pp_val v2 |
|
89 |
| "/", [v1; v2] -> |
|
90 |
if is_int then |
|
91 |
pp_div pp_val v1 v2 fmt |
|
92 |
else |
|
93 |
Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2 |
|
94 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
|
95 |
| _ -> (Format.eprintf "internal compilation error: basic function %s@." i; assert false) |
|
96 |
|
|
97 |
(** Printing function for basic assignement [var_name := value;]. |
|
98 |
|
|
99 |
@param pp_var pretty printer for variables |
|
100 |
@param fmt the formater to print on |
|
101 |
@param var_name the name of the variable |
|
102 |
@param value the value to be assigned |
|
103 |
**) |
|
104 |
let pp_basic_assign pp_var fmt var_name value = |
|
105 |
fprintf fmt "%a := %a;" |
|
106 |
pp_var var_name |
|
107 |
pp_var value |
|
108 |
|
|
109 |
(** Printing function for assignement. For the moment, only use |
|
110 |
[pp_basic_assign] function. |
|
111 |
|
|
112 |
@param pp_var pretty printer for variables |
|
113 |
@param fmt the formater to print on |
|
114 |
@param var_name the name of the variable |
|
115 |
@param value the value to be assigned |
|
116 |
**) |
|
117 |
let pp_assign pp_var fmt var_name value = pp_basic_assign |
|
118 |
|
|
119 |
(** Printing function for instruction. See |
|
120 |
{!type:Machine_code_types.instr_t} for more details on |
|
121 |
machine types. |
|
122 |
|
|
123 |
@param machine the current machine |
|
124 |
@param fmt the formater to print on |
|
125 |
@param instr the instruction to print |
|
126 |
**) |
|
127 |
let pp_machine_instr machine fmt instr = |
|
128 |
match get_instr_desc instr with |
|
129 |
(* no reset *) |
|
130 |
| MNoReset _ -> () |
|
131 |
(* reset *) |
|
132 |
| MReset i -> |
|
133 |
(* pp_machine_reset m self fmt i *) |
|
134 |
fprintf fmt "MReset %s@ " i |
|
135 |
| MLocalAssign (i,v) -> |
|
136 |
fprintf fmt "MLocalAssign"; |
|
137 |
(* pp_assign |
|
138 |
* machine self (pp_c_var_read m) fmt |
|
139 |
* i.var_type (mk_val (Var i) i.var_type) v *) |
|
140 |
| MStateAssign (i,v) -> |
|
141 |
fprintf fmt "MStateAssign" |
|
142 |
(* pp_assign |
|
143 |
* m self (pp_c_var_read m) fmt |
|
144 |
* i.var_type (mk_val (Var i) i.var_type) v *) |
|
145 |
| MStep ([i0], i, vl) when Basic_library.is_value_internal_fun |
|
146 |
(mk_val (Fun (i, vl)) i0.var_type) -> |
|
147 |
fprintf fmt "MStep basic" |
|
148 |
(* pp_machine_instr dependencies m self fmt |
|
149 |
* (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))) *) |
|
150 |
| MStep (il, i, vl) -> fprintf fmt "MStep" |
|
151 |
|
|
152 |
(* pp_basic_instance_call m self fmt i vl il *) |
|
153 |
| MBranch (_, []) -> fprintf fmt "MBranch []" |
|
154 |
|
|
155 |
(* (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false) *) |
|
156 |
| MBranch (g, hl) -> fprintf fmt "MBranch gen" |
|
157 |
(* if let t = fst (List.hd hl) in t = tag_true || t = tag_false |
|
158 |
* then (\* boolean case, needs special treatment in C because truth value is not unique *\) |
|
159 |
* (\* may disappear if we optimize code by replacing last branch test with default *\) |
|
160 |
* let tl = try List.assoc tag_true hl with Not_found -> [] in |
|
161 |
* let el = try List.assoc tag_false hl with Not_found -> [] in |
|
162 |
* pp_conditional dependencies m self fmt g tl el |
|
163 |
* else (\* enum type case *\) |
|
164 |
* (\*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*\) |
|
165 |
* fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]" |
|
166 |
* (pp_c_val m self (pp_c_var_read m)) g |
|
167 |
* (Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl *) |
|
168 |
| MComment s -> |
|
169 |
fprintf fmt "-- %s@ " s |
|
170 |
| _ -> fprintf fmt "Don't know" |
|
171 |
|
|
26 | 172 |
|
27 | 173 |
(** Keep only the MReset from an instruction list. |
28 | 174 |
@param list to filter |
29 | 175 |
**) |
30 | 176 |
let filter_reset instr_list = List.map |
31 |
(fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) |
|
177 |
(fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false)
|
|
32 | 178 |
instr_list |
33 | 179 |
|
34 | 180 |
(** Print the definition of the init procedure from a machine. |
... | ... | |
93 | 239 |
pp_end_package machine (*End the package*) |
94 | 240 |
|
95 | 241 |
end |
242 |
|
|
243 |
(* Local Variables: *) |
|
244 |
(* compile-command: "make -C ../../.." *) |
|
245 |
(* End: *) |
Also available in: Unified diff
Ada: first pretty printing functions for adb