Module Dim

module Dim: sig .. end

APRON Dimensions and related types

type t = int

type change = {

	`dim : int array;`
	`intdim : int;`
	`realdim : int;`

}

type change2 = {

	`add : change option;`
	`remove : change option;`

}

type perm = int array

type dimension = {

	`intd : int;`
	`reald : int;`

}
APRON Dimensions and related types

t=int is the type of dimensions.
The semantics of an object (change:change) is the following one:
- change.intdim and change.realdim indicate the number of integer and real dimensions to add or to remove
- In case of the addition of dimensions,
  change.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.
- In case of the removal of dimensions,
  dimchange.dimi=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.
The semantics of an object (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 -> unit

Assuming a transformation for add_dimensions, invert it in-place to obtain the inverse transformation using remove_dimensions

val perm_compose : perm -> perm -> perm

perm_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 -> perm

Invert a permutation