Array

Flat, contiguous, native-backed sequence with random access. ``Array`` is an opaque type parameterised by: * its element type ``a``; * an abstract refinement ``p`` (Liquid Haskell-style ``data Array a <p>``) that every element of the array satisfies. The underlying storage is a Python list, so operations are O(1) for indexed access and O(n) for prepend.
Table of Contents

Types

Array

(type)
Flat, contiguous, native-backed sequence with random access. ``Array`` is an opaque type parameterised by: * its element type ``a``; * an abstract refinement ``p`` (Liquid Haskell-style ``data Array a <p>``) that every element of the array satisfies. The underlying storage is a Python list, so operations are O(1) for indexed access and O(n) for prepend.
type Array a forall <p:(_ : a) -> Bool -> Bool>

Functions

functools

def functools : Unit

length

Length of the array.
def length (arr: Array a) : {n : Int | n == size arr}

new

Empty array.
def new : {arr : Array a | size arr == 0}

empty

True when the array is empty.
def empty (arr: Array a) : {b : Bool | b == (size arr == 0)}

append

Append an element to the back; the value must satisfy the refinement ``p``.
def append (arr: Array a) (x: {v : a | p v}) : {r : Array a | size r == size arr + 1}

cons

Prepend an element to the front; the value must satisfy the refinement ``p``.
def cons (arr: Array a) (x: {v : a | p v}) : {r : Array a | size r == size arr + 1}

get

Indexed read; the result is known to satisfy ``p``.
def get (arr: Array a) (i: {n : Int | n >= 0 && n < size arr}) : {v : a | p v}

set

Indexed write; preserves length, and the written value must satisfy ``p``.
def set (arr: Array a) (i: {n : Int | n >= 0 && n < size arr}) (x: {v : a | p v}) : {r : Array a | size r == size arr}

head

First element of a non-empty array.
def head (arr: {arr : Array a | size arr > 0}) : {v : a | p v}

reversed

Reversed copy; length is preserved.
def reversed (arr: Array a) : {r : Array a | size r == size arr}

map

Map a function across the array; length is preserved and the result refinement ``q`` is pushed through ``f``.
def map (f: (x : {v : a | p v}) -> {w : b | q w}) (arr: Array a) : {r : Array b | size r == size arr}

filter

Filter an array by ``f``; the length never grows.
def filter (f: (x : {v : a | p v}) -> Bool) (arr: Array a) : {r : Array a | size r <= size arr}

reduce

Right fold: ``reduce f z [x1, ..., xn] == f x1 (f x2 (... (f xn z)))``.
def reduce (f: (x : {v : a | p v}) -> (acc : b) -> b) (z: b) (arr: Array a) : b

sum

Sum of an Int array.
def sum (arr: Array Int) : Int

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

size

uninterpreted
Abstract length measure.
def size : (arr : Array a) -> Int