diff options
| -rw-r--r-- | docs/wiki_src/coding/meta-programming.md | 19 | ||||
| -rw-r--r-- | docs/wiki_src/custom.css | 7 | ||||
| -rw-r--r-- | std/Meta.bruijn | 18 |
3 files changed, 30 insertions, 14 deletions
diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md index 44f5ea2..5d1caa0 100644 --- a/docs/wiki_src/coding/meta-programming.md +++ b/docs/wiki_src/coding/meta-programming.md @@ -1,11 +1,10 @@ # Meta programming -TODO: more (blog) +Bruijn has a homoiconic meta encoding inspired by Lisp's quoting +feature. -Bruijn has a homoiconic meta encoding similar to Lisp's quoting feature. - -Blog post with more details: [Homoiconic self interpretation of lambda -calculus](https://text.marvinborner.de/2023-09-03-21.html). +Blog post with more details: [Metaprogramming and +self-interpretation](https://text.marvinborner.de/2023-09-03-21.html). ## Encoding @@ -52,7 +51,7 @@ add-two `[0 + (+2u)] # adds two using a reaching De Bruijn index add-two* [`(,0 + (+2u))] -:test (!(add-two* (+2u))) ((+4u)) +:test (!(add-two* `(+2u))) ((+4u)) ``` ## Meta library [`std/Meta`](/std/Meta.bruijn.html) @@ -69,4 +68,12 @@ Examples: # 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]) ``` diff --git a/docs/wiki_src/custom.css b/docs/wiki_src/custom.css index fdcea31..170b4cc 100644 --- a/docs/wiki_src/custom.css +++ b/docs/wiki_src/custom.css @@ -1,3 +1,10 @@ +pre { + width: 100%; + white-space: pre; + overflow-x: scroll; + display: inline-grid; +} + .headerlink { display: none; } diff --git a/std/Meta.bruijn b/std/Meta.bruijn index 92e097c..5eb6a21 100644 --- a/std/Meta.bruijn +++ b/std/Meta.bruijn @@ -117,8 +117,8 @@ blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit) # modified Tromp 232 bit universal machine eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a - rec 0 [[0 [2 case-0 case-1]]] ⧗ Self → Cont → (List LcBit) → a - case-0 5 [1 case-00 case-01] ⧗ LcBit → (List LcBit) → Self → Cont → (List LcBit) → a + rec 0 [[0 [2 case-0 case-1]]] + case-0 5 [1 case-00 case-01] case-00 5 [[2 (0 : 1)]] case-01 6 [6 [2 0 (1 0)]] case-1 0 case-10 case-11 @@ -127,15 +127,17 @@ eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a eval eval-blc ∘ blc ⧗ Meta → Meta -!‣ eval +# self interpreter for meta encoding +eval y [[[rec]]] [0 Ω] ⧗ Meta → a + rec 0 case-idx case-app case-abs + case-idx [2 [head (1 tail 0)]] + case-app 2 [3 [3 [2 0 (1 0)]]] + case-abs 2 [2 [[2 (0 : 1)]]] :test (eval `[(α-eq? `α-eq? `α-eq?)]) (true) -eval-meta y [[[rec]]] [0 Ω] ⧗ Meta → a - rec 0 case-idx case-app case-abs - case-idx [3 (0 k)] - case-app [3 [3 [2 0 (1 0)]]] - case-abs [2 [[2 [0 1 2]]]] +:test (!`(α-eq? `α-eq? `α-eq?)) (true) +:test (!`((+21u) + (+21u))) ((+42u)) # increments indices reaching out of their abstraction depth κ y [[[rec]]] ⧗ Meta → Unary → Meta |