Remove dead code in preparation for future changes.
parent
d7ae1f1294
commit
1321c7f54e
|
@ -45,15 +45,13 @@ library:
|
||||||
# Explicit import lists are generally a good thing, but I don't want them
|
# Explicit import lists are generally a good thing, but I don't want them
|
||||||
# in certain cases (e.g. importing my own modules, task-specific modules like the parser).
|
# in certain cases (e.g. importing my own modules, task-specific modules like the parser).
|
||||||
- -Wno-missing-import-lists
|
- -Wno-missing-import-lists
|
||||||
# I intentionally include unused top-level bindings
|
|
||||||
# as a way of documenting and explaining concepts.
|
|
||||||
- -Wno-unused-top-binds
|
|
||||||
|
|
||||||
executables:
|
executables:
|
||||||
jtm-lambda-calculus:
|
jtm-lambda-calculus:
|
||||||
main: Main.hs
|
main: Main.hs
|
||||||
source-dirs: app
|
source-dirs: app
|
||||||
ghc-options:
|
ghc-options:
|
||||||
|
- -Wall
|
||||||
- -threaded
|
- -threaded
|
||||||
- -rtsopts
|
- -rtsopts
|
||||||
- -with-rtsopts=-N
|
- -with-rtsopts=-N
|
||||||
|
@ -65,13 +63,11 @@ tests:
|
||||||
main: Spec.hs
|
main: Spec.hs
|
||||||
source-dirs: test
|
source-dirs: test
|
||||||
ghc-options:
|
ghc-options:
|
||||||
|
- -Wall
|
||||||
- -threaded
|
- -threaded
|
||||||
- -rtsopts
|
- -rtsopts
|
||||||
- -with-rtsopts=-N
|
- -with-rtsopts=-N
|
||||||
dependencies:
|
dependencies:
|
||||||
- jtm-lambda-calculus
|
- jtm-lambda-calculus
|
||||||
- generic-random >= 1.2 && < 2
|
|
||||||
- QuickCheck >= 2.14 && < 3
|
|
||||||
- tasty >= 1.2 && < 2
|
- tasty >= 1.2 && < 2
|
||||||
- tasty-hunit >= 0.10 && < 0.11
|
- tasty-hunit >= 0.10 && < 0.11
|
||||||
- tasty-quickcheck >= 0.10.1 && < 0.11
|
|
||||||
|
|
|
@ -3,8 +3,8 @@ module LambdaCalculus
|
||||||
, eval
|
, eval
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Control.Monad.State (State, evalState, modify', state, put, get)
|
import Control.Monad.State (State, evalState, modify', state, put, gets)
|
||||||
import Data.List (elemIndex, find)
|
import Data.List (find)
|
||||||
import Data.Maybe (fromJust)
|
import Data.Maybe (fromJust)
|
||||||
import Data.HashSet (HashSet)
|
import Data.HashSet (HashSet)
|
||||||
import Data.HashSet qualified as HS
|
import Data.HashSet qualified as HS
|
||||||
|
@ -17,46 +17,6 @@ import LambdaCalculus.Expression (Expression (..), foldExpr)
|
||||||
freeVariables :: Expression -> HashSet Text
|
freeVariables :: Expression -> HashSet Text
|
||||||
freeVariables = foldExpr HS.singleton HS.union HS.delete
|
freeVariables = foldExpr HS.singleton HS.union HS.delete
|
||||||
|
|
||||||
-- | Bound variables are variables which are bound by any abstraction in an expression.
|
|
||||||
boundVariables :: Expression -> HashSet Text
|
|
||||||
boundVariables = foldExpr (const HS.empty) HS.union HS.insert
|
|
||||||
|
|
||||||
-- | Return True if the given variable is free in the given expression.
|
|
||||||
freeIn :: Text -> Expression -> Bool
|
|
||||||
freeIn var = foldExpr (== var) (&&) (\name body -> (name == var) || body)
|
|
||||||
|
|
||||||
-- | A closed expression is an expression with no free variables.
|
|
||||||
-- Closed expressions are also known as combinators and are equivalent to terms in combinatory logic.
|
|
||||||
closed :: Expression -> Bool
|
|
||||||
closed = HS.null . freeVariables
|
|
||||||
|
|
||||||
-- | Alpha-equivalent terms differ only by the names of bound variables,
|
|
||||||
-- i.e. one can be converted to the other using only alpha-conversion.
|
|
||||||
alphaEquivalent :: Expression -> Expression -> Bool
|
|
||||||
alphaEquivalent = alphaEquivalent' [] []
|
|
||||||
where
|
|
||||||
alphaEquivalent' :: [Text] -> [Text] -> Expression -> Expression -> Bool
|
|
||||||
alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2)
|
|
||||||
-- Two variables are alpha-equivalent if they are bound in the same location.
|
|
||||||
= bindingSite ctx1 v1 == bindingSite ctx2 v2
|
|
||||||
alphaEquivalent' ctx1 ctx2 (Application ef1 ex1) (Application ef2 ex2)
|
|
||||||
-- Two applications are alpha-equivalent if their components are alpha-equivalent.
|
|
||||||
= alphaEquivalent' ctx1 ctx2 ef1 ef2
|
|
||||||
&& alphaEquivalent' ctx1 ctx2 ex1 ex2
|
|
||||||
alphaEquivalent' ctx1 ctx2 (Abstraction v1 b1) (Abstraction v2 b2)
|
|
||||||
-- Two abstractions are alpha-equivalent if their bodies are alpha-equivalent.
|
|
||||||
= alphaEquivalent' (v1 : ctx1) (v2 : ctx2) b1 b2
|
|
||||||
alphaEquivalent' ctx1 ctx2 (Continuation v1 b1) (Continuation v2 b2)
|
|
||||||
= alphaEquivalent' (v1 : ctx1) (v2 : ctx2) b1 b2
|
|
||||||
alphaEquivalent' _ _ _ _ = False
|
|
||||||
|
|
||||||
-- | The binding site of a variable is either the index of its binder
|
|
||||||
-- or, if it is unbound, the name of the free variable.
|
|
||||||
bindingSite :: [Text] -> Text -> Either Text Int
|
|
||||||
bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx
|
|
||||||
where maybeToRight :: b -> Maybe a -> Either b a
|
|
||||||
maybeToRight default_ = maybe (Left default_) Right
|
|
||||||
|
|
||||||
-- FIXME
|
-- FIXME
|
||||||
quickHack :: Expression -> Expression
|
quickHack :: Expression -> Expression
|
||||||
quickHack (Continuation name body) = Abstraction name body
|
quickHack (Continuation name body) = Abstraction name body
|
||||||
|
@ -93,38 +53,6 @@ substitute var1 value unmodified@(quickHack -> Abstraction var2 body)
|
||||||
free = (`HS.member` env)
|
free = (`HS.member` env)
|
||||||
substitute _ _ _ = error "impossible"
|
substitute _ _ _ = error "impossible"
|
||||||
|
|
||||||
-- | Returns True if the top-level expression is reducible by beta-reduction.
|
|
||||||
betaRedex :: Expression -> Bool
|
|
||||||
betaRedex (Application (quickHack -> (Abstraction _ _)) _) = True
|
|
||||||
betaRedex _ = False
|
|
||||||
|
|
||||||
-- | Returns True if the top-level expression is reducible by eta-reduction.
|
|
||||||
etaRedex :: Expression -> Bool
|
|
||||||
etaRedex (Abstraction var1 (Application ef (Variable var2)))
|
|
||||||
= var1 /= var2 || var1 `freeIn` ef
|
|
||||||
etaRedex _ = False
|
|
||||||
|
|
||||||
-- | In an expression in normal form, all reductions that can be applied have been applied.
|
|
||||||
-- This is the result of applying eager evaluation.
|
|
||||||
normal :: Expression -> Bool
|
|
||||||
-- The expression is beta-reducible.
|
|
||||||
normal (Application (quickHack -> (Abstraction _ _)) _) = False
|
|
||||||
-- The expression is eta-reducible.
|
|
||||||
normal (quickHack -> (Abstraction var1 (Application fe (Variable var2))))
|
|
||||||
= var1 /= var2 || var1 `freeIn` fe
|
|
||||||
normal (Application ef ex) = normal ef && normal ex
|
|
||||||
normal _ = True
|
|
||||||
|
|
||||||
-- | In an expression in weak head normal form, reductions to the function have been applied,
|
|
||||||
-- but not all reductions to the parameter have been applied.
|
|
||||||
-- This is the result of applying lazy evaluation.
|
|
||||||
whnf :: Expression -> Bool
|
|
||||||
whnf (Application (quickHack -> (Abstraction _ _)) _) = False
|
|
||||||
whnf (quickHack -> (Abstraction var1 (Application fe (Variable var2))))
|
|
||||||
= var1 /= var2 || var1 `freeIn` fe
|
|
||||||
whnf (Application ef _) = whnf ef
|
|
||||||
whnf _ = True
|
|
||||||
|
|
||||||
type EvaluatorM a = State Continuation a
|
type EvaluatorM a = State Continuation a
|
||||||
type Evaluator = Expression -> EvaluatorM Expression
|
type Evaluator = Expression -> EvaluatorM Expression
|
||||||
|
|
||||||
|
@ -167,7 +95,7 @@ evaluator unmodified@(Application ef ex)
|
||||||
-- capture the current continuation if requested...
|
-- capture the current continuation if requested...
|
||||||
Variable "callcc" -> do
|
Variable "callcc" -> do
|
||||||
-- Don't worry about variable capture here for now.
|
-- Don't worry about variable capture here for now.
|
||||||
k <- continue (Variable "!") <$> get
|
k <- gets $ continue (Variable "!")
|
||||||
evaluator (Application ex (Continuation "!" k))
|
evaluator (Application ex (Continuation "!" k))
|
||||||
-- otherwise the value is irreducible and we can continue evaluation.
|
-- otherwise the value is irreducible and we can continue evaluation.
|
||||||
_ -> ret unmodified
|
_ -> ret unmodified
|
||||||
|
|
|
@ -1,4 +1,3 @@
|
||||||
{-# LANGUAGE DeriveGeneric #-}
|
|
||||||
module LambdaCalculus.Expression
|
module LambdaCalculus.Expression
|
||||||
( Expression (..), foldExpr
|
( Expression (..), foldExpr
|
||||||
, ast2expr, expr2ast
|
, ast2expr, expr2ast
|
||||||
|
@ -19,7 +18,6 @@ import Data.Bifunctor (first, second)
|
||||||
import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList)
|
import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList)
|
||||||
import Data.Text (Text)
|
import Data.Text (Text)
|
||||||
import Data.Text qualified as T
|
import Data.Text qualified as T
|
||||||
import GHC.Generics (Generic)
|
|
||||||
import LambdaCalculus.Parser.AbstractSyntax (AbstractSyntax)
|
import LambdaCalculus.Parser.AbstractSyntax (AbstractSyntax)
|
||||||
import LambdaCalculus.Parser.AbstractSyntax qualified as AST
|
import LambdaCalculus.Parser.AbstractSyntax qualified as AST
|
||||||
import TextShow (Builder, fromText, TextShow, showb, showt)
|
import TextShow (Builder, fromText, TextShow, showb, showt)
|
||||||
|
@ -36,7 +34,7 @@ data Expression
|
||||||
--
|
--
|
||||||
-- Continuations do not have any corresponding surface-level syntax.
|
-- Continuations do not have any corresponding surface-level syntax.
|
||||||
| Continuation Text Expression
|
| Continuation Text Expression
|
||||||
deriving (Eq, Generic)
|
deriving Eq
|
||||||
|
|
||||||
foldExpr :: (Text -> a) -> (a -> a -> a) -> (Text -> a -> a) -> Expression -> a
|
foldExpr :: (Text -> a) -> (a -> a -> a) -> (Text -> a -> a) -> Expression -> a
|
||||||
foldExpr varf appf absf = foldExpr'
|
foldExpr varf appf absf = foldExpr'
|
||||||
|
@ -85,7 +83,7 @@ viewAbstraction x = ([], x)
|
||||||
|
|
||||||
-- | View left-nested applications as a list.
|
-- | View left-nested applications as a list.
|
||||||
pattern Applications :: [Expression] -> Expression
|
pattern Applications :: [Expression] -> Expression
|
||||||
pattern Applications exprs <- (viewApplication -> (exprs@(_:_:_)))
|
pattern Applications exprs <- (viewApplication -> exprs@(_:_:_))
|
||||||
|
|
||||||
{-# COMPLETE Abstractions, Applications, Continuation, Variable :: Expression #-}
|
{-# COMPLETE Abstractions, Applications, Continuation, Variable :: Expression #-}
|
||||||
|
|
||||||
|
|
12
test/Spec.hs
12
test/Spec.hs
|
@ -1,19 +1,7 @@
|
||||||
import Data.Char (isAlpha)
|
|
||||||
import qualified Data.Text as T
|
|
||||||
import Generic.Random (genericArbitraryRec, uniform)
|
|
||||||
import LambdaCalculus
|
import LambdaCalculus
|
||||||
import LambdaCalculus.Parser
|
import LambdaCalculus.Parser
|
||||||
import Test.QuickCheck
|
|
||||||
import Test.Tasty
|
import Test.Tasty
|
||||||
import Test.Tasty.HUnit
|
import Test.Tasty.HUnit
|
||||||
import Test.Tasty.QuickCheck
|
|
||||||
import TextShow (showt)
|
|
||||||
|
|
||||||
instance Arbitrary Expression where
|
|
||||||
arbitrary = genericArbitraryRec uniform
|
|
||||||
|
|
||||||
instance Arbitrary T.Text where
|
|
||||||
arbitrary = T.pack <$> listOf1 (elements $ ['A'..'Z'] ++ ['a'..'z'])
|
|
||||||
|
|
||||||
-- These are terms which have complex reduction steps and
|
-- These are terms which have complex reduction steps and
|
||||||
-- are likely to catch bugs in the substitution function, if there are any.
|
-- are likely to catch bugs in the substitution function, if there are any.
|
||||||
|
|
Loading…
Reference in New Issue