diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml index a4beb75b6..f47a09ef9 100644 --- a/sledge/src/llair/global.ml +++ b/sledge/src/llair/global.ml @@ -7,4 +7,31 @@ (** Global variables *) -include Exp.Global +type t = {var: Var.t; init: Exp.t option; siz: int; typ: Typ.t; loc: Loc.t} +[@@deriving compare, hash, sexp] + +let equal = [%compare.equal: t] + +let pp fs {var} = + let name = Var.name var in + let pf pp = + Format.pp_open_box fs 2 ; + Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp + in + pf "@%s%t" name (fun fs -> + let demangled = Llvm.demangle name in + if not (String.is_empty demangled || String.equal name demangled) then + Format.fprintf fs "ā€œ%sā€" demangled ) + +let pp_defn fs {var; init; typ} = + Format.fprintf fs "@[<2>%a %a%a@]" Typ.pp typ Var.pp var + (Option.pp " =@ @[%a@]" Exp.pp) + init + +let invariant g = + Invariant.invariant [%here] g [%sexp_of: t] + @@ fun () -> + let {typ} = g in + assert (Typ.is_sized typ) + +let mk ?init var siz typ loc = {var; init; siz; typ; loc} |> check invariant diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/global.mli index 24e923f84..5e91b5632 100644 --- a/sledge/src/llair/global.mli +++ b/sledge/src/llair/global.mli @@ -7,4 +7,14 @@ (** Global variables *) -include module type of Exp.Global +type t = private + {var: Var.t; init: Exp.t option; siz: int; typ: Typ.t; loc: Loc.t} +[@@deriving compare, hash, sexp] + +val equal : t -> t -> bool +val pp : t pp +val pp_defn : t pp + +include Invariant.S with type t := t + +val mk : ?init:Exp.t -> Var.t -> int -> Typ.t -> Loc.t -> t