mikrokosmos 0.2.0 → 0.3.0
raw patch · 18 files changed
+1101/−822 lines, 18 filesdep +directorydep +optionsdep +tastysetup-changed
Dependencies added: directory, options, tasty, tasty-hunit
Files
- Format.hs +0/−103
- Interpreter.hs +0/−197
- Lambda.hs +0/−130
- Main.hs +0/−124
- MultiBimap.hs +0/−52
- NamedLambda.hs +0/−133
- README.md +6/−77
- Setup.hs +0/−2
- mikrokosmos.cabal +10/−3
- source/Environment.hs +111/−0
- source/Format.hs +142/−0
- source/Interpreter.hs +179/−0
- source/Lambda.hs +138/−0
- source/Main.hs +231/−0
- source/MultiBimap.hs +52/−0
- source/NamedLambda.hs +133/−0
- source/Ski.hs +98/−0
- std.mkr +1/−1
− Format.hs
@@ -1,103 +0,0 @@-{-|-Module: Format-Description: Formatting the output of the interpreter-License: GPL-3--This module controls the format of the text and expressions printed by the-interpreter. Uses ANSI escape sequences to color the terminal and mark text-as bold or italics. It also stores the texts showed by the interpreter.--}--module Format- ( formatFormula- , formatIntro- , formatPrompt- , formatName- , formatSubs1- , formatSubs2- , end- , promptText- , helpText- , initialText- )-where--import System.Console.ANSI------ Colors--- | Prompt messages color-promptColor :: Color-promptColor = Blue---- | Named variables color-nameColor :: Color-nameColor = Green---- | Substitutions are marked with this color-substColor :: Color-substColor = Red---- | To-be-substituted expressions are marked with this color-subst2Color :: Color-subst2Color = Yellow----- Format sequences--- | Sequence of characters that signals the format of a formula to the terminal.-formatFormula :: String-formatFormula = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull promptColor]---- | Sequence of characters that signals the format of the introduction to the terminal.-formatIntro :: String-formatIntro = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull promptColor]---- | Sequence of characters that signals the format of the prompt to the terminal.-formatPrompt :: String-formatPrompt = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid promptColor]---- | Sequence of characters that signals the format of a name to the terminal.-formatName :: String-formatName = setSGRCode [SetColor Foreground Dull nameColor]---- | Sequence of characters that signals the format of a substitution to the terminal.-formatSubs1 :: String-formatSubs1 = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull substColor]---- | Sequence of characters that signals the format of a expression which will--- be substituted in the next reduction step to the terminal.-formatSubs2 :: String-formatSubs2 = setSGRCode [SetColor Foreground Dull subst2Color]---- | Sequence of characters that cleans all the format.-end :: String-end = setSGRCode []------- | Prompt line. It is shown when the interpreter asks the user--- to introduce a new command.-promptText :: String-promptText = formatPrompt ++ "mikroλ> " ++ end---- | Help line. It is shown when the user uses the :help command.-helpText :: String-helpText = unlines [- formatFormula ++- "Commands available from the prompt:",- "\t<expression>\t evaluates the expression",- "\t:quit \t quits the interpreter",- "\t:load <file>\t loads the given .mkr library or script",- "\t:verbose \t sets verbose mode on/off",- "\t:help \t shows this help"- ++ end- ]---- | Initial text on the interpreter. It is shown at startup.-initialText :: String-initialText = unlines [- formatIntro ++ "Welcome to the Mikrokosmos Lambda Interpreter!" ++ end,- formatFormula ++ "Version 0.1.0. GNU General Public License Version 3." ++ end- ]
− Interpreter.hs
@@ -1,197 +0,0 @@-{-|-Module: Interpreter-Description: Internal logic of the interpreter-License: GPL-3--This module contains auxiliary logic, types and representations of-the internal state of the interpreter.--}-module Interpreter- ( Context- , emptyContext- , InterpreterOptions (InterpreterOptions)- , defaultOptions- , changeVerbose- , changeColor- , getVerbose- , getColor- , InterpreterAction (..)- , interpreteractionParser- , act- , multipleAct- , Action (..)- , actionParser- )-where--import Control.Applicative ((<$>), (<*>))-import Control.Monad.State.Lazy -import Text.ParserCombinators.Parsec hiding (State)-import Data.Char-import Data.List-import MultiBimap-import NamedLambda-import Format-import Lambda---- | A context is an application between expressions and the names--- they may have.-type Context = MultiBimap Exp String---- | Empty context without any bindings-emptyContext :: Context-emptyContext = MultiBimap.empty----- Interpreter options--- | Configuration options for the interpreter. They can be changed dinamically.-data InterpreterOptions = InterpreterOptions- { verbose :: Bool -- ^ true to produce verbose output- , color :: Bool -- ^ true to color the output- }---- | Default configuration options for the interpreter.-defaultOptions :: InterpreterOptions-defaultOptions = InterpreterOptions- { verbose = False- , color = True- }---- | Gets the verbose configuration-getVerbose :: InterpreterOptions -> Bool-getVerbose = verbose---- | Gets the color configuration-getColor :: InterpreterOptions -> Bool-getColor = color---- | Sets the verbose configuration on/off.-changeVerbose :: InterpreterOptions -> InterpreterOptions-changeVerbose options = options {verbose = not $ verbose options}---- | Sets the color configuration on/off-changeColor :: InterpreterOptions -> InterpreterOptions-changeColor options = options {color = not $ color options}-------- | Interpreter action. It can be a language action (binding and evaluation)--- or an interpreter specific one, such as "quit". -data InterpreterAction = Interpret Action -- ^ Language action- | EmptyLine -- ^ Empty line, it will be ignored- | Error -- ^ Error on the interpreter- | Quit -- ^ Close the interpreter- | Load String -- ^ Load the given file- | SetVerbose -- ^ Changes verbosity- | SetColors -- ^ Changes colors- | Help -- ^ Shows help---- | Language action. The language has a number of possible valid statements;--- all on the following possible forms.-data Action = Bind (String, NamedLambda) -- ^ bind a name to an expression- | EvalBind (String, NamedLambda) -- ^ bind a name to an expression and simplify it- | Execute NamedLambda -- ^ execute an expression- | Comment -- ^ comment----- | Executes a language action. Given a context and an action, returns--- the new context after the action and a text output.-act :: Action -> State Context [String]-act Comment = return [""]-act (Bind (s,le)) =- do modify (\ctx -> MultiBimap.insert (toBruijn ctx le) s ctx)- return [""]-act (EvalBind (s,le)) =- do modify (\ctx -> MultiBimap.insert (simplifyAll $ toBruijn ctx le) s ctx)- return [""]-act (Execute le) =- do context <- get- return [unlines $- [ show le ] ++- [ unlines $ map showReduction $ simplifySteps $ toBruijn context le ] ++- [ showCompleteExp context $ simplifyAll $ toBruijn context le ]- ]----- TODO: Use Text instead of String for efficiency--- | Executes multiple actions. Given a context and a set of actions, returns--- the new context after the sequence of actions and a text output.-multipleAct :: [Action] -> State Context [String]-multipleAct actions = concat <$> mapM act actions------ | Shows an expression and the name that is bound to the expression--- in the current context-showCompleteExp :: Context -> Exp -> String-showCompleteExp context expr = case getExpressionName context expr of- Nothing -> show (nameExp expr)- Just expName -> show (nameExp expr) ++ formatName ++ " ⇒ " ++ expName ++ end----- | Given an expression, returns its name if it is bounded to any.-getExpressionName :: Context -> Exp -> Maybe String-getExpressionName context expr = case MultiBimap.lookup expr context of- [] -> Nothing- xs -> Just $ intercalate ", " xs------- Parsing of interpreter command line commands.--- | Parses an interpreter action.-interpreteractionParser :: Parser InterpreterAction-interpreteractionParser = choice- [ try interpretParser- , try quitParser- , try loadParser- , try verboseParser- , try helpParser- ]---- | Parses a language action as an interpreter action.-interpretParser :: Parser InterpreterAction-interpretParser = Interpret <$> actionParser---- | Parses a language action.-actionParser :: Parser Action-actionParser = choice- [ try bindParser- , try evalbindParser- , try executeParser- , try commentParser- ]---- | Parses a binding between a variable an its representation.-bindParser :: Parser Action-bindParser = fmap Bind $ (,) <$> many1 alphaNum <*> (spaces >> string "!=" >> spaces >> lambdaexp)---- | Parses a binding and evaluation expression between a variable an its representation-evalbindParser :: Parser Action-evalbindParser = fmap EvalBind $ (,) <$> many1 alphaNum <*> (spaces >> string "=" >> spaces >> lambdaexp)---- | Parses an expression in order to execute it.-executeParser :: Parser Action-executeParser = Execute <$> lambdaexp---- | Parses comments.-commentParser :: Parser Action-commentParser = string "#" >> many anyChar >> return Comment---- | Parses a "quit" command.-quitParser :: Parser InterpreterAction-quitParser = string ":quit" >> return Quit---- | Parses a "help" command.-helpParser :: Parser InterpreterAction-helpParser = string ":help" >> return Help---- | Parses a change in verbosity.-verboseParser :: Parser InterpreterAction-verboseParser = string ":verbose" >> return SetVerbose---- | Parses a "load-file" command.-loadParser :: Parser InterpreterAction-loadParser = Load <$> (string ":load" >> between spaces spaces (many1 (satisfy (not . isSpace))))
− Lambda.hs
@@ -1,130 +0,0 @@-{-|-Module: Lambda-Description: DeBruijn lambda expressions.-License: GPL-3--This module deals with the parsing, reduction and printing of lambda-expressions using DeBruijn notation. The interpreter uses DeBruijn-notation as an internal representation and as output format. This is because-it is easier to do beta reduction with DeBruijn indexes.--}--module Lambda- ( Exp (Var, Lambda, App)- , simplifyAll- , simplifySteps- , showReduction- )-where--import Format---- DeBruijn Expressions--- | A lambda expression using DeBruijn indexes.-data Exp = Var Integer -- ^ integer indexing the variable.- | Lambda Exp -- ^ lambda abstraction- | App Exp Exp -- ^ function application- deriving (Eq, Ord)--instance Show Exp where- show = showexp----- | Shows an expression with DeBruijn indexes.-showexp :: Exp -> String-showexp (Var n) = show n-showexp (Lambda e) = "λ" ++ showexp e ++ ""-showexp (App f g) = "(" ++ showexp f ++ " " ++ showexp g ++ ")"---- | Shows an expression coloring the next reduction.-showReduction :: Exp -> String-showReduction (Lambda e) = "λ" ++ showReduction e-showReduction (App (Lambda f) x) = betaColor (App (Lambda f) x)-showReduction (Var e) = show e-showReduction (App rs x) = "(" ++ showReduction rs ++ " "- ++ showReduction x ++ ")"---- | Colors a beta reduction-betaColor :: Exp -> String-betaColor (App (Lambda e) x) =- "(" ++- formatSubs1 ++ "λ" ++ formatFormula ++- indexColor 1 e ++- " " ++- formatSubs2 ++ showexp x ++ formatFormula- ++ ")"-betaColor e = show e---- | Colors all the appearances of a given color-indexColor :: Integer -> Exp -> String-indexColor n (Lambda e) = "λ" ++ indexColor (succ n) e-indexColor n (App f g) = "(" ++ indexColor n f ++ " " ++ indexColor n g ++ ")"-indexColor n (Var m)- | n == m = formatSubs1 ++ show m ++ formatFormula- | otherwise = show m------- Reductions of lambda expressions.---- | Applies repeated simplification to the expression until it stabilizes and--- returns the final simplified expression.------ >>> simplifyAll $ App (Lambda (Var 1)) (Lambda (Var 1))--- λ1----simplifyAll :: Exp -> Exp-simplifyAll = last . simplifySteps---- | Applies repeated simplification to the expression until it stabilizes and--- returns all the intermediate results.------ >>> simplifySteps $ App (Lambda (Var 1)) (Lambda (Var 1))--- [(λ1 λ1),λ1]----simplifySteps :: Exp -> [Exp]-simplifySteps e- | e == s = [e]- | otherwise = e : simplifySteps s- where s = simplify e---- | Simplifies the expression recursively.--- Applies only a beta reduction at each step.-simplify :: Exp -> Exp-simplify (Lambda e) = Lambda (simplify e)-simplify (App (Lambda f) x) = betared (App (Lambda f) x)-simplify (App (Var e) x) = App (Var e) (simplify x)-simplify (App (App f g) x) = App (simplify (App f g)) x-simplify (Var e) = Var e---- | Applies beta-reduction to a function application.--- Leaves the rest of the operations untouched.-betared :: Exp -> Exp-betared (App (Lambda e) x) = substitute 1 x e-betared e = e---- | Substitutes an index for a lambda expression-substitute :: Integer -- ^ deBruijn index of the desired target- -> Exp -- ^ replacement for the index- -> Exp -- ^ initial expression- -> Exp-substitute n x (Lambda e) = Lambda (substitute (succ n) (incrementFreeVars 0 x) e)-substitute n x (App f g) = App (substitute n x f) (substitute n x g)-substitute n x (Var m)- -- The lambda is replaced directly- | n == m = x- -- A more exterior lambda decreases a number- | n < m = Var (m-1)- -- An unrelated variable remains untouched- | otherwise = Var m---- | Increments free variables assuming they are bind to an--- external lambda. This is done to substitute them correctly in--- internal expressions.-incrementFreeVars :: Integer -> Exp -> Exp-incrementFreeVars n (App f g) = App (incrementFreeVars n f) (incrementFreeVars n g)-incrementFreeVars n (Lambda e) = Lambda (incrementFreeVars (succ n) e)-incrementFreeVars n (Var m)- | m > n = Var (succ m)- | otherwise = Var m
− Main.hs
@@ -1,124 +0,0 @@-module Main where--import Control.Monad.Trans-import Control.Monad.State-import Control.Exception-import System.Environment-import System.Console.Haskeline-import Text.ParserCombinators.Parsec hiding (try)-import Format-import Interpreter---- | A filename is a string containing the directory path and--- the real name of the file.-type Filename = String----- Lambda interpreter--- The actions of the interpreter are written here. It allows to execute normal--- actions (bindings and evaluation), and interpreter specific actions, as--- "quit" or "load".---- | Runs the interpreter with default settings and an empty context.-main :: IO ()-main = do- args <- getArgs- case args of- [] -> runInputT defaultSettings ( outputStrLn initialText- >> interpreterLoop defaultOptions emptyContext- )- [filename] -> executeFile filename- _ -> putStrLn "Wrong number of arguments"----- | Interpreter awaiting for an instruction.-interpreterLoop :: InterpreterOptions -> Context -> InputT IO ()-interpreterLoop options context = do- minput <- getInputLine promptText- let interpreteraction =- case minput of- Nothing -> Quit- Just "" -> EmptyLine- Just input -> case parse interpreteractionParser "" input of- Left _ -> Error- Right a -> a- case interpreteraction of- EmptyLine -> interpreterLoop options context- Quit -> return ()- Error -> do- outputStr formatFormula- outputStrLn "Unknown command"- outputStr end- interpreterLoop options context- SetVerbose -> do- outputStrLn $- formatFormula ++- "verbose mode: " ++ if getVerbose options then "off" else "on" ++- end- interpreterLoop (changeVerbose options) context- SetColors -> interpreterLoop (changeColor options) context- Help -> outputStr helpText >> interpreterLoop options context- Load filename -> do- maybeloadfile <- lift $ loadFile filename- case maybeloadfile of- Nothing -> do- outputStrLn "Error loading file"- interpreterLoop options context- Just actions -> case runState (multipleAct actions) context of- (output, ccontext) -> do- outputActions options output- interpreterLoop options ccontext- Interpret action -> case runState (act action) context of- (output, ccontext) -> do- outputActions options output- interpreterLoop options ccontext------- | Outputs results from actions. Given a list of options and outputs,--- formats and prints them in console.-outputActions :: InterpreterOptions -> [String] -> InputT IO ()-outputActions options output = do- outputStr formatFormula- mapM_ (outputStr . format) output- outputStr end- where- format :: String -> String- format "" = ""- format s- | not (getVerbose options) = (++"\n") . last . lines $ s- | otherwise = s------- Loading and reading files--- | Loads the given filename and returns the complete list of actions.--- Returns Nothing if there is an error reading or parsing the file.-loadFile :: String -> IO (Maybe [Action])-loadFile filename = do- putStrLn filename- input <- try $ (readFile filename) :: IO (Either IOException String)- case input of- Left _ -> return Nothing- Right inputs -> do- let parsing = map (parse actionParser "") $ filter (/="") $ lines inputs- let actions = map (\x -> case x of- Left _ -> Nothing- Right a -> Just a) parsing- return $ sequence actions---- | Executes the commands inside a file. A .mkr file can contain a sequence of--- expressions and variable bindings, and it is interpreted sequentially.-executeFile :: Filename -> IO ()-executeFile filename = do- maybeloadfile <- loadFile filename- case maybeloadfile of- Nothing -> putStrLn "Error loading file"- Just actions -> case runState (multipleAct actions) emptyContext of- (outputs, _) -> mapM_ (putStr . format) outputs- where- format :: String -> String- format "" = ""- format s = (++"\n") . last . lines $ s
− MultiBimap.hs
@@ -1,52 +0,0 @@-{-|-Module: MultiBimap-Description: A multibimap implementation-License: GPL-3--This module allows us to abstract a bidirectional multimap without-having to worry about implementation details. It is useful in the translation-between lambda expressions and names.- -Based on the bimap package:-<https://hackage.haskell.org/package/bimap-0.3.2/docs/Data-Bimap.html>--}-module MultiBimap- ( MultiBimap- , empty- , null- , insert- , lookup- , lookupR- )-where----import qualified Data.Map as M-import qualified Data.MultiMap as MM-import Prelude hiding (null,lookup)--data MultiBimap k v = MkMultiBimap (MM.MultiMap k v) (M.Map v k)---- | The empty multi-bimap-empty :: MultiBimap k v-empty = MkMultiBimap MM.empty M.empty---- | True if the multi-bimap is empty-null :: MultiBimap k v -> Bool-null (MkMultiBimap _ right) = M.null right---- | Inserts a key-value in the multi-bimap.--- The value can have been used earlier.-insert :: (Ord k, Ord v) => k -> v -> MultiBimap k v -> MultiBimap k v-insert k v (MkMultiBimap left right) =- MkMultiBimap (MM.insert k v left) (M.insert v k right)---- | Lookup a key in the multi-bimap, returning the list of--- associated values.-lookup :: (Ord k) => k -> MultiBimap k v -> [v]-lookup k (MkMultiBimap left _) = MM.lookup k left---- | Lookup a right value in the multi-bimap, returning the associated key.-lookupR :: (Ord v) => v -> MultiBimap k v -> Maybe k-lookupR v (MkMultiBimap _ right) = M.lookup v right
− NamedLambda.hs
@@ -1,133 +0,0 @@-{-|-Module: NamedLambda-Description: Lambda expressions with named variables-License: GPL-3--This package deals with lambda expressions containing named variables-instead of DeBruijn indexes. It contains parsing and printing fuctions.--}--module NamedLambda- ( NamedLambda (LambdaVariable, LambdaAbstraction, LambdaApplication)- , lambdaexp- , toBruijn- , nameExp- )-where--import Text.ParserCombinators.Parsec-import Control.Applicative ((<$>), (<*>))-import qualified Data.Map.Strict as Map-import Lambda-import MultiBimap-import Data.Maybe-import Control.Monad--type Context = MultiBimap Exp String---- Parsing of Lambda Expressions.--- The user can input a lambda expression with named variables, of--- the form of "\x.x" or "(\a.(\b.a b))". The interpreter will parse--- it into an internal representation.---- | A lambda expression with named variables.-data NamedLambda = LambdaVariable String -- ^ variable- | LambdaAbstraction String NamedLambda -- ^ lambda abstraction- | LambdaApplication NamedLambda NamedLambda -- ^ function application---- | Parses a lambda expression with named variables.--- A lambda expression is a sequence of one or more autonomous--- lambda expressions. They are parsed assuming left-associativity.------ >>> parse lambdaexp "" "\\f.\\x.f x"--- Right λf.λx.(f x)------ Note that double backslashes are neccessary only when we quote strings;--- it will work only with a simple backslash in the interpreter.-lambdaexp :: Parser NamedLambda-lambdaexp = foldl1 LambdaApplication <$> (spaces >> sepBy1 simpleexp spaces)---- | Parses a simple lambda expression, without function applications--- at the top level. It can be a lambda abstraction, a variable or another--- potentially complex lambda expression enclosed in parentheses.-simpleexp :: Parser NamedLambda-simpleexp = choice [lambdaAbstractionParser, variableParser, parens lambdaexp]---- | The returned parser parenthesizes the given parser-parens :: Parser a -> Parser a-parens = between (char '(') (char ')')---- | Parses a variable. Any name can form a lambda variable.-variableParser :: Parser NamedLambda-variableParser = LambdaVariable <$> nameParser---- | Allowed variable names-nameParser :: Parser String-nameParser = many1 alphaNum---- | Parses a lambda abstraction. The '\' is used as lambda. -lambdaAbstractionParser :: Parser NamedLambda-lambdaAbstractionParser = LambdaAbstraction <$>- (char lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)---- | Char used to represent lambda in user's input.-lambdaChar :: Char-lambdaChar = '\\'---- | Shows a lambda expression with named variables.--- Parentheses are ignored; they are written only around applications.-showNamedLambda :: NamedLambda -> String-showNamedLambda (LambdaVariable c) = c-showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e ++ ""-showNamedLambda (LambdaApplication f g) = "(" ++ showNamedLambda f ++ " " ++ showNamedLambda g ++ ")"--instance Show NamedLambda where- show = showNamedLambda------- | Translates a named variable expression into a DeBruijn one.--- Uses a dictionary of already binded numbers and variables.-tobruijn :: Map.Map String Integer -- ^ dictionary of the names of the variables used- -> Context -- ^ dictionary of the names already binded on the scope- -> NamedLambda -- ^ initial expression- -> Exp--- Every lambda abstraction is inserted in the variable dictionary,--- and every number in the dictionary increases to reflect we are entering--- into a deeper context.-tobruijn d context (LambdaAbstraction c e) = Lambda $ tobruijn newdict context e- where newdict = Map.insert c 1 (Map.map succ d)--- Translation of applications is trivial.-tobruijn d context (LambdaApplication f g) = App (tobruijn d context f) (tobruijn d context g)--- Every variable is checked on the variable dictionary and in the current scope.-tobruijn d context (LambdaVariable c) =- case Map.lookup c d of- Just n -> Var n- Nothing -> fromMaybe (Var 0) (MultiBimap.lookupR c context)---- | Transforms a lambda expression with named variables to a deBruijn index expression.--- Uses only the dictionary of the variables in the current context. -toBruijn :: Context -- ^ Variable context- -> NamedLambda -- ^ Initial lambda expression with named variables- -> Exp-toBruijn = tobruijn Map.empty------ | Translates a deBruijn expression into a lambda expression--- with named variables, given a list of used and unused variable names.-nameIndexes :: [String] -> [String] -> Exp -> NamedLambda-nameIndexes _ _ (Var 0) = LambdaVariable "undefined"-nameIndexes used _ (Var n) = LambdaVariable (used !! pred (fromInteger n))-nameIndexes used new (Lambda e) = LambdaAbstraction (head new) (nameIndexes (head new:used) (tail new) e)-nameIndexes used new (App f g) = LambdaApplication (nameIndexes used new f) (nameIndexes used new g)---- | Gives names to every variable in a deBruijn expression using--- alphabetic order.-nameExp :: Exp -> NamedLambda-nameExp = nameIndexes [] variableNames---- | A list of all possible variable names in lexicographical order.-variableNames :: [String]-variableNames = concatMap (`replicateM` ['a'..'z']) [1..]
README.md view
@@ -1,83 +1,12 @@ # mikrokosmos +<p align="center">+ <img src ="https://raw.githubusercontent.com/M42/mikrokosmos/master/docs/icon.svg.png" />+</p>+ **Mikrokosmos** is an untyped lambda calculus interpreter, borrowing its name from the series of progressive piano études *[Mikrokosmos](https://www.youtube.com/watch?v=VEsMk3DAzWM)* written by *Bela Bartok*. It aims to provide students with a tool to learn and understand lambda calculus.-If you want to start learning about lambda calculus, I suggest you to read: - * [The wikipedia page on Lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus#Informal_description)- * [A tutorial introduction to the Lambda calculus by Raúl Rojas](www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf)--And to install and to tinker with this interpreter.--## Installation--Mikrokosmos is installable from [Hackage](http://hackage.haskell.org/); you can install it directly from `cabal`: -```-cabal update-cabal install mikrokosmos-```--You can also install it by cloning the git repository and using [cabal](https://www.haskell.org/cabal/):--``` bash-git clone https://github.com/M42/mikrokosmos.git-cd mikrokosmos-cabal install-```--If you have `ghc` version 8 or greater you can also compile it directly using:--``` bash-git clone https://github.com/M42/mikrokosmos.git-cd mikrokosmos-ghc Main.hs-```--## First steps--Once installed, you can open the interpreter typing `mikrokosmos` in your terminal. It will show you a prompt where-you can write lambda expressions to evaluate them:----You can write expressions using `\var.` to denote a lambda abstraction on the `var` variable and-you can bind names to expressions using `=`. As you can see in the image, whenever the interpreter finds a known constant, it labels the expression with its name.--If you need help at any moment, you can type `:help` into the prompt to get a summary of the available options:----## The standard library--Mikrokosmos comes bundled with a standard library in a file called `std.mkr`; if it was not the case for you, you can download the [library](https://raw.githubusercontent.com/M42/mikrokosmos/master/std.mkr) from the git repository. It allows you to experiment with [Church encoding](https://en.wikipedia.org/wiki/Church_encoding) of booleans,-integers and much more. You can load it with `:load std.mkr`, given the file is in your working directory; after that, you can use a lot of new constants:----All this is written in lambda calculus! You can check the definitions on the `std.mkr` file.--## Debugging and verbose mode--If you want to check how the lambda reductions are being performed you can use the **verbose mode**.-It can be activated and deactivated writing `:verbose`, and it will show you every step on the reduction of-the expression, coloring the substitution at every step.----It uses [DeBruijn notation](https://en.wikipedia.org/wiki/De_Bruijn_notation) to show the substitutions, because this is the internal representation used by the interpreter. The term in red is being substituted by the term in yellow. --## Advanced data structures--There are representations of structures such as linked lists or trees in the standard library. -You can use them to do a bit of your usual functional programming:----Oh! And you can insert comments with `#`, both in the interpreter and in the files the interpreter can load.--### References & interesting links-* [Build you a Haskell - Stephen Diehl](http://dev.stephendiehl.com/fun/003_lambda_calculus.html) -* [Haskell from Scratch - Jekor](https://www.youtube.com/playlist?list=PLxj9UAX4Em-Ij4TKwKvo-SLp-Zbv-hB4B) -* [The Glambda interpreter](https://github.com/goldfirere/glambda) -* [Lecture notes on the lambda calculus - Peter Selinger](http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf)+ * [Mikrokosmos user's guide](https://m42.github.io/mikrokosmos/).+ * [Mikrokosmos on Hackage](https://hackage.haskell.org/package/mikrokosmos).
− Setup.hs
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
mikrokosmos.cabal view
@@ -1,5 +1,5 @@ name: mikrokosmos-version: 0.2.0+version: 0.3.0 synopsis: Lambda calculus interpreter description: A didactic untyped lambda calculus interpreter. homepage: https://github.com/M42/mikrokosmos@@ -12,7 +12,7 @@ build-type: Simple extra-source-files: README.md cabal-version: >=1.10-tested-with: GHC == 8.0.1+tested-with: GHC == 8.0.2 extra-source-files: std.mkr source-repository head@@ -22,6 +22,7 @@ executable mikrokosmos+ hs-source-dirs: ./source main-is: Main.hs build-depends: base >=4.7 && <5, mtl >=2.2,@@ -30,13 +31,19 @@ parsec >=3, ansi-terminal, multimap,- HUnit >=1.0+ HUnit >=1.0,+ options,+ tasty,+ tasty-hunit,+ directory >= 1.0 other-modules: Format Lambda NamedLambda MultiBimap Interpreter+ Environment+ Ski default-language: Haskell2010 ghc-options: -Wall
+ source/Environment.hs view
@@ -0,0 +1,111 @@+{-|+Module: Environment+Description: Internal state and environment of the interpreter+License: GPL-3++This module contains all the auxiliary logic necessary to represent the internal+state of the interpreter.+-}+module Environment+ (+ -- * Environment+ Environment+ , context+ , defaultEnv++ -- * Reading the environment+ , getVerbose+ , getColor+ , getSki+ , getExpressionName+ + -- * Modifying the environment+ , addBind+ , changeColor+ , changeVerbose+ , changeSkioutput++ -- * Filenames and Modulenames+ , Filename+ , Modulename+ )+where++import Data.List+import MultiBimap+import Lambda++-- | A filename is a string containing the directory path and+-- the real name of the file.+type Filename = String++-- | A modulename is a string naming a module.+type Modulename = String+++data Environment = Environment+ { context :: Context+ , loadedFiles :: [Filename]+ , verbose :: Bool+ , color :: Bool+ , skioutput :: Bool+ }++-- | Default environment for the interpreter.+defaultEnv :: Environment+defaultEnv = Environment+ { context = emptyContext+ , loadedFiles = []+ , verbose = False+ , color = True+ , skioutput = False+ }+++-- | Adds a name binding to the environment+addBind :: Environment -> String -> Exp -> Environment+addBind env s e =+ -- If the binding already exists, it changes nothing+ if elem s (MultiBimap.lookup e $ context env)+ then env+ else env {context = MultiBimap.insert e s (context env)}++-- | Gets the color configuration+getColor :: Environment -> Bool+getColor = color++-- | Gets the verbose configuration+getVerbose :: Environment -> Bool+getVerbose = verbose++-- | Gets the verbose configuration+getSki :: Environment -> Bool+getSki = skioutput++-- | Sets the verbose configuration on/off.+changeVerbose :: Environment -> Bool -> Environment+changeVerbose options setting = options {verbose = setting}++-- | Sets the color configuration on/off+changeColor :: Environment -> Bool -> Environment+changeColor options setting = options {color = setting}++-- | Sets the ski output configuration on/off+changeSkioutput :: Environment -> Bool -> Environment+changeSkioutput options setting = options {skioutput = setting}++-- | Given an expression, returns its name if it is bounded to any.+getExpressionName :: Environment -> Exp -> Maybe String+getExpressionName environment expr = case MultiBimap.lookup expr (context environment) of+ [] -> Nothing+ xs -> Just $ intercalate ", " xs++++-- | A context is an application between expressions and the names+-- they may have.+type Context = MultiBimap Exp String++-- | Empty context without any bindings+emptyContext :: Context+emptyContext = MultiBimap.empty
+ source/Format.hs view
@@ -0,0 +1,142 @@+{-|+Module: Format+Description: Formatting the output of the interpreter+License: GPL-3++This module controls the format of the text and expressions printed by the+interpreter. Uses ANSI escape sequences to color the terminal and mark text+as bold or italics. It also stores the texts showed by the interpreter.+-}++module Format+ (+ -- * Formatting+ formatFormula+ , formatIntro+ , formatLoading+ , formatPrompt+ , formatName+ , formatSubs1+ , formatSubs2+ , decolor+ , end++ -- * Interpreter texts+ , promptText+ , helpText+ , initialText+ , versionText+ )+where++import System.Console.ANSI+import Data.List+import Data.Monoid++-- Colors+-- | Prompt messages color+promptColor :: Color+promptColor = Blue++-- | Named variables color+nameColor :: Color+nameColor = Green++-- | Substitutions are marked with this color+substColor :: Color+substColor = Cyan++-- | To-be-substituted expressions are marked with this color+subst2Color :: Color+subst2Color = Cyan+++-- Format sequences+-- | Sequence of characters that signals the format of a formula to the terminal.+formatFormula :: String+formatFormula = setSGRCode [SetConsoleIntensity NormalIntensity, SetColor Foreground Dull promptColor]++-- | Sequence of characters that signals the format of the introduction to the terminal.+formatIntro :: String+formatIntro = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull promptColor]++-- | Sequence of characters that signals the format of the loading of a module to the terminal.+formatLoading :: String+formatLoading = formatIntro++-- | Sequence of characters that signals the format of the prompt to the terminal.+formatPrompt :: String+formatPrompt = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid promptColor]++-- | Sequence of characters that signals the format of a name to the terminal.+formatName :: String+formatName = setSGRCode [SetColor Foreground Dull nameColor]++-- | Sequence of characters that signals the format of a substitution to the terminal.+formatSubs1 :: String+formatSubs1 = setSGRCode [SetConsoleIntensity BoldIntensity, SetColor Foreground Dull substColor]++-- | Sequence of characters that signals the format of a expression which will+-- be substituted in the next reduction step to the terminal.+formatSubs2 :: String+formatSubs2 = setSGRCode [SetConsoleIntensity FaintIntensity, SetColor Foreground Dull subst2Color]++-- | Sequence of characters that cleans all the format.+end :: String+end = setSGRCode []+++-- | Removes all the ocurrences of a string from the other+removeString :: String -> String -> String+removeString _ "" = ""+removeString t s@(c:sc)+ | t `isPrefixOf` s = removeString t (drop (length t) s)+ | otherwise = c : removeString t sc++-- | Removes all color from a string+decolor :: String -> String+decolor = appEndo $ mconcat $ map (Endo . removeString)+ [ formatSubs1+ , formatSubs2+ , formatFormula+ , formatIntro+ , formatName+ , formatPrompt+ , formatLoading+ , end+ ]++++-- | Prompt line. It is shown when the interpreter asks the user+-- to introduce a new command.+promptText :: String+promptText = formatPrompt ++ "mikro> " ++ end++-- | Help line. It is shown when the user uses the :help command.+helpText :: String+helpText = unlines [+ formatFormula +++ "Commands available from the prompt:",+ "\t<expression>\t evaluates the expression",+ "\t:quit \t quits the interpreter",+ "\t:load <file>\t loads the given .mkr library or script",+ "\t:verbose \t sets verbose mode on/off",+ "\t:help \t shows this help"+ ++ end+ ]++-- | Initial text on the interpreter. It is shown at startup.+initialText :: String+initialText = unlines [+ formatIntro ++ "Welcome to the Mikrokosmos Lambda Interpreter!" ++ end,+ formatFormula ++ "Version " ++ version ++ ". GNU General Public License Version 3." ++ end+ ]++-- | Version complete text+versionText :: String+versionText = "Mikrokosmos, version " ++ version++-- | Version+version :: String+version = "0.3.0"
+ source/Interpreter.hs view
@@ -0,0 +1,179 @@+{-|+Module: Interpreter+Description: Internal logic of the interpreter+License: GPL-3++This module contains auxiliary logic, types and representations of+the internal state of the interpreter.+-}+module Interpreter+ ( + -- * Interpreter actions+ InterpreterAction (..)+ , interpreteractionParser+ , act+ , multipleAct+ , Action (..)+ , actionParser+ )+where++import Control.Applicative ((<$>), (<*>))+import Control.Monad.State.Lazy +import Text.ParserCombinators.Parsec hiding (State)+import Data.Char+import Format+import Environment+import NamedLambda+import Lambda+import Ski+++-- | Interpreter action. It can be a language action (binding and evaluation)+-- or an interpreter specific one, such as "quit".+data InterpreterAction = Interpret Action -- ^ Language action+ | EmptyLine -- ^ Empty line, it will be ignored+ | Error -- ^ Error on the interpreter+ | Quit -- ^ Close the interpreter+ | Load String -- ^ Load the given file+ | SetVerbose Bool -- ^ Changes verbosity+ | SetColor Bool -- ^ Changes colors+ | SetSki Bool -- ^ Changes ski output+ | Help -- ^ Shows help++-- | Language action. The language has a number of possible valid statements;+-- all on the following possible forms.+data Action = Bind (String, NamedLambda) -- ^ bind a name to an expression+ | EvalBind (String, NamedLambda) -- ^ bind a name to an expression and simplify it+ | Execute NamedLambda -- ^ execute an expression+ | Comment -- ^ comment+++-- | Executes a language action. Given a context and an action, returns+-- the new context after the action and a text output.+act :: Action -> State Environment [String]+act Comment = return [""]+act (Bind (s,le)) =+ do modify (\env -> addBind env s (toBruijn (context env) le))+ return [""]+act (EvalBind (s,le)) =+ do modify (\env -> addBind env s (simplifyAll $ toBruijn (context env) le))+ return [""]+act (Execute le) =+ do env <- get+ return [unlines $+ [ show le ] +++ [ unlines $ map showReduction $ simplifySteps $ toBruijn (context env) le ] +++ [ showCompleteExp env $ simplifyAll $ toBruijn (context env) le ] + ]+++-- | Executes multiple actions. Given a context and a set of actions, returns+-- the new context after the sequence of actions and a text output.+multipleAct :: [Action] -> State Environment [String]+multipleAct actions = concat <$> mapM act actions+++-- | Shows an expression and the name that is bound to the expression+-- in the current context+showCompleteExp :: Environment -> Exp -> String+showCompleteExp environment expr = let+ lambdaname = show $ nameExp expr+ skiname = if getSki environment+ then formatSubs2 ++ " ⇒ " ++ (show $ skiabs $ nameExp expr) ++ end+ else ""+ in+ case getExpressionName environment expr of+ Nothing -> lambdaname ++ skiname+ Just expName -> lambdaname ++ skiname ++ formatName ++ " ⇒ " ++ expName ++ end + ++++++-- Parsing of interpreter command line commands.+-- | Parses an interpreter action.+interpreteractionParser :: Parser InterpreterAction+interpreteractionParser = choice+ [ try interpretParser+ , try quitParser+ , try loadParser+ , try verboseParser+ , try colorParser+ , try skiOutputParser+ , try helpParser+ ]++-- | Parses a language action as an interpreter action.+interpretParser :: Parser InterpreterAction+interpretParser = Interpret <$> actionParser++-- | Parses a language action.+actionParser :: Parser Action+actionParser = choice+ [ try bindParser+ , try evalbindParser+ , try executeParser+ , try commentParser+ ]++-- | Parses a binding between a variable an its representation.+bindParser :: Parser Action+bindParser = fmap Bind $ (,) <$> many1 alphaNum <*> (spaces >> string "!=" >> spaces >> lambdaexp)++-- | Parses a binding and evaluation expression between a variable an its representation+evalbindParser :: Parser Action+evalbindParser = fmap EvalBind $ (,) <$> many1 alphaNum <*> (spaces >> string "=" >> spaces >> lambdaexp)++-- | Parses an expression in order to execute it.+executeParser :: Parser Action+executeParser = Execute <$> lambdaexp++-- | Parses comments.+commentParser :: Parser Action+commentParser = string "#" >> many anyChar >> return Comment++-- | Parses a "quit" command.+quitParser :: Parser InterpreterAction+quitParser = string ":quit" >> return Quit++-- | Parses a "help" command.+helpParser :: Parser InterpreterAction+helpParser = string ":help" >> return Help++-- | Parses a change in verbosity.+verboseParser :: Parser InterpreterAction+verboseParser = choice+ [ try verboseonParser+ , try verboseoffParser+ ]+ where+ verboseonParser = string ":verbose on" >> return (SetVerbose True)+ verboseoffParser = string ":verbose off" >> return (SetVerbose False)++-- | Parses a change in color.+colorParser :: Parser InterpreterAction+colorParser = choice+ [ try coloronParser+ , try coloroffParser+ ]+ where+ coloronParser = string ":color on" >> return (SetColor True)+ coloroffParser = string ":color off" >> return (SetColor False)++-- | Parses a change in ski output.+skiOutputParser :: Parser InterpreterAction+skiOutputParser = choice+ [ try skionParser+ , try skioffParser+ ]+ where+ skionParser = string ":ski on" >> return (SetSki True)+ skioffParser = string ":ski off" >> return (SetSki False)++++-- | Parses a "load-file" command.+loadParser :: Parser InterpreterAction+loadParser = Load <$> (string ":load" >> between spaces spaces (many1 (satisfy (not . isSpace))))
+ source/Lambda.hs view
@@ -0,0 +1,138 @@+{-|+Module: Lambda+Description: DeBruijn lambda expressions.+License: GPL-3++This module deals with the parsing, reduction and printing of lambda+expressions using DeBruijn notation. The interpreter uses DeBruijn+notation as an internal representation and as output format. This is because+it is easier to do beta reduction with DeBruijn indexes.+-}++module Lambda+ ( Exp (Var, Lambda, App)+ , simplifyAll+ , simplifySteps+ , showReduction+-- , freein+ )+where++import Format++-- DeBruijn Expressions+-- | A lambda expression using DeBruijn indexes.+data Exp = Var Integer -- ^ integer indexing the variable.+ | Lambda Exp -- ^ lambda abstraction+ | App Exp Exp -- ^ function application+ deriving (Eq, Ord)++instance Show Exp where+ show = showexp+++-- | Shows an expression with DeBruijn indexes.+showexp :: Exp -> String+showexp (Var n) = show n+showexp (Lambda e) = "λ" ++ showexp e ++ ""+showexp (App f g) = "(" ++ showexp f ++ " " ++ showexp g ++ ")"++-- | Shows an expression coloring the next reduction.+showReduction :: Exp -> String+showReduction (Lambda e) = "λ" ++ showReduction e+showReduction (App (Lambda f) x) = betaColor (App (Lambda f) x)+showReduction (Var e) = show e+showReduction (App rs x) = "(" ++ showReduction rs ++ " "+ ++ showReduction x ++ ")"++-- | Colors a beta reduction+betaColor :: Exp -> String+betaColor (App (Lambda e) x) =+ "(" +++ formatSubs1 ++ "λ" ++ formatFormula +++ indexColor 1 e +++ " " +++ formatSubs2 ++ showexp x ++ formatFormula+ ++ ")"+betaColor e = show e++-- | Colors all the appearances of a given color+indexColor :: Integer -> Exp -> String+indexColor n (Lambda e) = "λ" ++ indexColor (succ n) e+indexColor n (App f g) = "(" ++ indexColor n f ++ " " ++ indexColor n g ++ ")"+indexColor n (Var m)+ | n == m = formatSubs1 ++ show m ++ formatFormula+ | otherwise = show m+++++-- Reductions of lambda expressions.++-- | Applies repeated simplification to the expression until it stabilizes and+-- returns the final simplified expression.+--+-- >>> simplifyAll $ App (Lambda (Var 1)) (Lambda (Var 1))+-- λ1+--+simplifyAll :: Exp -> Exp+simplifyAll = last . simplifySteps++-- | Applies repeated simplification to the expression until it stabilizes and+-- returns all the intermediate results.+--+-- >>> simplifySteps $ App (Lambda (Var 1)) (Lambda (Var 1))+-- [(λ1 λ1),λ1]+--+simplifySteps :: Exp -> [Exp]+simplifySteps e+ | e == s = [e]+ | otherwise = e : simplifySteps s+ where s = simplify e++-- | Simplifies the expression recursively.+-- Applies only a beta reduction at each step.+simplify :: Exp -> Exp+simplify (Lambda e) = Lambda (simplify e)+simplify (App (Lambda f) x) = betared (App (Lambda f) x)+simplify (App (Var e) x) = App (Var e) (simplify x)+simplify (App (App f g) x) = App (simplify (App f g)) x+simplify (Var e) = Var e++-- | Applies beta-reduction to a function application.+-- Leaves the rest of the operations untouched.+betared :: Exp -> Exp+betared (App (Lambda e) x) = substitute 1 x e+betared e = e++-- | Substitutes an index for a lambda expression+substitute :: Integer -- ^ deBruijn index of the desired target+ -> Exp -- ^ replacement for the index+ -> Exp -- ^ initial expression+ -> Exp+substitute n x (Lambda e) = Lambda (substitute (succ n) (incrementFreeVars 0 x) e)+substitute n x (App f g) = App (substitute n x f) (substitute n x g)+substitute n x (Var m)+ -- The lambda is replaced directly+ | n == m = x+ -- A more exterior lambda decreases a number+ | n < m = Var (m-1)+ -- An unrelated variable remains untouched+ | otherwise = Var m++-- | Increments free variables assuming they are bind to an+-- external lambda. This is done to substitute them correctly in+-- internal expressions.+incrementFreeVars :: Integer -> Exp -> Exp+incrementFreeVars n (App f g) = App (incrementFreeVars n f) (incrementFreeVars n g)+incrementFreeVars n (Lambda e) = Lambda (incrementFreeVars (succ n) e)+incrementFreeVars n (Var m)+ | m > n = Var (succ m)+ | otherwise = Var m+++-- | Determines if the given variable is free on the expression.+-- freein :: Integer -> Exp -> Bool+-- freein n (Var m) = n == m+-- freein n (Lambda e) = freein (succ n) e+-- freein n (App u v) = (freein n u) && (freein n v)
+ source/Main.hs view
@@ -0,0 +1,231 @@+module Main where++import Control.Monad.Trans+import Control.Monad.State+import Control.Exception+import Data.List+import System.Directory+import System.Console.Haskeline+import Text.ParserCombinators.Parsec hiding (try)+import Format+import Interpreter+import Environment+import Options hiding (defaultOptions)+++-- Lambda interpreter+-- The actions of the interpreter are written here. It allows to execute normal+-- actions (bindings and evaluation), and interpreter specific actions, as "quit"+-- or "load".+++-- | Runs the interpreter with default settings and an empty context.+main :: IO ()+main =+ -- Uses the Options library, which requires the program to start with+ -- runCommand. The flags are stored in opts and other command line arguments+ -- are stored in args.+ runCommand $ \opts args -> do+ + -- Reads the flags+ case flagVersion opts of+ True -> putStrLn versionText+ False ->+ case args of+ [] -> runInputT defaultSettings ( outputStrLn initialText+ >> interpreterLoop defaultEnv+ )+ [filename] -> executeFile filename+ _ -> putStrLn "Wrong number of arguments"+++-- | Interpreter awaiting for an instruction.+interpreterLoop :: Environment -> InputT IO ()+interpreterLoop environment = do+ -- Gets the user input on the interpreter+ -- and parses it to a concrete action.+ minput <- getInputLine promptText+ let interpreteraction =+ case minput of+ Nothing -> Quit+ Just "" -> EmptyLine+ Just input -> case parse interpreteractionParser "" input of+ Left _ -> Error+ Right a -> a++ -- Executes the parsed action, every action may affect the+ -- context in a way, and returns the control to the interpreter. + case interpreteraction of+ -- Interprets an action+ Interpret action -> case runState (act action) environment of+ (output, newenv) -> do+ outputActions newenv output+ interpreterLoop newenv++ -- Loads a module and its dependencies given its name.+ -- Avoids repeated modules keeping only their first ocurrence.+ Load modulename -> do+ modules <- lift $ (nub <$> readAllModuleDepsRecursively [modulename])+ files <- lift $ mapM findFilename modules++ -- Concats all the module contents+ maybeactions <- (fmap concat) . sequence <$> (lift $ mapM loadFile files)+ case maybeactions of+ Nothing -> do+ outputStrLn "Error loading file"+ interpreterLoop environment+ Just actions -> case runState (multipleAct actions) environment of+ (output, newenv) -> do+ outputActions newenv output+ interpreterLoop newenv+ + -- Ignores the empty line+ EmptyLine -> interpreterLoop environment+ + -- Exists the interpreter+ Quit -> return ()++ -- Unknown command+ Error -> do+ outputStr (if getColor environment then formatFormula else "")+ outputStrLn "Unknown command"+ outputStr end+ interpreterLoop environment++ -- Sets the verbose option+ SetVerbose setting -> do+ outputStrLn $+ (if getColor environment then formatFormula else "") +++ "verbose mode: " ++ if setting then "on" else "off" +++ end+ interpreterLoop (changeVerbose environment setting)+ + -- Sets the color option+ SetColor setting -> do+ outputStrLn $+ (if getColor environment then formatFormula else "") +++ "color mode: " ++ if setting then "on" else "off" +++ end+ interpreterLoop (changeColor environment setting)++ -- Sets the ski option+ SetSki setting -> do+ outputStrLn $+ (if getColor environment then formatFormula else "") +++ "ski mode: " ++ if setting then "on" else "off" +++ end+ interpreterLoop (changeSkioutput environment setting)++ + -- Prints the help+ Help -> outputStr helpText >> interpreterLoop environment+++++-- | Outputs results from actions. Given a list of options and outputs,+-- formats and prints them in console.+outputActions :: Environment -> [String] -> InputT IO ()+outputActions environment output = do+ outputStr (if getColor environment then formatFormula else "")+ mapM_ (outputStr . format) output+ outputStr end+ where+ format = formatColor . formatVerbose++ formatColor s+ | getColor environment = s+ | otherwise = unlines $ map decolor $ lines s+ + formatVerbose "" = ""+ formatVerbose s+ | not (getVerbose environment) = (++"\n") . last . lines $ s+ | otherwise = s++++-- Loading and reading files+-- | Loads the given filename and returns the complete list of actions.+-- Returns Nothing if there is an error reading or parsing the file.+loadFile :: String -> IO (Maybe [Action])+loadFile filename = do+ putStrLn $ formatLoading ++ "Loading " ++ filename ++ "..." ++ end+ input <- try $ (readFile filename) :: IO (Either IOException String)+ case input of+ Left _ -> return Nothing+ Right inputs -> do+ let parsing = map (parse actionParser "") $ filter (/="") $ lines inputs+ let actions = map (\x -> case x of+ Left _ -> Nothing+ Right a -> Just a) parsing+ return $ sequence actions++-- | Executes the commands inside a file. A .mkr file can contain a sequence of+-- expressions and variable bindings, and it is interpreted sequentially.+executeFile :: Filename -> IO ()+executeFile filename = do+ maybeloadfile <- loadFile filename+ case maybeloadfile of+ Nothing -> putStrLn "Error loading file"+ Just actions -> case runState (multipleAct actions) defaultEnv of+ (outputs, _) -> mapM_ (putStr . format) outputs+ where+ format :: String -> String+ format "" = ""+ format s = (++"\n") . last . lines $ s+++-- | Reads module dependencies+readFileDependencies :: Filename -> IO [Modulename]+readFileDependencies filename = do+ input <- try $ (readFile filename) :: IO (Either IOException String)+ case input of+ Left _ -> return []+ Right inputs -> return $+ map (drop 9) (filter (isPrefixOf "#INCLUDE ") $ filter (/="") $ lines inputs)++-- | Reads all the dependencies from a module list+readAllModuleDeps :: [Modulename] -> IO [Modulename]+readAllModuleDeps modulenames = do+ files <- mapM findFilename modulenames+ deps <- mapM readFileDependencies files+ return $ concat deps++-- | Read module dependencies recursively+readAllModuleDepsRecursively :: [Modulename] -> IO [Modulename]+readAllModuleDepsRecursively modulenames = do+ newmodulenames <- readAllModuleDeps modulenames+ let allmodulenames = nub (newmodulenames ++ modulenames)+ if modulenames == allmodulenames+ then return modulenames+ else readAllModuleDepsRecursively allmodulenames++-- | Given a module name, returns the filename associated with it+findFilename :: Modulename -> IO Filename+findFilename s = do+ appdir <- getAppUserDataDirectory "mikrokosmos"+ homedir <- getHomeDirectory++ -- Looks for the module in the common locations+ head <$> filterM doesFileExist+ [ "lib/" ++ s ++ ".mkr"+ , "./" ++ s ++ ".mkr"+ , appdir ++ "/" ++ s ++ ".mkr"+ , homedir ++ "/" ++ s ++ ".mkr"+ ]+++-- Flags+-- | Flags datatype+data MainFlags = MainFlags+ { flagExec :: String+ , flagVersion :: Bool+ }++instance Options MainFlags where+ -- | Flags definition+ defineOptions = pure MainFlags+ <*> simpleOption "exec" ""+ "A file to execute and show its results"+ <*> simpleOption "version" False+ "Show program version"
+ source/MultiBimap.hs view
@@ -0,0 +1,52 @@+{-|+Module: MultiBimap+Description: A multibimap implementation+License: GPL-3++This module allows us to abstract a bidirectional multimap without+having to worry about implementation details. It is useful in the translation+between lambda expressions and names.+ +Based on the bimap package:+<https://hackage.haskell.org/package/bimap-0.3.2/docs/Data-Bimap.html>+-}+module MultiBimap+ ( MultiBimap+ , empty+ , null+ , insert+ , lookup+ , lookupR+ )+where++++import qualified Data.Map as M+import qualified Data.MultiMap as MM+import Prelude hiding (null,lookup)++data MultiBimap k v = MkMultiBimap (MM.MultiMap k v) (M.Map v k)++-- | The empty multi-bimap+empty :: MultiBimap k v+empty = MkMultiBimap MM.empty M.empty++-- | True if the multi-bimap is empty+null :: MultiBimap k v -> Bool+null (MkMultiBimap _ right) = M.null right++-- | Inserts a key-value in the multi-bimap.+-- The value can have been used earlier.+insert :: (Ord k, Ord v) => k -> v -> MultiBimap k v -> MultiBimap k v+insert k v (MkMultiBimap left right) =+ MkMultiBimap (MM.insert k v left) (M.insert v k right)++-- | Lookup a key in the multi-bimap, returning the list of+-- associated values.+lookup :: (Ord k) => k -> MultiBimap k v -> [v]+lookup k (MkMultiBimap left _) = MM.lookup k left++-- | Lookup a right value in the multi-bimap, returning the associated key.+lookupR :: (Ord v) => v -> MultiBimap k v -> Maybe k+lookupR v (MkMultiBimap _ right) = M.lookup v right
+ source/NamedLambda.hs view
@@ -0,0 +1,133 @@+{-|+Module: NamedLambda+Description: Lambda expressions with named variables+License: GPL-3++This package deals with lambda expressions containing named variables+instead of DeBruijn indexes. It contains parsing and printing fuctions.+-}++module NamedLambda+ ( NamedLambda (LambdaVariable, LambdaAbstraction, LambdaApplication)+ , lambdaexp+ , toBruijn+ , nameExp+ )+where++import Text.ParserCombinators.Parsec+import Control.Applicative ((<$>), (<*>))+import qualified Data.Map.Strict as Map+import Lambda+import MultiBimap+import Data.Maybe+import Control.Monad++type Context = MultiBimap Exp String++-- Parsing of Lambda Expressions.+-- The user can input a lambda expression with named variables, of+-- the form of "\x.x" or "(\a.(\b.a b))". The interpreter will parse+-- it into an internal representation.++-- | A lambda expression with named variables.+data NamedLambda = LambdaVariable String -- ^ variable+ | LambdaAbstraction String NamedLambda -- ^ lambda abstraction+ | LambdaApplication NamedLambda NamedLambda -- ^ function application++-- | Parses a lambda expression with named variables.+-- A lambda expression is a sequence of one or more autonomous+-- lambda expressions. They are parsed assuming left-associativity.+--+-- >>> parse lambdaexp "" "\\f.\\x.f x"+-- Right λf.λx.(f x)+--+-- Note that double backslashes are neccessary only when we quote strings;+-- it will work only with a simple backslash in the interpreter.+lambdaexp :: Parser NamedLambda+lambdaexp = foldl1 LambdaApplication <$> (spaces >> sepBy1 simpleexp spaces)++-- | Parses a simple lambda expression, without function applications+-- at the top level. It can be a lambda abstraction, a variable or another+-- potentially complex lambda expression enclosed in parentheses.+simpleexp :: Parser NamedLambda+simpleexp = choice [lambdaAbstractionParser, variableParser, parens lambdaexp]++-- | The returned parser parenthesizes the given parser+parens :: Parser a -> Parser a+parens = between (char '(') (char ')')++-- | Parses a variable. Any name can form a lambda variable.+variableParser :: Parser NamedLambda+variableParser = LambdaVariable <$> nameParser++-- | Allowed variable names+nameParser :: Parser String+nameParser = many1 alphaNum++-- | Parses a lambda abstraction. The '\' is used as lambda. +lambdaAbstractionParser :: Parser NamedLambda+lambdaAbstractionParser = LambdaAbstraction <$>+ (char lambdaChar >> nameParser) <*> (char '.' >> lambdaexp)++-- | Char used to represent lambda in user's input.+lambdaChar :: Char+lambdaChar = '\\'++-- | Shows a lambda expression with named variables.+-- Parentheses are ignored; they are written only around applications.+showNamedLambda :: NamedLambda -> String+showNamedLambda (LambdaVariable c) = c+showNamedLambda (LambdaAbstraction c e) = "λ" ++ c ++ "." ++ showNamedLambda e ++ ""+showNamedLambda (LambdaApplication f g) = "(" ++ showNamedLambda f ++ " " ++ showNamedLambda g ++ ")"++instance Show NamedLambda where+ show = showNamedLambda+++++-- | Translates a named variable expression into a DeBruijn one.+-- Uses a dictionary of already binded numbers and variables.+tobruijn :: Map.Map String Integer -- ^ dictionary of the names of the variables used+ -> Context -- ^ dictionary of the names already binded on the scope+ -> NamedLambda -- ^ initial expression+ -> Exp+-- Every lambda abstraction is inserted in the variable dictionary,+-- and every number in the dictionary increases to reflect we are entering+-- into a deeper context.+tobruijn d context (LambdaAbstraction c e) = Lambda $ tobruijn newdict context e+ where newdict = Map.insert c 1 (Map.map succ d)+-- Translation of applications is trivial.+tobruijn d context (LambdaApplication f g) = App (tobruijn d context f) (tobruijn d context g)+-- Every variable is checked on the variable dictionary and in the current scope.+tobruijn d context (LambdaVariable c) =+ case Map.lookup c d of+ Just n -> Var n+ Nothing -> fromMaybe (Var 0) (MultiBimap.lookupR c context)++-- | Transforms a lambda expression with named variables to a deBruijn index expression.+-- Uses only the dictionary of the variables in the current context. +toBruijn :: Context -- ^ Variable context+ -> NamedLambda -- ^ Initial lambda expression with named variables+ -> Exp+toBruijn = tobruijn Map.empty++++-- | Translates a deBruijn expression into a lambda expression+-- with named variables, given a list of used and unused variable names.+nameIndexes :: [String] -> [String] -> Exp -> NamedLambda+nameIndexes _ _ (Var 0) = LambdaVariable "undefined"+nameIndexes used _ (Var n) = LambdaVariable (used !! pred (fromInteger n))+nameIndexes used new (Lambda e) = LambdaAbstraction (head new) (nameIndexes (head new:used) (tail new) e)+nameIndexes used new (App f g) = LambdaApplication (nameIndexes used new f) (nameIndexes used new g)++-- | Gives names to every variable in a deBruijn expression using+-- alphabetic order.+nameExp :: Exp -> NamedLambda+nameExp = nameIndexes [] variableNames++-- | A list of all possible variable names in lexicographical order.+variableNames :: [String]+variableNames = concatMap (`replicateM` ['a'..'z']) [1..]
+ source/Ski.hs view
@@ -0,0 +1,98 @@+{-|+Module: Ski+Description: Ski expressions and bracket abstraction.+License: GPL-3++This module implements a representation of the SKI subset of the+calculus of combinators. It provides a lambda abstraction algorithm+writing lambda expressions as combinators.+-}++module Ski+ ( Ski (S, K, I, Comb)+ , skiabs+ )+where++import NamedLambda++-- | A SKI combinator expression+data Ski = S | K | I | Comb Ski Ski | Cte String+ deriving (Eq, Ord)++instance Show Ski where+ show = showski++-- | Shows a SKI expression+showski :: Ski -> String+showski S = "S"+showski K = "K"+showski I = "I"+showski (Cte _) = "?"+showski (Comb x S) = showski x ++ showski S+showski (Comb x K) = showski x ++ showski K+showski (Comb x I) = showski x ++ showski I+showski (Comb x (Cte c)) = showski x ++ showski (Cte c)+showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")"++++-- | SKI abstraction of a named lambda term. From a lambda expression+-- creates a SKI equivalent expression. The following algorithm is a+-- version of the algorithm 9.10 on the Hindley-Seldin book.+skiabs :: NamedLambda -> Ski+skiabs (LambdaVariable x) = Cte x+skiabs (LambdaApplication m n) = Comb (skiabs m) (skiabs n)+skiabs (LambdaAbstraction x m) = bracketabs x (skiabs m)++-- | Bracket abstraction of a SKI term, as defined in Hindley-Seldin+-- (2.18).+bracketabs :: String -> Ski -> Ski+bracketabs _ S = Comb K S+bracketabs _ K = Comb K K+bracketabs _ I = Comb K I+bracketabs x (Cte y) = if x == y then I else Comb K (Cte y)+bracketabs x (Comb u (Cte y))+ | freein x u && x == y = u+ | freein x u = Comb K (Comb u (Cte y))+ | otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x (Cte y))+bracketabs x (Comb u v)+ | freein x (Comb u v) = Comb K (Comb u v)+ | otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x v)++-- | Checks if a given variable is used on a SKI expression.+freein :: String -> Ski -> Bool+freein _ S = True+freein _ K = True+freein _ I = True+freein x (Cte y) = not (x == y)+freein x (Comb u v) = freein x u && freein x v+++-- -- | Bracket abstraction of a lambda term. The following algorithm is+-- -- an adaptation to deBruijn indexes of the definition 2.18 and 9.10+-- -- of the Hindley-Seldin book.+-- skiabs :: Exp -> Ski++-- -- Error, the formula is not a closed one+-- skiabs (Var n) = undefined++-- -- The first case is the identity+-- skiabs (Lambda (Var 1)) = I++-- -- Only if the variable is free+-- skiabs (Lambda (App u (Var 1)))+-- | freein 1 u = skiabs u+-- | otherwise = Comb (Comb S (skiabs u)) I++-- -- Combination+-- skiabs (Lambda m@(App u v))+-- | freein 1 m = Comb K (skiabs m)+-- | otherwise = Comb (Comb S (skiabs u)) (skiabs v)++-- -- Error on pattern matching+-- skiabs (Lambda e) = undefined++-- skiabs (App u v) = Comb (skiabs u) (skiabs v)++
std.mkr view
@@ -82,7 +82,7 @@ ## Fixpoint operator and recursion fix != (\f.(\x.f (x x)) (\x.f (x x))) fact != fix (\f.\n.iszero n (succ 0) (mult n (f (pred n))))-fib != fix (\f.\n.iszero n 1 (plus (f (pred n)) (f (pred (pred n)))))+fib != fix (\f.\n.iszero n (succ 0) (plus (f (pred n)) (f (pred (pred n)))))