module Environment:APRON Environments binding dimensions to names`sig`

..`end`

`type `

typvar =

`|` |
`INT` |

`|` |
`REAL` |

`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