math_sequence.bend

stelliferous@0.0.3.0 · 72 lines · 0 definitions

1# Element- and length-indexed sequence model. Random get is O(index);
2# runtime storage is Array<Element>, not this sequential observation.
3import Base
4
5law Values:
6  for -Element: Data
7  for length: Nat
8  Data
9
10type Elements<-Element: Data,-length: Nat> is Data:
11  Elements{head: Element,tail: Values(Element,length)}
12
13def Values(Element,length):
14  match length:
15    case 0n: Unit
16    case 1n+rest: Elements<Element,rest>
17
18law Index:
19  for length: Nat
20  Data
21
22type Position<-length: Nat> is Data:
23  First{}
24  Next{index: Index(length)}
25
26def Index(length):
27  match length:
28    case 0n: Empty
29    case 1n+rest: Position<rest>
30
31def index_value(length: Nat,index: Index(length)) -> Nat:
32  match length:
33    case 0n:
34      match index:
35    case 1n+rest:
36      match index:
37        case First{}: 0n
38        case Next{index}: 1n+index_value(rest,index)
39
40def tabulate(~Element: Data,~Context: Data,~sample: Context -> Nat -> Element,length: Nat,+offset: Nat,+context: Context) -> Values(Element,length):
41  match length:
42    case 0n: Unit{}
43    case 1n+rest:
44      Elements{sample(context,offset),tabulate(~Element,~Context,~sample,rest,1n+offset,context)}
45
46def get(-Element: Data,length: Nat,index: Index(length),vector: Values(Element,length)) -> Element:
47  match length:
48    case 0n:
49      match index:
50    case 1n+rest:
51      match index:
52        case First{}:
53          Elements{head,tail} = vector
54          head
55        case Next{index}:
56          Elements{head,tail} = vector
57          get(Element,rest,index,tail)
58
59def replicate(-Element: Data,length: Nat,+value: Element) -> Values(Element,length):
60  match length:
61    case 0n: Unit{}
62    case 1n+rest: Elements{value,replicate(Element,rest,value)}
63
64
65def zip_map(~Element: Data,~Context: Data,~combine: Context -> Element -> Element -> Element,
66  length: Nat,+context: Context,left: Values(Element,length),right: Values(Element,length)) -> Values(Element,length):
67  match length:
68    case 0n: Unit{}
69    case 1n+rest:
70      Elements{left_head,left_tail} = left
71      Elements{right_head,right_tail} = right
72      Elements{combine(context,left_head,right_head),zip_map(~Element,~Context,~combine,rest,context,left_tail,right_tail)}