8b252bd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2442 from david-christiansen/parser-highlights

More parser-driven highlighting

commit8b252bdc520007f8aeb8a193f08c0338cdabb0c2 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 17 Jul 2015, 20:53 (11 years ago) parent8addb63 9ba7407

5 files changed+72−42

compare with master

unifiedsplit

CHANGELOG+3−1 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Directives.hs+19−9 src/Idris/ParseExpr.hs+41−23 src/Idris/Parser.hs+7−7

CHANGELOG+3−1

@@ -17,7 +17,9 @@ New in 0.9.19:

1717* New command-line option --highlight that causes Idris to save highlighting

1818 information when successfully type checking. The information is in the same

1919 format sent by the IDE mode, and is saved in a file with the extension ".idh".

20−* Use predicates instead of boolean equality proofs as preconditions

20+* Highlighting information is saved by the parser as well, allowing it to highlight

21+ keywords like "case", "of", "let", and "do"

22+* Use predicates instead of boolean equality proofs as preconditions

2123 on List functions

2224* More flexible 'case' construct, allowing each branch to target different

2325 types, provided that the case analysis does not affect the form of any

src/Idris/AbsSyntaxTree.hs+2−2

@@ -678,8 +678,8 @@ data Directive = DLib Codegen String |

678678 DDefault Bool |

679679 DLogging Integer |

680680 DDynamicLibs [String] |

681− DNameHint Name [Name] |

682− DErrorHandlers Name Name [Name] |

681+ DNameHint Name FC [(Name, FC)] |

682+ DErrorHandlers Name FC Name FC [(Name, FC)] |

683683 DLanguage LanguageExt |

684684 DUsed FC Name Name

685685

src/Idris/Directives.hs+19−9

@@ -4,6 +4,7 @@ module Idris.Directives(directiveAction) where

44import Idris.AbsSyntax

55import Idris.ASTUtils

66import Idris.Imports

7+import Idris.Output (sendHighlighting)

89import Idris.Core.Evaluate

910import Idris.Core.TT

@@ -43,15 +44,24 @@ directiveAction (DDynamicLibs libs) = do added <- addDyLib libs

4344 Left lib -> addIBC (IBCDyLib (lib_name lib))

4445 Right msg -> fail $ msg

4546

46−directiveAction (DNameHint ty ns) = do ty' <- disambiguate ty

47− mapM_ (addNameHint ty') ns

48− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns

49−

50−directiveAction (DErrorHandlers fn arg ns) = do fn' <- disambiguate fn

51− ns' <- mapM disambiguate ns

52− addFunctionErrorHandlers fn' arg ns'

53− mapM_ (addIBC .

54− IBCFunctionErrorHandler fn' arg) ns'

47+directiveAction (DNameHint ty tyFC ns) = do ty' <- disambiguate ty

48+ mapM_ (addNameHint ty' . fst) ns

49+ mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns

50+ sendHighlighting $

51+ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++

52+ map (\(n, fc) -> (fc, AnnBoundName n False)) ns

53+

54+directiveAction (DErrorHandlers fn nfc arg afc ns) =

55+ do fn' <- disambiguate fn

56+ ns' <- mapM (\(n, fc) -> do n' <- disambiguate n

57+ return (n', fc)) ns

58+ addFunctionErrorHandlers fn' arg (map fst ns')

59+ mapM_ (addIBC .

60+ IBCFunctionErrorHandler fn' arg . fst) ns'

61+ sendHighlighting $

62+ [(nfc, AnnName fn' Nothing Nothing Nothing),

63+ (afc, AnnBoundName arg False)] ++

64+ map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'

5565

5666directiveAction (DLanguage ext) = addLangExt ext

5767

src/Idris/ParseExpr.hs+41−23

@@ -256,7 +256,9 @@ Impossible ::= 'impossible'

256256@

257257-}

258258impossible :: IdrisParser PTerm

259−impossible = PImpossible <$ reserved "impossible"

259+impossible = do fc <- reservedFC "impossible"

260+ highlightP fc AnnKeyword

261+ return PImpossible

260262

261263{- | Parses a case expression

262264@

@@ -265,9 +267,11 @@ CaseExpr ::=

265267@

266268-}

267269caseExpr :: SyntaxInfo -> IdrisParser PTerm

268−caseExpr syn = do reserved "case"; fc <- getFC

269− scr <- expr syn; reserved "of";

270+caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC

271+ scr <- expr syn; kw2 <- reservedFC "of";

270272 opts <- indentedBlock1 (caseOption syn)

273+ highlightP kw1 AnnKeyword

274+ highlightP kw2 AnnKeyword

271275 return (PCase fc scr opts)

272276 <?> "case expression"

273277

@@ -292,8 +296,9 @@ ProofExpr ::=

292296@

293297-}

294298proofExpr :: SyntaxInfo -> IdrisParser PTerm

295−proofExpr syn = do reserved "proof"

299+proofExpr syn = do kw <- reservedFC "proof"

296300 ts <- indentedBlock1 (tactic syn)

301+ highlightP kw AnnKeyword

297302 return $ PProof ts

298303 <?> "proof block"

299304

@@ -305,8 +310,9 @@ TacticsExpr :=

305310@

306311-}

307312tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

308−tacticsExpr syn = do reserved "tactics"

313+tacticsExpr syn = do kw <- reservedFC "tactics"

309314 ts <- indentedBlock1 (tactic syn)

315+ highlightP kw AnnKeyword

310316 return $ PTactics ts

311317 <?> "tactics block"

312318

@@ -508,8 +514,9 @@ UnifyLog ::=

508514 ;

509515-}

510516unifyLog :: SyntaxInfo -> IdrisParser PTerm

511−unifyLog syn = do try (lchar '%' *> reserved "unifyLog")

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

512518 tm <- simpleExpr syn

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

513520 return (PUnifyLog tm)

514521 <?> "unification log expression"

515522

@@ -519,10 +526,10 @@ RunTactics ::=

519526 ;

520527-}

521528runElab :: SyntaxInfo -> IdrisParser PTerm

522−runElab syn = do try (lchar '%' *> reserved "runElab")

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

523530 fc <- getFC

524531 tm <- simpleExpr syn

525− i <- get

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

526533 return $ PRunElab fc tm (syn_namespace syn)

527534 <?> "new-style tactics expression"

528535

@@ -532,11 +539,12 @@ Disamb ::=

532539 ;

533540-}

534541disamb :: SyntaxInfo -> IdrisParser PTerm

535−disamb syn = do reserved "with";

542+disamb syn = do kw <- reservedFC "with"

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

537544 tm <- expr' syn

545+ highlightP kw AnnKeyword

538546 return (PDisamb (map tons ns) tm)

539− <?> "unification log expression"

547+ <?> "namespace disambiguation expression"

540548 where tons (NS n s) = txt (show n) : s

541549 tons n = [txt (show n)]

542550{- | Parses a no implicits expression

@@ -715,12 +723,13 @@ FieldType ::=

715723-}

716724recordType :: SyntaxInfo -> IdrisParser PTerm

717725recordType syn =

718− do reserved "record"

726+ do kw <- reservedFC "record"

719727 lchar '{'

720728 fgs <- fieldGetOrSet

721729 lchar '}'

722730 fc <- getFC

723731 rec <- optional (simpleExpr syn)

732+ highlightP kw AnnKeyword

724733 case fgs of

725734 Left fields ->

726735 case rec of

@@ -842,11 +851,13 @@ RewriteTerm ::=

842851@

843852-}

844853rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

845−rewriteTerm syn = do reserved "rewrite"

854+rewriteTerm syn = do kw <- reservedFC "rewrite"

846855 fc <- getFC

847856 prf <- expr syn

848857 giving <- optional (do symbol "==>"; expr' syn)

849− reserved "in"; sc <- expr syn

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

859+ highlightP kw AnnKeyword

860+ highlightP kw' AnnKeyword

850861 return (PRewrite fc

851862 (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

852863 giving)

@@ -864,9 +875,10 @@ TypeSig' ::=

864875@

865876 -}

866877let_ :: SyntaxInfo -> IdrisParser PTerm

867−let_ syn = try (do reserved "let"

878+let_ syn = try (do kw <- reservedFC "let"

868879 ls <- indentedBlock (let_binding syn)

869− reserved "in"; sc <- expr syn

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

881+ highlightP kw AnnKeyword; highlightP kw' AnnKeyword

870882 return (buildLets ls sc))

871883 <?> "let binding"

872884 where buildLets [] sc = sc

@@ -911,12 +923,13 @@ QuoteGoal ::=

911923@

912924 -}

913925quoteGoal :: SyntaxInfo -> IdrisParser PTerm

914−quoteGoal syn = do reserved "quoteGoal"; n <- fst <$> name;

915− reserved "by"

926+quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;

927+ kw2 <- reservedFC "by"

916928 r <- expr syn

917− reserved "in"

929+ kw3 <- reservedFC "in"

918930 fc <- getFC

919931 sc <- expr syn

932+ mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]

920933 return (PGoal fc r n sc)

921934 <?> "quote goal expression"

922935

@@ -948,17 +961,18 @@ explicitPi opts st syn

948961 return (bindList (PPi binder) xt sc)

949962

950963autoImplicit opts st syn

951− = do reserved "auto"

964+ = do kw <- reservedFC "auto"

952965 when (st == Static) $ fail "auto implicits can not be static"

953966 xt <- typeDeclList syn

954967 lchar '}'

955968 symbol "->"

956969 sc <- expr syn

970+ highlightP kw AnnKeyword

957971 return (bindList (PPi

958972 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)

959973

960974defaultImplicit opts st syn = do

961− reserved "default"

975+ kw <- reservedFC "default"

962976 when (st == Static) $ fail "default implicits can not be static"

963977 ist <- get

964978 script' <- simpleExpr syn

@@ -967,6 +981,7 @@ defaultImplicit opts st syn = do

967981 lchar '}'

968982 symbol "->"

969983 sc <- expr syn

984+ highlightP kw AnnKeyword

970985 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

971986

972987normalImplicit opts st syn = do

@@ -1159,8 +1174,9 @@ DoBlock ::=

11591174 -}

11601175doBlock :: SyntaxInfo -> IdrisParser PTerm

11611176doBlock syn

1162− = do reserved "do"

1177+ = do kw <- reservedFC "do"

11631178 ds <- indentedBlock1 (do_ syn)

1179+ highlightP kw AnnKeyword

11641180 return (PDoBlock ds)

11651181 <?> "do block"

11661182

@@ -1177,19 +1193,21 @@ Do ::=

11771193-}

11781194do_ :: SyntaxInfo -> IdrisParser PDo

11791195do_ syn

1180− = try (do reserved "let"

1196+ = try (do kw <- reservedFC "let"

11811197 (i, ifc) <- name

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

11831199 expr' syn)

11841200 reservedOp "="

11851201 fc <- getFC

11861202 e <- expr syn

1203+ highlightP kw AnnKeyword

11871204 return (DoLet fc i ifc ty e))

1188− <|> try (do reserved "let"

1205+ <|> try (do kw <- reservedFC "let"

11891206 i <- expr' syn

11901207 reservedOp "="

11911208 fc <- getFC

11921209 sc <- expr syn

1210+ highlightP kw AnnKeyword

11931211 return (DoLetP fc i sc))

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

11951213 symbol "<-"

src/Idris/Parser.hs+7−7

@@ -1146,14 +1146,14 @@ directive syn = do try (lchar '%' *> reserved "lib")

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

11471147 return [PDirective (DDynamicLibs libs)]

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

1149− ty <- fst <$> fnName

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

1151− return [PDirective (DNameHint ty ns)]

1149+ (ty, tyFC) <- fnName

1150+ ns <- sepBy1 name (lchar ',')

1151+ return [PDirective (DNameHint ty tyFC ns)]

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

1153− fn <- fst <$> fnName

1154− arg <- fst <$> fnName

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

1156− return [PDirective (DErrorHandlers fn arg ns) ]

1153+ (fn, nfc) <- fnName

1154+ (arg, afc) <- fnName

1155+ ns <- sepBy1 name (lchar ',')

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

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

11581158 return [PDirective (DLanguage ext)]

11591159 <|> do fc <- getFC