diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) Thomas DuBuisson + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + +3. Neither the name of the author nor the names of his contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS +OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR +ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/LambdaCalculator.cabal b/LambdaCalculator.cabal new file mode 100644 --- /dev/null +++ b/LambdaCalculator.cabal @@ -0,0 +1,30 @@ +name: LambdaCalculator +version: 0.0.1 +license: BSD3 +license-file: LICENSE +copyright: Tim Sheard +author: Tim Sheard +maintainer: Thomas DuBuisson +description: A basic lambda calculator with beta reduction and a REPL +synopsis: A basic lambda calculator with beta reduction and a REPL +category: Language +stability: stable +build-type: Simple +cabal-version: >= 1.2 +tested-with: GHC == 6.10.3 + +flag small_base + Description: Choose the split-up base package. + +Executable LambdaCalculator + Main-is: LambdaCalculator.hs + if flag(small_base) + Build-Depends: base >= 3 && < 5, bytestring >= 0.9 && < 1.0 , binary >= 0.4.0 && < 0.6.0, + mtl >= 1.1.0.0 && < 1.2.0.0, haskeline >= 0.6 && < 0.7, + pretty >= 1.0 && < 1.1, + parsec >= 2.1 && < 2.2 + else + Build-Depends: base >= 3 && < 5, bytestring >= 0.9 && < 1.0, binary >= 0.4.0 && < 0.6.0, + mtl >= 1.1.0.0 && < 1.2.0.0, haskeline >= 0.6 && < 0.7, + pretty >= 1.0 && < 1.1, + parsec >= 2.1 && < 2.2 diff --git a/LambdaCalculator.hs b/LambdaCalculator.hs new file mode 100644 --- /dev/null +++ b/LambdaCalculator.hs @@ -0,0 +1,347 @@ +-- Copyright (c) Tim Sheard +-- Portland State University +-- Subject to conditions of distribution and use; see LICENSE for details. +-- Friday May 11, 2007 +-- Lambda Calculator: version 1.0 + + +module Main where + +import Text.ParserCombinators.Parsec -- This for defining parsers +import qualified Text.PrettyPrint.HughesPJ as PP +import Text.PrettyPrint.HughesPJ(Doc,text,int,(<>),(<+>),($$),($+$) + ,render,Style(..), renderStyle,Mode(..)) +import Data.List(union,(\\)) +import Data.Char(digitToInt) + +import System.Console.Haskeline +import Control.Monad.Trans + +------------------------------------------------ + +data Exp + = Lam String Exp + | Var String + | App Exp Exp + | Syn String Exp + + +----------------------------------------------- +-- Parsing + +------------ Lexical tokens + +lexeme p = do{ x <- p; whiteSpace; return x } +symbol name = lexeme (string name) +whiteSpace = many(space <|> tab <|> newline) +identifier = try (lexeme(do { c <- lower; cs <- many(lower <|> digit <|> upper); return (c:cs)})) +natural = lexeme(number 10 digit) +parens p = between (symbol "(") (symbol ")") p + +number :: Integer -> Parser Char -> Parser Integer +number base baseDigit + = do{ digits <- many1 baseDigit + ; let n = foldl (\x d -> base*x + toInteger (digitToInt d)) 0 digits + ; seq n (return n) + } + +------------- Parsers for lambda terms + +pExp:: Parser Exp +pExp = appExp <|> lamExp + where appExp = do { es <- many1 simple; return(foldl1 App es) } + lamExp = do { symbol "\\" + ; v <- identifier + ; symbol "." + ; e <- pExp + ; return(Lam v e)} + +simple:: Parser Exp +simple = var <|> try(parens pExp) <|> churchNum + where var = do { v <- identifier; return(Var v)} + churchNum = do { char '#' + ; n <- natural + ; let f n x = Syn ("#"++show n) x + ; return(f n (Lam "s" (Lam "z" (church n (Var "s") (Var "z")))))} + church 0 s z = z + church n s z = App s (church (n-1) s z) + +parse1 x s = parse (whiteSpace >> x) "keyboard input" s + +parse2 x s = + case parse1 x s of + Right(ans) -> ans + Left message -> error (show message) + +pe = parse2 pExp + +------------------------------------------------ +-- creating documents + +dExp :: Exp -> Doc +dExp (Syn s e) = text s +dExp (Var s) = text s +dExp (Lam x e) = PP.hsep [(PP.hsep [text "\\",text x,text "."]),(dExp e)] +dExp apply = PP.fsep (map parenApp (args apply)) + +args (App x y) = args x ++ [y] +args x = [x] + +parenApp (x@(App _ _)) = PP.parens (dExp x) +parenApp (x@(Lam _ _)) = PP.parens (dExp x) +parenApp x = dExp x + +style = (Style PageMode 70 1.5) +showe exp = putStrLn (renderStyle style (dExp exp)) + +instance Show Exp where + show x = renderStyle style (dExp x) + +pp (Var s) = s +pp (Syn n e) = "(Syn "++n++" "++pp e++")" +pp (App x y) = "(App "++pp x++" "++pp y++")" +pp (Lam x e) = "(Lam "++x++" "++pp e++")" + +--------------------------------------------- +-- free variables + +varsOf (Syn n e) = varsOf e +varsOf (Var x) = [x] +varsOf (App x y) = varsOf x `union` varsOf y +varsOf (Lam x e) = [x] `union` varsOf e + +freeOf (Syn n e) = freeOf e +freeOf (Var x) = [x] +freeOf (App x y) = freeOf x `union` freeOf y +freeOf (Lam x e) = freeOf e \\ [x] + +--------------------------------------------- +-- substitution + +sub env (Syn n e) = Syn n (sub env e) +sub env (Var x) = + case lookup x env of + Just e -> e + Nothing -> Var x +sub env (App x y) = App (sub env x) (sub env y) +sub env (Lam x e) = Lam new (sub env2 e) + where env2@((_,Var new):_) = bind env x + + +bind env x = if elem x free + then (x,Var(new 0 x)):env + else (x,Var x):env + where free = foldr union [] (map f env) + f (name,term) = freeOf term + new n x = if elem next free + then new (n+1) x + else next + where next = x++show n + +------------------------------------------------ +-- beta reduction + +beta (Syn n e) = Just e +beta (App (Syn _ e) x) = Just(App e x) +beta (App (Lam x e) v) = Just(sub [(x,v)] e) +beta (App x y) = + case (beta x) of + Just a -> Just(App a y) + Nothing -> case (beta y) of + Nothing -> Nothing + Just b -> Just(App x b) +beta (Var x) = Nothing +beta (Lam x e) = + case (beta e) of + Nothing -> Nothing + Just a -> Just(Lam x a) + + +deepBeta (Syn n e) = Just e +deepBeta (App (Syn _ e) x) = deepBeta (App e x) +deepBeta (App (Lam x e) v) = Just(sub [(x,v)] e) +deepBeta (App x y) = + case (deepBeta x) of + Just a -> deep a y + Nothing -> case (deepBeta y) of + Nothing -> Nothing + Just b -> Just(App x b) +deepBeta (Var x) = Nothing +deepBeta (Lam x e) = + case (deepBeta e) of + Nothing -> Nothing + Just a -> Just(Lam x a) + +deep (Lam x e) y = Just(sub [(x,y)] e) +deep (Syn _ x) y = deep x y +deep x y = Just(App x y) + +betaAll 0 x = x +betaAll n x = case deepBeta x of + Nothing -> x + Just e -> betaAll (n-1) e + +-------------------------------------------------- +-- commands + +data Command + = Execute Exp + | Set String Exp + | Fail String + | BetaStep + | Com Char deriving Show + +pCom :: Parser Command +pCom = try (do { s <- identifier; symbol "="; e <- pExp; return(Set s e)}) <|> + try (do {e <- pExp; return(Execute e)}) <|> + try (do { char ':'; c <- satisfy (const True); return(Com c)}) <|> + try ( eof >> return BetaStep ) + +command :: String -> Command +command str = + case parse1 pCom str of + Right(x) -> x + Left s -> Fail (show s) + +------------------------------------------------------ + +examples = + [("zero", "#0") + ,("one", "#1") + ,("two", "#2") + ,("add", "\\ x . \\ y . \\ s . \\ z . x s (y s z)") + ,("mult","\\ x . \\ y . \\ s . \\ z . x (\\ n . y s n) z") + ,("y", "\\ f . (\\ x .f (x x)) (\\ x . f (x x))") + ,("pair", "\\x.\\y.\\k.k x y") + ,("fst", "\\p.p(\\x.\\y.x)") + ,("snd", "\\p.p(\\x.\\y.y)") + ,("if", "\\b.\\then.\\else.b then else") + ,("true", "\\t.\\f.t") + ,("false", "\\t.\\f.f") + ,("succ", "\\n. \\s . \\z. n s (s z)") + ,("pred", "\\n . snd(n (\\ x . pair (succ (fst x)) (fst x)) (pair zero zero))") + ,("fact", "\\n . snd(n (\\ x . pair (succ (fst x)) (mult (succ (fst x))(snd x)) (pair zero one) ))" ) + ,("const", "\\c . \\a . c") + ,("ifZero","\\ x . x (const false) true") + ,("isZero", "ifZero") + ,("and", "\\ x . \\y . x y false") + ,("or", "\\ x . \\y . x true y") + ,("not", "\\ x . x false true") + ,("monus", "\\ x . \\y . y pred x") + ,("even", "\\ n . n not true") + ,("odd", "\\ n . not (even n)") + ,("eq", "\\x . \\y . and (isZero (monus x y)) (isZero (monus y x))") + ,("factHelp","\\ fact . \\ n . ifZero n one (mult n (fact (pred n)))") + ,("fact2","y factHelp") + ] + +doSub [] ans = ans +doSub ((nm,v):xs) ans = doSub xs ((nm,sub ans v):ans) + +env0 = doSub temp [] + where temp = map gen examples + gen (nm,v) = (nm,Syn nm (pe v)) + +---------------------------------------------------------- +-- commands + +check env term action = + do { let free = freeOf term + ; case free \\ map fst env of + [] -> action + left -> putStrLn ("Unknown free variables: "++ show left) >> + return(Just(Var "?",env))} + +action (term,env) (Set s e) = + check env e (do { let ans = sub env e + f (nm,v) = (nm,Syn nm v) + ; showe ans + ; return(Just(Var s,(f (s,ans)):env))}) +action (term,env) (Execute e) = check env e $ + do { let ans = sub env e + ; showe ans + ; return(Just(ans,env))} +action (term,env) BetaStep = + do { let ans = beta term + ; case ans of + Just new -> showe new >> return(Just(new,env)) + Nothing -> putStrLn "" >> return(Just(term,env))} +action (term,env) (Com 'q') = return Nothing +action (term,env) (Com 'b') = + do { let new = betaAll 1000 term + ; showe new >> return(Just(new,env))} +action (term,env) (Com 'c') = + do { showe term; return(Just(term,env))} +action env (Fail s) = do { putStrLn ("Error:\n "++s); return(Just env)} +action (term,env) (Com 'p') = + do { putStrLn (pp term); return(Just(term,env))} +action (term,env) (Com 'e') = putStrLn message >> return(Just (term,env)) + where message = renderStyle style (PP.fsep (map f (reverse env))) + f (nm,v) = text nm +action (term,env) (Com s) = putStrLn ("Unknown command:\n "++[s]) >> return(Just(term,env)) + + +commandP nm (Com s) = nm==s +commandP nm _ = False + +betaP BetaStep = True +betaP _ = False + +execP (Execute _) = True +execP _ = False + +setP (Set _ _) = True +setP _ = False + +commands = + [(setP,action, "n = term Install 'term' under the name `n`. It becomes the current term.\n") + ,(execP,action, "term Install 'term' as the current term.\n") + ,(betaP,action, " Take a single beta-step on the current term.\n") + ,(commandP 'c',action, ":c Print the current term.\n") + ,(commandP 'e',action, ":e List the names installed in the current environment.\n") + ,(commandP 'b',action, ":b Take a large number of beta-steps without pausing.\n") + ,(commandP 'q',action, ":q Exit the lambda calculator.\n") + ,(commandP 'p',action, ":p Print the current term in internal form (for system debugging).\n") + ,(commandP '?',comment,":? Show this set of command descriptions.") + ] + +comments = concat (map (\(pred,action,descr)-> descr) commands) +comment env com = putStrLn comments >> return(Just env) + +prolog = "\n\nThis is the Lambda Calculator. Enter lambda terms to set the\n"++ + "the current term. Step the current term by entering .\n"++ + "The syntax of terms is described by the following grammar:\n\n"++ + " T ::= \n"++ + " | T T\n"++ + " | \\ . T\n"++ + " | #\n\n"++ + "Type :? to see a listing of other legal commands." + +---------------------------------------------------- +-- main + +prompt = "\nprompt> " + +main :: IO () +main = do + putStrLn prolog + let env = (Var "?", env0) + runInputT defaultSettings (loop commands env) + +loop table environment = go environment + where + go env = do + minput <- getInputLine prompt + case minput of + Nothing -> return () + Just str -> do + e <- handleInput str env + case e of + Just e' -> go e' + Nothing -> return () + handleInput input env = do + let cmd = command input + find [] = outputStrLn ("Unknown command: " ++ input ++ "\n" ++ show cmd) >> return (Just env) + find ((pred,action,descr):ps) | pred cmd = lift (action env cmd) + find (p:ps) = find ps + find table diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain