1f8db23 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Import Trifecta qualified as P

commit1f8db23b10bac265041810aa325498451a98ec1e authorJason Felice <jason.m.felice@gmail.com> dateThu 26 Oct 2017, 13:32 (9 years ago) parent44a3f9c

11 files changed+681−708

compare with master

unifiedsplit

src/Idris/IdeMode.hs+17−18 src/Idris/Main.hs+19−19 src/Idris/Package/Parser.hs+38−38 src/Idris/Parser.hs+164−186 src/Idris/Parser/Data.hs+28−28 src/Idris/Parser/Expr.hs+152−153 src/Idris/Parser/Helpers.hs+82−82 src/Idris/Parser/Ops.hs+11−11 src/Idris/Prover.hs+23−23 src/Idris/REPL.hs+22−25 src/Idris/REPL/Parser.hs+125−125

src/Idris/IdeMode.hs+17−18

@@ -25,8 +25,8 @@ import qualified Data.Text as T

2525import Numeric

2626import System.IO

2727import Text.Printf

28−import Text.Trifecta hiding (Err)

29−import Text.Trifecta.Delta

28+import qualified Text.Trifecta as P

29+import qualified Text.Trifecta.Delta as P

3030

3131getNChar :: Handle -> Int -> String -> IO (String)

3232getNChar _ 0 s = return (reverse s)

@@ -205,28 +205,27 @@ escape = concatMap escapeChar

205205 escapeChar '"' = "\\\""

206206 escapeChar c = [c]

207207

208−pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))

209− return (SexpList xs)

208+pSExp = SexpList <$> P.between (P.char '(') (P.char ')') (pSExp `P.sepBy` (P.char ' '))

210209 <|> atom

211210

212−atom = do string "nil"; return (SexpList [])

213− <|> do char ':'; x <- atomC; return x

214− <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

215− <|> do ints <- some digit

211+atom = SexpList [] <$ P.string "nil"

212+ <|> P.char ':' *> atomC

213+ <|> StringAtom <$> P.between (P.char '"') (P.char '"') (P.many quotedChar)

214+ <|> do ints <- some P.digit

216215 case readDec ints of

217216 ((num, ""):_) -> return (IntegerAtom (toInteger num))

218217 _ -> return (StringAtom ints)

219218

220−atomC = do string "True"; return (BoolAtom True)

221− <|> do string "False"; return (BoolAtom False)

222− <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)

219+atomC = BoolAtom True <$ P.string "True"

220+ <|> BoolAtom False <$ P.string "False"

221+ <|> SymbolAtom <$> many (P.noneOf " \n\t\r\"()")

223222

224−quotedChar = try (string "\\\\" >> return '\\')

225− <|> try (string "\\\"" >> return '"')

226− <|> noneOf "\""

223+quotedChar = P.try ('\\' <$ P.string "\\\\")

224+ <|> P.try ('"' <$ P.string "\\\"")

225+ <|> P.noneOf "\""

227226

228−parseSExp :: String -> Result SExp

229−parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

227+parseSExp :: String -> P.Result SExp

228+parseSExp = P.parseString pSExp (P.Directed (UTF8.fromString "(unknown)") 0 0 0 0)

230229

231230data Opt = ShowImpl | ErrContext deriving Show

232231

@@ -324,8 +323,8 @@ parseMessage x = case receiveString x of

324323receiveString :: String -> Either Err SExp

325324receiveString x =

326325 case parseSExp x of

327− Failure _ -> Left . Msg $ "parse failure"

328− Success r -> Right r

326+ P.Failure _ -> Left . Msg $ "parse failure"

327+ P.Success r -> Right r

329328

330329convSExp :: SExpable a => String -> a -> Integer -> String

331330convSExp pre s id =

src/Idris/Main.hs+19−19

@@ -47,7 +47,7 @@ import System.Exit

4747import System.FilePath

4848import System.IO

4949import System.IO.CodePage (withCP65001)

50−import Text.Trifecta.Result (ErrInfo(..), Result(..))

50+import qualified Text.Trifecta.Result as P

5151

5252-- | How to run Idris programs.

5353runMain :: Idris () -> IO ()

@@ -196,9 +196,9 @@ idrisMain opts =

196196 mapM_ (\str -> do ist <- getIState

197197 c <- colourise

198198 case parseExpr ist str of

199− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

200− runIO $ exitWith (ExitFailure 1)

201− Success e -> process "" (Eval e))

199+ P.Failure (P.ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

200+ runIO $ exitWith (ExitFailure 1)

201+ P.Success e -> process "" (Eval e))

202202 exprs

203203 runIO exitSuccess

204204

@@ -273,12 +273,12 @@ execScript :: String -> Idris ()

273273execScript expr = do i <- getIState

274274 c <- colourise

275275 case parseExpr i expr of

276− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

277− runIO $ exitWith (ExitFailure 1)

278− Success term -> do ctxt <- getContext

279− (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

280− res <- execute tm

281− runIO $ exitSuccess

276+ P.Failure (P.ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

277+ runIO $ exitWith (ExitFailure 1)

278+ P.Success term -> do ctxt <- getContext

279+ (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

280+ res <- execute tm

281+ runIO $ exitSuccess

282282

283283-- | Run the initialisation script

284284initScript :: Idris ()

@@ -300,12 +300,12 @@ initScript = do script <- runIO $ getIdrisInitScript

300300 runInit h

301301 processLine i cmd input clr =

302302 case parseCmd i input cmd of

303− Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)

304− Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

305− Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

306− Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

307− Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

308− Success (Right Proofs) -> proofs i

309− Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

310− Success (Right cmd ) -> process [] cmd

311− Success (Left err) -> runIO $ print err

303+ P.Failure (P.ErrInfo err _) -> runIO $ print (fixColour clr err)

304+ P.Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

305+ P.Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

306+ P.Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

307+ P.Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

308+ P.Success (Right Proofs) -> proofs i

309+ P.Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

310+ P.Success (Right cmd ) -> process [] cmd

311+ P.Success (Left err) -> runIO $ print err

src/Idris/Package/Parser.hs+38−38

@@ -20,8 +20,8 @@ import System.Directory (doesFileExist)

2020import System.Exit

2121import System.FilePath (isValid, takeExtension, takeFileName)

2222import qualified Text.PrettyPrint.ANSI.Leijen as PP

23−import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,

24− whiteSpace)

23+import Text.Trifecta ((<?>))

24+import qualified Text.Trifecta as P

2525

2626type PParser = StateT PkgDesc IdrisInnerParser

2727

@@ -29,20 +29,20 @@ instance HasLastTokenSpan PParser where

2929 getLastTokenSpan = return Nothing

3030

3131#if MIN_VERSION_base(4,9,0)

32−instance {-# OVERLAPPING #-} DeltaParsing PParser where

33− line = lift line

32+instance {-# OVERLAPPING #-} P.DeltaParsing PParser where

33+ line = lift P.line

3434 {-# INLINE line #-}

35− position = lift position

35+ position = lift P.position

3636 {-# INLINE position #-}

37− slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

37+ slicedWith f (StateT m) = StateT $ \s -> P.slicedWith (\(a,s') b -> (f a b, s')) $ m s

3838 {-# INLINE slicedWith #-}

39− rend = lift rend

39+ rend = lift P.rend

4040 {-# INLINE rend #-}

41− restOfLine = lift restOfLine

41+ restOfLine = lift P.restOfLine

4242 {-# INLINE restOfLine #-}

4343#endif

4444

45−instance {-# OVERLAPPING #-} TokenParsing PParser where

45+instance {-# OVERLAPPING #-} P.TokenParsing PParser where

4646 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

4747

4848

@@ -56,8 +56,8 @@ parseDesc fp = do

5656 then do

5757 p <- readFile fp

5858 case runparser pPkg defaultPkg fp p of

59− Failure (ErrInfo err _) -> fail (show $ PP.plain err)

60− Success x -> return x

59+ P.Failure (P.ErrInfo err _) -> fail (show $ PP.plain err)

60+ P.Success x -> return x

6161 else do

6262 putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]

6363 exitWith (ExitFailure 1)

@@ -66,12 +66,12 @@ pPkg :: PParser PkgDesc

6666pPkg = do

6767 reserved "package"

6868 p <- pPkgName

69− someSpace

69+ P.someSpace

7070 st <- get

7171 put (st { pkgname = p })

7272 some pClause

7373 st <- get

74− eof

74+ P.eof

7575 return st

7676

7777pPkgName :: PParser PkgName

@@ -82,12 +82,12 @@ pPkgName = (either fail pure . pkgName =<< packageName) <?> "PkgName"

8282-- | Treated for now as an identifier or a double-quoted string.

8383filename :: (MonadicParsing m, HasLastTokenSpan m) => m String

8484filename = (do

85− filename <- token $

85+ filename <- P.token $

8686 -- Treat a double-quoted string as a filename to support spaces.

8787 -- This also moves away from tying filenames to identifiers, so

8888 -- it will also accept hyphens

8989 -- (https://github.com/idris-lang/Idris-dev/issues/2721)

90− stringLiteral

90+ P.stringLiteral

9191 <|>

9292 -- Through at least version 0.9.19.1, IPKG executable values were

9393 -- possibly namespaced identifiers, like foo.bar.baz.

@@ -137,13 +137,13 @@ pClause = do reserved "executable"; lchar '=';

137137 put (st { sourcedir = src })

138138

139139 <|> do reserved "opts"; lchar '=';

140− opts <- stringLiteral

140+ opts <- P.stringLiteral

141141 st <- get

142142 let args = pureArgParser (words opts)

143143 put (st { idris_opts = args ++ idris_opts st })

144144

145145 <|> do reserved "pkgs"; lchar '=';

146− ps <- sepBy1 (pPkgName <* someSpace) (lchar ',')

146+ ps <- P.sepBy1 (pPkgName <* P.someSpace) (lchar ',')

147147 st <- get

148148 let pkgs = pureArgParser $ concatMap (\x -> ["-p", show x]) ps

149149

@@ -151,17 +151,17 @@ pClause = do reserved "executable"; lchar '=';

151151 , idris_opts = pkgs ++ idris_opts st})

152152

153153 <|> do reserved "modules"; lchar '=';

154− ms <- sepBy1 (fst <$> iName []) (lchar ',')

154+ ms <- P.sepBy1 (fst <$> iName []) (lchar ',')

155155 st <- get

156156 put (st { modules = modules st ++ ms })

157157

158158 <|> do reserved "libs"; lchar '=';

159− ls <- sepBy1 (fst <$> identifier) (lchar ',')

159+ ls <- P.sepBy1 (fst <$> identifier) (lchar ',')

160160 st <- get

161161 put (st { libdeps = libdeps st ++ ls })

162162

163163 <|> do reserved "objs"; lchar '=';

164− ls <- sepBy1 (fst <$> identifier) (lchar ',')

164+ ls <- P.sepBy1 (fst <$> identifier) (lchar ',')

165165 st <- get

166166 put (st { objs = objs st ++ ls })

167167

@@ -171,74 +171,74 @@ pClause = do reserved "executable"; lchar '=';

171171 put (st { makefile = Just (show mk) })

172172

173173 <|> do reserved "tests"; lchar '=';

174− ts <- sepBy1 (fst <$> iName []) (lchar ',')

174+ ts <- P.sepBy1 (fst <$> iName []) (lchar ',')

175175 st <- get

176176 put st { idris_tests = idris_tests st ++ ts }

177177

178178 <|> do reserved "version"

179179 lchar '='

180− vStr <- many (satisfy (not . isEol))

180+ vStr <- many (P.satisfy (not . isEol))

181181 eol

182− someSpace

182+ P.someSpace

183183 st <- get

184184 put st {pkgversion = Just vStr}

185185

186186 <|> do reserved "readme"

187187 lchar '='

188− rme <- many (satisfy (not . isEol))

188+ rme <- many (P.satisfy (not . isEol))

189189 eol

190− someSpace

190+ P.someSpace

191191 st <- get

192192 put (st { pkgreadme = Just rme })

193193

194194 <|> do reserved "license"

195195 lchar '='

196− lStr <- many (satisfy (not . isEol))

196+ lStr <- many (P.satisfy (not . isEol))

197197 eol

198198 st <- get

199199 put st {pkglicense = Just lStr}

200200

201201 <|> do reserved "homepage"

202202 lchar '='

203− www <- many (satisfy (not . isEol))

203+ www <- many (P.satisfy (not . isEol))

204204 eol

205− someSpace

205+ P.someSpace

206206 st <- get

207207 put st {pkghomepage = Just www}

208208

209209 <|> do reserved "sourceloc"

210210 lchar '='

211− srcpage <- many (satisfy (not . isEol))

211+ srcpage <- many (P.satisfy (not . isEol))

212212 eol

213− someSpace

213+ P.someSpace

214214 st <- get

215215 put st {pkgsourceloc = Just srcpage}

216216

217217 <|> do reserved "bugtracker"

218218 lchar '='

219− src <- many (satisfy (not . isEol))

219+ src <- many (P.satisfy (not . isEol))

220220 eol

221− someSpace

221+ P.someSpace

222222 st <- get

223223 put st {pkgbugtracker = Just src}

224224

225225 <|> do reserved "brief"

226226 lchar '='

227− brief <- stringLiteral

227+ brief <- P.stringLiteral

228228 st <- get

229− someSpace

229+ P.someSpace

230230 put st {pkgbrief = Just brief}

231231

232232 <|> do reserved "author"; lchar '=';

233− author <- many (satisfy (not . isEol))

233+ author <- many (P.satisfy (not . isEol))

234234 eol

235− someSpace

235+ P.someSpace

236236 st <- get

237237 put st {pkgauthor = Just author}

238238

239239 <|> do reserved "maintainer"; lchar '=';

240− maintainer <- many (satisfy (not . isEol))

240+ maintainer <- many (P.satisfy (not . isEol))

241241 eol

242− someSpace

242+ P.someSpace

243243 st <- get

244244 put st {pkgmaintainer = Just maintainer}

src/Idris/Parser.hs+164−186

@@ -36,7 +36,7 @@ import Idris.Parser.Ops

3636import Idris.Termination

3737import Idris.Unlit

3838

39−import qualified Util.Pretty as P

39+import qualified Util.Pretty

4040import Util.System (readSource)

4141

4242import Prelude hiding (pi)

@@ -59,9 +59,9 @@ import qualified System.Directory as Dir (makeAbsolute)

5959import System.FilePath

6060import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

6161import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

62−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

63− stringLiteral, symbol, whiteSpace)

64−import Text.Trifecta.Delta

62+import Text.Trifecta ((<?>))

63+import qualified Text.Trifecta as P

64+import qualified Text.Trifecta.Delta as P

6565

6666{-

6767@

@@ -84,17 +84,17 @@ import Text.Trifecta.Delta

8484@

8585-}

8686moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

87−moduleHeader = try (do docs <- optional docComment

88− noArgs docs

89− reservedHL "module"

90− (i, ifc) <- identifier

91− option ';' (lchar ';')

92− let modName = moduleName i

93− return (fmap fst docs,

94− modName,

95− [(ifc, AnnNamespace (map T.pack modName) Nothing)]))

96− <|> try (do lchar '%'; reserved "unqualified"

97− return (Nothing, [], []))

87+moduleHeader = P.try (do docs <- optional docComment

88+ noArgs docs

89+ reservedHL "module"

90+ (i, ifc) <- identifier

91+ P.option ';' (lchar ';')

92+ let modName = moduleName i

93+ return (fmap fst docs,

94+ modName,

95+ [(ifc, AnnNamespace (map T.pack modName) Nothing)]))

96+ <|> P.try (do lchar '%'; reserved "unqualified"

97+ return (Nothing, [], []))

9898 <|> return (Nothing, moduleName "Main", [])

9999 where moduleName x = case span (/='.') x of

100100 (x, "") -> [x]

@@ -119,12 +119,11 @@ data ImportInfo = ImportInfo { import_reexport :: Bool

119119import_ :: IdrisParser ImportInfo

120120import_ = do fc <- getFC

121121 reservedHL "import"

122− reexport <- option False (do reservedHL "public"

123− return True)

122+ reexport <- P.option False (True <$ reservedHL "public")

124123 (id, idfc) <- identifier

125124 newName <- optional (do reservedHL "as"

126125 identifier)

127− option ';' (lchar ';')

126+ P.option ';' (lchar ';')

128127 return $ ImportInfo reexport (toPath id)

129128 (fmap (\(n, fc) -> (toPath n, fc)) newName)

130129 (map T.pack $ ns id) fc idfc

@@ -143,7 +142,7 @@ prog syn = do whiteSpace

143142 decls <- many (decl syn)

144143 let c = concat decls

145144 case maxline syn of

146− Nothing -> do notOpenBraces; eof

145+ Nothing -> do notOpenBraces; P.eof

147146 _ -> return ()

148147 ist <- get

149148 fc <- getFC

@@ -172,7 +171,7 @@ Decl ::=

172171@

173172-}

174173decl :: SyntaxInfo -> IdrisParser [PDecl]

175−decl syn = try (externalDecl syn)

174+decl syn = P.try (externalDecl syn)

176175 <|> internalDecl syn

177176 <?> "declaration"

178177

@@ -195,13 +194,13 @@ internalDecl syn

195194 if continue then

196195 do notEndBlock

197196 declBody continue

198− else try (do notEndBlock

199− declBody continue)

197+ else P.try (do notEndBlock

198+ declBody continue)

200199 <|> fail "End of readable input"

201200 where declBody :: Bool -> IdrisParser [PDecl]

202201 declBody b =

203− try (implementation True syn)

204− <|> try (openInterface syn)

202+ P.try (implementation True syn)

203+ <|> P.try (openInterface syn)

205204 <|> declBody' b

206205 <|> using_ syn

207206 <|> params syn

@@ -276,9 +275,9 @@ declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)

276275declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

277276 -> IdrisParser [PDecl]

278277declExtension syn ns rules =

279− choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

278+ P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

280279 case head rs of -- can never be []

281− DeclRule (symb:_) _ -> try $ do

280+ DeclRule (symb:_) _ -> P.try $ do

282281 n <- extSymbol symb

283282 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]

284283 -- If we have more than one Rule in this bucket, our grammar is

@@ -427,28 +426,28 @@ SyntaxSym ::= '[' Name_t ']'

427426-}

428427syntaxRule :: SyntaxInfo -> IdrisParser Syntax

429428syntaxRule syn

430− = do sty <- try (do

429+ = do sty <- P.try (do

431430 pushIndent

432− sty <- option AnySyntax

433− (do reservedHL "term"; return TermSyntax

434− <|> do reservedHL "pattern"; return PatternSyntax)

431+ sty <- P.option AnySyntax

432+ (TermSyntax <$ reservedHL "term"

433+ <|> PatternSyntax <$ reservedHL "pattern")

435434 reservedHL "syntax"

436435 return sty)

437436 syms <- some syntaxSym

438− when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

437+ when (all isExpr syms) $ P.unexpected "missing keywords in syntax rule"

439438 let ns = mapMaybe getName syms

440439 when (length ns /= length (nub ns))

441− $ unexpected "repeated variable in syntax rule"

440+ $ P.unexpected "repeated variable in syntax rule"

442441 lchar '='

443442 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

444443 terminator

445444 return (Rule (mkSimple syms) tm sty)

446445 <|> do reservedHL "decl"; reservedHL "syntax"

447446 syms <- some syntaxSym

448− when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

447+ when (all isExpr syms) $ P.unexpected "missing keywords in syntax rule"

449448 let ns = mapMaybe getName syms

450449 when (length ns /= length (nub ns))

451− $ unexpected "repeated variable in syntax rule"

450+ $ P.unexpected "repeated variable in syntax rule"

452451 lchar '='

453452 openBlock

454453 dec <- some (decl syn)

@@ -544,10 +543,10 @@ SyntaxSym ::= '[' Name_t ']'

544543@

545544 -}

546545syntaxSym :: IdrisParser SSymbol

547−syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'

548− return (Expr n))

549− <|> try (do lchar '{'; n <- fst <$> name; lchar '}'

550− return (Binding n))

546+syntaxSym = P.try (do lchar '['; n <- fst <$> name; lchar ']'

547+ return (Expr n))

548+ <|> P.try (do lchar '{'; n <- fst <$> name; lchar '}'

549+ return (Binding n))

551550 <|> do n <- fst <$> iName []

552551 return (Keyword n)

553552 <|> do sym <- fmap fst stringLiteral

@@ -561,11 +560,11 @@ syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'

561560@

562561-}

563562fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

564−fnDecl syn = try (do notEndBlock

565− d <- fnDecl' syn

566− i <- get

567− let d' = fmap (desugar syn i) d

568− return [d']) <?> "function declaration"

563+fnDecl syn = P.try (do notEndBlock

564+ d <- fnDecl' syn

565+ i <- get

566+ let d' = fmap (desugar syn i) d

567+ return [d']) <?> "function declaration"

569568

570569{-| Parses a function declaration

571570

@@ -580,7 +579,7 @@ fnDecl syn = try (do notEndBlock

580579-}

581580fnDecl' :: SyntaxInfo -> IdrisParser PDecl

582581fnDecl' syn = checkDeclFixity $

583− do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

582+ do (doc, argDocs, fc, opts', n, nfc, acc) <- P.try (do

584583 pushIndent

585584 (doc, argDocs) <- docstring syn

586585 (opts, acc) <- fnOpts

@@ -658,41 +657,32 @@ NameTimesList ::=

658657-}

659658fnOpt :: IdrisParser FnOpt

660659fnOpt = do reservedHL "total"; return TotalFn

661− <|> do reservedHL "partial"; return PartialFn

662− <|> do reservedHL "covering"; return CoveringFn

663− <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

664− return $ CExport c

665− <|> do try (lchar '%' *> reserved "no_implicit");

666− return NoImplicit

667− <|> do try (lchar '%' *> reserved "inline");

668− return Inlinable

669− <|> do try (lchar '%' *> reserved "static");

670− return StaticFn

671− <|> do try (lchar '%' *> reserved "assert_total");

660+ <|> PartialFn <$ reservedHL "partial"

661+ <|> CoveringFn <$ reservedHL "covering"

662+ <|> do P.try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

663+ return $ CExport c

664+ <|> NoImplicit <$ P.try (lchar '%' *> reserved "no_implicit")

665+ <|> Inlinable <$ P.try (lchar '%' *> reserved "inline")

666+ <|> StaticFn <$ P.try (lchar '%' *> reserved "static")

667+ <|> do P.try (lchar '%' *> reserved "assert_total");

672668 fc <- getFC

673669 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")

674670 return AssertTotal

675− <|> do try (lchar '%' *> reserved "error_handler");

676− return ErrorHandler

677− <|> do try (lchar '%' *> reserved "error_reverse");

678− return ErrorReverse

679− <|> do try (lchar '%' *> reserved "error_reduce");

680− return ErrorReduce

681− <|> do try (lchar '%' *> reserved "reflection");

682− return Reflection

683− <|> do try (lchar '%' *> reserved "hint");

684− return AutoHint

685− <|> do try (lchar '%' *> reserved "overlapping");

686− return OverlappingDictionary

671+ <|> ErrorHandler <$ P.try (lchar '%' *> reserved "error_handler")

672+ <|> ErrorReverse <$ P.try (lchar '%' *> reserved "error_reverse")

673+ <|> ErrorReduce <$ P.try (lchar '%' *> reserved "error_reduce")

674+ <|> Reflection <$ P.try (lchar '%' *> reserved "reflection")

675+ <|> AutoHint <$ P.try (lchar '%' *> reserved "hint")

676+ <|> OverlappingDictionary <$ P.try (lchar '%' *> reserved "overlapping")

687677 <|> do lchar '%'; reserved "specialise";

688− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

678+ lchar '['; ns <- P.sepBy nameTimes (lchar ','); lchar ']';

689679 return $ Specialise ns

690− <|> do reservedHL "implicit"; return Implicit

680+ <|> Implicit <$ reservedHL "implicit"

691681 <?> "function modifier"

692682 where nameTimes :: IdrisParser (Name, Maybe Int)

693683 nameTimes = do n <- fst <$> fnName

694− t <- option Nothing (do reds <- fmap fst natural

695− return (Just (fromInteger reds)))

684+ t <- P.option Nothing (do reds <- fmap fst natural

685+ return (Just (fromInteger reds)))

696686 return (n, t)

697687

698688{-| Parses a postulate

@@ -705,10 +695,10 @@ Postulate ::=

705695-}

706696postulate :: SyntaxInfo -> IdrisParser PDecl

707697postulate syn = do (doc, ext)

708− <- try $ do (doc, _) <- docstring syn

709− pushIndent

710− ext <- ppostDecl

711− return (doc, ext)

698+ <- P.try $ do (doc, _) <- docstring syn

699+ pushIndent

700+ ext <- ppostDecl

701+ return (doc, ext)

712702 ist <- get

713703 (opts, acc) <- fnOpts

714704 (n_in, nfc) <- fnName

@@ -768,7 +758,7 @@ openInterface syn =

768758 do reservedHL "using"

769759 reservedHL "implementation"

770760 fc <- getFC

771− ns <- sepBy1 fnName (lchar ',')

761+ ns <- P.sepBy1 fnName (lchar ',')

772762

773763 openBlock

774764 ds <- many (decl syn)

@@ -848,14 +838,14 @@ InterfaceBlock ::=

848838interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

849839interfaceBlock syn = do reservedHL "where"

850840 openBlock

851− (cn, cd) <- option (Nothing, emptyDocstring) $

852− try (do (doc, _) <- option noDocs docComment

853− n <- constructor

854− return (Just n, doc))

841+ (cn, cd) <- P.option (Nothing, emptyDocstring) $

842+ P.try (do (doc, _) <- P.option noDocs docComment

843+ n <- constructor

844+ return (Just n, doc))

855845 ist <- get

856846 let cd' = annotate syn ist cd

857847

858− ds <- many (notEndBlock >> try (implementation True syn)

848+ ds <- many (notEndBlock >> P.try (implementation True syn)

859849 <|> do x <- data_ syn

860850 return [x]

861851 <|> fnDecl syn)

@@ -886,24 +876,24 @@ Interface ::=

886876-}

887877interface_ :: SyntaxInfo -> IdrisParser [PDecl]

888878interface_ syn = do (doc, argDocs, acc)

889− <- try (do (doc, argDocs) <- docstring syn

890− acc <- accessibility

891− interfaceKeyword

892− return (doc, argDocs, acc))

879+ <- P.try (do (doc, argDocs) <- docstring syn

880+ acc <- accessibility

881+ interfaceKeyword

882+ return (doc, argDocs, acc))

893883 fc <- getFC

894884 cons <- constraintList syn

895885 let cons' = [(c, ty) | (_, c, _, ty) <- cons]

896886 (n_in, nfc) <- fnName

897887 let n = expandNS syn n_in

898888 cs <- many carg

899− fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

900− (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn)

889+ fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

890+ (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)

901891 accData acc n (concatMap declared ds)

902892 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]

903893 <?> "interface declaration"

904894 where

905895 fundeps :: IdrisParser [(Name, FC)]

906− fundeps = do lchar '|'; sepBy name (lchar ',')

896+ fundeps = do lchar '|'; P.sepBy name (lchar ',')

907897

908898 interfaceKeyword :: IdrisParser ()

909899 interfaceKeyword = reservedHL "interface"

@@ -964,7 +954,7 @@ implementation kwopt syn

964954

965955 implementationUsing :: IdrisParser [Name]

966956 implementationUsing = do reservedHL "using"

967− ns <- sepBy1 fnName (lchar ',')

957+ ns <- P.sepBy1 fnName (lchar ',')

968958 return (map fst ns)

969959 <|> return []

970960

@@ -972,7 +962,7 @@ implementation kwopt syn

972962docstring :: SyntaxInfo

973963 -> IdrisParser (Docstring (Either Err PTerm),

974964 [(Name,Docstring (Either Err PTerm))])

975−docstring syn = do (doc, argDocs) <- option noDocs docComment

965+docstring syn = do (doc, argDocs) <- P.option noDocs docComment

976966 ist <- get

977967 let doc' = annotCode (tryFullExpr syn ist) doc

978968 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

@@ -1005,8 +995,8 @@ NameList ::=

1005995-}

1006996usingDeclList :: SyntaxInfo -> IdrisParser [Using]

1007997usingDeclList syn

1008− = try (sepBy1 (usingDecl syn) (lchar ','))

1009− <|> do ns <- sepBy1 (fst <$> name) (lchar ',')

998+ = P.try (P.sepBy1 (usingDecl syn) (lchar ','))

999+ <|> do ns <- P.sepBy1 (fst <$> name) (lchar ',')

10101000 lchar ':'

10111001 t <- typeExpr (disallowImp syn)

10121002 return (map (\x -> UImplicit x t) ns)

@@ -1022,10 +1012,10 @@ UsingDecl ::=

10221012@

10231013-}

10241014usingDecl :: SyntaxInfo -> IdrisParser Using

1025−usingDecl syn = try (do x <- fst <$> fnName

1026− lchar ':'

1027− t <- typeExpr (disallowImp syn)

1028− return (UImplicit x t))

1015+usingDecl syn = P.try (do x <- fst <$> fnName

1016+ lchar ':'

1017+ t <- typeExpr (disallowImp syn)

1018+ return (UImplicit x t))

10291019 <|> do c <- fst <$> fnName

10301020 xs <- many (fst <$> fnName)

10311021 return (UConstraint c xs)

@@ -1068,7 +1058,7 @@ ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

10681058-}

10691059argExpr :: SyntaxInfo -> IdrisParser PTerm

10701060argExpr syn = let syn' = syn { inPattern = True } in

1071− try (hsimpleExpr syn') <|> simpleExternalExpr syn'

1061+ P.try (hsimpleExpr syn') <|> simpleExternalExpr syn'

10721062 <?> "argument expression"

10731063

10741064{-| Parse a right hand side of a function

@@ -1090,8 +1080,8 @@ rhs syn n = do lchar '='

10901080 expr syn

10911081 <|> do symbol "?=";

10921082 fc <- getFC

1093− name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";

1094− return n)

1083+ name <- P.option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";

1084+ return n)

10951085 r <- expr syn

10961086 return (addLet fc name r)

10971087 <|> impossible

@@ -1135,7 +1125,7 @@ WhereOrTerminator ::= WhereBlock | Terminator;

11351125-}

11361126clause :: SyntaxInfo -> IdrisParser PClause

11371127clause syn

1138− = do wargs <- try (do pushIndent; some (wExpr syn))

1128+ = do wargs <- P.try (do pushIndent; some (wExpr syn))

11391129 fc <- getFC

11401130 ist <- get

11411131 n <- case lastParse ist of

@@ -1143,11 +1133,8 @@ clause syn

11431133 Nothing -> fail "Invalid clause"

11441134 (do r <- rhs syn n

11451135 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1146− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1147− popIndent

1148− return x,

1149− do terminator

1150− return ([], [])]

1136+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1137+ <|> ([], []) <$ terminator

11511138 return $ PClauseR fc wargs r wheres) <|> (do

11521139 popIndent

11531140 reservedHL "with"

@@ -1158,19 +1145,16 @@ clause syn

11581145 let withs = concat ds

11591146 closeBlock

11601147 return $ PWithR fc wargs wval pn withs)

1161− <|> do ty <- try (do pushIndent

1162− ty <- simpleExpr syn

1163− symbol "<=="

1164− return ty)

1148+ <|> do ty <- P.try (do pushIndent

1149+ ty <- simpleExpr syn

1150+ symbol "<=="

1151+ return ty)

11651152 fc <- getFC

11661153 n_in <- fst <$> fnName; let n = expandNS syn n_in

11671154 r <- rhs syn n

11681155 let wsyn = syn { syn_namespace = [] }

1169− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1170− popIndent

1171− return x,

1172− do terminator

1173− return ([], [])]

1156+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1157+ <|> ([], []) <$ terminator

11741158 let capp = PLet fc RigW (sMN 0 "match") NoFC

11751159 ty

11761160 (PMatchApp fc n)

@@ -1178,7 +1162,7 @@ clause syn

11781162 ist <- get

11791163 put (ist { lastParse = Just n })

11801164 return $ PClause fc n capp [] r wheres

1181− <|> do (l, op, nfc) <- try (do

1165+ <|> do (l, op, nfc) <- P.try (do

11821166 pushIndent

11831167 l <- argExpr syn

11841168 (op, nfc) <- symbolicOperatorFC

@@ -1191,11 +1175,8 @@ clause syn

11911175 wargs <- many (wExpr syn)

11921176 (do rs <- rhs syn n

11931177 let wsyn = syn { syn_namespace = [] }

1194− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1195− popIndent

1196− return x,

1197− do terminator

1198− return ([], [])]

1178+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1179+ <|> ([], []) <$ terminator

11991180 ist <- get

12001181 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]

12011182 put (ist { lastParse = Just n })

@@ -1215,18 +1196,15 @@ clause syn

12151196 <|> do pushIndent

12161197 (n_in, nfc) <- fnName; let n = expandNS syn n_in

12171198 fc <- getFC

1218− args <- many (try (implicitArg (syn { inPattern = True } ))

1219− <|> try (constraintArg (syn { inPattern = True }))

1199+ args <- many (P.try (implicitArg (syn { inPattern = True } ))

1200+ <|> P.try (constraintArg (syn { inPattern = True }))

12201201 <|> (fmap pexp (argExpr syn)))

12211202 wargs <- many (wExpr syn)

12221203 let capp = PApp fc (PRef nfc [nfc] n) args

12231204 (do r <- rhs syn n

12241205 let wsyn = syn { syn_namespace = [] }

1225− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1226− popIndent

1227− return x,

1228− do terminator

1229− return ([], [])]

1206+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1207+ <|> ([], []) <$ terminator

12301208 ist <- get

12311209 put (ist { lastParse = Just n })

12321210 return $ PClause fc n capp wargs r wheres) <|> (do

@@ -1243,9 +1221,9 @@ clause syn

12431221 return $ PWith fc n capp wargs wval pn withs)

12441222 <?> "function clause"

12451223 where

1246− optProof = option Nothing (do reservedHL "proof"

1247− n <- fnName

1248− return (Just n))

1224+ optProof = P.option Nothing (do reservedHL "proof"

1225+ n <- fnName

1226+ return (Just n))

12491227

12501228 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause

12511229 fillLHS n capp owargs (PClauseR fc wargs v ws)

@@ -1336,74 +1314,74 @@ Directive' ::= 'lib' CodeGen String_t

13361314@

13371315-}

13381316directive :: SyntaxInfo -> IdrisParser [PDecl]

1339−directive syn = do try (lchar '%' *> reserved "lib")

1317+directive syn = do P.try (lchar '%' *> reserved "lib")

13401318 cgn <- codegen_

13411319 lib <- fmap fst stringLiteral

13421320 return [PDirective (DLib cgn lib)]

1343− <|> do try (lchar '%' *> reserved "link")

1321+ <|> do P.try (lchar '%' *> reserved "link")

13441322 cgn <- codegen_; obj <- fst <$> stringLiteral

13451323 return [PDirective (DLink cgn obj)]

1346− <|> do try (lchar '%' *> reserved "flag")

1324+ <|> do P.try (lchar '%' *> reserved "flag")

13471325 cgn <- codegen_; flag <- fst <$> stringLiteral

13481326 return [PDirective (DFlag cgn flag)]

1349− <|> do try (lchar '%' *> reserved "include")

1327+ <|> do P.try (lchar '%' *> reserved "include")

13501328 cgn <- codegen_

13511329 hdr <- fst <$> stringLiteral

13521330 return [PDirective (DInclude cgn hdr)]

1353− <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName

1331+ <|> do P.try (lchar '%' *> reserved "hide"); n <- fst <$> fnName

13541332 return [PDirective (DHide n)]

1355− <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

1333+ <|> do P.try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

13561334 return [PDirective (DFreeze n)]

1357− <|> do try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []

1335+ <|> do P.try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []

13581336 return [PDirective (DThaw n)]

13591337 -- injectivity assertins are intended for debugging purposes

13601338 -- only, and won't be documented/could be removed at any point

1361− <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

1339+ <|> do P.try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

13621340 return [PDirective (DInjective n)]

13631341 -- Assert totality of something after definition. This is

13641342 -- here as a debugging aid, so commented out...

1365−-- <|> do try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName

1343+-- <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName

13661344-- return [PDirective (DSetTotal n)]

1367− <|> do try (lchar '%' *> reserved "access")

1345+ <|> do P.try (lchar '%' *> reserved "access")

13681346 acc <- accessibility

13691347 ist <- get

13701348 put ist { default_access = acc }

13711349 return [PDirective (DAccess acc)]

1372− <|> do try (lchar '%' *> reserved "default"); tot <- totality

1350+ <|> do P.try (lchar '%' *> reserved "default"); tot <- totality

13731351 i <- get

13741352 put (i { default_total = tot } )

13751353 return [PDirective (DDefault tot)]

1376− <|> do try (lchar '%' *> reserved "logging")

1354+ <|> do P.try (lchar '%' *> reserved "logging")

13771355 i <- fst <$> natural

13781356 return [PDirective (DLogging i)]

1379− <|> do try (lchar '%' *> reserved "dynamic")

1380− libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')

1357+ <|> do P.try (lchar '%' *> reserved "dynamic")

1358+ libs <- P.sepBy1 (fmap fst stringLiteral) (lchar ',')

13811359 return [PDirective (DDynamicLibs libs)]

1382− <|> do try (lchar '%' *> reserved "name")

1360+ <|> do P.try (lchar '%' *> reserved "name")

13831361 (ty, tyFC) <- fnName

1384− ns <- sepBy1 name (lchar ',')

1362+ ns <- P.sepBy1 name (lchar ',')

13851363 return [PDirective (DNameHint ty tyFC ns)]

1386− <|> do try (lchar '%' *> reserved "error_handlers")

1364+ <|> do P.try (lchar '%' *> reserved "error_handlers")

13871365 (fn, nfc) <- fnName

13881366 (arg, afc) <- fnName

1389− ns <- sepBy1 name (lchar ',')

1367+ ns <- P.sepBy1 name (lchar ',')

13901368 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]

1391− <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

1369+ <|> do P.try (lchar '%' *> reserved "language"); ext <- pLangExt;

13921370 return [PDirective (DLanguage ext)]

1393− <|> do try (lchar '%' *> reserved "deprecate")

1371+ <|> do P.try (lchar '%' *> reserved "deprecate")

13941372 n <- fst <$> fnName

1395− alt <- option "" (fst <$> stringLiteral)

1373+ alt <- P.option "" (fst <$> stringLiteral)

13961374 return [PDirective (DDeprecate n alt)]

1397− <|> do try (lchar '%' *> reserved "fragile")

1375+ <|> do P.try (lchar '%' *> reserved "fragile")

13981376 n <- fst <$> fnName

1399− alt <- option "" (fst <$> stringLiteral)

1377+ alt <- P.option "" (fst <$> stringLiteral)

14001378 return [PDirective (DFragile n alt)]

14011379 <|> do fc <- getFC

1402− try (lchar '%' *> reserved "used")

1380+ P.try (lchar '%' *> reserved "used")

14031381 fn <- fst <$> fnName

14041382 arg <- fst <$> iName []

14051383 return [PDirective (DUsed fc fn arg)]

1406− <|> do try (lchar '%' *> reserved "auto_implicits")

1384+ <|> do P.try (lchar '%' *> reserved "auto_implicits")

14071385 b <- on_off

14081386 return [PDirective (DAutoImplicits b)]

14091387 <?> "directive"

@@ -1440,12 +1418,12 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

14401418@

14411419 -}

14421420provider :: SyntaxInfo -> IdrisParser [PDecl]

1443−provider syn = do doc <- try (do (doc, _) <- docstring syn

1444− fc1 <- getFC

1445− lchar '%'

1446− fc2 <- reservedFC "provide"

1447− highlightP (spanFC fc1 fc2) AnnKeyword

1448− return doc)

1421+provider syn = do doc <- P.try (do (doc, _) <- docstring syn

1422+ fc1 <- getFC

1423+ lchar '%'

1424+ fc2 <- reservedFC "provide"

1425+ highlightP (spanFC fc1 fc2) AnnKeyword

1426+ return doc)

14491427 provideTerm doc <|> providePostulate doc

14501428 <?> "type provider"

14511429 where provideTerm doc =

@@ -1469,7 +1447,7 @@ Transform ::= '%' 'transform' Expr '==>' Expr

14691447@

14701448-}

14711449transform :: SyntaxInfo -> IdrisParser [PDecl]

1472−transform syn = do try (lchar '%' *> reserved "transform")

1450+transform syn = do P.try (lchar '%' *> reserved "transform")

14731451 -- leave it unchecked, until we work out what this should

14741452 -- actually mean...

14751453-- safety <- option True (do reserved "unsafe"

@@ -1489,10 +1467,10 @@ RunElabDecl ::= '%' 'runElab' Expr

14891467-}

14901468runElabDecl :: SyntaxInfo -> IdrisParser PDecl

14911469runElabDecl syn =

1492− do kwFC <- try (do fc <- getFC

1493− lchar '%'

1494− fc' <- reservedFC "runElab"

1495− return (spanFC fc fc'))

1470+ do kwFC <- P.try (do fc <- getFC

1471+ lchar '%'

1472+ fc' <- reservedFC "runElab"

1473+ return (spanFC fc fc'))

14961474 script <- expr syn <?> "elaborator script"

14971475 highlightP kwFC AnnKeyword

14981476 return $ PRunElabDecl kwFC script (syn_namespace syn)

@@ -1500,19 +1478,19 @@ runElabDecl syn =

15001478

15011479{- * Loading and parsing -}

15021480{-| Parses an expression from input -}

1503−parseExpr :: IState -> String -> Result PTerm

1481+parseExpr :: IState -> String -> P.Result PTerm

15041482parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

15051483

15061484{-| Parses a constant form input -}

1507−parseConst :: IState -> String -> Result Const

1485+parseConst :: IState -> String -> P.Result Const

15081486parseConst st = runparser (fmap fst constant) st "(input)"

15091487

15101488{-| Parses a tactic from input -}

1511−parseTactic :: IState -> String -> Result PTactic

1489+parseTactic :: IState -> String -> P.Result PTactic

15121490parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

15131491

15141492{-| Parses a do-step from input (used in the elab shell) -}

1515−parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

1493+parseElabShellStep :: IState -> String -> P.Result (Either ElabShellCmd PDo)

15161494parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"

15171495 where elabShellCmd = char ':' >>

15181496 (reserved "qed" >> pure EQED ) <|>

@@ -1525,7 +1503,7 @@ parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left

15251503 (expressionTactic ["search"] ESearch ) <|>

15261504 (do reserved "doc"

15271505 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1528− eof

1506+ P.eof

15291507 return (EDocStr doc))

15301508 <?> "elab command"

15311509 expressionTactic cmds tactic =

@@ -1536,26 +1514,26 @@ parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left

15361514 spaced parser = indentGt *> parser

15371515

15381516-- | Parse module header and imports

1539−parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

1517+parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe P.Delta)

15401518parseImports fname input

15411519 = do i <- getIState

1542− case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

1543− Failure (ErrInfo err _) -> ifail $ show err

1544− Success (x, annots, i) ->

1520+ case P.parseString (runInnerParser (evalStateT imports i)) (P.Directed (UTF8.fromString fname) 0 0 0 0) input of

1521+ P.Failure (P.ErrInfo err _) -> ifail $ show err

1522+ P.Success (x, annots, i) ->

15451523 do putIState i

15461524 fname' <- runIO $ Dir.makeAbsolute fname

15471525 sendHighlighting $ addPath annots fname'

15481526 return x

15491527 where imports :: IdrisParser ((Maybe (Docstring ()), [String],

15501528 [ImportInfo],

1551− Maybe Delta),

1529+ Maybe P.Delta),

15521530 [(FC, OutputAnnotation)], IState)

15531531 imports = do optional shebang

15541532 whiteSpace

15551533 (mdoc, mname, annots) <- moduleHeader

15561534 ps_exp <- many import_

1557− mrk <- mark

1558− isEof <- lookAheadMatches eof

1535+ mrk <- P.mark

1536+ isEof <- lookAheadMatches P.eof

15591537 let mrk' = if isEof

15601538 then Nothing

15611539 else Just mrk

@@ -1572,7 +1550,7 @@ parseImports fname input

15721550 addPath (annot:annots) path = annot : addPath annots path

15731551

15741552 shebang :: IdrisParser ()

1575− shebang = string "#!" *> many (satisfy $ not . isEol) *> eol *> pure ()

1553+ shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()

15761554

15771555-- | There should be a better way of doing this...

15781556findFC :: Doc -> (FC, String)

@@ -1596,12 +1574,12 @@ fixColour True doc = doc

15961574

15971575-- | A program is a list of declarations, possibly with associated

15981576-- documentation strings.

1599−parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

1577+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe P.Delta ->

16001578 Idris [PDecl]

16011579parseProg syn fname input mrk

16021580 = do i <- getIState

16031581 case runparser mainProg i fname input of

1604− Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta

1582+ P.Failure (P.ErrInfo doc _) -> do -- FIXME: Get error location from trifecta

16051583 -- this can't be the solution!

16061584 -- Issue #1575 on the issue tracker.

16071585 -- https://github.com/idris-lang/Idris-dev/issues/1575

@@ -1609,17 +1587,17 @@ parseProg syn fname input mrk

16091587 i <- getIState

16101588 case idris_outputmode i of

16111589 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1612− IdeMode n h -> iWarn fc (P.text msg)

1590+ IdeMode n h -> iWarn fc (Util.Pretty.text msg)

16131591 putIState (i { errSpan = Just fc })

16141592 return []

1615− Success (x, i) -> do putIState i

1616− reportParserWarnings

1617− return $ collect x

1593+ P.Success (x, i) -> do putIState i

1594+ reportParserWarnings

1595+ return $ collect x

16181596 where mainProg :: IdrisParser ([PDecl], IState)

16191597 mainProg = case mrk of

16201598 Nothing -> do i <- get; return ([], i)

16211599 Just mrk -> do

1622− release mrk

1600+ P.release mrk

16231601 ds <- prog syn

16241602 i' <- get

16251603 return (ds, i')

src/Idris/Parser/Data.hs+28−28

@@ -22,16 +22,16 @@ import Control.Applicative

2222import Control.Monad.State.Strict

2323import Data.List

2424import Data.Maybe

25−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

26− stringLiteral, symbol, whiteSpace)

25+import Text.Trifecta ((<?>))

26+import qualified Text.Trifecta as P

2727

2828{- | Parses a record type declaration

2929Record ::=

3030 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

3131-}

3232record :: SyntaxInfo -> IdrisParser PDecl

33−record syn = do (doc, paramDocs, acc, opts) <- try (do

34− (doc, paramDocs) <- option noDocs docComment

33+record syn = do (doc, paramDocs, acc, opts) <- P.try (do

34+ (doc, paramDocs) <- P.option noDocs docComment

3535 ist <- get

3636 let doc' = annotCode (tryFullExpr syn ist) doc

3737 paramDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

@@ -45,7 +45,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

4545 let tyn = expandNS syn tyn_in

4646 let rsyn = syn { syn_namespace = show (nsroot tyn) :

4747 syn_namespace syn }

48− params <- manyTill (recordParameter rsyn) (reservedHL "where")

48+ params <- P.manyTill (recordParameter rsyn) (reservedHL "where")

4949 (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn

5050 let fnames = map (expandNS rsyn) (mapMaybe getName fields)

5151 case cname of

@@ -62,8 +62,8 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

6262 ist <- get

6363 fc <- getFC

6464

65− (constructorName, constructorDoc) <- option (Nothing, emptyDocstring)

66− (do (doc, _) <- option noDocs docComment

65+ (constructorName, constructorDoc) <- P.option (Nothing, emptyDocstring)

66+ (do (doc, _) <- P.option noDocs docComment

6767 n <- constructor

6868 return (Just n, doc))

6969

@@ -170,8 +170,8 @@ SimpleConstructorList ::=

170170-}

171171data_ :: SyntaxInfo -> IdrisParser PDecl

172172data_ syn = checkDeclFixity $

173− do (doc, argDocs, acc, dataOpts) <- try (do

174− (doc, argDocs) <- option noDocs docComment

173+ do (doc, argDocs, acc, dataOpts) <- P.try (do

174+ (doc, argDocs) <- P.option noDocs docComment

175175 pushIndent

176176 acc <- accessibility

177177 elim <- dataOpts []

@@ -184,10 +184,10 @@ data_ syn = checkDeclFixity $

184184 return (doc', argDocs', acc, dataOpts))

185185 fc <- getFC

186186 (tyn_in, nfc) <- fnName

187− (do try (lchar ':')

187+ (do P.try (lchar ':')

188188 ty <- typeExpr (allowImp syn)

189189 let tyn = expandNS syn tyn_in

190− d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

190+ d <- P.option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

191191 reservedHL "where"

192192 cons <- indentedBlock (constructor syn)

193193 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

@@ -199,19 +199,19 @@ data_ syn = checkDeclFixity $

199199 return x)

200200 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

201201 let tyn = expandNS syn tyn_in

202− d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

203− try (lchar '=') <|> do reservedHL "where"

204− let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

205− let n = show tyn_in ++ " "

206− let s = kw ++ n

207− let as = unwords (map show args) ++ " "

208− let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

209− let ss = concat (intersperse " -> " $ map (const "Type") args)

210− let fix1 = s ++ as ++ " = ..."

211− let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

212− let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

213− fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

214− cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

202+ d <- P.option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

203+ P.try (lchar '=') <|> do reservedHL "where"

204+ let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

205+ let n = show tyn_in ++ " "

206+ let s = kw ++ n

207+ let as = unwords (map show args) ++ " "

208+ let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

209+ let ss = concat (intersperse " -> " $ map (const "Type") args)

210+ let fix1 = s ++ as ++ " = ..."

211+ let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

212+ let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

213+ fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

214+ cons <- P.sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

215215 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

216216 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

217217 do let cty = bindArgs cargs conty

@@ -238,12 +238,12 @@ data_ syn = checkDeclFixity $

238238-}

239239constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])

240240constructor syn

241− = do (doc, argDocs) <- option noDocs docComment

241+ = do (doc, argDocs) <- P.option noDocs docComment

242242 (cn_in, nfc) <- fnName; fc <- getFC

243243 let cn = expandNS syn cn_in

244244 lchar ':'

245− fs <- option [] (do lchar '%'; reserved "erase"

246− sepBy1 (fst <$> name) (lchar ','))

245+ fs <- P.option [] (do lchar '%'; reserved "erase"

246+ P.sepBy1 (fst <$> name) (lchar ','))

247247 ty <- typeExpr (allowImp syn)

248248 ist <- get

249249 let doc' = annotCode (tryFullExpr syn ist) doc

@@ -258,7 +258,7 @@ constructor syn

258258-}

259259simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])

260260simpleConstructor syn

261− = do (doc, _) <- option noDocs (try docComment)

261+ = do (doc, _) <- P.option noDocs (P.try docComment)

262262 ist <- get

263263 let doc' = annotCode (tryFullExpr syn ist) doc

264264 (cn_in, nfc) <- fnName

src/Idris/Parser/Expr.hs+152−153

@@ -25,8 +25,8 @@ import Data.Function (on)

2525import Data.List

2626import Data.Maybe

2727import Text.Parser.Expression

28−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

29− stringLiteral, symbol, whiteSpace)

28+import Text.Trifecta ((<?>))

29+import qualified Text.Trifecta as P

3030

3131-- | Allow implicit type declarations

3232allowImp :: SyntaxInfo -> SyntaxInfo

@@ -53,15 +53,15 @@ allowConstr syn = syn { constraintAllowed = True }

5353 -}

5454fullExpr :: SyntaxInfo -> IdrisParser PTerm

5555fullExpr syn = do x <- expr syn

56− eof

56+ P.eof

5757 i <- get

5858 return $ debindApp syn (desugar syn i x)

5959

6060tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

6161tryFullExpr syn st input =

6262 case runparser (fullExpr syn) st "" input of

63− Success tm -> Right tm

64− Failure e -> Left (Msg (show e))

63+ P.Success tm -> Right tm

64+ P.Failure e -> Left (Msg (show e))

6565

6666{- | Parses an expression

6767@

@@ -89,7 +89,7 @@ Expr' ::= "External (User-defined) Syntax"

8989@

9090 -}

9191expr' :: SyntaxInfo -> IdrisParser PTerm

92−expr' syn = try (externalExpr syn)

92+expr' syn = P.try (externalExpr syn)

9393 <|> internalExpr syn

9494 <?> "expression"

9595

@@ -140,9 +140,9 @@ data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting in

140140

141141extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

142142extension syn ns rules =

143− choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

143+ P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

144144 case head rs of -- can never be []

145− Rule (symb:_) _ _ -> try $ do

145+ Rule (symb:_) _ _ -> P.try $ do

146146 n <- extensionSymbol symb

147147 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

148148 -- If we have more than one Rule in this bucket, our grammar is

@@ -397,8 +397,8 @@ SimpleExpr ::=

397397-}

398398simpleExpr :: SyntaxInfo -> IdrisParser PTerm

399399simpleExpr syn =

400− try (simpleExternalExpr syn)

401− <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

400+ P.try (simpleExternalExpr syn)

401+ <|> do (x, FC f (l, c) end) <- P.try (lchar '?' *> name)

402402 return (PMetavar (FC f (l, c-1) end) x)

403403 <|> do lchar '%'; fc <- getFC; reserved "implementation"; return (PResolveTC fc)

404404 <|> do lchar '%'; fc <- getFC; reserved "instance"

@@ -407,7 +407,7 @@ simpleExpr syn =

407407 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

408408 <|> proofExpr syn

409409 <|> tacticsExpr syn

410− <|> try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)

410+ <|> P.try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)

411411 <|> do fc <- reservedFC "AnyType"; return $ PUniverse fc AllTypes

412412 <|> PType <$> reservedFC "Type"

413413 <|> do fc <- reservedFC "UniqueType"; return $ PUniverse fc UniqueType

@@ -420,11 +420,11 @@ simpleExpr syn =

420420 [pexp (PConstant NoFC (Str (show str)))])

421421 <|> do (x, fc) <- fnName

422422 if inPattern syn

423− then option (PRef fc [fc] x)

424− (do reservedOp "@"

425− s <- simpleExpr syn

426− fcIn <- getFC

427− return (PAs fcIn x s))

423+ then P.option (PRef fc [fc] x)

424+ (do reservedOp "@"

425+ s <- simpleExpr syn

426+ fcIn <- getFC

427+ return (PAs fcIn x s))

428428 else return (PRef fc [fc] x)

429429 <|> idiom syn

430430 <|> listExpr syn

@@ -467,22 +467,22 @@ bracketed' open syn =

467467 do (FC f start (l, c)) <- getFC

468468 lchar ')'

469469 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

470− <|> try (dependentPair TypeOrTerm [] open syn)

471− <|> try (do (opName, fc) <- operatorName

472− guardNotPrefix opName

473−

474− e <- expr syn

475− lchar ')'

476− return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

477− (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),

478− pexp e]))

479− <|> try (simpleExpr syn >>= \l ->

480− try (do (opName, _) <- operatorName

481− lchar ')'

482− fc <- getFC

483− return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

484− (PApp fc (PRef fc [] opName) [pexp l,

485− pexp (PRef fc [] (sMN 1000 "ARG"))]))

470+ <|> P.try (dependentPair TypeOrTerm [] open syn)

471+ <|> P.try (do (opName, fc) <- operatorName

472+ guardNotPrefix opName

473+

474+ e <- expr syn

475+ lchar ')'

476+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

477+ (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),

478+ pexp e]))

479+ <|> P.try (simpleExpr syn >>= \l ->

480+ P.try (do (opName, _) <- operatorName

481+ lchar ')'

482+ fc <- getFC

483+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

484+ (PApp fc (PRef fc [] opName) [pexp l,

485+ pexp (PRef fc [] (sMN 1000 "ARG"))]))

486486 <|> bracketedExpr syn open l)

487487 <|> do l <- expr (allowConstr syn)

488488 bracketedExpr (allowConstr syn) open l

@@ -510,14 +510,14 @@ dependentPair pun prev openFC syn =

510510 IsTerm -> exprPart False

511511 TypeOrTerm -> nametypePart <|> namePart <|> exprPart False

512512 where nametypePart = do

513− (ln, lnfc, colonFC) <- try $ do

513+ (ln, lnfc, colonFC) <- P.try $ do

514514 (ln, lnfc) <- name

515515 colonFC <- lcharFC ':'

516516 return (ln, lnfc, colonFC)

517517 lty <- expr' syn

518518 starsFC <- reservedOpFC "**"

519519 dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn

520− namePart = try $ do

520+ namePart = P.try $ do

521521 (ln, lnfc) <- name

522522 starsFC <- reservedOpFC "**"

523523 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn

@@ -590,7 +590,7 @@ modifyConst syn fc x = x

590590@

591591-}

592592alt :: SyntaxInfo -> IdrisParser PTerm

593−alt syn = do symbol "(|"; alts <- sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"

593+alt syn = do symbol "(|"; alts <- P.sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"

594594 return (PAlternative [] FirstSuccess alts)

595595

596596{- | Parses a possibly hidden simple expression

@@ -615,7 +615,7 @@ UnifyLog ::=

615615 ;

616616-}

617617unifyLog :: SyntaxInfo -> IdrisParser PTerm

618−unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")

618+unifyLog syn = do (FC fn (sl, sc) kwEnd) <- P.try (lchar '%' *> reservedFC "unifyLog")

619619 tm <- simpleExpr syn

620620 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

621621 return (PUnifyLog tm)

@@ -627,7 +627,7 @@ RunTactics ::=

627627 ;

628628-}

629629runElab :: SyntaxInfo -> IdrisParser PTerm

630−runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")

630+runElab syn = do (FC fn (sl, sc) kwEnd) <- P.try (lchar '%' *> reservedFC "runElab")

631631 fc <- getFC

632632 tm <- simpleExpr syn

633633 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

@@ -641,7 +641,7 @@ Disamb ::=

641641-}

642642disamb :: SyntaxInfo -> IdrisParser PTerm

643643disamb syn = do kw <- reservedFC "with"

644− ns <- sepBy1 (fst <$> name) (lchar ',')

644+ ns <- P.sepBy1 (fst <$> name) (lchar ',')

645645 tm <- expr' syn

646646 highlightP kw AnnKeyword

647647 return (PDisamb (map tons ns) tm)

@@ -656,7 +656,7 @@ NoImplicits ::=

656656@

657657-}

658658noImplicits :: SyntaxInfo -> IdrisParser PTerm

659−noImplicits syn = do try (lchar '%' *> reserved "noImplicits")

659+noImplicits syn = do P.try (lchar '%' *> reserved "noImplicits")

660660 tm <- simpleExpr syn

661661 return (PNoImplicits tm)

662662 <?> "no implicits expression"

@@ -675,7 +675,7 @@ MatchApp ::=

675675-}

676676app :: SyntaxInfo -> IdrisParser PTerm

677677app syn = do f <- simpleExpr syn

678− (do try $ reservedOp "<=="

678+ (do P.try $ reservedOp "<=="

679679 fc <- getFC

680680 ff <- fst <$> fnName

681681 return (PLet fc RigW (sMN 0 "match") NoFC

@@ -737,8 +737,8 @@ implicitArg :: SyntaxInfo -> IdrisParser PArg

737737implicitArg syn = do lchar '{'

738738 (n, nfc) <- name

739739 fc <- getFC

740− v <- option (PRef nfc [nfc] n) (do lchar '='

741− expr syn)

740+ v <- P.option (PRef nfc [nfc] n) (do lchar '='

741+ expr syn)

742742 lchar '}'

743743 return (pimp n v True)

744744 <?> "implicit function argument"

@@ -800,8 +800,8 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)

800800-}

801801namequote :: SyntaxInfo -> IdrisParser PTerm

802802namequote syn = do (startFC, res) <-

803− try (do fc <- symbolFC "`{{"

804− return (fc, False)) <|>

803+ P.try (do fc <- symbolFC "`{{"

804+ return (fc, False)) <|>

805805 (do fc <- symbolFC "`{"

806806 return (fc, True))

807807 (n, nfc) <- fnName

@@ -871,11 +871,10 @@ recordType syn =

871871 <?> "field setter"

872872

873873 fieldGet :: IdrisParser [Name]

874− fieldGet = sepBy1 (fst <$> fnName) (symbol "->")

874+ fieldGet = P.sepBy1 (fst <$> fnName) (symbol "->")

875875

876876 fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])

877− fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')

878− return (Left fs))

877+ fieldGetOrSet = P.try (Left <$> P.sepBy1 fieldSet (lchar ','))

879878 <|> do f <- fieldGet

880879 return (Right f)

881880

@@ -942,15 +941,15 @@ LambdaTail ::=

942941-}

943942lambda :: SyntaxInfo -> IdrisParser PTerm

944943lambda syn = do lchar '\\' <?> "lambda expression"

945− ((do xt <- try $ tyOptDeclList (disallowImp syn)

944+ ((do xt <- P.try $ tyOptDeclList (disallowImp syn)

946945 fc <- getFC

947946 sc <- lambdaTail

948947 return (bindList (\r -> PLam fc) xt sc))

949948 <|>

950− (do ps <- sepBy (do fc <- getFC

951− e <- simpleExpr (disallowImp (syn { inPattern = True }))

952− return (fc, e))

953− (lchar ',')

949+ (do ps <- P.sepBy (do fc <- getFC

950+ e <- simpleExpr (disallowImp (syn { inPattern = True }))

951+ return (fc, e))

952+ (lchar ',')

954953 sc <- lambdaTail

955954 return (pmList (zip [0..] ps) sc)))

956955 <?> "lambda expression"

@@ -996,11 +995,11 @@ TypeSig' ::=

996995@

997996 -}

998997let_ :: SyntaxInfo -> IdrisParser PTerm

999−let_ syn = try (do kw <- reservedFC "let"

1000− ls <- indentedBlock (let_binding syn)

1001− kw' <- reservedFC "in"; sc <- expr syn

1002− highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1003− return (buildLets ls sc))

998+let_ syn = P.try (do kw <- reservedFC "let"

999+ ls <- indentedBlock (let_binding syn)

1000+ kw' <- reservedFC "in"; sc <- expr syn

1001+ highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1002+ return (buildLets ls sc))

10041003 <?> "let binding"

10051004 where buildLets [] sc = sc

10061005 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

@@ -1010,11 +1009,11 @@ let_ syn = try (do kw <- reservedFC "let"

10101009

10111010let_binding syn = do fc <- getFC;

10121011 pat <- expr' (syn { inPattern = True })

1013− ty <- option Placeholder (do lchar ':'; expr' syn)

1012+ ty <- P.option Placeholder (do lchar ':'; expr' syn)

10141013 lchar '='

10151014 v <- expr (syn { withAppAllowed = isVar pat })

1016− ts <- option [] (do lchar '|'

1017− sepBy1 (do_alt syn) (lchar '|'))

1015+ ts <- P.option [] (do lchar '|'

1016+ P.sepBy1 (do_alt syn) (lchar '|'))

10181017 return (fc,pat,ty,v,ts)

10191018 where isVar (PRef _ _ _) = True

10201019 isVar _ = False

@@ -1079,7 +1078,7 @@ bindsymbol opts st syn

10791078 return (Exp opts st False RigW)

10801079

10811080explicitPi opts st syn

1082− = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1081+ = do xt <- P.try (lchar '(' *> typeDeclList syn <* lchar ')')

10831082 binder <- bindsymbol opts st syn

10841083 sc <- expr (allowConstr syn)

10851084 return (bindList (\r -> PPi (binder { pcount = r })) xt sc)

@@ -1147,9 +1146,9 @@ unboundPiNoConstraint opts st syn = do

11471146 x <- opExpr syn

11481147 (do binder <- bindsymbol opts st syn

11491148 sc <- expr syn

1150− notFollowedBy $ reservedOp "=>"

1149+ P.notFollowedBy $ reservedOp "=>"

11511150 return (PPi binder (sUN "__pi_arg") NoFC x sc))

1152− <|> do notFollowedBy $ reservedOp "=>"

1151+ <|> do P.notFollowedBy $ reservedOp "=>"

11531152 return x

11541153

11551154

@@ -1158,10 +1157,10 @@ pi syn =

11581157 do opts <- piOpts syn

11591158 st <- static

11601159 explicitPi opts st syn

1161− <|> try (do lchar '{'; implicitPi opts st syn)

1160+ <|> P.try (do lchar '{'; implicitPi opts st syn)

11621161 <|> if constraintAllowed syn

1163− then try (unboundPiNoConstraint opts st syn)

1164− <|> constraintPi opts st syn

1162+ then P.try (unboundPiNoConstraint opts st syn)

1163+ <|> constraintPi opts st syn

11651164 else unboundPi opts st syn

11661165 <?> "dependent type signature"

11671166

@@ -1186,22 +1185,22 @@ ConstraintList ::=

11861185@

11871186-}

11881187constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1189−constraintList syn = try (constraintList1 syn)

1188+constraintList syn = P.try (constraintList1 syn)

11901189 <|> return []

11911190

11921191constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1193−constraintList1 syn = try (do lchar '('

1194− tys <- sepBy1 nexpr (lchar ',')

1195− lchar ')'

1196− reservedOp "=>"

1197− return tys)

1198− <|> try (do t <- opExpr (disallowImp syn)

1199− reservedOp "=>"

1200− return [(RigW, defname, NoFC, t)])

1192+constraintList1 syn = P.try (do lchar '('

1193+ tys <- P.sepBy1 nexpr (lchar ',')

1194+ lchar ')'

1195+ reservedOp "=>"

1196+ return tys)

1197+ <|> P.try (do t <- opExpr (disallowImp syn)

1198+ reservedOp "=>"

1199+ return [(RigW, defname, NoFC, t)])

12011200 <?> "type constraint list"

1202− where nexpr = try (do (n, fc) <- name; lchar ':'

1203− e <- expr (disallowImp syn)

1204− return (RigW, n, fc, e))

1201+ where nexpr = P.try (do (n, fc) <- name; lchar ':'

1202+ e <- expr (disallowImp syn)

1203+ return (RigW, n, fc, e))

12051204 <|> do e <- expr (disallowImp syn)

12061205 return (RigW, defname, NoFC, e)

12071206 defname = sMN 0 "constraint"

@@ -1222,13 +1221,13 @@ FunctionSignatureList ::=

12221221@

12231222-}

12241223typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1225−typeDeclList syn = try (sepBy1 (do rig <- option RigW rigCount

1226− (x, xfc) <- fnName

1227− lchar ':'

1228− t <- typeExpr (disallowImp syn)

1229− return (rig, x, xfc, t))

1230− (lchar ','))

1231− <|> do ns <- sepBy1 name (lchar ',')

1224+typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount

1225+ (x, xfc) <- fnName

1226+ lchar ':'

1227+ t <- typeExpr (disallowImp syn)

1228+ return (rig, x, xfc, t))

1229+ (lchar ','))

1230+ <|> do ns <- P.sepBy1 name (lchar ',')

12321231 lchar ':'

12331232 t <- typeExpr (disallowImp syn)

12341233 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)

@@ -1250,11 +1249,11 @@ NameOrPlaceHolder ::= Name | '_';

12501249@

12511250-}

12521251tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1253−tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1254− t <- option Placeholder (do lchar ':'

1255− expr syn)

1256− return (RigW, x, fc, t))

1257− (lchar ',')

1252+tyOptDeclList syn = P.sepBy1 (do (x, fc) <- nameOrPlaceholder

1253+ t <- P.option Placeholder (do lchar ':'

1254+ expr syn)

1255+ return (RigW, x, fc, t))

1256+ (lchar ',')

12581257 <?> "type declaration list"

12591258 where nameOrPlaceholder :: IdrisParser (Name, FC)

12601259 nameOrPlaceholder = fnName

@@ -1286,12 +1285,12 @@ ExprList ::=

12861285listExpr :: SyntaxInfo -> IdrisParser PTerm

12871286listExpr syn = do (FC f (l, c) _) <- getFC

12881287 lchar '['; fc <- getFC;

1289− (try . token $ do (char ']' <?> "end of list expression")

1290− (FC _ _ (l', c')) <- getFC

1291− return (mkNil (FC f (l, c) (l', c'))))

1288+ (P.try . P.token $ do (char ']' <?> "end of list expression")

1289+ (FC _ _ (l', c')) <- getFC

1290+ return (mkNil (FC f (l, c) (l', c'))))

12921291 <|> (do x <- expr (syn { withAppAllowed = False }) <?> "expression"

1293− (do try (lchar '|') <?> "list comprehension"

1294− qs <- sepBy1 (do_ syn) (lchar ',')

1292+ (do P.try (lchar '|') <?> "list comprehension"

1293+ qs <- P.sepBy1 (do_ syn) (lchar ',')

12951294 lchar ']'

12961295 return (PDoBlock (map addGuard qs ++

12971296 [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))

@@ -1350,53 +1349,53 @@ Do ::=

13501349-}

13511350do_ :: SyntaxInfo -> IdrisParser PDo

13521351do_ syn

1353− = try (do kw <- reservedFC "let"

1354− (i, ifc) <- name

1355− ty <- option Placeholder (do lchar ':'

1356− expr' syn)

1357− reservedOp "="

1358− fc <- getFC

1359− e <- expr syn

1360− highlightP kw AnnKeyword

1361− return (DoLet fc RigW i ifc ty e))

1362− <|> try (do kw <- reservedFC "let"

1363− i <- expr' syn

1364− reservedOp "="

1365− fc <- getFC

1366− sc <- expr syn

1367− highlightP kw AnnKeyword

1368− return (DoLetP fc i sc))

1369− <|> try (do kw <- reservedFC "rewrite"

1370− fc <- getFC

1371− sc <- expr syn

1372− highlightP kw AnnKeyword

1373− return (DoRewrite fc sc))

1374− <|> try (do (i, ifc) <- name

1375− symbol "<-"

1376− fc <- getFC

1377− e <- expr (syn { withAppAllowed = False });

1378− option (DoBind fc i ifc e)

1379− (do lchar '|'

1380− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1381− return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1382− <|> try (do i <- expr' syn

1383− symbol "<-"

1384− fc <- getFC

1385− e <- expr (syn { withAppAllowed = False });

1386− option (DoBindP fc i e [])

1387− (do lchar '|'

1388− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1389− return (DoBindP fc i e ts)))

1352+ = P.try (do kw <- reservedFC "let"

1353+ (i, ifc) <- name

1354+ ty <- P.option Placeholder (do lchar ':'

1355+ expr' syn)

1356+ reservedOp "="

1357+ fc <- getFC

1358+ e <- expr syn

1359+ highlightP kw AnnKeyword

1360+ return (DoLet fc RigW i ifc ty e))

1361+ <|> P.try (do kw <- reservedFC "let"

1362+ i <- expr' syn

1363+ reservedOp "="

1364+ fc <- getFC

1365+ sc <- expr syn

1366+ highlightP kw AnnKeyword

1367+ return (DoLetP fc i sc))

1368+ <|> P.try (do kw <- reservedFC "rewrite"

1369+ fc <- getFC

1370+ sc <- expr syn

1371+ highlightP kw AnnKeyword

1372+ return (DoRewrite fc sc))

1373+ <|> P.try (do (i, ifc) <- name

1374+ symbol "<-"

1375+ fc <- getFC

1376+ e <- expr (syn { withAppAllowed = False });

1377+ P.option (DoBind fc i ifc e)

1378+ (do lchar '|'

1379+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1380+ return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1381+ <|> P.try (do i <- expr' syn

1382+ symbol "<-"

1383+ fc <- getFC

1384+ e <- expr (syn { withAppAllowed = False });

1385+ P.option (DoBindP fc i e [])

1386+ (do lchar '|'

1387+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1388+ return (DoBindP fc i e ts)))

13901389 <|> do e <- expr syn

13911390 fc <- getFC

13921391 return (DoExp fc e)

13931392 <?> "do block expression"

13941393

13951394do_alt syn = do l <- expr' syn

1396− option (Placeholder, l)

1397− (do symbol "=>"

1398− r <- expr' syn

1399− return (l, r))

1395+ P.option (Placeholder, l)

1396+ (do symbol "=>"

1397+ r <- expr' syn

1398+ return (l, r))

14001399

14011400{- | Parses an expression in idiom brackets

14021401@

@@ -1451,14 +1450,14 @@ constants =

14511450

14521451-- | Parse a constant and its source span

14531452constant :: IdrisParser (Idris.Core.TT.Const, FC)

1454−constant = choice [ do fc <- reservedFC name; return (ty, fc)

1455− | (name, ty) <- constants

1456− ]

1457− <|> do (f, fc) <- try float; return (Fl f, fc)

1453+constant = P.choice [ do fc <- reservedFC name; return (ty, fc)

1454+ | (name, ty) <- constants

1455+ ]

1456+ <|> do (f, fc) <- P.try float; return (Fl f, fc)

14581457 <|> do (i, fc) <- natural; return (BI i, fc)

14591458 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

14601459 <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1461− <|> do (c, fc) <- try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

1460+ <|> do (c, fc) <- P.try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

14621461 <?> "constant or literal"

14631462

14641463{- | Parses a verbatim multi-line string literal (triple-quoted)

@@ -1470,11 +1469,11 @@ VerbatimString_t ::=

14701469@

14711470 -}

14721471verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1473−verbatimStringLiteral = token $ do (FC f start _) <- getFC

1474− try $ string "\"\"\""

1475− str <- manyTill anyChar $ try (string "\"\"\"")

1476− (FC _ _ end) <- getFC

1477− return (str, FC f start end)

1472+verbatimStringLiteral = P.token $ do (FC f start _) <- getFC

1473+ P.try $ string "\"\"\""

1474+ str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")

1475+ (FC _ _ end) <- getFC

1476+ return (str, FC f start end)

14781477

14791478{- | Parses a static modifier

14801479

@@ -1545,7 +1544,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

15451544tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

15461545tactics =

15471546 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1548− do ns <- sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

1547+ do ns <- P.sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

15491548 , noArgs ["intros"] Intros

15501549 , noArgs ["unfocus"] Unfocus

15511550 , (["refine"], Just ExprTArg, const $

@@ -1593,7 +1592,7 @@ tactics =

15931592 , noArgs ["trivial"] Trivial

15941593 , noArgs ["unify"] DoUnify

15951594 , (["search"], Nothing, const $

1596− do depth <- option 10 $ fst <$> natural

1595+ do depth <- P.option 10 $ fst <$> natural

15971596 return (ProofSearch True True (fromInteger depth) Nothing [] []))

15981597 , noArgs ["implementation"] TCImplementation

15991598 , noArgs ["solve"] Solve

@@ -1614,7 +1613,7 @@ tactics =

16141613 , ([":doc"], Just ExprTArg, const $

16151614 do whiteSpace

16161615 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1617− eof

1616+ P.eof

16181617 return (TDocStr doc))

16191618 ]

16201619 where

@@ -1630,12 +1629,12 @@ tactics =

16301629

16311630

16321631tactic :: SyntaxInfo -> IdrisParser PTactic

1633−tactic syn = choice [ do choice (map reserved names); parser syn

1634− | (names, _, parser) <- tactics ]

1632+tactic syn = P.choice [ do P.choice (map reserved names); parser syn

1633+ | (names, _, parser) <- tactics ]

16351634 <|> do lchar '{'

16361635 t <- tactic syn;

16371636 lchar ';';

1638− ts <- sepBy1 (tactic syn) (lchar ';')

1637+ ts <- P.sepBy1 (tactic syn) (lchar ';')

16391638 lchar '}'

16401639 return $ TSeq t (mergeSeq ts)

16411640 <|> ((lchar ':' >> empty) <?> "prover command")

@@ -1648,5 +1647,5 @@ tactic syn = choice [ do choice (map reserved names); parser syn

16481647-- | Parses a tactic as a whole

16491648fullTactic :: SyntaxInfo -> IdrisParser PTactic

16501649fullTactic syn = do t <- tactic syn

1651− eof

1650+ P.eof

16521651 return t

src/Idris/Parser/Helpers.hs+82−82

@@ -35,34 +35,34 @@ import qualified Text.Parser.Char as Chr

3535import Text.Parser.LookAhead

3636import qualified Text.Parser.Token as Tok

3737import qualified Text.Parser.Token.Highlight as Hi

38−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

39− stringLiteral, symbol, whiteSpace)

40−import Text.Trifecta.Delta

38+import Text.Trifecta ((<?>))

39+import qualified Text.Trifecta as P

40+import qualified Text.Trifecta.Delta as P

4141

4242-- | Idris parser with state used during parsing

4343type IdrisParser = StateT IState IdrisInnerParser

4444

45−newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

46− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

45+newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: P.Parser a }

46+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, P.CharParsing, LookAheadParsing, P.DeltaParsing, P.MarkParsing P.Delta, Monoid, P.TokenParsing)

4747

48−deriving instance Parsing IdrisInnerParser

48+deriving instance P.Parsing IdrisInnerParser

4949

5050#if MIN_VERSION_base(4,9,0)

51−instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where

52− line = lift line

51+instance {-# OVERLAPPING #-} P.DeltaParsing IdrisParser where

52+ line = lift P.line

5353 {-# INLINE line #-}

54− position = lift position

54+ position = lift P.position

5555 {-# INLINE position #-}

56− slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

56+ slicedWith f (StateT m) = StateT $ \s -> P.slicedWith (\(a,s') b -> (f a b, s')) $ m s

5757 {-# INLINE slicedWith #-}

58− rend = lift rend

58+ rend = lift P.rend

5959 {-# INLINE rend #-}

60− restOfLine = lift restOfLine

60+ restOfLine = lift P.restOfLine

6161 {-# INLINE restOfLine #-}

6262

6363#endif

6464

65−instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

65+instance {-# OVERLAPPING #-} P.TokenParsing IdrisParser where

6666 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

6767 token p = do s <- get

6868 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

@@ -73,7 +73,7 @@ instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

7373 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

7474 return r

7575-- | Generalized monadic parsing constraint type

76−type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

76+type MonadicParsing m = (P.DeltaParsing m, LookAheadParsing m, P.TokenParsing m, Monad m)

7777

7878class HasLastTokenSpan m where

7979 getLastTokenSpan :: m (Maybe FC)

@@ -82,10 +82,10 @@ instance HasLastTokenSpan IdrisParser where

8282 getLastTokenSpan = lastTokenSpan <$> get

8383

8484-- | Helper to run Idris inner parser based stateT parsers

85−runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res

85+runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> P.Result res

8686runparser p i inputname =

87− parseString (runInnerParser (evalStateT p i))

88− (Directed (UTF8.fromString inputname) 0 0 0 0)

87+ P.parseString (runInnerParser (evalStateT p i))

88+ (P.Directed (UTF8.fromString inputname) 0 0 0 0)

8989

9090highlightP :: FC -> OutputAnnotation -> IdrisParser ()

9191highlightP fc annot = do ist <- get

@@ -125,7 +125,7 @@ parserWarning fc warnOpt warnErr = do

125125

126126-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

127127simpleWhiteSpace :: MonadicParsing m => m ()

128−simpleWhiteSpace = satisfy isSpace *> pure ()

128+simpleWhiteSpace = () <$ P.satisfy isSpace

129129

130130-- | Checks if a charcter is end of line

131131isEol :: Char -> Bool

@@ -134,7 +134,7 @@ isEol _ = False

134134

135135-- | A parser that succeeds at the end of the line

136136eol :: MonadicParsing m => m ()

137−eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

137+eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"

138138

139139{- | Consumes a single-line comment

140140

@@ -144,7 +144,7 @@ eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

144144 -}

145145singleLineComment :: MonadicParsing m => m ()

146146singleLineComment = (string "--" *>

147− many (satisfy (not . isEol)) *>

147+ many (P.satisfy (not . isEol)) *>

148148 eol *> pure ())

149149 <?> ""

150150

@@ -166,15 +166,15 @@ singleLineComment = (string "--" *>

166166@

167167-}

168168multiLineComment :: MonadicParsing m => m ()

169−multiLineComment = try (string "{-" *> (string "-}") *> pure ())

169+multiLineComment = P.try (string "{-" *> (string "-}") *> pure ())

170170 <|> string "{-" *> inCommentChars

171171 <?> ""

172172 where inCommentChars :: MonadicParsing m => m ()

173173 inCommentChars = string "-}" *> pure ()

174− <|> try (multiLineComment) *> inCommentChars

175− <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

176− <|> skipSome (noneOf startEnd) *> inCommentChars

177− <|> oneOf startEnd *> inCommentChars

174+ <|> P.try (multiLineComment) *> inCommentChars

175+ <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars

176+ <|> P.skipSome (P.noneOf startEnd) *> inCommentChars

177+ <|> P.oneOf startEnd *> inCommentChars

178178 <?> "end of comment"

179179 startEnd :: String

180180 startEnd = "{}-"

@@ -197,23 +197,23 @@ docComment = do dc <- pushIndent *> docCommentLine

197197 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

198198

199199 where docCommentLine :: MonadicParsing m => m String

200− docCommentLine = try (do string "|||"

201− many (satisfy (==' '))

202− contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

203− res <- many (satisfy (not . isEol))

204− return $ first:res)

205− eol ; someSpace

206− return contents)-- ++ concat rest))

200+ docCommentLine = P.try (do string "|||"

201+ many (P.satisfy (==' '))

202+ contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))

203+ res <- many (P.satisfy (not . isEol))

204+ return $ first:res)

205+ eol ; P.someSpace

206+ return contents)

207207 <?> ""

208208

209209 argDocCommentLine = do string "|||"

210− many (satisfy isSpace)

210+ many (P.satisfy isSpace)

211211 char '@'

212− many (satisfy isSpace)

212+ many (P.satisfy isSpace)

213213 n <- fst <$> name

214− many (satisfy isSpace)

215− docs <- many (satisfy (not . isEol))

216− eol ; someSpace

214+ many (P.satisfy isSpace)

215+ docs <- many (P.satisfy (not . isEol))

216+ eol ; P.someSpace

217217 return (n, docs)

218218

219219-- | Parses some white space

@@ -252,12 +252,12 @@ float = do f <- Tok.double

252252

253253

254254-- | Idris Style for parsing identifiers/reserved keywords

255−idrisStyle :: MonadicParsing m => IdentifierStyle m

256−idrisStyle = IdentifierStyle {

257− _styleName = "Idris"

258− , _styleStart = satisfy isAlpha <|> oneOf "_"

259− , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

260− , _styleReserved = HS.fromList

255+idrisStyle :: MonadicParsing m => P.IdentifierStyle m

256+idrisStyle = P.IdentifierStyle {

257+ P._styleName = "Idris"

258+ , P._styleStart = P.satisfy isAlpha <|> P.oneOf "_"

259+ , P._styleLetter = P.satisfy isAlphaNum <|> P.oneOf "_'."

260+ , P._styleReserved = HS.fromList

261261 ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",

262262 "import", "impossible", "case", "of", "total", "partial", "mutual",

263263 "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",

@@ -265,8 +265,8 @@ idrisStyle = IdentifierStyle {

265265 "interface", "implementation", "parameters", "public", "private",

266266 "export", "abstract", "implicit", "quoteGoal", "constructor", "if",

267267 "then", "else"]

268− , _styleHighlight = Hi.Identifier

269− , _styleReservedHighlight = Hi.ReservedIdentifier }

268+ , P._styleHighlight = Hi.Identifier

269+ , P._styleReservedHighlight = Hi.ReservedIdentifier }

270270

271271char :: MonadicParsing m => Char -> m Char

272272char = Chr.char

@@ -276,12 +276,12 @@ string = Chr.string

276276

277277-- | Parses a character as a token

278278lchar :: MonadicParsing m => Char -> m Char

279−lchar = token . char

279+lchar = P.token . P.char

280280

281281-- | Parses a character as a token, returning the source span of the character

282282lcharFC :: MonadicParsing m => Char -> m FC

283283lcharFC ch = do (FC file (l, c) _) <- getFC

284− _ <- token (char ch)

284+ _ <- P.token (char ch)

285285 return $ FC file (l, c) (l, c+1)

286286

287287-- | Parses string as a token

@@ -311,9 +311,9 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

311311-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

312312-- | Parses a reserved operator

313313reservedOp :: MonadicParsing m => String -> m ()

314−reservedOp name = token $ try $

314+reservedOp name = P.token $ P.try $

315315 do string name

316− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

316+ P.notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

317317

318318reservedOpFC :: MonadicParsing m => String -> m FC

319319reservedOpFC name = do (FC f (l, c) _) <- getFC

@@ -322,12 +322,12 @@ reservedOpFC name = do (FC f (l, c) _) <- getFC

322322

323323-- | Parses an identifier as a token

324324identifier :: (MonadicParsing m) => m (String, FC)

325−identifier = try(do (i, fc) <-

326− token $ do (FC f (l, c) _) <- getFC

327− i <- Tok.ident idrisStyle

328− return (i, FC f (l, c) (l, c + length i))

329− when (i == "_") $ unexpected "wildcard"

330− return (i, fc))

325+identifier = P.try(do (i, fc) <-

326+ P.token $ do (FC f (l, c) _) <- getFC

327+ i <- Tok.ident idrisStyle

328+ return (i, FC f (l, c) (l, c + length i))

329+ when (i == "_") $ P.unexpected "wildcard"

330+ return (i, fc))

331331

332332-- | Parses an identifier with possible namespace as a name

333333iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

@@ -339,10 +339,10 @@ iName bad = do (n, fc) <- maybeWithNS identifier False bad

339339maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

340340maybeWithNS parser ascend bad = do

341341 fc <- getFC

342− i <- option "" (lookAhead (fst <$> identifier))

343− when (i `elem` bad) $ unexpected "reserved identifier"

342+ i <- P.option "" (lookAhead (fst <$> identifier))

343+ when (i `elem` bad) $ P.unexpected "reserved identifier"

344344 let transf = if ascend then id else reverse

345− (x, xs, fc) <- choice (transf (parserNoNS parser : parsersNS parser i))

345+ (x, xs, fc) <- P.choice (transf (parserNoNS parser : parsersNS parser i))

346346 return (mkName (x, xs), fc)

347347 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

348348 parserNoNS parser = do startFC <- getFC

@@ -354,7 +354,7 @@ maybeWithNS parser ascend bad = do

354354 lchar '.'; (x, nameFC) <- parser

355355 return (x, xs, spanFC startFC nameFC)

356356 parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

357− parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

357+ parsersNS parser i = [P.try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

358358

359359-- | Parses a name

360360name :: IdrisParser (Name, FC)

@@ -393,11 +393,11 @@ opChars :: String

393393opChars = ":!#$%&*+./<=>?@\\^|-~"

394394

395395operatorLetter :: MonadicParsing m => m Char

396−operatorLetter = oneOf opChars

396+operatorLetter = P.oneOf opChars

397397

398398-- | Parse a package name

399399packageName :: MonadicParsing m => m String

400−packageName = (:) <$> oneOf firstChars <*> many (oneOf remChars)

400+packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)

401401 where firstChars = ['a'..'z'] ++ ['A'..'Z']

402402 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

403403

@@ -409,7 +409,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%

409409

410410-- | Parses an operator

411411symbolicOperator :: MonadicParsing m => m String

412−symbolicOperator = do op <- token . some $ operatorLetter

412+symbolicOperator = do op <- P.token . some $ operatorLetter

413413 when (op `elem` (invalidOperators ++ commentMarkers)) $

414414 fail $ op ++ " is not a valid operator"

415415 return op

@@ -422,24 +422,24 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC

422422

423423{- * Position helpers -}

424424{- | Get filename from position (returns "(interactive)" when no source file is given) -}

425−fileName :: Delta -> String

426−fileName (Directed fn _ _ _ _) = UTF8.toString fn

427−fileName _ = "(interactive)"

425+fileName :: P.Delta -> String

426+fileName (P.Directed fn _ _ _ _) = UTF8.toString fn

427+fileName _ = "(interactive)"

428428

429429{- | Get line number from position -}

430−lineNum :: Delta -> Int

431−lineNum (Lines l _ _ _) = fromIntegral l + 1

432−lineNum (Directed _ l _ _ _) = fromIntegral l + 1

430+lineNum :: P.Delta -> Int

431+lineNum (P.Lines l _ _ _) = fromIntegral l + 1

432+lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1

433433lineNum _ = 0

434434

435435{- | Get column number from position -}

436−columnNum :: Delta -> Int

437−columnNum pos = fromIntegral (column pos) + 1

436+columnNum :: P.Delta -> Int

437+columnNum pos = fromIntegral (P.column pos) + 1

438438

439439

440440{- | Get file position as FC -}

441441getFC :: MonadicParsing m => m FC

442−getFC = do s <- position

442+getFC = do s <- P.position

443443 let (dir, file) = splitFileName (fileName s)

444444 let f = if dir == addTrailingPathSeparator "." then file else fileName s

445445 return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

@@ -456,15 +456,15 @@ bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)

456456{- | @commaSeparated p@ parses one or more occurences of `p`,

457457 separated by commas and optional whitespace. -}

458458commaSeparated :: MonadicParsing m => m a -> m [a]

459−commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)

459+commaSeparated p = p `P.sepBy1` (P.spaces >> P.char ',' >> P.spaces)

460460

461461{- * Layout helpers -}

462462

463463-- | Push indentation to stack

464464pushIndent :: IdrisParser ()

465−pushIndent = do pos <- position

465+pushIndent = do pos <- P.position

466466 ist <- get

467− put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })

467+ put (ist { indent_stack = (fromIntegral (P.column pos) + 1) : indent_stack ist })

468468

469469-- | Pops indentation from stack

470470popIndent :: IdrisParser ()

@@ -476,7 +476,7 @@ popIndent = do ist <- get

476476

477477-- | Gets current indentation

478478indent :: IdrisParser Int

479−indent = liftM ((+1) . fromIntegral . column) position

479+indent = liftM ((+1) . fromIntegral . P.column) P.position

480480

481481-- | Gets last indentation

482482lastIndent :: IdrisParser Int

@@ -544,7 +544,7 @@ openBlock = do lchar '{'

544544closeBlock :: IdrisParser ()

545545closeBlock = do ist <- get

546546 bs <- case brace_stack ist of

547− [] -> eof >> return []

547+ [] -> [] <$ P.eof

548548 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

549549 Just lvl : xs -> (do i <- indent

550550 isParen <- lookAheadMatches (char ')')

@@ -553,7 +553,7 @@ closeBlock = do ist <- get

553553 then fail "not end of block"

554554 else return xs)

555555 <|> (do notOpenBraces

556− eof

556+ P.eof

557557 return [])

558558 put (ist { brace_stack = bs })

559559

@@ -562,19 +562,19 @@ terminator :: IdrisParser ()

562562terminator = do lchar ';'; popIndent

563563 <|> do c <- indent; l <- lastIndent

564564 if c <= l then popIndent else fail "not a terminator"

565− <|> do isParen <- lookAheadMatches (oneOf ")}")

565+ <|> do isParen <- lookAheadMatches (P.oneOf ")}")

566566 if isParen then popIndent else fail "not a terminator"

567− <|> lookAhead eof

567+ <|> lookAhead P.eof

568568

569569-- | Parses and keeps a terminator

570570keepTerminator :: IdrisParser ()

571−keepTerminator = do lchar ';'; return ()

571+keepTerminator = () <$ lchar ';'

572572 <|> do c <- indent; l <- lastIndent

573573 unless (c <= l) $ fail "not a terminator"

574− <|> do isParen <- lookAheadMatches (oneOf ")}|")

574+ <|> do isParen <- lookAheadMatches (P.oneOf ")}|")

575575 isIn <- lookAheadMatches (reserved "in")

576576 unless (isIn || isParen) $ fail "not a terminator"

577− <|> lookAhead eof

577+ <|> lookAhead P.eof

578578

579579-- | Checks if application expression does not end

580580notEndApp :: IdrisParser ()

src/Idris/Parser/Ops.hs+11−11

@@ -22,8 +22,8 @@ import Control.Monad.State.Strict

2222import Data.Char (isAlpha)

2323import Data.List

2424import Text.Parser.Expression

25−import Text.Trifecta hiding (char, charLiteral, natural, span, string,

26− stringLiteral, symbol, whiteSpace)

25+import Text.Trifecta ((<?>))

26+import qualified Text.Trifecta as P

2727

2828-- | Creates table for fixity declarations to build expression parser

2929-- using pre-build and user-defined operator/fixity declarations

@@ -49,8 +49,8 @@ table fixes

4949 noFixityOperator :: Operator IdrisParser PTerm

5050 noFixityOperator = flip Infix AssocNone $ do

5151 indentGt

52− op <- try symbolicOperator

53− unexpected $ "Operator without known fixity: " ++ op

52+ op <- P.try symbolicOperator

53+ P.unexpected $ "Operator without known fixity: " ++ op

5454

5555 -- | Calculates table for fixity declarations

5656 toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

@@ -71,7 +71,7 @@ table fixes

7171

7272 binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm

7373 binary name assoc f

74− | isBacktick name = flip Infix assoc $ try $ do

74+ | isBacktick name = flip Infix assoc $ P.try $ do

7575 (n, fc) <- backtickOperator

7676 guard $ show (nsroot n) == name

7777 return $ f fc n

@@ -96,7 +96,7 @@ table fixes

9696@

9797-}

9898backtickOperator :: IdrisParser (Name, FC)

99−backtickOperator = between (indentGt *> lchar '`') (indentGt *> lchar '`') name

99+backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name

100100

101101{- | Parses an operator name (either a symbolic name or a backtick-quoted name)

102102

@@ -123,9 +123,9 @@ operatorName = first sUN <$> symbolicOperatorFC

123123

124124-}

125125operatorFront :: IdrisParser (Name, FC)

126−operatorFront = try (do (FC f (l, c) _) <- getFC

127− op <- lchar '(' *> reservedOp "=" <* lchar ')'

128− return (eqTy, FC f (l, c) (l, c+3)))

126+operatorFront = P.try (do (FC f (l, c) _) <- getFC

127+ op <- lchar '(' *> reservedOp "=" <* lchar ')'

128+ return (eqTy, FC f (l, c) (l, c+3)))

129129 <|> maybeWithNS (do (FC f (l, c) _) <- getFC

130130 op <- lchar '(' *> symbolicOperator

131131 (FC _ _ (l', c')) <- getFC

@@ -139,7 +139,7 @@ operatorFront = try (do (FC f (l, c) _) <- getFC

139139@

140140-}

141141fnName :: IdrisParser (Name, FC)

142−fnName = try operatorFront <|> name <?> "function name"

142+fnName = P.try operatorFront <|> name <?> "function name"

143143

144144{- | Parses a fixity declaration

145145@

@@ -151,7 +151,7 @@ Fixity ::=

151151fixity :: IdrisParser PDecl

152152fixity = do pushIndent

153153 f <- fixityType; i <- fst <$> natural;

154− ops <- sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

154+ ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

155155 terminator

156156 let prec = fromInteger i

157157 istate <- get

src/Idris/Prover.hs+23−23

@@ -43,7 +43,7 @@ import Control.Monad.State.Strict

4343import System.Console.Haskeline

4444import System.Console.Haskeline.History

4545import System.IO (Handle, hPutStrLn, stdin, stdout)

46−import Text.Trifecta.Result (ErrInfo(..), Result(..))

46+import qualified Text.Trifecta.Result as P

4747

4848-- | Launch the proof shell

4949prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

@@ -312,15 +312,15 @@ elabloop info fn d prompt prf e prev h env

312312

313313 -- if we're abandoning, it has to be outside the scope of the catch

314314 case cmd of

315− Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

315+ P.Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

316316 _ -> return ()

317317

318318 (d, prev', st, done, prf', env', res) <-

319319 idrisCatch

320320 (case cmd of

321− Failure (ErrInfo err _) ->

321+ P.Failure (P.ErrInfo err _) ->

322322 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

323− Success (Left cmd') ->

323+ P.Success (Left cmd') ->

324324 case cmd' of

325325 EQED -> do hs <- lifte e get_holes

326326 unless (null hs) $ ifail "Incomplete proof"

@@ -345,7 +345,7 @@ elabloop info fn d prompt prf e prev h env

345345 return (d', prev, st', done, prf', env, go)

346346 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

347347 return (d', prev, st', done, prf', env, go)

348− Success (Right cmd') ->

348+ P.Success (Right cmd') ->

349349 case cmd' of

350350 DoLetP {} -> ifail "Pattern-matching let not supported here"

351351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

@@ -430,27 +430,27 @@ ploop fn d prompt prf e h

430430 Nothing -> do iPrintError ""; ifail "Abandoned"

431431 Just input -> return (parseTactic i input, input)

432432 case cmd of

433− Success Abandon -> do iPrintError ""; ifail "Abandoned"

433+ P.Success Abandon -> do iPrintError ""; ifail "Abandoned"

434434 _ -> return ()

435435 (d, st, done, prf', res) <- idrisCatch

436436 (case cmd of

437− Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

438− Success Undo -> do (_, st) <- elabStep e loadState

439− return (True, st, False, init prf, Right $ iPrintResult "")

440− Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

441− Success ProofTerm -> do tm <- lifte e get_term

442− iputStrLn $ "TT: " ++ show tm ++ "\n"

443− return (False, e, False, prf, Right $ iPrintResult "")

444− Success Qed -> do hs <- lifte e get_holes

445− unless (null hs) $ ifail "Incomplete proof"

446− iputStrLn "Proof completed!"

447− return (False, e, True, prf, Right $ iPrintResult "")

448− Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

449− Success (TCheck t) -> checkType e prf t

450− Success (TEval t) -> evalTerm e prf t

451− Success (TDocStr x) -> docStr e prf x

452− Success (TSearch t) -> search e prf t

453− Success tac ->

437+ P.Failure (P.ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

438+ P.Success Undo -> do (_, st) <- elabStep e loadState

439+ return (True, st, False, init prf, Right $ iPrintResult "")

440+ P.Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

441+ P.Success ProofTerm -> do tm <- lifte e get_term

442+ iputStrLn $ "TT: " ++ show tm ++ "\n"

443+ return (False, e, False, prf, Right $ iPrintResult "")

444+ P.Success Qed -> do hs <- lifte e get_holes

445+ unless (null hs) $ ifail "Incomplete proof"

446+ iputStrLn "Proof completed!"

447+ return (False, e, True, prf, Right $ iPrintResult "")

448+ P.Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

449+ P.Success (TCheck t) -> checkType e prf t

450+ P.Success (TEval t) -> evalTerm e prf t

451+ P.Success (TDocStr x) -> docStr e prf x

452+ P.Success (TSearch t) -> search e prf t

453+ P.Success tac ->

454454 do (_, e) <- elabStep e saveState

455455 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

456456 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

src/Idris/REPL.hs+22−25

@@ -93,7 +93,7 @@ import System.FSNotify (watchDir, withManager)

9393import System.FSNotify.Devel (allEvents, doAllEvents)

9494import System.IO

9595import System.Process

96−import Text.Trifecta.Result (ErrInfo(..), Result(..))

96+import qualified Text.Trifecta.Result as P

9797import Util.DynamicLinker

9898import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

9999import Util.Pretty hiding ((</>))

@@ -177,9 +177,9 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

177177 IO (IState, FilePath)

178178processNetCmd orig i h fn cmd

179179 = do res <- case parseCmd i "(net)" cmd of

180− Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))

181− Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

182− Success (Left err) -> return (Left (Msg err))

180+ P.Failure (P.ErrInfo err _) -> return (Left (Msg " invalid command"))

181+ P.Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

182+ P.Success (Left err) -> return (Left (Msg err))

183183 case res of

184184 Right x -> return x

185185 Left err -> do hPutStrLn h (show err)

@@ -295,8 +295,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

295295 do c <- colourise

296296 i <- getIState

297297 case parseCmd i "(input)" cmd of

298− Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)

299− Success (Right (Prove mode n')) ->

298+ P.Failure (P.ErrInfo err _) -> iPrintError $ show (fixColour False err)

299+ P.Success (Right (Prove mode n')) ->

300300 idrisCatch

301301 (do process fn (Prove mode n')

302302 isetPrompt (mkPrompt mods)

@@ -315,10 +315,10 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

315315 IdeMode.convSExp "abandon-proof" "Abandoned" n

316316 _ -> return ()

317317 iRenderError $ pprintErr ist e)

318− Success (Right cmd) -> idrisCatch

318+ P.Success (Right cmd) -> idrisCatch

319319 (idemodeProcess fn cmd)

320320 (\e -> getIState >>= iRenderError . flip pprintErr e)

321− Success (Left err) -> iPrintError err

321+ P.Success (Left err) -> iPrintError err

322322runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

323323 do (unused, compls) <- replCompletion (reverse str, "")

324324 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

@@ -353,8 +353,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

353353 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

354354runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

355355 case parseConst orig name of

356− Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

357− Failure _ ->

356+ P.Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

357+ P.Failure _ ->

358358 case splitName name of

359359 Left err -> iPrintError err

360360 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

@@ -727,11 +727,10 @@ processInput cmd orig inputs efile

727727 let fn = fromMaybe "" (listToMaybe inputs)

728728 c <- colourise

729729 case parseCmd i "(input)" cmd of

730− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

731− return (Just inputs)

732− Success (Right Reload) ->

730+ P.Failure (P.ErrInfo err _) -> Just inputs <$ iputStrLn (show (fixColour c err))

731+ P.Success (Right Reload) ->

733732 reload orig inputs

734− Success (Right Watch) ->

733+ P.Success (Right Watch) ->

735734 if null inputs then

736735 do iputStrLn "No loaded files to watch."

737736 return (Just inputs)

@@ -739,7 +738,7 @@ processInput cmd orig inputs efile

739738 do iputStrLn efile

740739 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

741740 watch orig inputs

742− Success (Right (Load f toline)) ->

741+ P.Success (Right (Load f toline)) ->

743742 -- The $!! here prevents a space leak on reloading.

744743 -- This isn't a solution - but it's a temporary stopgap.

745744 -- See issue #2386

@@ -749,22 +748,20 @@ processInput cmd orig inputs efile

749748 clearErr

750749 mod <- loadInputs [f] toline

751750 return (Just mod)

752− Success (Right (ModImport f)) ->

751+ P.Success (Right (ModImport f)) ->

753752 do clearErr

754753 fmod <- loadModule f (IBC_REPL True)

755754 return (Just (inputs ++ maybe [] (:[]) fmod))

756− Success (Right Edit) -> do -- takeMVar stvar

755+ P.Success (Right Edit) -> do -- takeMVar stvar

757756 edit efile orig

758757 return (Just inputs)

759− Success (Right Proofs) -> do proofs orig

758+ P.Success (Right Proofs) -> Just inputs <$ proofs orig

759+ P.Success (Right Quit) -> Nothing <$ when (not quiet) (iputStrLn "Bye bye")

760+ P.Success (Right cmd ) -> do idrisCatch (process fn cmd)

761+ (\e -> do msg <- showErr e ; iputStrLn msg)

760762 return (Just inputs)

761− Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")

762− return Nothing

763− Success (Right cmd ) -> do idrisCatch (process fn cmd)

764− (\e -> do msg <- showErr e ; iputStrLn msg)

763+ P.Success (Left err) -> do runIO $ putStrLn err

765764 return (Just inputs)

766− Success (Left err) -> do runIO $ putStrLn err

767− return (Just inputs)

768765

769766resolveProof :: Name -> Idris Name

770767resolveProof n'

@@ -1429,7 +1426,7 @@ process fn (Browse ns) =

14291426process fn (MakeDoc s) =

14301427 do istate <- getIState

14311428 let names = words s

1432− parse n | Success x <- runparser (fmap fst name) istate fn n = Right x

1429+ parse n | P.Success x <- runparser (fmap fst name) istate fn n = Right x

14331430 parse n = Left n

14341431 (bad, nss) = partitionEithers $ map parse names

14351432 cd <- runIO getCurrentDirectory

src/Idris/REPL/Parser.hs+125−125

@@ -17,10 +17,10 @@ import Idris.Core.TT

1717import Idris.Help

1818import Idris.Imports

1919import Idris.Options

20−import qualified Idris.Parser as P

21−import qualified Idris.Parser.Expr as P

22−import qualified Idris.Parser.Helpers as P

23−import qualified Idris.Parser.Ops as P

20+import qualified Idris.Parser as IP

21+import qualified Idris.Parser.Expr as IP

22+import qualified Idris.Parser.Helpers as IP

23+import qualified Idris.Parser.Ops as IP

2424

2525import Idris.REPL.Commands

2626

@@ -33,15 +33,15 @@ import System.Console.ANSI (Color(..))

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

3434import Text.Parser.Char (anyChar, oneOf)

3535import Text.Parser.Combinators

36−import Text.Trifecta (Result)

36+import qualified Text.Trifecta as P

3737

38−parseCmd :: IState -> String -> String -> Result (Either String Command)

39−parseCmd i inputname = P.runparser pCmd i inputname . trim

38+parseCmd :: IState -> String -> String -> P.Result (Either String Command)

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

4040 where trim = f . f

4141 where f = reverse . dropWhile isSpace

4242

4343type CommandTable = [ ( [String], CmdArg, String

44− , String -> P.IdrisParser (Either String Command) ) ]

44+ , String -> IP.IdrisParser (Either String Command) ) ]

4545

4646setOptions :: [(String, Opt)]

4747setOptions = [("errorcontext", ErrContext),

@@ -168,8 +168,8 @@ parserCommands =

168168 , cmd_refine)

169169 , (["debugunify"], SeqArgs ExprArg ExprArg

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

171− l <- P.simpleExpr defaultSyntax

172− r <- P.simpleExpr defaultSyntax

171+ l <- IP.simpleExpr defaultSyntax

172+ r <- IP.simpleExpr defaultSyntax

173173 eof

174174 return (Right (DebugUnify l r))

175175 )

@@ -188,7 +188,7 @@ optArgCmd names command doc =

188188proofArgCmd names command doc =

189189 (names, NoArg, doc, proofArg command)

190190

191−pCmd :: P.IdrisParser (Either String Command)

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

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

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

194194 <|> unrecognized

@@ -196,23 +196,23 @@ pCmd = choice [ do c <- cmd names; parser c

196196 <|> eval

197197 where nop = do eof; return (Right NOP)

198198 unrecognized = do

199− P.lchar ':'

199+ IP.lchar ':'

200200 cmd <- many anyChar

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

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

203203

204−cmd :: [String] -> P.IdrisParser String

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

205205cmd xs = try $ do

206− P.lchar ':'

206+ IP.lchar ':'

207207 docmd sorted_xs

208208

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

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

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

211211

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

213213

214214

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

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

216216noArgs cmd name = do

217217 let emptyArgs = do

218218 eof

@@ -222,29 +222,29 @@ noArgs cmd name = do

222222

223223 emptyArgs <|> failure

224224

225−eval :: P.IdrisParser (Either String Command)

225+eval :: IP.IdrisParser (Either String Command)

226226eval = do

227− t <- P.fullExpr defaultSyntax

227+ t <- IP.fullExpr defaultSyntax

228228 return $ Right (Eval t)

229229

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

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

231231exprArg cmd name = do

232232 let noArg = do

233233 eof

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

235235

236236 let justOperator = do

237− (op, fc) <- P.symbolicOperatorFC

237+ (op, fc) <- IP.symbolicOperatorFC

238238 eof

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

240240

241241 let properArg = do

242− t <- P.fullExpr defaultSyntax

242+ t <- IP.fullExpr defaultSyntax

243243 return $ Right (cmd t)

244244 try noArg <|> try justOperator <|> properArg

245245

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

247− -> String -> P.IdrisParser (Either String Command)

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

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

248248genArg argName argParser cmd name = do

249249 let emptyArgs = do eof; failure

250250 oneArg = do arg <- argParser

@@ -254,24 +254,24 @@ genArg argName argParser cmd name = do

254254 where

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

256256

257−nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

258−nameArg = genArg "name" $ fst <$> P.name

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

257+nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)

258+nameArg = genArg "name" $ fst <$> IP.name

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

260260

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

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

262262strArg = genArg "string" (many anyChar)

263263

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

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

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

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

266266 where

267267 toPath n = foldl1' (</>) $ splitOn "." n

268268

269−namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

270−namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

269+namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)

270+namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)

271271 where

272272 toNS = splitOn "."

273273

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

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

275275optArg cmd name = do

276276 let emptyArgs = do

277277 eof

@@ -279,7 +279,7 @@ optArg cmd name = do

279279

280280 let oneArg = do

281281 o <- pOption

282− P.whiteSpace

282+ IP.whiteSpace

283283 eof

284284 return (Right (cmd o))

285285

@@ -288,58 +288,58 @@ optArg cmd name = do

288288 try emptyArgs <|> oneArg <|> failure

289289

290290 where

291− pOption :: P.IdrisParser Opt

292− pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

291+ pOption :: IP.IdrisParser Opt

292+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (IP.symbol a); return b) setOptions

293293

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

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

295295proofArg cmd name = do

296296 upd <- option False $ do

297− P.lchar '!'

297+ IP.lchar '!'

298298 return True

299− l <- fst <$> P.natural

300− n <- fst <$> P.name;

299+ l <- fst <$> IP.natural

300+ n <- fst <$> IP.name;

301301 return (Right (cmd upd (fromInteger l) n))

302302

303−cmd_doc :: String -> P.IdrisParser (Either String Command)

303+cmd_doc :: String -> IP.IdrisParser (Either String Command)

304304cmd_doc name = do

305305 let constant = do

306− c <- fmap fst P.constant

306+ c <- fmap fst IP.constant

307307 eof

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

309309

310310 let pType = do

311− P.reserved "Type"

311+ IP.reserved "Type"

312312 eof

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

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

314314

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

316316

317317 try constant <|> pType <|> fnName

318318

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

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

320320cmd_consolewidth name = do

321321 w <- pConsoleWidth

322322 return (Right (SetConsoleWidth w))

323323

324324 where

325− pConsoleWidth :: P.IdrisParser ConsoleWidth

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

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

328− <|> do n <- fmap (fromInteger . fst) P.natural

325+ pConsoleWidth :: IP.IdrisParser ConsoleWidth

326+ pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth

327+ <|> do discard (IP.symbol "infinite"); return InfinitelyWide

328+ <|> do n <- fmap (fromInteger . fst) IP.natural

329329 return (ColsWide n)

330330

331−cmd_printdepth :: String -> P.IdrisParser (Either String Command)

332−cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) P.natural)

331+cmd_printdepth :: String -> IP.IdrisParser (Either String Command)

332+cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)

333333 return (Right $ SetPrinterDepth d)

334334

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

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

336336cmd_execute name = do

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

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

338338 return (Right (Execute tm))

339339 where

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

341341

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

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

343343cmd_dynamic name = do

344344 let optArg = do l <- many anyChar

345345 if (l /= "")

@@ -348,101 +348,101 @@ cmd_dynamic name = do

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

349349 try optArg <|> failure

350350

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

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

352352cmd_pprint name = do

353353 fmt <- ppFormat

354− P.whiteSpace

355− n <- fmap (fromInteger . fst) P.natural

356− P.whiteSpace

357− t <- P.fullExpr defaultSyntax

354+ IP.whiteSpace

355+ n <- fmap (fromInteger . fst) IP.natural

356+ IP.whiteSpace

357+ t <- IP.fullExpr defaultSyntax

358358 return (Right (PPrint fmt n t))

359359

360360 where

361− ppFormat :: P.IdrisParser OutputFmt

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

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

361+ ppFormat :: IP.IdrisParser OutputFmt

362+ ppFormat = (discard (IP.symbol "html") >> return HTMLOutput)

363+ <|> (discard (IP.symbol "latex") >> return LaTeXOutput)

364364

365−cmd_compile :: String -> P.IdrisParser (Either String Command)

365+cmd_compile :: String -> IP.IdrisParser (Either String Command)

366366cmd_compile name = do

367367 let defaultCodegen = Via IBCFormat "c"

368368

369− let codegenOption :: P.IdrisParser Codegen

369+ let codegenOption :: IP.IdrisParser Codegen

370370 codegenOption = do

371− let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode

372− viaCodegen = do x <- fst <$> P.identifier

371+ let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode

372+ viaCodegen = do x <- fst <$> IP.identifier

373373 return (Via IBCFormat (map toLower x))

374374 bytecodeCodegen <|> viaCodegen

375375

376376 let hasOneArg = do

377377 i <- get

378− f <- fst <$> P.identifier

378+ f <- fst <$> IP.identifier

379379 eof

380380 return $ Right (Compile defaultCodegen f)

381381

382382 let hasTwoArgs = do

383383 i <- get

384384 codegen <- codegenOption

385− f <- fst <$> P.identifier

385+ f <- fst <$> IP.identifier

386386 eof

387387 return $ Right (Compile codegen f)

388388

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

390390 try hasTwoArgs <|> try hasOneArg <|> failure

391391

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

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

393393cmd_addproof name = do

394394 n <- option Nothing $ do

395− x <- fst <$> P.name

395+ x <- fst <$> IP.name

396396 return (Just x)

397397 eof

398398 return (Right (AddProof n))

399399

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

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

401401cmd_log name = do

402− i <- fmap (fromIntegral . fst) P.natural

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

403403 eof

404404 return (Right (LogLvl i))

405405

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

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

407407cmd_verb name = do

408− i <- fmap (fromIntegral . fst) P.natural

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

409409 eof

410410 return (Right (Verbosity i))

411411

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

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

413413cmd_cats name = do

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

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

415415 eof

416416 return $ Right $ LogCategory (concat cs)

417417 where

418418 badCat = do

419− c <- fst <$> P.identifier

419+ c <- fst <$> IP.identifier

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

421421

422− pLogCats :: P.IdrisParser [LogCat]

423− pLogCats = try (P.symbol (strLogCat IParse) >> return parserCats)

424− <|> try (P.symbol (strLogCat IElab) >> return elabCats)

425− <|> try (P.symbol (strLogCat ICodeGen) >> return codegenCats)

426− <|> try (P.symbol (strLogCat ICoverage) >> return [ICoverage])

427− <|> try (P.symbol (strLogCat IIBC) >> return [IIBC])

428− <|> try (P.symbol (strLogCat IErasure) >> return [IErasure])

422+ pLogCats :: IP.IdrisParser [LogCat]

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

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

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

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

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

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

429429 <|> badCat

430430

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

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

432432cmd_let name = do

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

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

434434 return (Right (NewDefn defn))

435435

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

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

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

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

438438

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

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

440440cmd_loadto name = do

441− toline <- fmap (fromInteger . fst) P.natural

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

442442 f <- many anyChar;

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

444444

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

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

446446cmd_colour name = fmap Right pSetColourCmd

447447

448448 where

@@ -458,29 +458,29 @@ cmd_colour name = fmap Right pSetColourCmd

458458 , ("default", Nothing)

459459 ]

460460

461− pSetColourCmd :: P.IdrisParser Command

461+ pSetColourCmd :: IP.IdrisParser Command

462462 pSetColourCmd = (do c <- pColourType

463463 let defaultColour = IdrisColour Nothing True False False False

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

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

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

466466 return $ SetColour c colour)

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

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

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

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

469469

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

470+ pColour :: IP.IdrisParser (Maybe Color)

471471 pColour = doColour colours

472472 where doColour [] = fail "Unknown colour"

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

474−

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

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

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

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

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

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

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

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

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

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

474+

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

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

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

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

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

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

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

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

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

484484 <|> try (pColour >>= return . doSetColour)

485485 where doVivid i = i { vivid = True }

486486 doDull i = i { vivid = False }

@@ -497,44 +497,44 @@ cmd_colour name = fmap Right pSetColourCmd

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

498498 enumFromTo minBound maxBound

499499

500− pColourType :: P.IdrisParser ColourType

500+ pColourType :: IP.IdrisParser ColourType

501501 pColourType = doColourType colourTypes

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

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

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

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

505505

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

507507

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

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

509509cmd_apropos = packageBasedCmd (some idChar) Apropos

510510

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

512− -> String -> P.IdrisParser (Either String Command)

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

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

513513packageBasedCmd valParser cmd name =

514− try (do P.lchar '('

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

516− P.lchar ')'

514+ try (do IP.lchar '('

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

516+ IP.lchar ')'

517517 val <- valParser

518518 return (Right (cmd pkgs val)))

519519 <|> do val <- valParser

520520 return (Right (cmd [] val))

521521 where

522− pkg = either fail pure . pkgName =<< P.packageName

522+ pkg = either fail pure . pkgName =<< IP.packageName

523523

524−cmd_search :: String -> P.IdrisParser (Either String Command)

524+cmd_search :: String -> IP.IdrisParser (Either String Command)

525525cmd_search = packageBasedCmd

526− (P.fullExpr (defaultSyntax { implicitAllowed = True })) Search

526+ (IP.fullExpr (defaultSyntax { implicitAllowed = True })) Search

527527

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

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

529529cmd_proofsearch name = do

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

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

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

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

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

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

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

534534

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

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

536536cmd_refine name = do

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

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

539− hint <- fst <$> P.fnName

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

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

539+ hint <- fst <$> IP.fnName

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