proofs/containers/dynamic_array/owned.bend
bend-collections-laws-containers@1.0.0.0 · 43 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as A
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
4
5# Owning storage laws quantify over Type, not just Data. They do not copy
6# elements at runtime: repeated terms occur only in erased equality types.
7
8def new_length(~T: Type) -> {A.length_owned(~T, A.new_owned(~T)) == (A.new_owned(~T), 0n) : A.DynArray<T> & Nat}:
9 {==}
10
11def new_capacity(~T: Type) -> {A.capacity_owned(~T, A.new_owned(~T)) == (A.new_owned(~T), 1n) : A.DynArray<T> & Nat}:
12 {==}
13
14def empty_pop(~T: Type, l: Nat, d: Nat, c: Nat, a: Array<Maybe<T>>) -> {A.pop_owned(~T, A.DA{l, d, c, 0n, a}) == (A.DA{l, d, c, 0n, a}, Fail{E.EmptyArray{}}) : A.DynArray<T> & Result<&2, &1, E.Error, T>}:
15 {==}
16
17def swap_rejected(~T: Type, l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<T>>, i: Nat, v: T) -> {A.swap_checked_owned(~T, l, d, c, n, a, i, v, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.IndexOutOfRange{}, v}}) : A.DynArray<T> & Result<&1, &1, E.Rejected<T>, Maybe<T>>}:
18 {==}
19
20def push_rejected(~T: Type, l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<T>>, v: T) -> {A.push_room_owned(~T, l, d, c, n, a, v, False{}, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.CapacityExceeded{}, v}}) : A.DynArray<T> & Result<&1, &2, E.Rejected<T>, Unit>}:
21 {==}
22
23def update_rejected(~T: Type, ~R: Type, l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<T>>, i: Nat, f: T -> T & R) -> {A.update_checked_owned(~T, ~R, l, d, c, n, a, i, f, False{}) == (A.DA{l, d, c, n, a}, Fail{E.IndexOutOfRange{}}) : A.DynArray<T> & Result<&2, &1, E.Error, R>}:
24 {==}
25
26# A real public push/pop roundtrip with an arbitrary owning payload.
27def first_push_pop(~T: Type, x: T) -> {A.pop_owned(~T, Pair.fst(A.DynArray<T>, Result<&1, &2, E.Rejected<T>, Unit>, A.push_owned(~T, A.new_owned(~T), x))) == (A.new_owned(~T), Done{x}) : A.DynArray<T> & Result<&2, &1, E.Error, T>}:
28 {==}
29
30def first_swap(~T: Type, x: T, y: T) -> {A.swap_owned(~T, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, y) == (A.DA{31n, 0n, 1n, 1n, ALeaf{Some{y}}}, Done{Some{x}}) : A.DynArray<T> & Result<&1, &1, E.Rejected<T>, Maybe<T>>}:
31 {==}
32
33def first_update(~T: Type, ~R: Type, x: T, f: T -> T & R) -> {A.update_owned(~T, ~R, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, f) == A.update_put_owned(~T, ~R, 31n, 0n, 1n, 1n, ALeaf{None{}}, 0n, f(x)) : A.DynArray<T> & Result<&2, &1, E.Error, R>}:
34 {==}
35
36def clear_length(~T: Type, l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<T>>) -> {A.length_owned(~T, A.clear_owned(~T, A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~T, d)}, 0n) : A.DynArray<T> & Nat}:
37 {==}
38
39def clear_capacity(~T: Type, l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<T>>) -> {A.capacity_owned(~T, A.clear_owned(~T, A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~T, d)}, c) : A.DynArray<T> & Nat}:
40 {==}
41
42def first_drain(~T: Type, x: T) -> {A.into_list_owned(~T, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}) == Con{x, Nil{}} : List<T>}:
43 {==}