Lots of changes. First working version

This commit is contained in:
Raphael Jacobs 2022-04-04 11:11:55 +02:00
parent 299c128bbc
commit 4997f9fb3d
11 changed files with 383 additions and 171 deletions

View File

@ -1,6 +1,6 @@
cabal-version: 1.12
-- This file has been generated from package.yaml by hpack version 0.34.4.
-- This file has been generated from package.yaml by hpack version 0.34.6.
--
-- see: https://github.com/sol/hpack
@ -19,19 +19,24 @@ extra-source-files:
library
exposed-modules:
GenericLambda
Lib
Parser
UL0Parser
UntypedLambda
UntypedLambdaExec
other-modules:
Paths_lambdatest
hs-source-dirs:
src
src/Untyped-0
build-depends:
attoparsec
, base >=4.7 && <5
, bytestring
, cleff
, containers
, haskeline
, mtl
, repline
, text
default-language: Haskell2010
executable lambdatest-exe
@ -46,10 +51,12 @@ executable lambdatest-exe
build-depends:
attoparsec
, base >=4.7 && <5
, bytestring
, cleff
, containers
, haskeline
, lambdatest
, mtl
, repline
, text
default-language: Haskell2010
test-suite lambdatest-test
@ -63,8 +70,10 @@ test-suite lambdatest-test
build-depends:
attoparsec
, base >=4.7 && <5
, bytestring
, cleff
, containers
, haskeline
, lambdatest
, mtl
, repline
, text
default-language: Haskell2010

16
lib/stdlib.lambda Normal file
View File

@ -0,0 +1,16 @@
id = λx.x
pair = λc x y.c x y
fst = λx y.x
snd = λx y.y
if = pair
true = fst
false = snd
zero = λf.λx.x
succ = λn.λf.λx.f (n f x)
plus = λm.λn.λf.λx.m f (n f x)

View File

@ -21,13 +21,18 @@ description: Please see the README on GitHub at <https://github.com/gith
dependencies:
- base >= 4.7 && < 5
- cleff
- attoparsec
- bytestring
- containers
- text
- repline
- haskeline
# - transformers
- mtl
library:
source-dirs: src
source-dirs:
- src
- src/Untyped-0
executables:
lambdatest-exe:

23
src/GenericLambda.hs Normal file
View File

@ -0,0 +1,23 @@
{-# LANGUAGE TypeFamilies #-}
module GenericLambda where
-- dumb attempt to generalize my lambda calculus functions
-- data instance Lambda UntypedLambda = UL UL.Environment UL.Expression UL.
class GenericLambda l where
data Env l
type Iden l
type Data l
data PRes l
emptyEnv :: Env l
updateEnv :: Env l -> Iden l -> Data l -> Env l
envStrings :: Env l -> [(String, String)]
normalform :: Env l -> Data l -> Either String String
execLine :: Env l -> String -> IO (Maybe String, Env l)
evalPrint' :: (GenericLambda l) => Env l -> Data l -> String
evalPrint' en ex = case normalform en ex of
Right res -> "-> " ++ res
Left err -> err

View File

@ -1,45 +1,85 @@
-- {-# LANGUAGE DataKinds, GADTs, TemplateHaskell, TypeOperators #-}
-- {-# LANGUAGE KindSignatures #-}
-- {-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
module Lib
( Identifier(..), Expression(..), -- exported for testing
entrypoint
( entrypoint,
-- replLoop
) where
import System.IO
import Parser
import UntypedLambda
import UntypedLambdaExec
import GenericLambda
-- import Cleff
-- import Cleff.Input
-- import Cleff.Output
-- import Cleff.State
-- import Data.Maybe (fromMaybe)
--
import Control.Monad (foldM)
import System.Console.Haskeline
import System.Console.Repline
mainloop :: Int -> Expression -> IO ()
mainloop i expr = do
putStrLn $ show i ++ ": " ++ show expr
-- _ <- getLine
let new = reduce expr
if new == expr
then do
putStrLn "reached normal form. Quitting."
else mainloop (i+1) $ reduce expr
import Control.Monad.IO.Class (MonadIO(liftIO))
import Control.Monad.State
import Data.List
entrypoint = do
setupbuffering
putStrLn "Write your lambda expression:\n"
expr <- getLine
case runparse expr of
Right ex -> mainloop 0 ex
Left err -> putStrLn $ "Parsing failed! :" ++ err
setupbuffering
_ <- uLrepl
return ()
setupbuffering :: IO ()
setupbuffering = do
hSetBuffering stdin LineBuffering
hSetBuffering stdout LineBuffering
setupbuffering = do
hSetBuffering stdin NoBuffering
hSetBuffering stdout NoBuffering
type Repl' a b = HaskelineT (StateT a IO) b
cmd' :: (GenericLambda l) => String -> Repl' (Env l) ()
cmd' input = do
env <- get
(toprint, newenv) <- liftIO $ execLine env input
case toprint of
Nothing -> pure ()
Just e -> liftIO $ putStrLn e
modify (const newenv)
completer' :: (GenericLambda l, Monad m, MonadState (Env l) m) => CompletionFunc m
completer' = \case
("", r) -> do
matches <- gets (map convertmatch . envStrings)
return ("", matches)
(s, r) -> do
let s' = head $ map reverse $ dumbsep s ""
matches <- gets (filter (isPrefixOf (reverse s') . fst) . envStrings)
let completions = map convertmatch matches
return (s, map (trimComplete s') completions)
where format s e = s ++ ": " ++ e
convertmatch (s, e) = Completion s (format s e) True
dumbsep :: String -> String -> [String]
dumbsep (' ':rest) curr = curr:dumbsep rest ""
dumbsep (c:rest) curr = dumbsep rest (c:curr)
dumbsep "" curr = pure curr
opts = []
-- ini :: Repl ()
-- ini = liftIO $ putStrLn "Type your lambda expression."
ini' :: (GenericLambda l) => Repl' (Env l) ()
ini' = liftIO $ putStrLn "Type your lambda expression."
final :: (GenericLambda l) => Repl' (Env l) ExitDecision
final = do
liftIO $ putStrLn "Goodbye!"
return Exit
repl' :: (GenericLambda l) => IO ((), Env l)
repl' = (runStateT $ evalRepl (const $ pure ">>> ") cmd' opts (Just ':') (Just "paste") (Custom completer') ini' final) emptyEnv
uLrepl :: IO ((), Env UntypedLambda)
uLrepl = repl'

View File

@ -1,62 +0,0 @@
module Parser where
import UntypedLambda
import Data.Attoparsec.ByteString
import Data.Attoparsec.ByteString.Char8
import qualified Data.ByteString as BS
import qualified Data.String as BS
import Control.Applicative ((<|>))
expressionparser :: Parser Expression
expressionparser = choice [applyparser, parensparser, identparser, lambdaparser]
-- exp <- choice [parensparser,
-- identparser,
-- lambdaparser,
-- applyparser]
-- endOfInput
-- return exp
parensparser :: Parser Expression
parensparser = do
char '('
many' space
exp <- expressionparser
many' space
char ')'
-- <?>
return exp
identparser :: Parser Expression
identparser = Var . Identifier <$> many1 letter_ascii
-- identparser = do
-- name <- many1 letter_ascii
lambdaparser :: Parser Expression
lambdaparser = do
char '\\' <|> char 'λ'
ids <- sepBy1' (many1 letter_ascii) (many1' space)
many' space
char '.'
many' space
Lambda (fmap Identifier ids) <$> expressionparser
applyparser :: Parser Expression
applyparser = do
firstexp <- nonrecexpparse
many1' space
otherexp <- sepBy1' nonrecexpparse (many1' space)
return $ leftassoc firstexp otherexp
-- Application e1 <$> expressionparser
where nonrecexpparse = choice [parensparser, identparser, lambdaparser]
leftassoc :: Expression -> [Expression] -> Expression
leftassoc x xs = foldl1 Application (x:xs)
-- runparse :: String -> Result Expression
runparse = parseOnly expressionparser . BS.fromString

View File

@ -0,0 +1,87 @@
{-# LANGUAGE OverloadedStrings #-}
module UL0Parser where
import UntypedLambda
import Data.Attoparsec.Text
import Data.String (fromString)
import Data.Text (unpack)
expressionparser :: Parser Expression
expressionparser = choice [lambdaparser, applyparser, parensparser, identparser]
-- This function parses an expression enclosed in parentheses.
parensparser :: Parser Expression
parensparser = do
char '('
many' space
exp <- expressionparser
many' space
char ')'
return exp
-- this function parses a single identifier and wraps it into our datatypes.
identparser :: Parser Expression
identparser = Var . Identifier <$> many1 letter
--parses a lambda expression, like \x.x
lambdaparser :: Parser Expression
lambdaparser = do
choice [char '\\', char 'λ']
ids <- sepBy1' (many1 letter) (many1' space)
many' space
char '.'
many' space
Lambda (fmap Identifier ids) <$> expressionparser
-- parses an application.
-- It will first try to parse as many expressions separated by a space as possible.
-- To avoid an infinite loop, the sub-expression must not be applications themselves.
-- We use a helper function, nonrececpparse (non-recursive expression parser) to
-- overcome this.
--
-- When we have a list of expression, since application is left associative
-- we run foldl1 to build our final expression, made of nested applications.
--
-- i.e.: a b c must be parsed exactly as (a b) c
applyparser :: Parser Expression
applyparser = do
firstexp <- nonrecexpparse
many1' space
otherexp <- sepBy1' nonrecexpparse (many1' space)
return $ leftassoc firstexp otherexp
-- Application e1 <$> expressionparser
where nonrecexpparse = choice [parensparser, identparser, lambdaparser]
leftassoc :: Expression -> [Expression] -> Expression
leftassoc x xs = foldl1 Application (x:xs)
-- parses a full statement.
-- A statement is either an import, a definition, or an expression.
statementparser :: Parser Statement
statementparser = choice [importparser, defineparser, Exp <$> expressionparser]
-- parses a definition: an indetified followed by '=' and then an expression.
defineparser :: Parser Statement
defineparser = do
id <- Identifier <$> many1 letter
many' space
char '='
many' space
Def id <$> expressionparser
-- parses an import statement. it just matches the import keyword, and then
-- considers whatever's left on the line as the filename to attempt opening,
importparser :: Parser Statement
importparser = do
string "import"
many' space
Imp . unpack <$> takeText
-- this is roughly taken from Attoparsec's documentation and it's how we
-- actually run the parser. the fromString part is to convert a string to a bytestring.
runparse = parseOnly statementparser . fromString

View File

@ -0,0 +1,96 @@
module UntypedLambda
(Environment, Statement(..), Expression(..), Identifier(..), updateEnv, envStrings, emptyEnv, normalform)
where
import qualified Data.Map as M
import Data.Bifunctor
-- Let's start defining a few wrapper types, togheter with
-- the definition of our lambda expression and a map-based environment.
-- IDENTIFIERS
newtype Identifier = Identifier String
deriving (Eq, Ord)
instance Show Identifier where
show (Identifier s) = s
-- THE ENVIRONMENT
newtype Environment = Env (M.Map Identifier Expression)
-- function we'll use to insert and update values in the environment.
updateEnv :: Environment -> Identifier -> Expression -> Environment
updateEnv (Env en) id exp = Env (M.insert id exp en)
envStrings (Env a) = map (bimap show show) (M.assocs a)
-- the empty environment. We need this to start our program.
emptyEnv :: Environment
emptyEnv = Env M.empty
lookupEnv :: Environment -> Identifier -> Maybe Expression
lookupEnv (Env en) = flip M.lookup en
-- EXPRESSION
data Expression = Var Identifier
| Lambda [Identifier] Expression
| Application Expression Expression
deriving (Eq)
-- this is a big show instance, but it's mostly uninteresting code
-- to pretty print our lambda expressions.
instance Show Expression where
show (Var s) = show s
show (Lambda ids ex) = "λ" ++ unwords (map show ids) ++ "." ++ show ex
show (Application m n) = enclosem m ++ " " ++ enclosen n
where
enclosem k@(Lambda _ _) = enclose $ show k
enclosem x = show x
enclosen k@(Lambda _ _) = enclose $ show k
enclosen k@(Application _ _) = enclose $ show k
enclosen x = show x
enclose s = "(" ++ s ++ ")"
-- STATEMENTS
-- a program in our language will be defined as a list of single-line statements, such as
-- id = \x.x
-- id y
-- import "FileName"
--
-- the first is a definition, and will update the environment.
-- the second is an expression that will be reduced to normal form and printed.
data Statement = Def Identifier Expression | Exp Expression | Imp String
-- now, the actual functions:
apply :: Environment -> Expression -> Expression -> Expression
apply en (Lambda [] ex) arg = reduce en arg
apply en (Lambda [i] ex) arg = reduce (updateEnv en i arg) ex
apply en (Lambda (i:ids) ex) arg = Lambda ids (reduce (updateEnv en i arg) ex)
apply en m n = Application (reduce en m) (reduce en n)
reduce :: Environment -> Expression -> Expression
reduce en (Application m n) = apply en (reduce en m) n
reduce en (Lambda ids m) = Lambda ids (reduce en m)
reduce en (Var id) = case lookupEnv en id of
Nothing -> Var id -- the variable is free, leave as it is.
Just exp -> exp
tries :: Int
tries = 50
normalform :: Environment -> Expression -> Maybe Expression
normalform = loop tries
where loop :: Int -> Environment -> Expression -> Maybe Expression
loop 0 _ _ = Nothing
loop n en ex = if reduce en ex == ex then Just ex else loop (n-1) en (reduce en ex)

View File

@ -0,0 +1,61 @@
{-# LANGUAGE TypeFamilies #-}
module UntypedLambdaExec where
import qualified UntypedLambda as UL
import UL0Parser
import GenericLambda
-- UntypedLambdaCalculus
data UntypedLambda
instance GenericLambda UntypedLambda where
data Env UntypedLambda = GEnv UL.Environment
type Iden UntypedLambda = UL.Identifier
type Data UntypedLambda = UL.Expression
data PRes UntypedLambda = ParseResult
emptyEnv = GEnv UL.emptyEnv
updateEnv (GEnv e) i d = GEnv $ UL.updateEnv e i d
envStrings (GEnv e) = UL.envStrings e
normalform (GEnv e) d = case UL.normalform e d of
Nothing -> Left ""
Just exp -> Right $ show exp
execLine (GEnv e) s = do
(r, e') <- execLine' e s
return (r, GEnv e')
data ParseResult = Error String | Success | ParsedExp String
evalPrint :: UL.Environment -> UL.Expression -> String
evalPrint en ex = case UL.normalform en ex of
Nothing -> "Expression took more than 50 steps before reaching normal form, halting"
Just res -> "-> " ++ show res
execLine' :: UL.Environment -> String -> IO (Maybe String, UL.Environment)
execLine' en s =
case runparse s of
Right (UL.Def id exp) -> return (Nothing, UL.updateEnv en id exp)
Right (UL.Exp ex) -> return (Just (evalPrint en ex), en)
Right (UL.Imp filename) -> do
env <- parseFile en filename
return (Nothing, env)
Left err -> return (Just $ "Parsing failed:" ++ err, en)
-- this function does nothing but calling execLine on a list of statements.
execList :: UL.Environment -> [String] -> IO UL.Environment
execList en [] = return en
execList en (s:ss) = do
(_, en') <- execLine' en s
execList en' ss
parseFile :: UL.Environment -> String -> IO UL.Environment
parseFile env filename = do
content <- readFile filename
let stmts = filter (/= "") $ lines content
execList env stmts

View File

@ -1,59 +0,0 @@
module UntypedLambda where
import qualified Data.Map as M
-- Let's start defining a few wrapper types, togheter with
-- the definition of our lambda expression and a map-based environment.
newtype Identifier = Identifier String
deriving Eq
instance Show Identifier where
show (Identifier s) = s
data Expression = Var Identifier
| Lambda [Identifier] Expression
| Application Expression Expression
deriving (Eq)
instance Show Expression where
show (Var s) = show s
show (Lambda ids ex) = "λ" ++ show ids ++ "." ++ show ex
show (Application m n) = enclosem m ++ " " ++ enclosen n
where
enclosem k@(Lambda _ _) = enclose $ show k
enclosem x = show x
enclosen k@(Lambda _ _) = enclose $ show k
enclosen k@(Application _ _) = enclose $ show k
enclosen x = show x
enclose s = "(" ++ s ++ ")"
-- name a more iconic duo: eval and apply!
--
-- data Lcomp :: Effect where
-- Reduce :: Expression -> Lcomp m Expression -- also known as EVAL
-- Apply :: Expression -> Expression -> Lcomp m Expression
-- makeEffect ''Lcomp
--
-- let's make our first, naive interpreter.
replace :: Identifier -> Expression -> Expression -> Expression
replace var ex k@(Var p) = if p == var then ex else k
replace var ex k@(Lambda ids body) = if var `elem` ids then k else Lambda ids (replace var ex body)
replace var ex k@(Application m n) = Application (replace var ex m) (replace var ex n)
simpleapply :: Expression -> Expression -> Expression
simpleapply (Lambda [] ex) p = Application ex p -- lambdas with no arguments are constants.
simpleapply (Lambda [i] ex) p = replace i p ex
simpleapply (Lambda (i:ids) ex) p = Lambda ids (replace i p ex)
simpleapply m n = Application m n
reduce :: Expression -> Expression
reduce (Application m n) = simpleapply (reduce m) (reduce n)
reduce (Lambda ids m) = Lambda ids (reduce m)
reduce (Var id) = Var id

View File

@ -17,9 +17,8 @@
#
# resolver: ./custom-snapshot.yaml
# resolver: https://example.com/snapshots/2018-01-01.yaml
resolver:
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/25.yaml
resolver: lts-19.00
# User packages to be built.
# Various formats can be used as shown in the example below.
#
@ -40,9 +39,6 @@ packages:
# - git: https://github.com/commercialhaskell/stack.git
# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
#
extra-deps:
- cleff-0.2.1.0
- rec-smallarray-0.1.0.0
# Override default flag values for local packages and extra-deps
# flags: {}