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

git.iko.soy/Idris-dev

on master help sign in

Import Trifecta qualified as P

1f8db23Jason Felice9 years ago

src/Idris/IdeMode.hs+17−18

compare with master

unifiedsplit

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

25import Numeric

26import System.IO

27import Text.Printf

28−import Text.Trifecta hiding (Err)

28+import qualified Text.Trifecta as P

29−import Text.Trifecta.Delta

29+import qualified Text.Trifecta.Delta as P

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

32getNChar _ 0 s = return (reverse s)

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

205 escapeChar '"' = "\\\""

206 escapeChar c = [c]

207

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

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

209− return (SexpList xs)

210 <|> atom

209 <|> atom

211

210

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

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

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

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

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

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

215− <|> do ints <- some digit

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

216 case readDec ints of

215 case readDec ints of

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

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

218 _ -> return (StringAtom ints)

217 _ -> return (StringAtom ints)

219

218

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

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

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

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

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

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

223

222

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

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

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

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

226− <|> noneOf "\""

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

227

226

228−parseSExp :: String -> Result SExp

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

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

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

230

229

231data Opt = ShowImpl | ErrContext deriving Show

230data Opt = ShowImpl | ErrContext deriving Show

232

231

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

324receiveString :: String -> Either Err SExp

323receiveString :: String -> Either Err SExp

325receiveString x =

324receiveString x =

326 case parseSExp x of

325 case parseSExp x of

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

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

328− Success r -> Right r

327+ P.Success r -> Right r

329

328

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

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

331convSExp pre s id =

330convSExp pre s id =

src/Idris/Main.hs+19−19

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

47import System.FilePath

48import System.IO

49import System.IO.CodePage (withCP65001)

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

50+import qualified Text.Trifecta.Result as P

52-- | How to run Idris programs.

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

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

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

197 c <- colourise

198 case parseExpr ist str of

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

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

200− runIO $ exitWith (ExitFailure 1)

200+ runIO $ exitWith (ExitFailure 1)

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

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

202 exprs

203 runIO exitSuccess

204

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

273execScript expr = do i <- getIState

274 c <- colourise

275 case parseExpr i expr of

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

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

277− runIO $ exitWith (ExitFailure 1)

277+ runIO $ exitWith (ExitFailure 1)

278− Success term -> do ctxt <- getContext

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

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

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

280− res <- execute tm

280+ res <- execute tm

281− runIO $ exitSuccess

281+ runIO $ exitSuccess

282

283-- | Run the initialisation script

284initScript :: Idris ()

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

300 runInit h

301 processLine i cmd input clr =

302 case parseCmd i input cmd of

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

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

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

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

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

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

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

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

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

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

308− Success (Right Proofs) -> proofs i

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

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

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

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

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

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

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

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

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

20import System.Exit

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

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

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

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

24− whiteSpace)

24+import qualified Text.Trifecta as P

26type PParser = StateT PkgDesc IdrisInnerParser

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

29 getLastTokenSpan = return Nothing

31#if MIN_VERSION_base(4,9,0)

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

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

33− line = lift line

33+ line = lift P.line

34 {-# INLINE line #-}

35− position = lift position

35+ position = lift P.position

36 {-# 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

38 {-# INLINE slicedWith #-}

39− rend = lift rend

39+ rend = lift P.rend

40 {-# INLINE rend #-}

41− restOfLine = lift restOfLine

41+ restOfLine = lift P.restOfLine

42 {-# INLINE restOfLine #-}

43#endif

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

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

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

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

56 then do

57 p <- readFile fp

58 case runparser pPkg defaultPkg fp p of

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

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

60− Success x -> return x

60+ P.Success x -> return x

61 else do

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

63 exitWith (ExitFailure 1)

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

66pPkg = do

67 reserved "package"

68 p <- pPkgName

69− someSpace

69+ P.someSpace

70 st <- get

71 put (st { pkgname = p })

72 some pClause

73 st <- get

74− eof

74+ P.eof

75 return st

77pPkgName :: PParser PkgName

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

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

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

84filename = (do

85− filename <- token $

85+ filename <- P.token $

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

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

88 -- it will also accept hyphens

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

90− stringLiteral

90+ P.stringLiteral

91 <|>

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

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

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

137 put (st { sourcedir = src })

138

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

140− opts <- stringLiteral

140+ opts <- P.stringLiteral

141 st <- get

142 let args = pureArgParser (words opts)

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

144

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

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

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

147 st <- get

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

149

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

151 , idris_opts = pkgs ++ idris_opts st})

152

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

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

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

155 st <- get

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

157

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

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

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

160 st <- get

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

162

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

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

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

165 st <- get

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

167

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

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

172

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

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

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

175 st <- get

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

177

178 <|> do reserved "version"

179 lchar '='

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

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

181 eol

182− someSpace

182+ P.someSpace

183 st <- get

184 put st {pkgversion = Just vStr}

185

186 <|> do reserved "readme"

187 lchar '='

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

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

189 eol

190− someSpace

190+ P.someSpace

191 st <- get

192 put (st { pkgreadme = Just rme })

193

194 <|> do reserved "license"

195 lchar '='

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

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

197 eol

198 st <- get

199 put st {pkglicense = Just lStr}

200

201 <|> do reserved "homepage"

202 lchar '='

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

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

204 eol

205− someSpace

205+ P.someSpace

206 st <- get

207 put st {pkghomepage = Just www}

208

209 <|> do reserved "sourceloc"

210 lchar '='

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

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

212 eol

213− someSpace

213+ P.someSpace

214 st <- get

215 put st {pkgsourceloc = Just srcpage}

216

217 <|> do reserved "bugtracker"

218 lchar '='

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

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

220 eol

221− someSpace

221+ P.someSpace

222 st <- get

223 put st {pkgbugtracker = Just src}

224

225 <|> do reserved "brief"

226 lchar '='

227− brief <- stringLiteral

227+ brief <- P.stringLiteral

228 st <- get

229− someSpace

229+ P.someSpace

230 put st {pkgbrief = Just brief}

231

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

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

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

234 eol

235− someSpace

235+ P.someSpace

236 st <- get

237 put st {pkgauthor = Just author}

238

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

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

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

241 eol

242− someSpace

242+ P.someSpace

243 st <- get

244 put st {pkgmaintainer = Just maintainer}

src/Idris/Parser.hs+164−186

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

36import Idris.Termination

37import Idris.Unlit

39−import qualified Util.Pretty as P

39+import qualified Util.Pretty

40import Util.System (readSource)

42import Prelude hiding (pi)

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

59import System.FilePath

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

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

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

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

63− stringLiteral, symbol, whiteSpace)

63+import qualified Text.Trifecta as P

64−import Text.Trifecta.Delta

64+import qualified Text.Trifecta.Delta as P

66{-

67@

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

84@

85-}

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

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

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

88− noArgs docs

88+ noArgs docs

89− reservedHL "module"

89+ reservedHL "module"

90− (i, ifc) <- identifier

90+ (i, ifc) <- identifier

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

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

92− let modName = moduleName i

92+ let modName = moduleName i

93− return (fmap fst docs,

93+ return (fmap fst docs,

94− modName,

94+ modName,

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

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

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

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

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

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

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

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

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

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

119import_ :: IdrisParser ImportInfo

120import_ = do fc <- getFC

121 reservedHL "import"

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

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

123− return True)

124 (id, idfc) <- identifier

123 (id, idfc) <- identifier

125 newName <- optional (do reservedHL "as"

124 newName <- optional (do reservedHL "as"

126 identifier)

125 identifier)

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

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

128 return $ ImportInfo reexport (toPath id)

127 return $ ImportInfo reexport (toPath id)

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

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

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

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

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

143 decls <- many (decl syn)

142 decls <- many (decl syn)

144 let c = concat decls

143 let c = concat decls

145 case maxline syn of

144 case maxline syn of

146− Nothing -> do notOpenBraces; eof

145+ Nothing -> do notOpenBraces; P.eof

147 _ -> return ()

146 _ -> return ()

148 ist <- get

147 ist <- get

149 fc <- getFC

148 fc <- getFC

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

172@

171@

173-}

172-}

174decl :: SyntaxInfo -> IdrisParser [PDecl]

173decl :: SyntaxInfo -> IdrisParser [PDecl]

175−decl syn = try (externalDecl syn)

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

176 <|> internalDecl syn

175 <|> internalDecl syn

177 <?> "declaration"

176 <?> "declaration"

178

177

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

195 if continue then

194 if continue then

196 do notEndBlock

195 do notEndBlock

197 declBody continue

196 declBody continue

198− else try (do notEndBlock

197+ else P.try (do notEndBlock

199− declBody continue)

198+ declBody continue)

200 <|> fail "End of readable input"

199 <|> fail "End of readable input"

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

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

202 declBody b =

201 declBody b =

203− try (implementation True syn)

202+ P.try (implementation True syn)

204− <|> try (openInterface syn)

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

205 <|> declBody' b

204 <|> declBody' b

206 <|> using_ syn

205 <|> using_ syn

207 <|> params syn

206 <|> params syn

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

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

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

277 -> IdrisParser [PDecl]

276 -> IdrisParser [PDecl]

278declExtension syn ns rules =

277declExtension syn ns rules =

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

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

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

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

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

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

282 n <- extSymbol symb

281 n <- extSymbol symb

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

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

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

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

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

427-}

426-}

428syntaxRule :: SyntaxInfo -> IdrisParser Syntax

427syntaxRule :: SyntaxInfo -> IdrisParser Syntax

429syntaxRule syn

428syntaxRule syn

430− = do sty <- try (do

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

431 pushIndent

430 pushIndent

432− sty <- option AnySyntax

431+ sty <- P.option AnySyntax

433− (do reservedHL "term"; return TermSyntax

432+ (TermSyntax <$ reservedHL "term"

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

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

435 reservedHL "syntax"

434 reservedHL "syntax"

436 return sty)

435 return sty)

437 syms <- some syntaxSym

436 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"

439 let ns = mapMaybe getName syms

438 let ns = mapMaybe getName syms

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

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

441− $ unexpected "repeated variable in syntax rule"

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

442 lchar '='

441 lchar '='

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

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

444 terminator

443 terminator

445 return (Rule (mkSimple syms) tm sty)

444 return (Rule (mkSimple syms) tm sty)

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

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

447 syms <- some syntaxSym

446 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"

449 let ns = mapMaybe getName syms

448 let ns = mapMaybe getName syms

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

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

451− $ unexpected "repeated variable in syntax rule"

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

452 lchar '='

451 lchar '='

453 openBlock

452 openBlock

454 dec <- some (decl syn)

453 dec <- some (decl syn)

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

544@

543@

545 -}

544 -}

546syntaxSym :: IdrisParser SSymbol

545syntaxSym :: IdrisParser SSymbol

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

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

548− return (Expr n))

547+ return (Expr n))

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

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

550− return (Binding n))

549+ return (Binding n))

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

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

552 return (Keyword n)

551 return (Keyword n)

553 <|> do sym <- fmap fst stringLiteral

552 <|> do sym <- fmap fst stringLiteral

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

561@

560@

562-}

561-}

563fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

562fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

564−fnDecl syn = try (do notEndBlock

563+fnDecl syn = P.try (do notEndBlock

565− d <- fnDecl' syn

564+ d <- fnDecl' syn

566− i <- get

565+ i <- get

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

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

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

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

569

568

570{-| Parses a function declaration

569{-| Parses a function declaration

571

570

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

580-}

579-}

581fnDecl' :: SyntaxInfo -> IdrisParser PDecl

580fnDecl' :: SyntaxInfo -> IdrisParser PDecl

582fnDecl' syn = checkDeclFixity $

581fnDecl' 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

584 pushIndent

583 pushIndent

585 (doc, argDocs) <- docstring syn

584 (doc, argDocs) <- docstring syn

586 (opts, acc) <- fnOpts

585 (opts, acc) <- fnOpts

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

658-}

657-}

659fnOpt :: IdrisParser FnOpt

658fnOpt :: IdrisParser FnOpt

660fnOpt = do reservedHL "total"; return TotalFn

659fnOpt = do reservedHL "total"; return TotalFn

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

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

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

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

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

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

664− return $ CExport c

663+ return $ CExport c

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

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

666− return NoImplicit

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

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

668− return Inlinable

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

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

670− return StaticFn

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

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

672 fc <- getFC

668 fc <- getFC

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

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

674 return AssertTotal

670 return AssertTotal

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

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

676− return ErrorHandler

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

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

678− return ErrorReverse

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

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

680− return ErrorReduce

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

682− return Reflection

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

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

684− return AutoHint

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

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

686− return OverlappingDictionary

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

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

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

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

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

689 return $ Specialise ns

679 return $ Specialise ns

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

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

691 <?> "function modifier"

681 <?> "function modifier"

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

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

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

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

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

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

695− return (Just (fromInteger reds)))

685+ return (Just (fromInteger reds)))

696 return (n, t)

686 return (n, t)

697

687

698{-| Parses a postulate

688{-| Parses a postulate

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

705-}

695-}

706postulate :: SyntaxInfo -> IdrisParser PDecl

696postulate :: SyntaxInfo -> IdrisParser PDecl

707postulate syn = do (doc, ext)

697postulate syn = do (doc, ext)

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

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

709− pushIndent

699+ pushIndent

710− ext <- ppostDecl

700+ ext <- ppostDecl

711− return (doc, ext)

701+ return (doc, ext)

712 ist <- get

702 ist <- get

713 (opts, acc) <- fnOpts

703 (opts, acc) <- fnOpts

714 (n_in, nfc) <- fnName

704 (n_in, nfc) <- fnName

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

768 do reservedHL "using"

758 do reservedHL "using"

769 reservedHL "implementation"

759 reservedHL "implementation"

770 fc <- getFC

760 fc <- getFC

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

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

772

762

773 openBlock

763 openBlock

774 ds <- many (decl syn)

764 ds <- many (decl syn)

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

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

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

849interfaceBlock syn = do reservedHL "where"

839interfaceBlock syn = do reservedHL "where"

850 openBlock

840 openBlock

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

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

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

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

853− n <- constructor

843+ n <- constructor

854− return (Just n, doc))

844+ return (Just n, doc))

855 ist <- get

845 ist <- get

856 let cd' = annotate syn ist cd

846 let cd' = annotate syn ist cd

857

847

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

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

859 <|> do x <- data_ syn

849 <|> do x <- data_ syn

860 return [x]

850 return [x]

861 <|> fnDecl syn)

851 <|> fnDecl syn)

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

886-}

876-}

887interface_ :: SyntaxInfo -> IdrisParser [PDecl]

877interface_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

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

890− acc <- accessibility

880+ acc <- accessibility

891− interfaceKeyword

881+ interfaceKeyword

892− return (doc, argDocs, acc))

882+ return (doc, argDocs, acc))

893 fc <- getFC

883 fc <- getFC

894 cons <- constraintList syn

884 cons <- constraintList syn

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

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

896 (n_in, nfc) <- fnName

886 (n_in, nfc) <- fnName

897 let n = expandNS syn n_in

887 let n = expandNS syn n_in

898 cs <- many carg

888 cs <- many carg

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

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

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

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

901 accData acc n (concatMap declared ds)

891 accData acc n (concatMap declared ds)

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

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

903 <?> "interface declaration"

893 <?> "interface declaration"

904 where

894 where

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

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

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

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

907

897

908 interfaceKeyword :: IdrisParser ()

898 interfaceKeyword :: IdrisParser ()

909 interfaceKeyword = reservedHL "interface"

899 interfaceKeyword = reservedHL "interface"

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

964

954

965 implementationUsing :: IdrisParser [Name]

955 implementationUsing :: IdrisParser [Name]

966 implementationUsing = do reservedHL "using"

956 implementationUsing = do reservedHL "using"

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

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

968 return (map fst ns)

958 return (map fst ns)

969 <|> return []

959 <|> return []

970

960

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

972docstring :: SyntaxInfo

962docstring :: SyntaxInfo

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

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

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

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

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

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

976 ist <- get

966 ist <- get

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

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

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

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

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

1005-}

995-}

1006usingDeclList :: SyntaxInfo -> IdrisParser [Using]

996usingDeclList :: SyntaxInfo -> IdrisParser [Using]

1007usingDeclList syn

997usingDeclList syn

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

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

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

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

1010 lchar ':'

1000 lchar ':'

1011 t <- typeExpr (disallowImp syn)

1001 t <- typeExpr (disallowImp syn)

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

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

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

1022@

1012@

1023-}

1013-}

1024usingDecl :: SyntaxInfo -> IdrisParser Using

1014usingDecl :: SyntaxInfo -> IdrisParser Using

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

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

1026− lchar ':'

1016+ lchar ':'

1027− t <- typeExpr (disallowImp syn)

1017+ t <- typeExpr (disallowImp syn)

1028− return (UImplicit x t))

1018+ return (UImplicit x t))

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

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

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

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

1031 return (UConstraint c xs)

1021 return (UConstraint c xs)

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

1068-}

1058-}

1069argExpr :: SyntaxInfo -> IdrisParser PTerm

1059argExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

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

1072 <?> "argument expression"

1062 <?> "argument expression"

1073

1063

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

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

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

1090 expr syn

1080 expr syn

1091 <|> do symbol "?=";

1081 <|> do symbol "?=";

1092 fc <- getFC

1082 fc <- getFC

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

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

1094− return n)

1084+ return n)

1095 r <- expr syn

1085 r <- expr syn

1096 return (addLet fc name r)

1086 return (addLet fc name r)

1097 <|> impossible

1087 <|> impossible

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

1135-}

1125-}

1136clause :: SyntaxInfo -> IdrisParser PClause

1126clause :: SyntaxInfo -> IdrisParser PClause

1137clause syn

1127clause syn

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

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

1139 fc <- getFC

1129 fc <- getFC

1140 ist <- get

1130 ist <- get

1141 n <- case lastParse ist of

1131 n <- case lastParse ist of

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

1143 Nothing -> fail "Invalid clause"

1133 Nothing -> fail "Invalid clause"

1144 (do r <- rhs syn n

1134 (do r <- rhs syn n

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

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

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

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

1147− popIndent

1148− return x,

1149− do terminator

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

1150− return ([], [])]

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

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

1152 popIndent

1139 popIndent

1153 reservedHL "with"

1140 reservedHL "with"

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

1158 let withs = concat ds

1145 let withs = concat ds

1159 closeBlock

1146 closeBlock

1160 return $ PWithR fc wargs wval pn withs)

1147 return $ PWithR fc wargs wval pn withs)

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

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

1162− ty <- simpleExpr syn

1149+ ty <- simpleExpr syn

1163− symbol "<=="

1150+ symbol "<=="

1164− return ty)

1151+ return ty)

1165 fc <- getFC

1152 fc <- getFC

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

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

1167 r <- rhs syn n

1154 r <- rhs syn n

1168 let wsyn = syn { syn_namespace = [] }

1155 let wsyn = syn { syn_namespace = [] }

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

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

1170− popIndent

1171− return x,

1172− do terminator

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

1173− return ([], [])]

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

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

1175 ty

1159 ty

1176 (PMatchApp fc n)

1160 (PMatchApp fc n)

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

1178 ist <- get

1162 ist <- get

1179 put (ist { lastParse = Just n })

1163 put (ist { lastParse = Just n })

1180 return $ PClause fc n capp [] r wheres

1164 return $ PClause fc n capp [] r wheres

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

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

1182 pushIndent

1166 pushIndent

1183 l <- argExpr syn

1167 l <- argExpr syn

1184 (op, nfc) <- symbolicOperatorFC

1168 (op, nfc) <- symbolicOperatorFC

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

1191 wargs <- many (wExpr syn)

1175 wargs <- many (wExpr syn)

1192 (do rs <- rhs syn n

1176 (do rs <- rhs syn n

1193 let wsyn = syn { syn_namespace = [] }

1177 let wsyn = syn { syn_namespace = [] }

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

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

1195− popIndent

1196− return x,

1197− do terminator

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

1198− return ([], [])]

1199 ist <- get

1180 ist <- get

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

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

1201 put (ist { lastParse = Just n })

1182 put (ist { lastParse = Just n })

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

1215 <|> do pushIndent

1196 <|> do pushIndent

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

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

1217 fc <- getFC

1198 fc <- getFC

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

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

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

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

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

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

1221 wargs <- many (wExpr syn)

1202 wargs <- many (wExpr syn)

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

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

1223 (do r <- rhs syn n

1204 (do r <- rhs syn n

1224 let wsyn = syn { syn_namespace = [] }

1205 let wsyn = syn { syn_namespace = [] }

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

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

1226− popIndent

1227− return x,

1228− do terminator

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

1229− return ([], [])]

1230 ist <- get

1208 ist <- get

1231 put (ist { lastParse = Just n })

1209 put (ist { lastParse = Just n })

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

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

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

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

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

1244 <?> "function clause"

1222 <?> "function clause"

1245 where

1223 where

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

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

1247− n <- fnName

1225+ n <- fnName

1248− return (Just n))

1226+ return (Just n))

1249

1227

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

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

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

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

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

1336@

1314@

1337-}

1315-}

1338directive :: SyntaxInfo -> IdrisParser [PDecl]

1316directive :: SyntaxInfo -> IdrisParser [PDecl]

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

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

1340 cgn <- codegen_

1318 cgn <- codegen_

1341 lib <- fmap fst stringLiteral

1319 lib <- fmap fst stringLiteral

1342 return [PDirective (DLib cgn lib)]

1320 return [PDirective (DLib cgn lib)]

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

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

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

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

1345 return [PDirective (DLink cgn obj)]

1323 return [PDirective (DLink cgn obj)]

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

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

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

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

1348 return [PDirective (DFlag cgn flag)]

1326 return [PDirective (DFlag cgn flag)]

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

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

1350 cgn <- codegen_

1328 cgn <- codegen_

1351 hdr <- fst <$> stringLiteral

1329 hdr <- fst <$> stringLiteral

1352 return [PDirective (DInclude cgn hdr)]

1330 return [PDirective (DInclude cgn hdr)]

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

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

1354 return [PDirective (DHide n)]

1332 return [PDirective (DHide n)]

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

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

1356 return [PDirective (DFreeze n)]

1334 return [PDirective (DFreeze n)]

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

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

1358 return [PDirective (DThaw n)]

1336 return [PDirective (DThaw n)]

1359 -- injectivity assertins are intended for debugging purposes

1337 -- injectivity assertins are intended for debugging purposes

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

1338 -- 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

1362 return [PDirective (DInjective n)]

1340 return [PDirective (DInjective n)]

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

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

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

1342 -- 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

1366-- return [PDirective (DSetTotal n)]

1344-- return [PDirective (DSetTotal n)]

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

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

1368 acc <- accessibility

1346 acc <- accessibility

1369 ist <- get

1347 ist <- get

1370 put ist { default_access = acc }

1348 put ist { default_access = acc }

1371 return [PDirective (DAccess acc)]

1349 return [PDirective (DAccess acc)]

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

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

1373 i <- get

1351 i <- get

1374 put (i { default_total = tot } )

1352 put (i { default_total = tot } )

1375 return [PDirective (DDefault tot)]

1353 return [PDirective (DDefault tot)]

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

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

1377 i <- fst <$> natural

1355 i <- fst <$> natural

1378 return [PDirective (DLogging i)]

1356 return [PDirective (DLogging i)]

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

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

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

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

1381 return [PDirective (DDynamicLibs libs)]

1359 return [PDirective (DDynamicLibs libs)]

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

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

1383 (ty, tyFC) <- fnName

1361 (ty, tyFC) <- fnName

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

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

1385 return [PDirective (DNameHint ty tyFC ns)]

1363 return [PDirective (DNameHint ty tyFC ns)]

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

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

1387 (fn, nfc) <- fnName

1365 (fn, nfc) <- fnName

1388 (arg, afc) <- fnName

1366 (arg, afc) <- fnName

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

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

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

1368 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;

1392 return [PDirective (DLanguage ext)]

1370 return [PDirective (DLanguage ext)]

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

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

1394 n <- fst <$> fnName

1372 n <- fst <$> fnName

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

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

1396 return [PDirective (DDeprecate n alt)]

1374 return [PDirective (DDeprecate n alt)]

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

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

1398 n <- fst <$> fnName

1376 n <- fst <$> fnName

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

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

1400 return [PDirective (DFragile n alt)]

1378 return [PDirective (DFragile n alt)]

1401 <|> do fc <- getFC

1379 <|> do fc <- getFC

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

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

1403 fn <- fst <$> fnName

1381 fn <- fst <$> fnName

1404 arg <- fst <$> iName []

1382 arg <- fst <$> iName []

1405 return [PDirective (DUsed fc fn arg)]

1383 return [PDirective (DUsed fc fn arg)]

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

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

1407 b <- on_off

1385 b <- on_off

1408 return [PDirective (DAutoImplicits b)]

1386 return [PDirective (DAutoImplicits b)]

1409 <?> "directive"

1387 <?> "directive"

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

1440@

1418@

1441 -}

1419 -}

1442provider :: SyntaxInfo -> IdrisParser [PDecl]

1420provider :: SyntaxInfo -> IdrisParser [PDecl]

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

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

1444− fc1 <- getFC

1422+ fc1 <- getFC

1445− lchar '%'

1423+ lchar '%'

1446− fc2 <- reservedFC "provide"

1424+ fc2 <- reservedFC "provide"

1447− highlightP (spanFC fc1 fc2) AnnKeyword

1425+ highlightP (spanFC fc1 fc2) AnnKeyword

1448− return doc)

1426+ return doc)

1449 provideTerm doc <|> providePostulate doc

1427 provideTerm doc <|> providePostulate doc

1450 <?> "type provider"

1428 <?> "type provider"

1451 where provideTerm doc =

1429 where provideTerm doc =

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

1469@

1447@

1470-}

1448-}

1471transform :: SyntaxInfo -> IdrisParser [PDecl]

1449transform :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

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

1474 -- actually mean...

1452 -- actually mean...

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

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

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

1489-}

1467-}

1490runElabDecl :: SyntaxInfo -> IdrisParser PDecl

1468runElabDecl :: SyntaxInfo -> IdrisParser PDecl

1491runElabDecl syn =

1469runElabDecl syn =

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

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

1493− lchar '%'

1471+ lchar '%'

1494− fc' <- reservedFC "runElab"

1472+ fc' <- reservedFC "runElab"

1495− return (spanFC fc fc'))

1473+ return (spanFC fc fc'))

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

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

1497 highlightP kwFC AnnKeyword

1475 highlightP kwFC AnnKeyword

1498 return $ PRunElabDecl kwFC script (syn_namespace syn)

1476 return $ PRunElabDecl kwFC script (syn_namespace syn)

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

1500

1478

1501{- * Loading and parsing -}

1479{- * Loading and parsing -}

1502{-| Parses an expression from input -}

1480{-| Parses an expression from input -}

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

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

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

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

1505

1483

1506{-| Parses a constant form input -}

1484{-| Parses a constant form input -}

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

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

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

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

1509

1487

1510{-| Parses a tactic from input -}

1488{-| Parses a tactic from input -}

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

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

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

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

1513

1491

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

1492{-| 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)

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

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

1517 where elabShellCmd = char ':' >>

1495 where elabShellCmd = char ':' >>

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

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

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

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

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

1526 (do reserved "doc"

1504 (do reserved "doc"

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

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

1528− eof

1506+ P.eof

1529 return (EDocStr doc))

1507 return (EDocStr doc))

1530 <?> "elab command"

1508 <?> "elab command"

1531 expressionTactic cmds tactic =

1509 expressionTactic cmds tactic =

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

1536 spaced parser = indentGt *> parser

1514 spaced parser = indentGt *> parser

1537

1515

1538-- | Parse module header and imports

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

1540parseImports fname input

1518parseImports fname input

1541 = do i <- getIState

1519 = do i <- getIState

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

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

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

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

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

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

1545 do putIState i

1523 do putIState i

1546 fname' <- runIO $ Dir.makeAbsolute fname

1524 fname' <- runIO $ Dir.makeAbsolute fname

1547 sendHighlighting $ addPath annots fname'

1525 sendHighlighting $ addPath annots fname'

1548 return x

1526 return x

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

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

1550 [ImportInfo],

1528 [ImportInfo],

1551− Maybe Delta),

1529+ Maybe P.Delta),

1552 [(FC, OutputAnnotation)], IState)

1530 [(FC, OutputAnnotation)], IState)

1553 imports = do optional shebang

1531 imports = do optional shebang

1554 whiteSpace

1532 whiteSpace

1555 (mdoc, mname, annots) <- moduleHeader

1533 (mdoc, mname, annots) <- moduleHeader

1556 ps_exp <- many import_

1534 ps_exp <- many import_

1557− mrk <- mark

1535+ mrk <- P.mark

1558− isEof <- lookAheadMatches eof

1536+ isEof <- lookAheadMatches P.eof

1559 let mrk' = if isEof

1537 let mrk' = if isEof

1560 then Nothing

1538 then Nothing

1561 else Just mrk

1539 else Just mrk

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

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

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

1573

1551

1574 shebang :: IdrisParser ()

1552 shebang :: IdrisParser ()

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

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

1576

1554

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

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

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

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

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

1596

1574

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

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

1598-- documentation strings.

1576-- documentation strings.

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

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

1600 Idris [PDecl]

1578 Idris [PDecl]

1601parseProg syn fname input mrk

1579parseProg syn fname input mrk

1602 = do i <- getIState

1580 = do i <- getIState

1603 case runparser mainProg i fname input of

1581 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

1605 -- this can't be the solution!

1583 -- this can't be the solution!

1606 -- Issue #1575 on the issue tracker.

1584 -- Issue #1575 on the issue tracker.

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

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

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

1609 i <- getIState

1587 i <- getIState

1610 case idris_outputmode i of

1588 case idris_outputmode i of

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

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

1613 putIState (i { errSpan = Just fc })

1591 putIState (i { errSpan = Just fc })

1614 return []

1592 return []

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

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

1616− reportParserWarnings

1594+ reportParserWarnings

1617− return $ collect x

1595+ return $ collect x

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

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

1619 mainProg = case mrk of

1597 mainProg = case mrk of

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

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

1621 Just mrk -> do

1599 Just mrk -> do

1622− release mrk

1600+ P.release mrk

1623 ds <- prog syn

1601 ds <- prog syn

1624 i' <- get

1602 i' <- get

1625 return (ds, i')

1603 return (ds, i')

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

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

22import Control.Monad.State.Strict

23import Data.List

24import Data.Maybe

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

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

26− stringLiteral, symbol, whiteSpace)

26+import qualified Text.Trifecta as P

28{- | Parses a record type declaration

29Record ::=

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

31-}

32record :: SyntaxInfo -> IdrisParser PDecl

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

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

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

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

35 ist <- get

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

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

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

45 let tyn = expandNS syn tyn_in

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

47 syn_namespace syn }

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

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

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

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

51 case cname of

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

62 ist <- get

63 fc <- getFC

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

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

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

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

67 n <- constructor

68 return (Just n, doc))

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

170-}

171data_ :: SyntaxInfo -> IdrisParser PDecl

172data_ syn = checkDeclFixity $

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

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

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

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

175 pushIndent

176 acc <- accessibility

177 elim <- dataOpts []

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

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

185 fc <- getFC

186 (tyn_in, nfc) <- fnName

187− (do try (lchar ':')

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

188 ty <- typeExpr (allowImp syn)

189 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

191 reservedHL "where"

192 cons <- indentedBlock (constructor syn)

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

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

199 return x)

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

201 let tyn = expandNS syn tyn_in

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

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

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

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 "

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

205− let n = show tyn_in ++ " "

205+ let n = show tyn_in ++ " "

206− let s = kw ++ n

206+ let s = kw ++ n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

217 do let cty = bindArgs cargs conty

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

238-}

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

240constructor syn

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

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

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

243 let cn = expandNS syn cn_in

244 lchar ':'

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

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

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

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

247 ty <- typeExpr (allowImp syn)

248 ist <- get

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

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

258-}

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

260simpleConstructor syn

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

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

262 ist <- get

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

264 (cn_in, nfc) <- fnName

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

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

25import Data.List

26import Data.Maybe

27import Text.Parser.Expression

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

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

29− stringLiteral, symbol, whiteSpace)

29+import qualified Text.Trifecta as P

31-- | Allow implicit type declarations

32allowImp :: SyntaxInfo -> SyntaxInfo

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

53 -}

54fullExpr :: SyntaxInfo -> IdrisParser PTerm

55fullExpr syn = do x <- expr syn

56− eof

56+ P.eof

57 i <- get

58 return $ debindApp syn (desugar syn i x)

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

61tryFullExpr syn st input =

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

63− Success tm -> Right tm

63+ P.Success tm -> Right tm

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

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

66{- | Parses an expression

67@

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

89@

90 -}

91expr' :: SyntaxInfo -> IdrisParser PTerm

92−expr' syn = try (externalExpr syn)

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

93 <|> internalExpr syn

94 <?> "expression"

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

140

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

142extension syn ns rules =

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

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

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

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

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

146 n <- extensionSymbol symb

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

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

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

397-}

398simpleExpr :: SyntaxInfo -> IdrisParser PTerm

399simpleExpr syn =

400− try (simpleExternalExpr syn)

400+ P.try (simpleExternalExpr syn)

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

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

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

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

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

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

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

408 <|> proofExpr syn

409 <|> tacticsExpr syn

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

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

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

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

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

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

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

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

422 if inPattern syn

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

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

424− (do reservedOp "@"

424+ (do reservedOp "@"

425− s <- simpleExpr syn

425+ s <- simpleExpr syn

426− fcIn <- getFC

426+ fcIn <- getFC

427− return (PAs fcIn x s))

427+ return (PAs fcIn x s))

428 else return (PRef fc [fc] x)

429 <|> idiom syn

430 <|> listExpr syn

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

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

468 lchar ')'

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

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

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

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

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

472− guardNotPrefix opName

472+ guardNotPrefix opName

473−

473+

474− e <- expr syn

474+ e <- expr syn

475− lchar ')'

475+ lchar ')'

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

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

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

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

478− pexp e]))

478+ pexp e]))

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

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

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

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

481− lchar ')'

481+ lchar ')'

482− fc <- getFC

482+ fc <- getFC

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

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

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

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

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

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

486 <|> bracketedExpr syn open l)

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

488 bracketedExpr (allowConstr syn) open l

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

510 IsTerm -> exprPart False

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

512 where nametypePart = do

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

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

514 (ln, lnfc) <- name

515 colonFC <- lcharFC ':'

516 return (ln, lnfc, colonFC)

517 lty <- expr' syn

518 starsFC <- reservedOpFC "**"

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

520− namePart = try $ do

520+ namePart = P.try $ do

521 (ln, lnfc) <- name

522 starsFC <- reservedOpFC "**"

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

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

590@

591-}

592alt :: 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 "|)"

594 return (PAlternative [] FirstSuccess alts)

595

596{- | Parses a possibly hidden simple expression

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

615 ;

616-}

617unifyLog :: 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")

619 tm <- simpleExpr syn

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

621 return (PUnifyLog tm)

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

627 ;

628-}

629runElab :: 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")

631 fc <- getFC

632 tm <- simpleExpr syn

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

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

641-}

642disamb :: SyntaxInfo -> IdrisParser PTerm

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

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

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

645 tm <- expr' syn

646 highlightP kw AnnKeyword

647 return (PDisamb (map tons ns) tm)

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

656@

657-}

658noImplicits :: SyntaxInfo -> IdrisParser PTerm

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

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

660 tm <- simpleExpr syn

661 return (PNoImplicits tm)

662 <?> "no implicits expression"

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

675-}

676app :: SyntaxInfo -> IdrisParser PTerm

677app syn = do f <- simpleExpr syn

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

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

679 fc <- getFC

680 ff <- fst <$> fnName

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

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

737implicitArg syn = do lchar '{'

738 (n, nfc) <- name

739 fc <- getFC

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

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

741− expr syn)

741+ expr syn)

742 lchar '}'

743 return (pimp n v True)

744 <?> "implicit function argument"

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

800-}

801namequote :: SyntaxInfo -> IdrisParser PTerm

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

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

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

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

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

805 (do fc <- symbolFC "`{"

806 return (fc, True))

807 (n, nfc) <- fnName

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

871 <?> "field setter"

872

873 fieldGet :: IdrisParser [Name]

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

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

875

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

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

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

878− return (Left fs))

879 <|> do f <- fieldGet

878 <|> do f <- fieldGet

880 return (Right f)

879 return (Right f)

881

880

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

942-}

941-}

943lambda :: SyntaxInfo -> IdrisParser PTerm

942lambda :: SyntaxInfo -> IdrisParser PTerm

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

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

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

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

946 fc <- getFC

945 fc <- getFC

947 sc <- lambdaTail

946 sc <- lambdaTail

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

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

949 <|>

948 <|>

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

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

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

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

952− return (fc, e))

951+ return (fc, e))

953− (lchar ',')

952+ (lchar ',')

954 sc <- lambdaTail

953 sc <- lambdaTail

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

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

956 <?> "lambda expression"

955 <?> "lambda expression"

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

996@

995@

997 -}

996 -}

998let_ :: SyntaxInfo -> IdrisParser PTerm

997let_ :: SyntaxInfo -> IdrisParser PTerm

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

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

1000− ls <- indentedBlock (let_binding syn)

999+ ls <- indentedBlock (let_binding syn)

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

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

1002− highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1001+ highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1003− return (buildLets ls sc))

1002+ return (buildLets ls sc))

1004 <?> "let binding"

1003 <?> "let binding"

1005 where buildLets [] sc = sc

1004 where buildLets [] sc = sc

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

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

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

1010

1009

1011let_binding syn = do fc <- getFC;

1010let_binding syn = do fc <- getFC;

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

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

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

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

1014 lchar '='

1013 lchar '='

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

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

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

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

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

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

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

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

1019 where isVar (PRef _ _ _) = True

1018 where isVar (PRef _ _ _) = True

1020 isVar _ = False

1019 isVar _ = False

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

1079 return (Exp opts st False RigW)

1078 return (Exp opts st False RigW)

1080

1079

1081explicitPi opts st syn

1080explicitPi opts st syn

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

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

1083 binder <- bindsymbol opts st syn

1082 binder <- bindsymbol opts st syn

1084 sc <- expr (allowConstr syn)

1083 sc <- expr (allowConstr syn)

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

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

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

1147 x <- opExpr syn

1146 x <- opExpr syn

1148 (do binder <- bindsymbol opts st syn

1147 (do binder <- bindsymbol opts st syn

1149 sc <- expr syn

1148 sc <- expr syn

1150− notFollowedBy $ reservedOp "=>"

1149+ P.notFollowedBy $ reservedOp "=>"

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

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

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

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

1153 return x

1152 return x

1154

1153

1155

1154

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

1158 do opts <- piOpts syn

1157 do opts <- piOpts syn

1159 st <- static

1158 st <- static

1160 explicitPi opts st syn

1159 explicitPi opts st syn

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

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

1162 <|> if constraintAllowed syn

1161 <|> if constraintAllowed syn

1163− then try (unboundPiNoConstraint opts st syn)

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

1164− <|> constraintPi opts st syn

1163+ <|> constraintPi opts st syn

1165 else unboundPi opts st syn

1164 else unboundPi opts st syn

1166 <?> "dependent type signature"

1165 <?> "dependent type signature"

1167

1166

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

1186@

1185@

1187-}

1186-}

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

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

1189−constraintList syn = try (constraintList1 syn)

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

1190 <|> return []

1189 <|> return []

1191

1190

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

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

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

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

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

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

1195− lchar ')'

1194+ lchar ')'

1196− reservedOp "=>"

1195+ reservedOp "=>"

1197− return tys)

1196+ return tys)

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

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

1199− reservedOp "=>"

1198+ reservedOp "=>"

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

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

1201 <?> "type constraint list"

1200 <?> "type constraint list"

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

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

1203− e <- expr (disallowImp syn)

1202+ e <- expr (disallowImp syn)

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

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

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

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

1206 return (RigW, defname, NoFC, e)

1205 return (RigW, defname, NoFC, e)

1207 defname = sMN 0 "constraint"

1206 defname = sMN 0 "constraint"

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

1222@

1221@

1223-}

1222-}

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

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

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

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

1226− (x, xfc) <- fnName

1225+ (x, xfc) <- fnName

1227− lchar ':'

1226+ lchar ':'

1228− t <- typeExpr (disallowImp syn)

1227+ t <- typeExpr (disallowImp syn)

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

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

1230− (lchar ','))

1229+ (lchar ','))

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

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

1232 lchar ':'

1231 lchar ':'

1233 t <- typeExpr (disallowImp syn)

1232 t <- typeExpr (disallowImp syn)

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

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

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

1250@

1249@

1251-}

1250-}

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

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

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

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

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

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

1255− expr syn)

1254+ expr syn)

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

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

1257− (lchar ',')

1256+ (lchar ',')

1258 <?> "type declaration list"

1257 <?> "type declaration list"

1259 where nameOrPlaceholder :: IdrisParser (Name, FC)

1258 where nameOrPlaceholder :: IdrisParser (Name, FC)

1260 nameOrPlaceholder = fnName

1259 nameOrPlaceholder = fnName

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

1286listExpr :: SyntaxInfo -> IdrisParser PTerm

1285listExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

1288 lchar '['; fc <- getFC;

1287 lchar '['; fc <- getFC;

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

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

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

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

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

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

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

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

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

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

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

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

1295 lchar ']'

1294 lchar ']'

1296 return (PDoBlock (map addGuard qs ++

1295 return (PDoBlock (map addGuard qs ++

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

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

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

1350-}

1349-}

1351do_ :: SyntaxInfo -> IdrisParser PDo

1350do_ :: SyntaxInfo -> IdrisParser PDo

1352do_ syn

1351do_ syn

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

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

1354− (i, ifc) <- name

1353+ (i, ifc) <- name

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

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

1356− expr' syn)

1355+ expr' syn)

1357− reservedOp "="

1356+ reservedOp "="

1358− fc <- getFC

1357+ fc <- getFC

1359− e <- expr syn

1358+ e <- expr syn

1360− highlightP kw AnnKeyword

1359+ highlightP kw AnnKeyword

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

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

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

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

1363− i <- expr' syn

1362+ i <- expr' syn

1364− reservedOp "="

1363+ reservedOp "="

1365− fc <- getFC

1364+ fc <- getFC

1366− sc <- expr syn

1365+ sc <- expr syn

1367− highlightP kw AnnKeyword

1366+ highlightP kw AnnKeyword

1368− return (DoLetP fc i sc))

1367+ return (DoLetP fc i sc))

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

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

1370− fc <- getFC

1369+ fc <- getFC

1371− sc <- expr syn

1370+ sc <- expr syn

1372− highlightP kw AnnKeyword

1371+ highlightP kw AnnKeyword

1373− return (DoRewrite fc sc))

1372+ return (DoRewrite fc sc))

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

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

1375− symbol "<-"

1374+ symbol "<-"

1376− fc <- getFC

1375+ fc <- getFC

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

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

1378− option (DoBind fc i ifc e)

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

1379− (do lchar '|'

1378+ (do lchar '|'

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

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

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

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

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

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

1383− symbol "<-"

1382+ symbol "<-"

1384− fc <- getFC

1383+ fc <- getFC

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

1384+ e <- expr (syn { withAppAllowed = False });

1386− option (DoBindP fc i e [])

1385+ P.option (DoBindP fc i e [])

1387− (do lchar '|'

1386+ (do lchar '|'

1388− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1387+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1389− return (DoBindP fc i e ts)))

1388+ return (DoBindP fc i e ts)))

1390 <|> do e <- expr syn

1389 <|> do e <- expr syn

1391 fc <- getFC

1390 fc <- getFC

1392 return (DoExp fc e)

1391 return (DoExp fc e)

1393 <?> "do block expression"

1392 <?> "do block expression"

1394

1393

1395do_alt syn = do l <- expr' syn

1394do_alt syn = do l <- expr' syn

1396− option (Placeholder, l)

1395+ P.option (Placeholder, l)

1397− (do symbol "=>"

1396+ (do symbol "=>"

1398− r <- expr' syn

1397+ r <- expr' syn

1399− return (l, r))

1398+ return (l, r))

1400

1399

1401{- | Parses an expression in idiom brackets

1400{- | Parses an expression in idiom brackets

1402@

1401@

@@ -1451,14 +1450,14 @@ constants =

1451

1450

1452-- | Parse a constant and its source span

1451-- | Parse a constant and its source span

1453constant :: IdrisParser (Idris.Core.TT.Const, FC)

1452constant :: IdrisParser (Idris.Core.TT.Const, FC)

1454−constant = choice [ do fc <- reservedFC name; return (ty, fc)

1453+constant = P.choice [ do fc <- reservedFC name; return (ty, fc)

1455− | (name, ty) <- constants

1454+ | (name, ty) <- constants

1456− ]

1455+ ]

1457− <|> do (f, fc) <- try float; return (Fl f, fc)

1456+ <|> do (f, fc) <- P.try float; return (Fl f, fc)

1458 <|> do (i, fc) <- natural; return (BI i, fc)

1457 <|> do (i, fc) <- natural; return (BI i, fc)

1459 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

1458 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

1460 <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1459 <|> 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

1462 <?> "constant or literal"

1461 <?> "constant or literal"

1463

1462

1464{- | Parses a verbatim multi-line string literal (triple-quoted)

1463{- | Parses a verbatim multi-line string literal (triple-quoted)

@@ -1470,11 +1469,11 @@ VerbatimString_t ::=

1470@

1469@

1471 -}

1470 -}

1472verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1471verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1473−verbatimStringLiteral = token $ do (FC f start _) <- getFC

1472+verbatimStringLiteral = P.token $ do (FC f start _) <- getFC

1474− try $ string "\"\"\""

1473+ P.try $ string "\"\"\""

1475− str <- manyTill anyChar $ try (string "\"\"\"")

1474+ str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")

1476− (FC _ _ end) <- getFC

1475+ (FC _ _ end) <- getFC

1477− return (str, FC f start end)

1476+ return (str, FC f start end)

1478

1477

1479{- | Parses a static modifier

1478{- | Parses a static modifier

1480

1479

@@ -1545,7 +1544,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

1545tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1544tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1546tactics =

1545tactics =

1547 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1546 [ (["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)

1549 , noArgs ["intros"] Intros

1548 , noArgs ["intros"] Intros

1550 , noArgs ["unfocus"] Unfocus

1549 , noArgs ["unfocus"] Unfocus

1551 , (["refine"], Just ExprTArg, const $

1550 , (["refine"], Just ExprTArg, const $

@@ -1593,7 +1592,7 @@ tactics =

1593 , noArgs ["trivial"] Trivial

1592 , noArgs ["trivial"] Trivial

1594 , noArgs ["unify"] DoUnify

1593 , noArgs ["unify"] DoUnify

1595 , (["search"], Nothing, const $

1594 , (["search"], Nothing, const $

1596− do depth <- option 10 $ fst <$> natural

1595+ do depth <- P.option 10 $ fst <$> natural

1597 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1596 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1598 , noArgs ["implementation"] TCImplementation

1597 , noArgs ["implementation"] TCImplementation

1599 , noArgs ["solve"] Solve

1598 , noArgs ["solve"] Solve

@@ -1614,7 +1613,7 @@ tactics =

1614 , ([":doc"], Just ExprTArg, const $

1613 , ([":doc"], Just ExprTArg, const $

1615 do whiteSpace

1614 do whiteSpace

1616 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1615 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1617− eof

1616+ P.eof

1618 return (TDocStr doc))

1617 return (TDocStr doc))

1619 ]

1618 ]

1620 where

1619 where

@@ -1630,12 +1629,12 @@ tactics =

1630

1629

1631

1630

1632tactic :: SyntaxInfo -> IdrisParser PTactic

1631tactic :: SyntaxInfo -> IdrisParser PTactic

1633−tactic syn = choice [ do choice (map reserved names); parser syn

1632+tactic syn = P.choice [ do P.choice (map reserved names); parser syn

1634− | (names, _, parser) <- tactics ]

1633+ | (names, _, parser) <- tactics ]

1635 <|> do lchar '{'

1634 <|> do lchar '{'

1636 t <- tactic syn;

1635 t <- tactic syn;

1637 lchar ';';

1636 lchar ';';

1638− ts <- sepBy1 (tactic syn) (lchar ';')

1637+ ts <- P.sepBy1 (tactic syn) (lchar ';')

1639 lchar '}'

1638 lchar '}'

1640 return $ TSeq t (mergeSeq ts)

1639 return $ TSeq t (mergeSeq ts)

1641 <|> ((lchar ':' >> empty) <?> "prover command")

1640 <|> ((lchar ':' >> empty) <?> "prover command")

@@ -1648,5 +1647,5 @@ tactic syn = choice [ do choice (map reserved names); parser syn

1648-- | Parses a tactic as a whole

1647-- | Parses a tactic as a whole

1649fullTactic :: SyntaxInfo -> IdrisParser PTactic

1648fullTactic :: SyntaxInfo -> IdrisParser PTactic

1650fullTactic syn = do t <- tactic syn

1649fullTactic syn = do t <- tactic syn

1651− eof

1650+ P.eof

1652 return t

1651 return t

src/Idris/Parser/Helpers.hs+82−82

@@ -35,34 +35,34 @@ import qualified Text.Parser.Char as Chr

35import Text.Parser.LookAhead

36import qualified Text.Parser.Token as Tok

37import qualified Text.Parser.Token.Highlight as Hi

38−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

38+import Text.Trifecta ((<?>))

39− stringLiteral, symbol, whiteSpace)

39+import qualified Text.Trifecta as P

40−import Text.Trifecta.Delta

40+import qualified Text.Trifecta.Delta as P

42-- | Idris parser with state used during parsing

43type IdrisParser = StateT IState IdrisInnerParser

45−newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

45+newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: P.Parser a }

46− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

46+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, P.CharParsing, LookAheadParsing, P.DeltaParsing, P.MarkParsing P.Delta, Monoid, P.TokenParsing)

48−deriving instance Parsing IdrisInnerParser

48+deriving instance P.Parsing IdrisInnerParser

50#if MIN_VERSION_base(4,9,0)

51−instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where

51+instance {-# OVERLAPPING #-} P.DeltaParsing IdrisParser where

52− line = lift line

52+ line = lift P.line

53 {-# INLINE line #-}

54− position = lift position

54+ position = lift P.position

55 {-# 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

57 {-# INLINE slicedWith #-}

58− rend = lift rend

58+ rend = lift P.rend

59 {-# INLINE rend #-}

60− restOfLine = lift restOfLine

60+ restOfLine = lift P.restOfLine

61 {-# INLINE restOfLine #-}

63#endif

65−instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

65+instance {-# OVERLAPPING #-} P.TokenParsing IdrisParser where

66 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

67 token p = do s <- get

68 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

@@ -73,7 +73,7 @@ instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

73 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

74 return r

75-- | 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)

78class HasLastTokenSpan m where

79 getLastTokenSpan :: m (Maybe FC)

@@ -82,10 +82,10 @@ instance HasLastTokenSpan IdrisParser where

82 getLastTokenSpan = lastTokenSpan <$> get

84-- | 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

86runparser p i inputname =

87− parseString (runInnerParser (evalStateT p i))

87+ P.parseString (runInnerParser (evalStateT p i))

88− (Directed (UTF8.fromString inputname) 0 0 0 0)

88+ (P.Directed (UTF8.fromString inputname) 0 0 0 0)

90highlightP :: FC -> OutputAnnotation -> IdrisParser ()

91highlightP fc annot = do ist <- get

@@ -125,7 +125,7 @@ parserWarning fc warnOpt warnErr = do

125

126-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

127simpleWhiteSpace :: MonadicParsing m => m ()

128−simpleWhiteSpace = satisfy isSpace *> pure ()

128+simpleWhiteSpace = () <$ P.satisfy isSpace

129

130-- | Checks if a charcter is end of line

131isEol :: Char -> Bool

@@ -134,7 +134,7 @@ isEol _ = False

134

135-- | A parser that succeeds at the end of the line

136eol :: MonadicParsing m => m ()

137−eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

137+eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"

138

139{- | Consumes a single-line comment

140

@@ -144,7 +144,7 @@ eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

144 -}

145singleLineComment :: MonadicParsing m => m ()

146singleLineComment = (string "--" *>

147− many (satisfy (not . isEol)) *>

147+ many (P.satisfy (not . isEol)) *>

148 eol *> pure ())

149 <?> ""

150

@@ -166,15 +166,15 @@ singleLineComment = (string "--" *>

166@

167-}

168multiLineComment :: MonadicParsing m => m ()

169−multiLineComment = try (string "{-" *> (string "-}") *> pure ())

169+multiLineComment = P.try (string "{-" *> (string "-}") *> pure ())

170 <|> string "{-" *> inCommentChars

171 <?> ""

172 where inCommentChars :: MonadicParsing m => m ()

173 inCommentChars = string "-}" *> pure ()

174− <|> try (multiLineComment) *> inCommentChars

174+ <|> P.try (multiLineComment) *> inCommentChars

175− <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

175+ <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars

176− <|> skipSome (noneOf startEnd) *> inCommentChars

176+ <|> P.skipSome (P.noneOf startEnd) *> inCommentChars

177− <|> oneOf startEnd *> inCommentChars

177+ <|> P.oneOf startEnd *> inCommentChars

178 <?> "end of comment"

179 startEnd :: String

180 startEnd = "{}-"

@@ -197,23 +197,23 @@ docComment = do dc <- pushIndent *> docCommentLine

197 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

198

199 where docCommentLine :: MonadicParsing m => m String

200− docCommentLine = try (do string "|||"

200+ docCommentLine = P.try (do string "|||"

201− many (satisfy (==' '))

201+ many (P.satisfy (==' '))

202− contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

202+ contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))

203− res <- many (satisfy (not . isEol))

203+ res <- many (P.satisfy (not . isEol))

204− return $ first:res)

204+ return $ first:res)

205− eol ; someSpace

205+ eol ; P.someSpace

206− return contents)-- ++ concat rest))

206+ return contents)

207 <?> ""

208

209 argDocCommentLine = do string "|||"

210− many (satisfy isSpace)

210+ many (P.satisfy isSpace)

211 char '@'

212− many (satisfy isSpace)

212+ many (P.satisfy isSpace)

213 n <- fst <$> name

214− many (satisfy isSpace)

214+ many (P.satisfy isSpace)

215− docs <- many (satisfy (not . isEol))

215+ docs <- many (P.satisfy (not . isEol))

216− eol ; someSpace

216+ eol ; P.someSpace

217 return (n, docs)

218

219-- | Parses some white space

@@ -252,12 +252,12 @@ float = do f <- Tok.double

252

253

254-- | Idris Style for parsing identifiers/reserved keywords

255−idrisStyle :: MonadicParsing m => IdentifierStyle m

255+idrisStyle :: MonadicParsing m => P.IdentifierStyle m

256−idrisStyle = IdentifierStyle {

256+idrisStyle = P.IdentifierStyle {

257− _styleName = "Idris"

257+ P._styleName = "Idris"

258− , _styleStart = satisfy isAlpha <|> oneOf "_"

258+ , P._styleStart = P.satisfy isAlpha <|> P.oneOf "_"

259− , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

259+ , P._styleLetter = P.satisfy isAlphaNum <|> P.oneOf "_'."

260− , _styleReserved = HS.fromList

260+ , P._styleReserved = HS.fromList

261 ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",

262 "import", "impossible", "case", "of", "total", "partial", "mutual",

263 "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",

@@ -265,8 +265,8 @@ idrisStyle = IdentifierStyle {

265 "interface", "implementation", "parameters", "public", "private",

266 "export", "abstract", "implicit", "quoteGoal", "constructor", "if",

267 "then", "else"]

268− , _styleHighlight = Hi.Identifier

268+ , P._styleHighlight = Hi.Identifier

269− , _styleReservedHighlight = Hi.ReservedIdentifier }

269+ , P._styleReservedHighlight = Hi.ReservedIdentifier }

270

271char :: MonadicParsing m => Char -> m Char

272char = Chr.char

@@ -276,12 +276,12 @@ string = Chr.string

276

277-- | Parses a character as a token

278lchar :: MonadicParsing m => Char -> m Char

279−lchar = token . char

279+lchar = P.token . P.char

280

281-- | Parses a character as a token, returning the source span of the character

282lcharFC :: MonadicParsing m => Char -> m FC

283lcharFC ch = do (FC file (l, c) _) <- getFC

284− _ <- token (char ch)

284+ _ <- P.token (char ch)

285 return $ FC file (l, c) (l, c+1)

286

287-- | Parses string as a token

@@ -311,9 +311,9 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

311-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

312-- | Parses a reserved operator

313reservedOp :: MonadicParsing m => String -> m ()

314−reservedOp name = token $ try $

314+reservedOp name = P.token $ P.try $

315 do string name

316− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

316+ P.notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

317

318reservedOpFC :: MonadicParsing m => String -> m FC

319reservedOpFC name = do (FC f (l, c) _) <- getFC

@@ -322,12 +322,12 @@ reservedOpFC name = do (FC f (l, c) _) <- getFC

322

323-- | Parses an identifier as a token

324identifier :: (MonadicParsing m) => m (String, FC)

325−identifier = try(do (i, fc) <-

325+identifier = P.try(do (i, fc) <-

326− token $ do (FC f (l, c) _) <- getFC

326+ P.token $ do (FC f (l, c) _) <- getFC

327− i <- Tok.ident idrisStyle

327+ i <- Tok.ident idrisStyle

328− return (i, FC f (l, c) (l, c + length i))

328+ return (i, FC f (l, c) (l, c + length i))

329− when (i == "_") $ unexpected "wildcard"

329+ when (i == "_") $ P.unexpected "wildcard"

330− return (i, fc))

330+ return (i, fc))

331

332-- | Parses an identifier with possible namespace as a name

333iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

@@ -339,10 +339,10 @@ iName bad = do (n, fc) <- maybeWithNS identifier False bad

339maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

340maybeWithNS parser ascend bad = do

341 fc <- getFC

342− i <- option "" (lookAhead (fst <$> identifier))

342+ i <- P.option "" (lookAhead (fst <$> identifier))

343− when (i `elem` bad) $ unexpected "reserved identifier"

343+ when (i `elem` bad) $ P.unexpected "reserved identifier"

344 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))

346 return (mkName (x, xs), fc)

347 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

348 parserNoNS parser = do startFC <- getFC

@@ -354,7 +354,7 @@ maybeWithNS parser ascend bad = do

354 lchar '.'; (x, nameFC) <- parser

355 return (x, xs, spanFC startFC nameFC)

356 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)]

358

359-- | Parses a name

360name :: IdrisParser (Name, FC)

@@ -393,11 +393,11 @@ opChars :: String

393opChars = ":!#$%&*+./<=>?@\\^|-~"

394

395operatorLetter :: MonadicParsing m => m Char

396−operatorLetter = oneOf opChars

396+operatorLetter = P.oneOf opChars

397

398-- | Parse a package name

399packageName :: MonadicParsing m => m String

400−packageName = (:) <$> oneOf firstChars <*> many (oneOf remChars)

400+packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)

401 where firstChars = ['a'..'z'] ++ ['A'..'Z']

402 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

403

@@ -409,7 +409,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%

409

410-- | Parses an operator

411symbolicOperator :: MonadicParsing m => m String

412−symbolicOperator = do op <- token . some $ operatorLetter

412+symbolicOperator = do op <- P.token . some $ operatorLetter

413 when (op `elem` (invalidOperators ++ commentMarkers)) $

414 fail $ op ++ " is not a valid operator"

415 return op

@@ -422,24 +422,24 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC

422

423{- * Position helpers -}

424{- | Get filename from position (returns "(interactive)" when no source file is given) -}

425−fileName :: Delta -> String

425+fileName :: P.Delta -> String

426−fileName (Directed fn _ _ _ _) = UTF8.toString fn

426+fileName (P.Directed fn _ _ _ _) = UTF8.toString fn

427−fileName _ = "(interactive)"

427+fileName _ = "(interactive)"

428

429{- | Get line number from position -}

430−lineNum :: Delta -> Int

430+lineNum :: P.Delta -> Int

431−lineNum (Lines l _ _ _) = fromIntegral l + 1

431+lineNum (P.Lines l _ _ _) = fromIntegral l + 1

432−lineNum (Directed _ l _ _ _) = fromIntegral l + 1

432+lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1

433lineNum _ = 0

434

435{- | Get column number from position -}

436−columnNum :: Delta -> Int

436+columnNum :: P.Delta -> Int

437−columnNum pos = fromIntegral (column pos) + 1

437+columnNum pos = fromIntegral (P.column pos) + 1

438

439

440{- | Get file position as FC -}

441getFC :: MonadicParsing m => m FC

442−getFC = do s <- position

442+getFC = do s <- P.position

443 let (dir, file) = splitFileName (fileName s)

444 let f = if dir == addTrailingPathSeparator "." then file else fileName s

445 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)

456{- | @commaSeparated p@ parses one or more occurences of `p`,

457 separated by commas and optional whitespace. -}

458commaSeparated :: 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)

460

461{- * Layout helpers -}

462

463-- | Push indentation to stack

464pushIndent :: IdrisParser ()

465−pushIndent = do pos <- position

465+pushIndent = do pos <- P.position

466 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 })

468

469-- | Pops indentation from stack

470popIndent :: IdrisParser ()

@@ -476,7 +476,7 @@ popIndent = do ist <- get

476

477-- | Gets current indentation

478indent :: IdrisParser Int

479−indent = liftM ((+1) . fromIntegral . column) position

479+indent = liftM ((+1) . fromIntegral . P.column) P.position

480

481-- | Gets last indentation

482lastIndent :: IdrisParser Int

@@ -544,7 +544,7 @@ openBlock = do lchar '{'

544closeBlock :: IdrisParser ()

545closeBlock = do ist <- get

546 bs <- case brace_stack ist of

547− [] -> eof >> return []

547+ [] -> [] <$ P.eof

548 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

549 Just lvl : xs -> (do i <- indent

550 isParen <- lookAheadMatches (char ')')

@@ -553,7 +553,7 @@ closeBlock = do ist <- get

553 then fail "not end of block"

554 else return xs)

555 <|> (do notOpenBraces

556− eof

556+ P.eof

557 return [])

558 put (ist { brace_stack = bs })

559

@@ -562,19 +562,19 @@ terminator :: IdrisParser ()

562terminator = do lchar ';'; popIndent

563 <|> do c <- indent; l <- lastIndent

564 if c <= l then popIndent else fail "not a terminator"

565− <|> do isParen <- lookAheadMatches (oneOf ")}")

565+ <|> do isParen <- lookAheadMatches (P.oneOf ")}")

566 if isParen then popIndent else fail "not a terminator"

567− <|> lookAhead eof

567+ <|> lookAhead P.eof

568

569-- | Parses and keeps a terminator

570keepTerminator :: IdrisParser ()

571−keepTerminator = do lchar ';'; return ()

571+keepTerminator = () <$ lchar ';'

572 <|> do c <- indent; l <- lastIndent

573 unless (c <= l) $ fail "not a terminator"

574− <|> do isParen <- lookAheadMatches (oneOf ")}|")

574+ <|> do isParen <- lookAheadMatches (P.oneOf ")}|")

575 isIn <- lookAheadMatches (reserved "in")

576 unless (isIn || isParen) $ fail "not a terminator"

577− <|> lookAhead eof

577+ <|> lookAhead P.eof

578

579-- | Checks if application expression does not end

580notEndApp :: IdrisParser ()

src/Idris/Parser/Ops.hs+11−11

@@ -22,8 +22,8 @@ import Control.Monad.State.Strict

22import Data.Char (isAlpha)

23import Data.List

24import Text.Parser.Expression

25−import Text.Trifecta hiding (char, charLiteral, natural, span, string,

25+import Text.Trifecta ((<?>))

26− stringLiteral, symbol, whiteSpace)

26+import qualified Text.Trifecta as P

28-- | Creates table for fixity declarations to build expression parser

29-- using pre-build and user-defined operator/fixity declarations

@@ -49,8 +49,8 @@ table fixes

49 noFixityOperator :: Operator IdrisParser PTerm

50 noFixityOperator = flip Infix AssocNone $ do

51 indentGt

52− op <- try symbolicOperator

52+ op <- P.try symbolicOperator

53− unexpected $ "Operator without known fixity: " ++ op

53+ P.unexpected $ "Operator without known fixity: " ++ op

55 -- | Calculates table for fixity declarations

56 toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

@@ -71,7 +71,7 @@ table fixes

72 binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm

73 binary name assoc f

74− | isBacktick name = flip Infix assoc $ try $ do

74+ | isBacktick name = flip Infix assoc $ P.try $ do

75 (n, fc) <- backtickOperator

76 guard $ show (nsroot n) == name

77 return $ f fc n

@@ -96,7 +96,7 @@ table fixes

96@

97-}

98backtickOperator :: IdrisParser (Name, FC)

99−backtickOperator = between (indentGt *> lchar '`') (indentGt *> lchar '`') name

99+backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name

100

101{- | Parses an operator name (either a symbolic name or a backtick-quoted name)

102

@@ -123,9 +123,9 @@ operatorName = first sUN <$> symbolicOperatorFC

123

124-}

125operatorFront :: IdrisParser (Name, FC)

126−operatorFront = try (do (FC f (l, c) _) <- getFC

126+operatorFront = P.try (do (FC f (l, c) _) <- getFC

127− op <- lchar '(' *> reservedOp "=" <* lchar ')'

127+ op <- lchar '(' *> reservedOp "=" <* lchar ')'

128− return (eqTy, FC f (l, c) (l, c+3)))

128+ return (eqTy, FC f (l, c) (l, c+3)))

129 <|> maybeWithNS (do (FC f (l, c) _) <- getFC

130 op <- lchar '(' *> symbolicOperator

131 (FC _ _ (l', c')) <- getFC

@@ -139,7 +139,7 @@ operatorFront = try (do (FC f (l, c) _) <- getFC

139@

140-}

141fnName :: IdrisParser (Name, FC)

142−fnName = try operatorFront <|> name <?> "function name"

142+fnName = P.try operatorFront <|> name <?> "function name"

143

144{- | Parses a fixity declaration

145@

@@ -151,7 +151,7 @@ Fixity ::=

151fixity :: IdrisParser PDecl

152fixity = do pushIndent

153 f <- fixityType; i <- fst <$> natural;

154− ops <- sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

154+ ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

155 terminator

156 let prec = fromInteger i

157 istate <- get

src/Idris/Prover.hs+23−23

@@ -43,7 +43,7 @@ import Control.Monad.State.Strict

43import System.Console.Haskeline

44import System.Console.Haskeline.History

45import System.IO (Handle, hPutStrLn, stdin, stdout)

46−import Text.Trifecta.Result (ErrInfo(..), Result(..))

46+import qualified Text.Trifecta.Result as P

48-- | Launch the proof shell

49prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

@@ -312,15 +312,15 @@ elabloop info fn d prompt prf e prev h env

312

313 -- if we're abandoning, it has to be outside the scope of the catch

314 case cmd of

315− Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

315+ P.Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

316 _ -> return ()

317

318 (d, prev', st, done, prf', env', res) <-

319 idrisCatch

320 (case cmd of

321− Failure (ErrInfo err _) ->

321+ P.Failure (P.ErrInfo err _) ->

322 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

323− Success (Left cmd') ->

323+ P.Success (Left cmd') ->

324 case cmd' of

325 EQED -> do hs <- lifte e get_holes

326 unless (null hs) $ ifail "Incomplete proof"

@@ -345,7 +345,7 @@ elabloop info fn d prompt prf e prev h env

345 return (d', prev, st', done, prf', env, go)

346 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

347 return (d', prev, st', done, prf', env, go)

348− Success (Right cmd') ->

348+ P.Success (Right cmd') ->

349 case cmd' of

350 DoLetP {} -> ifail "Pattern-matching let not supported here"

351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

@@ -430,27 +430,27 @@ ploop fn d prompt prf e h

430 Nothing -> do iPrintError ""; ifail "Abandoned"

431 Just input -> return (parseTactic i input, input)

432 case cmd of

433− Success Abandon -> do iPrintError ""; ifail "Abandoned"

433+ P.Success Abandon -> do iPrintError ""; ifail "Abandoned"

434 _ -> return ()

435 (d, st, done, prf', res) <- idrisCatch

436 (case cmd of

437− Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

437+ P.Failure (P.ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

438− Success Undo -> do (_, st) <- elabStep e loadState

438+ P.Success Undo -> do (_, st) <- elabStep e loadState

439− return (True, st, False, init prf, Right $ iPrintResult "")

439+ return (True, st, False, init prf, Right $ iPrintResult "")

440− Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

440+ P.Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

441− Success ProofTerm -> do tm <- lifte e get_term

441+ P.Success ProofTerm -> do tm <- lifte e get_term

442− iputStrLn $ "TT: " ++ show tm ++ "\n"

442+ iputStrLn $ "TT: " ++ show tm ++ "\n"

443− return (False, e, False, prf, Right $ iPrintResult "")

443+ return (False, e, False, prf, Right $ iPrintResult "")

444− Success Qed -> do hs <- lifte e get_holes

444+ P.Success Qed -> do hs <- lifte e get_holes

445− unless (null hs) $ ifail "Incomplete proof"

445+ unless (null hs) $ ifail "Incomplete proof"

446− iputStrLn "Proof completed!"

446+ iputStrLn "Proof completed!"

447− return (False, e, True, prf, Right $ iPrintResult "")

447+ return (False, e, True, prf, Right $ iPrintResult "")

448− Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

448+ P.Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

449− Success (TCheck t) -> checkType e prf t

449+ P.Success (TCheck t) -> checkType e prf t

450− Success (TEval t) -> evalTerm e prf t

450+ P.Success (TEval t) -> evalTerm e prf t

451− Success (TDocStr x) -> docStr e prf x

451+ P.Success (TDocStr x) -> docStr e prf x

452− Success (TSearch t) -> search e prf t

452+ P.Success (TSearch t) -> search e prf t

453− Success tac ->

453+ P.Success tac ->

454 do (_, e) <- elabStep e saveState

455 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

456 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

src/Idris/REPL.hs+22−25

@@ -93,7 +93,7 @@ import System.FSNotify (watchDir, withManager)

93import System.FSNotify.Devel (allEvents, doAllEvents)

94import System.IO

95import System.Process

96−import Text.Trifecta.Result (ErrInfo(..), Result(..))

96+import qualified Text.Trifecta.Result as P

97import Util.DynamicLinker

98import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

99import Util.Pretty hiding ((</>))

@@ -177,9 +177,9 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

177 IO (IState, FilePath)

178processNetCmd orig i h fn cmd

179 = do res <- case parseCmd i "(net)" cmd of

180− Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))

180+ P.Failure (P.ErrInfo err _) -> return (Left (Msg " invalid command"))

181− Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

181+ P.Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

182− Success (Left err) -> return (Left (Msg err))

182+ P.Success (Left err) -> return (Left (Msg err))

183 case res of

184 Right x -> return x

185 Left err -> do hPutStrLn h (show err)

@@ -295,8 +295,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

295 do c <- colourise

296 i <- getIState

297 case parseCmd i "(input)" cmd of

298− Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)

298+ P.Failure (P.ErrInfo err _) -> iPrintError $ show (fixColour False err)

299− Success (Right (Prove mode n')) ->

299+ P.Success (Right (Prove mode n')) ->

300 idrisCatch

301 (do process fn (Prove mode n')

302 isetPrompt (mkPrompt mods)

@@ -315,10 +315,10 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

315 IdeMode.convSExp "abandon-proof" "Abandoned" n

316 _ -> return ()

317 iRenderError $ pprintErr ist e)

318− Success (Right cmd) -> idrisCatch

318+ P.Success (Right cmd) -> idrisCatch

319 (idemodeProcess fn cmd)

320 (\e -> getIState >>= iRenderError . flip pprintErr e)

321− Success (Left err) -> iPrintError err

321+ P.Success (Left err) -> iPrintError err

322runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

323 do (unused, compls) <- replCompletion (reverse str, "")

324 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

@@ -353,8 +353,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

353 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

354runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

355 case parseConst orig name of

356− Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

356+ P.Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

357− Failure _ ->

357+ P.Failure _ ->

358 case splitName name of

359 Left err -> iPrintError err

360 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

@@ -727,11 +727,10 @@ processInput cmd orig inputs efile

727 let fn = fromMaybe "" (listToMaybe inputs)

728 c <- colourise

729 case parseCmd i "(input)" cmd of

730− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

730+ P.Failure (P.ErrInfo err _) -> Just inputs <$ iputStrLn (show (fixColour c err))

731− return (Just inputs)

732− Success (Right Reload) ->

731+ P.Success (Right Reload) ->

733 reload orig inputs

732 reload orig inputs

734− Success (Right Watch) ->

733+ P.Success (Right Watch) ->

735 if null inputs then

734 if null inputs then

736 do iputStrLn "No loaded files to watch."

735 do iputStrLn "No loaded files to watch."

737 return (Just inputs)

736 return (Just inputs)

@@ -739,7 +738,7 @@ processInput cmd orig inputs efile

739 do iputStrLn efile

738 do iputStrLn efile

740 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

739 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

741 watch orig inputs

740 watch orig inputs

742− Success (Right (Load f toline)) ->

741+ P.Success (Right (Load f toline)) ->

743 -- The $!! here prevents a space leak on reloading.

742 -- The $!! here prevents a space leak on reloading.

744 -- This isn't a solution - but it's a temporary stopgap.

743 -- This isn't a solution - but it's a temporary stopgap.

745 -- See issue #2386

744 -- See issue #2386

@@ -749,22 +748,20 @@ processInput cmd orig inputs efile

749 clearErr

748 clearErr

750 mod <- loadInputs [f] toline

749 mod <- loadInputs [f] toline

751 return (Just mod)

750 return (Just mod)

752− Success (Right (ModImport f)) ->

751+ P.Success (Right (ModImport f)) ->

753 do clearErr

752 do clearErr

754 fmod <- loadModule f (IBC_REPL True)

753 fmod <- loadModule f (IBC_REPL True)

755 return (Just (inputs ++ maybe [] (:[]) fmod))

754 return (Just (inputs ++ maybe [] (:[]) fmod))

756− Success (Right Edit) -> do -- takeMVar stvar

755+ P.Success (Right Edit) -> do -- takeMVar stvar

757 edit efile orig

756 edit efile orig

758 return (Just inputs)

757 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)

760 return (Just inputs)

762 return (Just inputs)

761− Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")

763+ P.Success (Left err) -> do runIO $ putStrLn err

762− return Nothing

763− Success (Right cmd ) -> do idrisCatch (process fn cmd)

764− (\e -> do msg <- showErr e ; iputStrLn msg)

765 return (Just inputs)

764 return (Just inputs)

766− Success (Left err) -> do runIO $ putStrLn err

767− return (Just inputs)

768

765

769resolveProof :: Name -> Idris Name

766resolveProof :: Name -> Idris Name

770resolveProof n'

767resolveProof n'

@@ -1429,7 +1426,7 @@ process fn (Browse ns) =

1429process fn (MakeDoc s) =

1426process fn (MakeDoc s) =

1430 do istate <- getIState

1427 do istate <- getIState

1431 let names = words s

1428 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

1433 parse n = Left n

1430 parse n = Left n

1434 (bad, nss) = partitionEithers $ map parse names

1431 (bad, nss) = partitionEithers $ map parse names

1435 cd <- runIO getCurrentDirectory

1432 cd <- runIO getCurrentDirectory

src/Idris/REPL/Parser.hs+125−125

@@ -17,10 +17,10 @@ import Idris.Core.TT

17import Idris.Help

18import Idris.Imports

19import Idris.Options

20−import qualified Idris.Parser as P

20+import qualified Idris.Parser as IP

21−import qualified Idris.Parser.Expr as P

21+import qualified Idris.Parser.Expr as IP

22−import qualified Idris.Parser.Helpers as P

22+import qualified Idris.Parser.Helpers as IP

23−import qualified Idris.Parser.Ops as P

23+import qualified Idris.Parser.Ops as IP

25import Idris.REPL.Commands

@@ -33,15 +33,15 @@ import System.Console.ANSI (Color(..))

33import System.FilePath ((</>))

34import Text.Parser.Char (anyChar, oneOf)

35import Text.Parser.Combinators

36−import Text.Trifecta (Result)

36+import qualified Text.Trifecta as P

38−parseCmd :: IState -> String -> String -> Result (Either String Command)

38+parseCmd :: IState -> String -> String -> P.Result (Either String Command)

39−parseCmd i inputname = P.runparser pCmd i inputname . trim

39+parseCmd i inputname = IP.runparser pCmd i inputname . trim

40 where trim = f . f

41 where f = reverse . dropWhile isSpace

43type CommandTable = [ ( [String], CmdArg, String

44− , String -> P.IdrisParser (Either String Command) ) ]

44+ , String -> IP.IdrisParser (Either String Command) ) ]

46setOptions :: [(String, Opt)]

47setOptions = [("errorcontext", ErrContext),

@@ -168,8 +168,8 @@ parserCommands =

168 , cmd_refine)

169 , (["debugunify"], SeqArgs ExprArg ExprArg

170 , "(Debugging) Try to unify two expressions", const $ do

171− l <- P.simpleExpr defaultSyntax

171+ l <- IP.simpleExpr defaultSyntax

172− r <- P.simpleExpr defaultSyntax

172+ r <- IP.simpleExpr defaultSyntax

173 eof

174 return (Right (DebugUnify l r))

175 )

@@ -188,7 +188,7 @@ optArgCmd names command doc =

188proofArgCmd names command doc =

189 (names, NoArg, doc, proofArg command)

190

191−pCmd :: P.IdrisParser (Either String Command)

191+pCmd :: IP.IdrisParser (Either String Command)

192pCmd = choice [ do c <- cmd names; parser c

193 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

194 <|> unrecognized

@@ -196,23 +196,23 @@ pCmd = choice [ do c <- cmd names; parser c

196 <|> eval

197 where nop = do eof; return (Right NOP)

198 unrecognized = do

199− P.lchar ':'

199+ IP.lchar ':'

200 cmd <- many anyChar

201 let cmd' = takeWhile (/=' ') cmd

202 return (Left $ "Unrecognized command: " ++ cmd')

203

204−cmd :: [String] -> P.IdrisParser String

204+cmd :: [String] -> IP.IdrisParser String

205cmd xs = try $ do

206− P.lchar ':'

206+ IP.lchar ':'

207 docmd sorted_xs

208

209 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

211

212 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

213

214

215−noArgs :: Command -> String -> P.IdrisParser (Either String Command)

215+noArgs :: Command -> String -> IP.IdrisParser (Either String Command)

216noArgs cmd name = do

217 let emptyArgs = do

218 eof

@@ -222,29 +222,29 @@ noArgs cmd name = do

222

223 emptyArgs <|> failure

224

225−eval :: P.IdrisParser (Either String Command)

225+eval :: IP.IdrisParser (Either String Command)

226eval = do

227− t <- P.fullExpr defaultSyntax

227+ t <- IP.fullExpr defaultSyntax

228 return $ Right (Eval t)

229

230−exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

230+exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)

231exprArg cmd name = do

232 let noArg = do

233 eof

234 return $ Left ("Usage is :" ++ name ++ " <expression>")

235

236 let justOperator = do

237− (op, fc) <- P.symbolicOperatorFC

237+ (op, fc) <- IP.symbolicOperatorFC

238 eof

239 return $ Right $ cmd (PRef fc [] (sUN op))

240

241 let properArg = do

242− t <- P.fullExpr defaultSyntax

242+ t <- IP.fullExpr defaultSyntax

243 return $ Right (cmd t)

244 try noArg <|> try justOperator <|> properArg

245

246−genArg :: String -> P.IdrisParser a -> (a -> Command)

246+genArg :: String -> IP.IdrisParser a -> (a -> Command)

247− -> String -> P.IdrisParser (Either String Command)

247+ -> String -> IP.IdrisParser (Either String Command)

248genArg argName argParser cmd name = do

249 let emptyArgs = do eof; failure

250 oneArg = do arg <- argParser

@@ -254,24 +254,24 @@ genArg argName argParser cmd name = do

254 where

255 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

256

257−nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

257+nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)

258−nameArg = genArg "name" $ fst <$> P.name

258+nameArg = genArg "name" $ fst <$> IP.name

259−fnNameArg = genArg "functionname" $ fst <$> P.fnName

259+fnNameArg = genArg "functionname" $ fst <$> IP.fnName

260

261−strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

261+strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

262strArg = genArg "string" (many anyChar)

263

264−moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

264+moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

265−moduleArg = genArg "module" (fmap (toPath . fst) P.identifier)

265+moduleArg = genArg "module" (fmap (toPath . fst) IP.identifier)

266 where

267 toPath n = foldl1' (</>) $ splitOn "." n

268

269−namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

269+namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)

270−namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

270+namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)

271 where

272 toNS = splitOn "."

273

274−optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

274+optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)

275optArg cmd name = do

276 let emptyArgs = do

277 eof

@@ -279,7 +279,7 @@ optArg cmd name = do

279

280 let oneArg = do

281 o <- pOption

282− P.whiteSpace

282+ IP.whiteSpace

283 eof

284 return (Right (cmd o))

285

@@ -288,58 +288,58 @@ optArg cmd name = do

288 try emptyArgs <|> oneArg <|> failure

289

290 where

291− pOption :: P.IdrisParser Opt

291+ pOption :: IP.IdrisParser Opt

292− pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

292+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (IP.symbol a); return b) setOptions

293

294−proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

294+proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)

295proofArg cmd name = do

296 upd <- option False $ do

297− P.lchar '!'

297+ IP.lchar '!'

298 return True

299− l <- fst <$> P.natural

299+ l <- fst <$> IP.natural

300− n <- fst <$> P.name;

300+ n <- fst <$> IP.name;

301 return (Right (cmd upd (fromInteger l) n))

302

303−cmd_doc :: String -> P.IdrisParser (Either String Command)

303+cmd_doc :: String -> IP.IdrisParser (Either String Command)

304cmd_doc name = do

305 let constant = do

306− c <- fmap fst P.constant

306+ c <- fmap fst IP.constant

307 eof

308 return $ Right (DocStr (Right c) FullDocs)

309

310 let pType = do

311− P.reserved "Type"

311+ IP.reserved "Type"

312 eof

313− return $ Right (DocStr (Left $ P.mkName ("Type", "")) FullDocs)

313+ return $ Right (DocStr (Left $ IP.mkName ("Type", "")) FullDocs)

314

315 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

316

317 try constant <|> pType <|> fnName

318

319−cmd_consolewidth :: String -> P.IdrisParser (Either String Command)

319+cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)

320cmd_consolewidth name = do

321 w <- pConsoleWidth

322 return (Right (SetConsoleWidth w))

323

324 where

325− pConsoleWidth :: P.IdrisParser ConsoleWidth

325+ pConsoleWidth :: IP.IdrisParser ConsoleWidth

326− pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

326+ pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth

327− <|> do discard (P.symbol "infinite"); return InfinitelyWide

327+ <|> do discard (IP.symbol "infinite"); return InfinitelyWide

328− <|> do n <- fmap (fromInteger . fst) P.natural

328+ <|> do n <- fmap (fromInteger . fst) IP.natural

329 return (ColsWide n)

330

331−cmd_printdepth :: String -> P.IdrisParser (Either String Command)

331+cmd_printdepth :: String -> IP.IdrisParser (Either String Command)

332−cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) P.natural)

332+cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)

333 return (Right $ SetPrinterDepth d)

334

335−cmd_execute :: String -> P.IdrisParser (Either String Command)

335+cmd_execute :: String -> IP.IdrisParser (Either String Command)

336cmd_execute name = do

337− tm <- option maintm (P.fullExpr defaultSyntax)

337+ tm <- option maintm (IP.fullExpr defaultSyntax)

338 return (Right (Execute tm))

339 where

340 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

341

342−cmd_dynamic :: String -> P.IdrisParser (Either String Command)

342+cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

343cmd_dynamic name = do

344 let optArg = do l <- many anyChar

345 if (l /= "")

@@ -348,101 +348,101 @@ cmd_dynamic name = do

348 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

349 try optArg <|> failure

350

351−cmd_pprint :: String -> P.IdrisParser (Either String Command)

351+cmd_pprint :: String -> IP.IdrisParser (Either String Command)

352cmd_pprint name = do

353 fmt <- ppFormat

354− P.whiteSpace

354+ IP.whiteSpace

355− n <- fmap (fromInteger . fst) P.natural

355+ n <- fmap (fromInteger . fst) IP.natural

356− P.whiteSpace

356+ IP.whiteSpace

357− t <- P.fullExpr defaultSyntax

357+ t <- IP.fullExpr defaultSyntax

358 return (Right (PPrint fmt n t))

359

360 where

361− ppFormat :: P.IdrisParser OutputFmt

361+ ppFormat :: IP.IdrisParser OutputFmt

362− ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

362+ ppFormat = (discard (IP.symbol "html") >> return HTMLOutput)

363− <|> (discard (P.symbol "latex") >> return LaTeXOutput)

363+ <|> (discard (IP.symbol "latex") >> return LaTeXOutput)

364

365−cmd_compile :: String -> P.IdrisParser (Either String Command)

365+cmd_compile :: String -> IP.IdrisParser (Either String Command)

366cmd_compile name = do

367 let defaultCodegen = Via IBCFormat "c"

368

369− let codegenOption :: P.IdrisParser Codegen

369+ let codegenOption :: IP.IdrisParser Codegen

370 codegenOption = do

371− let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode

371+ let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode

372− viaCodegen = do x <- fst <$> P.identifier

372+ viaCodegen = do x <- fst <$> IP.identifier

373 return (Via IBCFormat (map toLower x))

374 bytecodeCodegen <|> viaCodegen

375

376 let hasOneArg = do

377 i <- get

378− f <- fst <$> P.identifier

378+ f <- fst <$> IP.identifier

379 eof

380 return $ Right (Compile defaultCodegen f)

381

382 let hasTwoArgs = do

383 i <- get

384 codegen <- codegenOption

385− f <- fst <$> P.identifier

385+ f <- fst <$> IP.identifier

386 eof

387 return $ Right (Compile codegen f)

388

389 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

390 try hasTwoArgs <|> try hasOneArg <|> failure

391

392−cmd_addproof :: String -> P.IdrisParser (Either String Command)

392+cmd_addproof :: String -> IP.IdrisParser (Either String Command)

393cmd_addproof name = do

394 n <- option Nothing $ do

395− x <- fst <$> P.name

395+ x <- fst <$> IP.name

396 return (Just x)

397 eof

398 return (Right (AddProof n))

399

400−cmd_log :: String -> P.IdrisParser (Either String Command)

400+cmd_log :: String -> IP.IdrisParser (Either String Command)

401cmd_log name = do

402− i <- fmap (fromIntegral . fst) P.natural

402+ i <- fmap (fromIntegral . fst) IP.natural

403 eof

404 return (Right (LogLvl i))

405

406−cmd_verb :: String -> P.IdrisParser (Either String Command)

406+cmd_verb :: String -> IP.IdrisParser (Either String Command)

407cmd_verb name = do

408− i <- fmap (fromIntegral . fst) P.natural

408+ i <- fmap (fromIntegral . fst) IP.natural

409 eof

410 return (Right (Verbosity i))

411

412−cmd_cats :: String -> P.IdrisParser (Either String Command)

412+cmd_cats :: String -> IP.IdrisParser (Either String Command)

413cmd_cats name = do

414− cs <- sepBy pLogCats (P.whiteSpace)

414+ cs <- sepBy pLogCats (IP.whiteSpace)

415 eof

416 return $ Right $ LogCategory (concat cs)

417 where

418 badCat = do

419− c <- fst <$> P.identifier

419+ c <- fst <$> IP.identifier

420 fail $ "Category: " ++ c ++ " is not recognised."

421

422− pLogCats :: P.IdrisParser [LogCat]

422+ pLogCats :: IP.IdrisParser [LogCat]

423− pLogCats = try (P.symbol (strLogCat IParse) >> return parserCats)

423+ pLogCats = try (parserCats <$ IP.symbol (strLogCat IParse))

424− <|> try (P.symbol (strLogCat IElab) >> return elabCats)

424+ <|> try (elabCats <$ IP.symbol (strLogCat IElab))

425− <|> try (P.symbol (strLogCat ICodeGen) >> return codegenCats)

425+ <|> try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

426− <|> try (P.symbol (strLogCat ICoverage) >> return [ICoverage])

426+ <|> try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

427− <|> try (P.symbol (strLogCat IIBC) >> return [IIBC])

427+ <|> try ([IIBC] <$ IP.symbol (strLogCat IIBC))

428− <|> try (P.symbol (strLogCat IErasure) >> return [IErasure])

428+ <|> try ([IErasure] <$ IP.symbol (strLogCat IErasure))

429 <|> badCat

430

431−cmd_let :: String -> P.IdrisParser (Either String Command)

431+cmd_let :: String -> IP.IdrisParser (Either String Command)

432cmd_let name = do

433− defn <- concat <$> many (P.decl defaultSyntax)

433+ defn <- concat <$> many (IP.decl defaultSyntax)

434 return (Right (NewDefn defn))

435

436−cmd_unlet :: String -> P.IdrisParser (Either String Command)

436+cmd_unlet :: String -> IP.IdrisParser (Either String Command)

437−cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> P.name)

437+cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> IP.name)

438

439−cmd_loadto :: String -> P.IdrisParser (Either String Command)

439+cmd_loadto :: String -> IP.IdrisParser (Either String Command)

440cmd_loadto name = do

441− toline <- fmap (fromInteger . fst) P.natural

441+ toline <- fmap (fromInteger . fst) IP.natural

442 f <- many anyChar;

443 return (Right (Load f (Just toline)))

444

445−cmd_colour :: String -> P.IdrisParser (Either String Command)

445+cmd_colour :: String -> IP.IdrisParser (Either String Command)

446cmd_colour name = fmap Right pSetColourCmd

447

448 where

@@ -458,29 +458,29 @@ cmd_colour name = fmap Right pSetColourCmd

458 , ("default", Nothing)

459 ]

460

461− pSetColourCmd :: P.IdrisParser Command

461+ pSetColourCmd :: IP.IdrisParser Command

462 pSetColourCmd = (do c <- pColourType

463 let defaultColour = IdrisColour Nothing True False False False

464− opts <- sepBy pColourMod (P.whiteSpace)

464+ opts <- sepBy pColourMod (IP.whiteSpace)

465 let colour = foldr ($) defaultColour $ reverse opts

466 return $ SetColour c colour)

467− <|> try (P.symbol "on" >> return ColourOn)

467+ <|> try (IP.symbol "on" >> return ColourOn)

468− <|> try (P.symbol "off" >> return ColourOff)

468+ <|> try (IP.symbol "off" >> return ColourOff)

469

470− pColour :: P.IdrisParser (Maybe Color)

470+ pColour :: IP.IdrisParser (Maybe Color)

471 pColour = doColour colours

472 where doColour [] = fail "Unknown colour"

473− doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs

473+ doColour ((s, c):cs) = (try (IP.symbol s) >> return c) <|> doColour cs

474−

474+

475− pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)

475+ pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)

476− pColourMod = try (P.symbol "vivid" >> return doVivid)

476+ pColourMod = try (doVivid <$ IP.symbol "vivid")

477− <|> try (P.symbol "dull" >> return doDull)

477+ <|> try (doDull <$ IP.symbol "dull")

478− <|> try (P.symbol "underline" >> return doUnderline)

478+ <|> try (doUnderline <$ IP.symbol "underline")

479− <|> try (P.symbol "nounderline" >> return doNoUnderline)

479+ <|> try (doNoUnderline <$ IP.symbol "nounderline")

480− <|> try (P.symbol "bold" >> return doBold)

480+ <|> try (doBold <$ IP.symbol "bold")

481− <|> try (P.symbol "nobold" >> return doNoBold)

481+ <|> try (doNoBold <$ IP.symbol "nobold")

482− <|> try (P.symbol "italic" >> return doItalic)

482+ <|> try (doItalic <$ IP.symbol "italic")

483− <|> try (P.symbol "noitalic" >> return doNoItalic)

483+ <|> try (doNoItalic <$ IP.symbol "noitalic")

484 <|> try (pColour >>= return . doSetColour)

485 where doVivid i = i { vivid = True }

486 doDull i = i { vivid = False }

@@ -497,44 +497,44 @@ cmd_colour name = fmap Right pSetColourCmd

497 colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

498 enumFromTo minBound maxBound

499

500− pColourType :: P.IdrisParser ColourType

500+ pColourType :: IP.IdrisParser ColourType

501 pColourType = doColourType colourTypes

502 where doColourType [] = fail $ "Unknown colour category. Options: " ++

503 (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

505

506idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

507

508−cmd_apropos :: String -> P.IdrisParser (Either String Command)

508+cmd_apropos :: String -> IP.IdrisParser (Either String Command)

509cmd_apropos = packageBasedCmd (some idChar) Apropos

510

511−packageBasedCmd :: P.IdrisParser a -> ([PkgName] -> a -> Command)

511+packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)

512− -> String -> P.IdrisParser (Either String Command)

512+ -> String -> IP.IdrisParser (Either String Command)

513packageBasedCmd valParser cmd name =

514− try (do P.lchar '('

514+ try (do IP.lchar '('

515− pkgs <- sepBy (pkg <* P.whiteSpace) (P.lchar ',')

515+ pkgs <- sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

516− P.lchar ')'

516+ IP.lchar ')'

517 val <- valParser

518 return (Right (cmd pkgs val)))

519 <|> do val <- valParser

520 return (Right (cmd [] val))

521 where

522− pkg = either fail pure . pkgName =<< P.packageName

522+ pkg = either fail pure . pkgName =<< IP.packageName

523

524−cmd_search :: String -> P.IdrisParser (Either String Command)

524+cmd_search :: String -> IP.IdrisParser (Either String Command)

525cmd_search = packageBasedCmd

526− (P.fullExpr (defaultSyntax { implicitAllowed = True })) Search

526+ (IP.fullExpr (defaultSyntax { implicitAllowed = True })) Search

527

528−cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

528+cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)

529cmd_proofsearch name = do

530− upd <- option False (do P.lchar '!'; return True)

530+ upd <- option False (True <$ IP.lchar '!')

531− l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

531+ l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

532− hints <- many (fst <$> P.fnName)

532+ hints <- many (fst <$> IP.fnName)

533 return (Right (DoProofSearch upd True l n hints))

534

535−cmd_refine :: String -> P.IdrisParser (Either String Command)

535+cmd_refine :: String -> IP.IdrisParser (Either String Command)

536cmd_refine name = do

537− upd <- option False (do P.lchar '!'; return True)

537+ upd <- option False (do IP.lchar '!'; return True)

538− l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

538+ l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

539− hint <- fst <$> P.fnName

539+ hint <- fst <$> IP.fnName

540 return (Right (DoProofSearch upd False l n [hint]))