src/containers/types/dynamic_array.bend

bend-collections-laws-containers@1.0.0.0 · 31 lines · 0 definitions

1import Base
2
3# Neutral datatypes shared by src/dynamic_array.bend and spec/dynamic_array.bend.
4
5type Error is Data:
6  IndexOutOfRange{}
7  EmptyArray{}
8  CapacityExceeded{}
9
10# One public operation, for arbitrary finite operation traces.
11type Op<-T: Data> is Data:
12  Length{}
13  Capacity{}
14  Get{index: Nat}
15  Set{index: Nat, value: T}
16  Push{value: T}
17  Pop{}
18  Reserve{wanted: Nat}
19  Clear{}
20  ToList{}
21
22# The observable answer of one operation.
23type Obs<-T: Data> is Data:
24  ONat{value: Nat}
25  OItem{result: Result<&2, &2, Error, T>}
26  OUnit{result: Result<&2, &2, Error, Unit>}
27  OList{items: List<&2, T>}
28
29# A rejected owning write returns its input value to the caller.
30type Rejected<-T: Type> is Type:
31  Rejected{error: Error, value: T}