{-|
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 = 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 = [(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") ([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
':' Char -> String -> String
forall a. a -> [a] -> [a]
:) [String]
names, CmdArg
args, String
text) | ([String]
names, CmdArg
args, String
text, String -> Parser IState (Either String Command)
_) <- CommandTable
parserCommandsForHelp ]

allHelp :: [([String], CmdArg, String)]
allHelp :: [([String], CmdArg, String)]
allHelp = [ ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char
':' Char -> String -> String
forall a. a -> [a] -> [a]
:) [String]
names, CmdArg
args, String
text)
          | ([String]
names, CmdArg
args, String
text, String -> Parser IState (Either String Command)
_) <- 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 [String
"t", String
"type"] PTerm -> Command
Check String
"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 [String
"core"] PTerm -> Command
Core String
"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 [String
"miss", String
"missing"] Name -> Command
Missing String
"Show missing clauses"
  , ([String
"doc"], CmdArg
NameArg, String
"Show internal documentation", String -> Parser IState (Either String Command)
cmd_doc)
  , ([String
"mkdoc"], CmdArg
NamespaceArg, String
"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 String
"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
StateT IState (WriterT FC (Parsec Void String)) (Token String)
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 -> Parser IState (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 -> 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 [String
"wc", String
"whocalls"] Name -> Command
WhoCalls String
"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 [String
"cw", String
"callswho"] Name -> Command
CallsWho String
"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 [String
"browse"] [String] -> Command
Browse String
"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 [String
"total"] Name -> Command
TotCheck String
"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 [String
"r", String
"reload"] Command
Reload String
"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 [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 -> Parser IState (Either String Command)
strArg (\String
f -> String -> Maybe Int -> Command
Load String
f Maybe Int
forall a. Maybe a
Nothing))
  , ([String
"!"], CmdArg
ShellCommandArg, String
"Run a shell command", (String -> Command)
-> String -> Parser IState (Either String Command)
strArg String -> Command
RunShellCommand)
  , ([String
"cd"], CmdArg
FileArg, String
"Change working directory"
    , (String -> Command)
-> String -> Parser IState (Either String Command)
strArg String -> Command
ChangeDirectory)
  , ([String
"module"], CmdArg
ModuleArg, String
"Import an extra module", (String -> Command)
-> String -> Parser IState (Either String Command)
moduleArg String -> Command
ModImport) -- NOTE: dragons
  , [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 [String
"e", String
"edit"] Command
Edit String
"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 [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 -> Parser IState (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 -> Parser IState (Either String Command)
nameArg (Bool -> Name -> Command
Prove Bool
True))
  , ([String
"a", String
"addproof"], CmdArg
NameArg, String
"Add proof to source file", String -> Parser IState (Either String Command)
cmd_addproof)
  , ([String
"rmproof"], CmdArg
NameArg, String
"Remove proof from proof stack"
    , (Name -> Command)
-> String -> Parser IState (Either String Command)
nameArg Name -> Command
RmProof)
  , ([String
"showproof"], CmdArg
NameArg, String
"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 [String
"proofs"] Command
Proofs String
"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 [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 -> Parser IState (Either String Command)
cmd_compile)
  , ([String
"exec", String
"execute"], CmdArg -> CmdArg
OptionalArg CmdArg
ExprArg, String
"Compile to an executable and run", String -> Parser IState (Either String Command)
cmd_execute)
  , ([String
"dynamic"], CmdArg
FileArg, String
"Dynamically load a C library (similar to %dynamic)", String -> Parser IState (Either String Command)
cmd_dynamic)
  , ([String
"dynamic"], CmdArg
NoArg, String
"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 [String
"?", String
"h", String
"help"] Command
Help String
"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 [String
"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
$ String
"Set an option (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
optionsList String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  , [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 [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 -> Parser IState (Either String Command)
cmd_colour)
  , ([String
"consolewidth"], CmdArg
ConsoleWidthArg, String
"Set the width of the console", String -> Parser IState (Either String Command)
cmd_consolewidth)
  , ([String
"printerdepth"], CmdArg -> CmdArg
OptionalArg CmdArg
NumberArg, String
"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 [String
"q", String
"quit"] Command
Quit String
"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 [String
"version"] Command
ShowVersion String
"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 [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 -> Parser IState (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 -> 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 [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 -> Parser IState (Either String Command)
cmd_pprint)
  , ([String
"verbosity"], CmdArg
NumberArg, String
"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] -> 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 [String
"u", String
"universes"] Command
Universes String
"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 [String
"errorhandlers"] Command
ListErrorHandlers String
"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 [String
"d", String
"def"] Name -> Command
Defn String
"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 [String
"transinfo"] Name -> Command
TransformInfo String
"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 [String
"di", String
"dbginfo"] Name -> Command
DebugInfo String
"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 [String
"patt"] PTerm -> Command
Pattelab String
"(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 [String
"spec"] PTerm -> Command
Spec String
"?"
  , [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 [String
"whnf"] PTerm -> Command
WHNF String
"(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 [String
"inline"] PTerm -> Command
TestInline String
"?"
  , [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 [String
"cs", String
"casesplit"] Bool -> Int -> Name -> Command
CaseSplitAt
      String
":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 [String
"apc", String
"addproofclause"] Bool -> Int -> Name -> Command
AddProofClauseFrom
      String
":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 [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"
  , [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 [String
"am", String
"addmissing"] Bool -> Int -> Name -> Command
AddMissing
      String
":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 [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"
  , [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 [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"
  , [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 [String
"ml", String
"makelemma"] Bool -> Int -> Name -> Command
MakeLemma String
"?"
  , ([String
"log"], CmdArg
NumberArg, String
"Set logging level", String -> Parser IState (Either String Command)
cmd_log)
  , ( [String
"logcats"]
    , CmdArg -> CmdArg
ManyArgs CmdArg
NameArg
    , String
"Set logging categories"
    , String -> Parser IState (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 -> Parser IState (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 -> Parser IState (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 -> Parser IState (Either String Command)
cmd_refine)
  , ([String
"debugunify"], CmdArg -> CmdArg -> CmdArg
SeqArgs CmdArg
ExprArg CmdArg
ExprArg
    , String
"(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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a
names Command
command 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 a
names Name -> Command
command 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 a
names [String] -> Command
command 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 a
names PTerm -> Command
command 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 a
names Opt -> Command
command 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 a
names Bool -> Int -> Name -> Command
command 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
                | ([String]
names, CmdArg
_, String
_, 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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 Char
':'
              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
StateT IState (WriterT FC (Parsec Void String)) (Token String)
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
/=Char
' ') String
cmd
              Either String b
-> StateT
     IState (WriterT FC (Parsec Void String)) (Either String b)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
"Unrecognized command: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmd')

cmd :: [String] -> IP.IdrisParser String
cmd :: [String] -> IdrisParser String
cmd [String]
xs = IdrisParser String -> IdrisParser String
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 Char
':'
    [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 a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Could not parse command"
          docmd (String
x:[String]
xs) = m String -> m String
forall a. m a -> m a
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 a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
x) m String -> m String -> m String
forall a. m a -> m a -> m a
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 (\String
x String
y -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
y) (String -> Int
forall a. [a] -> 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 Command
cmd 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 PTerm -> Command
cmd 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
"Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
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) <- 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 :: forall a.
String
-> IdrisParser a
-> (a -> Command)
-> String
-> Parser IState (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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
"Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
argName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">")

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 String
"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 String
"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
"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
StateT IState (WriterT FC (Parsec Void String)) (Token String)
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 String
"module" ((String -> String) -> IdrisParser String -> IdrisParser String
forall a b.
(a -> b)
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
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 String
n = (String -> String -> String) -> [String] -> String
forall a. HasCallStack => (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
"." 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 String
"namespace" ((String -> [String]) -> IdrisParser String -> IdrisParser [String]
forall a b.
(a -> b)
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
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 String
"."

optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)
optArg :: (Opt -> Command) -> String -> Parser IState (Either String Command)
optArg Opt -> Command
cmd 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
"Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
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
          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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
"Unrecognized setting"

    Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl IdrisParser Opt -> IdrisParser Opt -> IdrisParser Opt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) IdrisParser Opt
forall a. StateT IState (WriterT FC (Parsec Void String)) a
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 (\(String
a, 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 a. a -> StateT IState (WriterT FC (Parsec Void 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 -> Parser IState (Either String Command)
proofArg Bool -> Int -> Name -> Command
cmd 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 Char
'!'
        Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"Type") HowMuchDocs
FullDocs)

    let fnName :: Parser IState (Either String Command)
fnName = (Name -> Command)
-> String -> Parser IState (Either String Command)
fnNameArg (\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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
name = do
    ConsoleWidth
w <- IdrisParser ConsoleWidth
pConsoleWidth
    Either String Command -> Parser IState (Either String Command)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"auto"); ConsoleWidth -> IdrisParser ConsoleWidth
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ConsoleWidth
AutomaticWidth
                    IdrisParser ConsoleWidth
-> IdrisParser ConsoleWidth -> IdrisParser ConsoleWidth
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"infinite"); ConsoleWidth -> IdrisParser ConsoleWidth
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ConsoleWidth
InfinitelyWide
                    IdrisParser ConsoleWidth
-> IdrisParser ConsoleWidth -> IdrisParser ConsoleWidth
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
_ = 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"(repl)") [] (Name -> [String] -> Name
sNS (String -> Name
sUN String
"main") [String
"Main"])

cmd_dynamic :: String -> IP.IdrisParser (Either String Command)
cmd_dynamic :: String -> Parser IState (Either String Command)
cmd_dynamic 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
StateT IState (WriterT FC (Parsec Void String)) (Token String)
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
/= String
"")
                        then Either a Command
-> StateT
     IState (WriterT FC (Parsec Void String)) (Either a Command)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
$ String
"Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" [<library>]"
    Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"html") StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser OutputFmt -> IdrisParser OutputFmt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputFmt -> IdrisParser OutputFmt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return OutputFmt
HTMLOutput)
               IdrisParser OutputFmt
-> IdrisParser OutputFmt -> IdrisParser OutputFmt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"latex") StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser OutputFmt -> IdrisParser OutputFmt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> OutputFmt -> IdrisParser OutputFmt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 = 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
"bytecode") StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser Codegen -> IdrisParser Codegen
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Codegen -> IdrisParser Codegen
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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
$ String
"Usage is :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" [<codegen>] <filename>"
    Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
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
$ String
"Category: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) [LogCat]
forall a. StateT IState (WriterT FC (Parsec Void String)) a
badCat

cmd_let :: String -> IP.IdrisParser (Either String Command)
cmd_let :: String -> Parser IState (Either String Command)
cmd_let 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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 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
StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle
    Either String Command -> Parser IState (Either String Command)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String
name = (Command -> Either String Command)
-> StateT IState (WriterT FC (Parsec Void String)) Command
-> Parser IState (Either String Command)
forall a b.
(a -> b)
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
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 = [ (String
"black", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Black)
                  , (String
"red", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Red)
                  , (String
"green", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Green)
                  , (String
"yellow", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Yellow)
                  , (String
"blue", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Blue)
                  , (String
"magenta", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Magenta)
                  , (String
"cyan", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
Cyan)
                  , (String
"white", Color -> Maybe Color
forall a. a -> Maybe a
Just Color
White)
                  , (String
"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 a b. (a -> b -> b) -> b -> [a] -> b
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT IState (WriterT FC (Parsec Void String)) Command
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT IState (WriterT FC (Parsec Void String)) Command
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Unknown colour"
                  doColour ((String
s, a
c):[(String, a)]
cs) = (m () -> m ()
forall a. m a -> m a
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 a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
c) m a -> m a -> m a
forall a. 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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 String
"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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> (a -> StateT IState (WriterT FC (Parsec Void String)) b)
-> StateT IState (WriterT FC (Parsec Void String)) b
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 IdrisColour
i       = IdrisColour
i { vivid = True }
                  doDull :: IdrisColour -> IdrisColour
doDull IdrisColour
i        = IdrisColour
i { vivid = False }
                  doUnderline :: IdrisColour -> IdrisColour
doUnderline IdrisColour
i   = IdrisColour
i { underline = True }
                  doNoUnderline :: IdrisColour -> IdrisColour
doNoUnderline IdrisColour
i = IdrisColour
i { underline = False }
                  doBold :: IdrisColour -> IdrisColour
doBold IdrisColour
i        = IdrisColour
i { bold = True }
                  doNoBold :: IdrisColour -> IdrisColour
doNoBold IdrisColour
i      = IdrisColour
i { bold = False }
                  doItalic :: IdrisColour -> IdrisColour
doItalic IdrisColour
i      = IdrisColour
i { italic = True }
                  doNoItalic :: IdrisColour -> IdrisColour
doNoItalic IdrisColour
i    = IdrisColour
i { italic = False }
                  doSetColour :: Maybe Color -> IdrisColour -> IdrisColour
doSetColour Maybe Color
c IdrisColour
i = IdrisColour
i { colour = c }

        -- | Generate the colour type names using the default Show instance.
        colourTypes :: [(String, ColourType)]
        colourTypes :: [(String, ColourType)]
colourTypes = (ColourType -> (String, ColourType))
-> [ColourType] -> [(String, ColourType)]
forall a b. (a -> b) -> [a] -> [b]
map (\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 Int
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 a. 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
$ String
"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])
-> ([(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 ((String
s,a
ct):[(String, a)]
cts) = (m () -> m ()
forall a. m a -> m a
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 a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
ct) m a -> m a -> m a
forall a. 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 ([Char
'a'..Char
'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'_'])

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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
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 :: forall a.
IdrisParser a
-> ([PkgName] -> a -> Command)
-> String
-> Parser IState (Either String Command)
packageBasedCmd IdrisParser a
valParser [PkgName] -> a -> Command
cmd String
name =
  Parser IState (Either String Command)
-> Parser IState (Either String Command)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 Char
'('
            [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 a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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
',')
            Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
IP.lchar Char
')'
            a
val <- IdrisParser a
valParser
            Either String Command -> Parser IState (Either String Command)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail PkgName -> StateT IState (WriterT FC (Parsec Void String)) PkgName
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 = True })) [PkgName] -> PTerm -> Command
Search

cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)
cmd_proofsearch :: String -> Parser IState (Either String Command)
cmd_proofsearch 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 a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
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 Char
'!')
    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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 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 Char
'!'; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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]))