Implemented RKNL in Haskell

7 files changed, 129 insertions, 61 deletions

diff --git a/bruijn.cabal b/bruijn.cabal
index f5d3bb4..927172e 100644
--- a/bruijn.cabal
+++ b/bruijn.cabal
@@ -13,12 +13,12 @@ author:         Marvin Borner
 maintainer:     develop@marvinborner.de
 copyright:      2022 Marvin Borner
 license:        MIT
-license-file:   LICENSE
 build-type:     Simple
 extra-source-files:
-    README.md
+    readme.md
 data-files:
     config
+    std/Binary.bruijn
     std/Byte.bruijn
     std/Church.bruijn
     std/Combinator.bruijn
@@ -62,6 +62,7 @@ library
     , haskeline
     , megaparsec
     , mtl
+    , random
   default-language: Haskell2010
 
 executable bruijn
@@ -86,6 +87,7 @@ executable bruijn
     , haskeline
     , megaparsec
     , mtl
+    , random
   default-language: Haskell2010
 
 test-suite bruijn-test
@@ -111,4 +113,5 @@ test-suite bruijn-test
     , haskeline
     , megaparsec
     , mtl
+    , random
   default-language: Haskell2010
diff --git a/package.yaml b/package.yaml
index 0bd59a1..536a5ee 100644
--- a/package.yaml
+++ b/package.yaml
@@ -7,7 +7,7 @@ maintainer:          "develop@marvinborner.de"
 copyright:           "2022 Marvin Borner"
 
 extra-source-files:
-- README.md
+- readme.md
 
 data-files:
 - config
@@ -26,9 +26,9 @@ default-extensions:
   - LambdaCase
 
 dependencies:
+- array
 - base >= 4.7 && < 5
 - binary
-- array
 - bitstring
 - bytestring
 - containers
@@ -37,6 +37,7 @@ dependencies:
 - haskeline
 - megaparsec
 - mtl
+- random
 
 library:
   source-dirs: src
diff --git a/src/Binary.hs b/src/Binary.hs
index 44ac1bd..ad67b20 100644
--- a/src/Binary.hs
+++ b/src/Binary.hs
@@ -1,3 +1,4 @@
+-- MIT License, Copyright (c) 2022 Marvin Borner
 module Binary
   ( toBinary
   , fromBinary
diff --git a/src/Eval.hs b/src/Eval.hs
index 0e0e650..276524c 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -1,3 +1,4 @@
+-- MIT License, Copyright (c) 2022 Marvin Borner
 module Eval
   ( evalMain
   ) where
@@ -129,7 +130,6 @@ 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 _                     = error "invalid"
 
 evalDefinition
   :: Identifier -> Expression -> Environment -> EvalState (Failable Expression)
@@ -230,17 +230,15 @@ evalCommand inp s@(EnvState env@(Environment envDefs) conf cache) = \case
   Test e1 e2
     | _evalTests conf
     -> let (res, _) = evalTest e1 e2 (Environment M.empty) `runState` env
-       in
-         case res of
-           Left err ->
-             print (ContextualError err $ Context inp $ _nicePath conf)
-               >> pure s
-           Right (Test e1' e2') ->
-             when (lhs /= rhs) (print $ FailedTest e1 e2 lhs rhs) >> pure s
-            where
-             lhs = reduce e1'
-             rhs = reduce e2'
-           _ -> pure s
+       in  case res of
+             Left err ->
+               print (ContextualError err $ Context inp $ _nicePath conf)
+                 >> pure s
+             Right (Test e1' e2') -> do
+               lhs <- reduce e1'
+               rhs <- reduce e2'
+               when (lhs /= rhs) (print $ FailedTest e1 e2 lhs rhs) >> pure s
+             _ -> pure s
     | otherwise
     -> pure s
 
@@ -274,10 +272,12 @@ evalInstruction (ContextualInstruction instr inp) s@(EnvState env conf _) rec =
     Evaluate e ->
       let (res, _) = evalExp e (Environment M.empty) `runState` env
       in  (case res of
-            Left  err -> print err
-            Right e'  -> showResult e' (reduce e') env
+            Left  err -> print err >> rec s
+            Right e'  -> do
+              red <- reduce e'
+              showResult e' red env
+              rec s
           )
-            >> rec s
     Commands cs -> yeet (pure s) cs >>= rec
      where -- TODO: sus
       yeet s' []        = s'
@@ -322,8 +322,9 @@ evalFileConf path conf = do
   case M.lookup entryFunction env of
     Nothing -> print
       $ ContextualError (UndefinedIdentifier entryFunction) (Context "" path)
-    Just EnvDef { _exp = e } ->
-      showResult e (reduce $ Application e arg) (Environment env)
+    Just EnvDef { _exp = e } -> do
+      red <- reduce $ Application e arg
+      showResult e red (Environment env)
 
 evalFile :: String -> IO ()
 evalFile path = evalFileConf path (defaultConf path)
@@ -337,8 +338,10 @@ exec path rd conv = do
   f   <- rd path
   arg <- encodeStdin
   case f of
-    Left exception -> print (exception :: IOError)
-    Right f' -> showResult e (reduce $ Application e arg) (Environment M.empty)
+    Left  exception -> print (exception :: IOError)
+    Right f'        -> do
+      red <- reduce $ Application e arg
+      showResult e red (Environment M.empty)
       where e = fromBinary $ conv f'
 
 repl :: EnvState -> InputT M ()
diff --git a/src/Helper.hs b/src/Helper.hs
index a1333fb..a10fbee 100644
--- a/src/Helper.hs
+++ b/src/Helper.hs
@@ -1,3 +1,4 @@
+-- MIT License, Copyright (c) 2022 Marvin Borner
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RecordWildCards #-}
diff --git a/src/Parser.hs b/src/Parser.hs
index b2579a9..74c2585 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -1,3 +1,4 @@
+-- MIT License, Copyright (c) 2022 Marvin Borner
 module Parser
   ( parseBlock
   , parseReplLine
@@ -248,7 +249,7 @@ parseReplDefine = do
   var <- defIdentifier
   _   <- sc *> char '=' <* sc
   e   <- parseExpression
-  t   <- parseDefineType
+  _   <- parseDefineType
   pure $ ContextualInstruction (Define var e []) inp
 
 parseComment :: Parser ()
diff --git a/src/Reducer.hs b/src/Reducer.hs
index 7ba5845..8ff23b1 100644
--- a/src/Reducer.hs
+++ b/src/Reducer.hs
@@ -1,43 +1,101 @@
+-- MIT License, Copyright (c) 2023 Marvin Borner
+-- based on the RKNL abstract machine
 module Reducer
   ( reduce
   ) where
 
+import           Data.IORef
+import           Data.List                      ( elemIndex )
+import           Data.Map                       ( Map )
+import qualified Data.Map                      as Map
 import           Helper
+import           System.Random                  ( randomIO )
 
--- TODO: Research interaction nets and optimal reduction
-
--- TODO: Eta-reduction: [f 0] => f
---   (Abstraction f@_ (Bruijn 0)) = f
-
-(<+>) :: Expression -> Int -> Expression
-(<+>) (Bruijn x         ) n = if x > n then Bruijn (pred x) else Bruijn x
-(<+>) (Application e1 e2) n = Application (e1 <+> n) (e2 <+> n)
-(<+>) (Abstraction e    ) n = Abstraction $ e <+> (succ n)
-(<+>) _                   _ = error "invalid"
-
-(<->) :: Expression -> Int -> Expression
-(<->) (Bruijn x         ) n = if x > n then Bruijn (succ x) else Bruijn x
-(<->) (Application e1 e2) n = Application (e1 <-> n) (e2 <-> n)
-(<->) (Abstraction e    ) n = Abstraction $ e <-> (succ n)
-(<->) _                   _ = error "invalid"
-
-bind :: Expression -> Expression -> Int -> Expression
-bind e (Bruijn x         ) n = if x == n then e else Bruijn x
-bind e (Application e1 e2) n = Application (bind e e1 n) (bind e e2 n)
-bind e (Abstraction exp' ) n = Abstraction $ bind (e <-> (-1)) exp' (succ n)
-bind _ _                   _ = error "invalid"
-
-step :: Expression -> Expression
-step (Bruijn e) = Bruijn e
-step (Application (Abstraction e) app) = (bind (app <-> (-1)) e 0) <+> 0
-step (Application e1 e2) = Application (step e1) (step e2)
-step (Abstraction e) = Abstraction (step e)
-step _ = error "invalid"
-
--- until eq
-converge :: Eq a => (a -> a) -> a -> a
-converge = until =<< ((==) =<<)
-
--- alpha conversion is not needed with de bruijn indexing
-reduce :: Expression -> Expression
-reduce = converge step
+type Store = Map Int Box
+type Stack = [Redex]
+
+data BoxValue = Todo Redex | Done Redex | Empty
+data Box = Box (IORef BoxValue)
+data Rvar = Num Int | Hole
+data Redex = Rabs Int Redex | Rapp Redex Redex | Rvar Rvar | Rclosure Redex Store | Rcache Box Redex
+data Conf = Econf Redex Store Stack | Cconf Stack Redex | End
+
+toRedex :: Expression -> IO Redex
+toRedex = convertWorker []
+ where
+  convertWorker ns (Abstraction e) = do
+    v <- randomIO :: IO Int
+    t <- convertWorker (v : ns) e
+    pure $ Rabs v t
+  convertWorker ns (Application l r) = do
+    lhs <- convertWorker ns l
+    rhs <- convertWorker ns r
+    pure $ Rapp lhs rhs
+  convertWorker ns (Bruijn i) = pure $ Rvar $ Num
+    (if idx < 0 then i else ns !! idx)
+    where idx = i
+  convertWorker _ _ = error "invalid"
+
+fromRedex :: Redex -> IO Expression
+fromRedex = pure . convertWorker []
+ where
+  convertWorker es (Rabs n e) = Abstraction $ convertWorker (n : es) e
+  convertWorker es (Rapp l r) =
+    Application (convertWorker es l) (convertWorker es r)
+  convertWorker es (Rvar (Num n)) =
+    Bruijn $ maybe (error $ "unbound variable " ++ show n) id $ elemIndex n es
+  convertWorker _ _ = error "invalid"
+
+transition :: Conf -> IO Conf
+transition (Econf (Rapp u v) e s) =
+  pure $ Econf u e ((Rapp (Rvar Hole) (Rclosure v e)) : s)
+transition (Econf (Rabs x t) e s) = do
+  box <- newIORef Empty
+  pure $ Cconf s (Rcache (Box box) (Rclosure (Rabs x t) e))
+transition (Econf (Rvar (Num x)) e s) = do
+  def <- newIORef $ Done $ Rvar $ Num x
+  let b@(Box m) = Map.findWithDefault (Box def) x e
+  rd <- readIORef m
+  case rd of
+    Todo (Rclosure v e') -> pure $ Econf v e' ((Rcache b (Rvar Hole)) : s)
+    Done t               -> pure $ Cconf s t
+    _                    -> error "invalid"
+transition (Cconf ((Rcache (Box m) (Rvar Hole)) : s) t) = do
+  writeIORef m (Done t)
+  pure $ Cconf s t
+transition (Cconf ((Rapp (Rvar Hole) ve) : s) (Rcache _ (Rclosure (Rabs x t) e)))
+  = do
+    box <- newIORef (Todo ve)
+    pure $ Econf t (Map.insert x (Box box) e) s
+transition (Cconf s (Rcache (Box m) (Rclosure (Rabs x t) e))) = do
+  rd <- readIORef m
+  case rd of
+    Done v -> pure $ Cconf s v
+    Empty  -> do
+      x1  <- randomIO :: IO Int
+      box <- newIORef $ Done $ Rvar $ Num x1
+      pure $ Econf t
+                   (Map.insert x (Box box) e)
+                   ((Rabs x1 (Rvar Hole)) : (Rcache (Box m) (Rvar Hole)) : s)
+    Todo _ -> error "invalid"
+transition (Cconf ((Rapp (Rvar Hole) (Rclosure v e)) : s) t) =
+  pure $ Econf v e ((Rapp t (Rvar Hole)) : s)
+transition (Cconf ((Rapp t (Rvar Hole)) : s) v) = pure $ Cconf s (Rapp t v)
+transition (Cconf ((Rabs x1 (Rvar Hole)) : s) v) = pure $ Cconf s (Rabs x1 v)
+transition (Cconf [] _) = pure End
+transition _ = error "invalid"
+
+forEachState :: Conf -> (Conf -> IO Conf) -> IO Conf
+forEachState conf trans = trans conf >>= \case
+  End  -> pure conf
+  next -> forEachState next trans
+
+loadTerm :: Redex -> Conf
+loadTerm t = Econf t Map.empty []
+
+reduce :: Expression -> IO Expression
+reduce e = do
+  redex <- toRedex e
+  forEachState (loadTerm redex) transition >>= \case
+    Cconf [] v -> fromRedex v
+    _          -> error "invalid"