module Idris.REPLParser(parseCmd) where
import System.FilePath ((</>))
import System.Console.ANSI (Color(..))
import Idris.Colours
import Idris.AbsSyntax
import Idris.Core.TT
import qualified Idris.Parser as P
import Control.Applicative
import Control.Monad.State.Strict
import Text.Parser.Combinators
import Text.Parser.Char(anyChar)
import Text.Trifecta(Result, parseString)
import Text.Trifecta.Delta
import Debug.Trace
import Data.List
import Data.List.Split(splitOn)
import Data.Char(toLower)
import qualified Data.ByteString.UTF8 as UTF8
parseCmd :: IState -> String -> String -> Result (Either String Command)
parseCmd i inputname = P.runparser pCmd i inputname
pCmd :: P.IdrisParser (Either String Command)
pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit
<|> do c <- cmd ["h", "?", "help"]; noArgs c Help
<|> do c <- cmd ["w", "warranty"]; noArgs c Warranty
<|> do c <- cmd ["r", "reload"]; noArgs c Reload
<|> do c <- cmd ["exec", "execute"]; noArgs c Execute
<|> do c <- cmd ["proofs"]; noArgs c Proofs
<|> do c <- cmd ["u", "universes"]; noArgs c Universes
<|> do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers
<|> do c <- cmd ["m", "metavars"]; noArgs c Metavars
<|> do c <- cmd ["e", "edit"]; noArgs c Edit
<|> do c <- cmd ["d", "def"]; fnNameArg c Defn
<|> do c <- cmd ["total"]; fnNameArg c TotCheck
<|> do c <- cmd ["printdef"]; fnNameArg c PrintDef
<|> do c <- cmd ["transinfo"]; fnNameArg c TransformInfo
<|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls
<|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho
<|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo
<|> do c <- cmd ["miss", "missing"]; fnNameArg c Missing
<|> do c <- cmd ["t", "type"]; exprArg c Check
<|> do c <- cmd ["x"]; exprArg c ExecVal
<|> do c <- cmd ["patt"]; exprArg c Pattelab
<|> do c <- cmd ["spec"]; exprArg c Spec
<|> do c <- cmd ["hnf"]; exprArg c HNF
<|> do c <- cmd ["inline"]; exprArg c TestInline
<|> do c <- cmd ["rmproof"]; nameArg c RmProof
<|> do c <- cmd ["showproof"]; nameArg c ShowProof
<|> do c <- cmd ["p", "prove"]; nameArg c Prove
<|> do c <- cmd ["set"]; optArg c SetOpt
<|> do c <- cmd ["unset"]; optArg c UnsetOpt
<|> do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)
<|> do c <- cmd ["cd"]; strArg c ChangeDirectory
<|> do c <- cmd ["apropos"]; strArg c Apropos
<|> do c <- cmd ["mkdoc"]; strArg c MakeDoc
<|> do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt
<|> do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom
<|> do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom
<|> do c <- cmd ["am", "addmissing"]; proofArg c AddMissing
<|> do c <- cmd ["mw", "makewith"]; proofArg c MakeWith
<|> do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma
<|> do c <- cmd ["pp", "pprint"]; cmd_pprint c
<|> do c <- cmd ["doc"]; cmd_doc c
<|> do c <- cmd ["dynamic"]; cmd_dynamic c
<|> do c <- cmd ["consolewidth"]; cmd_consolewidth c
<|> do c <- cmd ["module"]; cmd_module c
<|> do c <- cmd ["c", "compile"]; cmd_compile c
<|> do c <- cmd ["a", "addproof"]; cmd_addproof c
<|> do c <- cmd ["log"]; cmd_log c
<|> do c <- cmd ["let"]; cmd_let c
<|> do c <- cmd ["unlet","undefine"]; cmd_unlet c
<|> do c <- cmd ["lto", "loadto"]; cmd_loadto c
<|> do c <- cmd ["color", "colour"]; cmd_colour c
<|> do c <- cmd ["s", "search"]; cmd_search c
<|> do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c
<|> do c <- cmd ["ref", "refine"]; cmd_refine c
<|> unrecognized
<|> nop
<|> eval
where nop = do P.whiteSpace; eof; return (Right NOP)
eval = exprArg "" Eval
unrecognized = do
P.lchar ':'
cmd <- many anyChar
let cmd' = takeWhile (/=' ') cmd
return (Left $ "Unrecognized command: " ++ cmd')
cmd :: [String] -> P.IdrisParser String
cmd xs = try $ do
P.lchar ':'
docmd sorted_xs
where docmd [] = fail "Could not parse command"
docmd (x:xs) = try (P.reserved x >> return x) <|> docmd xs
sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs
noArgs :: String -> Command -> P.IdrisParser (Either String Command)
noArgs name cmd = do
let emptyArgs = do
P.whiteSpace
eof
return (Right cmd)
let failure = return (Left $ ":" ++ name ++ " takes no arguments")
try emptyArgs <|> failure
exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)
exprArg name cmd = do
P.whiteSpace
let noArg = do
eof
return $ Left ("Usage is :" ++ name ++ " <expression>")
let properArg = do
t <- P.fullExpr defaultSyntax
return $ Right (cmd t)
try noArg <|> properArg
fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
fnNameArg name cmd = do
P.whiteSpace
let emptyArgs = do eof
return $ Left ("Usage is :" ++ name ++ " <functionname>")
oneArg = do n <- P.fnName
eof
return (Right (cmd n))
badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
try emptyArgs <|> try oneArg <|> badArg
nameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
nameArg name cmd = do
P.whiteSpace
let emptyArgs = do eof
return $ Left ("Usage is :" ++ name ++ " <functionname>")
oneArg = do n <- P.name
eof
return (Right (cmd n))
badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
try emptyArgs <|> try oneArg <|> badArg
strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)
strArg name cmd = do
n <- many anyChar
eof
return (Right (cmd n))
optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)
optArg name cmd = do
let emptyArgs = do
eof
return $ Left ("Usage is :" ++ name ++ " <option>")
let oneArg = do
P.whiteSpace
o <- pOption
P.whiteSpace
eof
return (Right (cmd o))
let failure = do
return $ Left "Unrecognized setting"
try emptyArgs <|> try oneArg <|> failure
where
pOption :: P.IdrisParser Opt
pOption = do discard (P.symbol "errorcontext"); return ErrContext
<|> do discard (P.symbol "showimplicits"); return ShowImpl
<|> do discard (P.symbol "originalerrors"); return ShowOrigErr
<|> do discard (P.symbol "autosolve"); return AutoSolve
<|> do discard (P.symbol "nobanner") ; return NoBanner
<|> do discard (P.symbol "warnreach"); return WarnReach
proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)
proofArg name cmd = do
P.whiteSpace
upd <- option False $ do
P.lchar '!'
return True
l <- P.natural
n <- P.name;
return (Right (cmd upd (fromInteger l) n))
cmd_doc :: String -> P.IdrisParser (Either String Command)
cmd_doc name = do
let constant = do
c <- P.constant
eof
return $ Right (DocStr (Right c))
let fnName = fnNameArg name (\n -> DocStr (Left n))
try constant <|> fnName
cmd_consolewidth :: String -> P.IdrisParser (Either String Command)
cmd_consolewidth name = do
w <- pConsoleWidth
return (Right (SetConsoleWidth w))
where
pConsoleWidth :: P.IdrisParser ConsoleWidth
pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
<|> do discard (P.symbol "infinite"); return InfinitelyWide
<|> do n <- fmap fromInteger P.natural; return (ColsWide n)
cmd_dynamic :: String -> P.IdrisParser (Either String Command)
cmd_dynamic name = do
let emptyArgs = noArgs name ListDynamic
let oneArg = do l <- many anyChar
return $ Right (DynamicLink l)
let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"
try emptyArgs <|> try oneArg <|> failure
cmd_pprint :: String -> P.IdrisParser (Either String Command)
cmd_pprint name = do
P.whiteSpace
fmt <- ppFormat
P.whiteSpace
n <- fmap fromInteger P.natural
P.whiteSpace
t <- P.fullExpr defaultSyntax
return (Right (PPrint fmt n t))
where
ppFormat :: P.IdrisParser OutputFmt
ppFormat = (discard (P.symbol "html") >> return HTMLOutput)
<|> (discard (P.symbol "latex") >> return LaTeXOutput)
cmd_module :: String -> P.IdrisParser (Either String Command)
cmd_module name = do
f <- P.identifier
eof;
return (Right (ModImport (toPath f)))
where
toPath n = foldl1' (</>) $ splitOn "." n
cmd_compile :: String -> P.IdrisParser (Either String Command)
cmd_compile name = do
let defaultCodegen = Via "c"
let codegenOption :: P.IdrisParser Codegen
codegenOption = do
let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
viaCodegen = do x <- P.identifier
return (Via (map toLower x))
bytecodeCodegen <|> viaCodegen
let hasOneArg = do
i <- get
f <- P.identifier
eof
return $ Right (Compile defaultCodegen f)
let hasTwoArgs = do
i <- get
codegen <- codegenOption
f <- P.identifier
eof
return $ Right (Compile codegen f)
let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"
try hasTwoArgs <|> try hasOneArg <|> failure
cmd_addproof :: String -> P.IdrisParser (Either String Command)
cmd_addproof name = do
n <- option Nothing $ do
x <- P.name;
return (Just x)
eof
return (Right (AddProof n))
cmd_log :: String -> P.IdrisParser (Either String Command)
cmd_log name = do
i <- P.natural
eof
return (Right (LogLvl (fromIntegral i)))
cmd_let :: String -> P.IdrisParser (Either String Command)
cmd_let name = do
defn <- concat <$> many (P.decl defaultSyntax)
return (Right (NewDefn defn))
cmd_unlet :: String -> P.IdrisParser (Either String Command)
cmd_unlet name = do
(Right . Undefine) `fmap` many P.name
cmd_loadto :: String -> P.IdrisParser (Either String Command)
cmd_loadto name = do
toline <- P.natural
f <- many anyChar;
return (Right (Load f (Just (fromInteger toline))))
cmd_colour :: String -> P.IdrisParser (Either String Command)
cmd_colour name = do
pSetColourCmd >>= return . Right
where
colours :: [(String, Maybe Color)]
colours = [ ("black", Just Black)
, ("red", Just Red)
, ("green", Just Green)
, ("yellow", Just Yellow)
, ("blue", Just Blue)
, ("magenta", Just Magenta)
, ("cyan", Just Cyan)
, ("white", Just White)
, ("default", Nothing)
]
pSetColourCmd :: P.IdrisParser Command
pSetColourCmd = (do c <- pColourType
let defaultColour = IdrisColour Nothing True False False False
opts <- sepBy pColourMod (P.whiteSpace)
let colour = foldr ($) defaultColour $ reverse opts
return $ SetColour c colour)
<|> try (P.symbol "on" >> return ColourOn)
<|> try (P.symbol "off" >> return ColourOff)
pColour :: P.IdrisParser (Maybe Color)
pColour = doColour colours
where doColour [] = fail "Unknown colour"
doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs
pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)
pColourMod = try (P.symbol "vivid" >> return doVivid)
<|> try (P.symbol "dull" >> return doDull)
<|> try (P.symbol "underline" >> return doUnderline)
<|> try (P.symbol "nounderline" >> return doNoUnderline)
<|> try (P.symbol "bold" >> return doBold)
<|> try (P.symbol "nobold" >> return doNoBold)
<|> try (P.symbol "italic" >> return doItalic)
<|> try (P.symbol "noitalic" >> return doNoItalic)
<|> try (pColour >>= return . doSetColour)
where doVivid i = i { vivid = True }
doDull i = i { vivid = False }
doUnderline i = i { underline = True }
doNoUnderline i = i { underline = False }
doBold i = i { bold = True }
doNoBold i = i { bold = False }
doItalic i = i { italic = True }
doNoItalic i = i { italic = False }
doSetColour c i = i { colour = c }
colourTypes :: [(String, ColourType)]
colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
enumFromTo minBound maxBound
pColourType :: P.IdrisParser ColourType
pColourType = doColourType colourTypes
where doColourType [] = fail $ "Unknown colour category. Options: " ++
(concat . intersperse ", " . map fst) colourTypes
doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts
cmd_search :: String -> P.IdrisParser (Either String Command)
cmd_search name = do
P.whiteSpace;
t <- P.typeExpr (defaultSyntax { implicitAllowed = True })
return (Right (Search t))
cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
cmd_proofsearch name = do
P.whiteSpace
upd <- option False (do P.lchar '!'; return True)
l <- P.natural; n <- P.name;
hints <- many P.fnName
return (Right (DoProofSearch upd True (fromInteger l) n hints))
cmd_refine :: String -> P.IdrisParser (Either String Command)
cmd_refine name = do
P.whiteSpace
upd <- option False (do P.lchar '!'; return True)
l <- P.natural; n <- P.name;
hint <- P.fnName
return (Right (DoProofSearch upd False (fromInteger l) n [hint]))