Basic reduction

3 files changed, 44 insertions, 17 deletions

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 []