Fix reducer and examples

6 files changed, 102 insertions, 72 deletions

diff --git a/readme.md b/readme.md
index bd1f455..7d0378d 100644
--- a/readme.md
+++ b/readme.md
@@ -16,11 +16,11 @@ while still benefitting from the advantages of syntactic linearity.
 Mili's core syntactic representation consists of only five constructs:
 
 ``` haskell
-data Term = Abs Int Term                   -- | Abstraction at level
-          | App Term Term                  -- | Application
-          | Lvl Int                        -- | de Bruijn level
-          | Num Nat                        -- | Peano numeral
-          | Rec (Term, Nat) Term Term Term -- | Unbounded iteration
+data Term = Abs Int Term                    -- | Abstraction at level
+          | App Term Term                   -- | Application
+          | Lvl Int                         -- | de Bruijn level
+          | Num Nat                         -- | Peano numeral
+          | Rec (Term, Term) Term Term Term -- | Unbounded iteration
 ```
 
 Lets and Pairs are only used in the higher-level syntax. This allows us
@@ -38,6 +38,7 @@ to use a minimal abstract reduction machine.
     -   [ ] `:test`
     -   [ ] `:import`
 -   [ ] more examples
+-   [ ] compile to LLVM stack machine
 
 ## references
 
diff --git a/samples/math.mili b/samples/math.mili
index 6fff8d2..8d8810a 100644
--- a/samples/math.mili
+++ b/samples/math.mili
@@ -1,3 +1,28 @@
-add = [[REC (1, <0>), 0, [S 0], [[[0 2 1]]]]]
-mul = [[REC (1, <0>), <0>, (add 0), [[[0 2 1]]]]]
-add <0> <2>
+-- identity
+i = [0]
+
+-- first element of Church pair
+fst = [0 [[REC (0, <0>), 1, i, i]]]
+
+-- second element of Church pair
+snd = [0 [[REC (1, <0>), 0, i, i]]]
+
+-- copy numbers
+c = [REC (0, <0>), [0 <0> <0>], [0 [[[0 (S 2) (S 1)]]]], i]
+
+-- add two numbers
+add = [[REC (1, <0>), 0, [S 0], i]]
+
+-- multiply two numbers
+mul = [[REC (1, <0>), <0>, (add 0), i]]
+
+-- decrement number by one
+dec = [
+  f = [c (snd 0) [[[0 2 (S 1)]]]]
+  fst (REC (0, <0>), [0 <0> <0>], f, i)
+]
+
+-- <0> if zero, <1> if not
+iszero = [fst (REC (0, <0>), [0 <0> (S <0>)], [c (snd 0)], i)]
+
+iszero (mul <5> (dec <4>))
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index 9ba832b..e5609ad 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -13,11 +13,11 @@ import           Prelude                 hiding ( abs
 
 data Nat = Z | S Term
 
-data Term = Abs Int Term                   -- | Abstraction with level
-          | App Term Term                  -- | Application
-          | Lvl Int                        -- | de Bruijn level
-          | Num Nat                        -- | Peano numeral
-          | Rec (Term, Nat) Term Term Term -- | Unbounded iteration
+data Term = Abs Int Term                    -- | Abstraction with level
+          | App Term Term                   -- | Application
+          | Lvl Int                         -- | de Bruijn level
+          | Num Nat                         -- | Peano numeral
+          | Rec (Term, Term) Term Term Term -- | Unbounded iteration
 
 instance Show Nat where
   show Z     = "Z"
@@ -29,11 +29,11 @@ instance Show Term where
     showString "(" . shows m . showString " " . shows n . showString ")"
   showsPrec _ (Lvl i) = shows i
   showsPrec _ (Num n) = shows n
-  showsPrec _ (Rec (n, t) u v w) =
+  showsPrec _ (Rec (t1, t2) u v w) =
     showString "REC ("
-      . shows n
+      . shows t1
       . showString ", "
-      . shows t
+      . shows t2
       . showString "), "
       . shows u
       . showString ", "
@@ -46,21 +46,21 @@ fold
   -> (Term -> Term -> Term)
   -> (Int -> Term)
   -> (Nat -> Term)
-  -> ((Term, Nat) -> Term -> Term -> Term -> Term)
+  -> ((Term, Term) -> Term -> Term -> Term -> Term)
   -> Term
   -> Term
 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
-fold _   _   _   num _   (Num Z           ) = num Z
+fold _   _   lvl _   _   (Lvl n             ) = lvl n
+fold _   _   _   num _   (Num Z             ) = num Z
 fold abs app lvl num rec (Num (S t)) = num $ S $ fold abs app lvl num rec t
-fold abs app lvl num rec (Rec (t, n) u v w) = rec
-  (fold abs app lvl num rec t, n) -- TODO: t'
+fold abs app lvl num rec (Rec (t1, t2) u v w) = rec
+  (fold abs app lvl num rec t1, fold abs app lvl num rec t2)
   (fold abs app lvl num rec u)
   (fold abs app lvl num rec v)
   (fold abs app lvl num rec w)
 
 shift :: Int -> Term -> Term
 shift 0 = id
-shift n = fold Abs App (\l -> Lvl $ l + n) Num Rec
+shift n = fold (\l m -> Abs (l + n) m) App (\l -> Lvl $ l + n) Num Rec
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 []