From 292789f61f0b85439036bd3cb60fd52f011fdcf2 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Fri, 15 Nov 2024 01:37:12 +0100
Subject: Fix reducer and examples

---
 src/Data/Mili.hs | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'src/Data')

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
-- 
cgit v1.2.3