Fix reducer and examples

3 files changed, 54 insertions, 50 deletions

diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index e0d94b7..d4996ee 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -17,15 +17,16 @@ import           Debug.Trace
 -- | A trace specifies the exact path to any subterm
 type Trace = [Breadcrumb]
 
-data Breadcrumb = AbsD -- | Down into abstraction
-                | AppL -- | Left side of application
-                | AppR -- | Right side of application
-                | NumS -- | Successor of number
-                | RecT -- | Term of rec -- TODO: RecT2??
-                | RecU -- | End of rec
-                | RecV -- | Function 1 of rec
-                | RecW -- | Function 2 of rec
-                | Root -- | Root
+data Breadcrumb = AbsD  -- | Down into abstraction
+                | AppL  -- | Left side of application
+                | AppR  -- | Right side of application
+                | NumS  -- | Successor of number
+                | RecT1 -- | Term 1 of rec
+                | RecT2 -- | Term 2 of rec
+                | RecU  -- | End of rec
+                | RecV  -- | Function 1 of rec
+                | RecW  -- | Function 2 of rec
+                | Root  -- | Root
   deriving (Eq, Show)
 
 -- | Map abstractions to a hashmap such that de Bruijn levels correspond to traces
@@ -36,15 +37,16 @@ traceAbs = go 0 [Root]
   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
-  go _ _ (Num Z            ) = M.empty
-  go n t (Num (S i)        ) = go n (NumS : t) i
-  go n t (Rec (t1, _) u v w) = foldl1
+  go _ _ (Lvl _             ) = M.empty
+  go _ _ (Num Z             ) = M.empty
+  go n t (Num (S i)         ) = go n (NumS : t) i
+  go n t (Rec (t1, t2) u v w) = foldl1
     (M.unionWith (++))
-    [ go n (RecT : t) t1
-    , go n (RecU : t) u
-    , go n (RecV : t) v
-    , go n (RecW : t) w
+    [ go n (RecT1 : t) t1
+    , go n (RecT2 : t) t2
+    , go n (RecU : t)  u
+    , go n (RecV : t)  v
+    , go n (RecW : t)  w
     ]
 
 -- TODO: Merge these two v^
@@ -54,14 +56,19 @@ 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
-  go t (Num (S i)        ) = go (NumS : t) i
-  go t (Rec (t1, _) u v w) = foldl1
+  go t (Lvl l             ) = M.singleton l [t]
+  go _ (Num Z             ) = M.empty
+  go t (Num (S i)         ) = go (NumS : t) i
+  go t (Rec (t1, t2) u v w) = foldl1
     (M.unionWith (++))
-    [go (RecT : t) t1, go (RecU : t) u, go (RecV : t) v, go (RecW : t) w]
+    [ go (RecT1 : t) t1
+    , go (RecT2 : t) t2
+    , go (RecU : t)  u
+    , go (RecV : t)  v
+    , go (RecW : t)  w
+    ]
 
 -- | Unify two two mapped traces to find levels at which the traces are no suffixes
 -- | Level traces not being a suffix of abstraction traces implies nonlinearity
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index 958c0a8..b9f7881 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -101,10 +101,10 @@ rec = do
   _  <- symbol "REC"
   _  <- spaces
   _  <- startSymbol "("
-  t  <- term
+  t1 <- term
   _  <- spaces
   _  <- startSymbol ","
-  t' <- nat
+  t2 <- term
   _  <- spaces
   _  <- startSymbol ")"
   _  <- startSymbol ","
@@ -115,7 +115,7 @@ rec = do
   _  <- spaces
   _  <- startSymbol ","
   w  <- term
-  pure $ Rec (t, t') u v w
+  pure $ Rec (t1, t2) 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 c10828e..dc8c9bd 100644
--- a/src/Language/Mili/Reducer.hs
+++ b/src/Language/Mili/Reducer.hs
@@ -10,34 +10,31 @@ import           Data.Mili                      ( Nat(..)
                                                 )
 
 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)
+-- WARNING: This function also shifts the substituted term and the levels of the parent!
+subst :: Int -> Int -> Term -> Term -> Term
+subst c l (Abs d m) s = Abs (d - 1) $ subst (c + 1) l m s
+subst c l (App a b) s = App (subst c l a s) (subst c l b s)
+subst c l (Lvl i) s | l == i    = shift c s
+                    | otherwise = Lvl $ i - 1
+subst _ _ (Num Z             ) _ = Num Z
+subst c l (Num (S m)         ) s = Num $ S $ subst c l m s
+subst c l (Rec (t1, t2) u v w) s = Rec (subst c l t1 s, subst c l t2 s)
+                                       (subst c l u s)
+                                       (subst c l v s)
+                                       (subst c 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 :: Term -> [Singleton] -> Term
+machine (App a b           ) s                    = machine a (TermTag b : s)
+machine (Abs l u           ) (TermTag t : s)      = machine (subst 0 l u t) s
+machine (Rec (t1, t2) u v w) s = machine t1 (RecTag t2 u v w : s)
+machine (Num Z             ) (RecTag _ u _ _ : s) = machine 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'
+  machine v (TermTag (Rec (App w t1, App w t2) u v w) : s)
+machine (Num (S t)) s = Num $ S $ machine t s -- TODO: ??
+machine t           _ = t
 
 -- | Reduce term to normal form
 nf :: Term -> Term
-nf = runMachine []
+nf t = machine t []