diff options
| author | Marvin Borner | 2024-11-15 01:37:12 +0100 |
|---|---|---|
| committer | Marvin Borner | 2024-11-15 01:37:12 +0100 |
| commit | 292789f61f0b85439036bd3cb60fd52f011fdcf2 (patch) | |
| tree | 4c243e9450bad1152cbc067795c95d5306a8a6f5 /src/Data/Mili.hs | |
| parent | 4a6378aa868e9c1d49fc5ad1576616933c913004 (diff) | |
Fix reducer and examples
Diffstat (limited to 'src/Data/Mili.hs')
| -rw-r--r-- | src/Data/Mili.hs | 28 |
1 files changed, 14 insertions, 14 deletions
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 |