Switched to RKNL reducer

1 files changed, 100 insertions, 35 deletions

diff --git a/src/Term.hs b/src/Term.hs
index c2a47f1..c5a4fa0 100644
--- a/src/Term.hs
+++ b/src/Term.hs
@@ -6,12 +6,17 @@ module Term
   , nf
   ) where
 
+import           Control.Concurrent.MVar
 import           Data.IORef                     ( IORef
                                                 , modifyIORef
                                                 , newIORef
                                                 , readIORef
                                                 , writeIORef
                                                 )
+import           Data.List                      ( elemIndex )
+import           Data.Map.Strict                ( Map )
+import qualified Data.Map.Strict               as Map
+import           Data.Maybe                     ( fromMaybe )
 import           Utils
 
 data Term = Abs Term | App Term Term | Idx Int
@@ -42,41 +47,101 @@ fromBLC' inp = case inp of
 fromBLC :: String -> Term
 fromBLC = fst . fromBLC'
 
-shift :: Int -> Term -> Term
-shift i (Idx j) | i <= j    = Idx $ j + 1
-                | otherwise = Idx j
-shift i (App a b) = App (shift i a) (shift i b)
-shift i (Abs a  ) = Abs (shift (i + 1) a)
+-- RKNL abstract machine, call-by-need reducer
+-- written for my bruijn programming language
 
-subst :: Int -> Term -> Term -> Term
-subst i (Idx j) c | i == j    = c
-                  | j > i     = Idx $ j - 1
-                  | otherwise = Idx j
-subst i (App a b) c = App (subst i a c) (subst i b c)
-subst i (Abs a  ) c = Abs (subst (i + 1) a (shift 0 c))
+type Store = Map Int Box
+type Stack = [Redex]
 
-nf :: Term -> IO Term
-nf o = do -- TODO: pointfree??
-  -- i <- newIORef 1000
-  i <- newIORef 100000000
-  go i o
+newtype NameGen = NameGen Int
+data BoxValue = Todo Redex | Done Redex | Empty
+newtype Box = Box (MVar BoxValue)
+data Ridx = Num Int | Hole
+data Redex = Rabs Int Redex | Rapp Redex Redex | Ridx Ridx | Rclosure Redex Store | Rcache Box Redex
+data Conf = Econf NameGen Redex Store Stack | Cconf NameGen Stack Redex | End
+
+nextName :: NameGen -> (Int, NameGen)
+nextName (NameGen x) = (x, NameGen $ x + 1)
+
+toRedex :: Term -> Redex
+toRedex = convertWorker (NameGen 1) []
+ where
+  convertWorker g ns (Abs e) =
+    let (v, g') = nextName g
+        t       = convertWorker g' (v : ns) e
+    in  Rabs v t
+  convertWorker g ns (App l r) =
+    let lhs = convertWorker g ns l
+        rhs = convertWorker g ns r
+    in  Rapp lhs rhs
+  convertWorker _ ns (Idx i) =
+    Ridx $ Num (if i < 0 || i >= length ns then i else ns !! i)
+  convertWorker _ _ _ = invalid
+
+fromRedex :: Redex -> Term
+fromRedex = convertWorker []
  where
-  go :: IORef Integer -> Term -> IO Term
-  go i t = do -- oracle
-    readIORef i >>= \case
-      -- 0    -> writeIORef i (-1) >> return (Idx 0)
-      0 -> do
-        putStrLn "💥 potential infinite loop, continue? [yn]"
-        getLine >>= \case
-          "y" -> writeIORef i (-2) >> re i t
-          "n" -> writeIORef i (-1) >> return t
-          _   -> go i t
-      (-1) -> return t
-      _    -> modifyIORef i (subtract 1) >> re i t
-
-  re :: IORef Integer -> Term -> IO Term
-  re i (App l r) = go i l >>= \case
-    Abs t -> go i (subst 0 t r)
-    t     -> App t <$> go i r
-  re i (Abs t) = Abs <$> go i t
-  re _ t       = pure t
+  convertWorker es (Rabs n e) = Abs $ convertWorker (n : es) e
+  convertWorker es (Rapp l r) =
+    let lhs = convertWorker es l
+        rhs = convertWorker es r
+    in  App lhs rhs
+  convertWorker es (Ridx (Num n)) = Idx $ fromMaybe n (elemIndex n es)
+  convertWorker _  _              = invalid
+
+transition :: Conf -> IO Conf
+transition (Econf g (Rapp u v) e s) =
+  pure $ Econf g u e (Rapp (Ridx Hole) (Rclosure v e) : s)
+transition (Econf g (Rabs x t) e s) = do
+  box <- newMVar Empty
+  pure $ Cconf g s (Rcache (Box box) (Rclosure (Rabs x t) e))
+transition (Econf g (Ridx (Num x)) e s) = do
+  def <- newMVar $ Done $ Ridx $ Num x
+  let b@(Box m) = Map.findWithDefault (Box def) x e
+  rd <- readMVar m
+  case rd of
+    Todo (Rclosure v e') -> pure $ Econf g v e' (Rcache b (Ridx Hole) : s)
+    Done t               -> pure $ Cconf g s t
+    _                    -> invalid
+transition (Cconf g ((Rcache (Box m) (Ridx Hole)) : s) t) = do
+  modifyMVar_ m (\_ -> pure $ Done t)
+  pure $ Cconf g s t
+transition (Cconf g ((Rapp (Ridx Hole) ve) : s) (Rcache _ (Rclosure (Rabs x t) e)))
+  = do
+    box <- newMVar (Todo ve)
+    pure $ Econf g t (Map.insert x (Box box) e) s
+transition (Cconf g s (Rcache (Box m) (Rclosure (Rabs x t) e))) = do
+  rd <- readMVar m
+  case rd of
+    Done v -> pure $ Cconf g s v
+    Empty  -> do
+      let (x1, g') = nextName g
+      box <- newMVar $ Done $ Ridx $ Num x1
+      pure $ Econf g'
+                   t
+                   (Map.insert x (Box box) e)
+                   (Rabs x1 (Ridx Hole) : Rcache (Box m) (Ridx Hole) : s)
+    Todo _ -> invalid
+transition (Cconf g ((Rapp (Ridx Hole) (Rclosure v e)) : s) t) =
+  pure $ Econf g v e (Rapp t (Ridx Hole) : s)
+transition (Cconf g ((Rapp t (Ridx Hole)) : s) v) = pure $ Cconf g s (Rapp t v)
+transition (Cconf g ((Rabs x1 (Ridx Hole)) : s) v) =
+  pure $ Cconf g s (Rabs x1 v)
+transition (Cconf _ [] _) = pure End
+transition _              = invalid
+
+forEachState :: Conf -> (Conf -> IO Conf) -> IO Conf
+forEachState conf trans = trans conf >>= \case
+  End  -> pure conf
+  next -> forEachState next trans
+
+-- TODO: NameGen is arbitrary to not conflict with toRedex
+loadTerm :: Redex -> Conf
+loadTerm t = Econf (NameGen 1000000) t Map.empty []
+
+nf :: Term -> IO Term
+nf e = do
+  let redex = toRedex e
+  forEachState (loadTerm redex) transition >>= \case
+    Cconf _ [] v -> pure $ fromRedex v
+    _            -> invalid