module Idris.REPLParser (parseCmd, help, allHelp) where import System.FilePath (()) import System.Console.ANSI (Color(..)) import Idris.Colours import Idris.AbsSyntax import Idris.Core.TT import Idris.Help import qualified Idris.Parser as P import Control.Applicative import Control.Monad.State.Strict import Text.Parser.Combinators import Text.Parser.Char(anyChar,oneOf) import Text.Trifecta(Result, parseString) import Text.Trifecta.Delta import Debug.Trace import Data.List import Data.List.Split(splitOn) import Data.Char(isSpace, toLower) import qualified Data.ByteString.UTF8 as UTF8 parseCmd :: IState -> String -> String -> Result (Either String Command) parseCmd i inputname = P.runparser pCmd i inputname . trim where trim = f . f where f = reverse . dropWhile isSpace type CommandTable = [ ( [String], CmdArg, String , String -> P.IdrisParser (Either String Command) ) ] help :: [([String], CmdArg, String)] help = ([""], NoArg, "Evaluate an expression") : [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ] allHelp :: [([String], CmdArg, String)] allHelp = [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ] parserCommandsForHelp :: CommandTable parserCommandsForHelp = [ exprArgCmd ["t", "type"] Check "Check the type of an expression" , exprArgCmd ["core"] Core "View the core language representation of a term" , nameArgCmd ["miss", "missing"] Missing "Show missing clauses" , (["doc"], NameArg, "Show internal documentation", cmd_doc) , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies" , genArg "namespace" (many anyChar) MakeDoc) , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation" , cmd_apropos) , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg , " Search for values by type", cmd_search) , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name" , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name" , namespaceArgCmd ["browse"] Browse "List the contents of some namespace" , nameArgCmd ["total"] TotCheck "Check the totality of a name" , noArgCmd ["r", "reload"] Reload "Reload current file" , (["l", "load"], FileArg, "Load a new file" , strArg (\f -> Load f Nothing)) , (["cd"], FileArg, "Change working directory" , strArg ChangeDirectory) , (["module"], ModuleArg, "Import an extra module", moduleArg ModImport) -- NOTE: dragons , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL" , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables or holes)" , (["p", "prove"], MetaVarArg, "Prove a metavariable" , nameArg (Prove False)) , (["elab"], MetaVarArg, "Build a metavariable using the elaboration shell" , nameArg (Prove True)) , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof) , (["rmproof"], NameArg, "Remove proof from proof stack" , nameArg RmProof) , (["showproof"], NameArg, "Show proof" , nameArg ShowProof) , noArgCmd ["proofs"] Proofs "Show available proofs" , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter" , (["c", "compile"], FileArg, "Compile to an executable [codegen] ", cmd_compile) , (["exec", "execute"], OptionalArg ExprArg, "Compile to an executable and run", cmd_execute) , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic) , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic) , noArgCmd ["?", "h", "help"] Help "Display this help text" , optArgCmd ["set"] SetOpt "Set an option (errorcontext, showimplicits)" , optArgCmd ["unset"] UnsetOpt "Unset an option" , (["color", "colour"], ColourArg , "Turn REPL colours on or off; set a specific colour" , cmd_colour) , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth) , (["printerdepth"], OptionalArg NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", cmd_printdepth) , noArgCmd ["q", "quit"] Quit "Exit the Idris system" , noArgCmd ["w", "warranty"] Warranty "Displays warranty information" , (["let"], ManyArgs DeclArg , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration" , cmd_let) , (["unlet", "undefine"], ManyArgs NameArg , "Remove the listed repl definitions, or all repl definitions if no names given" , cmd_unlet) , nameArgCmd ["printdef"] PrintDef "Show the definition of a function" , (["pp", "pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg)) , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width." , cmd_pprint) ] parserCommands = [ noArgCmd ["u", "universes"] Universes "Display universe constraints" , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers" , nameArgCmd ["d", "def"] Defn "Display a name's internal definitions" , nameArgCmd ["transinfo"] TransformInfo "Show relevant transformation rules for a name" , nameArgCmd ["di", "dbginfo"] DebugInfo "Show debugging information for a name" , exprArgCmd ["patt"] Pattelab "(Debugging) Elaborate pattern expression" , exprArgCmd ["spec"] Spec "?" , exprArgCmd ["whnf"] WHNF "(Debugging) Show weak head normal form of an expression" , exprArgCmd ["inline"] TestInline "?" , proofArgCmd ["cs", "casesplit"] CaseSplitAt ":cs splits the pattern variable on the line" , proofArgCmd ["apc", "addproofclause"] AddProofClauseFrom ":apc adds a pattern-matching proof clause to name on line" , proofArgCmd ["ac", "addclause"] AddClauseFrom ":ac adds a clause for the definition of the name on the line" , proofArgCmd ["am", "addmissing"] AddMissing ":am adds all missing pattern matches for the name on the line" , proofArgCmd ["mw", "makewith"] MakeWith ":mw adds a with clause for the definition of the name on the line" , proofArgCmd ["mc", "makecase"] MakeCase ":mc adds a case block for the definition of the metavariable on the line" , proofArgCmd ["ml", "makelemma"] MakeLemma "?" , (["log"], NumberArg, "Set logging verbosity level", cmd_log) , (["lto", "loadto"], SeqArgs NumberArg FileArg , "Load file up to line number", cmd_loadto) , (["ps", "proofsearch"], NoArg , ":ps does proof search for name on line, with names as hints" , cmd_proofsearch) , (["ref", "refine"], NoArg , ":ref attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable" , cmd_refine) , (["debugunify"], SeqArgs ExprArg ExprArg , "(Debugging) Try to unify two expressions", const $ do l <- P.simpleExpr defaultSyntax r <- P.simpleExpr defaultSyntax eof return (Right (DebugUnify l r)) ) ] noArgCmd names command doc = (names, NoArg, doc, noArgs command) nameArgCmd names command doc = (names, NameArg, doc, fnNameArg command) namespaceArgCmd names command doc = (names, NamespaceArg, doc, namespaceArg command) exprArgCmd names command doc = (names, ExprArg, doc, exprArg command) metavarArgCmd names command doc = (names, MetaVarArg, doc, fnNameArg command) optArgCmd names command doc = (names, OptionArg, doc, optArg command) proofArgCmd names command doc = (names, NoArg, doc, proofArg command) pCmd :: P.IdrisParser (Either String Command) pCmd = choice [ do c <- cmd names; parser c | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ] <|> unrecognized <|> nop <|> eval where nop = do 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 :: Command -> String -> P.IdrisParser (Either String Command) noArgs cmd name = do let emptyArgs = do eof return (Right cmd) let failure = return (Left $ ":" ++ name ++ " takes no arguments") emptyArgs <|> failure exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command) exprArg cmd name = do let noArg = do eof return $ Left ("Usage is :" ++ name ++ " ") let properArg = do t <- P.fullExpr defaultSyntax return $ Right (cmd t) try noArg <|> properArg genArg :: String -> P.IdrisParser a -> (a -> Command) -> String -> P.IdrisParser (Either String Command) genArg argName argParser cmd name = do let emptyArgs = do eof; failure oneArg = do arg <- argParser eof return (Right (cmd arg)) try emptyArgs <|> oneArg <|> failure where failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">") nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command) nameArg = genArg "name" $ fst <$> P.name fnNameArg = genArg "functionname" $ fst <$> P.fnName strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command) strArg = genArg "string" (many anyChar) moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command) moduleArg = genArg "module" (fmap (toPath . fst) P.identifier) where toPath n = foldl1' () $ splitOn "." n namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command) namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier) where toNS = splitOn "." optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command) optArg cmd name = do let emptyArgs = do eof return $ Left ("Usage is :" ++ name ++ "