Experiments with monadic folding

1 files changed, 43 insertions, 19 deletions

diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index e5609ad..c10b24f 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -3,33 +3,36 @@
 module Data.Mili
   ( Term(..)
   , Nat(..)
+  , foldM
   , fold
   , shift
   ) where
 
+import           Data.Functor.Identity          ( runIdentity )
 import           Prelude                 hiding ( abs
                                                 , min
                                                 )
 
 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, Term) 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"
   show (S t) = "S(" <> show t <> ")"
 
 instance Show Term where
-  showsPrec _ (Abs _ m) = showString "[" . shows m . showString "]"
+  showsPrec _ (Abs l m) =
+    showString "(\\" . shows l . showString "." . shows m . showString ")"
   showsPrec _ (App m n) =
     showString "(" . shows m . showString " " . shows n . showString ")"
   showsPrec _ (Lvl i) = shows i
   showsPrec _ (Num n) = shows n
-  showsPrec _ (Rec (t1, t2) u v w) =
+  showsPrec _ (Rec t1 t2 u v w) =
     showString "REC ("
       . shows t1
       . showString ", "
@@ -41,25 +44,46 @@ instance Show Term where
       . showString ", "
       . shows w
 
+foldM
+  :: Monad m
+  => (Int -> Term -> m Term)
+  -> (Term -> Term -> m Term)
+  -> (Int -> m Term)
+  -> (Nat -> m Term)
+  -> (Term -> Term -> Term -> Term -> Term -> m Term)
+  -> Term
+  -> m Term
+foldM abs app lvl num rec (Abs d m) = foldM abs app lvl num rec m >>= abs d
+foldM abs app lvl num rec (App a b) = do
+  a' <- foldM abs app lvl num rec a
+  b' <- foldM abs app lvl num rec b
+  app a' b'
+foldM _   _   lvl _   _   (Lvl i          ) = pure i >>= lvl
+foldM _   _   _   num _   (Num Z          ) = pure Z >>= num
+foldM abs app lvl num rec (Num (S m)) = foldM abs app lvl num rec m >>= num . S
+foldM abs app lvl num rec (Rec t1 t2 u v w) = do
+  t1' <- foldM abs app lvl num rec t1
+  t2' <- foldM abs app lvl num rec t2
+  u'  <- foldM abs app lvl num rec u
+  v'  <- foldM abs app lvl num rec v
+  w'  <- foldM abs app lvl num rec w
+  rec t1' t2' u' v' w'
+
 fold
   :: (Int -> Term -> Term)
   -> (Term -> Term -> Term)
   -> (Int -> Term)
   -> (Nat -> Term)
-  -> ((Term, Term) -> 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 abs app lvl num rec (Num (S t)) = num $ S $ fold abs app lvl num rec 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)
+fold abs app lvl num rec term = runIdentity $ foldM
+  (\d m -> pure $ abs d m)
+  (\a b -> pure $ app a b)
+  (pure . lvl)
+  (pure . num)
+  (\t1 t2 u v w -> pure $ rec t1 t2 u v w)
+  term
 
 shift :: Int -> Term -> Term
 shift 0 = id