6042cfe · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+13−4

compare with master

unifiedsplit

@@ -96,14 +96,22 @@ addAutoImport fp = do i <- getIState

96 put (i { idris_options = opts { opt_autoImport =

97 fp : opt_autoImport opts } } )

98

99+addDefinedName :: Name -> Idris ()

100+addDefinedName n = do ist <- getIState

101+ putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }

102+

103+getDefinedNames :: Idris [Name]

104+getDefinedNames = do ist <- getIState

105+ return (S.toList (idris_inmodule ist))

106+

99addTT :: Term -> Idris (Maybe Term)

107addTT :: Term -> Idris (Maybe Term)

100−addTT t = do ist <- get

108+addTT t = do ist <- getIState

101 case M.lookup t (idris_ttstats ist) of

109 case M.lookup t (idris_ttstats ist) of

102 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)

110 Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)

103− put $ ist { idris_ttstats = tt' }

111+ putIState $ ist { idris_ttstats = tt' }

104 return Nothing

112 return Nothing

105 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)

113 Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)

106− put $ ist { idris_ttstats = tt' }

114+ putIState $ ist { idris_ttstats = tt' }

107 return (Just t')

115 return (Just t')

108

116

109dumpTT :: Idris ()

117dumpTT :: Idris ()

@@ -461,7 +469,8 @@ addIBC ibc@(IBCDef n)

461addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

469addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

462

470

463clearIBC :: Idris ()

471clearIBC :: Idris ()

464−clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

472+clearIBC = do i <- getIState; putIState $ i { ibc_write = [],

473+ idris_inmodule = S.empty }

465

474

466resetNameIdx :: Idris ()

475resetNameIdx :: Idris ()

467resetNameIdx = do i <- getIState

476resetNameIdx = do i <- getIState

src/Idris/AbsSyntaxTree.hs+2−1

@@ -262,6 +262,7 @@ data IState = IState {

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

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

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

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

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

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

266 }

267 }

267

268

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

352 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

353 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

354 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

355 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

355− emptyContext M.empty

356+ emptyContext S.empty M.empty

356

357

358

358-- | The monad for the main REPL - reading and processing files and updating

359-- | The monad for the main REPL - reading and processing files and updating

src/Idris/DeepSeq.hs+2−2

@@ -696,8 +696,8 @@ instance NFData IState where

696 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

697 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

698 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

699− x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74)

699+ x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75)

700 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

701 rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

702 rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

703− rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` ()

703+ rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` ()

src/Idris/Elab/Clause.hs+1

@@ -244,6 +244,7 @@ elabClauses info' fc opts n_in cs =

244 ctxt

245 setContext ctxt'

246 addIBC (IBCDef n)

247+ addDefinedName n

247 setTotality n tot

248 setTotality n tot

248 when (not reflect && PEGenerated `notElem` opts) $

249 when (not reflect && PEGenerated `notElem` opts) $

249 do totcheck (fc, n)

250 do totcheck (fc, n)

src/Idris/Elab/Type.hs+1

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

167 let usety = if norm then nty' else nty

168 ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]

169 addIBC (IBCDef n)

170+ addDefinedName n

170 let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds

171 let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True))) ds

171 addDeferred ds'

172 addDeferred ds'

172 setFlags n opts'

173 setFlags n opts'