path: root/abstract/environment_domain.ml

open Abstract_syntax_tree

module type ENVIRONMENT_DOMAIN = sig
    type t

    (* construction *)
    val init    : t
    val bottom  : t
    val is_bot  : t -> bool

    (* variable management *)
    val addvar  : t -> id -> t
    val rmvar   : t -> id -> t
    val vars    : t -> id list

    (* abstract operation *)
    val assign  : t -> id -> expr ext -> t      (*    S[id <- expr]     *)
    val compare_leq : t -> expr ext -> expr ext -> t    (*    S[expr <= expr ?] *)
    val compare_eq : t -> expr ext -> expr ext -> t    (*    S[expr = expr ?] *)

    (* set-theoretic operations *)
    val join    : t -> t -> t       (* union *)
    val meet    : t -> t -> t       (* intersection *)
    val widen   : t -> t -> t

    (* order *)
    val subset  : t -> t -> bool
    val eq      : t -> t -> bool

    (* pretty-printing *)
    val var_str : t -> id list -> string
end