Something went wrong. Try again.
A cunning interpreter for the pure untyped λ-calculus.
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104-- SPDX-FileCopyrightText: 2022 Severen Redwood <sev@severen.dev>-- SPDX-License-Identifier: GPL-3.0-or-later
module Sly.Syntax ( Name (..), Statement (..), Term (..), astShow, toChurchNat, fromChurchNat, toChurchBool, fromChurchBool, )where
import Data.String (IsString)import Data.String.Interpolate (i)import Data.Text (Text)import Data.Text qualified as T
-- | A name in a program.---- A name is an identifier that is either used as a variable or an identifier to which an-- arbitrary term is bound.newtype Name = Name Text deriving (Eq, Ord, Show, IsString)
-- | A program statement.data Statement = -- | A λ-term. Term Term | -- | An assignment of a name to a λ-term. Ass {-# UNPACK #-} !Name Term deriving (Eq)
instance Show Statement where show (Term t) = show t <> "." show (Ass (Name n) t) = T.unpack [i|let #{n} := #{T.pack (show t)}.|]
-- | A λ-term.data Term = -- | A variable. Var {-# UNPACK #-} !Name | -- | A λ-abstraction. Abs {-# UNPACK #-} !Name Term | -- | An application of a λ-abstraction. App Term Term deriving (Eq)
instance Show Term where show = T.unpack . go where go :: Term -> Text go (Var (Name n)) = n go (Abs (Name n) body) = "λ" <> n <> slurp body go (App l@(Abs _ _) r@(Abs _ _)) = [i|(#{go l}) (#{go r})|] go (App l@(Abs _ _) r) = [i|(#{go l}) #{go r}|] go (App l r@(Abs _ _)) = [i|#{go l} (#{go r})|] go (App l r@(App _ _)) = [i|#{go l} (#{go r})|] go (App l r) = [i|#{go l} #{go r}|]
-- Slurp up λ-abstractions! slurp :: Term -> Text slurp (Abs (Name n) body) = " " <> n <> slurp body slurp body = " -> " <> go body
-- | Like regular show, but displays the term fully bracketed.astShow :: Term -> StringastShow = T.unpack . go where go (Var (Name n)) = n go (Abs (Name n) t) = [i|(λ#{n} -> #{go t})|] go (App l r) = [i|(#{go l} #{go r})|]
-- | Convert a nonnegative integer into a Church numeral term.toChurchNat :: Int -> TermtoChurchNat n = Abs "s" $ Abs "z" $ iterate (App (Var "s")) (Var "z") !! n
-- | Convert a term into a nonnegative integer if it has the shape of a Church-- numeral.fromChurchNat :: Term -> Maybe IntfromChurchNat (Abs f (Abs x body)) = go 0 body where go :: Int -> Term -> Maybe Int go n = \case Var y | y == x -> Just n App (Var g) t | g == f -> go (n + 1) t _ -> NothingfromChurchNat _ = Nothing
-- | Convert a Boolean into a Church Boolean term.toChurchBool :: Bool -> TermtoChurchBool True = Abs "t" $ Abs "f" (Var "t")toChurchBool False = Abs "t" $ Abs "f" (Var "f")
-- | Convert a term into a Boolean if it has the shape of a Church Boolean.fromChurchBool :: Term -> Maybe BoolfromChurchBool (Abs t (Abs f (Var x))) | x == t = Just True | x == f = Just FalsefromChurchBool _ = Nothing