1	import Base
2	import ../../../src/containers/doubly_linked_list.bend as D
3	import ../../../src/containers/internal/dlist_storage.bend as R
4	import ../../../src/containers/types/internal_dlist.bend as I
5	import ../../../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	
13	def 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	
18	def 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	
23	def 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	
30	def 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	
35	def 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	
40	def 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	
47	def 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	
52	def 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	
57	def 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	
64	def 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	
69	def 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	
74	def 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	
81	def 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	
86	def 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	
91	def 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	
98	def 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	
103	def 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	
108	def 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	
115	def 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	
120	def 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	
125	def 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	
132	def 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	
137	def 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	
144	def 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	
147	def 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	
150	def 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	
153	def 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	
156	def 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	
159	def 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	
162	def 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))