4 files changed, 49 insertions, 22 deletions
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index ac6703a..9ba832b 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -13,7 +13,7 @@ import           Prelude                 hiding ( abs
 
 data Nat = Z | S Term
 
-data Term = Abs Term                       -- | Abstraction
+data Term = Abs Int Term                   -- | Abstraction with level
           | App Term Term                  -- | Application
           | Lvl Int                        -- | de Bruijn level
           | Num Nat                        -- | Peano numeral
@@ -21,10 +21,10 @@ data Term = Abs Term                       -- | Abstraction
 
 instance Show Nat where
   show Z     = "Z"
-  show (S t) = "S " <> show t
+  show (S t) = "S(" <> show t <> ")"
 
 instance Show Term where
-  showsPrec _ (Abs m) = showString "[" . shows m . showString "]"
+  showsPrec _ (Abs _ m) = showString "[" . shows m . showString "]"
   showsPrec _ (App m n) =
     showString "(" . shows m . showString " " . shows n . showString ")"
   showsPrec _ (Lvl i) = shows i
@@ -42,14 +42,14 @@ instance Show Term where
       . shows w
 
 fold
-  :: (Term -> Term)
+  :: (Int -> Term -> Term)
   -> (Term -> Term -> Term)
   -> (Int -> Term)
   -> (Nat -> Term)
   -> ((Term, Nat) -> Term -> Term -> Term -> Term)
   -> Term
   -> Term
-fold abs app lvl num rec (Abs m) = abs $ fold abs app lvl num rec m
+fold abs app lvl num rec (Abs l m) = abs l $ fold abs app lvl num rec m
 fold abs app lvl num rec (App a b) =
   app (fold abs app lvl num rec a) (fold abs app lvl num rec b)
 fold _   _   lvl _   _   (Lvl n           ) = lvl n
diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index 8befe0b..e0d94b7 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -33,7 +33,7 @@ data Breadcrumb = AbsD -- | Down into abstraction
 traceAbs :: Term -> HashMap Int [Trace]
 traceAbs = go 0 [Root]
  where
-  go n t (Abs m) =
+  go n t (Abs _ m) =
     M.unionWith (++) (go (n + 1) (AbsD : t) m) (M.singleton n [t])
   go n t (App a b) = M.unionWith (++) (go n (AppL : t) a) (go n (AppR : t) b)
   go _ _ (Lvl _            ) = M.empty
@@ -54,7 +54,7 @@ traceAbs = go 0 [Root]
 traceLvl :: Term -> HashMap Int [Trace]
 traceLvl = go [Root]
  where
-  go t (Abs m            ) = go (AbsD : t) m
+  go t (Abs _ m          ) = go (AbsD : t) m
   go t (App a b) = M.unionWith (++) (go (AppL : t) a) (go (AppR : t) b)
   go t (Lvl l            ) = M.singleton l [t]
   go _ (Num Z            ) = M.empty
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index a733ade..958c0a8 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -77,7 +77,9 @@ toLevel n = do
 
 -- | abstraction, entering increases the abstraction depth
 abs :: Parser Term
-abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec))
+abs = between (startSymbol "[")
+              (symbol "]")
+              (gets (Abs <$> _depth) <*> (inc *> block <* dec))
  where
   inc = modify $ \r@(PS { _depth = d }) -> r { _depth = d + 1 }
   dec = modify $ \r@(PS { _depth = d }) -> r { _depth = d - 1 }
@@ -98,28 +100,22 @@ rec :: Parser Term
 rec = do
   _  <- symbol "REC"
   _  <- spaces
-  _  <- symbol "("
-  _  <- spaces
+  _  <- startSymbol "("
   t  <- term
   _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ","
   t' <- nat
   _  <- spaces
-  _  <- symbol ")"
-  _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ")"
+  _  <- startSymbol ","
   u  <- term
   _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ","
   v  <- term
   _  <- spaces
-  _  <- symbol ","
-  _  <- spaces
+  _  <- startSymbol ","
   w  <- term
-  pure $ Rec (t, t') u v w -- TODO
+  pure $ Rec (t, t') u v w
 
 -- | single identifier, directly parsed to corresponding term
 def :: Parser Term
diff --git a/src/Language/Mili/Reducer.hs b/src/Language/Mili/Reducer.hs
index 8074bdf..c10828e 100644
--- a/src/Language/Mili/Reducer.hs
+++ b/src/Language/Mili/Reducer.hs
@@ -6,7 +6,38 @@ module Language.Mili.Reducer
 
 import           Data.Mili                      ( Nat(..)
                                                 , Term(..)
+                                                , shift
                                                 )
+
+data Singleton = TermTag Term | RecTag Term Term Term Term
+  deriving Show
+
+-- TODO: There will only ever be one substitution, so don't iterate the entire tree!
+-- Otherwise replace with fold
+subst :: Int -> Term -> Term -> Term
+subst l (Abs d m) s = Abs d $ subst l m s
+subst l (App a b) s = App (subst l a s) (subst l b s)
+subst l (Lvl i) s | l == i    = s
+                  | otherwise = (Lvl i)
+subst _ (Num Z    ) _ = Num Z
+subst l (Num (S m)) s = Num $ S $ subst l m s
+subst l (Rec (t1, t2) u v w) s =
+  Rec (subst l t1 s, t2) (subst l u s) (subst l v s) (subst l w s)
+
+machine :: Term -> [Singleton] -> (Term, [Singleton])
+machine (App a b) s = (a, TermTag b : s)
+machine (Abs l u) (TermTag t : s) = (shift (-1) (subst l u t), s)
+machine (Rec (t1, t2) u v w) s = (t1, RecTag (Num t2) u v w : s)
+machine (Num Z) (RecTag _ u _ _ : s) = (u, s)
+machine (Num (S t1)) ((RecTag t2 u v w) : s) =
+  (v, RecTag (App (App w t1) t2) u v w : s)
+machine t s = error $ show t <> show s
+
+runMachine :: [Singleton] -> Term -> Term
+runMachine s t = case machine t s of
+  (t', []) -> t'
+  (t', s') -> runMachine s' t'
+
 -- | Reduce term to normal form
 nf :: Term -> Term
-nf t = t
+nf = runMachine []