diff options
Diffstat (limited to 'std/Meta.bruijn')
| -rw-r--r-- | std/Meta.bruijn | 163 |
1 files changed, 122 insertions, 41 deletions
diff --git a/std/Meta.bruijn b/std/Meta.bruijn index 723d5dc..92e097c 100644 --- a/std/Meta.bruijn +++ b/std/Meta.bruijn @@ -9,68 +9,64 @@ # constructor of meta abstraction abs [[[[0 3]]]] ⧗ Meta → Meta -:test (abs '0) ('[0]) +:test (abs `0) (`[0]) # true if abstraction abs? [0 [false] [[false]] [true]] ⧗ Meta → Bool -:test (abs? '[0]) (true) -:test (abs? '([0] [0])) (false) -:test (abs? '0) (false) +:test (abs? `[0]) (true) +:test (abs? `([0] [0])) (false) +:test (abs? `0) (false) # extracts meta term from meta abstraction abs! [0 0 0 [0]] ⧗ Meta → Meta -:test (abs! '[[0]]) ('[0]) +:test (abs! `[[0]]) (`[0]) # constructor of meta application app [[[[[1 4 3]]]]] ⧗ Meta → Meta → Meta -# TODO: parser bug without lhs application - -:test ((app '[[1]]) '[0]) ('([[1]] [0])) +:test (app `[[1]] `[0]) (`([[1]] [0])) # true if application app? [0 [false] [[true]] [false]] ⧗ Meta → Bool -:test (app? '[0]) (false) -:test (app? '([0] [0])) (true) -:test (app? '0) (false) +:test (app? `[0]) (false) +:test (app? `([0] [0])) (true) +:test (app? `0) (false) # extracts both meta terms from meta application -app! [0 0 [[1 : 0]] 0] ⧗ Meta → (Pair Meta Meta) - -# TODO: parser bug with mixfix application +app! [0 0 cons 0] ⧗ Meta → (Pair Meta Meta) -:test (app! '([[1]] [[0]])) ((cons '[[1]]) '[[0]]) +:test (app! `([[1]] [[0]])) (`[[1]] : `[[0]]) # extracts lhs meta term from meta application app-lhs! ^‣ ∘ app! ⧗ Meta → Meta -:test (app-lhs! '([[1]] [[0]])) ('[[1]]) +:test (app-lhs! `([[1]] [[0]])) (`[[1]]) # extracts rhs meta term from meta application app-rhs! ~‣ ∘ app! ⧗ Meta → Meta -:test (app-rhs! '([[1]] [[0]])) ('[[0]]) +:test (app-rhs! `([[1]] [[0]])) (`[[0]]) # constructor of meta variable/index idx [[[[2 3]]]] ⧗ Unary → Meta -:test (idx (+0u)) ('0) +:test (idx (+0u)) (`0) # true if variable/index idx? [0 [true] [[false]] [false]] ⧗ Meta → Bool -:test (idx? '[0]) (false) -:test (idx? '([0] [0])) (false) -:test (idx? '0) (true) +:test (idx? `[0]) (false) +:test (idx? `([0] [0])) (false) +:test (idx? `0) (true) # extracts index from meta index idx! [0 [0] 0 0] ⧗ Meta → Unary -:test (idx! '0) ((+0u)) -:test (idx! '3) ((+3u)) +:test (idx! `0) ((+0u)) +:test (idx! `3) ((+3u)) # traverses meta term fold y [[[[[rec]]]]] ⧗ (Unary → a) → (a → a → a) → (a → a) → Meta → a @@ -85,8 +81,8 @@ length fold idx-cb app-cb abs-cb ⧗ Meta → Unary app-cb (add (+2u)) ∘∘ add abs-cb add (+2u) -:test (length '[0]) ((+4u)) -:test (length '[[1 1]]) ((+12u)) +:test (length `[0]) ((+4u)) +:test (length `[[1 1]]) ((+12u)) # true bit blc1 [[0]] ⧗ LcBit @@ -100,22 +96,107 @@ blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit) app-cb (cons blc0) ∘ (cons blc1) ∘∘ append abs-cb (cons blc0) ∘ (cons blc0) -:test (blc '[0]) (blc0 : (blc0 : (blc1 : {}blc0))) -:test (blc '[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0))))))))))) +:test (blc `[0]) (blc0 : (blc0 : (blc1 : {}blc0))) +:test (blc `[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0))))))))))) α-eq? y [[[rec]]] ⧗ Meta → Meta → Bool rec 1 case-idx case-app case-abs - case-idx [(idx? 1) ⋀? (0 =? (idx! 1))] - case-app [[(app? 2) ⋀? (4 1 (app-lhs! 2)) ⋀? (4 0 (app-rhs! 2))]] - case-abs [(abs? 1) ⋀? (3 (abs! 1) 0)] - -# TODO: parser bug - -:test ((α-eq? '0) '1) ([[0]]) -:test ((α-eq? '1) '1) ([[1]]) -:test ((α-eq? '(0 0)) '1) ([[0]]) -:test ((α-eq? '(0 0)) '(1 0)) ([[0]]) -:test ((α-eq? '(0 0)) '(0 0)) ([[1]]) -:test ((α-eq? '(0 1)) '(0 1)) ([[1]]) -:test ((α-eq? '[0]) '[1]) ([[0]]) -:test ((α-eq? '[0]) '[0]) ([[1]]) + case-idx [(idx? 1) (0 =? (idx! 1)) false] + case-app [[(app? 2) (app! 2 [[(6 3 1) ⋀? (6 2 0)]]) false]] + case-abs [(abs? 1) (3 (abs! 1) 0) false] + +:test (α-eq? `0 `1) (false) +:test (α-eq? `1 `1) (true) +:test (α-eq? `(0 0) `1) (false) +:test (α-eq? `(0 0) `(1 0)) (false) +:test (α-eq? `(0 0) `(0 0)) (true) +:test (α-eq? `(0 1) `(0 1)) (true) +:test (α-eq? `[0] `[1]) (false) +:test (α-eq? `[0] `[0]) (true) +:test (α-eq? `α-eq? `α-eq?) (true) + +# 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 + case-00 5 [[2 (0 : 1)]] + case-01 6 [6 [2 0 (1 0)]] + case-1 0 case-10 case-11 + case-10 4 head + case-11 [6 [6 [1 ~0]] 2] + +eval eval-blc ∘ blc ⧗ Meta → Meta + +!‣ eval + +: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]]]] + +# increments indices reaching out of their abstraction depth +κ y [[[rec]]] ⧗ Meta → Unary → Meta + rec 1 case-idx case-app case-abs + case-idx [idx ((1 >? 0) 0 ++0)] + case-app [[app (4 1 2) (4 0 2)]] + case-abs [abs (3 0 ++1)] + +:test (κ `0 (+1u)) (`0) +:test (κ `0 (+0u)) (`1) +:test (κ `1 (+0u)) (`2) +:test (κ `[0] (+0u)) (`[0]) +:test (κ `[1] (+0u)) (`[2]) +:test (κ `[2] (+1u)) (`[3]) +:test (κ `(1 0) (+1u)) (`(2 0)) + +# substitutes term based on unary abstraction depth +σ y [[[[rec]]]] ⧗ Meta → Meta → Unary → Meta + rec 2 case-idx case-app case-abs + case-idx [compare-case case-eq case-lt case-gt 1 0] + case-eq 2 + case-lt idx 0 + case-gt idx --0 + case-app [[app (5 1 3 2) (5 0 3 2)]] + case-abs [abs (4 0 (κ 2 (+0u)) ++1)] + +:test (σ `0 `2 (+0u)) (`2) +:test (σ `[1] `2 (+0u)) (`[3]) +:test (σ `[[4 0]] `2 (+1u)) (`[[3 0]]) +:test (σ `[[3] [3]] `0 (+0u)) (`[[2] [2]]) + +# reduces given term to its normal form +β* y [[rec]] ⧗ Meta → Meta + rec 0 case-idx case-app case-abs + case-idx idx + case-app [[(3 1) case-idx case-app case-abs]] + case-idx [app (idx 0) (4 1)] + case-app [[app (app 1 0) (5 2)]] + case-abs [4 (σ 0 1 (+0u))] + case-abs [abs (2 0)] + +:test (β* `0) (`0) +:test (β* `[0]) (`[0]) +:test (β* `([0] [0])) (`[0]) +:test (β* `(++(+2u))) (`(+3u)) + +# single-pass beta reduction +β y [[rec]] ⧗ Meta → Meta + rec 0 case-idx case-app case-abs + case-idx idx + case-app [[abs? 1 redex normal]] + redex σ (abs! 1) 0 (+0u) + normal app 1 (3 0) + case-abs [abs (2 0)] + case-ass abs ∘ 2 + +:test (β `0) (`0) +:test (β `[0]) (`[0]) +:test (β `([0] [0])) (`[0]) + +# TODO! +test [`(0 + (+1u))] + +# :test (!(test (+3u))) ((+4u)) |