a675cdb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4494 from jfdm/fix-nubbing

Why nub a list when you can use a set.

commita675cdb9a712c05486a17d6139e5b135b5924873 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateTue 26 Jun 2018, 12:50 (8 years ago) parentdbe521f 193589f

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