blob: f5614fee76a34d4c392597958391fdb777e1fd16 (
plain) (
tree)
|
|
open Abstract_syntax_tree
module type ENVIRONMENT_DOMAIN = sig
type t
(* construction *)
val init : t
val bottom : t
(* variable management *)
val addvar : t -> id -> t
val rmvar : t -> id -> t
(* abstract operation *)
val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
val compare : 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
end
|