src/list.bend

bend-lawful-stdlib@0.1.0.0 · 70 lines · 5 definitions

1import Base
2
3# list.bend: laws about Base's List.append and List.reverse, for any Data
4# element.
5#
6#   import ./list.bend as List
7#
8# Equations put the side a caller rewrites away on the right.
9
10# One step of reading a sequence: nothing left, or an element and the rest.
11# The quantity a is the rest's: &2 for a list, &1 for a linear queue.
12type Step<a, -A: Data, -S: Kind(a)> is Kind(a):
13  Stop{}
14  Next{x: A, rest: S}
15
16def uncons(-A: Data, xs: List<&2, A>) -> Step<&2, A, List<&2, A>>:
17  match xs:
18    case Nil{}:
19      Stop{}
20    case h <> t:
21      Next{h, t}
22
23law append_nil:
24  for -A: Data
25  for xs: List<&2, A>
26  {xs == List.append(&2, A, xs, Nil{}) : List<&2, A>}
27
28def append_nil(A, xs):
29  match xs:
30    case Nil{}:
31      {==}
32    case h <> t:
33      %append_nil(A, t) : {h <> t == h <> _ : List<&2, A>}
34      {==}
35
36law append_assoc:
37  for -A: Data
38  for a: List<&2, A>
39  for -b: List<&2, A>
40  for -c: List<&2, A>
41  {List.append(&2, A, a, List.append(&2, A, b, c)) == List.append(&2, A, List.append(&2, A, a, b), c) : List<&2, A>}
42
43def append_assoc(A, a, b, c):
44  match a:
45    case Nil{}:
46      {==}
47    case h <> t:
48      %append_assoc(A, t, b, c) : {h <> List.append(&2, A, t, List.append(&2, A, b, c)) == h <> _ : List<&2, A>}
49      {==}
50
51# List.reverse is List.reverse.go(xs, Nil{}); this says what the
52# accumulator does.
53law reverse_go:
54  for -A: Data
55  for +xs: List<&2, A>
56  for +acc: List<&2, A>
57  {List.append(&2, A, List.reverse(&2, A, xs), acc) == List.reverse.go(&2, A, xs, acc) : List<&2, A>}
58
59def reverse_go(A, xs, acc):
60  match xs:
61    case Nil{}:
62      {==}
63    case h <> t:
64      -g = List.append(&2, A, List.reverse(&2, A, h <> t), acc)
65      %reverse_go(A, t, h <> acc) : {g == _ : List<&2, A>}
66      %reverse_go(A, t, [h]) : {List.append(&2, A, _, acc) == List.append(&2, A, List.reverse(&2, A, t), h <> acc) : List<&2, A>}
67      Equal.sym(List<&2, A>,
68        List.append(&2, A, List.reverse(&2, A, t), List.append(&2, A, [h], acc)),
69        List.append(&2, A, List.append(&2, A, List.reverse(&2, A, t), [h]), acc),
70        append_assoc(A, List.reverse(&2, A, t), [h], acc))