1	import Base
2	import ../../../src/containers/dynamic_array.bend as A
3	import ../../../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	
8	def new_length(~T: Type) -> {A.length_owned(~T, A.new_owned(~T)) == (A.new_owned(~T), 0n) : A.DynArray<T> & Nat}:
9	  {==}
10	
11	def new_capacity(~T: Type) -> {A.capacity_owned(~T, A.new_owned(~T)) == (A.new_owned(~T), 1n) : A.DynArray<T> & Nat}:
12	  {==}
13	
14	def 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	
17	def 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	
20	def 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	
23	def 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.
27	def 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	
30	def 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	
33	def 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	
36	def 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	
39	def 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	
42	def 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	  {==}