{-# LANGUAGE FlexibleContexts #-}
module Idris.REPL.Parser (
parseCmd
, help
, allHelp
, setOptions
) where
import Idris.AbsSyntax
import Idris.Colours
import Idris.Core.TT
import Idris.Help
import Idris.Imports
import Idris.Options
import qualified Idris.Parser as IP
import qualified Idris.Parser.Expr as IP
import qualified Idris.Parser.Helpers as IP
import qualified Idris.Parser.Ops as IP
import Idris.REPL.Commands
import Control.Applicative
import Control.Monad.State.Strict
import Data.Char (isSpace, toLower)
import Data.List
import Data.List.Split (splitOn)
import System.Console.ANSI (Color(..))
import System.FilePath ((</>))
import qualified Text.Megaparsec as P
parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)
parseCmd :: IState
-> String -> String -> Either ParseError (Either String Command)
parseCmd i :: IState
i inputname :: String
inputname = Parser IState (Either String Command)
-> IState
-> String
-> String
-> Either ParseError (Either String Command)
forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
IP.runparser Parser IState (Either String Command)
pCmd IState
i String
inputname (String -> Either ParseError (Either String Command))
-> (String -> String)
-> String
-> Either ParseError (Either String Command)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
trim
where trim :: String -> String
trim = String -> String
f (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
f
where f :: String -> String
f = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
type CommandTable = [ ( [String], CmdArg, String
, String -> IP.IdrisParser (Either String Command) ) ]
setOptions :: [(String, Opt)]
setOptions :: [(String, Opt)]
setOptions = [("errorcontext", Opt
ErrContext),
("showimplicits", Opt
ShowImpl),
("originalerrors", Opt
ShowOrigErr),
("autosolve", Opt
AutoSolve),
("nobanner", Opt
NoBanner),
("warnreach", Opt
WarnReach),
("evaltypes", Opt
EvalTypes),
("desugarnats", Opt
DesugarNats)]
help :: [([String], CmdArg, String)]
help :: [([String], CmdArg, String)]
help = (["<expr>"], CmdArg
NoArg, "Evaluate an expression") ([String], CmdArg, String)
-> [([String], CmdArg, String)] -> [([String], CmdArg, String)]
forall a. a -> [a] -> [a]
:
[ ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (':' Char -> String -> String
forall a. a -> [a] -> [a]
:) [String]
names, CmdArg
args, String
text) | (names :: [String]
names, args :: CmdArg
args, text :: String
text, _) <- CommandTable
parserCommandsForHelp ]
allHelp :: [([String], CmdArg, String)]
allHelp :: [([String], CmdArg, String)]
allHelp = [ ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (':' Char -> String -> String
forall a. a -> [a] -> [a]
:) [String]
names, CmdArg
args, String
text)
| (names :: [String]
names, args :: CmdArg
args, text :: String
text, _) <- CommandTable
parserCommandsForHelp CommandTable -> CommandTable -> CommandTable
forall a. [a] -> [a] -> [a]
++ CommandTable
parserCommands ]
parserCommandsForHelp :: CommandTable
parserCommandsForHelp :: CommandTable
parserCommandsForHelp =
[ [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["t", "type"] PTerm -> Command
Check "Check the type of an expression"
, [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["core"] PTerm -> Command
Core "View the core language representation of a term"
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["miss", "missing"] Name -> Command
Missing "Show missing clauses"
, (["doc"], CmdArg
NameArg, "Show internal documentation", String -> Parser IState (Either String Command)
cmd_doc)
, (["mkdoc"], CmdArg
NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"
, String
-> IdrisParser String
-> (String -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg "namespace" (StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle) String -> Command
MakeDoc)
, (["apropos"], CmdArg -> CmdArg -> CmdArg
SeqArgs (CmdArg -> CmdArg
OptionalArg CmdArg
PkgArgs) CmdArg
NameArg, " Search names, types, and documentation"
, String -> Parser IState (Either String Command)
cmd_apropos)
, (["s", "search"], CmdArg -> CmdArg -> CmdArg
SeqArgs (CmdArg -> CmdArg
OptionalArg CmdArg
PkgArgs) CmdArg
ExprArg
, " Search for values by type", String -> Parser IState (Either String Command)
cmd_search)
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["wc", "whocalls"] Name -> Command
WhoCalls "List the callers of some name"
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["cw", "callswho"] Name -> Command
CallsWho "List the callees of some name"
, [String]
-> ([String] -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> ([String] -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
namespaceArgCmd ["browse"] [String] -> Command
Browse "List the contents of some namespace"
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["total"] Name -> Command
TotCheck "Check the totality of a name"
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["r", "reload"] Command
Reload "Reload current file"
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["w", "watch"] Command
Watch "Watch the current file for changes"
, (["l", "load"], CmdArg
FileArg, "Load a new file"
, (String -> Command)
-> String -> Parser IState (Either String Command)
strArg (\f :: String
f -> String -> Maybe Int -> Command
Load String
f Maybe Int
forall a. Maybe a
Nothing))
, (["!"], CmdArg
ShellCommandArg, "Run a shell command", (String -> Command)
-> String -> Parser IState (Either String Command)
strArg String -> Command
RunShellCommand)
, (["cd"], CmdArg
FileArg, "Change working directory"
, (String -> Command)
-> String -> Parser IState (Either String Command)
strArg String -> Command
ChangeDirectory)
, (["module"], CmdArg
ModuleArg, "Import an extra module", (String -> Command)
-> String -> Parser IState (Either String Command)
moduleArg String -> Command
ModImport)
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["e", "edit"] Command
Edit "Edit current file using $EDITOR or $VISUAL"
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["m", "metavars"] Command
Metavars "Show remaining proof obligations (metavariables or holes)"
, (["p", "prove"], CmdArg
MetaVarArg, "Prove a metavariable"
, (Name -> Command)
-> String -> Parser IState (Either String Command)
nameArg (Bool -> Name -> Command
Prove Bool
False))
, (["elab"], CmdArg
MetaVarArg, "Build a metavariable using the elaboration shell"
, (Name -> Command)
-> String -> Parser IState (Either String Command)
nameArg (Bool -> Name -> Command
Prove Bool
True))
, (["a", "addproof"], CmdArg
NameArg, "Add proof to source file", String -> Parser IState (Either String Command)
cmd_addproof)
, (["rmproof"], CmdArg
NameArg, "Remove proof from proof stack"
, (Name -> Command)
-> String -> Parser IState (Either String Command)
nameArg Name -> Command
RmProof)
, (["showproof"], CmdArg
NameArg, "Show proof"
, (Name -> Command)
-> String -> Parser IState (Either String Command)
nameArg Name -> Command
ShowProof)
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["proofs"] Command
Proofs "Show available proofs"
, [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["x"] PTerm -> Command
ExecVal "Execute IO actions resulting from an expression using the interpreter"
, (["c", "compile"], CmdArg
FileArg, "Compile to an executable [codegen] <filename>", String -> Parser IState (Either String Command)
cmd_compile)
, (["exec", "execute"], CmdArg -> CmdArg
OptionalArg CmdArg
ExprArg, "Compile to an executable and run", String -> Parser IState (Either String Command)
cmd_execute)
, (["dynamic"], CmdArg
FileArg, "Dynamically load a C library (similar to %dynamic)", String -> Parser IState (Either String Command)
cmd_dynamic)
, (["dynamic"], CmdArg
NoArg, "List dynamically loaded C libraries", String -> Parser IState (Either String Command)
cmd_dynamic)
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["?", "h", "help"] Command
Help "Display this help text"
, [String]
-> (Opt -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Opt -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
optArgCmd ["set"] Opt -> Command
SetOpt (String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command)))
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a b. (a -> b) -> a -> b
$ "Set an option (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
optionsList String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
, [String]
-> (Opt -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Opt -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
optArgCmd ["unset"] Opt -> Command
UnsetOpt "Unset an option"
, (["color", "colour"], CmdArg
ColourArg
, "Turn REPL colours on or off; set a specific colour"
, String -> Parser IState (Either String Command)
cmd_colour)
, (["consolewidth"], CmdArg
ConsoleWidthArg, "Set the width of the console", String -> Parser IState (Either String Command)
cmd_consolewidth)
, (["printerdepth"], CmdArg -> CmdArg
OptionalArg CmdArg
NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", String -> Parser IState (Either String Command)
cmd_printdepth)
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["q", "quit"] Command
Quit "Exit the Idris system"
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["version"] Command
ShowVersion "Display the Idris version"
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["warranty"] Command
Warranty "Displays warranty information"
, (["let"], CmdArg -> CmdArg
ManyArgs CmdArg
DeclArg
, "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"
, String -> Parser IState (Either String Command)
cmd_let)
, (["unlet", "undefine"], CmdArg -> CmdArg
ManyArgs CmdArg
NameArg
, "Remove the listed repl definitions, or all repl definitions if no names given"
, String -> Parser IState (Either String Command)
cmd_unlet)
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["printdef"] Name -> Command
PrintDef "Show the definition of a function"
, (["pp", "pprint"], (CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
OptionArg (CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
NumberArg CmdArg
NameArg))
, "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."
, String -> Parser IState (Either String Command)
cmd_pprint)
, (["verbosity"], CmdArg
NumberArg, "Set verbosity level", String -> Parser IState (Either String Command)
cmd_verb)
]
where optionsList :: String
optionsList = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, Opt) -> String) -> [(String, Opt)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Opt) -> String
forall a b. (a, b) -> a
fst [(String, Opt)]
setOptions
parserCommands :: CommandTable
parserCommands :: CommandTable
parserCommands =
[ [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["u", "universes"] Command
Universes "Display universe constraints"
, [String]
-> Command
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd ["errorhandlers"] Command
ListErrorHandlers "List registered error handlers"
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["d", "def"] Name -> Command
Defn "Display a name's internal definitions"
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["transinfo"] Name -> Command
TransformInfo "Show relevant transformation rules for a name"
, [String]
-> (Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd ["di", "dbginfo"] Name -> Command
DebugInfo "Show debugging information for a name"
, [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["patt"] PTerm -> Command
Pattelab "(Debugging) Elaborate pattern expression"
, [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["spec"] PTerm -> Command
Spec "?"
, [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["whnf"] PTerm -> Command
WHNF "(Debugging) Show weak head normal form of an expression"
, [String]
-> (PTerm -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd ["inline"] PTerm -> Command
TestInline "?"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["cs", "casesplit"] Bool -> Int -> Name -> Command
CaseSplitAt
":cs <line> <name> splits the pattern variable on the line"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["apc", "addproofclause"] Bool -> Int -> Name -> Command
AddProofClauseFrom
":apc <line> <name> adds a pattern-matching proof clause to name on line"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["ac", "addclause"] Bool -> Int -> Name -> Command
AddClauseFrom
":ac <line> <name> adds a clause for the definition of the name on the line"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["am", "addmissing"] Bool -> Int -> Name -> Command
AddMissing
":am <line> <name> adds all missing pattern matches for the name on the line"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["mw", "makewith"] Bool -> Int -> Name -> Command
MakeWith
":mw <line> <name> adds a with clause for the definition of the name on the line"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["mc", "makecase"] Bool -> Int -> Name -> Command
MakeCase
":mc <line> <name> adds a case block for the definition of the metavariable on the line"
, [String]
-> (Bool -> Int -> Name -> Command)
-> String
-> ([String], CmdArg, String,
String -> Parser IState (Either String Command))
forall a c.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd ["ml", "makelemma"] Bool -> Int -> Name -> Command
MakeLemma "?"
, (["log"], CmdArg
NumberArg, "Set logging level", String -> Parser IState (Either String Command)
cmd_log)
, ( ["logcats"]
, CmdArg -> CmdArg
ManyArgs CmdArg
NameArg
, "Set logging categories"
, String -> Parser IState (Either String Command)
cmd_cats)
, (["lto", "loadto"], CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
NumberArg CmdArg
FileArg
, "Load file up to line number", String -> Parser IState (Either String Command)
cmd_loadto)
, (["ps", "proofsearch"], CmdArg
NoArg
, ":ps <line> <name> <names> does proof search for name on line, with names as hints"
, String -> Parser IState (Either String Command)
cmd_proofsearch)
, (["ref", "refine"], CmdArg
NoArg
, ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable"
, String -> Parser IState (Either String Command)
cmd_refine)
, (["debugunify"], CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
ExprArg CmdArg
ExprArg
, "(Debugging) Try to unify two expressions", Parser IState (Either String Command)
-> String -> Parser IState (Either String Command)
forall a b. a -> b -> a
const (Parser IState (Either String Command)
-> String -> Parser IState (Either String Command))
-> Parser IState (Either String Command)
-> String
-> Parser IState (Either String Command)
forall a b. (a -> b) -> a -> b
$ do
PTerm
l <- SyntaxInfo -> IdrisParser PTerm
IP.simpleExpr SyntaxInfo
defaultSyntax
PTerm
r <- SyntaxInfo -> IdrisParser PTerm
IP.simpleExpr SyntaxInfo
defaultSyntax
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (PTerm -> PTerm -> Command
DebugUnify PTerm
l PTerm
r))
)
]
noArgCmd :: a
-> Command
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
noArgCmd names :: a
names command :: Command
command doc :: c
doc =
(a
names, CmdArg
NoArg, c
doc, Command -> String -> Parser IState (Either String Command)
noArgs Command
command)
nameArgCmd :: a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
nameArgCmd names :: a
names command :: Name -> Command
command doc :: c
doc =
(a
names, CmdArg
NameArg, c
doc, (Name -> Command)
-> String -> Parser IState (Either String Command)
fnNameArg Name -> Command
command)
namespaceArgCmd :: a
-> ([String] -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
namespaceArgCmd names :: a
names command :: [String] -> Command
command doc :: c
doc =
(a
names, CmdArg
NamespaceArg, c
doc, ([String] -> Command)
-> String -> Parser IState (Either String Command)
namespaceArg [String] -> Command
command)
exprArgCmd :: a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
exprArgCmd names :: a
names command :: PTerm -> Command
command doc :: c
doc =
(a
names, CmdArg
ExprArg, c
doc, (PTerm -> Command)
-> String -> Parser IState (Either String Command)
exprArg PTerm -> Command
command)
optArgCmd :: a
-> (Opt -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
optArgCmd names :: a
names command :: Opt -> Command
command doc :: c
doc =
(a
names, CmdArg
OptionArg, c
doc, (Opt -> Command) -> String -> Parser IState (Either String Command)
optArg Opt -> Command
command)
proofArgCmd :: a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> Parser IState (Either String Command))
proofArgCmd names :: a
names command :: Bool -> Int -> Name -> Command
command doc :: c
doc =
(a
names, CmdArg
NoArg, c
doc, (Bool -> Int -> Name -> Command)
-> String -> Parser IState (Either String Command)
proofArg Bool -> Int -> Name -> Command
command)
pCmd :: IP.IdrisParser (Either String Command)
pCmd :: Parser IState (Either String Command)
pCmd = [Parser IState (Either String Command)]
-> Parser IState (Either String Command)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ do String
c <- [String] -> IdrisParser String
cmd [String]
names; String -> Parser IState (Either String Command)
parser String
c
| (names :: [String]
names, _, _, parser :: String -> Parser IState (Either String Command)
parser) <- CommandTable
parserCommandsForHelp CommandTable -> CommandTable -> CommandTable
forall a. [a] -> [a] -> [a]
++ CommandTable
parserCommands ]
Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
unrecognized
Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
nop
Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
eval
where nop :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
nop = do StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof; Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either a Command
forall a b. b -> Either a b
Right Command
NOP)
unrecognized :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
unrecognized = do
Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar ':'
String
cmd <- StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
let cmd' :: String
cmd' = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=' ') String
cmd
Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ "Unrecognized command: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmd')
cmd :: [String] -> IP.IdrisParser String
cmd :: [String] -> IdrisParser String
cmd xs :: [String]
xs = IdrisParser String -> IdrisParser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser String -> IdrisParser String)
-> IdrisParser String -> IdrisParser String
forall a b. (a -> b) -> a -> b
$ do
Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar ':'
[String] -> IdrisParser String
forall (m :: * -> *).
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[String] -> m String
docmd [String]
sorted_xs
where docmd :: [String] -> m String
docmd [] = String -> m String
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Could not parse command"
docmd (x :: String
x:xs :: [String]
xs) = m String -> m String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> m ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.reserved String
x m () -> m String -> m String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
x) m String -> m String -> m String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [String] -> m String
docmd [String]
xs
sorted_xs :: [String]
sorted_xs = (String -> String -> Ordering) -> [String] -> [String]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\x :: String
x y :: String
y -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y) (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x)) [String]
xs
noArgs :: Command -> String -> IP.IdrisParser (Either String Command)
noArgs :: Command -> String -> Parser IState (Either String Command)
noArgs cmd :: Command
cmd name :: String
name = do
let emptyArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
emptyArgs = do
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either a Command
forall a b. b -> Either a b
Right Command
cmd)
let failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ ":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " takes no arguments")
Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
emptyArgs Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure
eval :: IP.IdrisParser (Either String Command)
eval :: Parser IState (Either String Command)
eval = do
PTerm
t <- SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String Command -> Parser IState (Either String Command))
-> Either String Command -> Parser IState (Either String Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either String Command
forall a b. b -> Either a b
Right (PTerm -> Command
Eval PTerm
t)
exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)
exprArg :: (PTerm -> Command)
-> String -> Parser IState (Either String Command)
exprArg cmd :: PTerm -> Command
cmd name :: String
name = do
let noArg :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
noArg = do
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b))
-> Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall a b. (a -> b) -> a -> b
$ String -> Either String b
forall a b. a -> Either a b
Left ("Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " <expression>")
let justOperator :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
justOperator = do
(op :: String
op, fc :: FC
fc) <- IdrisParser String
-> StateT IState (WriterT FC (Parsec Void String)) (String, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
IP.withExtent IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.symbolicOperator
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (Command -> Either a Command) -> Command -> Either a Command
forall a b. (a -> b) -> a -> b
$ PTerm -> Command
cmd (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
op))
let properArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
properArg = do
PTerm
t <- SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (PTerm -> Command
cmd PTerm
t)
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
noArg Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
justOperator Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
properArg
genArg :: String -> IP.IdrisParser a -> (a -> Command)
-> String -> IP.IdrisParser (Either String Command)
genArg :: String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg argName :: String
argName argParser :: IdrisParser a
argParser cmd :: a -> Command
cmd name :: String
name = do
let emptyArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs = do StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof; StateT IState (WriterT FC (Parsec Void String)) (Either String b)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure
oneArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg = do a
arg <- IdrisParser a
argParser
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either a Command
forall a b. b -> Either a b
Right (a -> Command
cmd a
arg))
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure
where
failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b))
-> Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall a b. (a -> b) -> a -> b
$ String -> Either String b
forall a b. a -> Either a b
Left ("Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
argName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ">")
nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)
nameArg :: (Name -> Command)
-> String -> Parser IState (Either String Command)
nameArg = String
-> IdrisParser Name
-> (Name -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg "name" IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
fnNameArg :: (Name -> Command)
-> String -> Parser IState (Either String Command)
fnNameArg = String
-> IdrisParser Name
-> (Name -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg "functionname" IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.fnName
strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)
strArg :: (String -> Command)
-> String -> Parser IState (Either String Command)
strArg = String
-> IdrisParser String
-> (String -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg "string" (StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle)
moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)
moduleArg :: (String -> Command)
-> String -> Parser IState (Either String Command)
moduleArg = String
-> IdrisParser String
-> (String -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg "module" ((String -> String) -> IdrisParser String -> IdrisParser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
toPath IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.identifier)
where
toPath :: String -> String
toPath n :: String
n = (String -> String -> String) -> [String] -> String
forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn "." String
n
namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)
namespaceArg :: ([String] -> Command)
-> String -> Parser IState (Either String Command)
namespaceArg = String
-> IdrisParser [String]
-> ([String] -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (Either String Command)
genArg "namespace" ((String -> [String]) -> IdrisParser String -> IdrisParser [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [String]
toNS IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.identifier)
where
toNS :: String -> [String]
toNS = String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn "."
optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)
optArg :: (Opt -> Command) -> String -> Parser IState (Either String Command)
optArg cmd :: Opt -> Command
cmd name :: String
name = do
let emptyArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs = do
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b))
-> Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall a b. (a -> b) -> a -> b
$ String -> Either String b
forall a b. a -> Either a b
Left ("Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " <option>")
let oneArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg = do
Opt
o <- IdrisParser Opt
pOption
StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either a Command
forall a b. b -> Either a b
Right (Opt -> Command
cmd Opt
o))
let failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b))
-> Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall a b. (a -> b) -> a -> b
$ String -> Either String b
forall a b. a -> Either a b
Left "Unrecognized setting"
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure
where
pOption :: IP.IdrisParser Opt
pOption :: IdrisParser Opt
pOption = (IdrisParser Opt -> IdrisParser Opt -> IdrisParser Opt)
-> IdrisParser Opt -> [IdrisParser Opt] -> IdrisParser Opt
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl IdrisParser Opt -> IdrisParser Opt -> IdrisParser Opt
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) IdrisParser Opt
forall (f :: * -> *) a. Alternative f => f a
empty ([IdrisParser Opt] -> IdrisParser Opt)
-> [IdrisParser Opt] -> IdrisParser Opt
forall a b. (a -> b) -> a -> b
$ ((String, Opt) -> IdrisParser Opt)
-> [(String, Opt)] -> [IdrisParser Opt]
forall a b. (a -> b) -> [a] -> [b]
map (\(a :: String
a, b :: Opt
b) -> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
discard (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
a); Opt -> IdrisParser Opt
forall (m :: * -> *) a. Monad m => a -> m a
return Opt
b) [(String, Opt)]
setOptions
proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)
proofArg :: (Bool -> Int -> Name -> Command)
-> String -> Parser IState (Either String Command)
proofArg cmd :: Bool -> Int -> Name -> Command
cmd name :: String
name = do
Bool
upd <- Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False (StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool)
-> StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a b. (a -> b) -> a -> b
$ do
Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar '!'
Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Integer
l <- StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural
Name
n <- IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Bool -> Int -> Name -> Command
cmd Bool
upd (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
l) Name
n))
cmd_doc :: String -> IP.IdrisParser (Either String Command)
cmd_doc :: String -> Parser IState (Either String Command)
cmd_doc name :: String
name = do
let constant :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
constant = do
Const
c <- StateT IState (WriterT FC (Parsec Void String)) Const
forall (m :: * -> *). Parsing m => m Const
IP.constant
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (Either Name Const -> HowMuchDocs -> Command
DocStr (Const -> Either Name Const
forall a b. b -> Either a b
Right Const
c) HowMuchDocs
FullDocs)
let pType :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
pType = do
String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.reserved "Type"
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (Either Name Const -> HowMuchDocs -> Command
DocStr (Name -> Either Name Const
forall a b. a -> Either a b
Left (Name -> Either Name Const) -> Name -> Either Name Const
forall a b. (a -> b) -> a -> b
$ String -> Name
sUN "Type") HowMuchDocs
FullDocs)
let fnName :: Parser IState (Either String Command)
fnName = (Name -> Command)
-> String -> Parser IState (Either String Command)
fnNameArg (\n :: Name
n -> Either Name Const -> HowMuchDocs -> Command
DocStr (Name -> Either Name Const
forall a b. a -> Either a b
Left Name
n) HowMuchDocs
FullDocs) String
name
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
constant Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
pType Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
fnName
cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)
cmd_consolewidth :: String -> Parser IState (Either String Command)
cmd_consolewidth name :: String
name = do
ConsoleWidth
w <- IdrisParser ConsoleWidth
pConsoleWidth
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (ConsoleWidth -> Command
SetConsoleWidth ConsoleWidth
w))
where
pConsoleWidth :: IP.IdrisParser ConsoleWidth
pConsoleWidth :: IdrisParser ConsoleWidth
pConsoleWidth = do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
discard (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "auto"); ConsoleWidth -> IdrisParser ConsoleWidth
forall (m :: * -> *) a. Monad m => a -> m a
return ConsoleWidth
AutomaticWidth
IdrisParser ConsoleWidth
-> IdrisParser ConsoleWidth -> IdrisParser ConsoleWidth
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
discard (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "infinite"); ConsoleWidth -> IdrisParser ConsoleWidth
forall (m :: * -> *) a. Monad m => a -> m a
return ConsoleWidth
InfinitelyWide
IdrisParser ConsoleWidth
-> IdrisParser ConsoleWidth -> IdrisParser ConsoleWidth
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Int
n <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural
ConsoleWidth -> IdrisParser ConsoleWidth
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ConsoleWidth
ColsWide Int
n)
cmd_printdepth :: String -> IP.IdrisParser (Either String Command)
cmd_printdepth :: String -> Parser IState (Either String Command)
cmd_printdepth _ = do Maybe Int
d <- StateT IState (WriterT FC (Parsec Void String)) Int
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Int)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural)
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Command -> Either String Command)
-> Command -> Either String Command
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Command
SetPrinterDepth Maybe Int
d)
cmd_execute :: String -> IP.IdrisParser (Either String Command)
cmd_execute :: String -> Parser IState (Either String Command)
cmd_execute name :: String
name = do
PTerm
tm <- PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option PTerm
maintm (SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax)
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (PTerm -> Command
Execute PTerm
tm))
where
maintm :: PTerm
maintm = FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC "(repl)") [] (Name -> [String] -> Name
sNS (String -> Name
sUN "main") ["Main"])
cmd_dynamic :: String -> IP.IdrisParser (Either String Command)
cmd_dynamic :: String -> Parser IState (Either String Command)
cmd_dynamic name :: String
name = do
let optArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
optArg = do String
l <- StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
if (String
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "")
then Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (String -> Command
DynamicLink String
l)
else Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right Command
ListDynamic
let failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b))
-> Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall a b. (a -> b) -> a -> b
$ String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ "Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [<library>]"
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
optArg Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure
cmd_pprint :: String -> IP.IdrisParser (Either String Command)
cmd_pprint :: String -> Parser IState (Either String Command)
cmd_pprint name :: String
name = do
OutputFmt
fmt <- IdrisParser OutputFmt
ppFormat
StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace
Int
n <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural
StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace
PTerm
t <- SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (OutputFmt -> Int -> PTerm -> Command
PPrint OutputFmt
fmt Int
n PTerm
t))
where
ppFormat :: IP.IdrisParser OutputFmt
ppFormat :: IdrisParser OutputFmt
ppFormat = (StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
discard (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "html") StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser OutputFmt -> IdrisParser OutputFmt
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputFmt -> IdrisParser OutputFmt
forall (m :: * -> *) a. Monad m => a -> m a
return OutputFmt
HTMLOutput)
IdrisParser OutputFmt
-> IdrisParser OutputFmt -> IdrisParser OutputFmt
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
discard (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "latex") StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser OutputFmt -> IdrisParser OutputFmt
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputFmt -> IdrisParser OutputFmt
forall (m :: * -> *) a. Monad m => a -> m a
return OutputFmt
LaTeXOutput)
cmd_compile :: String -> IP.IdrisParser (Either String Command)
cmd_compile :: String -> Parser IState (Either String Command)
cmd_compile name :: String
name = do
let defaultCodegen :: Codegen
defaultCodegen = IRFormat -> String -> Codegen
Via IRFormat
IBCFormat "c"
let codegenOption :: IP.IdrisParser Codegen
codegenOption :: IdrisParser Codegen
codegenOption = do
let bytecodeCodegen :: IdrisParser Codegen
bytecodeCodegen = StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
discard (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "bytecode") StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser Codegen -> IdrisParser Codegen
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Codegen -> IdrisParser Codegen
forall (m :: * -> *) a. Monad m => a -> m a
return Codegen
Bytecode
viaCodegen :: IdrisParser Codegen
viaCodegen = do String
x <- IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.identifier
Codegen -> IdrisParser Codegen
forall (m :: * -> *) a. Monad m => a -> m a
return (IRFormat -> String -> Codegen
Via IRFormat
IBCFormat ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
x))
IdrisParser Codegen
bytecodeCodegen IdrisParser Codegen -> IdrisParser Codegen -> IdrisParser Codegen
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser Codegen
viaCodegen
let hasOneArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
hasOneArg = do
IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
String
f <- IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.identifier
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (Codegen -> String -> Command
Compile Codegen
defaultCodegen String
f)
let hasTwoArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
hasTwoArgs = do
IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
Codegen
codegen <- IdrisParser Codegen
codegenOption
String
f <- IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.identifier
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command))
-> Either a Command
-> StateT
IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either a Command
forall a b. b -> Either a b
Right (Codegen -> String -> Command
Compile Codegen
codegen String
f)
let failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b))
-> Either String b
-> StateT
IState (WriterT FC (Parsec Void String)) (Either String b)
forall a b. (a -> b) -> a -> b
$ String -> Either String b
forall a b. a -> Either a b
Left (String -> Either String b) -> String -> Either String b
forall a b. (a -> b) -> a -> b
$ "Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [<codegen>] <filename>"
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
hasTwoArgs Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
hasOneArg Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure
cmd_addproof :: String -> IP.IdrisParser (Either String Command)
cmd_addproof :: String -> Parser IState (Either String Command)
cmd_addproof name :: String
name = do
Maybe Name
n <- Maybe Name
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Maybe Name
forall a. Maybe a
Nothing (StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name))
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
forall a b. (a -> b) -> a -> b
$ do
Name
x <- IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
Maybe Name
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x)
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Maybe Name -> Command
AddProof Maybe Name
n))
cmd_log :: String -> IP.IdrisParser (Either String Command)
cmd_log :: String -> Parser IState (Either String Command)
cmd_log name :: String
name = do
Int
i <- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Int -> Command
LogLvl Int
i))
cmd_verb :: String -> IP.IdrisParser (Either String Command)
cmd_verb :: String -> Parser IState (Either String Command)
cmd_verb name :: String
name = do
Int
i <- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Int -> Command
Verbosity Int
i))
cmd_cats :: String -> IP.IdrisParser (Either String Command)
cmd_cats :: String -> Parser IState (Either String Command)
cmd_cats name :: String
name = do
[[LogCat]]
cs <- StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [[LogCat]]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy StateT IState (WriterT FC (Parsec Void String)) [LogCat]
pLogCats (StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace)
StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String Command -> Parser IState (Either String Command))
-> Either String Command -> Parser IState (Either String Command)
forall a b. (a -> b) -> a -> b
$ Command -> Either String Command
forall a b. b -> Either a b
Right (Command -> Either String Command)
-> Command -> Either String Command
forall a b. (a -> b) -> a -> b
$ [LogCat] -> Command
LogCategory ([[LogCat]] -> [LogCat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[LogCat]]
cs)
where
badCat :: StateT IState (WriterT FC (Parsec Void String)) b
badCat = do
String
c <- IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.identifier
String -> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT IState (WriterT FC (Parsec Void String)) b)
-> String -> StateT IState (WriterT FC (Parsec Void String)) b
forall a b. (a -> b) -> a -> b
$ "Category: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not recognised."
pLogCats :: IP.IdrisParser [LogCat]
pLogCats :: StateT IState (WriterT FC (Parsec Void String)) [LogCat]
pLogCats = StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat]
parserCats [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IParse))
StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat]
elabCats [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IElab))
StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat]
codegenCats [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
ICodeGen))
StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat
ICoverage] [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
ICoverage))
StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat
IIBC] [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IIBC))
StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat
IErasure] [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IErasure))
StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
-> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall b. StateT IState (WriterT FC (Parsec Void String)) b
badCat
cmd_let :: String -> IP.IdrisParser (Either String Command)
cmd_let :: String -> Parser IState (Either String Command)
cmd_let name :: String
name = do
[PDecl]
defn <- [[PDecl]] -> [PDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PDecl]] -> [PDecl])
-> StateT IState (WriterT FC (Parsec Void String)) [[PDecl]]
-> StateT IState (WriterT FC (Parsec Void String)) [PDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) [PDecl]
-> StateT IState (WriterT FC (Parsec Void String)) [[PDecl]]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) [PDecl]
IP.decl SyntaxInfo
defaultSyntax)
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right ([PDecl] -> Command
NewDefn [PDecl]
defn))
cmd_unlet :: String -> IP.IdrisParser (Either String Command)
cmd_unlet :: String -> Parser IState (Either String Command)
cmd_unlet name :: String
name = Command -> Either String Command
forall a b. b -> Either a b
Right (Command -> Either String Command)
-> ([Name] -> Command) -> [Name] -> Either String Command
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Command
Undefine ([Name] -> Either String Command)
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
-> Parser IState (Either String Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IdrisParser Name
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
cmd_loadto :: String -> IP.IdrisParser (Either String Command)
cmd_loadto :: String -> Parser IState (Either String Command)
cmd_loadto name :: String
name = do
Int
toline <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural
String
f <- StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (String -> Maybe Int -> Command
Load String
f (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
toline)))
cmd_colour :: String -> IP.IdrisParser (Either String Command)
cmd_colour :: String -> Parser IState (Either String Command)
cmd_colour name :: String
name = (Command -> Either String Command)
-> StateT IState (WriterT FC (Parsec Void String)) Command
-> Parser IState (Either String Command)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Command -> Either String Command
forall a b. b -> Either a b
Right StateT IState (WriterT FC (Parsec Void String)) Command
pSetColourCmd
where
colours :: [(String, Maybe Color)]
colours :: [(String, Maybe Color)]
colours = [ ("black", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Black)
, ("red", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Red)
, ("green", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Green)
, ("yellow", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Yellow)
, ("blue", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Blue)
, ("magenta", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Magenta)
, ("cyan", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Cyan)
, ("white", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
White)
, ("default", Maybe Color
forall a. Maybe a
Nothing)
]
pSetColourCmd :: IP.IdrisParser Command
pSetColourCmd :: StateT IState (WriterT FC (Parsec Void String)) Command
pSetColourCmd = (do ColourType
c <- IdrisParser ColourType
pColourType
let defaultColour :: IdrisColour
defaultColour = Maybe Color -> Bool -> Bool -> Bool -> Bool -> IdrisColour
IdrisColour Maybe Color
forall a. Maybe a
Nothing Bool
True Bool
False Bool
False Bool
False
[IdrisColour -> IdrisColour]
opts <- StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
[IdrisColour -> IdrisColour]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
pColourMod (StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace)
let colour :: IdrisColour
colour = ((IdrisColour -> IdrisColour) -> IdrisColour -> IdrisColour)
-> IdrisColour -> [IdrisColour -> IdrisColour] -> IdrisColour
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (IdrisColour -> IdrisColour) -> IdrisColour -> IdrisColour
forall a b. (a -> b) -> a -> b
($) IdrisColour
defaultColour ([IdrisColour -> IdrisColour] -> IdrisColour)
-> [IdrisColour -> IdrisColour] -> IdrisColour
forall a b. (a -> b) -> a -> b
$ [IdrisColour -> IdrisColour] -> [IdrisColour -> IdrisColour]
forall a. [a] -> [a]
reverse [IdrisColour -> IdrisColour]
opts
Command -> StateT IState (WriterT FC (Parsec Void String)) Command
forall (m :: * -> *) a. Monad m => a -> m a
return (Command
-> StateT IState (WriterT FC (Parsec Void String)) Command)
-> Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall a b. (a -> b) -> a -> b
$ ColourType -> IdrisColour -> Command
SetColour ColourType
c IdrisColour
colour)
StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "on" StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT IState (WriterT FC (Parsec Void String)) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
ColourOn)
StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "off" StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Command
-> StateT IState (WriterT FC (Parsec Void String)) Command
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT IState (WriterT FC (Parsec Void String)) Command
forall (m :: * -> *) a. Monad m => a -> m a
return Command
ColourOff)
pColour :: IP.IdrisParser (Maybe Color)
pColour :: IdrisParser (Maybe Color)
pColour = [(String, Maybe Color)] -> IdrisParser (Maybe Color)
forall (m :: * -> *) a.
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[(String, a)] -> m a
doColour [(String, Maybe Color)]
colours
where doColour :: [(String, a)] -> m a
doColour [] = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Unknown colour"
doColour ((s :: String
s, c :: a
c):cs :: [(String, a)]
cs) = (m () -> m ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> m ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
s) m () -> m a -> m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
c) m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(String, a)] -> m a
doColour [(String, a)]
cs
pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)
pColourMod :: StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
pColourMod = StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doVivid (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "vivid")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doDull (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "dull")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doUnderline (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "underline")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doNoUnderline (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "nounderline")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doBold (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "bold")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doNoBold (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "nobold")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doItalic (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "italic")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doNoItalic (IdrisColour -> IdrisColour)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol "noitalic")
StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser (Maybe Color)
pColour IdrisParser (Maybe Color)
-> (Maybe Color
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour))
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall (m :: * -> *) a. Monad m => a -> m a
return ((IdrisColour -> IdrisColour)
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour))
-> (Maybe Color -> IdrisColour -> IdrisColour)
-> Maybe Color
-> StateT
IState
(WriterT FC (Parsec Void String))
(IdrisColour -> IdrisColour)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Color -> IdrisColour -> IdrisColour
doSetColour)
where doVivid :: IdrisColour -> IdrisColour
doVivid i :: IdrisColour
i = IdrisColour
i { vivid :: Bool
vivid = Bool
True }
doDull :: IdrisColour -> IdrisColour
doDull i :: IdrisColour
i = IdrisColour
i { vivid :: Bool
vivid = Bool
False }
doUnderline :: IdrisColour -> IdrisColour
doUnderline i :: IdrisColour
i = IdrisColour
i { underline :: Bool
underline = Bool
True }
doNoUnderline :: IdrisColour -> IdrisColour
doNoUnderline i :: IdrisColour
i = IdrisColour
i { underline :: Bool
underline = Bool
False }
doBold :: IdrisColour -> IdrisColour
doBold i :: IdrisColour
i = IdrisColour
i { bold :: Bool
bold = Bool
True }
doNoBold :: IdrisColour -> IdrisColour
doNoBold i :: IdrisColour
i = IdrisColour
i { bold :: Bool
bold = Bool
False }
doItalic :: IdrisColour -> IdrisColour
doItalic i :: IdrisColour
i = IdrisColour
i { italic :: Bool
italic = Bool
True }
doNoItalic :: IdrisColour -> IdrisColour
doNoItalic i :: IdrisColour
i = IdrisColour
i { italic :: Bool
italic = Bool
False }
doSetColour :: Maybe Color -> IdrisColour -> IdrisColour
doSetColour c :: Maybe Color
c i :: IdrisColour
i = IdrisColour
i { colour :: Maybe Color
colour = Maybe Color
c }
colourTypes :: [(String, ColourType)]
colourTypes :: [(String, ColourType)]
colourTypes = (ColourType -> (String, ColourType))
-> [ColourType] -> [(String, ColourType)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: ColourType
x -> (((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> String
forall a. Int -> [a] -> [a]
drop 6 (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String)
-> (ColourType -> String) -> ColourType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ColourType -> String
forall a. Show a => a -> String
show) ColourType
x, ColourType
x)) ([ColourType] -> [(String, ColourType)])
-> [ColourType] -> [(String, ColourType)]
forall a b. (a -> b) -> a -> b
$
ColourType -> ColourType -> [ColourType]
forall a. Enum a => a -> a -> [a]
enumFromTo ColourType
forall a. Bounded a => a
minBound ColourType
forall a. Bounded a => a
maxBound
pColourType :: IP.IdrisParser ColourType
pColourType :: IdrisParser ColourType
pColourType = [(String, ColourType)] -> IdrisParser ColourType
forall (m :: * -> *) a.
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[(String, a)] -> m a
doColourType [(String, ColourType)]
colourTypes
where doColourType :: [(String, a)] -> m a
doColourType [] = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ "Unknown colour category. Options: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String)
-> ([(String, ColourType)] -> [String])
-> [(String, ColourType)]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse ", " ([String] -> [String])
-> ([(String, ColourType)] -> [String])
-> [(String, ColourType)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, ColourType) -> String)
-> [(String, ColourType)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, ColourType) -> String
forall a b. (a, b) -> a
fst) [(String, ColourType)]
colourTypes
doColourType ((s :: String
s,ct :: a
ct):cts :: [(String, a)]
cts) = (m () -> m ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> m ()
forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
s) m () -> m a -> m a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
ct) m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(String, a)] -> m a
doColourType [(String, a)]
cts
idChar :: StateT IState (WriterT FC (Parsec Void String)) (Token String)
idChar = [Token String]
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf (['a'..'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ ['A'..'Z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ ['0'..'9'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ ['_'])
cmd_apropos :: String -> IP.IdrisParser (Either String Command)
cmd_apropos :: String -> Parser IState (Either String Command)
cmd_apropos = IdrisParser String
-> ([PkgName] -> String -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> Parser IState (Either String Command)
packageBasedCmd (StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some StateT IState (WriterT FC (Parsec Void String)) Char
StateT IState (WriterT FC (Parsec Void String)) (Token String)
idChar) [PkgName] -> String -> Command
Apropos
packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)
-> String -> IP.IdrisParser (Either String Command)
packageBasedCmd :: IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> Parser IState (Either String Command)
packageBasedCmd valParser :: IdrisParser a
valParser cmd :: [PkgName] -> a -> Command
cmd name :: String
name =
Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar '('
[PkgName]
pkgs <- StateT IState (WriterT FC (Parsec Void String)) PkgName
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [PkgName]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (StateT IState (WriterT FC (Parsec Void String)) PkgName
pkg StateT IState (WriterT FC (Parsec Void String)) PkgName
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar ',')
Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar ')'
a
val <- IdrisParser a
valParser
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right ([PkgName] -> a -> Command
cmd [PkgName]
pkgs a
val)))
Parser IState (Either String Command)
-> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do a
val <- IdrisParser a
valParser
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right ([PkgName] -> a -> Command
cmd [] a
val))
where
pkg :: StateT IState (WriterT FC (Parsec Void String)) PkgName
pkg = (String -> StateT IState (WriterT FC (Parsec Void String)) PkgName)
-> (PkgName
-> StateT IState (WriterT FC (Parsec Void String)) PkgName)
-> Either String PkgName
-> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall (m :: * -> *) a. MonadFail m => String -> m a
fail PkgName -> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String PkgName
-> StateT IState (WriterT FC (Parsec Void String)) PkgName)
-> (String -> Either String PkgName)
-> String
-> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String PkgName
pkgName (String -> StateT IState (WriterT FC (Parsec Void String)) PkgName)
-> IdrisParser String
-> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IdrisParser String
forall (m :: * -> *). Parsing m => m String
IP.packageName
cmd_search :: String -> IP.IdrisParser (Either String Command)
cmd_search :: String -> Parser IState (Either String Command)
cmd_search = IdrisParser PTerm
-> ([PkgName] -> PTerm -> Command)
-> String
-> Parser IState (Either String Command)
forall a.
IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> Parser IState (Either String Command)
packageBasedCmd
(SyntaxInfo -> IdrisParser PTerm
IP.fullExpr (SyntaxInfo
defaultSyntax { implicitAllowed :: Bool
implicitAllowed = Bool
True })) [PkgName] -> PTerm -> Command
Search
cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)
cmd_proofsearch :: String -> Parser IState (Either String Command)
cmd_proofsearch name :: String
name = do
Bool
upd <- Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False (Bool
True Bool
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar '!')
Int
l <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural; Name
n <- IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
[Name]
hints <- IdrisParser Name
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.fnName
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Bool -> Bool -> Int -> Name -> [Name] -> Command
DoProofSearch Bool
upd Bool
True Int
l Name
n [Name]
hints))
cmd_refine :: String -> IP.IdrisParser (Either String Command)
cmd_refine :: String -> Parser IState (Either String Command)
cmd_refine name :: String
name = do
Bool
upd <- Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar '!'; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
Int
l <- Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
IP.natural; Name
n <- IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
Name
hint <- IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.fnName
Either String Command -> Parser IState (Either String Command)
forall (m :: * -> *) a. Monad m => a -> m a
return (Command -> Either String Command
forall a b. b -> Either a b
Right (Bool -> Bool -> Int -> Name -> [Name] -> Command
DoProofSearch Bool
upd Bool
False Int
l Name
n [Name
hint]))