Project

General

Profile

« Previous | Next » 

Revision 66359a5e

Added by Pierre-Loïc Garoche about 7 years ago

[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

View differences:

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