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

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