Fix substitution bug

1 files changed, 30 insertions, 0 deletions

diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index b407d00..1fdaa40 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -1,5 +1,7 @@
 module Data.Mili
   ( Term(..)
+  , fold
+  , shift
   ) where
 
 data Term = Abs Term      -- | Abstraction
@@ -11,3 +13,31 @@ instance Show Term where
   showsPrec _ (App m n) =
     showString "(" . shows m . showString " " . shows n . showString ")"
   showsPrec _ (Lvl i) = shows i
+  showsPrec _ (Num n) = shows n
+  showsPrec _ (Min n u f) =
+    showString "μ"
+      . shows n
+      . showString " "
+      . shows u
+      . showString " "
+      . shows f
+
+fold
+  :: (t -> t)
+  -> (t -> t -> t)
+  -> (Int -> t)
+  -> (Nat -> t)
+  -> (Nat -> t -> t -> t)
+  -> Term
+  -> t
+fold abs app lvl num min (Abs m) = abs (fold abs app lvl num min m)
+fold abs app lvl num min (App a b) =
+  app (fold abs app lvl num min a) (fold abs app lvl num min b)
+fold _ _ lvl _   _ (Lvl n) = lvl n
+fold _ _ _   num _ (Num n) = num n
+fold abs app lvl num min (Min n u f) =
+  min n (fold abs app lvl num min u) (fold abs app lvl num min f)
+
+shift :: Int -> Term -> Term
+shift 0 = id
+shift n = fold Abs App (\l -> Lvl $ l + n) Num Min