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

git.iko.soy/Idris-dev

on master help sign in

Highlight names of simple variable references

4ebafb4David Raymond Christiansen11 years ago

src/Idris/Core/TT.hs+25

compare with master

unifiedsplit

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

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

58 deriving (Data, Typeable, Ord)

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+

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

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

61instance Eq FC where

86instance Eq FC where

62 _ == _ = True

87 _ == _ = True

src/Idris/ParseData.hs+15−15

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

53 co <- recordI

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

55 fc <- getFC

56− tyn_in <- fnName

56+ tyn_in <- fst <$> fnName

57 let tyn = expandNS syn tyn_in

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

59 syn_namespace syn }

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

87 let constructorDoc' = annotate syn ist constructorDoc

89 fields <- many . indented $ field syn

90−

90+

91 return (fields, constructorName, constructorDoc')

92− where

92+ where

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

94 field syn = do doc <- optional docComment

95 c <- optional $ lchar '{'

96− n <- (do n <- fnName

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

97 return $ Just (expandNS syn n))

98 <|> (do symbol "_"

99 return Nothing)

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

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

108

109 constructor :: IdrisParser Name

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

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

111

112 endPlicity :: Maybe Char -> IdrisParser Plicity

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

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

130 where

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

132 namedTy syn =

133− do n <- fnName

133+ do n <- fst <$> fnName

134 lchar ':'

135 ty <- typeExpr (allowImp syn)

136 return (expandNS syn n, ty)

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

138 onlyName syn =

139− do n <- fnName

139+ do n <- fst <$> fnName

140 fc <- getFC

141 return (expandNS syn n, PType fc)

142

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

191 | (n, d) <- argDocs ]

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

193 fc <- getFC

194− tyn_in <- fnName

194+ tyn_in <- fst <$> fnName

195 (do try (lchar ':')

196 popIndent

197 ty <- typeExpr (allowImp syn)

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

201 cons <- indentedBlock (constructor syn)

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

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

204− args <- many name

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

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

206 let tyn = expandNS syn tyn_in

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

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

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

244constructor syn

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

246− cn_in <- fnName; fc <- getFC

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

247 let cn = expandNS syn cn_in

248 lchar ':'

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

250− sepBy1 name (lchar ','))

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

251 ty <- typeExpr (allowImp syn)

252 ist <- get

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

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

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

265 ist <- get

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

267− cn_in <- fnName

267+ cn_in <- fst <$> fnName

268 let cn = expandNS syn cn_in

269 fc <- getFC

270 args <- many (do notEndApp

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

277 -}

278dsl :: SyntaxInfo -> IdrisParser PDecl

279dsl syn = do reserved "dsl"

280− n <- fnName

280+ n <- fst <$> fnName

281 bs <- indentedBlock (overload syn)

282 let dsl = mkDSL bs (dsl_info syn)

283 checkDSL dsl

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

314Overload ::= OverloadIdentifier '=' Expr;

315-}

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

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

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

318− return "let"

318+ return "let"

319 if o `notElem` overloadable

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

321 else do

src/Idris/ParseExpr.hs+27−27

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

142 return $ Just (n, SynTm tm)

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

144 return $ Just (n, SynTm tm)

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

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

146 return $ Just (n, SynBind b)

147 extensionSymbol (Symbol s) = do symbol s

148 return Nothing

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

324simpleExpr :: SyntaxInfo -> IdrisParser PTerm

325simpleExpr syn =

326 try (simpleExternalExpr syn)

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

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

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

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

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

331 return t)

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

334 <|> proofExpr syn

335 <|> tacticsExpr syn

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

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

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

342 fc <- getFC

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

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

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

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

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

347− <|> do fc <- getFC

348− x <- fnName

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

349 if inPattern syn

348 if inPattern syn

350 then option (PRef fc x)

349 then option (PRef fc x)

351 (do reservedOp "@"

350 (do reservedOp "@"

352 s <- simpleExpr syn

351 s <- simpleExpr syn

352+ fcIn <- getFC

353− return (PAs fc x s))

353+ return (PAs fcIn x s))

354 else return (PRef fc x)

355 <|> idiom syn

356 <|> listExpr syn

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

392 do lchar ')'

393 fc <- getFC

394 return $ PTrue fc TypeOrTerm

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

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

396 lty <- expr syn

397 reservedOp "**"

398 fc <- getFC

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

522-}

523disamb :: SyntaxInfo -> IdrisParser PTerm

524disamb syn = do reserved "with";

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

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

526 tm <- expr' syn

527 return (PDisamb (map tons ns) tm)

528 <?> "unification log expression"

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

557app syn = do f <- simpleExpr syn

558 (do try $ reservedOp "<=="

559 fc <- getFC

560− ff <- fnName

560+ ff <- fst <$> fnName

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

562 f

563 (PMatchApp fc ff)

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

596-}

597implicitArg :: SyntaxInfo -> IdrisParser PArg

598implicitArg syn = do lchar '{'

599− n <- name

599+ n <- fst <$> name

600 fc <- getFC

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

602 expr syn)

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

653-}

654namequote :: SyntaxInfo -> IdrisParser PTerm

655namequote syn = do symbol "`{"

656− n <- fnName

656+ n <- fst <$> fnName

657 symbol "}"

658 return $ PQuoteName n

659 <?> "quoted name"

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

708 <?> "field setter"

709

710 fieldGet :: IdrisParser [Name]

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

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

712

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

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

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

874@

875 -}

876quoteGoal :: SyntaxInfo -> IdrisParser PTerm

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

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

878 reserved "by"

879 r <- expr syn

880 reserved "in"

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

1001 reservedOp "=>"

1002 return [(defname, t)])

1003 <?> "type constraint list"

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

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

1005 e <- expr syn

1006 return (n, e))

1007 <|> do e <- expr syn

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

1024@

1025-}

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

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

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

1028 lchar ':'

1029 t <- typeExpr (disallowImp syn)

1030 return (x,t))

1031 (lchar ','))

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

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

1033 lchar ':'

1034 t <- typeExpr (disallowImp syn)

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

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

1055 (lchar ',')

1056 <?> "type declaration list"

1057 where nameOrPlaceholder :: IdrisParser Name

1058− nameOrPlaceholder = fnName

1058+ nameOrPlaceholder = fst <$> fnName

1059 <|> do symbol "_"

1060 return (sMN 0 "underscore")

1061 <?> "name or placeholder"

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

1136do_ :: SyntaxInfo -> IdrisParser PDo

1137do_ syn

1138 = try (do reserved "let"

1139− i <- name

1139+ i <- fst <$> name

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

1141 expr' syn)

1142 reservedOp "="

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

1149 fc <- getFC

1150 sc <- expr syn

1151 return (DoLetP fc i sc))

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

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

1153 symbol "<-"

1154 fc <- getFC

1155 e <- expr syn;

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

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

1326tactics =

1327 [ (["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)

1329 , noArgs ["intros"] Intros

1330 , noArgs ["unfocus"] Unfocus

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

1332− do n <- spaced fnName

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

1333 imps <- many imp

1334 return $ Refine n imps)

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

1336− do n <- indentPropHolds gtProp *> name

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

1337 goal <- indentPropHolds gtProp *> expr syn

1338 return $ Claim n goal)

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

1340− do n <- spaced fnName

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

1341 return $ MatchRefine n)

1342 , expressionTactic ["rewrite"] Rewrite

1343 , expressionTactic ["case"] CaseTac

1344 , expressionTactic ["induction"] Induction

1345 , expressionTactic ["equiv"] Equiv

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

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

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

1348 (do indentPropHolds gtProp *> lchar ':'

1349 ty <- indentPropHolds gtProp *> expr' syn

1350 indentPropHolds gtProp *> lchar '='

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

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

1358

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

1360− do n <- spaced name

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

1361 return $ Focus n)

1362 , expressionTactic ["exact"] Exact

1363 , expressionTactic ["applyTactic"] ApplyTactic

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

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

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

1395 do whiteSpace

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

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

1397 eof

1398 return (TDocStr doc))

1399 ]

src/Idris/ParseHelpers.hs+28−18

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

189 many (satisfy isSpace)

190 char '@'

191 many (satisfy isSpace)

192− n <- name

192+ n <- fst <$> name

193 many (satisfy isSpace)

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

195 eol ; someSpace

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

278 do string name

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

280

281−-- | Parses an identifier as a token

281+-- | Parses an identifier as a token

282−identifier :: MonadicParsing m => m String

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

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

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

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

285+ i <- Tok.ident idrisStyle

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

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

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

285− return i)

288+ return (i, fc))

286

289

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

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

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

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

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

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

293+ return (n, fc)

294+ <?> "name"

290

295

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

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

293maybeWithNS parser ascend bad = do

298maybeWithNS parser ascend bad = do

299+ fc <- getFC

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

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

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

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

296 let transf = if ascend then id else reverse

302 let transf = if ascend then id else reverse

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

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

298− return $ mkName (x, xs)

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

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

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

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

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

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

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

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

308+ parserNS parser ns = do startFC <- getFC

309+ xs <- string ns

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

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

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

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

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

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

305

314

306-- | Parses a name

315-- | Parses a name

307−name :: IdrisParser Name

316+name :: IdrisParser (Name, FC)

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

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

309 keywords <- syntax_keywords <$> get

318 keywords <- syntax_keywords <$> get

310 aliases <- module_aliases <$> get

319 aliases <- module_aliases <$> get

311− unalias aliases <$> iName keywords

320+ (n, fc) <- iName keywords

321+ return (unalias aliases n, fc)

312 where

322 where

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

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

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

324 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

77-- | Backtick operator

78backtick :: Operator IdrisParser PTerm

79backtick = Infix (do indentPropHolds gtProp

80− lchar '`'; n <- fnName

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

81 lchar '`'

82 indentPropHolds gtProp

83 fc <- getFC

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

101@

102

103-}

104−operatorFront :: IdrisParser Name

104+operatorFront :: IdrisParser (Name, FC)

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

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

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

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

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

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

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

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

107

111

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

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

109

113

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

111 FnName ::= Name | OperatorFront;

115 FnName ::= Name | OperatorFront;

112@

116@

113-}

117-}

114−fnName :: IdrisParser Name

118+fnName :: IdrisParser (Name, FC)

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

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

116

120

117{- | Parses a fixity declaration

121{- | Parses a fixity declaration

src/Idris/Parser.hs+38−37

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

96moduleHeader = try (do docs <- optional docComment

97 noArgs docs

98 reserved "module"

99− i <- identifier

99+ i <- fst <$> identifier

100 option ';' (lchar ';')

101 return (fmap fst docs, moduleName i))

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

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

118import_ = do fc <- getFC

119 reserved "import"

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

121− id <- identifier

121+ id <- fst <$> identifier

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

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

123 option ';' (lchar ';')

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

125 <?> "import statement"

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

356@

357 -}

358syntaxSym :: IdrisParser SSymbol

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

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

360 return (Expr n))

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

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

362 return (Binding n))

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

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

364 return (Keyword n)

365 <|> do sym <- fmap fst stringLiteral

366 return (Symbol sym)

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

402 opts <- fnOpts initOpts

403 acc <- optional accessibility

404 opts' <- fnOpts opts

405− n_in <- fnName

405+ n_in <- fst <$> fnName

406 let n = expandNS syn n_in

407 fc <- getFC

408 lchar ':'

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

489 <|> return opts

490 <?> "function modifier"

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

492− nameTimes = do n <- fnName

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

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

494 return (Just (fromInteger reds)))

495 return (n, t)

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

515 opts <- fnOpts initOpts

516 acc <- optional accessibility

517 opts' <- fnOpts opts

518− n_in <- fnName

518+ n_in <- fst <$> fnName

519 let n = expandNS syn n_in

520 lchar ':'

521 ty <- typeExpr (allowImp syn)

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

592-}

593namespace :: SyntaxInfo -> IdrisParser [PDecl]

594namespace syn =

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

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

596 openBlock

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

598 closeBlock

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

659 return (doc, argDocs, acc))

660 fc <- getFC

661 cons <- constraintList syn

662− n_in <- fnName

662+ n_in <- fst <$> fnName

663 let n = expandNS syn n_in

664 cs <- many carg

665 fds <- option (map fst cs) fundeps

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

669 <?> "type-class declaration"

670 where

671 fundeps :: IdrisParser [Name]

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

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

673

674 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 ')'

676 return (i, ty)

677− <|> do i <- name

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

678 fc <- getFC

679 return (i, PType fc)

680

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

696 fc <- getFC

697 en <- optional instanceName

698 cs <- constraintList syn

699− cn <- fnName

699+ cn <- fst <$> fnName

700 args <- many (simpleExpr syn)

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

702 let t = bindList (PPi constraint) cs sc

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

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

705 <?> "instance declaration"

706 where instanceName :: IdrisParser Name

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

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

708 let n = expandNS syn n_in

709 return n

710 <?> "instance name"

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

748usingDeclList :: SyntaxInfo -> IdrisParser [Using]

749usingDeclList syn

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

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

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

752 lchar ':'

753 t <- typeExpr (disallowImp syn)

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

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

764@

765-}

766usingDecl :: SyntaxInfo -> IdrisParser Using

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

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

768 lchar ':'

769 t <- typeExpr (disallowImp syn)

770 return (UImplicit x t))

771− <|> do c <- fnName

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

772− xs <- some fnName

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

773 return (UConstraint c xs)

774 <?> "using declaration"

775

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

793-}

794caf :: SyntaxInfo -> IdrisParser PDecl

795caf 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

797 lchar '='

798 t <- expr syn

799 terminator

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

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

830 <|> do symbol "?=";

831 fc <- getFC

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

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

833 return n)

834 r <- expr syn

835 return (addLet fc name r)

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

903 symbol "<=="

904 return ty)

905 fc <- getFC

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

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

907 r <- rhs syn n

908 ist <- get

909 let ctxt = tt_ctxt ist

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

955 put (ist { lastParse = Just n })

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

957 <|> do pushIndent

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

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

959 cargs <- many (constraintArg syn)

960 fc <- getFC

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

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

989 <?> "function clause"

990 where

991 optProof = option Nothing (do reserved "proof"

992− n <- fnName

992+ n <- fst <$> fnName

993 return (Just n))

994

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

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

1042@

1043-}

1044codegen_ :: IdrisParser Codegen

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

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

1046+ return (Via (map toLower n))

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

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

1047 <?> "code generation language"

1048 <?> "code generation language"

1048

1049

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

1091 cgn <- codegen_

1092 cgn <- codegen_

1092 hdr <- fst <$> stringLiteral

1093 hdr <- fst <$> stringLiteral

1093 return [PDirective (DInclude cgn hdr)]

1094 return [PDirective (DInclude cgn hdr)]

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

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

1095 return [PDirective (DHide n)]

1096 return [PDirective (DHide n)]

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

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

1097 return [PDirective (DFreeze n)]

1098 return [PDirective (DFreeze n)]

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

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

1099 return [PDirective (DAccess acc)]

1100 return [PDirective (DAccess acc)]

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

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

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

1109 return [PDirective (DDynamicLibs libs)]

1110 return [PDirective (DDynamicLibs libs)]

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

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

1111− ty <- fnName

1112+ ty <- fst <$> fnName

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

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

1113 return [PDirective (DNameHint ty ns)]

1114 return [PDirective (DNameHint ty ns)]

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

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

1115− fn <- fnName

1116+ fn <- fst <$> fnName

1116− arg <- fnName

1117+ arg <- fst <$> fnName

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

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

1118 return [PDirective (DErrorHandlers fn arg ns) ]

1119 return [PDirective (DErrorHandlers fn arg ns) ]

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

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

1120 return [PDirective (DLanguage ext)]

1121 return [PDirective (DLanguage ext)]

1121 <|> do fc <- getFC

1122 <|> do fc <- getFC

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

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

1123− fn <- fnName

1124+ fn <- fst <$> fnName

1124− arg <- iName []

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

1125 return [PDirective (DUsed fc fn arg)]

1126 return [PDirective (DUsed fc fn arg)]

1126 <?> "directive"

1127 <?> "directive"

1127

1128

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

1156 provideTerm doc <|> providePostulate doc

1157 provideTerm doc <|> providePostulate doc

1157 <?> "type provider"

1158 <?> "type provider"

1158 where provideTerm doc =

1159 where provideTerm doc =

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

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

1160 fc <- getFC

1161 fc <- getFC

1161 reserved "with"

1162 reserved "with"

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

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

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

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

1164 providePostulate doc =

1165 providePostulate doc =

1165 do reserved "postulate"

1166 do reserved "postulate"

1166− n <- fnName

1167+ n <- fst <$> fnName

1167 fc <- getFC

1168 fc <- getFC

1168 reserved "with"

1169 reserved "with"

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

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

src/Idris/REPL.hs+1−1

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

1293process fn (MakeDoc s) =

1294 do istate <- getIState

1295 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

1297 parse n = Left n

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

1299 cd <- runIO $ getCurrentDirectory

src/Idris/REPLParser.hs+15−15

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

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

213

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

215−nameArg = genArg "name" P.name

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

216−fnNameArg = genArg "functionname" P.fnName

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

217

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

219strArg = genArg "string" (many anyChar)

220

221moduleArg :: (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)

223 where

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

225

226namespaceArg :: ([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)

228 where

229 toNS = splitOn "."

230

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

258 upd <- option False $ do

259 P.lchar '!'

260 return True

261− l <- fmap fst P.natural

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

262− n <- P.name;

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

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

264

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

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

327 let codegenOption :: P.IdrisParser Codegen

328 codegenOption = do

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

330− viaCodegen = do x <- P.identifier

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

331 return (Via (map toLower x))

332 bytecodeCodegen <|> viaCodegen

333

334 let hasOneArg = do

335 i <- get

336− f <- P.identifier

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

337 eof

338 return $ Right (Compile defaultCodegen f)

339

340 let hasTwoArgs = do

341 i <- get

342 codegen <- codegenOption

343− f <- P.identifier

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

344 eof

345 return $ Right (Compile codegen f)

346

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

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

351cmd_addproof name = do

352 n <- option Nothing $ do

353− x <- P.name

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

354 return (Just x)

355 eof

356 return (Right (AddProof n))

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

367 return (Right (NewDefn defn))

368

369cmd_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)

371

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

373cmd_loadto name = do

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

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

460cmd_proofsearch name = do

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

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

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

463− hints <- many P.fnName

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

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

465

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

467cmd_refine name = do

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

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

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

470− hint <- P.fnName

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

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

src/Pkg/PParser.hs+11−8

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

34 }

35 deriving Show

37+instance HasLastTokenSpan PParser where

38+ getLastTokenSpan = return Nothing

39+

37#if MIN_VERSION_base(4,8,0)

40#if MIN_VERSION_base(4,8,0)

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

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

39#else

42#else

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

51 Success x -> return x

54 Success x -> return x

53pPkg :: PParser PkgDesc

56pPkg :: PParser PkgDesc

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

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

55 st <- get

58 st <- get

56 put (st { pkgname = p })

59 put (st { pkgname = p })

57 some pClause

60 some pClause

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

68 else ( show exec )

71 else ( show exec )

69 ) })

72 ) })

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

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

71− main <- iName []

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

72 st <- get

75 st <- get

73 put (st { idris_main = main })

76 put (st { idris_main = main })

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

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

75− src <- identifier

78+ src <- fst <$> identifier

76 st <- get

79 st <- get

77 put (st { sourcedir = src })

80 put (st { sourcedir = src })

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

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

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

81 let args = pureArgParser (words opts)

84 let args = pureArgParser (words opts)

82 put (st { idris_opts = args })

85 put (st { idris_opts = args })

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

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

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

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

85 st <- get

88 st <- get

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

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

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

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

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

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

89 st <- get

92 st <- get

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

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

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

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

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

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

93 st <- get

96 st <- get

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

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

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

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

96− mk <- iName []

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

97 st <- get

100 st <- get

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

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

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

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

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

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

101 st <- get

104 st <- get

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

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

103

106