proofs/containers/doubly_linked_list/direct_laws.bend
bend-collections-laws-containers@1.0.0.0 · 133 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
3import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
5import bend-collections-laws-containers@1.0.0.0/src/containers/types/internal_dlist.bend as I
6
7def result_same(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, T>) -> {D.get_result(~T, tag, depth, cap, gens, r) == D.project_value(~T, D.value_result(~T, tag, depth, cap, gens, r)) : D.DList<T> & Result<&2, &2, E.Error, T>}:
8 match r:
9 case Tuple{raw, result}:
10 {==}
11
12def ready_same(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.get_ready(~T, h, r) == D.project_value(~T, D.checked(~T, E.Get{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, T>}:
13 match r:
14 case Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
15 {==}
16 case Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
17 result_same(~T, tag, depth, cap, gens, R.get(~T, raw, D.old_handle(h)))
18
19def get_same(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.get(~T, s, h) == D.project_value(~T, D.step(~T, s, E.Get{h})) : D.DList<T> & Result<&2, &2, E.Error, T>}:
20 ready_same(~T, h, D.validate(~T, s, h))
21
22def get_u32(s: D.DList<U32>, +h: E.Handle) -> {D.get(~U32, s, h) == D.project_value(~U32, D.step(~U32, s, E.Get{h})) : D.DList<U32> & Result<&2, &2, E.Error, U32>}:
23 get_same(~U32, s, h)
24
25def get_string(s: D.DList<String>, +h: E.Handle) -> {D.get(~String, s, h) == D.project_value(~String, D.step(~String, s, E.Get{h})) : D.DList<String> & Result<&2, &2, E.Error, String>}:
26 get_same(~String, s, h)
27
28def set_result_same(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<T> & Result<&2, &2, I.Error, Unit>) -> {D.set_result(~T, tag, depth, cap, gens, r) == D.project_unit(~T, D.unit_result(~T, tag, depth, cap, gens, r)) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:
29 match r:
30 case Tuple{raw, result}:
31 {==}
32
33def set_ready_same(~T: Data, +h: E.Handle, +x: T, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.set_ready(~T, h, x, r) == D.project_unit(~T, D.checked(~T, E.Set{h, x}, r)) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:
34 match r:
35 case Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
36 {==}
37 case Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
38 set_result_same(~T, tag, depth, cap, gens, R.set(~T, raw, D.old_handle(h), x))
39
40def set_same(~T: Data, s: D.DList<T>, +h: E.Handle, +x: T) -> {D.set(~T, s, h, x) == D.project_unit(~T, D.step(~T, s, E.Set{h, x})) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:
41 set_ready_same(~T, h, x, D.validate(~T, s, h))
42
43def set_u32(s: D.DList<U32>, +h: E.Handle, +x: U32) -> {D.set(~U32, s, h, x) == D.project_unit(~U32, D.step(~U32, s, E.Set{h, x})) : D.DList<U32> & Result<&2, &2, E.Error, Unit>}:
44 set_same(~U32, s, h, x)
45
46def set_string(s: D.DList<String>, +h: E.Handle, +x: String) -> {D.set(~String, s, h, x) == D.project_unit(~String, D.step(~String, s, E.Set{h, x})) : D.DList<String> & Result<&2, &2, E.Error, Unit>}:
47 set_same(~String, s, h, x)
48
49def length_result_same(tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<U32> & Nat) -> {D.length_direct_result(~U32, tag, depth, cap, gens, r) == D.project_length(~U32, D.length_result(~U32, tag, depth, cap, gens, r)) : D.DList<U32> & Nat}:
50 match r:
51 case Tuple{raw, x}:
52 {==}
53
54def length_same(s: D.DList<U32>) -> {D.length(~U32, s) == D.project_length(~U32, D.step(~U32, s, E.Length{})) : D.DList<U32> & Nat}:
55 match s:
56 case D.DL{tag, depth, cap, raw, gens}:
57 length_result_same(tag, depth, cap, gens, R.length(~U32, raw))
58
59def to_list_result_same(tag: U32, depth: Nat, cap: U32, gens: Array<U32>, r: R.DList<U32> & List<&2, U32>) -> {D.to_list_direct_result(~U32, tag, depth, cap, gens, r) == D.project_list(~U32, D.list_result(~U32, tag, depth, cap, gens, r)) : D.DList<U32> & List<&2, U32>}:
60 match r:
61 case Tuple{raw, x}:
62 {==}
63
64def to_list_same(s: D.DList<U32>) -> {D.to_list(~U32, s) == D.project_list(~U32, D.step(~U32, s, E.ToList{})) : D.DList<U32> & List<&2, U32>}:
65 match s:
66 case D.DL{tag, depth, cap, raw, gens}:
67 to_list_result_same(tag, depth, cap, gens, R.to_list(~U32, raw))
68
69def next_ready_same(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.next_ready(~T, h, r) == D.project_neighbour(~T, D.checked(~T, E.Next{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
70 match r:
71 case Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
72 {==}
73 case Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
74 {==}
75
76def next_U32(s: D.DList<U32>, +h: E.Handle) -> {D.next(~U32, s, h) == D.project_neighbour(~U32, D.step(~U32, s, E.Next{h})) : D.DList<U32> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
77 next_ready_same(~U32, h, D.validate(~U32, s, h))
78
79def next_String(s: D.DList<String>, +h: E.Handle) -> {D.next(~String, s, h) == D.project_neighbour(~String, D.step(~String, s, E.Next{h})) : D.DList<String> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
80 next_ready_same(~String, h, D.validate(~String, s, h))
81
82def prev_ready_same(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.prev_ready(~T, h, r) == D.project_neighbour(~T, D.checked(~T, E.Prev{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
83 match r:
84 case Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
85 {==}
86 case Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
87 {==}
88
89def prev_U32(s: D.DList<U32>, +h: E.Handle) -> {D.prev(~U32, s, h) == D.project_neighbour(~U32, D.step(~U32, s, E.Prev{h})) : D.DList<U32> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
90 prev_ready_same(~U32, h, D.validate(~U32, s, h))
91
92def prev_String(s: D.DList<String>, +h: E.Handle) -> {D.prev(~String, s, h) == D.project_neighbour(~String, D.step(~String, s, E.Prev{h})) : D.DList<String> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
93 prev_ready_same(~String, h, D.validate(~String, s, h))
94
95def insert_before_ready_same(~T: Data, +h: E.Handle, +x: T, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.insert_before_ready(~T, h, x, r) == D.project_insert(~T, D.checked(~T, E.InsertBefore{h, x}, r)) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
96 match r:
97 case Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
98 {==}
99 case Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
100 {==}
101
102def insert_before_U32(s: D.DList<U32>, +h: E.Handle, +x: U32) -> {D.insert_before(~U32, s, h, x) == D.project_insert(~U32, D.step(~U32, s, E.InsertBefore{h, x})) : D.DList<U32> & Result<&2, &2, E.Error, E.Handle>}:
103 insert_before_ready_same(~U32, h, x, D.validate(~U32, s, h))
104
105def insert_before_String(s: D.DList<String>, +h: E.Handle, +x: String) -> {D.insert_before(~String, s, h, x) == D.project_insert(~String, D.step(~String, s, E.InsertBefore{h, x})) : D.DList<String> & Result<&2, &2, E.Error, E.Handle>}:
106 insert_before_ready_same(~String, h, x, D.validate(~String, s, h))
107
108def insert_after_ready_same(~T: Data, +h: E.Handle, +x: T, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.insert_after_ready(~T, h, x, r) == D.project_insert(~T, D.checked(~T, E.InsertAfter{h, x}, r)) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
109 match r:
110 case Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
111 {==}
112 case Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
113 {==}
114
115def insert_after_U32(s: D.DList<U32>, +h: E.Handle, +x: U32) -> {D.insert_after(~U32, s, h, x) == D.project_insert(~U32, D.step(~U32, s, E.InsertAfter{h, x})) : D.DList<U32> & Result<&2, &2, E.Error, E.Handle>}:
116 insert_after_ready_same(~U32, h, x, D.validate(~U32, s, h))
117
118def insert_after_String(s: D.DList<String>, +h: E.Handle, +x: String) -> {D.insert_after(~String, s, h, x) == D.project_insert(~String, D.step(~String, s, E.InsertAfter{h, x})) : D.DList<String> & Result<&2, &2, E.Error, E.Handle>}:
119 insert_after_ready_same(~String, h, x, D.validate(~String, s, h))
120
121def remove_ready_same(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.remove_ready(~T, h, r) == D.project_value(~T, D.checked(~T, E.Remove{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, T>}:
122 match h r:
123 case E.H{owner, id, generation} Tuple{D.DL{tag, depth, cap, raw, gens}, Some{e}}:
124 {==}
125 case E.H{owner, id, generation} Tuple{D.DL{tag, depth, cap, raw, gens}, None{}}:
126 {==}
127
128def remove_U32(s: D.DList<U32>, +h: E.Handle) -> {D.remove(~U32, s, h) == D.project_value(~U32, D.step(~U32, s, E.Remove{h})) : D.DList<U32> & Result<&2, &2, E.Error, U32>}:
129 remove_ready_same(~U32, h, D.validate(~U32, s, h))
130
131def remove_String(s: D.DList<String>, +h: E.Handle) -> {D.remove(~String, s, h) == D.project_value(~String, D.step(~String, s, E.Remove{h})) : D.DList<String> & Result<&2, &2, E.Error, String>}:
132 remove_ready_same(~String, h, D.validate(~String, s, h))
133