More work on transpiler

1 files changed, 48 insertions, 0 deletions

diff --git a/src/Term.hs b/src/Term.hs
index 081363d..c2a47f1 100644
--- a/src/Term.hs
+++ b/src/Term.hs
@@ -1,8 +1,17 @@
+{-# LANGUAGE LambdaCase #-}
+
 module Term
   ( Term(..)
   , fromBLC
+  , nf
   ) where
 
+import           Data.IORef                     ( IORef
+                                                , modifyIORef
+                                                , newIORef
+                                                , readIORef
+                                                , writeIORef
+                                                )
 import           Utils
 
 data Term = Abs Term | App Term Term | Idx Int
@@ -32,3 +41,42 @@ 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)
+
+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))
+
+nf :: Term -> IO Term
+nf o = do -- TODO: pointfree??
+  -- i <- newIORef 1000
+  i <- newIORef 100000000
+  go i o
+ 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