proofs/containers/doubly_linked_list/direct.bend
bend-collections-laws-containers@1.0.0.0 · 163 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/internal_dlist.bend as I
5import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
6
7# The public list's direct operations: each is the projection of the trace
8# step on the same operation, for every list and handle.
9
10
11# ---- the verdict's continuations ----
12
13def gv(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, p: R.DList<T> & Result<&2, &2, I.Error, T>) -> {D.get_result(~T, tag, depth, cap, gens, p) == D.project_value(~T, D.value_result(~T, tag, depth, cap, gens, p)) : D.DList<T> & Result<&2, &2, E.Error, T>}:
14 match p:
15 case Tuple{raw, res}:
16 {==}
17
18def sv(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, p: R.DList<T> & Result<&2, &2, I.Error, Unit>) -> {D.set_result(~T, tag, depth, cap, gens, p) == D.project_unit(~T, D.unit_result(~T, tag, depth, cap, gens, p)) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:
19 match p:
20 case Tuple{raw, res}:
21 {==}
22
23def get_m(~T: Data, +h: E.Handle, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.get_ready(~T, h, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_value(~T, D.checked(~T, E.Get{h}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:
24 match m:
25 case Some{e}:
26 {==}
27 case None{}:
28 gv(~T, tag, depth, cap, gens, R.get(~T, raw, D.old_handle(h)))
29
30def get_s(~T: Data, +h: E.Handle, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.get_ready(~T, h, (s, m)) == D.project_value(~T, D.checked(~T, E.Get{h}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:
31 match s:
32 case D.DL{+tag, +depth, +cap, raw, gens}:
33 get_m(~T, h, tag, depth, cap, raw, gens, m)
34
35def get_r(~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>}:
36 match r:
37 case Tuple{s, m}:
38 get_s(~T, h, s, m)
39
40def set_m(~T: Data, +h: E.Handle, +x: T, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.set_ready(~T, h, x, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_unit(~T, D.checked(~T, E.Set{h, x}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:
41 match m:
42 case Some{e}:
43 {==}
44 case None{}:
45 sv(~T, tag, depth, cap, gens, R.set(~T, raw, D.old_handle(h), x))
46
47def set_s(~T: Data, +h: E.Handle, +x: T, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.set_ready(~T, h, x, (s, m)) == D.project_unit(~T, D.checked(~T, E.Set{h, x}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:
48 match s:
49 case D.DL{+tag, +depth, +cap, raw, gens}:
50 set_m(~T, h, x, tag, depth, cap, raw, gens, m)
51
52def set_r(~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>}:
53 match r:
54 case Tuple{s, m}:
55 set_s(~T, h, x, s, m)
56
57def rm_m(~T: Data, +owner: U32, +id: U32, +g: U32, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.remove_ready(~T, E.H{owner, id, g}, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_value(~T, D.checked(~T, E.Remove{E.H{owner, id, g}}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:
58 match m:
59 case Some{e}:
60 {==}
61 case None{}:
62 {==}
63
64def rm_s(~T: Data, +owner: U32, +id: U32, +g: U32, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.remove_ready(~T, E.H{owner, id, g}, (s, m)) == D.project_value(~T, D.checked(~T, E.Remove{E.H{owner, id, g}}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:
65 match s:
66 case D.DL{+tag, +depth, +cap, raw, gens}:
67 rm_m(~T, owner, id, g, tag, depth, cap, raw, gens, m)
68
69def rm_r(~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>}:
70 match h r:
71 case E.H{+owner, +id, +g} Tuple{s, m}:
72 rm_s(~T, owner, id, g, s, m)
73
74def nx_m(~T: Data, +h: E.Handle, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.next_ready(~T, h, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_neighbour(~T, D.checked(~T, E.Next{h}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
75 match m:
76 case Some{e}:
77 {==}
78 case None{}:
79 {==}
80
81def nx_s(~T: Data, +h: E.Handle, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.next_ready(~T, h, (s, m)) == D.project_neighbour(~T, D.checked(~T, E.Next{h}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
82 match s:
83 case D.DL{+tag, +depth, +cap, raw, gens}:
84 nx_m(~T, h, tag, depth, cap, raw, gens, m)
85
86def nx_r(~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>>}:
87 match r:
88 case Tuple{s, m}:
89 nx_s(~T, h, s, m)
90
91def pv_m(~T: Data, +h: E.Handle, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.prev_ready(~T, h, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_neighbour(~T, D.checked(~T, E.Prev{h}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
92 match m:
93 case Some{e}:
94 {==}
95 case None{}:
96 {==}
97
98def pv_s(~T: Data, +h: E.Handle, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.prev_ready(~T, h, (s, m)) == D.project_neighbour(~T, D.checked(~T, E.Prev{h}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
99 match s:
100 case D.DL{+tag, +depth, +cap, raw, gens}:
101 pv_m(~T, h, tag, depth, cap, raw, gens, m)
102
103def pv_r(~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>>}:
104 match r:
105 case Tuple{s, m}:
106 pv_s(~T, h, s, m)
107
108def ib_m(~T: Data, +h: E.Handle, +x: T, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.insert_before_ready(~T, h, x, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_insert(~T, D.checked(~T, E.InsertBefore{h, x}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
109 match m:
110 case Some{e}:
111 {==}
112 case None{}:
113 {==}
114
115def ib_s(~T: Data, +h: E.Handle, +x: T, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.insert_before_ready(~T, h, x, (s, m)) == D.project_insert(~T, D.checked(~T, E.InsertBefore{h, x}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
116 match s:
117 case D.DL{+tag, +depth, +cap, raw, gens}:
118 ib_m(~T, h, x, tag, depth, cap, raw, gens, m)
119
120def ib_r(~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>}:
121 match r:
122 case Tuple{s, m}:
123 ib_s(~T, h, x, s, m)
124
125def ia_m(~T: Data, +h: E.Handle, +x: T, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.insert_after_ready(~T, h, x, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_insert(~T, D.checked(~T, E.InsertAfter{h, x}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
126 match m:
127 case Some{e}:
128 {==}
129 case None{}:
130 {==}
131
132def ia_s(~T: Data, +h: E.Handle, +x: T, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.insert_after_ready(~T, h, x, (s, m)) == D.project_insert(~T, D.checked(~T, E.InsertAfter{h, x}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
133 match s:
134 case D.DL{+tag, +depth, +cap, raw, gens}:
135 ia_m(~T, h, x, tag, depth, cap, raw, gens, m)
136
137def ia_r(~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>}:
138 match r:
139 case Tuple{s, m}:
140 ia_s(~T, h, x, s, m)
141
142# ---- the direct operations are projected steps ----
143
144def get_step(~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>}:
145 get_r(~T, h, D.validate(~T, s, h))
146
147def set_step(~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>}:
148 set_r(~T, h, x, D.validate(~T, s, h))
149
150def remove_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.remove(~T, s, h) == D.project_value(~T, D.step(~T, s, E.Remove{h})) : D.DList<T> & Result<&2, &2, E.Error, T>}:
151 rm_r(~T, h, D.validate(~T, s, h))
152
153def next_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.next(~T, s, h) == D.project_neighbour(~T, D.step(~T, s, E.Next{h})) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
154 nx_r(~T, h, D.validate(~T, s, h))
155
156def prev_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.prev(~T, s, h) == D.project_neighbour(~T, D.step(~T, s, E.Prev{h})) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:
157 pv_r(~T, h, D.validate(~T, s, h))
158
159def before_step(~T: Data, s: D.DList<T>, +h: E.Handle, +x: T) -> {D.insert_before(~T, s, h, x) == D.project_insert(~T, D.step(~T, s, E.InsertBefore{h, x})) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
160 ib_r(~T, h, x, D.validate(~T, s, h))
161
162def after_step(~T: Data, s: D.DList<T>, +h: E.Handle, +x: T) -> {D.insert_after(~T, s, h, x) == D.project_insert(~T, D.step(~T, s, E.InsertAfter{h, x})) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:
163 ia_r(~T, h, x, D.validate(~T, s, h))