diff options
| -rw-r--r-- | bruijn.cabal | 1 | ||||
| -rw-r--r-- | src/Eval.hs | 22 | ||||
| -rw-r--r-- | src/Helper.hs | 4 | ||||
| -rw-r--r-- | src/Parser.hs | 19 | ||||
| -rw-r--r-- | src/Reducer.hs | 11 | ||||
| -rw-r--r-- | std/List.bruijn | 4 | ||||
| -rw-r--r-- | std/Meta.bruijn | 163 |
7 files changed, 176 insertions, 48 deletions
diff --git a/bruijn.cabal b/bruijn.cabal index bb29aee..8914b59 100644 --- a/bruijn.cabal +++ b/bruijn.cabal @@ -25,6 +25,7 @@ data-files: std/List.bruijn std/Logic.bruijn std/Math.bruijn + std/Meta.bruijn std/Monad.bruijn std/Number.bruijn std/Option.bruijn diff --git a/src/Eval.hs b/src/Eval.hs index 6af1959..223a43a 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -131,6 +131,24 @@ evalPrefix :: Identifier -> Expression -> Environment -> EvalState (Failable Expression) 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' + 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 + +evalUnquote :: Expression -> Environment -> EvalState (Failable Expression) +evalUnquote f sub = evalExp f sub >>= \case + Left e -> pure $ Left e + Right f' -> pure $ Right $ Unquote $ unsafeReduce f' + evalExp :: Expression -> Environment -> EvalState (Failable Expression) evalExp idx@(Bruijn _ ) = const $ pure $ Right idx evalExp ( Function fun) = evalFun fun @@ -138,6 +156,8 @@ evalExp ( Abstraction e ) = evalAbs e evalExp ( Application f g) = evalApp f g evalExp ( MixfixChain es ) = evalMixfix es evalExp ( Prefix p e ) = evalPrefix p e +evalExp ( Quote e ) = evalQuote e +evalExp ( Unquote e ) = evalUnquote e evalDefinition :: Identifier -> Expression -> Environment -> EvalState (Failable Expression) @@ -290,7 +310,7 @@ evalCommand inp s@(EnvState env@(Environment envDefs) conf cache) = \case putStrLn $ toBinary red pure s Jot str -> do - let e = fromJot str + let e = fromJot str let (res, _) = evalExp e (Environment M.empty) `runState` env case res of Left err -> print err diff --git a/src/Helper.hs b/src/Helper.hs index 83bf95d..df1918b 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -135,7 +135,7 @@ instance Show Mixfix where show (MixfixExpression e) = show e -- TODO: Remove Application and replace with Chain (renaming of MixfixChain) -data Expression = Bruijn Int | Function Identifier | Abstraction Expression | Application Expression Expression | MixfixChain [Mixfix] | Prefix Identifier Expression +data Expression = Bruijn Int | Function Identifier | Abstraction Expression | Application Expression Expression | MixfixChain [Mixfix] | Prefix Identifier Expression | Quote Expression | Unquote Expression deriving (Ord, Eq, Generic, NFData) instance Show Expression where @@ -156,6 +156,8 @@ instance Show Expression where . foldr1 (\x y -> x . showString " " . y) (map shows ms) . showString "\ESC[33m)\ESC[0m" showsPrec _ (Prefix p e) = shows p . showString " " . shows e + showsPrec _ (Quote e ) = showString "\ESC[36m`\ESC[0m" . shows e + showsPrec _ (Unquote e ) = showString "\ESC[36m,\ESC[0m" . shows e data Command = Input String | Watch String | Import String String | Test Expression Expression | ClearState | Time Expression | Length Expression | Blc Expression | Jot String deriving (Show) diff --git a/src/Parser.hs b/src/Parser.hs index aee282b..57d6f58 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -42,9 +42,10 @@ mathematicalArrow = satisfy isMathematicalOperator -- "'" can't be in special chars because of 'c' char notation and prefixation -- "." can't be in special chars because of namespaced functions and UFCS syntax +-- "," can't be in special chars because of unquote specialChar :: Parser Char specialChar = - oneOf "!?*@,:;+-_#$%^&<>/\\|{}~=" + oneOf "!?*@:;+-_#$%^&<>/\\|{}~=" <|> mathematicalOperator <|> mathematicalArrow @@ -177,6 +178,18 @@ parseMixfix = do operatorAsMixfix = MixfixOperator . MixfixFunction <$> some mixfixSome singletonAsMixfix = MixfixExpression <$> parseSingleton +parseQuote :: Parser Expression +parseQuote = do + _ <- char '`' <?> "quote start" + e <- parseSingleton + pure $ Quote e + +parseUnquote :: Parser Expression +parseUnquote = do + _ <- char ',' <?> "unquote start" + e <- parseSingleton + pure $ Unquote e + parsePrefix :: Parser Expression parsePrefix = do p <- prefixOperator @@ -189,7 +202,9 @@ parseSingleton = parseBruijn <|> try parseNumeral <|> parseString - <|> parseChar + <|> try parseChar + <|> parseQuote + <|> parseUnquote <|> parseAbstraction <|> try parseFunction <|> parsePrefix diff --git a/src/Reducer.hs b/src/Reducer.hs index f5c1b7a..820cc04 100644 --- a/src/Reducer.hs +++ b/src/Reducer.hs @@ -2,6 +2,7 @@ -- based on the RKNL abstract machine module Reducer ( reduce + , unsafeReduce ) where import Control.Concurrent.MVar @@ -10,6 +11,7 @@ import Data.Map.Strict ( Map ) import qualified Data.Map.Strict as Map import Data.Maybe ( fromMaybe ) import Helper +import System.IO.Unsafe ( unsafePerformIO ) -- TODO: AAH type Store = Map Int Box type Stack = [Redex] @@ -37,7 +39,8 @@ toRedex = convertWorker (NameGen 1) [] in Rapp lhs rhs convertWorker _ ns (Bruijn i) = Rvar $ Num (if i < 0 || i >= length ns then i else ns !! i) - convertWorker _ _ _ = invalidProgramState + convertWorker g ns (Unquote e) = convertWorker g ns e + convertWorker _ _ _ = invalidProgramState fromRedex :: Redex -> Expression fromRedex = convertWorker [] @@ -106,3 +109,9 @@ reduce e = do forEachState (loadTerm redex) transition >>= \case Cconf _ [] v -> pure $ fromRedex v _ -> invalidProgramState + +-- TODO: AAAAAAAAAAAAAAAAH remove this +-- (probably not thaaat bad) +{-# NOINLINE unsafeReduce #-} +unsafeReduce :: Expression -> Expression +unsafeReduce = unsafePerformIO . reduce diff --git a/std/List.bruijn b/std/List.bruijn index 19fac6b..39aecf8 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -266,9 +266,9 @@ zip-with z [[[[rec]]]] ⧗ (a → b → c) → (List a) → (List b) → (List c :test ({ ++‣ | ((+0) : {}(+2)) }) ((+1) : {}(+3)) # doubled list comprehension -{…|…,…} zip-with ⧗ (a → b → c) → (List a) → (List b) → (List c) +{…|…;…} zip-with ⧗ (a → b → c) → (List a) → (List b) → (List c) -:test ({ …+… | ((+0) : {}(+2)) , ((+1) : {}(+3)) }) ((+1) : {}(+5)) +:test ({ …+… | ((+0) : {}(+2)) ; ((+1) : {}(+3)) }) ((+1) : {}(+5)) # returns first n elements of a list take z [[[rec]]] ⧗ Number → (List a) → (List a) 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)) |