5e9d8de · Idris-dev · git.iko.soy

32import Data.List.Split (splitOn)

33import System.Console.ANSI (Color(..))

34import System.FilePath ((</>))

35−import Text.Parser.Char (anyChar, oneOf)

35+import qualified Text.Megaparsec as P

36−import Text.Parser.Combinators

36+import qualified Text.Megaparsec.Char as P

37

38parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

39parseCmd i inputname = IP.runparser pCmd i inputname . trim

68 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

69 , (["doc"], NameArg, "Show internal documentation", cmd_doc)

70 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

71− , genArg "namespace" (many anyChar) MakeDoc)

71+ , genArg "namespace" (P.many P.anyChar) MakeDoc)

72 , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"

73 , cmd_apropos)

74 , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg

170 , "(Debugging) Try to unify two expressions", const $ do

171 l <- IP.simpleExpr defaultSyntax

172 r <- IP.simpleExpr defaultSyntax

173− eof

173+ P.eof

174 return (Right (DebugUnify l r))

175 )

176 ]

189 (names, NoArg, doc, proofArg command)

190

191pCmd :: IP.IdrisParser (Either String Command)

192−pCmd = choice [ do c <- cmd names; parser c

192+pCmd = P.choice [ do c <- cmd names; parser c

193− | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

193+ | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

194 <|> unrecognized

195 <|> nop

196 <|> eval

197− where nop = do eof; return (Right NOP)

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

198 unrecognized = do

199 IP.lchar ':'

200− cmd <- many anyChar

200+ cmd <- P.many P.anyChar

201 let cmd' = takeWhile (/=' ') cmd

202 return (Left $ "Unrecognized command: " ++ cmd')

203

204cmd :: [String] -> IP.IdrisParser String

205−cmd xs = try $ do

205+cmd xs = P.try $ do

206 IP.lchar ':'

207 docmd sorted_xs

208

209 where docmd [] = fail "Could not parse command"

210− docmd (x:xs) = try (IP.reserved x >> return x) <|> docmd xs

210+ docmd (x:xs) = P.try (IP.reserved x >> return x) <|> docmd xs

211

212 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

213

215noArgs :: Command -> String -> IP.IdrisParser (Either String Command)

216noArgs cmd name = do

217 let emptyArgs = do

218− eof

218+ P.eof

219 return (Right cmd)

220

221 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

230exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)

231exprArg cmd name = do

232 let noArg = do

233− eof

233+ P.eof

234 return $ Left ("Usage is :" ++ name ++ " <expression>")

235

236 let justOperator = do

237 (op, fc) <- IP.symbolicOperatorFC

238− eof

238+ P.eof

239 return $ Right $ cmd (PRef fc [] (sUN op))

240

241 let properArg = do

242 t <- IP.fullExpr defaultSyntax

243 return $ Right (cmd t)

244− try noArg <|> try justOperator <|> properArg

244+ P.try noArg <|> P.try justOperator <|> properArg

245

246genArg :: String -> IP.IdrisParser a -> (a -> Command)

247 -> String -> IP.IdrisParser (Either String Command)

248genArg argName argParser cmd name = do

249− let emptyArgs = do eof; failure

249+ let emptyArgs = do P.eof; failure

250 oneArg = do arg <- argParser

251− eof

251+ P.eof

252 return (Right (cmd arg))

253− try emptyArgs <|> oneArg <|> failure

253+ P.try emptyArgs <|> oneArg <|> failure

254 where

255 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

256

259fnNameArg = genArg "functionname" $ fst <$> IP.fnName

260

261strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

262−strArg = genArg "string" (many anyChar)

262+strArg = genArg "string" (P.many P.anyChar)

263

264moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

265moduleArg = genArg "module" (fmap (toPath . fst) IP.identifier)

274optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)

275optArg cmd name = do

276 let emptyArgs = do

277− eof

277+ P.eof

278 return $ Left ("Usage is :" ++ name ++ " <option>")

279

280 let oneArg = do

281 o <- pOption

282 IP.whiteSpace

283− eof

283+ P.eof

284 return (Right (cmd o))

285

286 let failure = return $ Left "Unrecognized setting"

287

288− try emptyArgs <|> oneArg <|> failure

288+ P.try emptyArgs <|> oneArg <|> failure

289

290 where

291 pOption :: IP.IdrisParser Opt

293

294proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)

295proofArg cmd name = do

296− upd <- option False $ do

296+ upd <- P.option False $ do

297 IP.lchar '!'

298 return True

299 l <- fst <$> IP.natural

304cmd_doc name = do

305 let constant = do

306 c <- fmap fst IP.constant

307− eof

307+ P.eof

308 return $ Right (DocStr (Right c) FullDocs)

309

310 let pType = do

311 IP.reserved "Type"

312− eof

312+ P.eof

313 return $ Right (DocStr (Left $ IP.mkName ("Type", "")) FullDocs)

314

315 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

316

317− try constant <|> pType <|> fnName

317+ P.try constant <|> pType <|> fnName

318

319cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)

320cmd_consolewidth name = do

334

335cmd_execute :: String -> IP.IdrisParser (Either String Command)

336cmd_execute name = do

337− tm <- option maintm (IP.fullExpr defaultSyntax)

337+ tm <- P.option maintm (IP.fullExpr defaultSyntax)

338 return (Right (Execute tm))

339 where

340 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

341

342cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

343cmd_dynamic name = do

344− let optArg = do l <- many anyChar

344+ let optArg = do l <- P.many P.anyChar

345 if (l /= "")

346 then return $ Right (DynamicLink l)

347 else return $ Right ListDynamic

348 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

349− try optArg <|> failure

349+ P.try optArg <|> failure

350

351cmd_pprint :: String -> IP.IdrisParser (Either String Command)

352cmd_pprint name = do

376 let hasOneArg = do

377 i <- get

378 f <- fst <$> IP.identifier

379− eof

379+ P.eof

380 return $ Right (Compile defaultCodegen f)

381

382 let hasTwoArgs = do

383 i <- get

384 codegen <- codegenOption

385 f <- fst <$> IP.identifier

386− eof

386+ P.eof

387 return $ Right (Compile codegen f)

388

389 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

390− try hasTwoArgs <|> try hasOneArg <|> failure

390+ P.try hasTwoArgs <|> P.try hasOneArg <|> failure

391

392cmd_addproof :: String -> IP.IdrisParser (Either String Command)

393cmd_addproof name = do

394− n <- option Nothing $ do

394+ n <- P.option Nothing $ do

395 x <- fst <$> IP.name

396 return (Just x)

397− eof

397+ P.eof

398 return (Right (AddProof n))

399

400cmd_log :: String -> IP.IdrisParser (Either String Command)

401cmd_log name = do

402 i <- fmap (fromIntegral . fst) IP.natural

403− eof

403+ P.eof

404 return (Right (LogLvl i))

405

406cmd_verb :: String -> IP.IdrisParser (Either String Command)

407cmd_verb name = do

408 i <- fmap (fromIntegral . fst) IP.natural

409− eof

409+ P.eof

410 return (Right (Verbosity i))

411

412cmd_cats :: String -> IP.IdrisParser (Either String Command)

413cmd_cats name = do

414− cs <- sepBy pLogCats (IP.whiteSpace)

414+ cs <- P.sepBy pLogCats (IP.whiteSpace)

415− eof

415+ P.eof

416 return $ Right $ LogCategory (concat cs)

417 where

418 badCat = do

420 fail $ "Category: " ++ c ++ " is not recognised."

421

422 pLogCats :: IP.IdrisParser [LogCat]

423− pLogCats = try (parserCats <$ IP.symbol (strLogCat IParse))

423+ pLogCats = P.try (parserCats <$ IP.symbol (strLogCat IParse))

424− <|> try (elabCats <$ IP.symbol (strLogCat IElab))

424+ <|> P.try (elabCats <$ IP.symbol (strLogCat IElab))

425− <|> try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

425+ <|> P.try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

426− <|> try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

426+ <|> P.try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

427− <|> try ([IIBC] <$ IP.symbol (strLogCat IIBC))

427+ <|> P.try ([IIBC] <$ IP.symbol (strLogCat IIBC))

428− <|> try ([IErasure] <$ IP.symbol (strLogCat IErasure))

428+ <|> P.try ([IErasure] <$ IP.symbol (strLogCat IErasure))

429 <|> badCat

430

431cmd_let :: String -> IP.IdrisParser (Either String Command)

432cmd_let name = do

433− defn <- concat <$> many (IP.decl defaultSyntax)

433+ defn <- concat <$> P.many (IP.decl defaultSyntax)

434 return (Right (NewDefn defn))

435

436cmd_unlet :: String -> IP.IdrisParser (Either String Command)

437−cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> IP.name)

437+cmd_unlet name = (Right . Undefine) `fmap` P.many (fst <$> IP.name)

438

439cmd_loadto :: String -> IP.IdrisParser (Either String Command)

440cmd_loadto name = do

441 toline <- fmap (fromInteger . fst) IP.natural

442− f <- many anyChar;

442+ f <- P.many P.anyChar

443 return (Right (Load f (Just toline)))

444

445cmd_colour :: String -> IP.IdrisParser (Either String Command)

461 pSetColourCmd :: IP.IdrisParser Command

462 pSetColourCmd = (do c <- pColourType

463 let defaultColour = IdrisColour Nothing True False False False

464− opts <- sepBy pColourMod (IP.whiteSpace)

464+ opts <- P.sepBy pColourMod (IP.whiteSpace)

465 let colour = foldr ($) defaultColour $ reverse opts

466 return $ SetColour c colour)

467− <|> try (IP.symbol "on" >> return ColourOn)

467+ <|> P.try (IP.symbol "on" >> return ColourOn)

468− <|> try (IP.symbol "off" >> return ColourOff)

468+ <|> P.try (IP.symbol "off" >> return ColourOff)

469

470 pColour :: IP.IdrisParser (Maybe Color)

471 pColour = doColour colours

472 where doColour [] = fail "Unknown colour"

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

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

474

475 pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)

476− pColourMod = try (doVivid <$ IP.symbol "vivid")

476+ pColourMod = P.try (doVivid <$ IP.symbol "vivid")

477− <|> try (doDull <$ IP.symbol "dull")

477+ <|> P.try (doDull <$ IP.symbol "dull")

478− <|> try (doUnderline <$ IP.symbol "underline")

478+ <|> P.try (doUnderline <$ IP.symbol "underline")

479− <|> try (doNoUnderline <$ IP.symbol "nounderline")

479+ <|> P.try (doNoUnderline <$ IP.symbol "nounderline")

480− <|> try (doBold <$ IP.symbol "bold")

480+ <|> P.try (doBold <$ IP.symbol "bold")

481− <|> try (doNoBold <$ IP.symbol "nobold")

481+ <|> P.try (doNoBold <$ IP.symbol "nobold")

482− <|> try (doItalic <$ IP.symbol "italic")

482+ <|> P.try (doItalic <$ IP.symbol "italic")

483− <|> try (doNoItalic <$ IP.symbol "noitalic")

483+ <|> P.try (doNoItalic <$ IP.symbol "noitalic")

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

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

485 where doVivid i = i { vivid = True }

486 doDull i = i { vivid = False }

487 doUnderline i = i { underline = True }

501 pColourType = doColourType colourTypes

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

503 (concat . intersperse ", " . map fst) colourTypes

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

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

505

506−idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

506+idChar = P.oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

507

508cmd_apropos :: String -> IP.IdrisParser (Either String Command)

509cmd_apropos = packageBasedCmd (some idChar) Apropos

511packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)

512 -> String -> IP.IdrisParser (Either String Command)

513packageBasedCmd valParser cmd name =

514− try (do IP.lchar '('

514+ P.try (do IP.lchar '('

515− pkgs <- sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

515+ pkgs <- P.sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

516− IP.lchar ')'

516+ IP.lchar ')'

517− val <- valParser

517+ val <- valParser

518− return (Right (cmd pkgs val)))

518+ return (Right (cmd pkgs val)))

519 <|> do val <- valParser

520 return (Right (cmd [] val))

521 where

527

528cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)

529cmd_proofsearch name = do

530− upd <- option False (True <$ IP.lchar '!')

530+ upd <- P.option False (True <$ IP.lchar '!')

531 l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

532− hints <- many (fst <$> IP.fnName)

532+ hints <- P.many (fst <$> IP.fnName)

533 return (Right (DoProofSearch upd True l n hints))

534

535cmd_refine :: String -> IP.IdrisParser (Either String Command)

536cmd_refine name = do

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

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

538 l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

539 hint <- fst <$> IP.fnName

540 return (Right (DoProofSearch upd False l n [hint]))