Module Wp.Matrix

type t

Matrix dimensions. Encodes the number of dimensions and their kind

val of_dims : int option list -> t
val compare : t -> t -> int
val pretty : Stdlib.Format.formatter -> t -> unit
val pp_suffix_id : Stdlib.Format.formatter -> t -> unit
val merge : int option list -> int option list -> int option list option
type env = {
  1. size_var : Lang.F.var list;
    (*

    size variables

    *)
  2. size_val : Lang.F.term list;
    (*

    size values

    *)
  3. index_var : Lang.F.var list;
    (*

    index variables

    *)
  4. index_val : Lang.F.term list;
    (*

    index values

    *)
  5. index_range : Lang.F.pred list;
    (*

    indices are in range of size variables

    *)
  6. index_offset : Lang.F.term list;
    (*

    polynomial of indices

    *)
  7. length : Lang.F.term option;
    (*

    number of cells (None is infinite)

    *)
}
val cc_tau : Lang.F.tau -> t -> Lang.F.tau

Type of matrix

val cc_env : t -> env

Dimension environment

val cc_dims : int option list -> Lang.F.term list

Value of size variables