module Environment: sig
.. end
APRON Environments binding dimensions to names
type
typvar =
type
t
APRON Environments binding dimensions to names
val make : Var.t array -> Var.t array -> t
Making an environment from a set of integer and real variables. Raise Failure
in case of name conflict.
val add : t -> Var.t array -> Var.t array -> t
Adding to an environment a set of integer and real variables. Raise Failure
in case of name conflict.
val remove : t -> Var.t array -> t
Remove from an environment a set of variables. Raise Failure
in case of non-existing variables.
val rename : t -> Var.t array -> Var.t array -> t
Renaming in an environment a set of variables. Raise Failure
in case of interferences with the variables that are not renamed.
val rename_perm : t -> Var.t array -> Var.t array -> t * Dim.perm
Similar to previous function, but returns also
the permutation on dimensions induced by the renaming.
val lce : t -> t -> t
Compute the least common environment of 2 environment,
that is, the environment composed of all the variables
of the 2 environments.
Raise Failure
if the same variable has different types
in the 2 environment.
val lce_change : t ->
t -> t * Dim.change option * Dim.change option
Similar to the previous function, but returns also the transformations
required to convert from e1
(resp. e2
)
to the lce. If None
is returned, this means
that e1
(resp. e2
) is identic to the lce.
val dimchange : t -> t -> Dim.change
dimchange e1 e2
computes the transformation for
converting from an environment e1
to a superenvironment
e2
. Raises Failure
if e2
is not a superenvironment.
val dimchange2 : t -> t -> Dim.change2
dimchange2 e1 e2
computes the transformation for
converting from an environment e1
to a (compatible) environment
e2
, by first adding (some) variables of e2
and then removing
(some) variables of e1
. Raises Failure
if the two environments
are incompatible.
val equal : t -> t -> bool
Test equality if two environments
val compare : t -> t -> int
Compare two environment. compare env1 env2
return -2
if the environements are not compatible (a variable has different types in the 2 environements), -1
if env1
is a subset of env2, 0
if equality, +1
if env1 is a superset of env2, and +2
otherwise (the lce exists and is a strict superset of both)
val hash : t -> int
Hashing function for environments
val dimension : t -> Dim.dimension
Return the dimension of the environment
val size : t -> int
Return the size of the environment
val mem_var : t -> Var.t -> bool
Return true if the variable is present in the environment.
val typ_of_var : t -> Var.t -> typvar
Return the type of variables in the environment. If the variable does not belong to the environment, raise a Failure
exception.
val vars : t -> Var.t array * Var.t array
Return the (lexicographically ordered) sets of integer and real variables in the environment
val var_of_dim : t -> Dim.t -> Var.t
Return the variable corresponding to the given dimension in the environment. Raise Failure
is the dimension is out of the range of the environment (greater than or equal to dim env
)
val dim_of_var : t -> Var.t -> Dim.t
Return the dimension associated to the given variable in the environment. Raise Failure
if the variable does not belong to the environment.
val print : ?first:(unit, Format.formatter, unit) Pervasives.format ->
?sep:(unit, Format.formatter, unit) Pervasives.format ->
?last:(unit, Format.formatter, unit) Pervasives.format ->
Format.formatter -> t -> unit
Printing