4ebafb4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Highlight names of simple variable references

commit4ebafb4b2cd7763b5bf35ec689eb037b9104f781 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 9 May 2015, 16:03 (11 years ago) parent604bde0

9 files changed+169−126

compare with master

unifiedsplit

src/Idris/Core/TT.hs+25 src/Idris/ParseData.hs+15−15 src/Idris/ParseExpr.hs+27−27 src/Idris/ParseHelpers.hs+28−18 src/Idris/ParseOps.hs+9−5 src/Idris/Parser.hs+38−37 src/Idris/REPL.hs+1−1 src/Idris/REPLParser.hs+15−15 src/Pkg/PParser.hs+11−8

src/Idris/Core/TT.hs+25

@@ -57,6 +57,31 @@ data FC = FC { fc_fname :: String, -- ^ Filename

5757 | FileFC { fc_fname :: String } -- ^ Locations with file only

5858 deriving (Data, Typeable, Ord)

5959

60+-- | Get the largest span containing the two FCs

61+spanFC :: FC -> FC -> FC

62+spanFC (FC f start end) (FC f' start' end')

63+ | f == f' = FC f (minLocation start start') (maxLocation end end')

64+ | otherwise = NoFC

65+ where minLocation (l, c) (l', c') =

66+ case compare l l' of

67+ LT -> (l, c)

68+ EQ -> (l, min c c')

69+ GT -> (l', c')

70+ maxLocation (l, c) (l', c') =

71+ case compare l l' of

72+ LT -> (l', c')

73+ EQ -> (l, max c c')

74+ GT -> (l, c)

75+spanFC fc@(FC f _ _) (FileFC f') | f == f' = fc

76+ | otherwise = NoFC

77+spanFC (FileFC f') fc@(FC f _ _) | f == f' = fc

78+ | otherwise = NoFC

79+spanFC (FileFC f) (FileFC f') | f == f' = FileFC f

80+ | otherwise = NoFC

81+spanFC NoFC fc = fc

82+spanFC fc NoFC = fc

83+

84+

6085-- | Ignore source location equality (so deriving classes do not compare FCs)

6186instance Eq FC where

6287 _ == _ = True

src/Idris/ParseData.hs+15−15

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

5353 co <- recordI

5454 return (doc', paramDocs', acc, opts ++ co))

5555 fc <- getFC

56− tyn_in <- fnName

56+ tyn_in <- fst <$> fnName

5757 let tyn = expandNS syn tyn_in

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

5959 syn_namespace syn }

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

8787 let constructorDoc' = annotate syn ist constructorDoc

8888

8989 fields <- many . indented $ field syn

90−

90+

9191 return (fields, constructorName, constructorDoc')

92− where

92+ where

9393 field :: SyntaxInfo -> IdrisParser ((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

9494 field syn = do doc <- optional docComment

9595 c <- optional $ lchar '{'

96− n <- (do n <- fnName

96+ n <- (do n <- fst <$> fnName

9797 return $ Just (expandNS syn n))

9898 <|> (do symbol "_"

9999 return Nothing)

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

107107 return (n, p, t, doc')

108108

109109 constructor :: IdrisParser Name

110− constructor = (reserved "constructor") *> fnName

110+ constructor = (reserved "constructor") *> (fst <$> fnName)

111111

112112 endPlicity :: Maybe Char -> IdrisParser Plicity

113113 endPlicity (Just _) = do lchar '}'

@@ -130,13 +130,13 @@ recordParameter syn =

130130 where

131131 namedTy :: SyntaxInfo -> IdrisParser (Name, PTerm)

132132 namedTy syn =

133− do n <- fnName

133+ do n <- fst <$> fnName

134134 lchar ':'

135135 ty <- typeExpr (allowImp syn)

136136 return (expandNS syn n, ty)

137137 onlyName :: SyntaxInfo -> IdrisParser (Name, PTerm)

138138 onlyName syn =

139− do n <- fnName

139+ do n <- fst <$> fnName

140140 fc <- getFC

141141 return (expandNS syn n, PType fc)

142142

@@ -191,7 +191,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

191191 | (n, d) <- argDocs ]

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

193193 fc <- getFC

194− tyn_in <- fnName

194+ tyn_in <- fst <$> fnName

195195 (do try (lchar ':')

196196 popIndent

197197 ty <- typeExpr (allowImp syn)

@@ -201,7 +201,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

201201 cons <- indentedBlock (constructor syn)

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

203203 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

204− args <- many name

204+ args <- many (fst <$> name)

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

206206 let tyn = expandNS syn tyn_in

207207 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

@@ -243,11 +243,11 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

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

244244constructor syn

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

246− cn_in <- fnName; fc <- getFC

246+ cn_in <- fst <$> fnName; fc <- getFC

247247 let cn = expandNS syn cn_in

248248 lchar ':'

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

250− sepBy1 name (lchar ','))

250+ sepBy1 (fst <$> name) (lchar ','))

251251 ty <- typeExpr (allowImp syn)

252252 ist <- get

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

@@ -264,7 +264,7 @@ simpleConstructor syn

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

265265 ist <- get

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

267− cn_in <- fnName

267+ cn_in <- fst <$> fnName

268268 let cn = expandNS syn cn_in

269269 fc <- getFC

270270 args <- many (do notEndApp

@@ -277,7 +277,7 @@ DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

277277 -}

278278dsl :: SyntaxInfo -> IdrisParser PDecl

279279dsl syn = do reserved "dsl"

280− n <- fnName

280+ n <- fst <$> fnName

281281 bs <- indentedBlock (overload syn)

282282 let dsl = mkDSL bs (dsl_info syn)

283283 checkDSL dsl

@@ -314,8 +314,8 @@ OverloadIdentifier ::= 'let' | Identifier;

314314Overload ::= OverloadIdentifier '=' Expr;

315315-}

316316overload :: SyntaxInfo -> IdrisParser (String, PTerm)

317−overload syn = do o <- identifier <|> do reserved "let"

318− return "let"

317+overload syn = do o <- (fst <$> identifier) <|> do reserved "let"

318+ return "let"

319319 if o `notElem` overloadable

320320 then fail $ show o ++ " is not an overloading"

321321 else do

src/Idris/ParseExpr.hs+27−27

@@ -142,7 +142,7 @@ extension syn ns rules =

142142 return $ Just (n, SynTm tm)

143143 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

144144 return $ Just (n, SynTm tm)

145− extensionSymbol (Binding n) = do b <- name

145+ extensionSymbol (Binding n) = do b <- fst <$> name

146146 return $ Just (n, SynBind b)

147147 extensionSymbol (Symbol s) = do symbol s

148148 return Nothing

@@ -324,13 +324,13 @@ SimpleExpr ::=

324324simpleExpr :: SyntaxInfo -> IdrisParser PTerm

325325simpleExpr syn =

326326 try (simpleExternalExpr syn)

327− <|> do x <- try (lchar '?' *> name); return (PMetavar x)

327+ <|> do x <- try (lchar '?' *> (fst <$> name)); return (PMetavar x)

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

329329 <|> do fc <- reservedFC "Refl"

330330 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

331331 return t)

332332 return (PRefl fc tm)

333− <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

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

334334 <|> proofExpr syn

335335 <|> tacticsExpr syn

336336 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

@@ -341,16 +341,16 @@ simpleExpr syn =

341341 <|> do (c, cfc) <- constant

342342 fc <- getFC

343343 return (modifyConst syn fc (PConstant cfc c))

344− <|> do symbol "'"; fc <- getFC; str <- name

344+ <|> do symbol "'"; fc <- getFC; str <- fst <$> name

345345 return (PApp fc (PRef fc (sUN "Symbol_"))

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

347− <|> do fc <- getFC

348− x <- fnName

347+ <|> do (x, fc) <- fnName

349348 if inPattern syn

350349 then option (PRef fc x)

351350 (do reservedOp "@"

352351 s <- simpleExpr syn

353− return (PAs fc x s))

352+ fcIn <- getFC

353+ return (PAs fcIn x s))

354354 else return (PRef fc x)

355355 <|> idiom syn

356356 <|> listExpr syn

@@ -392,7 +392,7 @@ bracketed' syn =

392392 do lchar ')'

393393 fc <- getFC

394394 return $ PTrue fc TypeOrTerm

395− <|> try (do ln <- name; lchar ':';

395+ <|> try (do ln <- fst <$> name; lchar ':';

396396 lty <- expr syn

397397 reservedOp "**"

398398 fc <- getFC

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

522522-}

523523disamb :: SyntaxInfo -> IdrisParser PTerm

524524disamb syn = do reserved "with";

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

525+ ns <- sepBy1 (fst <$> name) (lchar ',')

526526 tm <- expr' syn

527527 return (PDisamb (map tons ns) tm)

528528 <?> "unification log expression"

@@ -557,7 +557,7 @@ app :: SyntaxInfo -> IdrisParser PTerm

557557app syn = do f <- simpleExpr syn

558558 (do try $ reservedOp "<=="

559559 fc <- getFC

560− ff <- fnName

560+ ff <- fst <$> fnName

561561 return (PLet fc (sMN 0 "match")

562562 f

563563 (PMatchApp fc ff)

@@ -596,7 +596,7 @@ ImplicitArg ::=

596596-}

597597implicitArg :: SyntaxInfo -> IdrisParser PArg

598598implicitArg syn = do lchar '{'

599− n <- name

599+ n <- fst <$> name

600600 fc <- getFC

601601 v <- option (PRef fc n) (do lchar '='

602602 expr syn)

@@ -653,7 +653,7 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)

653653-}

654654namequote :: SyntaxInfo -> IdrisParser PTerm

655655namequote syn = do symbol "`{"

656− n <- fnName

656+ n <- fst <$> fnName

657657 symbol "}"

658658 return $ PQuoteName n

659659 <?> "quoted name"

@@ -708,7 +708,7 @@ recordType syn =

708708 <?> "field setter"

709709

710710 fieldGet :: IdrisParser [Name]

711− fieldGet = sepBy1 fnName (symbol "->")

711+ fieldGet = sepBy1 (fst <$> fnName) (symbol "->")

712712

713713 fieldGetOrSet :: IdrisParser (Either [([Name], PTerm)] [Name])

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

@@ -874,7 +874,7 @@ QuoteGoal ::=

874874@

875875 -}

876876quoteGoal :: SyntaxInfo -> IdrisParser PTerm

877−quoteGoal syn = do reserved "quoteGoal"; n <- name;

877+quoteGoal syn = do reserved "quoteGoal"; n <- fst <$> name;

878878 reserved "by"

879879 r <- expr syn

880880 reserved "in"

@@ -1001,7 +1001,7 @@ constraintList1 syn = try (do lchar '('

10011001 reservedOp "=>"

10021002 return [(defname, t)])

10031003 <?> "type constraint list"

1004− where nexpr = try (do n <- name; lchar ':'

1004+ where nexpr = try (do n <- fst <$> name; lchar ':'

10051005 e <- expr syn

10061006 return (n, e))

10071007 <|> do e <- expr syn

@@ -1024,12 +1024,12 @@ FunctionSignatureList ::=

10241024@

10251025-}

10261026typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

1027−typeDeclList syn = try (sepBy1 (do x <- fnName

1027+typeDeclList syn = try (sepBy1 (do x <- fst <$> fnName

10281028 lchar ':'

10291029 t <- typeExpr (disallowImp syn)

10301030 return (x,t))

10311031 (lchar ','))

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

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

10331033 lchar ':'

10341034 t <- typeExpr (disallowImp syn)

10351035 return (map (\x -> (x, t)) ns)

@@ -1055,7 +1055,7 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

10551055 (lchar ',')

10561056 <?> "type declaration list"

10571057 where nameOrPlaceholder :: IdrisParser Name

1058− nameOrPlaceholder = fnName

1058+ nameOrPlaceholder = fst <$> fnName

10591059 <|> do symbol "_"

10601060 return (sMN 0 "underscore")

10611061 <?> "name or placeholder"

@@ -1136,7 +1136,7 @@ Do ::=

11361136do_ :: SyntaxInfo -> IdrisParser PDo

11371137do_ syn

11381138 = try (do reserved "let"

1139− i <- name

1139+ i <- fst <$> name

11401140 ty <- option Placeholder (do lchar ':'

11411141 expr' syn)

11421142 reservedOp "="

@@ -1149,7 +1149,7 @@ do_ syn

11491149 fc <- getFC

11501150 sc <- expr syn

11511151 return (DoLetP fc i sc))

1152− <|> try (do i <- name

1152+ <|> try (do i <- fst <$> name

11531153 symbol "<-"

11541154 fc <- getFC

11551155 e <- expr syn;

@@ -1325,26 +1325,26 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

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

13261326tactics =

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

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

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

13291329 , noArgs ["intros"] Intros

13301330 , noArgs ["unfocus"] Unfocus

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

1332− do n <- spaced fnName

1332+ do n <- spaced (fst <$> fnName)

13331333 imps <- many imp

13341334 return $ Refine n imps)

13351335 , (["claim"], Nothing, \syn ->

1336− do n <- indentPropHolds gtProp *> name

1336+ do n <- indentPropHolds gtProp *> (fst <$> name)

13371337 goal <- indentPropHolds gtProp *> expr syn

13381338 return $ Claim n goal)

13391339 , (["mrefine"], Just ExprTArg, const $

1340− do n <- spaced fnName

1340+ do n <- spaced (fst <$> fnName)

13411341 return $ MatchRefine n)

13421342 , expressionTactic ["rewrite"] Rewrite

13431343 , expressionTactic ["case"] CaseTac

13441344 , expressionTactic ["induction"] Induction

13451345 , expressionTactic ["equiv"] Equiv

13461346 , (["let"], Nothing, \syn -> -- FIXME syntax for let

1347− do n <- (indentPropHolds gtProp *> name)

1347+ do n <- (indentPropHolds gtProp *> (fst <$> name))

13481348 (do indentPropHolds gtProp *> lchar ':'

13491349 ty <- indentPropHolds gtProp *> expr' syn

13501350 indentPropHolds gtProp *> lchar '='

@@ -1357,7 +1357,7 @@ tactics =

13571357 return $ LetTac n (desugar syn i t)))

13581358

13591359 , (["focus"], Just ExprTArg, const $

1360− do n <- spaced name

1360+ do n <- spaced (fst <$> name)

13611361 return $ Focus n)

13621362 , expressionTactic ["exact"] Exact

13631363 , expressionTactic ["applyTactic"] ApplyTactic

@@ -1393,7 +1393,7 @@ tactics =

13931393 return $ TFail [Idris.Core.TT.TextPart msg])

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

13951395 do whiteSpace

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

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

13971397 eof

13981398 return (TDocStr doc))

13991399 ]

src/Idris/ParseHelpers.hs+28−18

@@ -189,7 +189,7 @@ docComment = do dc <- pushIndent *> docCommentLine

189189 many (satisfy isSpace)

190190 char '@'

191191 many (satisfy isSpace)

192− n <- name

192+ n <- fst <$> name

193193 many (satisfy isSpace)

194194 docs <- many (satisfy (not . isEol))

195195 eol ; someSpace

@@ -278,37 +278,47 @@ reservedOp name = token $ try $

278278 do string name

279279 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

280280

281−-- | Parses an identifier as a token

282−identifier :: MonadicParsing m => m String

283−identifier = try(do i <- token $ Tok.ident idrisStyle

281+-- | Parses an identifier as a token

282+identifier :: (MonadicParsing m) => m (String, FC)

283+identifier = try(do (i, fc) <-

284+ token $ do (FC f (l, c) _) <- getFC

285+ i <- Tok.ident idrisStyle

286+ return (i, FC f (l, c) (l, c + length i))

284287 when (i == "_") $ unexpected "wildcard"

285− return i)

288+ return (i, fc))

286289

287290-- | Parses an identifier with possible namespace as a name

288−iName :: MonadicParsing m => [String] -> m Name

289−iName bad = maybeWithNS identifier False bad <?> "name"

291+iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

292+iName bad = do (n, fc) <- maybeWithNS identifier False bad

293+ return (n, fc)

294+ <?> "name"

290295

291296-- | Parses an string possibly prefixed by a namespace

292−maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m Name

297+maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

293298maybeWithNS parser ascend bad = do

294− i <- option "" (lookAhead identifier)

299+ fc <- getFC

300+ i <- option "" (lookAhead (fst <$> identifier))

295301 when (i `elem` bad) $ unexpected "reserved identifier"

296302 let transf = if ascend then id else reverse

297− (x, xs) <- choice (transf (parserNoNS parser : parsersNS parser i))

298− return $ mkName (x, xs)

299− where parserNoNS :: MonadicParsing m => m String -> m (String, String)

300− parserNoNS parser = do x <- parser; return (x, "")

301− parserNS :: MonadicParsing m => m String -> String -> m (String, String)

302− parserNS parser ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)

303− parsersNS :: MonadicParsing m => m String -> String -> [m (String, String)]

303+ (x, xs, fc) <- choice (transf (parserNoNS parser : parsersNS parser i))

304+ return (mkName (x, xs), fc)

305+ where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

306+ parserNoNS parser = do (x, fc) <- parser; return (x, "", fc)

307+ parserNS :: MonadicParsing m => m (String, FC) -> String -> m (String, String, FC)

308+ parserNS parser ns = do startFC <- getFC

309+ xs <- string ns

310+ lchar '.'; (x, nameFC) <- parser

311+ return (x, xs, spanFC startFC nameFC)

312+ parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

304313 parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

305314

306315-- | Parses a name

307−name :: IdrisParser Name

316+name :: IdrisParser (Name, FC)

308317name = (<?> "name") $ do

309318 keywords <- syntax_keywords <$> get

310319 aliases <- module_aliases <$> get

311− unalias aliases <$> iName keywords

320+ (n, fc) <- iName keywords

321+ return (unalias aliases n, fc)

312322 where

313323 unalias :: M.Map [T.Text] [T.Text] -> Name -> Name

314324 unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'

src/Idris/ParseOps.hs+9−5

@@ -77,7 +77,7 @@ prefix name f = Prefix (do reservedOp name

7777-- | Backtick operator

7878backtick :: Operator IdrisParser PTerm

7979backtick = Infix (do indentPropHolds gtProp

80− lchar '`'; n <- fnName

80+ lchar '`'; n <- fst <$> fnName

8181 lchar '`'

8282 indentPropHolds gtProp

8383 fc <- getFC

@@ -101,9 +101,13 @@ nofixityoperator = Infix (do indentPropHolds gtProp

101101@

102102

103103-}

104−operatorFront :: IdrisParser Name

105−operatorFront = try ((lchar '(' *> reservedOp "=" <* lchar ')') >> (return eqTy))

106− <|> maybeWithNS (lchar '(' *> operator <* lchar ')') False []

104+operatorFront :: IdrisParser (Name, FC)

105+operatorFront = try (do (FC f (l, c) _) <- getFC

106+ op <- lchar '(' *> reservedOp "=" <* lchar ')'

107+ return (eqTy, FC f (l, c) (l, c+3)))

108+ <|> maybeWithNS (do (FC f (l, c) _) <- getFC

109+ op <- lchar '(' *> operator <* lchar ')'

110+ return (op, (FC f (l, c) (l, c+1)))) False []

107111

108112{- | Parses a function (either normal name or operator)

109113

@@ -111,7 +115,7 @@ operatorFront = try ((lchar '(' *> reservedOp "=" <* lchar ')') >> (return eqTy

111115 FnName ::= Name | OperatorFront;

112116@

113117-}

114−fnName :: IdrisParser Name

118+fnName :: IdrisParser (Name, FC)

115119fnName = try operatorFront <|> name <?> "function name"

116120

117121{- | Parses a fixity declaration

src/Idris/Parser.hs+38−37

@@ -96,7 +96,7 @@ moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])

9696moduleHeader = try (do docs <- optional docComment

9797 noArgs docs

9898 reserved "module"

99− i <- identifier

99+ i <- fst <$> identifier

100100 option ';' (lchar ';')

101101 return (fmap fst docs, moduleName i))

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

@@ -118,8 +118,8 @@ import_ :: IdrisParser (Bool, String, Maybe String, FC)

118118import_ = do fc <- getFC

119119 reserved "import"

120120 reexport <- option False (do reserved "public"; return True)

121− id <- identifier

122− newName <- optional (reserved "as" *> identifier)

121+ id <- fst <$> identifier

122+ newName <- optional (reserved "as" *> (fst <$> identifier))

123123 option ';' (lchar ';')

124124 return (reexport, toPath id, toPath <$> newName, fc)

125125 <?> "import statement"

@@ -356,11 +356,11 @@ SyntaxSym ::= '[' Name_t ']'

356356@

357357 -}

358358syntaxSym :: IdrisParser SSymbol

359−syntaxSym = try (do lchar '['; n <- name; lchar ']'

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

360360 return (Expr n))

361− <|> try (do lchar '{'; n <- name; lchar '}'

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

362362 return (Binding n))

363− <|> do n <- iName []

363+ <|> do n <- fst <$> iName []

364364 return (Keyword n)

365365 <|> do sym <- fmap fst stringLiteral

366366 return (Symbol sym)

@@ -402,7 +402,7 @@ fnDecl' syn = checkFixity $

402402 opts <- fnOpts initOpts

403403 acc <- optional accessibility

404404 opts' <- fnOpts opts

405− n_in <- fnName

405+ n_in <- fst <$> fnName

406406 let n = expandNS syn n_in

407407 fc <- getFC

408408 lchar ':'

@@ -489,7 +489,7 @@ fnOpts opts

489489 <|> return opts

490490 <?> "function modifier"

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

492− nameTimes = do n <- fnName

492+ nameTimes = do n <- fst <$> fnName

493493 t <- option Nothing (do reds <- fmap fst natural

494494 return (Just (fromInteger reds)))

495495 return (n, t)

@@ -515,7 +515,7 @@ postulate syn = do (doc, ext)

515515 opts <- fnOpts initOpts

516516 acc <- optional accessibility

517517 opts' <- fnOpts opts

518− n_in <- fnName

518+ n_in <- fst <$> fnName

519519 let n = expandNS syn n_in

520520 lchar ':'

521521 ty <- typeExpr (allowImp syn)

@@ -592,7 +592,7 @@ Namespace ::=

592592-}

593593namespace :: SyntaxInfo -> IdrisParser [PDecl]

594594namespace syn =

595− do reserved "namespace"; n <- identifier;

595+ do reserved "namespace"; n <- fst <$> identifier

596596 openBlock

597597 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })

598598 closeBlock

@@ -659,7 +659,7 @@ class_ syn = do (doc, argDocs, acc)

659659 return (doc, argDocs, acc))

660660 fc <- getFC

661661 cons <- constraintList syn

662− n_in <- fnName

662+ n_in <- fst <$> fnName

663663 let n = expandNS syn n_in

664664 cs <- many carg

665665 fds <- option (map fst cs) fundeps

@@ -669,12 +669,12 @@ class_ syn = do (doc, argDocs, acc)

669669 <?> "type-class declaration"

670670 where

671671 fundeps :: IdrisParser [Name]

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

672+ fundeps = do lchar '|'; sepBy (fst <$> name) (lchar ',')

673673

674674 carg :: IdrisParser (Name, PTerm)

675− carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

675+ carg = do lchar '('; i <- (fst <$> name); lchar ':'; ty <- expr syn; lchar ')'

676676 return (i, ty)

677− <|> do i <- name

677+ <|> do i <- fst <$> name

678678 fc <- getFC

679679 return (i, PType fc)

680680

@@ -696,7 +696,7 @@ instance_ syn = do (doc, argDocs)

696696 fc <- getFC

697697 en <- optional instanceName

698698 cs <- constraintList syn

699− cn <- fnName

699+ cn <- fst <$> fnName

700700 args <- many (simpleExpr syn)

701701 let sc = PApp fc (PRef fc cn) (map pexp args)

702702 let t = bindList (PPi constraint) cs sc

@@ -704,7 +704,7 @@ instance_ syn = do (doc, argDocs)

704704 return [PInstance doc argDocs syn fc cs cn args t en ds]

705705 <?> "instance declaration"

706706 where instanceName :: IdrisParser Name

707− instanceName = do lchar '['; n_in <- fnName; lchar ']'

707+ instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

708708 let n = expandNS syn n_in

709709 return n

710710 <?> "instance name"

@@ -748,7 +748,7 @@ NameList ::=

748748usingDeclList :: SyntaxInfo -> IdrisParser [Using]

749749usingDeclList syn

750750 = try (sepBy1 (usingDecl syn) (lchar ','))

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

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

752752 lchar ':'

753753 t <- typeExpr (disallowImp syn)

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

@@ -764,12 +764,12 @@ UsingDecl ::=

764764@

765765-}

766766usingDecl :: SyntaxInfo -> IdrisParser Using

767−usingDecl syn = try (do x <- fnName

767+usingDecl syn = try (do x <- fst <$> fnName

768768 lchar ':'

769769 t <- typeExpr (disallowImp syn)

770770 return (UImplicit x t))

771− <|> do c <- fnName

772− xs <- some fnName

771+ <|> do c <- fst <$> fnName

772+ xs <- some (fst <$> fnName)

773773 return (UConstraint c xs)

774774 <?> "using declaration"

775775

@@ -793,7 +793,7 @@ CAF ::= 'let' FnName '=' Expr Terminator;

793793-}

794794caf :: SyntaxInfo -> IdrisParser PDecl

795795caf syn = do reserved "let"

796− n_in <- fnName; let n = expandNS syn n_in

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

797797 lchar '='

798798 t <- expr syn

799799 terminator

@@ -829,7 +829,7 @@ rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

829829rhs syn n = do lchar '='; expr syn

830830 <|> do symbol "?=";

831831 fc <- getFC

832− name <- option n' (do symbol "{"; n <- fnName; symbol "}";

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

833833 return n)

834834 r <- expr syn

835835 return (addLet fc name r)

@@ -903,7 +903,7 @@ clause syn

903903 symbol "<=="

904904 return ty)

905905 fc <- getFC

906− n_in <- fnName; let n = expandNS syn n_in

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

907907 r <- rhs syn n

908908 ist <- get

909909 let ctxt = tt_ctxt ist

@@ -955,7 +955,7 @@ clause syn

955955 put (ist { lastParse = Just n })

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

957957 <|> do pushIndent

958− n_in <- fnName; let n = expandNS syn n_in

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

959959 cargs <- many (constraintArg syn)

960960 fc <- getFC

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

@@ -989,7 +989,7 @@ clause syn

989989 <?> "function clause"

990990 where

991991 optProof = option Nothing (do reserved "proof"

992− n <- fnName

992+ n <- fst <$> fnName

993993 return (Just n))

994994

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

@@ -1042,7 +1042,8 @@ Codegen ::= 'C'

10421042@

10431043-}

10441044codegen_ :: IdrisParser Codegen

1045−codegen_ = do n <- identifier; return (Via (map toLower n))

1045+codegen_ = do n <- fst <$> identifier

1046+ return (Via (map toLower n))

10461047 <|> do reserved "Bytecode"; return Bytecode

10471048 <?> "code generation language"

10481049

@@ -1091,9 +1092,9 @@ directive syn = do try (lchar '%' *> reserved "lib")

10911092 cgn <- codegen_

10921093 hdr <- fst <$> stringLiteral

10931094 return [PDirective (DInclude cgn hdr)]

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

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

10951096 return [PDirective (DHide n)]

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

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

10971098 return [PDirective (DFreeze n)]

10981099 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility

10991100 return [PDirective (DAccess acc)]

@@ -1108,20 +1109,20 @@ directive syn = do try (lchar '%' *> reserved "lib")

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

11091110 return [PDirective (DDynamicLibs libs)]

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

1111− ty <- fnName

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

1112+ ty <- fst <$> fnName

1113+ ns <- sepBy1 (fst <$> name) (lchar ',')

11131114 return [PDirective (DNameHint ty ns)]

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

1115− fn <- fnName

1116− arg <- fnName

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

1116+ fn <- fst <$> fnName

1117+ arg <- fst <$> fnName

1118+ ns <- sepBy1 (fst <$> name) (lchar ',')

11181119 return [PDirective (DErrorHandlers fn arg ns) ]

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

11201121 return [PDirective (DLanguage ext)]

11211122 <|> do fc <- getFC

11221123 try (lchar '%' *> reserved "used")

1123− fn <- fnName

1124− arg <- iName []

1124+ fn <- fst <$> fnName

1125+ arg <- fst <$> iName []

11251126 return [PDirective (DUsed fc fn arg)]

11261127 <?> "directive"

11271128

@@ -1156,14 +1157,14 @@ provider syn = do doc <- try (do (doc, _) <- docstring syn

11561157 provideTerm doc <|> providePostulate doc

11571158 <?> "type provider"

11581159 where provideTerm doc =

1159− do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1160+ do lchar '('; n <- fst <$> fnName; lchar ':'; t <- typeExpr syn; lchar ')'

11601161 fc <- getFC

11611162 reserved "with"

11621163 e <- expr syn <?> "provider expression"

11631164 return [PProvider doc syn fc (ProvTerm t e) n]

11641165 providePostulate doc =

11651166 do reserved "postulate"

1166− n <- fnName

1167+ n <- fst <$> fnName

11671168 fc <- getFC

11681169 reserved "with"

11691170 e <- expr syn <?> "provider expression"

src/Idris/REPL.hs+1−1

@@ -1293,7 +1293,7 @@ process fn (Browse ns) =

12931293process fn (MakeDoc s) =

12941294 do istate <- getIState

12951295 let names = words s

1296− parse n | Success x <- runparser name istate fn n = Right x

1296+ parse n | Success x <- runparser (fmap fst name) istate fn n = Right x

12971297 parse n = Left n

12981298 (bad, nss) = partitionEithers $ map parse names

12991299 cd <- runIO $ getCurrentDirectory

src/Idris/REPLParser.hs+15−15

@@ -212,19 +212,19 @@ genArg argName argParser cmd name = do

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

213213

214214nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

215−nameArg = genArg "name" P.name

216−fnNameArg = genArg "functionname" P.fnName

215+nameArg = genArg "name" $ fst <$> P.name

216+fnNameArg = genArg "functionname" $ fst <$> P.fnName

217217

218218strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

219219strArg = genArg "string" (many anyChar)

220220

221221moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

222−moduleArg = genArg "module" (fmap toPath P.identifier)

222+moduleArg = genArg "module" (fmap (toPath . fst) P.identifier)

223223 where

224224 toPath n = foldl1' (</>) $ splitOn "." n

225225

226226namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

227−namespaceArg = genArg "namespace" (fmap toNS P.identifier)

227+namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

228228 where

229229 toNS = splitOn "."

230230

@@ -258,8 +258,8 @@ proofArg cmd name = do

258258 upd <- option False $ do

259259 P.lchar '!'

260260 return True

261− l <- fmap fst P.natural

262− n <- P.name;

261+ l <- fst <$> P.natural

262+ n <- fst <$> P.name;

263263 return (Right (cmd upd (fromInteger l) n))

264264

265265cmd_doc :: String -> P.IdrisParser (Either String Command)

@@ -327,20 +327,20 @@ cmd_compile name = do

327327 let codegenOption :: P.IdrisParser Codegen

328328 codegenOption = do

329329 let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode

330− viaCodegen = do x <- P.identifier

330+ viaCodegen = do x <- fst <$> P.identifier

331331 return (Via (map toLower x))

332332 bytecodeCodegen <|> viaCodegen

333333

334334 let hasOneArg = do

335335 i <- get

336− f <- P.identifier

336+ f <- fst <$> P.identifier

337337 eof

338338 return $ Right (Compile defaultCodegen f)

339339

340340 let hasTwoArgs = do

341341 i <- get

342342 codegen <- codegenOption

343− f <- P.identifier

343+ f <- fst <$> P.identifier

344344 eof

345345 return $ Right (Compile codegen f)

346346

@@ -350,7 +350,7 @@ cmd_compile name = do

350350cmd_addproof :: String -> P.IdrisParser (Either String Command)

351351cmd_addproof name = do

352352 n <- option Nothing $ do

353− x <- P.name

353+ x <- fst <$> P.name

354354 return (Just x)

355355 eof

356356 return (Right (AddProof n))

@@ -367,7 +367,7 @@ cmd_let name = do

367367 return (Right (NewDefn defn))

368368

369369cmd_unlet :: String -> P.IdrisParser (Either String Command)

370−cmd_unlet name = (Right . Undefine) `fmap` many P.name

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

371371

372372cmd_loadto :: String -> P.IdrisParser (Either String Command)

373373cmd_loadto name = do

@@ -459,13 +459,13 @@ cmd_search = packageBasedCmd

459459cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

460460cmd_proofsearch name = do

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

462− l <- fmap (fromInteger . fst) P.natural; n <- P.name

463− hints <- many P.fnName

462+ l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

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

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

465465

466466cmd_refine :: String -> P.IdrisParser (Either String Command)

467467cmd_refine name = do

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

469− l <- fmap (fromInteger . fst) P.natural; n <- P.name

470− hint <- P.fnName

469+ l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

470+ hint <- fst <$> P.fnName

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

src/Pkg/PParser.hs+11−8

@@ -34,6 +34,9 @@ data PkgDesc = PkgDesc { pkgname :: String,

3434 }

3535 deriving Show

3636

37+instance HasLastTokenSpan PParser where

38+ getLastTokenSpan = return Nothing

39+

3740#if MIN_VERSION_base(4,8,0)

3841instance {-# OVERLAPPING #-} TokenParsing PParser where

3942#else

@@ -51,7 +54,7 @@ parseDesc fp = do p <- readFile fp

5154 Success x -> return x

5255

5356pPkg :: PParser PkgDesc

54−pPkg = do reserved "package"; p <- identifier

57+pPkg = do reserved "package"; p <- fst <$> identifier

5558 st <- get

5659 put (st { pkgname = p })

5760 some pClause

@@ -68,11 +71,11 @@ pClause = do reserved "executable"; lchar '=';

6871 else ( show exec )

6972 ) })

7073 <|> do reserved "main"; lchar '=';

71− main <- iName []

74+ main <- fst <$> iName []

7275 st <- get

7376 put (st { idris_main = main })

7477 <|> do reserved "sourcedir"; lchar '=';

75− src <- identifier

78+ src <- fst <$> identifier

7679 st <- get

7780 put (st { sourcedir = src })

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

@@ -81,23 +84,23 @@ pClause = do reserved "executable"; lchar '=';

8184 let args = pureArgParser (words opts)

8285 put (st { idris_opts = args })

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

84− ms <- sepBy1 (iName []) (lchar ',')

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

8588 st <- get

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

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

88− ls <- sepBy1 identifier (lchar ',')

91+ ls <- sepBy1 (fst <$> identifier) (lchar ',')

8992 st <- get

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

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

92− ls <- sepBy1 identifier (lchar ',')

95+ ls <- sepBy1 (fst <$> identifier) (lchar ',')

9396 st <- get

9497 put (st { objs = libdeps st ++ ls })

9598 <|> do reserved "makefile"; lchar '=';

96− mk <- iName []

99+ mk <- fst <$> iName []

97100 st <- get

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

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

100− ts <- sepBy1 (iName []) (lchar ',')

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

101104 st <- get

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

103106