1	import Base
2	import ../../../src/containers/dlist_iterator.bend as I
3	import ../../../src/containers/doubly_linked_list.bend as D
4	import ../../../src/containers/types/doubly_linked_list.bend as E
5	import ../../../src/containers/internal/dlist_storage.bend as R
6	import ../../../spec/containers/dlist_iterator.bend as S
7	
8	# Component laws over the actual cursor implementation. These are not a full
9	# sequence-refinement proof for all edits/traces or the underlying arena.
10	def finish_owns(s: D.DList<U32>, n: U32, last: U32, f: Bool, i: Nat) -> {I.finish(~U32, I.IT{s, n, last, f, i}) == s : D.DList<U32>}:
11	  {==}
12	
13	def next_exhausted(s: D.DList<U32>, +last: U32, +f: Bool, +i: Nat) -> {I.next(~U32, I.IT{s, 0, last, f, i}) == (I.IT{s, 0, last, f, i}, Fail{I.Exhausted{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, U32>}:
14	  match s:
15	    case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
16	      {==}
17	
18	def set_requires_current(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat, x: U32) -> {I.set(~U32, I.IT{s, n, 0, f, i}, x) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
19	  {==}
20	
21	def remove_requires_current(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat) -> {I.remove(~U32, I.IT{s, n, 0, f, i}) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
22	  match s:
23	    case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
24	      {==}
25	
26	def has_next_state(s: D.DList<U32>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_next(~U32, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, I.present(n)) : I.Iterator<U32> & Bool}:
27	  {==}
28	
29	def has_previous_state(s: D.DList<U32>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_previous(~U32, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, Nat.is_lt(0n, i)) : I.Iterator<U32> & Bool}:
30	  {==}
31	
32	def added_clears_current(s: D.DList<U32>, +n: U32, last: U32, +f: Bool, +i: Nat, h: E.Handle) -> {I.added(~U32, n, last, f, i, (s, Done{h})) == (I.IT{s, n, 0, f, 1n+i}, Done{Unit{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
33	  {==}
34	
35	def removed_forward(s: D.DList<U32>, n: U32, last: U32, +i: Nat, +after: U32, x: U32) -> {I.removed(~U32, n, last, True{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, True{}, Nat.sub(i, 1n)}, Done{Unit{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
36	  {==}
37	
38	def removed_backward(s: D.DList<U32>, n: U32, last: U32, +i: Nat, +after: U32, x: U32) -> {I.removed(~U32, n, last, False{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, False{}, i}, Done{Unit{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
39	  {==}
40	
41	def finish_owns_string(s: D.DList<String>, n: U32, last: U32, f: Bool, i: Nat) -> {I.finish(~String, I.IT{s, n, last, f, i}) == s : D.DList<String>}:
42	  {==}
43	
44	def next_exhausted_string(s: D.DList<String>, +last: U32, +f: Bool, +i: Nat) -> {I.next(~String, I.IT{s, 0, last, f, i}) == (I.IT{s, 0, last, f, i}, Fail{I.Exhausted{}}) : I.Iterator<String> & Result<&2, &2, I.Error, String>}:
45	  match s:
46	    case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
47	      {==}
48	
49	def set_requires_current_string(s: D.DList<String>, +n: U32, +f: Bool, +i: Nat, x: String) -> {I.set(~String, I.IT{s, n, 0, f, i}, x) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
50	  {==}
51	
52	def remove_requires_current_string(s: D.DList<String>, +n: U32, +f: Bool, +i: Nat) -> {I.remove(~String, I.IT{s, n, 0, f, i}) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
53	  match s:
54	    case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
55	      {==}
56	
57	def has_next_state_string(s: D.DList<String>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_next(~String, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, I.present(n)) : I.Iterator<String> & Bool}:
58	  {==}
59	
60	def has_previous_state_string(s: D.DList<String>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_previous(~String, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, Nat.is_lt(0n, i)) : I.Iterator<String> & Bool}:
61	  {==}
62	
63	def added_clears_current_string(s: D.DList<String>, +n: U32, last: U32, +f: Bool, +i: Nat, h: E.Handle) -> {I.added(~String, n, last, f, i, (s, Done{h})) == (I.IT{s, n, 0, f, 1n+i}, Done{Unit{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
64	  {==}
65	
66	def removed_forward_string(s: D.DList<String>, n: U32, last: U32, +i: Nat, +after: U32, x: String) -> {I.removed(~String, n, last, True{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, True{}, Nat.sub(i, 1n)}, Done{Unit{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
67	  {==}
68	
69	def removed_backward_string(s: D.DList<String>, n: U32, last: U32, +i: Nat, +after: U32, x: String) -> {I.removed(~String, n, last, False{}, i, after, (s, Done{x})) == (I.IT{s, after, 0, False{}, i}, Done{Unit{}}) : I.Iterator<String> & Result<&2, &2, I.Error, Unit>}:
70	  {==}
71	
72	# The end-gap insertion is exactly the public DLL append, including capacity
73	# growth, free-slot reuse, and generation bookkeeping. This is an algorithm
74	# bridge, not merely an equality with a model that invokes the iterator.
75	def end_gap_is_append(s: D.DList<U32>, x: U32) -> {I.cursor_insert_gap(~U32, s, 0, x) == I.insert_gap_result(~U32, D.push_back(~U32, s, x)) : D.DList<U32> & Result<&2, &2, E.Error, E.Handle>}:
76	  match s:
77	    case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
78	      {==}
79	
80	def end_gap_is_append_string(s: D.DList<String>, x: String) -> {I.cursor_insert_gap(~String, s, 0, x) == I.insert_gap_result(~String, D.push_back(~String, s, x)) : D.DList<String> & Result<&2, &2, E.Error, E.Handle>}:
81	  match s:
82	    case D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}:
83	      {==}
84	
85	def move_forward_cursor(n: U32, last: U32, f: Bool, +i: Nat, +h: U32, +after: U32, +x: U32) -> {I.move_meta(~U32, n, last, f, i, h, after, True{}, Done{x}) == I.M{after, h, True{}, 1n+i, Done{x}} : I.Move<U32>}:
86	  {==}
87	
88	def move_backward_cursor(n: U32, last: U32, f: Bool, +i: Nat, +h: U32, +x: U32) -> {I.move_meta(~U32, n, last, f, i, h, h, False{}, Done{x}) == I.M{h, h, False{}, Nat.sub(i, 1n), Done{x}} : I.Move<U32>}:
89	  {==}
90	
91	def failed_move_preserves_cursor(+n: U32, +last: U32, +f: Bool, +i: Nat, h: U32, after: U32, forward: Bool, +e: I.Error) -> {I.move_meta(~U32, n, last, f, i, h, after, forward, Fail{e}) == I.M{n, last, f, i, Fail{e}} : I.Move<U32>}:
92	  {==}
93	
94	# ==== the contract of dlist_iterator (stated in spec/containers/dlist_iterator.bend) ====================
95	
96	def has_element(s: D.DList<U32>, +n: U32, +last: U32, +f: Bool, +i: Nat) -> {I.has_next(~U32, I.IT{s, n, last, f, i}) == (I.IT{s, n, last, f, i}, I.present(n)) : I.Iterator<U32> & Bool}:
97	  has_next_state(s, n, last, f, i)
98	
99	def next_at_end(s: D.DList<U32>, +last: U32, +f: Bool, +i: Nat) -> {I.next(~U32, I.IT{s, 0, last, f, i}) == (I.IT{s, 0, last, f, i}, Fail{I.Exhausted{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, U32>}:
100	  next_exhausted(s, last, f, i)
101	
102	def replace_pre(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat, x: U32) -> {I.set(~U32, I.IT{s, n, 0, f, i}, x) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
103	  set_requires_current(s, n, f, i, x)
104	
105	def delete_pre(s: D.DList<U32>, +n: U32, +f: Bool, +i: Nat) -> {I.remove(~U32, I.IT{s, n, 0, f, i}) == (I.IT{s, n, 0, f, i}, Fail{I.NoCurrent{}}) : I.Iterator<U32> & Result<&2, &2, I.Error, Unit>}:
106	  remove_requires_current(s, n, f, i)