Parse directly to Expr without any intermediate Ast type.
parent
d74f17007a
commit
43e4a77cdc
|
|
@ -3,7 +3,7 @@ module Main where
|
|||
import Control.Monad (forever)
|
||||
import System.IO (hFlush, stdout)
|
||||
import Text.Parsec (parse)
|
||||
import UntypedLambdaCalculus (eval, canonym)
|
||||
import UntypedLambdaCalculus (eval)
|
||||
import UntypedLambdaCalculus.Parser (expr)
|
||||
|
||||
prompt :: String -> IO String
|
||||
|
|
@ -14,7 +14,7 @@ prompt text = do
|
|||
|
||||
main :: IO ()
|
||||
main = forever $ do
|
||||
expr <- parse expr "stdin" <$> prompt ">> "
|
||||
case expr of
|
||||
input <- expr "stdin" <$> prompt ">> "
|
||||
case input of
|
||||
Left parseError -> putStrLn $ "Parse error: " ++ show parseError
|
||||
Right expr -> print $ eval $ canonym expr
|
||||
Right ast -> print $ eval ast
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ dependencies:
|
|||
- parsec >= 3.1 && < 4
|
||||
- recursion-schemes >= 5.1 && < 6
|
||||
- unordered-containers >= 0.2.10 && < 0.3
|
||||
- transformers >= 0.5.6 && < 0.6
|
||||
|
||||
library:
|
||||
source-dirs: src
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses #-}
|
||||
module Data.Fin (Fin (Zero, Succ), finUp, toInt, pred, finRemove) where
|
||||
{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-}
|
||||
module Data.Fin (Fin (Zero, Succ), toInt, pred, finRemove) where
|
||||
|
||||
import Data.Functor.Foldable (Base, Recursive, project, cata)
|
||||
import Data.Injection (Injection, inject)
|
||||
|
|
@ -14,17 +14,13 @@ data Fin n where
|
|||
|
||||
type instance Base (Fin n) = Maybe
|
||||
|
||||
instance (Nat n, Nat m, GTorEQ m n) => Injection (Fin n) (Fin m) where
|
||||
inject = unsafeCoerce
|
||||
|
||||
-- | Coerce a `Fin n` into a `Fin (Succ n)`.
|
||||
finUp :: Nat n => Fin n -> Fin (Succ n)
|
||||
finUp Zero = Zero
|
||||
finUp (Succ n) = Succ (finUp n)
|
||||
instance (Nat n) => Injection (Fin n) (Fin (Succ n)) where
|
||||
inject Zero = Zero
|
||||
inject (Succ n) = Succ (inject n)
|
||||
|
||||
instance (Nat n) => Recursive (Fin n) where
|
||||
project Zero = Nothing
|
||||
project (Succ n) = Just $ finUp n
|
||||
project (Succ n) = Just $ inject n
|
||||
|
||||
instance (Nat n) => Eq (Fin n) where
|
||||
Zero == Zero = True
|
||||
|
|
|
|||
|
|
@ -1,23 +1,27 @@
|
|||
{-# LANGUAGE GADTs, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}
|
||||
module Data.Vec (Vec (Empty, (:.)), (!.), elemIndexVec, vmap) where
|
||||
module Data.Vec (Vec (Empty, (:.)), (!.), elemIndexVec) where
|
||||
|
||||
import Data.Fin (Fin (Zero, Succ))
|
||||
import Data.Type.Nat (Nat, Zero, Succ)
|
||||
|
||||
data Vec a n where
|
||||
Empty :: Vec a Zero
|
||||
(:.) :: Nat n => a -> Vec a n -> Vec a (Succ n)
|
||||
data Vec n a where
|
||||
Empty :: Vec Zero a
|
||||
(:.) :: Nat n => a -> Vec n a -> Vec (Succ n) a
|
||||
|
||||
-- | Equivalent to fmap. It is impossible to implement Functor on Vec for stupid reasons.
|
||||
vmap :: (a -> b) -> Vec a n -> Vec b n
|
||||
vmap _ Empty = Empty
|
||||
vmap f (x :. xs) = f x :. vmap f xs
|
||||
instance Nat n => Functor (Vec n) where
|
||||
fmap _ Empty = Empty
|
||||
fmap f (x :. xs) = f x :. fmap f xs
|
||||
|
||||
(!.) :: Nat n => Vec a n -> Fin n -> a
|
||||
(!.) (x :. _ ) Zero = x
|
||||
(!.) (_ :. xs) (Succ n) = xs !. n
|
||||
instance Nat n => Foldable (Vec n) where
|
||||
foldr _ base Empty = base
|
||||
foldr f base (x :. xs) = x `f` foldr f base xs
|
||||
|
||||
elemIndexVec :: (Eq a, Nat n) => a -> Vec a n -> Maybe (Fin n)
|
||||
(!.) :: Nat n => Vec n a -> Fin n -> a
|
||||
(x :. _ ) !. Zero = x
|
||||
(_ :. xs) !. (Succ n) = xs !. n
|
||||
_ !. _ = error "Impossible"
|
||||
|
||||
elemIndexVec :: (Eq a, Nat n) => a -> Vec n a -> Maybe (Fin n)
|
||||
elemIndexVec _ Empty = Nothing
|
||||
elemIndexVec x (x' :. xs)
|
||||
| x == x' = Just Zero
|
||||
|
|
|
|||
|
|
@ -1,19 +1,11 @@
|
|||
{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
|
||||
module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), canonym, eval, normal, whnf) where
|
||||
{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, MultiParamTypeClasses #-}
|
||||
module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), eval) where
|
||||
|
||||
import Control.Applicative (liftA2)
|
||||
import Control.Monad.Reader (Reader, runReader, ask, local, withReader, reader, asks)
|
||||
import Data.Fin (Fin (Zero, Succ), finUp, finRemove)
|
||||
import Data.Function (fix)
|
||||
import Data.Functor.Foldable (Base, Recursive, Corecursive, ListF (Nil, Cons), cata, embed, project)
|
||||
import Data.Functor.Foldable.TH (makeBaseFunctor)
|
||||
import Data.Injection (inject)
|
||||
import Data.Maybe (fromJust)
|
||||
import Control.Monad.Reader (Reader, runReader, withReader, reader, asks)
|
||||
import Data.Fin (Fin (Zero, Succ), finRemove)
|
||||
import Data.Injection (Injection, inject)
|
||||
import Data.Type.Nat (Nat, Succ, Zero)
|
||||
import Data.Vec (Vec (Empty, (:.)), (!.), vmap, elemIndexVec)
|
||||
import UntypedLambdaCalculus.Parser (Ast (AstVar, AstLam, AstApp))
|
||||
|
||||
type Algebra f a = f a -> a
|
||||
import Data.Vec (Vec (Empty, (:.)), (!.))
|
||||
|
||||
-- | A lambda calculus expression where variables are identified
|
||||
-- | by their distance from their binding site (De Bruijn indices).
|
||||
|
|
@ -22,17 +14,15 @@ data Expr n = Free String
|
|||
| Lam String (Expr (Succ n))
|
||||
| App (Expr n) (Expr n)
|
||||
|
||||
makeBaseFunctor ''Expr
|
||||
|
||||
exprUp :: Nat n => Expr n -> Expr (Succ n)
|
||||
exprUp (Free v) = Free v
|
||||
exprUp (Var v) = Var $ finUp v
|
||||
exprUp (Lam v e) = Lam v $ exprUp e
|
||||
exprUp (App f x) = App (exprUp f) (exprUp x)
|
||||
instance (Nat n) => Injection (Expr n) (Expr (Succ n)) where
|
||||
inject (Free v) = Free v
|
||||
inject (Var v) = Var $ inject v
|
||||
inject (Lam v e) = Lam v $ inject e
|
||||
inject (App f x) = App (inject f) (inject x)
|
||||
|
||||
instance Show (Expr Zero) where
|
||||
show x = runReader (alg x) Empty
|
||||
where alg :: Nat n => Expr n -> Reader (Vec String n) String
|
||||
show expr = runReader (alg expr) Empty
|
||||
where alg :: Nat n => Expr n -> Reader (Vec n String) String
|
||||
alg (Free v) = return v
|
||||
alg (Var v) = reader (\vars -> vars !. v ++ ':' : show v)
|
||||
alg (Lam v e) = do
|
||||
|
|
@ -46,68 +36,40 @@ instance Show (Expr Zero) where
|
|||
-- | Determine whether the variable bound by a lambda expression is used in its body.
|
||||
-- | This is used in eta reduction, where `(\x. f x)` reduces to `f` when `x` is not bound in `f`.
|
||||
unbound :: Nat n => Expr (Succ n) -> Bool
|
||||
unbound x = runReader (alg x) Zero
|
||||
unbound expr = runReader (alg expr) Zero
|
||||
where alg :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) Bool
|
||||
alg (Free _) = return True
|
||||
alg (Var v) = reader (/= v)
|
||||
alg (App f x) = (&&) <$> alg f <*> alg x
|
||||
alg (Lam _ e) = withReader Succ $ alg e
|
||||
|
||||
-- | Convert an Ast into an Expression where all variables have canonical, unique names.
|
||||
-- | Namely, bound variables are identified according to their distance from their binding site
|
||||
-- | (i.e. De Bruijn indices).
|
||||
canonym :: Ast -> Expr Zero
|
||||
canonym x = runReader (alg x) Empty
|
||||
where alg :: Nat n => Ast -> Reader (Vec String n) (Expr n)
|
||||
alg (AstVar v) = maybe (Free v) Var <$> elemIndexVec v <$> ask
|
||||
alg (AstLam v e) = Lam v <$> withReader (v :.) (alg e)
|
||||
alg (AstApp n m) = App <$> alg n <*> alg m
|
||||
|
||||
-- | When we bind a new variable, we enter a new scope.
|
||||
-- | Since variables are identified by their distance from their binder,
|
||||
-- | we must increment them to account for the incremented distance.
|
||||
introduceBindingInExpr :: Nat n => Expr n -> Expr (Succ n)
|
||||
introduceBindingInExpr (Var v) = Var $ Succ v
|
||||
introduceBindingInExpr o@(Lam _ _) = exprUp o
|
||||
introduceBindingInExpr (Free x) = Free x
|
||||
introduceBindingInExpr (App f x) = App (introduceBindingInExpr f) (introduceBindingInExpr x)
|
||||
|
||||
intoEta :: Nat n => Expr (Succ n) -> Expr n
|
||||
intoEta x = runReader (intoEta' x) Zero
|
||||
where intoEta' :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n)
|
||||
intoEta' (Free x) = return $ Free x
|
||||
intoEta' (Var x) = Var <$> fromJust <$> asks (finRemove x)
|
||||
intoEta' (App f x) = App <$> intoEta' f <*> intoEta' x
|
||||
intoEta' (Lam v e) = Lam v <$> withReader Succ (intoEta' e)
|
||||
-- | we must increment them to account for the incremented distance,
|
||||
-- | thus embedding them into the new expression.
|
||||
embed' :: Nat n => Expr n -> Expr (Succ n)
|
||||
embed' (Var v) = Var $ Succ v
|
||||
embed' o@(Lam _ _) = inject o
|
||||
embed' (Free x) = Free x
|
||||
embed' (App f x) = App (embed' f) (embed' x)
|
||||
|
||||
subst :: Nat n => Expr n -> Expr (Succ n) -> Expr n
|
||||
subst val x = runReader (subst' val x) Zero
|
||||
subst value expr = runReader (subst' value expr) Zero
|
||||
where subst' :: Nat n => Expr n -> Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n)
|
||||
subst' _ (Free x) = return $ Free x
|
||||
subst' val (Var x) = maybe val Var <$> asks (finRemove x)
|
||||
subst' val (App f x) = App <$> subst' val f <*> subst' val x
|
||||
subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (introduceBindingInExpr val) e)
|
||||
subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (embed' val) e)
|
||||
|
||||
-- | Evaluate a variable to normal form.
|
||||
-- | Evaluate an expression to normal form.
|
||||
eval :: Nat n => Expr n -> Expr n
|
||||
eval (App f' x) = case eval f' of
|
||||
-- Beta reduction.
|
||||
Lam _ e -> eval $ subst x e
|
||||
f -> App f (eval x)
|
||||
eval o@(Lam _ (App f (Var Zero)))
|
||||
| unbound f = eval $ intoEta f
|
||||
-- Eta reduction. We know that `0` is not bound in `f`,
|
||||
-- so we can simply substitute it for undefined.
|
||||
| unbound f = eval $ subst undefined f
|
||||
| otherwise = o
|
||||
eval o = o
|
||||
|
||||
-- | Is an expression in normal form?
|
||||
normal :: Nat n => Expr n -> Bool
|
||||
normal (App (Lam _ _) _) = False
|
||||
normal (Lam _ (App f (Var Zero))) = unbound f
|
||||
normal (App f x) = normal f && normal x
|
||||
normal _ = True
|
||||
|
||||
-- | Is an expression in weak head normal form?
|
||||
whnf :: Nat n => Expr n -> Bool
|
||||
whnf (App (Lam _ _) _) = False
|
||||
whnf (Lam _ (App f (Var Zero))) = unbound f
|
||||
whnf (App f _) = whnf f
|
||||
whnf _ = True
|
||||
|
|
|
|||
|
|
@ -1,82 +1,71 @@
|
|||
{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
|
||||
module UntypedLambdaCalculus.Parser ( Ast (AstVar, AstLam, AstApp)
|
||||
, AstF (AstVarF, AstLamF, AstAppF)
|
||||
, expr
|
||||
) where
|
||||
module UntypedLambdaCalculus.Parser (expr) where
|
||||
|
||||
import Data.Functor.Foldable (cata)
|
||||
import Data.Functor.Foldable.TH (makeBaseFunctor,)
|
||||
import Control.Applicative (liftA)
|
||||
import Control.Monad.Reader (ReaderT, runReaderT, withReaderT, mapReaderT, ask)
|
||||
import Control.Monad.Trans.Class (lift)
|
||||
import Data.Functor (void)
|
||||
import Data.List (foldl1')
|
||||
import Text.Parsec
|
||||
import Text.Parsec.String
|
||||
import Data.Type.Nat (Nat, Zero )
|
||||
import Data.Vec (Vec (Empty, (:.)), elemIndexVec)
|
||||
import Text.Parsec hiding (Empty)
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
import UntypedLambdaCalculus (Expr (Free, Var, Lam, App))
|
||||
|
||||
-- | The abstract syntax tree of lambda calculus.
|
||||
data Ast = AstVar String
|
||||
| AstLam String Ast
|
||||
| AstApp Ast Ast
|
||||
| AstLet String Ast Ast
|
||||
|
||||
makeBaseFunctor ''Ast
|
||||
|
||||
instance Show Ast where
|
||||
show = cata alg
|
||||
where alg (AstVarF v) = v
|
||||
alg (AstLamF v e) = "(\\" ++ v ++ ". " ++ e ++ ")"
|
||||
alg (AstAppF f x) = "(" ++ f ++ " " ++ x ++ ")"
|
||||
|
||||
somespaces :: Parser ()
|
||||
somespaces = skipMany1 space
|
||||
type Parser s a = ReaderT s (Parsec String ()) a
|
||||
|
||||
-- | A variable name.
|
||||
name :: Parser String
|
||||
name :: Parsec String () String
|
||||
name = do
|
||||
c <- letter
|
||||
cs <- many alphaNum
|
||||
return $ c : cs
|
||||
|
||||
-- | A variable expression.
|
||||
var :: Parser Ast
|
||||
var = AstVar <$> name
|
||||
var :: Nat n => Parser (Vec n String) (Expr n)
|
||||
var = do
|
||||
varn <- lift name
|
||||
bound <- ask
|
||||
return $ maybe (Free varn) Var $ elemIndexVec varn bound
|
||||
|
||||
-- | Run parser between parentheses.
|
||||
parens :: Parser a -> Parser a
|
||||
parens = between (char '(') (char ')')
|
||||
|
||||
let_ :: Parser Ast
|
||||
let_ = do
|
||||
string ".let"
|
||||
somespaces
|
||||
v <- name
|
||||
somespaces
|
||||
char '='
|
||||
somespaces
|
||||
x <- safeExpr
|
||||
somespaces
|
||||
string ".in"
|
||||
e <- expr
|
||||
return $ AstApp (AstLam v e) x
|
||||
parens :: Parsec String () a -> Parsec String () a
|
||||
parens p = do
|
||||
_ <- char '('
|
||||
x <- p
|
||||
_ <- char ')'
|
||||
return x
|
||||
|
||||
-- | A lambda expression.
|
||||
lam :: Parser Ast
|
||||
lam :: Nat n => Parser (Vec n String) (Expr n)
|
||||
lam = do
|
||||
char '\\'
|
||||
vars <- name `sepBy1` spaces
|
||||
char '.'
|
||||
spaces
|
||||
body <- expr
|
||||
return $ foldr AstLam body vars
|
||||
vars <- lift $ do
|
||||
_ <- char '\\'
|
||||
vars <- name `sepBy1` spaces
|
||||
_ <- char '.'
|
||||
spaces
|
||||
return vars
|
||||
help vars
|
||||
where help :: Nat n => [String] -> Parser (Vec n String) (Expr n)
|
||||
help [] = app
|
||||
help (v:vs) = Lam v <$> withReaderT (v :.) (help vs)
|
||||
|
||||
-- | An application expression.
|
||||
app :: Parser Ast
|
||||
app = foldl1' AstApp <$> sepBy1 safeExpr spaces
|
||||
app :: Nat n => Parser (Vec n String) (Expr n)
|
||||
app = foldl1' App <$> mapReaderT (`sepBy1` spaces) safeExpr
|
||||
|
||||
ll :: (Parsec String () a -> Parsec String () b -> Parsec String () c) -> Parser s a -> Parser s b -> Parser s c
|
||||
ll f p1 p2 = do
|
||||
bound <- ask
|
||||
lift $ f (runReaderT p1 bound) (runReaderT p2 bound)
|
||||
|
||||
-- | An expression, but where applications must be surrounded by parentheses,
|
||||
-- | to avoid ambiguity (infinite recursion on `app` in the case where the first
|
||||
-- | expression in the application is also an `app`, consuming no input).
|
||||
safeExpr :: Parser Ast
|
||||
safeExpr = var <|> lam <|> parens (lam <|> app)
|
||||
safeExpr :: Nat n => Parser (Vec n String) (Expr n)
|
||||
safeExpr = ll (<|>) var $ ll (<|>) lam $ mapReaderT parens (ll (<|>) lam app)
|
||||
|
||||
-- | Since applications do not require parentheses and can contain only a single item,
|
||||
-- | the `app` parser is sufficient to parse any expression at all.
|
||||
expr :: Parser Ast
|
||||
expr = app
|
||||
expr :: SourceName -> String -> Either ParseError (Expr Zero)
|
||||
expr sourceName code = parse (runReaderT app Empty) sourceName code
|
||||
|
|
|
|||
Loading…
Reference in New Issue