Skip to content

Commit

Permalink
Derive IsString for the Name newtype
Browse files Browse the repository at this point in the history
  • Loading branch information
severen committed Jul 3, 2024
1 parent 2cb7494 commit 006e7c6
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 20 deletions.
13 changes: 7 additions & 6 deletions src/Sly/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ module Sly.Syntax (
fromChurchBool,
) where

import Data.String (IsString)
import Data.String.Interpolate (i)
import Data.Text (Text)

Expand All @@ -22,7 +23,7 @@ import Data.Text qualified as T
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)
newtype Name = Name Text deriving (Eq, Ord, Show, IsString)

-- | A program statement.
data Statement
Expand Down Expand Up @@ -74,9 +75,9 @@ astShow = T.unpack . go
-- | Convert a nonnegative integer into a Church numeral term.
toChurchNat :: Int -> Term
toChurchNat n =
Abs (Name "s") $
Abs (Name "z") $
iterate (App (Var $ Name "s")) (Var $ Name "z") !! 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.
Expand All @@ -92,8 +93,8 @@ fromChurchNat _ = Nothing

-- | Convert a Boolean into a Church Boolean term.
toChurchBool :: Bool -> Term
toChurchBool True = Abs (Name "t") $ Abs (Name "f") $ Var (Name "t")
toChurchBool False = Abs (Name "t") $ Abs (Name "f") $ Var (Name "f")
toChurchBool 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 Bool
Expand Down
27 changes: 13 additions & 14 deletions tests/UnitTests.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ import Test.Tasty.Hspec

import Sly.Eval (hnf, whnf)
import Sly.Syntax (
Name (..),
Term (..),
fromChurchNat,
toChurchNat,
Expand All @@ -21,53 +20,53 @@ unitTests :: IO TestTree
unitTests = testSpec "Unit Tests" do
describe "Church Numerals" do
it "0 == \\s z -> z" do
let zero = Abs (Name "s") $ Abs (Name "z") (Var $ Name "z")
let zero = Abs "s" $ Abs "z" (Var "z")
toChurchNat 0 `shouldBe` zero
fromChurchNat zero `shouldBe` Just 0

it "1 == \\s z -> s z" do
let one = Abs (Name "s") $ Abs (Name "z") $ App (Var $ Name "s") (Var $ Name "z")
let one = Abs "s" $ Abs "z" $ App (Var "s") (Var "z")
toChurchNat 1 `shouldBe` one
fromChurchNat one `shouldBe` Just 1

it "2 == \\s z -> s (s z)" do
let two =
Abs (Name "s") $
Abs (Name "z") $
App (Var $ Name "s") (App (Var $ Name "s") (Var $ Name "z"))
Abs "s" $
Abs "z" $
App (Var "s") (App (Var "s") (Var "z"))
toChurchNat 2 `shouldBe` two
fromChurchNat two `shouldBe` Just 2

describe "Church Booleans" do
it "#t == \\t f -> t" do
let true = Abs (Name "t") $ Abs (Name "f") $ Var (Name "t")
let true = Abs "t" $ Abs "f" (Var "t")
toChurchBool True `shouldBe` true
fromChurchBool true `shouldBe` Just True

it "#f == \\t f -> f" do
let false = Abs (Name "t") $ Abs (Name "f") $ Var (Name "f")
let false = Abs "t" $ Abs "f" (Var "f")
toChurchBool False `shouldBe` false
fromChurchBool false `shouldBe` Just False

describe "Evaluator" do
let x = (Var $ Name "x")
let x = (Var "x")
in do
it "hnf x == x" $ hnf x `shouldBe` x
it "whnf x == x" $ whnf x `shouldBe` x

let f = Abs (Name "x") $ App (Var $ Name "x") (Var $ Name "y")
let f = Abs "x" $ App (Var "x") (Var "y")
in do
it "hnf (\\x -> x y) == \\x -> x y" $ hnf f `shouldBe` f
it "whnf (\\x -> x y) == \\x -> x y" $ whnf f `shouldBe` f

let t = App (Var $ Name "x") (Var $ Name "y")
let t = App (Var "x") (Var "y")
in do
it "hnf (x y) == x y" $ hnf t `shouldBe` t
it "whnf (x y) == x y" $ whnf t `shouldBe` t

let f = Var $ Name "f"
g = Abs (Name "x") $ App (Var $ Name "f") (Var $ Name "x")
y = Var $ Name "y"
let f = Var "f"
g = Abs "x" $ App (Var "f") (Var "x")
y = Var "y"
t = App g y
in do
it "hnf ((\\x -> f x) y) == f y" $ hnf t `shouldBe` App f y
Expand Down

0 comments on commit 006e7c6

Please sign in to comment.