Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
src/backends/Horn/horn_backend_common.ml | ||
---|---|---|
19 | 19 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id |
20 | 20 |
|
21 | 21 |
let rec pp_type fmt t = |
22 |
if Types.is_bool_type t then fprintf fmt "Bool" else |
|
23 |
if Types.is_int_type t then fprintf fmt "Int" else |
|
24 |
if Types.is_real_type t then fprintf fmt "Real" else |
|
22 | 25 |
match (Types.repr t).Types.tdesc with |
23 |
| Types.Tbool -> fprintf fmt "Bool" |
|
24 |
| Types.Tint -> fprintf fmt "Int" |
|
25 |
| Types.Treal -> fprintf fmt "Real" |
|
26 | 26 |
| Types.Tconst ty -> pp_print_string fmt ty |
27 | 27 |
| Types.Tclock t -> pp_type fmt t |
28 | 28 |
| Types.Tarray(dim,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")" |
Also available in: Unified diff
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program