blob: 716cc7aabae1aba66f143275c6754013d4c27490 (
plain) (
blame)
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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
# Metaprogramming
Bruijn has a homoiconic meta encoding inspired by Lisp's quoting
feature.
Blog post with more details: [Metaprogramming and
self-interpretation](https://text.marvinborner.de/2023-09-03-21.html).
## Encoding
`X ⤳ [[[2 (+Xu)]]]
`(M N) ⤳ [[[1 `M `N]]]
`[M] ⤳ [[[0 `M]]]
Any quoted term gets converted to this encoding:
``` bruijn
# example quotations
:test (`0) ([[[2 (+0u)]]])
:test (`[0]) ([[[0 [[[2 (+0u)]]]]]])
:test (`'0') ([[[0 [[[0 [[[0 [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+1u)]]] [[[1 [[[2 (+1u)]]] [[[1 [[[2 (+0u)]]] [[[1 [[[2 (+0u)]]] [[[2 (+2u)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]])
# quotes are nestable!
:test (``0) ([[[0 [[[0 [[[0 [[[1 [[[2 (+2u)]]] [[[0 [[[0 [[[2 (+0u)]]]]]]]]]]]]]]]]]]]]])
:test (`[0 `0]) ([[[0 [[[1 [[[2 (+0u)]]] [[[0 [[[0 [[[0 [[[1 [[[2 (+2u)]]] [[[0 [[[0 [[[2 (+0u)]]]]]]]]]]]]]]]]]]]]]]]]]]])
```
## Quasiquotation
Quoted terms can be escaped (*unquoted*) using the comma symbol.
Unquoted terms will be fully evaluated first before getting quoted
again.
``` bruijn
:test (```,[0]) (``[0])
:test (`,`,[0]) ([0])
:test (`[0 `,[0]]) (`[0 [0]])
```
Unquoted De Bruijn indices will get bound to the respective abstraction
outside of its meta encoding.
``` bruijn
# adds two using normal quotation
add-two `[0 + (+2u)]
:test (!add-two (+2u)) ((+4u))
# adds two using a reaching De Bruijn index
add-two* [`(,0 + (+2u))]
:test (!(add-two* `(+2u))) ((+4u))
```
## Meta library [`std/Meta`](/std/Meta.bruijn.html)
The meta library enables simple interaction with the meta encoding.
Examples:
``` bruijn
# testing equivalence
:test (α-eq? `[0 0] `[0 0]) (true)
:test (α-eq? `α-eq? `α-eq?) (true)
# BLC length of meta term
:test (length `[0]) ((+4u))
:test (length `[[1 1]]) ((+12u))
# self-modification
:test (lhs `(1 0) `0) (`(0 0))
:test (rhs `(0 1) `0) (`(0 0))
:test (swap `(1 0)) (`(0 1))
:test (map inc `0) (`1)
:test (map (map inc) `[0]) (`[1])
:test (map swap `[0 1]) (`[1 0])
# encoding terms as numbers
:test ((encode `(0 0)) =? (+3)) (true)
:test ((encode `[0]) =? (+8)) (true)
# decoding numbers to terms
:test (decode (+3)) (`(0 0))
:test (decode (+8)) (`[0])
```
|
