Initial bounded iteration and unbounded minimization

1 files changed, 34 insertions, 11 deletions

diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index 1fdaa40..f05a606 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -4,9 +4,22 @@ module Data.Mili
   , shift
   ) where
 
-data Term = Abs Term      -- | Abstraction
-          | App Term Term -- | Application
-          | Lvl Int       -- | de Bruijn level
+import           Prelude                 hiding ( abs
+                                                , min
+                                                )
+
+data Nat = Z | S Nat
+
+data Term = Abs Term          -- | Abstraction
+          | App Term Term     -- | Application
+          | Lvl Int           -- | de Bruijn level
+          | Num Nat           -- | Peano numeral
+          | Min Nat Term Term -- | Unbounded minimizer
+          | Itr Nat Term Term -- | Bounded iterator
+
+instance Show Nat where
+  show Z     = "0"
+  show (S n) = show (read (show n) + 1 :: Integer)
 
 instance Show Term where
   showsPrec _ (Abs m) = showString "[" . shows m . showString "]"
@@ -21,6 +34,13 @@ instance Show Term where
       . shows u
       . showString " "
       . shows f
+  showsPrec _ (Itr n u v) =
+    showString "iter "
+      . shows n
+      . showString " "
+      . shows u
+      . showString " "
+      . shows v
 
 fold
   :: (t -> t)
@@ -28,16 +48,19 @@ fold
   -> (Int -> t)
   -> (Nat -> t)
   -> (Nat -> t -> t -> 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)
+fold abs app lvl num min itr (Abs m) = abs (fold abs app lvl num min itr m)
+fold abs app lvl num min itr (App a b) =
+  app (fold abs app lvl num min itr a) (fold abs app lvl num min itr b)
+fold _ _ lvl _   _ _ (Lvl n) = lvl n
+fold _ _ _   num _ _ (Num n) = num n
+fold abs app lvl num min itr (Min n u f) =
+  min n (fold abs app lvl num min itr u) (fold abs app lvl num min itr f)
+fold abs app lvl num min itr (Itr n u v) =
+  min n (fold abs app lvl num min itr u) (fold abs app lvl num min itr v)
 
 shift :: Int -> Term -> Term
 shift 0 = id
-shift n = fold Abs App (\l -> Lvl $ l + n) Num Min
+shift n = fold Abs App (\l -> Lvl $ l + n) Num Min Itr