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 = {
size_var : Lang.F.var list;(*

size variables

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

size values

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

index variables

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

index values

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

indices are in range of size variables

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

polynomial of indices

*)
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