Unbounded iteration

1 files changed, 37 insertions, 37 deletions

diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index f05a606..ac6703a 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -1,5 +1,8 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
 module Data.Mili
   ( Term(..)
+  , Nat(..)
   , fold
   , shift
   ) where
@@ -8,18 +11,17 @@ import           Prelude                 hiding ( abs
                                                 , min
                                                 )
 
-data Nat = Z | S Nat
+data Nat = Z | S Term
 
-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
+data Term = Abs Term                       -- | Abstraction
+          | App Term Term                  -- | Application
+          | Lvl Int                        -- | de Bruijn level
+          | Num Nat                        -- | Peano numeral
+          | Rec (Term, Nat) Term Term Term -- | Unbounded iteration
 
 instance Show Nat where
-  show Z     = "0"
-  show (S n) = show (read (show n) + 1 :: Integer)
+  show Z     = "Z"
+  show (S t) = "S " <> show t
 
 instance Show Term where
   showsPrec _ (Abs m) = showString "[" . shows m . showString "]"
@@ -27,40 +29,38 @@ instance Show Term where
     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
-  showsPrec _ (Itr n u v) =
-    showString "iter "
+  showsPrec _ (Rec (n, t) u v w) =
+    showString "REC ("
       . shows n
-      . showString " "
+      . showString ", "
+      . shows t
+      . showString "), "
       . shows u
-      . showString " "
+      . showString ", "
       . shows v
+      . showString ", "
+      . shows w
 
 fold
-  :: (t -> t)
-  -> (t -> t -> t)
-  -> (Int -> t)
-  -> (Nat -> t)
-  -> (Nat -> t -> t -> t)
-  -> (Nat -> t -> t -> t)
+  :: (Term -> Term)
+  -> (Term -> Term -> Term)
+  -> (Int -> Term)
+  -> (Nat -> Term)
+  -> ((Term, Nat) -> Term -> Term -> Term -> Term)
+  -> Term
   -> Term
-  -> t
-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)
+fold abs app lvl num rec (Abs m) = abs $ 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 (t, n) u v w) = rec
+  (fold abs app lvl num rec t, n) -- TODO: t'
+  (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 Min Itr
+shift n = fold Abs App (\l -> Lvl $ l + n) Num Rec