8fc9ffd · Idris-dev · git.iko.soy

26parseCmd :: IState -> String -> String -> Result (Either String Command)

27parseCmd i inputname = P.runparser pCmd i inputname

28

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−

34pCmd :: P.IdrisParser (Either String Command)

29pCmd :: P.IdrisParser (Either String Command)

35−pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return (Right Quit)

30+pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit

36− <|> do cmd ["h", "?", "help"]; eof; return (Right Help)

31+ <|> do c <- cmd ["h", "?", "help"]; noArgs c Help

37− <|> do cmd ["w", "warranty"]; eof; return (Right Warranty)

32+ <|> do c <- cmd ["w", "warranty"]; noArgs c Warranty

38− <|> do cmd ["r", "reload"]; eof; return (Right Reload)

33+ <|> do c <- cmd ["r", "reload"]; noArgs c Reload

39− <|> do cmd ["module"]; f <- P.identifier; eof;

34+ <|> do c <- cmd ["exec", "execute"]; noArgs c Execute

40− return (Right (ModImport (toPath f)))

41− <|> do cmd ["e", "edit"]; eof; return (Right Edit)

42− <|> do cmd ["exec", "execute"]; ((try $ eof >> return (Right Execute)) <|> return (Left "exec(ute) does not take any parameters"))

43− <|> try (do cmd ["c", "compile"]

44− i <- get

45− f <- P.identifier

46− eof

47− return (Right (Compile (Via "c") f)))

48− <|> do cmd ["c", "compile"]

49− i <- get

50− c <- codegenOption

51− f <- P.identifier

52− eof

53− return (Right (Compile c f))

54− <|> do cmd ["proofs"]; eof; return (Right Proofs)

35+ <|> do c <- cmd ["proofs"]; noArgs c Proofs

55− <|> do cmd ["rmproof"]; n <- P.name; eof; return (Right (RmProof n))

36+ <|> do c <- cmd ["u", "universes"]; noArgs c Universes

56− <|> do cmd ["showproof"]; n <- P.name; eof; return (Right (ShowProof n))

37+ <|> do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers

57− <|> do cmd ["log"]; i <- P.natural; eof; return (Right (LogLvl (fromIntegral i)))

38+ <|> do c <- cmd ["m", "metavars"]; noArgs c Metavars

58− <|> do cmd ["let"]

39+ <|> do c <- cmd ["e", "edit"]; noArgs c Edit

59− defn <- concat <$> many (P.decl defaultSyntax)

40+

60− return (Right (NewDefn defn))

41+ <|> do c <- cmd ["d", "def"]; fnNameArg c Defn

61− <|> do cmd ["unlet","undefine"]

62− (Right . Undefine) `fmap` many P.name

63− <|> do cmd ["lto", "loadto"];

64− toline <- P.natural

65− f <- many anyChar;

66− return (Right (Load f (Just (fromInteger toline))))

67− <|> do cmd ["l", "load"]; f <- many anyChar;

68− return (Right (Load f Nothing))

69− <|> do cmd ["cd"]; f <- many anyChar; return (Right (ChangeDirectory f))

70− <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Spec t))

71− <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (HNF t))

72− <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (TestInline t))

73− <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (Right (DocStr (Right c)))

74− <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (Right (DocStr (Left n)))

75− <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Right (Defn n))

76− <|> do cmd ["total"]; do n <- P.fnName; eof; return (Right (TotCheck n))

42+ <|> do c <- cmd ["total"]; fnNameArg c TotCheck

77− <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Check t))

43+ <|> do c <- cmd ["printdef"]; fnNameArg c PrintDef

78− <|> do cmd ["u", "universes"]; eof; return (Right Universes)

44+ <|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls

45+ <|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho

79− <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (Right (DebugInfo n))

46+ <|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo

80− <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Right (Missing n))

47+ <|> do c <- cmd ["miss", "missing"]; fnNameArg c Missing

81− <|> try (do cmd ["dynamic"]; eof; return (Right ListDynamic))

48+

82− <|> do cmd ["dynamic"]; l <- many anyChar; return (Right (DynamicLink l))

49+ <|> do c <- cmd ["t", "type"]; exprArg c Check

83− <|> do cmd ["color", "colour"]; pSetColourCmd >>= return . Right

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+

84− <|> do cmd ["set"]; o <- pOption; return (Right (SetOpt o))

60+ <|> do c <- cmd ["set"]; optArg c SetOpt

85− <|> do cmd ["unset"]; o <- pOption; return (Right (UnsetOpt o))

61+ <|> do c <- cmd ["unset"]; optArg c UnsetOpt

86− <|> do cmd ["s", "search"]; P.whiteSpace;

62+

87− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Right (Search t))

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+

88− <|> do cmd ["cs", "casesplit"]; P.whiteSpace;

68+ <|> do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt

89− upd <- option False (do P.lchar '!'; return True)

90− l <- P.natural; n <- P.name;

91− return (Right (CaseSplitAt upd (fromInteger l) n))

92− <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;

69+ <|> do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom

93− upd <- option False (do P.lchar '!'; return True)

94− l <- P.natural; n <- P.name;

95− return (Right (AddProofClauseFrom upd (fromInteger l) n))

96− <|> do cmd ["ac", "addclause"]; P.whiteSpace;

70+ <|> do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom

97− upd <- option False (do P.lchar '!'; return True)

98− l <- P.natural; n <- P.name;

99− return (Right (AddClauseFrom upd (fromInteger l) n))

100− <|> do cmd ["am", "addmissing"]; P.whiteSpace;

71+ <|> do c <- cmd ["am", "addmissing"]; proofArg c AddMissing

101− upd <- option False (do P.lchar '!'; return True)

102− l <- P.natural; n <- P.name;

103− return (Right (AddMissing upd (fromInteger l) n))

104− <|> do cmd ["mw", "makewith"]; P.whiteSpace;

72+ <|> do c <- cmd ["mw", "makewith"]; proofArg c MakeWith

105− upd <- option False (do P.lchar '!'; return True)

106− l <- P.natural; n <- P.name;

107− return (Right (MakeWith upd (fromInteger l) n))

108− <|> do cmd ["ml", "makelemma"]; P.whiteSpace;

73+ <|> do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma

109− upd <- option False (do P.lchar '!'; return True)

74+

110− l <- P.natural; n <- P.name;

75+ <|> do c <- cmd ["pp", "pprint"]; cmd_pprint c

111− return (Right (MakeLemma upd (fromInteger l) n))

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

112− <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;

88+ <|> do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c

113− upd <- option False (do P.lchar '!'; return True)

114− l <- P.natural; n <- P.name;

115− hints <- many P.fnName

116− return (Right (DoProofSearch upd True (fromInteger l) n hints))

117− <|> do cmd ["ref", "refine"]; P.whiteSpace;

89+ <|> do c <- cmd ["ref", "refine"]; cmd_refine c

118− upd <- option False (do P.lchar '!'; return True)

90+

119− l <- P.natural; n <- P.name;

91+ <|> unrecognized

120− hint <- P.fnName

92+ <|> nop

121− return (Right (DoProofSearch upd False (fromInteger l) n [hint]))

93+ <|> eval

122− <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Right (Prove n))

94+

123− <|> do cmd ["m", "metavars"]; eof; return (Right Metavars)

124− <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

125− return (Just x))

126− eof; return (Right (AddProof n))

127− <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (ExecVal t))

128− <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Pattelab t))

129− <|> do cmd ["errorhandlers"]; eof ; return (Right ListErrorHandlers)

130− <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (Right (SetConsoleWidth w))

131− <|> do cmd ["apropos"]; str <- many anyChar ; return (Right (Apropos str))

132− <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (Right (WhoCalls n))

133− <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (Right (CallsWho n))

134− <|> do cmd ["mkdoc"]; str <- many anyChar; return (Right (MakeDoc str))

135− <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (Right (PrintDef n))

136− <|> do cmd ["pp", "pprint"]

137− P.whiteSpace

138− fmt <- ppFormat

139− P.whiteSpace

140− n <- fmap fromInteger P.natural

141− P.whiteSpace

142− t <- P.fullExpr defaultSyntax

143− return (Right (PPrint fmt n t))

144− <|> do P.whiteSpace; do eof; return (Right NOP)

95+ where nop = do P.whiteSpace; eof; return (Right NOP)

145− <|> do t <- P.fullExpr defaultSyntax; return (Right (Eval t))

96+ eval = exprArg "" Eval

146−

97+ unrecognized = do

147− where toPath n = foldl1' (</>) $ splitOn "." n

98+ P.lchar ':'

148−

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

149−pOption :: P.IdrisParser Opt

185+ pOption :: P.IdrisParser Opt

150−pOption = do discard (P.symbol "errorcontext"); return ErrContext

186+ pOption = do discard (P.symbol "errorcontext"); return ErrContext

151− <|> do discard (P.symbol "showimplicits"); return ShowImpl

187+ <|> do discard (P.symbol "showimplicits"); return ShowImpl

152− <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

188+ <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

153− <|> do discard (P.symbol "autosolve"); return AutoSolve

189+ <|> do discard (P.symbol "autosolve"); return AutoSolve

154− <|> do discard (P.symbol "nobanner") ; return NoBanner

190+ <|> do discard (P.symbol "nobanner") ; return NoBanner

155− <|> do discard (P.symbol "warnreach"); return WarnReach

191+ <|> do discard (P.symbol "warnreach"); return WarnReach

156−

192+

157−codegenOption :: P.IdrisParser Codegen

193+proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)

158−codegenOption = do discard (P.symbol "bytecode"); return Bytecode

194+proofArg name cmd = do

159− <|> do x <- P.identifier

195+ P.whiteSpace

160− return (Via (map toLower x))

196+ upd <- option False $ do

161−

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

162−pConsoleWidth :: P.IdrisParser ConsoleWidth

225+ pConsoleWidth :: P.IdrisParser ConsoleWidth

163−pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

226+ pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

164− <|> do discard (P.symbol "infinite"); return InfinitelyWide

227+ <|> do discard (P.symbol "infinite"); return InfinitelyWide

165− <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

228+ <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

166−

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

167−ppFormat :: P.IdrisParser OutputFmt

252+ ppFormat :: P.IdrisParser OutputFmt

168−ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

253+ ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

169− <|> (discard (P.symbol "latex") >> return LaTeXOutput)

254+ <|> (discard (P.symbol "latex") >> return LaTeXOutput)

170−

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

171−colours :: [(String, Maybe Color)]

326+ colours :: [(String, Maybe Color)]

172−colours = [ ("black", Just Black)

327+ colours = [ ("black", Just Black)

173− , ("red", Just Red)

328+ , ("red", Just Red)

174− , ("green", Just Green)

329+ , ("green", Just Green)

175− , ("yellow", Just Yellow)

330+ , ("yellow", Just Yellow)

176− , ("blue", Just Blue)

331+ , ("blue", Just Blue)

177− , ("magenta", Just Magenta)

332+ , ("magenta", Just Magenta)

178− , ("cyan", Just Cyan)

333+ , ("cyan", Just Cyan)

179− , ("white", Just White)

334+ , ("white", Just White)

180− , ("default", Nothing)

335+ , ("default", Nothing)

181− ]

336+ ]

182−

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+

183−pColour :: P.IdrisParser (Maybe Color)

347+ pColour :: P.IdrisParser (Maybe Color)

184−pColour = doColour colours

348+ pColour = doColour colours

185− where doColour [] = fail "Unknown colour"

349+ where doColour [] = fail "Unknown colour"

186− doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs

350+ doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs

187−

351+

188−pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)

352+ pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)

189−pColourMod = try (P.symbol "vivid" >> return doVivid)

353+ pColourMod = try (P.symbol "vivid" >> return doVivid)

190− <|> try (P.symbol "dull" >> return doDull)

354+ <|> try (P.symbol "dull" >> return doDull)

191− <|> try (P.symbol "underline" >> return doUnderline)

355+ <|> try (P.symbol "underline" >> return doUnderline)

192− <|> try (P.symbol "nounderline" >> return doNoUnderline)

356+ <|> try (P.symbol "nounderline" >> return doNoUnderline)

193− <|> try (P.symbol "bold" >> return doBold)

357+ <|> try (P.symbol "bold" >> return doBold)

194− <|> try (P.symbol "nobold" >> return doNoBold)

358+ <|> try (P.symbol "nobold" >> return doNoBold)

195− <|> try (P.symbol "italic" >> return doItalic)

359+ <|> try (P.symbol "italic" >> return doItalic)

196− <|> try (P.symbol "noitalic" >> return doNoItalic)

360+ <|> try (P.symbol "noitalic" >> return doNoItalic)

197− <|> try (pColour >>= return . doSetColour)

361+ <|> try (pColour >>= return . doSetColour)

198− where doVivid i = i { vivid = True }

362+ where doVivid i = i { vivid = True }

199− doDull i = i { vivid = False }

363+ doDull i = i { vivid = False }

200− doUnderline i = i { underline = True }

364+ doUnderline i = i { underline = True }

201− doNoUnderline i = i { underline = False }

365+ doNoUnderline i = i { underline = False }

202− doBold i = i { bold = True }

366+ doBold i = i { bold = True }

203− doNoBold i = i { bold = False }

367+ doNoBold i = i { bold = False }

204− doItalic i = i { italic = True }

368+ doItalic i = i { italic = True }

205− doNoItalic i = i { italic = False }

369+ doNoItalic i = i { italic = False }

206− doSetColour c i = i { colour = c }

370+ doSetColour c i = i { colour = c }

207−

371+

208−-- | Generate the colour type names using the default Show instance.

372+ -- | Generate the colour type names using the default Show instance.

209−colourTypes :: [(String, ColourType)]

373+ colourTypes :: [(String, ColourType)]

210−colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

374+ colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

211− enumFromTo minBound maxBound

375+ enumFromTo minBound maxBound

212−

376+

213−pColourType :: P.IdrisParser ColourType

377+ pColourType :: P.IdrisParser ColourType

214−pColourType = doColourType colourTypes

378+ pColourType = doColourType colourTypes

215− where doColourType [] = fail $ "Unknown colour category. Options: " ++

379+ where doColourType [] = fail $ "Unknown colour category. Options: " ++

216− (concat . intersperse ", " . map fst) colourTypes

380+ (concat . intersperse ", " . map fst) colourTypes

217− doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts

381+ doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts

218−

382+

383+

219−pSetColourCmd :: P.IdrisParser Command

384+cmd_search :: String -> P.IdrisParser (Either String Command)

220−pSetColourCmd = (do c <- pColourType

385+cmd_search name = do

221− let defaultColour = IdrisColour Nothing True False False False

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

222− opts <- sepBy pColourMod (P.whiteSpace)

392+ P.whiteSpace

223− let colour = foldr ($) defaultColour $ reverse opts

393+ upd <- option False (do P.lchar '!'; return True)

224− return $ SetColour c colour)

394+ l <- P.natural; n <- P.name;

225− <|> try (P.symbol "on" >> return ColourOn)

395+ hints <- many P.fnName

226− <|> try (P.symbol "off" >> return ColourOff)

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]))