diff --git a/Format.hs b/Format.hs
deleted file mode 100644
--- a/Format.hs
+++ /dev/null
@@ -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
-  ]
diff --git a/Interpreter.hs b/Interpreter.hs
deleted file mode 100644
--- a/Interpreter.hs
+++ /dev/null
@@ -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))))
diff --git a/Lambda.hs b/Lambda.hs
deleted file mode 100644
--- a/Lambda.hs
+++ /dev/null
@@ -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
diff --git a/Main.hs b/Main.hs
deleted file mode 100644
--- a/Main.hs
+++ /dev/null
@@ -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
diff --git a/MultiBimap.hs b/MultiBimap.hs
deleted file mode 100644
--- a/MultiBimap.hs
+++ /dev/null
@@ -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
diff --git a/NamedLambda.hs b/NamedLambda.hs
deleted file mode 100644
--- a/NamedLambda.hs
+++ /dev/null
@@ -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..]
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -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:
-
-![First steps](https://cloud.githubusercontent.com/assets/5337877/18649151/337c6782-7ebe-11e6-9701-495c2cb40675.gif)
-
-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:
-
-![Help screen](https://cloud.githubusercontent.com/assets/5337877/18882511/bfc84c34-84df-11e6-8215-870b29e49b8f.gif)
-
-## 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:
-
-![Standard library](https://cloud.githubusercontent.com/assets/5337877/18663278/1a6374e2-7f1e-11e6-99b5-279de7428a10.gif)
-
-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.
-
-![Verbose mode](https://cloud.githubusercontent.com/assets/5337877/18882803/060a2dec-84e1-11e6-9dfa-9c08957b559e.gif)
-
-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:
-
-![Trees](https://cloud.githubusercontent.com/assets/5337877/18883269/d7c3d616-84e2-11e6-9fc9-aa6e3df606f9.gif)
-
-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).
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/mikrokosmos.cabal b/mikrokosmos.cabal
--- a/mikrokosmos.cabal
+++ b/mikrokosmos.cabal
@@ -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
diff --git a/source/Environment.hs b/source/Environment.hs
new file mode 100644
--- /dev/null
+++ b/source/Environment.hs
@@ -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
diff --git a/source/Format.hs b/source/Format.hs
new file mode 100644
--- /dev/null
+++ b/source/Format.hs
@@ -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"
diff --git a/source/Interpreter.hs b/source/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/source/Interpreter.hs
@@ -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))))
diff --git a/source/Lambda.hs b/source/Lambda.hs
new file mode 100644
--- /dev/null
+++ b/source/Lambda.hs
@@ -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)
diff --git a/source/Main.hs b/source/Main.hs
new file mode 100644
--- /dev/null
+++ b/source/Main.hs
@@ -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"
diff --git a/source/MultiBimap.hs b/source/MultiBimap.hs
new file mode 100644
--- /dev/null
+++ b/source/MultiBimap.hs
@@ -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
diff --git a/source/NamedLambda.hs b/source/NamedLambda.hs
new file mode 100644
--- /dev/null
+++ b/source/NamedLambda.hs
@@ -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..]
diff --git a/source/Ski.hs b/source/Ski.hs
new file mode 100644
--- /dev/null
+++ b/source/Ski.hs
@@ -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)
+
+
diff --git a/std.mkr b/std.mkr
--- a/std.mkr
+++ b/std.mkr
@@ -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)))))