{-|
Module      : Idris.REPL.Parser
Description : Parser for the REPL commands.
License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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 IState
i String
inputname = forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
IP.runparser IdrisParser (Either String Command)
pCmd IState
i String
inputname forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
trim
    where trim :: String -> String
trim = String -> String
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
f
              where f :: String -> String
f = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = [(String
"errorcontext", Opt
ErrContext),
              (String
"showimplicits", Opt
ShowImpl),
              (String
"originalerrors", Opt
ShowOrigErr),
              (String
"autosolve", Opt
AutoSolve),
              (String
"nobanner", Opt
NoBanner),
              (String
"warnreach", Opt
WarnReach),
              (String
"evaltypes", Opt
EvalTypes),
              (String
"desugarnats", Opt
DesugarNats)]

help :: [([String], CmdArg, String)]
help :: [([String], CmdArg, String)]
help = ([String
"<expr>"], CmdArg
NoArg, String
"Evaluate an expression") forall a. a -> [a] -> [a]
:
  [ (forall a b. (a -> b) -> [a] -> [b]
map (Char
':' forall a. a -> [a] -> [a]
:) [String]
names, CmdArg
args, String
text) | ([String]
names, CmdArg
args, String
text, String -> IdrisParser (Either String Command)
_) <- CommandTable
parserCommandsForHelp ]

allHelp :: [([String], CmdArg, String)]
allHelp :: [([String], CmdArg, String)]
allHelp = [ (forall a b. (a -> b) -> [a] -> [b]
map (Char
':' forall a. a -> [a] -> [a]
:) [String]
names, CmdArg
args, String
text)
          | ([String]
names, CmdArg
args, String
text, String -> IdrisParser (Either String Command)
_) <- CommandTable
parserCommandsForHelp forall a. [a] -> [a] -> [a]
++ CommandTable
parserCommands ]

parserCommandsForHelp :: CommandTable
parserCommandsForHelp :: CommandTable
parserCommandsForHelp =
  [ forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"t", String
"type"] PTerm -> Command
Check String
"Check the type of an expression"
  , forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"core"] PTerm -> Command
Core String
"View the core language representation of a term"
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"miss", String
"missing"] Name -> Command
Missing String
"Show missing clauses"
  , ([String
"doc"], CmdArg
NameArg, String
"Show internal documentation", String -> IdrisParser (Either String Command)
cmd_doc)
  , ([String
"mkdoc"], CmdArg
NamespaceArg, String
"Generate IdrisDoc for namespace(s) and dependencies"
    , forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
"namespace" (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle) String -> Command
MakeDoc)
  , ([String
"apropos"], CmdArg -> CmdArg -> CmdArg
SeqArgs (CmdArg -> CmdArg
OptionalArg CmdArg
PkgArgs) CmdArg
NameArg, String
" Search names, types, and documentation"
    , String -> IdrisParser (Either String Command)
cmd_apropos)
  , ([String
"s", String
"search"], CmdArg -> CmdArg -> CmdArg
SeqArgs (CmdArg -> CmdArg
OptionalArg CmdArg
PkgArgs) CmdArg
ExprArg
    , String
" Search for values by type", String -> IdrisParser (Either String Command)
cmd_search)
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"wc", String
"whocalls"] Name -> Command
WhoCalls String
"List the callers of some name"
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"cw", String
"callswho"] Name -> Command
CallsWho String
"List the callees of some name"
  , forall {a} {c}.
a
-> ([String] -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
namespaceArgCmd [String
"browse"] [String] -> Command
Browse String
"List the contents of some namespace"
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"total"] Name -> Command
TotCheck String
"Check the totality of a name"
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"r", String
"reload"] Command
Reload String
"Reload current file"
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"w", String
"watch"] Command
Watch String
"Watch the current file for changes"
  , ([String
"l", String
"load"], CmdArg
FileArg, String
"Load a new file"
    , (String -> Command)
-> String -> IdrisParser (Either String Command)
strArg (\String
f -> String -> Maybe Int -> Command
Load String
f forall a. Maybe a
Nothing))
  , ([String
"!"], CmdArg
ShellCommandArg, String
"Run a shell command", (String -> Command)
-> String -> IdrisParser (Either String Command)
strArg String -> Command
RunShellCommand)
  , ([String
"cd"], CmdArg
FileArg, String
"Change working directory"
    , (String -> Command)
-> String -> IdrisParser (Either String Command)
strArg String -> Command
ChangeDirectory)
  , ([String
"module"], CmdArg
ModuleArg, String
"Import an extra module", (String -> Command)
-> String -> IdrisParser (Either String Command)
moduleArg String -> Command
ModImport) -- NOTE: dragons
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"e", String
"edit"] Command
Edit String
"Edit current file using $EDITOR or $VISUAL"
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"m", String
"metavars"] Command
Metavars String
"Show remaining proof obligations (metavariables or holes)"
  , ([String
"p", String
"prove"], CmdArg
MetaVarArg, String
"Prove a metavariable"
    , (Name -> Command) -> String -> IdrisParser (Either String Command)
nameArg (Bool -> Name -> Command
Prove Bool
False))
  , ([String
"elab"], CmdArg
MetaVarArg, String
"Build a metavariable using the elaboration shell"
    , (Name -> Command) -> String -> IdrisParser (Either String Command)
nameArg (Bool -> Name -> Command
Prove Bool
True))
  , ([String
"a", String
"addproof"], CmdArg
NameArg, String
"Add proof to source file", String -> IdrisParser (Either String Command)
cmd_addproof)
  , ([String
"rmproof"], CmdArg
NameArg, String
"Remove proof from proof stack"
    , (Name -> Command) -> String -> IdrisParser (Either String Command)
nameArg Name -> Command
RmProof)
  , ([String
"showproof"], CmdArg
NameArg, String
"Show proof"
    , (Name -> Command) -> String -> IdrisParser (Either String Command)
nameArg Name -> Command
ShowProof)
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"proofs"] Command
Proofs String
"Show available proofs"
  , forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"x"] PTerm -> Command
ExecVal String
"Execute IO actions resulting from an expression using the interpreter"
  , ([String
"c", String
"compile"], CmdArg
FileArg, String
"Compile to an executable [codegen] <filename>", String -> IdrisParser (Either String Command)
cmd_compile)
  , ([String
"exec", String
"execute"], CmdArg -> CmdArg
OptionalArg CmdArg
ExprArg, String
"Compile to an executable and run", String -> IdrisParser (Either String Command)
cmd_execute)
  , ([String
"dynamic"], CmdArg
FileArg, String
"Dynamically load a C library (similar to %dynamic)", String -> IdrisParser (Either String Command)
cmd_dynamic)
  , ([String
"dynamic"], CmdArg
NoArg, String
"List dynamically loaded C libraries", String -> IdrisParser (Either String Command)
cmd_dynamic)
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"?", String
"h", String
"help"] Command
Help String
"Display this help text"
  , forall {a} {c}.
a
-> (Opt -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
optArgCmd [String
"set"] Opt -> Command
SetOpt forall a b. (a -> b) -> a -> b
$ String
"Set an option (" forall a. [a] -> [a] -> [a]
++ String
optionsList forall a. [a] -> [a] -> [a]
++ String
")"
  , forall {a} {c}.
a
-> (Opt -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
optArgCmd [String
"unset"] Opt -> Command
UnsetOpt String
"Unset an option"
  , ([String
"color", String
"colour"], CmdArg
ColourArg
    , String
"Turn REPL colours on or off; set a specific colour"
    , String -> IdrisParser (Either String Command)
cmd_colour)
  , ([String
"consolewidth"], CmdArg
ConsoleWidthArg, String
"Set the width of the console", String -> IdrisParser (Either String Command)
cmd_consolewidth)
  , ([String
"printerdepth"], CmdArg -> CmdArg
OptionalArg CmdArg
NumberArg, String
"Set the maximum pretty-printer depth (no arg for infinite)", String -> IdrisParser (Either String Command)
cmd_printdepth)
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"q", String
"quit"] Command
Quit String
"Exit the Idris system"
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"version"] Command
ShowVersion String
"Display the Idris version"
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"warranty"] Command
Warranty String
"Displays warranty information"
  , ([String
"let"], CmdArg -> CmdArg
ManyArgs CmdArg
DeclArg
    , String
"Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"
    , String -> IdrisParser (Either String Command)
cmd_let)
  , ([String
"unlet", String
"undefine"], CmdArg -> CmdArg
ManyArgs CmdArg
NameArg
    , String
"Remove the listed repl definitions, or all repl definitions if no names given"
    , String -> IdrisParser (Either String Command)
cmd_unlet)
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"printdef"] Name -> Command
PrintDef String
"Show the definition of a function"
  , ([String
"pp", String
"pprint"], (CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
OptionArg (CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
NumberArg CmdArg
NameArg))
    , String
"Pretty prints an Idris function in either LaTeX or HTML and for a specified width."
    , String -> IdrisParser (Either String Command)
cmd_pprint)
  , ([String
"verbosity"], CmdArg
NumberArg, String
"Set verbosity level", String -> IdrisParser (Either String Command)
cmd_verb)
  ]
  where optionsList :: String
optionsList = forall a. [a] -> [[a]] -> [a]
intercalate String
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, Opt)]
setOptions


parserCommands :: CommandTable
parserCommands :: CommandTable
parserCommands =
  [ forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"u", String
"universes"] Command
Universes String
"Display universe constraints"
  , forall {a} {c}.
a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd [String
"errorhandlers"] Command
ListErrorHandlers String
"List registered error handlers"

  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"d", String
"def"] Name -> Command
Defn String
"Display a name's internal definitions"
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"transinfo"] Name -> Command
TransformInfo String
"Show relevant transformation rules for a name"
  , forall {a} {c}.
a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd [String
"di", String
"dbginfo"] Name -> Command
DebugInfo String
"Show debugging information for a name"

  , forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"patt"] PTerm -> Command
Pattelab String
"(Debugging) Elaborate pattern expression"
  , forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"spec"] PTerm -> Command
Spec String
"?"
  , forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"whnf"] PTerm -> Command
WHNF String
"(Debugging) Show weak head normal form of an expression"
  , forall {a} {c}.
a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd [String
"inline"] PTerm -> Command
TestInline String
"?"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"cs", String
"casesplit"] Bool -> Int -> Name -> Command
CaseSplitAt
      String
":cs <line> <name> splits the pattern variable on the line"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"apc", String
"addproofclause"] Bool -> Int -> Name -> Command
AddProofClauseFrom
      String
":apc <line> <name> adds a pattern-matching proof clause to name on line"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"ac", String
"addclause"] Bool -> Int -> Name -> Command
AddClauseFrom
      String
":ac <line> <name> adds a clause for the definition of the name on the line"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"am", String
"addmissing"] Bool -> Int -> Name -> Command
AddMissing
      String
":am <line> <name> adds all missing pattern matches for the name on the line"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"mw", String
"makewith"] Bool -> Int -> Name -> Command
MakeWith
      String
":mw <line> <name> adds a with clause for the definition of the name on the line"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"mc", String
"makecase"] Bool -> Int -> Name -> Command
MakeCase
      String
":mc <line> <name> adds a case block for the definition of the metavariable on the line"
  , forall {a} {c}.
a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd [String
"ml", String
"makelemma"] Bool -> Int -> Name -> Command
MakeLemma String
"?"
  , ([String
"log"], CmdArg
NumberArg, String
"Set logging level", String -> IdrisParser (Either String Command)
cmd_log)
  , ( [String
"logcats"]
    , CmdArg -> CmdArg
ManyArgs CmdArg
NameArg
    , String
"Set logging categories"
    , String -> IdrisParser (Either String Command)
cmd_cats)
  , ([String
"lto", String
"loadto"], CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
NumberArg CmdArg
FileArg
    , String
"Load file up to line number", String -> IdrisParser (Either String Command)
cmd_loadto)
  , ([String
"ps", String
"proofsearch"], CmdArg
NoArg
    , String
":ps <line> <name> <names> does proof search for name on line, with names as hints"
    , String -> IdrisParser (Either String Command)
cmd_proofsearch)
  , ([String
"ref", String
"refine"], CmdArg
NoArg
    , String
":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable"
    , String -> IdrisParser (Either String Command)
cmd_refine)
  , ([String
"debugunify"], CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
ExprArg CmdArg
ExprArg
    , String
"(Debugging) Try to unify two expressions", forall a b. a -> b -> a
const 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
       forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (PTerm -> PTerm -> Command
DebugUnify PTerm
l PTerm
r))
    )
  ]

noArgCmd :: a
-> Command
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
noArgCmd a
names Command
command c
doc =
  (a
names, CmdArg
NoArg, c
doc, Command -> String -> IdrisParser (Either String Command)
noArgs Command
command)
nameArgCmd :: a
-> (Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
nameArgCmd a
names Name -> Command
command c
doc =
  (a
names, CmdArg
NameArg, c
doc, (Name -> Command) -> String -> IdrisParser (Either String Command)
fnNameArg Name -> Command
command)
namespaceArgCmd :: a
-> ([String] -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
namespaceArgCmd a
names [String] -> Command
command c
doc =
  (a
names, CmdArg
NamespaceArg, c
doc, ([String] -> Command)
-> String -> IdrisParser (Either String Command)
namespaceArg [String] -> Command
command)
exprArgCmd :: a
-> (PTerm -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
exprArgCmd a
names PTerm -> Command
command c
doc =
  (a
names, CmdArg
ExprArg, c
doc, (PTerm -> Command) -> String -> IdrisParser (Either String Command)
exprArg PTerm -> Command
command)
optArgCmd :: a
-> (Opt -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
optArgCmd a
names Opt -> Command
command c
doc =
  (a
names, CmdArg
OptionArg, c
doc, (Opt -> Command) -> String -> IdrisParser (Either String Command)
optArg Opt -> Command
command)
proofArgCmd :: a
-> (Bool -> Int -> Name -> Command)
-> c
-> (a, CmdArg, c, String -> IdrisParser (Either String Command))
proofArgCmd a
names Bool -> Int -> Name -> Command
command c
doc =
  (a
names, CmdArg
NoArg, c
doc, (Bool -> Int -> Name -> Command)
-> String -> IdrisParser (Either String Command)
proofArg Bool -> Int -> Name -> Command
command)

pCmd :: IP.IdrisParser (Either String Command)
pCmd :: IdrisParser (Either String Command)
pCmd = 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 -> IdrisParser (Either String Command)
parser String
c
                | ([String]
names, CmdArg
_, String
_, String -> IdrisParser (Either String Command)
parser) <- CommandTable
parserCommandsForHelp forall a. [a] -> [a] -> [a]
++ CommandTable
parserCommands ]
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
unrecognized
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
nop
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser (Either String Command)
eval
    where nop :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
nop = do forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right Command
NOP)
          unrecognized :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
unrecognized = do
              forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
':'
              String
cmd <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
              let cmd' :: String
cmd' = forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Eq a => a -> a -> Bool
/=Char
' ') String
cmd
              forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Unrecognized command: " forall a. [a] -> [a] -> [a]
++ String
cmd')

cmd :: [String] -> IP.IdrisParser String
cmd :: [String] -> IdrisParser String
cmd [String]
xs = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
':'
    forall {m :: * -> *}.
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[String] -> m String
docmd [String]
sorted_xs

    where docmd :: [String] -> m String
docmd [] = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Could not parse command"
          docmd (String
x:[String]
xs) = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => String -> m ()
IP.reserved String
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return String
x) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [String] -> m String
docmd [String]
xs

          sorted_xs :: [String]
sorted_xs = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\String
x String
y -> forall a. Ord a => a -> a -> Ordering
compare (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y) (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x)) [String]
xs


noArgs :: Command -> String -> IP.IdrisParser (Either String Command)
noArgs :: Command -> String -> IdrisParser (Either String Command)
noArgs Command
cmd String
name = do
    let emptyArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
emptyArgs = do
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right Command
cmd)

    let failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
":" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" takes no arguments")

    forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
emptyArgs forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure

eval :: IP.IdrisParser (Either String Command)
eval :: IdrisParser (Either String Command)
eval = do
  PTerm
t <- SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 -> IdrisParser (Either String Command)
exprArg PTerm -> Command
cmd String
name = do
    let noArg :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
noArg = do
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (String
"Usage is :" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" <expression>")

    let justOperator :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
justOperator = do
          (String
op, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
IP.withExtent forall (m :: * -> *). Parsing m => m String
IP.symbolicOperator
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right 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
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (PTerm -> Command
cmd PTerm
t)
    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
noArg forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
justOperator forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 :: forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
argName IdrisParser a
argParser a -> Command
cmd String
name = do
    let emptyArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs = do forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof; 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
                    forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (a -> Command
cmd a
arg))
    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (String
"Usage is :" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" <" forall a. [a] -> [a] -> [a]
++ String
argName forall a. [a] -> [a] -> [a]
++ String
">")

nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)
nameArg :: (Name -> Command) -> String -> IdrisParser (Either String Command)
nameArg = forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
"name" forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
fnNameArg :: (Name -> Command) -> String -> IdrisParser (Either String Command)
fnNameArg = forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
"functionname" forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.fnName

strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)
strArg :: (String -> Command)
-> String -> IdrisParser (Either String Command)
strArg = forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
"string" (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many 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 -> IdrisParser (Either String Command)
moduleArg = forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
"module" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
toPath forall (m :: * -> *). Parsing m => m String
IP.identifier)
  where
    toPath :: String -> String
toPath String
n = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [[a]]
splitOn String
"." String
n

namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)
namespaceArg :: ([String] -> Command)
-> String -> IdrisParser (Either String Command)
namespaceArg = forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> IdrisParser (Either String Command)
genArg String
"namespace" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> [String]
toNS forall (m :: * -> *). Parsing m => m String
IP.identifier)
  where
    toNS :: String -> [String]
toNS  = forall a. Eq a => [a] -> [a] -> [[a]]
splitOn String
"."

optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)
optArg :: (Opt -> Command) -> String -> IdrisParser (Either String Command)
optArg Opt -> Command
cmd String
name = do
    let emptyArgs :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs = do
            forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (String
"Usage is :" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" <option>")

    let oneArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg = do
          Opt
o <- IdrisParser Opt
pOption
          forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left String
"Unrecognized setting"

    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
emptyArgs forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
oneArg forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure

    where
        pOption :: IP.IdrisParser Opt
        pOption :: IdrisParser Opt
pOption = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a. Alternative f => f a
empty forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(String
a, Opt
b) -> do forall (m :: * -> *) a. Monad m => m a -> m ()
discard (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
a); 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 -> IdrisParser (Either String Command)
proofArg Bool -> Int -> Name -> Command
cmd String
name = do
    Bool
upd <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
'!'
        forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Integer
l <- forall (m :: * -> *). Parsing m => m Integer
IP.natural
    Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Bool -> Int -> Name -> Command
cmd Bool
upd (forall a. Num a => Integer -> a
fromInteger Integer
l) Name
n))

cmd_doc :: String -> IP.IdrisParser (Either String Command)
cmd_doc :: String -> IdrisParser (Either String Command)
cmd_doc String
name = do
    let constant :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
constant = do
          Const
c <- forall (m :: * -> *). Parsing m => m Const
IP.constant
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (Either Name Const -> HowMuchDocs -> Command
DocStr (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
          forall (m :: * -> *). Parsing m => String -> m ()
IP.reserved String
"Type"
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (Either Name Const -> HowMuchDocs -> Command
DocStr (forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String -> Name
sUN String
"Type") HowMuchDocs
FullDocs)

    let fnName :: IdrisParser (Either String Command)
fnName = (Name -> Command) -> String -> IdrisParser (Either String Command)
fnNameArg (\Name
n -> Either Name Const -> HowMuchDocs -> Command
DocStr (forall a b. a -> Either a b
Left Name
n) HowMuchDocs
FullDocs) String
name

    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
constant forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
pType forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser (Either String Command)
fnName

cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)
cmd_consolewidth :: String -> IdrisParser (Either String Command)
cmd_consolewidth String
name = do
    ConsoleWidth
w <- IdrisParser ConsoleWidth
pConsoleWidth
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (ConsoleWidth -> Command
SetConsoleWidth ConsoleWidth
w))

    where
        pConsoleWidth :: IP.IdrisParser ConsoleWidth
        pConsoleWidth :: IdrisParser ConsoleWidth
pConsoleWidth = do forall (m :: * -> *) a. Monad m => m a -> m ()
discard (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"auto"); forall (m :: * -> *) a. Monad m => a -> m a
return ConsoleWidth
AutomaticWidth
                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *) a. Monad m => m a -> m ()
discard (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"infinite"); forall (m :: * -> *) a. Monad m => a -> m a
return ConsoleWidth
InfinitelyWide
                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Int
n <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural
                           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 -> IdrisParser (Either String Command)
cmd_printdepth String
_ = do Maybe Int
d <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural)
                      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right 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 -> IdrisParser (Either String Command)
cmd_execute String
name = do
    PTerm
tm <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option PTerm
maintm (SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax)
    forall (m :: * -> *) a. Monad m => a -> m a
return (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 String
"(repl)") [] (Name -> [String] -> Name
sNS (String -> Name
sUN String
"main") [String
"Main"])

cmd_dynamic :: String -> IP.IdrisParser (Either String Command)
cmd_dynamic :: String -> IdrisParser (Either String Command)
cmd_dynamic String
name = do
    let optArg :: StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
optArg = do String
l <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
                    if (String
l forall a. Eq a => a -> a -> Bool
/= String
"")
                        then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (String -> Command
DynamicLink String
l)
                        else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right Command
ListDynamic
    let failure :: StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Usage is :" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" [<library>]"
    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
optArg forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure

cmd_pprint :: String -> IP.IdrisParser (Either String Command)
cmd_pprint :: String -> IdrisParser (Either String Command)
cmd_pprint String
name = do
     OutputFmt
fmt <- IdrisParser OutputFmt
ppFormat
     forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace
     Int
n <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural
     forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace
     PTerm
t <- SyntaxInfo -> IdrisParser PTerm
IP.fullExpr SyntaxInfo
defaultSyntax
     forall (m :: * -> *) a. Monad m => a -> m a
return (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 = (forall (m :: * -> *) a. Monad m => m a -> m ()
discard (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"html") forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return OutputFmt
HTMLOutput)
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *) a. Monad m => m a -> m ()
discard (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"latex") forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return OutputFmt
LaTeXOutput)

cmd_compile :: String -> IP.IdrisParser (Either String Command)
cmd_compile :: String -> IdrisParser (Either String Command)
cmd_compile String
name = do
    let defaultCodegen :: Codegen
defaultCodegen = IRFormat -> String -> Codegen
Via IRFormat
IBCFormat String
"c"

    let codegenOption :: IP.IdrisParser Codegen
        codegenOption :: IdrisParser Codegen
codegenOption = do
            let bytecodeCodegen :: IdrisParser Codegen
bytecodeCodegen = forall (m :: * -> *) a. Monad m => m a -> m ()
discard (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"bytecode") forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return Codegen
Bytecode
                viaCodegen :: IdrisParser Codegen
viaCodegen = do String
x <- forall (m :: * -> *). Parsing m => m String
IP.identifier
                                forall (m :: * -> *) a. Monad m => a -> m a
return (IRFormat -> String -> Codegen
Via IRFormat
IBCFormat (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
x))
            IdrisParser Codegen
bytecodeCodegen 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 <- forall s (m :: * -> *). MonadState s m => m s
get
          String
f <- forall (m :: * -> *). Parsing m => m String
IP.identifier
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall s (m :: * -> *). MonadState s m => m s
get
          Codegen
codegen <- IdrisParser Codegen
codegenOption
          String
f <- forall (m :: * -> *). Parsing m => m String
IP.identifier
          forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Usage is :" forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" [<codegen>] <filename>"
    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
hasTwoArgs forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall {a}.
StateT IState (WriterT FC (Parsec Void String)) (Either a Command)
hasOneArg forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}.
StateT IState (WriterT FC (Parsec Void String)) (Either String b)
failure

cmd_addproof :: String -> IP.IdrisParser (Either String Command)
cmd_addproof :: String -> IdrisParser (Either String Command)
cmd_addproof String
name = do
    Maybe Name
n <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ do
        Name
x <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Name
x)
    forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
    forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> IdrisParser (Either String Command)
cmd_log String
name = do
    Int
i <- forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural
    forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Int -> Command
LogLvl Int
i))

cmd_verb :: String -> IP.IdrisParser (Either String Command)
cmd_verb :: String -> IdrisParser (Either String Command)
cmd_verb String
name = do
    Int
i <- forall a b. (Integral a, Num b) => a -> b
fromIntegral forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural
    forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Int -> Command
Verbosity Int
i))

cmd_cats :: String -> IP.IdrisParser (Either String Command)
cmd_cats :: String -> IdrisParser (Either String Command)
cmd_cats String
name = do
    [[LogCat]]
cs <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy IdrisParser [LogCat]
pLogCats (forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace)
    forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ [LogCat] -> Command
LogCategory (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 <- forall (m :: * -> *). Parsing m => m String
IP.identifier
      forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Category: " forall a. [a] -> [a] -> [a]
++ String
c forall a. [a] -> [a] -> [a]
++ String
" is not recognised."

    pLogCats :: IP.IdrisParser [LogCat]
    pLogCats :: IdrisParser [LogCat]
pLogCats = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat]
parserCats  forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IParse))
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat]
elabCats    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IElab))
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat]
codegenCats forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
ICodeGen))
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat
ICoverage] forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
ICoverage))
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat
IIBC]      forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IIBC))
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([LogCat
IErasure]  forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol (LogCat -> String
strLogCat LogCat
IErasure))
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {b}. StateT IState (WriterT FC (Parsec Void String)) b
badCat

cmd_let :: String -> IP.IdrisParser (Either String Command)
cmd_let :: String -> IdrisParser (Either String Command)
cmd_let String
name = do
    [PDecl]
defn <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) [PDecl]
IP.decl SyntaxInfo
defaultSyntax)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right ([PDecl] -> Command
NewDefn [PDecl]
defn))

cmd_unlet :: String -> IP.IdrisParser (Either String Command)
cmd_unlet :: String -> IdrisParser (Either String Command)
cmd_unlet String
name = forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Command
Undefine forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name

cmd_loadto :: String -> IP.IdrisParser (Either String Command)
cmd_loadto :: String -> IdrisParser (Either String Command)
cmd_loadto String
name = do
    Int
toline <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural
    String
f <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (String -> Maybe Int -> Command
Load String
f (forall a. a -> Maybe a
Just Int
toline)))

cmd_colour :: String -> IP.IdrisParser (Either String Command)
cmd_colour :: String -> IdrisParser (Either String Command)
cmd_colour String
name = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right IdrisParser Command
pSetColourCmd

    where
        colours :: [(String, Maybe Color)]
        colours :: [(String, Maybe Color)]
colours = [ (String
"black", forall a. a -> Maybe a
Just Color
Black)
                  , (String
"red", forall a. a -> Maybe a
Just Color
Red)
                  , (String
"green", forall a. a -> Maybe a
Just Color
Green)
                  , (String
"yellow", forall a. a -> Maybe a
Just Color
Yellow)
                  , (String
"blue", forall a. a -> Maybe a
Just Color
Blue)
                  , (String
"magenta", forall a. a -> Maybe a
Just Color
Magenta)
                  , (String
"cyan", forall a. a -> Maybe a
Just Color
Cyan)
                  , (String
"white", forall a. a -> Maybe a
Just Color
White)
                  , (String
"default", forall a. Maybe a
Nothing)
                  ]

        pSetColourCmd :: IP.IdrisParser Command
        pSetColourCmd :: IdrisParser Command
pSetColourCmd = (do ColourType
c <- IdrisParser ColourType
pColourType
                            let defaultColour :: IdrisColour
defaultColour = Maybe Color -> Bool -> Bool -> Bool -> Bool -> IdrisColour
IdrisColour forall a. Maybe a
Nothing Bool
True Bool
False Bool
False Bool
False
                            [IdrisColour -> IdrisColour]
opts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy IdrisParser (IdrisColour -> IdrisColour)
pColourMod (forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace)
                            let colour :: IdrisColour
colour = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
($) IdrisColour
defaultColour forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [IdrisColour -> IdrisColour]
opts
                            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ColourType -> IdrisColour -> Command
SetColour ColourType
c IdrisColour
colour)
                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"on" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Command
ColourOn)
                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"off" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Command
ColourOff)

        pColour :: IP.IdrisParser (Maybe Color)
        pColour :: IdrisParser (Maybe Color)
pColour = 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 [] = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Unknown colour"
                  doColour ((String
s, a
c):[(String, a)]
cs) = (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return a
c) 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 :: IdrisParser (IdrisColour -> IdrisColour)
pColourMod = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doVivid forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"vivid")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doDull forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"dull")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doUnderline forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"underline")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doNoUnderline forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"nounderline")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doBold forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"bold")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doNoBold forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"nobold")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doItalic forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"italic")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisColour -> IdrisColour
doNoItalic forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
"noitalic")
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser (Maybe Color)
pColour forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Color -> IdrisColour -> IdrisColour
doSetColour)
            where doVivid :: IdrisColour -> IdrisColour
doVivid IdrisColour
i       = IdrisColour
i { vivid :: Bool
vivid = Bool
True }
                  doDull :: IdrisColour -> IdrisColour
doDull IdrisColour
i        = IdrisColour
i { vivid :: Bool
vivid = Bool
False }
                  doUnderline :: IdrisColour -> IdrisColour
doUnderline IdrisColour
i   = IdrisColour
i { underline :: Bool
underline = Bool
True }
                  doNoUnderline :: IdrisColour -> IdrisColour
doNoUnderline IdrisColour
i = IdrisColour
i { underline :: Bool
underline = Bool
False }
                  doBold :: IdrisColour -> IdrisColour
doBold IdrisColour
i        = IdrisColour
i { bold :: Bool
bold = Bool
True }
                  doNoBold :: IdrisColour -> IdrisColour
doNoBold IdrisColour
i      = IdrisColour
i { bold :: Bool
bold = Bool
False }
                  doItalic :: IdrisColour -> IdrisColour
doItalic IdrisColour
i      = IdrisColour
i { italic :: Bool
italic = Bool
True }
                  doNoItalic :: IdrisColour -> IdrisColour
doNoItalic IdrisColour
i    = IdrisColour
i { italic :: Bool
italic = Bool
False }
                  doSetColour :: Maybe Color -> IdrisColour -> IdrisColour
doSetColour Maybe Color
c IdrisColour
i = IdrisColour
i { colour :: Maybe Color
colour = Maybe Color
c }

        -- | Generate the colour type names using the default Show instance.
        colourTypes :: [(String, ColourType)]
        colourTypes :: [(String, ColourType)]
colourTypes = forall a b. (a -> b) -> [a] -> [b]
map (\ColourType
x -> ((forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop Int
6 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) ColourType
x, ColourType
x)) forall a b. (a -> b) -> a -> b
$
                      forall a. Enum a => a -> a -> [a]
enumFromTo forall a. Bounded a => a
minBound forall a. Bounded a => a
maxBound

        pColourType :: IP.IdrisParser ColourType
        pColourType :: IdrisParser ColourType
pColourType = 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 [] = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Unknown colour category. Options: " forall a. [a] -> [a] -> [a]
++
                                           (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse String
", " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst) [(String, ColourType)]
colourTypes
                  doColourType ((String
s,a
ct):[(String, a)]
cts) = (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => String -> m ()
IP.symbol String
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return a
ct) 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 = forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf ([Char
'a'..Char
'z'] forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z'] forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9'] forall a. [a] -> [a] -> [a]
++ [Char
'_'])

cmd_apropos :: String -> IP.IdrisParser (Either String Command)
cmd_apropos :: String -> IdrisParser (Either String Command)
cmd_apropos = forall a.
IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> IdrisParser (Either String Command)
packageBasedCmd (forall (f :: * -> *) a. Alternative f => f a -> f [a]
some 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 :: forall a.
IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> IdrisParser (Either String Command)
packageBasedCmd IdrisParser a
valParser [PkgName] -> a -> Command
cmd String
name =
  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
'('
            [PkgName]
pkgs <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (StateT IState (WriterT FC (Parsec Void String)) PkgName
pkg forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => m ()
IP.whiteSpace) (forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
',')
            forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
')'
            a
val <- IdrisParser a
valParser
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right ([PkgName] -> a -> Command
cmd [PkgName]
pkgs a
val)))
   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do a
val <- IdrisParser a
valParser
          forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String PkgName
pkgName forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). Parsing m => m String
IP.packageName

cmd_search :: String -> IP.IdrisParser (Either String Command)
cmd_search :: String -> IdrisParser (Either String Command)
cmd_search = forall a.
IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> IdrisParser (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 -> IdrisParser (Either String Command)
cmd_proofsearch String
name = do
    Bool
upd <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False (Bool
True forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
'!')
    Int
l <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural; Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
    [Name]
hints <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.fnName
    forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> IdrisParser (Either String Command)
cmd_refine String
name = do
   Bool
upd <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False (do forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
'!'; forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
   Int
l <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
IP.natural; Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.name
   Name
hint <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
IP.fnName
   forall (m :: * -> *) a. Monad m => a -> m a
return (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]))