module Dim:sig..end
typet =int
type
|
dim : |
|
intdim : |
|
realdim : |
type
|
add : |
|
remove : |
typeperm =int array
type
|
intd : |
|
reald : |
APRON Dimensions and related types
t=int is the type of dimensions.(change:change) is the following one:
change.intdim and change.realdim indicate the number of integer and
real dimensions to add or to removechange.dim[i]=k means: add one dimension at dimension k and shift the
already existing dimensions greater than or equal to k one step on the
right (or increment them).
if k is equal to the size of the vector, then it means: add a dimension at
the end.
Repetition are allowed, and means that one inserts more than one dimensions.
Example:
add_dimensions [i0 i1 r0 r1] { dim=[0 1 2 2 4]; intdim=3; realdim=1 }
returns 0 i0 0 i1 0 0 r0 r1 0, considered as a vector with 6 integer
dimensions and 3 real dimensions.i=k means: remove the dimension k and shift the dimensions
greater than k one step on the left (or decrement them).
Repetitions are meaningless (and are not correct specification)
Example: remove_dimensions [i0 i1 i2 r0 r1 r2] { dim=[0 2 4]; intdim=2;
realdim=1 } returns i1 r0 r2, considered as a vector with 1 integer
dimensions and 2 real dimensions.
(change2:change2) is the combination of the
two following transformations:
change2.add indicates an optional addition of dimensions.change2.remove indicates an optional removal of dimensions.perm defines a permutation.dimension defines the dimensionality of an abstract value (number of
integer and real dimensions).
val change_add_invert : change -> unitAssuming a transformation for add_dimensions, invert it in-place to obtain the inverse transformation using remove_dimensions
val perm_compose : perm -> perm -> permperm_compose perm1 perm2 composes the 2 permutations perm1 and perm2
(in this order). The sizes of permutations are supposed to be equal.
val perm_invert : perm -> permInvert a permutation