content: {-|
  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
    , executeWithEnv
    , librariesEnv
    , preformat
    )
  where
  
  import           Control.Applicative           ((<$>), (<*>))
  import           Control.Monad.State.Lazy      
  import           Text.ParserCombinators.Parsec hiding (State)
  import           Data.Char
  import           Data.Maybe
  import           Format
  import           Environment
  import           NamedLambda
  import           Lambda
  import           Libraries
  import           Ski
  import           Stlc.Types
  import           Stlc.Gentzen
  
  
  -- | Execute a block of code in a given environment
  executeWithEnv :: Environment -> String -> (String, Environment)
  executeWithEnv initEnv block = do
    let parsing = map (parse actionParser "" . preformat) . filter (/="") . lines $ block
    let actions = mapMaybe (\x -> case x of
                               Left _  -> Nothing
                               Right a -> Just a) parsing
    case runState (multipleAct actions) initEnv of
      (outputs, env) -> (unlines outputs, env)
  
  -- | Default environment plus standard libraries
  librariesEnv :: Environment
  librariesEnv = snd $ executeWithEnv defaultEnv stdlibraries
  
  -- | Preformats text before sending it to the interpreter
  preformat :: String -> String
  preformat = reverse . dropWhile (==' ') . reverse . dropWhile (==' ')
  
  -- | 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
                         | Quit             -- ^ Close the interpreter
                         | Load String      -- ^ Load the given file
  
  -- | 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
              | Diagram NamedLambda            -- ^ show the diagram of a lambda expression
              | SimpDiagram NamedLambda        -- ^ show the diagram of the simplified expression
              | Comment                        -- ^ comment
              | EmptyLine                      -- ^ empty line, it will be ignored
              | Error                          -- ^ error on the interpreter
              | Restart                        -- ^ restarts the environment
              | Help                           -- ^ shows help
              | Ask String                     -- ^ asks for the definition of a function
              | SetVerbose Bool                -- ^ changes verbosity
              | SetColor Bool                  -- ^ changes colors
              | SetSki Bool                    -- ^ changes ski output
              | SetTypes Bool                  -- ^ changes type configuration
              | SetStrategy String             -- ^ changes reduction strategy
              | SetTopo Bool
  
                
  -- | 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 (getStrategy env) (toBruijn (context env) le)))
    return [""]
  act (Execute le) = executeExpression le
  act (Diagram le) = drawDiagram False le
  act (SimpDiagram le) = drawDiagram True le
  act EmptyLine = return [""]
  act Error = return [errorUnknownCommand ++ "\n"]
  act Restart = put defaultEnv >> return [restartText ++ "\n"]
  act Help = return [helpText ++ "\n"]
  act (SetVerbose setting) = setOption setting changeVerbose "verbose: "
  act (SetColor setting) = setOption setting changeColor "color mode: "
  act (SetSki setting) = setOption setting changeSkioutput "ski mode: "
  act (SetTypes setting) = setOption setting changeTypes "types: "
  act (SetStrategy setting) = setOption' setting changeStrategy "strategy: "
  act (SetTopo setting) = setOption setting changeTopo "topology: "
  act (Ask func) = return $ askfor func
  
  
  -- | Asks for the name of a function.
  askfor :: String -> [String]
  askfor func = case stdquery func of
    Nothing -> ["Error: the function '" ++ func ++ "' is not defined on the standard library.\n"]
    Just f -> [description f ++ "\n", "Defined as: " ++ code f,"\n"]
      
  
  -- | Sets the given option on/off.
  setOption :: Bool ->
               (Environment -> Bool -> Environment) ->
               String ->
               State Environment [String]
  setOption setting change message = do
    modify (`change` setting)
    env <- get
    return [messageenv env ++ "\n"]
      where messageenv env =
              (if getColor env then formatFormula else "") ++ message ++
              (if setting then "on" else "off") ++ end
  
  -- | Sets the given string option.
  setOption' :: String ->
               (Environment -> String -> Environment) ->
               String ->
               State Environment [String]
  setOption' setting change message = do
    modify (`change` setting)
    env <- get
    return [messageenv env ++ "\n"]
      where messageenv env =
              (if getColor env then formatFormula else "") ++ message ++
              setting ++ end
  
  drawDiagram :: Bool -> NamedLambda -> State Environment [String]
  drawDiagram wantsimplification le = do
    env <- get
    let bruijn = toBruijn (context env) le
    let isopen = isOpenExp bruijn
    let simpbruijn = simplifyAll (getStrategy env) bruijn
    let maybediagram = gentzendiagram (if wantsimplification then simpbruijn else bruijn)
  
    return $
      if isopen then [errorUndefinedText ++ "\n"] else
        case maybediagram of
          Nothing -> [errorNonTypeableText ++ "\n"]
          Just diagram -> map (++ "\n") . lines $ showProofTree diagram
    
  -- | Executes a lambda expression. Given the context, returns the new
  -- context after the evaluation.
  executeExpression :: NamedLambda -> State Environment [String]
  executeExpression le = do
       env <- get
       let typed = getTypes env
       let bruijn = toBruijn (context env) le
       let illtyped = typed && isNothing (typeinference bruijn)
       let notypes = not typed && usestypecons bruijn
       let verbose = getVerbose env
       let completeexp = showCompleteExp env $ simplifyAll (getStrategy env) bruijn
       let isopen = isOpenExp bruijn
       let coloring = getColor env
       let decolorif = if coloring then id else decolor
       
       return $
         if isopen then [errorUndefinedText ++ "\n"] else
         if illtyped then [errorNonTypeableText ++ "\n"] else
         if notypes then [errorTypeConstructors ++ "\n"] else
         if not verbose then [completeexp ++ "\n"] else
           [unlines $
             [show le] ++
             [unlines $ map (decolorif . showReduction) $ simplifySteps (getStrategy env) bruijn] ++
             [completeexp]
           ]
    
  
  -- | 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 = 
    lambdaname ++ skiname ++ expName ++ typename ++ end
    where
      coloring = getColor environment
      ifvoid b x = if b then x else ""
      typesset = getTypes environment
      skiset = getSki environment
      lambdaname = show $ nameExp expr
      skiname = ifvoid skiset $ formatSubs2 ++ " ⇒ " ++ show (skiabs $ nameExp expr) ++ end
      inferredtype = case typeinference expr of
                       Just s -> if getTopo environment then show (Top s) else show s
                       Nothing -> "Type error!"
      typename = ifvoid typesset $ ifvoid coloring formatType ++ " :: " ++ inferredtype ++ end
      expName = case getExpressionName environment expr of
                  Just exname -> ifvoid coloring formatName ++ " ⇒ " ++ exname ++ end
                  Nothing -> ""
  
  
  -- Parsing of interpreter command line commands.
  -- | Parses an interpreter action.
  interpreteractionParser :: Parser InterpreterAction
  interpreteractionParser = choice
    [ try interpretParser
    , try quitParser
    , try loadParser
    ]
  
  -- | Parses a language action as an interpreter action.
  interpretParser :: Parser InterpreterAction
  interpretParser = Interpret <$> actionParser
  
  -- | Parses a language action.
  actionParser :: Parser Action
  actionParser = choice $ map try
    [ simpdiagramParser
    , diagramParser
    , bindParser
    , evalbindParser
    , executeParser
    , commentParser
    , helpParser
    , askParser
    , restartParser
    , verboseParser
    , colorParser
    , skiOutputParser
    , typesParser
    , strategyParser
    , topoParser
    ]
  
  
  -- | Parses a diagram request
  diagramParser :: Parser Action
  diagramParser = Diagram <$> (string "@ " >> lambdaexp)
  
  -- | Parses a simplfication and diagram request
  simpdiagramParser :: Parser Action
  simpdiagramParser = SimpDiagram <$> (string "@@ " >> lambdaexp)
  
  -- | Parses a binding between a variable an its representation.
  bindParser :: Parser Action
  bindParser = fmap Bind $ (,) <$>
    many1 alphaNum <*>
    (spaces >> choice [try (string "!="), try (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 a definition request to the interpreter.
  askParser :: Parser Action
  askParser = Ask <$> (string ":? " >> many1 alphaNum)
  
  -- | Parses comments.
  commentParser :: Parser Action
  commentParser = string "#" >> many anyChar >> return Comment
  
  strategyParser :: Parser Action
  strategyParser = SetStrategy <$> (
    string ":strategy" >> spaces >> (string "full" <|> try (string "cbn")  <|> string "cbv" )) 
  
  quitParser :: Parser InterpreterAction
  quitParser    = string ":quit" >> return Quit
  restartParser, helpParser :: Parser Action
  restartParser = string ":restart" >> return Restart
  helpParser    = string ":help" >> return Help
  
  -- | Parses a change in a setting
  settingParser :: (Bool -> Action) -> String -> Parser Action
  settingParser setSetting settingname = choice
    [ try settingonParser
    , try settingoffParser
    ]
    where
      settingonParser  = string (settingname ++ " on")  >> return (setSetting True)
      settingoffParser = string (settingname ++ " off") >> return (setSetting False)
  
  -- | Multiple setting parsers
  verboseParser, colorParser, skiOutputParser, typesParser, topoParser :: Parser Action
  verboseParser   = settingParser SetVerbose ":verbose"
  colorParser     = settingParser SetColor   ":color"
  skiOutputParser = settingParser SetSki     ":ski"
  typesParser     = settingParser SetTypes   ":types"
  topoParser      = settingParser SetTopo    ":topology"
  
  
  -- | Parses a "load-file" command.
  loadParser :: Parser InterpreterAction
  loadParser = Load <$> (string ":load" >> between spaces spaces (many1 (satisfy (not . isSpace))))
   