be33df4 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+19

compare with master

unifiedsplit

@@ -96,6 +96,25 @@ addAutoImport fp = do i <- getIState

96 put (i { idris_options = opts { opt_autoImport =

97 fp : opt_autoImport opts } } )

98

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

100+addTT t = do ist <- get

101+ case M.lookup t (idris_ttstats ist) of

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

103+ put $ ist { idris_ttstats = tt' }

104+ return Nothing

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

106+ put $ ist { idris_ttstats = tt' }

107+ return (Just t')

108+

109+dumpTT :: Idris ()

110+dumpTT = do ist <- get

111+ let sts = sortBy count (M.toList (idris_ttstats ist))

112+ mapM_ dump sts

113+ return ()

114+ where

115+ count (_,x) (_,y) = compare y x

116+ dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)

117+

99addHdr :: Codegen -> String -> Idris ()

118addHdr :: Codegen -> String -> Idris ()

100addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

119addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

101

120

src/Idris/AbsSyntaxTree.hs+4−2

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

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

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

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

265− idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation

265+ idris_deprecated :: Ctxt String, -- ^ Deprecated names and explanation

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

266 }

267 }

267

268

268-- Required for parsers library, and therefore trifecta

269-- Required for parsers library, and therefore trifecta

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

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

354 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

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

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

356− emptyContext

357+ emptyContext M.empty

358+

357

359

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

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

359-- global state (hence the IO inner monad).

361-- global state (hence the IO inner monad).

src/Idris/DeepSeq.hs+1−1

@@ -696,7 +696,7 @@ 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`

src/Idris/IBC.hs+21−11

@@ -120,6 +120,7 @@ loadIBC reexport fp

120 ++ "Please clean and rebuild it."

121 Right archive -> do process reexport archive fp

122 addImported reexport fp

123+-- dumpTT

123

124

124-- | Load an entire package from its index file

125-- | Load an entire package from its index file

125loadPkgIndex :: String -> Idris ()

126loadPkgIndex :: String -> Idris ()

@@ -562,19 +563,28 @@ pDefs reexp ds

562 updateAlt (DefaultCase t) = do t' <- updateSC t

563 updateAlt (DefaultCase t) = do t' <- updateSC t

563 return (DefaultCase t')

564 return (DefaultCase t')

564

565

566+ -- We get a lot of repetition in sub terms and can save a fair chunk

567+ -- of memory if we make sure they're shared. addTT looks for a term

568+ -- and returns it if it exists already, while also keeping stats of

569+ -- how many times a subterm is repeated.

570+ update t = do tm <- addTT t

571+ case tm of

572+ Nothing -> update' t

573+ Just t' -> return t'

574+

565− update (P t n ty) = do n' <- getSymbol n

575+ update' (P t n ty) = do n' <- getSymbol n

566− return $ P t n' ty

576+ return $ P t n' ty

567− update (App s f a) = liftM2 (App s) (update f) (update a)

577+ update' (App s f a) = liftM2 (App s) (update' f) (update' a)

568− update (Bind n b sc) = do b' <- updateB b

578+ update' (Bind n b sc) = do b' <- updateB b

569− sc' <- update sc

579+ sc' <- update sc

570− return $ Bind n b' sc'

580+ return $ Bind n b' sc'

571 where

581 where

572− updateB (Let t v) = liftM2 Let (update t) (update v)

582+ updateB (Let t v) = liftM2 Let (update' t) (update' v)

573− updateB b = do ty' <- update (binderTy b)

583+ updateB b = do ty' <- update' (binderTy b)

574 return (b { binderTy = ty' })

584 return (b { binderTy = ty' })

575− update (Proj t i) = do t' <- update t

585+ update' (Proj t i) = do t' <- update' t

576− return $ Proj t' i

586+ return $ Proj t' i

577− update t = return t

587+ update' t = return t

578

588

579pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()

589pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()

580pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds

590pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds

src/Idris/Parser.hs+10−1

@@ -1491,14 +1491,23 @@ parseImports fname input

1491 [(FC, OutputAnnotation)], IState)

1492 imports = do whiteSpace

1493 (mdoc, mname, annots) <- moduleHeader

1494− ps <- many import_

1494+ ps_exp <- many import_

1495 mrk <- mark

1496 isEof <- lookAheadMatches eof

1497 let mrk' = if isEof

1498 then Nothing

1499 else Just mrk

1500 i <- get

1501+ -- add Builtins and Prelude, unless options say

1502+ -- not to

1503+ let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

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

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

1505+

1506+ imp m = ImportInfo False (toPath m)

1507+ Nothing [] NoFC NoFC

1508+ ns = Spl.splitOn "."

1509+ toPath = foldl1' (</>) . ns

1510+

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

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

1503 addPath [] _ = []

1512 addPath [] _ = []

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

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

src/Idris/REPL.hs+1−2

@@ -1733,7 +1733,6 @@ idrisMain opts =

1733 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

1734 addAutoImport "Prelude"

1735 return ()

1736−

1737 when (runrepl && not idesl) initScript

1736 when (runrepl && not idesl) initScript

1738

1737

1739 nobanner <- getNoBanner

1738 nobanner <- getNoBanner

@@ -1794,7 +1793,7 @@ idrisMain opts =

1794 when (runrepl && not idesl) $ do

1793 when (runrepl && not idesl) $ do

1795-- clearOrigPats

1794-- clearOrigPats

1796 startServer port orig mods

1795 startServer port orig mods

1797− runInputT (replSettings (Just historyFile)) $ repl orig mods efile

1796+ runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile

1798 let idesock = IdemodeSocket `elem` opts

1797 let idesock = IdemodeSocket `elem` opts

1799 when (idesl) $ idemodeStart idesock orig inputs

1798 when (idesl) $ idemodeStart idesock orig inputs

1800 ok <- noErrors

1799 ok <- noErrors