module Interpreter
(
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
executeWithEnv :: Environment -> String -> (String, Environment)
executeWithEnv initEnv code = do
let parsing = map (parse actionParser "" . preformat) . filter (/="") . lines $ code
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)
librariesEnv :: Environment
librariesEnv = snd $ executeWithEnv defaultEnv stdlibraries
preformat :: String -> String
preformat = reverse . dropWhile (==' ') . reverse . dropWhile (==' ')
data InterpreterAction = Interpret Action
| Quit
| Load String
data Action = Bind (String, NamedLambda)
| EvalBind (String, NamedLambda)
| Execute NamedLambda
| Diagram NamedLambda
| SimpDiagram NamedLambda
| Comment
| EmptyLine
| Error
| Restart
| Help
| SetVerbose Bool
| SetColor Bool
| SetSki Bool
| SetTypes Bool
| SetTopo Bool
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) = 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 (SetTopo setting) = setOption setting changeTopo "topology: "
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
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 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
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 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 bruijn] ++
[completeexp]
]
multipleAct :: [Action] -> State Environment [String]
multipleAct actions = concat <$> mapM act actions
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 -> ""
interpreteractionParser :: Parser InterpreterAction
interpreteractionParser = choice
[ try interpretParser
, try quitParser
, try loadParser
]
interpretParser :: Parser InterpreterAction
interpretParser = Interpret <$> actionParser
actionParser :: Parser Action
actionParser = choice $ map try
[ simpdiagramParser
, diagramParser
, bindParser
, evalbindParser
, executeParser
, commentParser
, helpParser
, restartParser
, verboseParser
, colorParser
, skiOutputParser
, typesParser
, topoParser
]
diagramParser :: Parser Action
diagramParser = Diagram <$> (string "@ " >> lambdaexp)
simpdiagramParser :: Parser Action
simpdiagramParser = SimpDiagram <$> (string "@@ " >> lambdaexp)
bindParser :: Parser Action
bindParser = fmap Bind $ (,) <$>
many1 alphaNum <*>
(spaces >> choice [try (string "!="), try (string ":=")] >> spaces >> lambdaexp)
evalbindParser :: Parser Action
evalbindParser = fmap EvalBind $ (,) <$> many1 alphaNum <*> (spaces >> string "=" >> spaces >> lambdaexp)
executeParser :: Parser Action
executeParser = Execute <$> lambdaexp
commentParser :: Parser Action
commentParser = string "#" >> many anyChar >> return Comment
quitParser :: Parser InterpreterAction
quitParser = string ":quit" >> return Quit
restartParser, helpParser :: Parser Action
restartParser = string ":restart" >> return Restart
helpParser = string ":help" >> return Help
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)
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"
loadParser :: Parser InterpreterAction
loadParser = Load <$> (string ":load" >> between spaces spaces (many1 (satisfy (not . isSpace))))