diff options
| author | Marvin Borner | 2024-11-14 16:54:14 +0100 |
|---|---|---|
| committer | Marvin Borner | 2024-11-14 16:59:59 +0100 |
| commit | 4a6378aa868e9c1d49fc5ad1576616933c913004 (patch) | |
| tree | fb42733e3f774a9716a14b4332d96b503dab769a /src/Data | |
| parent | d7bbded8b0aa3086692b2363076be48c2fbb5a33 (diff) | |
Basic reduction
Diffstat (limited to 'src/Data')
| -rw-r--r-- | src/Data/Mili.hs | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs index ac6703a..9ba832b 100644 --- a/src/Data/Mili.hs +++ b/src/Data/Mili.hs @@ -13,7 +13,7 @@ import Prelude hiding ( abs data Nat = Z | S Term -data Term = Abs Term -- | Abstraction +data Term = Abs Int Term -- | Abstraction with level | App Term Term -- | Application | Lvl Int -- | de Bruijn level | Num Nat -- | Peano numeral @@ -21,10 +21,10 @@ data Term = Abs Term -- | Abstraction instance Show Nat where show Z = "Z" - show (S t) = "S " <> show t + show (S t) = "S(" <> show t <> ")" instance Show Term where - showsPrec _ (Abs m) = showString "[" . shows m . showString "]" + showsPrec _ (Abs _ m) = showString "[" . shows m . showString "]" showsPrec _ (App m n) = showString "(" . shows m . showString " " . shows n . showString ")" showsPrec _ (Lvl i) = shows i @@ -42,14 +42,14 @@ instance Show Term where . shows w fold - :: (Term -> Term) + :: (Int -> Term -> Term) -> (Term -> Term -> Term) -> (Int -> Term) -> (Nat -> Term) -> ((Term, Nat) -> Term -> Term -> Term -> Term) -> Term -> Term -fold abs app lvl num rec (Abs m) = abs $ fold abs app lvl num rec m +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 |