193589f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Why nub a list when you can use a set.

Highlighting information was contained in an association list. Not only were there duplicates in the list, nubbing the list resulted in performance losses on proper sized code bases. We migrate the lists to sets and use `FC'` to ensure no false positives are returned when comparing to elements in the list. `FC'` is `FC` but with equality. Anecdotal tests show good performance improvements wrt to code highlighting.

commit193589fa0988bdd49ad5b0b04781a7998962e29b authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateTue 26 Jun 2018, 11:04 (8 years ago) parentdbe521f

14 files changed+61−49

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+6−6 src/Idris/Core/TT.hs+3−3 src/Idris/Directives.hs+7−5 src/Idris/Elab/Clause.hs+2−1 src/Idris/Elab/Data.hs+4−3 src/Idris/Elab/Interface.hs+6−5 src/Idris/Elab/Record.hs+5−4 src/Idris/Elab/Term.hs+1−1 src/Idris/Elab/Type.hs+2−2 src/Idris/Elab/Value.hs+1 src/Idris/ElabDecls.hs+3−1 src/Idris/Output.hs+13−12 src/Idris/Parser.hs+6−5 src/Idris/Parser/Helpers.hs+2−1

src/Idris/AbsSyntaxTree.hs+6−6

@@ -302,8 +302,8 @@ data IState = IState {

302302

303303 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

304304 , idris_exports :: [Name] -- ^ Functions with ExportList

305− , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output

306− , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser

305+ , idris_highlightedRegions :: S.Set (FC', OutputAnnotation) -- ^ Highlighting information to output

306+ , idris_parserHighlights :: S.Set (FC', OutputAnnotation) -- ^ Highlighting information from the parser

307307 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation

308308 , idris_inmodule :: S.Set Name -- ^ Names defined in current module

309309 , idris_ttstats :: M.Map Term (Int, Term)

@@ -411,7 +411,7 @@ idrisInit = IState initContext S.empty []

411411 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

412412 [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

413413 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

414− AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []

414+ AutomaticWidth S.empty S.empty [] [] [] M.empty [] S.empty S.empty

415415 emptyContext S.empty M.empty emptyContext initialInteractiveOpts

416416

417417

@@ -710,19 +710,19 @@ data EState = EState {

710710 case_decls :: [(Name, PDecl)]

711711 , delayed_elab :: [(Int, Elab' EState ())]

712712 , new_tyDecls :: [RDeclInstructions]

713− , highlighting :: [(FC, OutputAnnotation)]

713+ , highlighting :: S.Set (FC', OutputAnnotation)

714714 , auto_binds :: [Name] -- ^ names bound as auto implicits

715715 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)

716716 }

717717

718718initEState :: EState

719−initEState = EState [] [] [] [] [] []

719+initEState = EState [] [] [] S.empty [] []

720720

721721type ElabD a = Elab' EState a

722722

723723highlightSource :: FC -> OutputAnnotation -> ElabD ()

724724highlightSource fc annot =

725− updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })

725+ updateAux (\aux -> aux { highlighting = S.insert (FC' fc, annot) (highlighting aux) })

726726

727727-- | One clause of a top-level definition. Term arguments to constructors are:

728728--

src/Idris/Core/TT.hs+3−3

@@ -197,10 +197,10 @@ instance Show FC where

197197 show (FileFC f) = f

198198

199199-- | Output annotation for pretty-printed name - decides colour

200−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Generic)

200+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Ord, Generic)

201201

202202-- | Text formatting output

203−data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Generic)

203+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Ord, Generic)

204204

205205-- | Output annotations for pretty-printing

206206data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

@@ -227,7 +227,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

227227 | AnnQuasiquote

228228 | AnnAntiquote

229229 | AnnSyntax String -- ^ type of syntax element: backslash or braces etc.

230− deriving (Show, Eq, Generic)

230+ deriving (Show, Eq, Generic, Ord)

231231

232232-- | Used for error reflection

233233data ErrorReportPart = TextPart String

src/Idris/Directives.hs+7−5

@@ -13,6 +13,8 @@ import Idris.Core.TT

1313import Idris.Imports

1414import Idris.Output (sendHighlighting)

1515

16+import qualified Data.Set as S

17+

1618import Util.DynamicLinker

1719

1820-- | Run the action corresponding to a directive

@@ -81,7 +83,7 @@ directiveAction (DNameHint ty tyFC ns) = do

8183 ty' <- disambiguate ty

8284 mapM_ (addNameHint ty' . fst) ns

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

84− sendHighlighting $ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns

86+ sendHighlighting $ S.fromList $ [(FC' tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (FC' fc, AnnBoundName n False)) ns

8587

8688directiveAction (DErrorHandlers fn nfc arg afc ns) = do

8789 fn' <- disambiguate fn

@@ -90,10 +92,10 @@ directiveAction (DErrorHandlers fn nfc arg afc ns) = do

9092 return (n', fc)) ns

9193 addFunctionErrorHandlers fn' arg (map fst ns')

9294 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'

93− sendHighlighting $

94− [ (nfc, AnnName fn' Nothing Nothing Nothing)

95− , (afc, AnnBoundName arg False)

96− ] ++ map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'

95+ sendHighlighting $ S.fromList $

96+ [ (FC' nfc, AnnName fn' Nothing Nothing Nothing)

97+ , (FC' afc, AnnBoundName arg False)

98+ ] ++ map (\(n, fc) -> (FC' fc, AnnName n Nothing Nothing Nothing)) ns'

9799

98100directiveAction (DLanguage ext) = addLangExt ext

99101

src/Idris/Elab/Clause.hs+2−1

@@ -44,6 +44,7 @@ import qualified Control.Monad.State.Lazy as LState

4444import Control.Monad.State.Strict as State

4545import Data.List

4646import Data.Maybe

47+import qualified Data.Set as S

4748import Data.Word

4849import Debug.Trace

4950import Numeric

@@ -1028,7 +1029,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10281029 Just (n, nfc) -> Just (uniqueName n (map fst bargs))

10291030

10301031 -- Highlight explicit proofs

1031− sendHighlighting [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

1032+ sendHighlighting $ S.fromList [(FC' fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

10321033

10331034 logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++

10341035 " depends on " ++ show pdeps ++ " from " ++ show pvars)

src/Idris/Elab/Data.hs+4−3

@@ -37,6 +37,7 @@ import Data.Char (isLetter, toLower)

3737import Data.List

3838import qualified Data.Map as Map

3939import Data.Maybe

40+import qualified Data.Set as S

4041import qualified Data.Text as T

4142

4243warnLC :: FC -> Name -> Idris ()

@@ -53,7 +54,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

5354

5455 addIBC (IBCDef n)

5556 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

56− sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

57+ sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]

5758

5859elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

5960 = do let codata = Codata `elem` opts

@@ -118,9 +119,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

118119 when (n /= sUN "=") $

119120 elabRewriteLemma info n cty

120121 -- Emit highlighting info

121− sendHighlighting $ [(nfc, AnnName n Nothing Nothing Nothing)] ++

122+ sendHighlighting $ S.fromList $ [(FC' nfc, AnnName n Nothing Nothing Nothing)] ++

122123 map (\(_, _, n, nfc, _, _, _) ->

123− (nfc, AnnName n Nothing Nothing Nothing))

124+ (FC' nfc, AnnName n Nothing Nothing Nothing))

124125 dcons

125126 where

126127 checkDefinedAs fc n t i

src/Idris/Elab/Interface.hs+6−5

@@ -26,6 +26,7 @@ import Control.Monad

2626import Data.Generics.Uniplate.Data (transform)

2727import Data.List

2828import Data.Maybe

29+import qualified Data.Set as S

2930

3031data MArgTy = IA Name | EA Name | CA deriving Show

3132

@@ -167,11 +168,11 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

167168 mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

168169 addIBC (IBCInterface tn)

169170

170− sendHighlighting $

171− [(tnfc, AnnName tn Nothing Nothing Nothing)] ++

172− [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

173− [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

174− maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

171+ sendHighlighting $ S.fromList $

172+ [(FC' tnfc, AnnName tn Nothing Nothing Nothing)] ++

173+ [(FC' pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

174+ [(FC' fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

175+ maybe [] (\(conN, conNFC) -> [(FC' conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

175176

176177 where

177178 info = info_in { noCaseLift = tn : noCaseLift info_in }

src/Idris/Elab/Record.hs+5−4

@@ -20,6 +20,7 @@ import Idris.Output (sendHighlighting)

2020import Control.Monad

2121import Data.List

2222import Data.Maybe

23+import qualified Data.Set as S

2324

2425-- | Elaborate a record declaration

2526elabRecord :: ElabInfo

@@ -66,10 +67,10 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc

6667 logElab 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

6768 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

6869

69− sendHighlighting $

70− [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

71− maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

72− [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

70+ sendHighlighting $ S.fromList $

71+ [(FC' nfc, AnnName tyn Nothing Nothing Nothing)] ++

72+ maybe [] (\(_, cnfc) -> [(FC' cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

73+ [(FC' ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

7374

7475 where

7576 -- | Generates a type constructor.

src/Idris/Elab/Term.hs+1−1

@@ -56,7 +56,7 @@ data ElabResult = ElabResult {

5656 -- | Meta-info about the new type declarations

5757 , resultTyDecls :: [RDeclInstructions]

5858 -- | Saved highlights from elaboration

59− , resultHighlighting :: [(FC, OutputAnnotation)]

59+ , resultHighlighting :: S.Set (FC', OutputAnnotation)

6060 -- | The new global name counter

6161 , resultName :: Int

6262 }

src/Idris/Elab/Type.hs+2−2

@@ -205,7 +205,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

205205 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

206206 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

207207 -- Send highlighting information about the name being declared

208− sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

208+ sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]

209209 -- if it's an export list type, make a note of it

210210 case (unApply usety) of

211211 (P _ ut _, _)

@@ -238,7 +238,7 @@ elabPostulate info syn doc fc nfc opts n ty = do

238238 elabType info syn doc [] fc opts n NoFC ty

239239 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState

240240 addIBC (IBCPostulate n)

241− sendHighlighting [(nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]

241+ sendHighlighting $ S.fromList [(FC' nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]

242242

243243 -- remove it from the deferred definitions list

244244 solveDeferred fc n

src/Idris/Elab/Value.hs+1

@@ -26,6 +26,7 @@ import Prelude hiding (id, (.))

2626

2727import Control.Category

2828import Data.Char (toLower)

29+import qualified Data.Set as S ()

2930import qualified Data.Traversable as Traversable

3031

3132-- | Elaborate a value, returning any new bindings created (this will only

src/Idris/ElabDecls.hs+3−1

@@ -41,8 +41,10 @@ import Control.Category

4141import Control.Monad

4242import Control.Monad.State.Strict as State

4343import Data.Maybe

44+import qualified Data.Set as S

4445import qualified Data.Text as T

4546

47+

4648-- | Top level elaborator info, supporting recursive elaboration

4749recinfo :: FC -> ElabInfo

4850recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 [] id elabDecl'

@@ -260,7 +262,7 @@ elabDecl' what info (POpenInterfaces f ns ds)

260262elabDecl' what info (PNamespace n nfc ps) =

261263 do mapM_ (elabDecl' what ninfo) ps

262264 let ns = reverse (map T.pack newNS)

263− sendHighlighting [(nfc, AnnNamespace ns Nothing)]

265+ sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns Nothing)]

264266 where

265267 newNS = n : namespace info

266268 ninfo = info { namespace = newNS }

src/Idris/Output.hs+13−12

@@ -38,8 +38,9 @@ import Prelude hiding ((<$>))

3838

3939import Control.Arrow (first)

4040import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

41−import Data.List (intersperse, nub, nubBy)

41+import Data.List (intersperse, nub)

4242import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)

43+import qualified Data.Set as S

4344import System.Console.Haskeline.MonadException (MonadException(controlIO),

4445 RunIO(RunIO))

4546import System.FilePath (replaceExtension)

@@ -77,9 +78,12 @@ formatMessage w = do

7778 maybeSource <- case messageSource w of

7879 Just src -> pure (Just src)

7980 Nothing -> readSource fc

80− let maybeFormattedSource = maybeSource >>= layoutSource fc (idris_highlightedRegions i)

81+ let maybeFormattedSource = maybeSource >>= layoutSource fc (regions (idris_highlightedRegions i))

8182 return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)

8283 where

84+ regions :: S.Set (FC', OutputAnnotation) -> [(FC, OutputAnnotation)]

85+ regions rs = map (\(FC' a,b) -> (a, b)) $ S.toList rs

86+

8387 fc :: FC

8488 fc = messageExtent w

8589

@@ -359,23 +363,21 @@ prettyDocumentedIst ist (name, ty, docs) =

359363sendParserHighlighting :: Idris ()

360364sendParserHighlighting =

361365 do ist <- getIState

362− let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist

366+ let hs = idris_parserHighlights ist

363367 sendHighlighting hs

364368 ist <- getIState

365− putIState ist {idris_parserHighlights = []}

366− where wrap (fc, a) = (FC' fc, a)

367− unwrap (fc', a) = (unwrapFC fc', a)

369+ putIState ist {idris_parserHighlights = S.empty}

368370

369−sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

371+sendHighlighting :: S.Set (FC', OutputAnnotation) -> Idris ()

370372sendHighlighting highlights =

371373 do ist <- getIState

372374 case idris_outputmode ist of

373375 RawOutput _ -> updateIState $

374376 \ist -> ist { idris_highlightedRegions =

375− nubBy canNub $ highlights ++ idris_highlightedRegions ist }

377+ S.union highlights (idris_highlightedRegions ist) }

376378 IdeMode n h ->

377379 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)

378− | (fc, annot) <- nubBy canNub highlights, fullFC fc

380+ | (FC' fc, annot) <- S.toList highlights, fullFC fc

379381 ] in

380382 case fancier of

381383 [] -> return ()

@@ -386,14 +388,13 @@ sendHighlighting highlights =

386388

387389 where fullFC (FC _ _ _) = True

388390 fullFC _ = False

389− canNub (fA,x) (fB,y) = show fA == show fB && x == y

390391

391392-- | Write the highlighting information to a file, for use in external tools

392393-- or in editors that don't support the IDE protocol

393394writeHighlights :: FilePath -> Idris ()

394395writeHighlights f =

395396 do ist <- getIState

396− let hs = reverse $ idris_highlightedRegions ist

397+ let hs = reverse $ map (\(FC' a, b) -> (a,b)) $ S.toList (idris_highlightedRegions ist)

397398 let hfile = replaceExtension f "idh"

398399 let annots = toSExp [ (fc, fancifyAnnots ist False annot)

399400 | (fc@(FC _ _ _), annot) <- hs

@@ -401,7 +402,7 @@ writeHighlights f =

401402 runIO $ writeFile hfile $ sExpToString annots

402403

403404clearHighlights :: Idris ()

404−clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }

405+clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = S.empty }

405406

406407renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

407408renderExternal fmt width doc

src/Idris/Parser.hs+6−5

@@ -53,6 +53,7 @@ import qualified Data.List.Split as Spl

5353import qualified Data.Map as M

5454import Data.Maybe

5555import Data.Ord

56+import qualified Data.Set as S

5657import qualified Data.Text as T

5758import qualified System.Directory as Dir (makeAbsolute)

5859import System.FilePath

@@ -1491,7 +1492,7 @@ parseImports fname input

14911492 Right (x, annots, i) ->

14921493 do putIState i

14931494 fname' <- runIO $ Dir.makeAbsolute fname

1494− sendHighlighting $ addPath annots fname'

1495+ sendHighlighting $ S.fromList $ addPath annots fname'

14951496 return x

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

14971498 [ImportInfo],

@@ -1512,11 +1513,11 @@ parseImports fname input

15121513 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

15131514 return ((mdoc, mname, ps, mrk'), annots, i)

15141515

1515− addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

1516+ addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC', OutputAnnotation)]

15161517 addPath [] _ = []

15171518 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

1518− (fc, AnnNamespace ns (Just path)) : addPath annots path

1519− addPath (annot:annots) path = annot : addPath annots path

1519+ (FC' fc, AnnNamespace ns (Just path)) : addPath annots path

1520+ addPath ((fc,annot):annots) path = (FC' fc, annot) : addPath annots path

15201521

15211522 shebang :: IdrisParser ()

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

@@ -1664,7 +1665,7 @@ loadSource lidr f toline

16641665 srcFnAbs <- case srcFn of

16651666 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)

16661667 Nothing -> return Nothing

1667− sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])

1668+ sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])

16681669 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

16691670 reportParserWarnings

16701671 sendParserHighlighting

src/Idris/Parser/Helpers.hs+2−1

@@ -89,6 +89,7 @@ import Data.List

8989import qualified Data.List.NonEmpty as NonEmpty

9090import qualified Data.Map as M

9191import Data.Maybe

92+import qualified Data.Set as S

9293import qualified Data.Text as T

9394import Text.Megaparsec ((<?>))

9495import qualified Text.Megaparsec as P

@@ -112,7 +113,7 @@ token p = trackExtent p <* whiteSpace

112113highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a

113114highlight annot p = do

114115 (result, fc) <- withExtent p

115− modify $ \ist -> ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist }

116+ modify $ \ist -> ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }

116117 return result

117118

118119-- | Parse a reserved identfier, highlighting it as a keyword