diff options
| -rw-r--r-- | src/Eval.hs | 15 | ||||
| -rw-r--r-- | std/Meta.bruijn | 35 |
2 files changed, 36 insertions, 14 deletions
diff --git a/src/Eval.hs b/src/Eval.hs index 223a43a..426b733 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -134,15 +134,16 @@ evalPrefix p e = evalExp $ Application (Function p) e evalQuote :: Expression -> Environment -> EvalState (Failable Expression) evalQuote f sub = evalExp f sub >>= \case Left e -> pure $ Left e - Right f' -> pure $ Right $ quotify f' + Right f' -> pure $ Right $ quotify 0 f' where base l r = Abstraction $ Abstraction $ Abstraction $ Application l r - quotify (Abstraction e) = base (Bruijn 0) (quotify e) - quotify (Application l r) = - base (Application (Bruijn 1) (quotify l)) (quotify r) - quotify (Bruijn i) = base (Bruijn 2) (decimalToUnary $ fromIntegral i) - quotify (Unquote e) = quotify e - quotify _ = invalidProgramState + quotify n (Abstraction e) = base (Bruijn 0) (quotify (n + 1) e) + quotify n (Application l r) = + base (Application (Bruijn 1) (quotify (n + 1) l)) (quotify (n + 1) r) + quotify _ (Bruijn i) = base (Bruijn 2) (decimalToUnary $ fromIntegral i) + quotify n (Unquote (Bruijn i)) = Bruijn $ n * 3 + i + quotify n (Unquote e ) = quotify n e + quotify _ _ = invalidProgramState evalUnquote :: Expression -> Environment -> EvalState (Failable Expression) evalUnquote f sub = evalExp f sub >>= \case 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]) |