Use Text instead of String in expressions.
parent
25658f370a
commit
3fd494a398
|
@ -2,15 +2,17 @@
|
||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
import Control.Monad (forever)
|
import Control.Monad (forever)
|
||||||
|
import Data.Text
|
||||||
|
import qualified Data.Text.IO as TIO
|
||||||
import LambdaCalculus.Expression (lazyEval)
|
import LambdaCalculus.Expression (lazyEval)
|
||||||
import LambdaCalculus.Parser (parseExpression)
|
import LambdaCalculus.Parser (parseExpression)
|
||||||
import System.IO (hFlush, stdout)
|
import System.IO (hFlush, stdout)
|
||||||
|
|
||||||
prompt :: String -> IO String
|
prompt :: Text -> IO Text
|
||||||
prompt text = do
|
prompt text = do
|
||||||
putStr text
|
TIO.putStr text
|
||||||
hFlush stdout
|
hFlush stdout
|
||||||
getLine
|
TIO.getLine
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = forever $ parseExpression <$> prompt ">> " >>= \case
|
main = forever $ parseExpression <$> prompt ">> " >>= \case
|
||||||
|
|
|
@ -12,9 +12,14 @@ description: Please see the README on GitHub at <https://github.com/jame
|
||||||
extra-source-files:
|
extra-source-files:
|
||||||
- README.md
|
- README.md
|
||||||
|
|
||||||
|
default-extensions:
|
||||||
|
- OverloadedStrings
|
||||||
|
|
||||||
dependencies:
|
dependencies:
|
||||||
- base >= 4.12 && < 5
|
- base >= 4.12 && < 5
|
||||||
- parsec >= 3.1 && < 4
|
- parsec >= 3.1 && < 4
|
||||||
|
- text >= 1.2 && < 2
|
||||||
|
- text-show >= 3.8 && < 4
|
||||||
- unordered-containers >= 0.2.10 && < 0.3
|
- unordered-containers >= 0.2.10 && < 0.3
|
||||||
|
|
||||||
library:
|
library:
|
||||||
|
|
|
@ -5,33 +5,39 @@ import Data.List (elemIndex, find)
|
||||||
import Data.Maybe (fromJust)
|
import Data.Maybe (fromJust)
|
||||||
import Data.HashSet (HashSet)
|
import Data.HashSet (HashSet)
|
||||||
import qualified Data.HashSet as HS
|
import qualified Data.HashSet as HS
|
||||||
|
import Data.Text (Text)
|
||||||
|
import qualified Data.Text as T
|
||||||
import GHC.Generics (Generic)
|
import GHC.Generics (Generic)
|
||||||
|
import TextShow
|
||||||
|
|
||||||
data Expression
|
data Expression
|
||||||
= Variable String
|
= Variable Text
|
||||||
| Application Expression Expression
|
| Application Expression Expression
|
||||||
| Abstraction String Expression
|
| Abstraction Text Expression
|
||||||
deriving (Eq, Generic)
|
deriving (Eq, Generic)
|
||||||
|
|
||||||
|
instance TextShow Expression where
|
||||||
|
showb (Variable var) = fromText var
|
||||||
|
showb (Application ef ex) = "(" <> showb ef <> " " <> showb ex <> ")"
|
||||||
|
showb (Abstraction var body) = "(^" <> fromText var <> "." <> showb body <> ")"
|
||||||
|
|
||||||
instance Show Expression where
|
instance Show Expression where
|
||||||
show (Variable var) = var
|
show = T.unpack . showt
|
||||||
show (Application ef ex) = "(" ++ show ef ++ " " ++ show ex ++ ")"
|
|
||||||
show (Abstraction var body) = "(^" ++ var ++ "." ++ show body ++ ")"
|
|
||||||
|
|
||||||
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
|
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
|
||||||
freeVariables :: Expression -> HashSet String
|
freeVariables :: Expression -> HashSet Text
|
||||||
freeVariables (Variable variable) = HS.singleton variable
|
freeVariables (Variable variable) = HS.singleton variable
|
||||||
freeVariables (Application ef ex) = freeVariables ef `HS.union` freeVariables ex
|
freeVariables (Application ef ex) = freeVariables ef `HS.union` freeVariables ex
|
||||||
freeVariables (Abstraction variable body) = HS.delete variable $ freeVariables body
|
freeVariables (Abstraction variable body) = HS.delete variable $ freeVariables body
|
||||||
|
|
||||||
-- | Return True if the given variable is free in the given expression.
|
-- | Return True if the given variable is free in the given expression.
|
||||||
freeIn :: String -> Expression -> Bool
|
freeIn :: Text -> Expression -> Bool
|
||||||
freeIn var1 (Variable var2) = var1 == var2
|
freeIn var1 (Variable var2) = var1 == var2
|
||||||
freeIn var (Application ef ex) = var `freeIn` ef && var `freeIn` ex
|
freeIn var (Application ef ex) = var `freeIn` ef && var `freeIn` ex
|
||||||
freeIn var1 (Abstraction var2 body) = var1 == var2 || var1 `freeIn` body
|
freeIn var1 (Abstraction var2 body) = var1 == var2 || var1 `freeIn` body
|
||||||
|
|
||||||
-- | Bound variables are variables which are bound by any abstraction in an expression.
|
-- | Bound variables are variables which are bound by any abstraction in an expression.
|
||||||
boundVariables :: Expression -> HashSet String
|
boundVariables :: Expression -> HashSet Text
|
||||||
boundVariables (Variable _) = HS.empty
|
boundVariables (Variable _) = HS.empty
|
||||||
boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
|
boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
|
||||||
boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
|
boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
|
||||||
|
@ -45,7 +51,7 @@ closed = HS.null . freeVariables
|
||||||
-- i.e. one can be converted to the other using only alpha-conversion.
|
-- i.e. one can be converted to the other using only alpha-conversion.
|
||||||
alphaEquivalent :: Expression -> Expression -> Bool
|
alphaEquivalent :: Expression -> Expression -> Bool
|
||||||
alphaEquivalent = alphaEquivalent' [] []
|
alphaEquivalent = alphaEquivalent' [] []
|
||||||
where alphaEquivalent' :: [String] -> [String] -> Expression -> Expression -> Bool
|
where alphaEquivalent' :: [Text] -> [Text] -> Expression -> Expression -> Bool
|
||||||
alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2)
|
alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2)
|
||||||
-- Two variables are alpha-equivalent if they are bound in the same location.
|
-- Two variables are alpha-equivalent if they are bound in the same location.
|
||||||
= bindingSite ctx1 v1 == bindingSite ctx2 v2
|
= bindingSite ctx1 v1 == bindingSite ctx2 v2
|
||||||
|
@ -59,13 +65,13 @@ alphaEquivalent = alphaEquivalent' [] []
|
||||||
|
|
||||||
-- | The binding site of a variable is either the index of its binder
|
-- | The binding site of a variable is either the index of its binder
|
||||||
-- or, if it is unbound, the name of the free variable.
|
-- or, if it is unbound, the name of the free variable.
|
||||||
bindingSite :: [String] -> String -> Either String Int
|
bindingSite :: [Text] -> Text -> Either Text Int
|
||||||
bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx
|
bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx
|
||||||
where maybeToRight :: b -> Maybe a -> Either b a
|
where maybeToRight :: b -> Maybe a -> Either b a
|
||||||
maybeToRight default_ = maybe (Left default_) Right
|
maybeToRight default_ = maybe (Left default_) Right
|
||||||
|
|
||||||
-- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression.
|
-- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression.
|
||||||
substitute :: String -> Expression -> Expression -> Expression
|
substitute :: Text -> Expression -> Expression -> Expression
|
||||||
substitute var1 value unmodified@(Variable var2)
|
substitute var1 value unmodified@(Variable var2)
|
||||||
| var1 == var2 = value
|
| var1 == var2 = value
|
||||||
| otherwise = unmodified
|
| otherwise = unmodified
|
||||||
|
@ -74,11 +80,17 @@ substitute var value (Application ef ex)
|
||||||
substitute var1 value unmodified@(Abstraction var2 body)
|
substitute var1 value unmodified@(Abstraction var2 body)
|
||||||
| var1 == var2 = unmodified
|
| var1 == var2 = unmodified
|
||||||
| otherwise = Abstraction var2' $ substitute var1 value $ alphaConvert var2 var2' body
|
| otherwise = Abstraction var2' $ substitute var1 value $ alphaConvert var2 var2' body
|
||||||
where var2' = escapeName (freeVariables value) var2
|
where var2' :: Text
|
||||||
|
var2' = escapeName (freeVariables value) var2
|
||||||
|
|
||||||
|
alphaConvert :: Text -> Text -> Expression -> Expression
|
||||||
alphaConvert oldName newName expr = substitute oldName (Variable newName) expr
|
alphaConvert oldName newName expr = substitute oldName (Variable newName) expr
|
||||||
-- | Generate a new name which isn't present in the set, based on the old name.
|
-- | Generate a new name which isn't present in the set, based on the old name.
|
||||||
|
escapeName :: HashSet Text -> Text -> Text
|
||||||
escapeName env name = fromJust $ find (not . free) names
|
escapeName env name = fromJust $ find (not . free) names
|
||||||
where names = name : map ('\'' :) names
|
where names :: [Text]
|
||||||
|
names = name : map (`T.snoc` '\'') names
|
||||||
|
free :: Text -> Bool
|
||||||
free = (`HS.member` env)
|
free = (`HS.member` env)
|
||||||
|
|
||||||
-- | Returns True if the top-level expression is reducible by beta-reduction.
|
-- | Returns True if the top-level expression is reducible by beta-reduction.
|
||||||
|
|
|
@ -2,15 +2,17 @@ module LambdaCalculus.Parser (parseExpression) where
|
||||||
|
|
||||||
import Control.Applicative ((*>))
|
import Control.Applicative ((*>))
|
||||||
import Control.Monad (void)
|
import Control.Monad (void)
|
||||||
import LambdaCalculus.Expression (Expression (Variable, Application, Abstraction))
|
import Data.Text (Text)
|
||||||
|
import qualified Data.Text as T
|
||||||
|
import LambdaCalculus.Expression
|
||||||
import Text.Parsec hiding (spaces)
|
import Text.Parsec hiding (spaces)
|
||||||
import Text.Parsec.String
|
import Text.Parsec.Text
|
||||||
|
|
||||||
spaces :: Parser ()
|
spaces :: Parser ()
|
||||||
spaces = void $ many1 space
|
spaces = void $ many1 space
|
||||||
|
|
||||||
variableName :: Parser String
|
variableName :: Parser Text
|
||||||
variableName = many1 letter
|
variableName = T.pack <$> many1 letter
|
||||||
|
|
||||||
variable :: Parser Expression
|
variable :: Parser Expression
|
||||||
variable = Variable <$> variableName
|
variable = Variable <$> variableName
|
||||||
|
@ -33,5 +35,5 @@ abstraction = do
|
||||||
expression :: Parser Expression
|
expression :: Parser Expression
|
||||||
expression = abstraction <|> application <|> variable
|
expression = abstraction <|> application <|> variable
|
||||||
|
|
||||||
parseExpression :: String -> Either ParseError Expression
|
parseExpression :: Text -> Either ParseError Expression
|
||||||
parseExpression = parse (expression <* eof) "input"
|
parseExpression code = parse (expression <* eof) "input" code
|
||||||
|
|
13
test/Spec.hs
13
test/Spec.hs
|
@ -1,4 +1,5 @@
|
||||||
import Data.Char (isAlpha)
|
import Data.Char (isAlpha)
|
||||||
|
import qualified Data.Text as T
|
||||||
import Generic.Random (genericArbitraryRec, uniform)
|
import Generic.Random (genericArbitraryRec, uniform)
|
||||||
import LambdaCalculus.Expression
|
import LambdaCalculus.Expression
|
||||||
import LambdaCalculus.Parser
|
import LambdaCalculus.Parser
|
||||||
|
@ -6,10 +7,14 @@ import Test.QuickCheck
|
||||||
import Test.Tasty
|
import Test.Tasty
|
||||||
import Test.Tasty.HUnit
|
import Test.Tasty.HUnit
|
||||||
import Test.Tasty.QuickCheck
|
import Test.Tasty.QuickCheck
|
||||||
|
import TextShow (showt)
|
||||||
|
|
||||||
instance Arbitrary Expression where
|
instance Arbitrary Expression where
|
||||||
arbitrary = genericArbitraryRec uniform
|
arbitrary = genericArbitraryRec uniform
|
||||||
|
|
||||||
|
instance Arbitrary T.Text where
|
||||||
|
arbitrary = T.pack <$> listOf1 (elements $ ['A'..'Z'] ++ ['a'..'z'])
|
||||||
|
|
||||||
dfi :: Expression
|
dfi :: Expression
|
||||||
dfi = Application d (Application f i)
|
dfi = Application d (Application f i)
|
||||||
where d = Abstraction "x" $ Application (Variable "x") (Variable "x")
|
where d = Abstraction "x" $ Application (Variable "x") (Variable "x")
|
||||||
|
@ -31,13 +36,7 @@ ttttt = Application (Application (Application f t) (Abstraction "x" (Variable "x
|
||||||
(Variable "x")
|
(Variable "x")
|
||||||
|
|
||||||
prop_parseExpression_inverse :: Expression -> Bool
|
prop_parseExpression_inverse :: Expression -> Bool
|
||||||
prop_parseExpression_inverse expr' = Right expr == parseExpression (show expr)
|
prop_parseExpression_inverse expr = Right expr == parseExpression (showt expr)
|
||||||
where expr = legalizeVariables expr'
|
|
||||||
legalizeVariables (Variable var) = Variable $ legalVar var
|
|
||||||
legalizeVariables (Application ef ex) = Application (legalizeVariables ef) (legalizeVariables ex)
|
|
||||||
legalizeVariables (Abstraction var body) = Abstraction (legalVar var) $ legalizeVariables body
|
|
||||||
legalVar var = 'v' : filter isAlpha var
|
|
||||||
|
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = defaultMain $
|
main = defaultMain $
|
||||||
|
|
Loading…
Reference in New Issue