Wp.Matrix
val of_dims : int option list -> t
val pretty : Stdlib.Format.formatter -> t -> unit
val pp_suffix_id : Stdlib.Format.formatter -> t -> unit
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_dims : int option list -> Lang.F.term list
Value of size variables