hvm-core 0.2.26

HVM-Core is a massively parallel Interaction Combinator evaluator.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

// Decreases a tree of λ-encoded binary counters until they're all 0 (parallel).
// Takes about ~16s on Apple M1, and ~0.5s on RTX 4090

@c3  = ({1 {1 (c b) (b a)} (a R)} (c R))
@c4  = ({1 {1 {1 (d c) (c b)} (b a)} (a R)} (d R))
@c6  = ({1 {1 {1 {1 {1 (f e) (e d)} (d c)} (c b)} (b a)} (a R)} (f R))
@c8  = ({1 {1 {1 {1 {1 {1 {1 (h g) (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (h R))
@c10 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 (j i) (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (j R))
@c12 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (l k) (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (l R))
@c14 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (n m) (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (n R))
@c16 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (p o) (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (p R))
@c20 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (t s) (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (t R))
@c22 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (v u) (u t)} (t s)} (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (v R))
@c24 = ({1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 {1 (x w) (w v)} (v u)} (u t)} (t s)} (s r)} (r q)} (q p)} (p o)} (o n)} (n m)} (m l)} (l k)} (k j)} (j i)} (i h)} (h g)} (g f)} (f e)} (e d)} (d c)} (c b)} (b a)} (a R)} (x R))

@S = (a ((a b) (* b)))
@Z = (* (a a))

@O = (xs ((xs r) (* (* r))))
@I = (xs (* ((xs r) (* r))))
@E = (* (* (e e)))

@decO = (p idecp) & @I ~ (decp idecp) & @dec ~ (p decp)
@decI = (p lowp) & @low ~ (p lowp)
@dec  = ((@decO (@decI (@E R))) R)

@lowO = (p oop) & @O ~ (p op) & @O ~ (op oop)
@lowI = (p oip) & @I ~ (p ip) & @O ~ (ip oip)
@low  = ((@lowO (@lowI (@E R))) R)

@runO = (p R) & @run ~ (decop R) & @dec ~ (op decop) & @O ~ (p op)
@runI = (p R) & @run ~ (decip R) & @dec ~ (ip decip) & @I ~ (p ip)
@run  = ((@runO (@runI (@E R))) R)

@brnZ = (* R) & @run ~ (val R) & @c20 ~ (@I (@E val))
@brnS = ({1 p0 p1} (r0 r1)) & @brn ~ (p0 r0) & @brn ~ (p1 r1)
@brn  = ((@brnS (@brnZ r)) r)

@main
  = R
  & @c3 ~ (@S (@Z dep))
  & @brn ~ (dep R)