diff options
Diffstat (limited to 'std')
| -rw-r--r-- | std/Meta.bruijn | 35 |
1 files changed, 28 insertions, 7 deletions
diff --git a/std/Meta.bruijn b/std/Meta.bruijn index 5eb6a21..31d781a 100644 --- a/std/Meta.bruijn +++ b/std/Meta.bruijn @@ -5,6 +5,7 @@ :import std/Combinator . :import std/Number/Unary . :import std/List . +:import std/Pair P # constructor of meta abstraction abs [[[[0 3]]]] ⧗ Meta → Meta @@ -125,16 +126,16 @@ eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a case-10 4 head case-11 [6 [6 [1 ~0]] 2] -eval eval-blc ∘ blc ⧗ Meta → Meta +eval* eval-blc ∘ blc ⧗ Meta → Meta # 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-idx [2 [1 [0 [[0]]] 0 [[1]]]] case-app 2 [3 [3 [2 0 (1 0)]]] - case-abs 2 [2 [[2 (0 : 1)]]] + case-abs 2 [2 [[2 [0 1 2]]]] -:test (eval `[(α-eq? `α-eq? `α-eq?)]) (true) +!‣ eval :test (!`(α-eq? `α-eq? `α-eq?)) (true) :test (!`((+21u) + (+21u))) ((+42u)) @@ -198,7 +199,27 @@ eval y [[[rec]]] [0 Ω] ⧗ Meta → a :test (β `[0]) (`[0]) :test (β `([0] [0])) (`[0]) -# TODO! -test [`(0 + (+1u))] +# set lhs of meta application +lhs [[1 i [[[[1 4 2]]]]]] ⧗ Meta → Meta → Meta -# :test (!(test (+3u))) ((+4u)) +:test (lhs `(1 0) `0) (`(0 0)) + +# set rhs of meta application +rhs [[1 i [[[[1 3 4]]]]]] ⧗ Meta → Meta → Meta + +:test (rhs `(0 1) `0) (`(0 0)) + +# swap terms of meta application +swap [0 i [[[[1 2 3]]]]] ⧗ Meta → Meta + +:test (swap `(1 0)) (`(0 1)) + +# applies a function to the body of a meta term +map [[0 case-idx case-app case-abs]] ⧗ (Meta → Meta) → Meta → Meta + case-idx [idx (2 0)] + case-app [[app (3 1 0)]] + case-abs [abs (2 0)] + +:test (map swap `[0 1]) (`[1 0]) +:test (map inc `0) (`1) +:test (map (map inc) `[0]) (`[1]) |