@@ -23,205 +23,382 @@ import Data.List.Split(splitOn)
2323import Data.Char(toLower)
2424import qualified Data.ByteString.UTF8 as UTF8
2525
26−parseCmd :: IState -> String -> String -> Result Command
26+parseCmd :: IState -> String -> String -> Result (Either String Command)
2727parseCmd i inputname = P.runparser pCmd i inputname
2828
29−cmd :: [String] -> P.IdrisParser ()
30−cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs))
31− where docmd [] = fail "No such command"
32− docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs
33−
34−pCmd :: P.IdrisParser Command
35−
36−pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit
37− <|> do cmd ["h", "?", "help"]; eof; return Help
38− <|> do cmd ["w", "warranty"]; eof; return Warranty
39− <|> do cmd ["r", "reload"]; eof; return Reload
40− <|> do cmd ["module"]; f <- P.identifier; eof;
41− return (ModImport (toPath f))
42− <|> do cmd ["e", "edit"]; eof; return Edit
43− <|> do cmd ["exec", "execute"]; eof; return Execute
44− <|> try (do cmd ["c", "compile"]
45− i <- get
46− f <- P.identifier
47− eof
48− return (Compile (Via "c") f))
49− <|> do cmd ["c", "compile"]
50− i <- get
51− c <- codegenOption
52− f <- P.identifier
53− eof
54− return (Compile c f)
55− <|> do cmd ["proofs"]; eof; return Proofs
56− <|> do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n)
57− <|> do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n)
58− <|> do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i))
59− <|> do cmd ["let"]
60− defn <- concat <$> many (P.decl defaultSyntax)
61− return (NewDefn defn)
62− <|> do cmd ["unlet","undefine"]
63− Undefine `fmap` many P.name
64− <|> do cmd ["lto", "loadto"];
65− toline <- P.natural
66− f <- many anyChar;
67− return (Load f (Just (fromInteger toline)))
68− <|> do cmd ["l", "load"]; f <- many anyChar;
69− return (Load f Nothing)
70− <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)
71− <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)
72− <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)
73− <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)
74− <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))
75− <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))
76− <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)
77− <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)
78− <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)
79− <|> do cmd ["u", "universes"]; eof; return Universes
80− <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)
81− <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)
82− <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
83− <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)
84− <|> do cmd ["color", "colour"]; pSetColourCmd
85− <|> do cmd ["set"]; o <- pOption; return (SetOpt o)
86− <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)
87− <|> do cmd ["s", "search"]; P.whiteSpace;
88− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)
89− <|> do cmd ["cs", "casesplit"]; P.whiteSpace;
90− upd <- option False (do P.lchar '!'; return True)
91− l <- P.natural; n <- P.name;
92− return (CaseSplitAt upd (fromInteger l) n)
93− <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;
94− upd <- option False (do P.lchar '!'; return True)
95− l <- P.natural; n <- P.name;
96− return (AddProofClauseFrom upd (fromInteger l) n)
97− <|> do cmd ["ac", "addclause"]; P.whiteSpace;
98− upd <- option False (do P.lchar '!'; return True)
99− l <- P.natural; n <- P.name;
100− return (AddClauseFrom upd (fromInteger l) n)
101− <|> do cmd ["am", "addmissing"]; P.whiteSpace;
102− upd <- option False (do P.lchar '!'; return True)
103− l <- P.natural; n <- P.name;
104− return (AddMissing upd (fromInteger l) n)
105− <|> do cmd ["mw", "makewith"]; P.whiteSpace;
106− upd <- option False (do P.lchar '!'; return True)
107− l <- P.natural; n <- P.name;
108− return (MakeWith upd (fromInteger l) n)
109− <|> do cmd ["ml", "makelemma"]; P.whiteSpace;
110− upd <- option False (do P.lchar '!'; return True)
111− l <- P.natural; n <- P.name;
112− return (MakeLemma upd (fromInteger l) n)
113− <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;
114− upd <- option False (do P.lchar '!'; return True)
115− l <- P.natural; n <- P.name;
116− hints <- many P.fnName
117− return (DoProofSearch upd True (fromInteger l) n hints)
118− <|> do cmd ["ref", "refine"]; P.whiteSpace;
119− upd <- option False (do P.lchar '!'; return True)
120− l <- P.natural; n <- P.name;
121− hint <- P.fnName
122− return (DoProofSearch upd False (fromInteger l) n [hint])
123− <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)
124− <|> do cmd ["m", "metavars"]; eof; return Metavars
125− <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;
126− return (Just x))
127− eof; return (AddProof n)
128− <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)
129− <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)
130− <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers
131− <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)
132− <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)
133− <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)
134− <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)
135− <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)
136− <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (PrintDef n)
137− <|> do cmd ["pp", "pprint"]
138− P.whiteSpace
139− fmt <- ppFormat
140− P.whiteSpace
141− n <- fmap fromInteger P.natural
142− P.whiteSpace
143− t <- P.fullExpr defaultSyntax
144− return (PPrint fmt n t)
145− <|> do P.whiteSpace; do eof; return NOP
146− <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
147−
148− where toPath n = foldl1' (</>) $ splitOn "." n
149−
150−pOption :: P.IdrisParser Opt
151−pOption = do discard (P.symbol "errorcontext"); return ErrContext
152− <|> do discard (P.symbol "showimplicits"); return ShowImpl
153− <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
154− <|> do discard (P.symbol "autosolve"); return AutoSolve
155− <|> do discard (P.symbol "nobanner") ; return NoBanner
156− <|> do discard (P.symbol "warnreach"); return WarnReach
157−
158−codegenOption :: P.IdrisParser Codegen
159−codegenOption = do discard (P.symbol "bytecode"); return Bytecode
160− <|> do x <- P.identifier
161− return (Via (map toLower x))
162−
163−pConsoleWidth :: P.IdrisParser ConsoleWidth
164−pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
165− <|> do discard (P.symbol "infinite"); return InfinitelyWide
166− <|> do n <- fmap fromInteger P.natural; return (ColsWide n)
167−
168−ppFormat :: P.IdrisParser OutputFmt
169−ppFormat = (discard (P.symbol "html") >> return HTMLOutput)
170− <|> (discard (P.symbol "latex") >> return LaTeXOutput)
171−
172−colours :: [(String, Maybe Color)]
173−colours = [ ("black", Just Black)
174− , ("red", Just Red)
175− , ("green", Just Green)
176− , ("yellow", Just Yellow)
177− , ("blue", Just Blue)
178− , ("magenta", Just Magenta)
179− , ("cyan", Just Cyan)
180− , ("white", Just White)
181− , ("default", Nothing)
182− ]
183−
184−pColour :: P.IdrisParser (Maybe Color)
185−pColour = doColour colours
186− where doColour [] = fail "Unknown colour"
187− doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs
188−
189−pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)
190−pColourMod = try (P.symbol "vivid" >> return doVivid)
191− <|> try (P.symbol "dull" >> return doDull)
192− <|> try (P.symbol "underline" >> return doUnderline)
193− <|> try (P.symbol "nounderline" >> return doNoUnderline)
194− <|> try (P.symbol "bold" >> return doBold)
195− <|> try (P.symbol "nobold" >> return doNoBold)
196− <|> try (P.symbol "italic" >> return doItalic)
197− <|> try (P.symbol "noitalic" >> return doNoItalic)
198− <|> try (pColour >>= return . doSetColour)
199− where doVivid i = i { vivid = True }
200− doDull i = i { vivid = False }
201− doUnderline i = i { underline = True }
202− doNoUnderline i = i { underline = False }
203− doBold i = i { bold = True }
204− doNoBold i = i { bold = False }
205− doItalic i = i { italic = True }
206− doNoItalic i = i { italic = False }
207− doSetColour c i = i { colour = c }
208−
209−-- | Generate the colour type names using the default Show instance.
210−colourTypes :: [(String, ColourType)]
211−colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
212− enumFromTo minBound maxBound
213−
214−pColourType :: P.IdrisParser ColourType
215−pColourType = doColourType colourTypes
216− where doColourType [] = fail $ "Unknown colour category. Options: " ++
217− (concat . intersperse ", " . map fst) colourTypes
218− doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts
219−
220−pSetColourCmd :: P.IdrisParser Command
221−pSetColourCmd = (do c <- pColourType
222− let defaultColour = IdrisColour Nothing True False False False
223− opts <- sepBy pColourMod (P.whiteSpace)
224− let colour = foldr ($) defaultColour $ reverse opts
225− return $ SetColour c colour)
226− <|> try (P.symbol "on" >> return ColourOn)
227− <|> try (P.symbol "off" >> return ColourOff)
29+pCmd :: P.IdrisParser (Either String Command)
30+pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit
31+ <|> do c <- cmd ["h", "?", "help"]; noArgs c Help
32+ <|> do c <- cmd ["w", "warranty"]; noArgs c Warranty
33+ <|> do c <- cmd ["r", "reload"]; noArgs c Reload
34+ <|> do c <- cmd ["exec", "execute"]; noArgs c Execute
35+ <|> do c <- cmd ["proofs"]; noArgs c Proofs
36+ <|> do c <- cmd ["u", "universes"]; noArgs c Universes
37+ <|> do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers
38+ <|> do c <- cmd ["m", "metavars"]; noArgs c Metavars
39+ <|> do c <- cmd ["e", "edit"]; noArgs c Edit
40+
41+ <|> do c <- cmd ["d", "def"]; fnNameArg c Defn
42+ <|> do c <- cmd ["total"]; fnNameArg c TotCheck
43+ <|> do c <- cmd ["printdef"]; fnNameArg c PrintDef
44+ <|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls
45+ <|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho
46+ <|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo
47+ <|> do c <- cmd ["miss", "missing"]; fnNameArg c Missing
48+
49+ <|> do c <- cmd ["t", "type"]; exprArg c Check
50+ <|> do c <- cmd ["x"]; exprArg c ExecVal
51+ <|> do c <- cmd ["patt"]; exprArg c Pattelab
52+ <|> do c <- cmd ["spec"]; exprArg c Spec
53+ <|> do c <- cmd ["hnf"]; exprArg c HNF
54+ <|> do c <- cmd ["inline"]; exprArg c TestInline
55+
56+ <|> do c <- cmd ["rmproof"]; nameArg c RmProof
57+ <|> do c <- cmd ["showproof"]; nameArg c ShowProof
58+ <|> do c <- cmd ["p", "prove"]; nameArg c Prove
59+
60+ <|> do c <- cmd ["set"]; optArg c SetOpt
61+ <|> do c <- cmd ["unset"]; optArg c UnsetOpt
62+
63+ <|> do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)
64+ <|> do c <- cmd ["cd"]; strArg c ChangeDirectory
65+ <|> do c <- cmd ["apropos"]; strArg c Apropos
66+ <|> do c <- cmd ["mkdoc"]; strArg c MakeDoc
67+
68+ <|> do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt
69+ <|> do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom
70+ <|> do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom
71+ <|> do c <- cmd ["am", "addmissing"]; proofArg c AddMissing
72+ <|> do c <- cmd ["mw", "makewith"]; proofArg c MakeWith
73+ <|> do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma
74+
75+ <|> do c <- cmd ["pp", "pprint"]; cmd_pprint c
76+ <|> do c <- cmd ["doc"]; cmd_doc c
77+ <|> do c <- cmd ["dynamic"]; cmd_dynamic c
78+ <|> do c <- cmd ["consolewidth"]; cmd_consolewidth c
79+ <|> do c <- cmd ["module"]; cmd_module c
80+ <|> do c <- cmd ["c", "compile"]; cmd_compile c
81+ <|> do c <- cmd ["a", "addproof"]; cmd_addproof c
82+ <|> do c <- cmd ["log"]; cmd_log c
83+ <|> do c <- cmd ["let"]; cmd_let c
84+ <|> do c <- cmd ["unlet","undefine"]; cmd_unlet c
85+ <|> do c <- cmd ["lto", "loadto"]; cmd_loadto c
86+ <|> do c <- cmd ["color", "colour"]; cmd_colour c
87+ <|> do c <- cmd ["s", "search"]; cmd_search c
88+ <|> do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c
89+ <|> do c <- cmd ["ref", "refine"]; cmd_refine c
90+
91+ <|> unrecognized
92+ <|> nop
93+ <|> eval
94+
95+ where nop = do P.whiteSpace; eof; return (Right NOP)
96+ eval = exprArg "" Eval
97+ unrecognized = do
98+ P.lchar ':'
99+ cmd <- many anyChar
100+ let cmd' = takeWhile (/=' ') cmd
101+ return (Left $ "Unrecognized command: " ++ cmd')
102+
103+cmd :: [String] -> P.IdrisParser String
104+cmd xs = try $ do
105+ P.lchar ':'
106+ docmd sorted_xs
107+
108+ where docmd [] = fail "Could not parse command"
109+ docmd (x:xs) = try (P.reserved x >> return x) <|> docmd xs
110+
111+ sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs
112+
113+
114+noArgs :: String -> Command -> P.IdrisParser (Either String Command)
115+noArgs name cmd = do
116+ let emptyArgs = do
117+ P.whiteSpace
118+ eof
119+ return (Right cmd)
120+
121+ let failure = return (Left $ ":" ++ name ++ " takes no arguments")
122+
123+ try emptyArgs <|> failure
124+
125+exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)
126+exprArg name cmd = do
127+ P.whiteSpace
128+ let noArg = do
129+ eof
130+ return $ Left ("Usage is :" ++ name ++ " <expression>")
131+
132+ let properArg = do
133+ t <- P.fullExpr defaultSyntax
134+ return $ Right (cmd t)
135+ try noArg <|> properArg
136+
137+
138+fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
139+fnNameArg name cmd = do
140+ P.whiteSpace
141+ let emptyArgs = do eof
142+ return $ Left ("Usage is :" ++ name ++ " <functionname>")
143+ oneArg = do n <- P.fnName
144+ eof
145+ return (Right (cmd n))
146+ badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
147+ try emptyArgs <|> try oneArg <|> badArg
148+
149+nameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
150+nameArg name cmd = do
151+ P.whiteSpace
152+ let emptyArgs = do eof
153+ return $ Left ("Usage is :" ++ name ++ " <functionname>")
154+ oneArg = do n <- P.name
155+ eof
156+ return (Right (cmd n))
157+ badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
158+ try emptyArgs <|> try oneArg <|> badArg
159+
160+strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)
161+strArg name cmd = do
162+ n <- many anyChar
163+ eof
164+ return (Right (cmd n))
165+
166+optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)
167+optArg name cmd = do
168+ let emptyArgs = do
169+ eof
170+ return $ Left ("Usage is :" ++ name ++ " <option>")
171+
172+ let oneArg = do
173+ P.whiteSpace
174+ o <- pOption
175+ P.whiteSpace
176+ eof
177+ return (Right (cmd o))
178+
179+ let failure = do
180+ return $ Left "Unrecognized setting"
181+
182+ try emptyArgs <|> try oneArg <|> failure
183+
184+ where
185+ pOption :: P.IdrisParser Opt
186+ pOption = do discard (P.symbol "errorcontext"); return ErrContext
187+ <|> do discard (P.symbol "showimplicits"); return ShowImpl
188+ <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
189+ <|> do discard (P.symbol "autosolve"); return AutoSolve
190+ <|> do discard (P.symbol "nobanner") ; return NoBanner
191+ <|> do discard (P.symbol "warnreach"); return WarnReach
192+
193+proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)
194+proofArg name cmd = do
195+ P.whiteSpace
196+ upd <- option False $ do
197+ P.lchar '!'
198+ return True
199+ l <- P.natural
200+ n <- P.name;
201+ return (Right (cmd upd (fromInteger l) n))
202+
203+cmd_doc :: String -> P.IdrisParser (Either String Command)
204+cmd_doc name = do
205+ let constant = do
206+ c <- P.constant
207+ eof
208+ return $ Right (DocStr (Right c))
209+
210+ let bottom = do
211+ P.string "_|_"
212+ eof
213+ return $ Right (DocStr (Left falseTy))
214+
215+ let fnName = fnNameArg name (\n -> DocStr (Left n))
216+
217+ try constant <|> try bottom <|> fnName
218+
219+cmd_consolewidth :: String -> P.IdrisParser (Either String Command)
220+cmd_consolewidth name = do
221+ w <- pConsoleWidth
222+ return (Right (SetConsoleWidth w))
223+
224+ where
225+ pConsoleWidth :: P.IdrisParser ConsoleWidth
226+ pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
227+ <|> do discard (P.symbol "infinite"); return InfinitelyWide
228+ <|> do n <- fmap fromInteger P.natural; return (ColsWide n)
229+
230+cmd_dynamic :: String -> P.IdrisParser (Either String Command)
231+cmd_dynamic name = do
232+ let emptyArgs = noArgs name ListDynamic
233+
234+ let oneArg = do l <- many anyChar
235+ return $ Right (DynamicLink l)
236+
237+ let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"
238+
239+ try emptyArgs <|> try oneArg <|> failure
240+
241+cmd_pprint :: String -> P.IdrisParser (Either String Command)
242+cmd_pprint name = do
243+ P.whiteSpace
244+ fmt <- ppFormat
245+ P.whiteSpace
246+ n <- fmap fromInteger P.natural
247+ P.whiteSpace
248+ t <- P.fullExpr defaultSyntax
249+ return (Right (PPrint fmt n t))
250+
251+ where
252+ ppFormat :: P.IdrisParser OutputFmt
253+ ppFormat = (discard (P.symbol "html") >> return HTMLOutput)
254+ <|> (discard (P.symbol "latex") >> return LaTeXOutput)
255+
256+
257+cmd_module :: String -> P.IdrisParser (Either String Command)
258+cmd_module name = do
259+ f <- P.identifier
260+ eof;
261+ return (Right (ModImport (toPath f)))
262+ where
263+ toPath n = foldl1' (</>) $ splitOn "." n
264+
265+cmd_compile :: String -> P.IdrisParser (Either String Command)
266+cmd_compile name = do
267+ let defaultCodegen = Via "c"
268+
269+ let codegenOption :: P.IdrisParser Codegen
270+ codegenOption = do
271+ let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
272+ viaCodegen = do x <- P.identifier
273+ return (Via (map toLower x))
274+ bytecodeCodegen <|> viaCodegen
275+
276+ let hasOneArg = do
277+ i <- get
278+ f <- P.identifier
279+ eof
280+ return $ Right (Compile defaultCodegen f)
281+
282+ let hasTwoArgs = do
283+ i <- get
284+ codegen <- codegenOption
285+ f <- P.identifier
286+ eof
287+ return $ Right (Compile codegen f)
288+
289+ let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"
290+ try hasTwoArgs <|> try hasOneArg <|> failure
291+
292+cmd_addproof :: String -> P.IdrisParser (Either String Command)
293+cmd_addproof name = do
294+ n <- option Nothing $ do
295+ x <- P.name;
296+ return (Just x)
297+ eof
298+ return (Right (AddProof n))
299+
300+cmd_log :: String -> P.IdrisParser (Either String Command)
301+cmd_log name = do
302+ i <- P.natural
303+ eof
304+ return (Right (LogLvl (fromIntegral i)))
305+
306+cmd_let :: String -> P.IdrisParser (Either String Command)
307+cmd_let name = do
308+ defn <- concat <$> many (P.decl defaultSyntax)
309+ return (Right (NewDefn defn))
310+
311+cmd_unlet :: String -> P.IdrisParser (Either String Command)
312+cmd_unlet name = do
313+ (Right . Undefine) `fmap` many P.name
314+
315+cmd_loadto :: String -> P.IdrisParser (Either String Command)
316+cmd_loadto name = do
317+ toline <- P.natural
318+ f <- many anyChar;
319+ return (Right (Load f (Just (fromInteger toline))))
320+
321+cmd_colour :: String -> P.IdrisParser (Either String Command)
322+cmd_colour name = do
323+ pSetColourCmd >>= return . Right
324+
325+ where
326+ colours :: [(String, Maybe Color)]
327+ colours = [ ("black", Just Black)
328+ , ("red", Just Red)
329+ , ("green", Just Green)
330+ , ("yellow", Just Yellow)
331+ , ("blue", Just Blue)
332+ , ("magenta", Just Magenta)
333+ , ("cyan", Just Cyan)
334+ , ("white", Just White)
335+ , ("default", Nothing)
336+ ]
337+
338+ pSetColourCmd :: P.IdrisParser Command
339+ pSetColourCmd = (do c <- pColourType
340+ let defaultColour = IdrisColour Nothing True False False False
341+ opts <- sepBy pColourMod (P.whiteSpace)
342+ let colour = foldr ($) defaultColour $ reverse opts
343+ return $ SetColour c colour)
344+ <|> try (P.symbol "on" >> return ColourOn)
345+ <|> try (P.symbol "off" >> return ColourOff)
346+
347+ pColour :: P.IdrisParser (Maybe Color)
348+ pColour = doColour colours
349+ where doColour [] = fail "Unknown colour"
350+ doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs
351+
352+ pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)
353+ pColourMod = try (P.symbol "vivid" >> return doVivid)
354+ <|> try (P.symbol "dull" >> return doDull)
355+ <|> try (P.symbol "underline" >> return doUnderline)
356+ <|> try (P.symbol "nounderline" >> return doNoUnderline)
357+ <|> try (P.symbol "bold" >> return doBold)
358+ <|> try (P.symbol "nobold" >> return doNoBold)
359+ <|> try (P.symbol "italic" >> return doItalic)
360+ <|> try (P.symbol "noitalic" >> return doNoItalic)
361+ <|> try (pColour >>= return . doSetColour)
362+ where doVivid i = i { vivid = True }
363+ doDull i = i { vivid = False }
364+ doUnderline i = i { underline = True }
365+ doNoUnderline i = i { underline = False }
366+ doBold i = i { bold = True }
367+ doNoBold i = i { bold = False }
368+ doItalic i = i { italic = True }
369+ doNoItalic i = i { italic = False }
370+ doSetColour c i = i { colour = c }
371+
372+ -- | Generate the colour type names using the default Show instance.
373+ colourTypes :: [(String, ColourType)]
374+ colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
375+ enumFromTo minBound maxBound
376+
377+ pColourType :: P.IdrisParser ColourType
378+ pColourType = doColourType colourTypes
379+ where doColourType [] = fail $ "Unknown colour category. Options: " ++
380+ (concat . intersperse ", " . map fst) colourTypes
381+ doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts
382+
383+
384+cmd_search :: String -> P.IdrisParser (Either String Command)
385+cmd_search name = do
386+ P.whiteSpace;
387+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True })
388+ return (Right (Search t))
389+
390+cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
391+cmd_proofsearch name = do
392+ P.whiteSpace
393+ upd <- option False (do P.lchar '!'; return True)
394+ l <- P.natural; n <- P.name;
395+ hints <- many P.fnName
396+ return (Right (DoProofSearch upd True (fromInteger l) n hints))
397+
398+cmd_refine :: String -> P.IdrisParser (Either String Command)
399+cmd_refine name = do
400+ P.whiteSpace
401+ upd <- option False (do P.lchar '!'; return True)
402+ l <- P.natural; n <- P.name;
403+ hint <- P.fnName
404+ return (Right (DoProofSearch upd False (fromInteger l) n [hint]))