src/v2.bend

bend-lawful-stdlib@0.1.0.0 · 48 lines · 6 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/class.bend as C
3import bend-lawful-stdlib@0.1.0.0/src/u32.bend as U32
4
5# v2.bend: 2D integer vectors with wrapping + and -.
6#
7#   import ./v2.bend as V2
8#   V2.V2{x, y}, V2.group()
9
10type V2 is Data:
11  V2{x: U32, y: U32}
12
13def add(a: V2, b: V2) -> V2:
14  match a b:
15    case V2{ax, ay} V2{bx, by}:
16      V2{U32.add(ax, bx), U32.add(ay, by)}
17
18def sub(a: V2, b: V2) -> V2:
19  match a b:
20    case V2{ax, ay} V2{bx, by}:
21      V2{U32.sub(ax, bx), U32.sub(ay, by)}
22
23law sub_add:
24  for a: V2
25  for b: V2
26  {a == sub(add(a, b), b) : V2}
27
28def sub_add(a, b):
29  match a b:
30    case V2{+ax, +ay} V2{+bx, +by}:
31      %U32.sub_add(ax, bx) : {V2{ax, ay} == V2{_, U32.sub(U32.add(ay, by), by)} : V2}
32      %U32.sub_add(ay, by) : {V2{ax, ay} == V2{ax, _} : V2}
33      {==}
34
35law add_sub:
36  for a: V2
37  for b: V2
38  {a == add(sub(a, b), b) : V2}
39
40def add_sub(a, b):
41  match a b:
42    case V2{+ax, +ay} V2{+bx, +by}:
43      %U32.add_sub(ax, bx) : {V2{ax, ay} == V2{_, U32.add(U32.sub(ay, by), by)} : V2}
44      %U32.add_sub(ay, by) : {V2{ax, ay} == V2{ax, _} : V2}
45      {==}
46
47def group() -> C.Group<V2>:
48  C.Group{add, sub, sub_add, add_sub}