66ec833 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Minor memory usage improvements

* Don't store internal definitions if we're not starting a REPL, since they won't be used for interactive editing * Use a strict map instead * Clear original pattern definitions since they are only used for termination/coverage checking

commit66ec83311f32c4ebccb7d0f3eb3e85623e76b3ee authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 Jan 2014, 21:21 (13 years ago) parenta611deb

8 files changed+69−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+21 src/Idris/Core/CaseTree.hs+4−2 src/Idris/Core/DeepSeq.hs+15 src/Idris/Core/Evaluate.hs+5 src/Idris/Core/TT.hs+13−1 src/Idris/DeepSeq.hs−1 src/Idris/ElabDecls.hs+9−6 src/Idris/REPL.hs+2

src/Idris/AbsSyntax.hs+21

@@ -302,6 +302,27 @@ getInternalApp fp l = do i <- getIState

302302 Nothing -> return Placeholder

303303 -- TODO: What if it's not there?

304304

305+-- Pattern definitions are only used for coverage checking, so erase them

306+-- when we're done

307+clearOrigPats :: Idris ()

308+clearOrigPats = do i <- get

309+ let ps = idris_patdefs i

310+ let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps

311+ put (i { idris_patdefs = ps' })

312+

313+-- Erase types from Ps in the context (basically ending up with what's in

314+-- the .ibc, which is all we need after all the analysis is done)

315+clearPTypes :: Idris ()

316+clearPTypes = do i <- get

317+ let ctxt = tt_ctxt i

318+ put (i { tt_ctxt = mapDefCtxt pErase ctxt })

319+ where pErase (CaseOp c t tys orig tot cds)

320+ = CaseOp c t tys orig [] (pErase' cds)

321+ pErase x = x

322+ pErase' (CaseDefs _ (cs, c) _ rs)

323+ = let c' = (cs, fmap pEraseType c) in

324+ CaseDefs c' c' c' rs

325+

305326checkUndefined :: FC -> Name -> Idris ()

306327checkUndefined fc n

307328 = do i <- getContext

src/Idris/Core/CaseTree.hs+4−2

@@ -21,7 +21,8 @@ data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

2121 | ImpossibleCase -- ^ already checked to be impossible

2222 deriving (Eq, Ord, Functor)

2323{-!

24−deriving instance Binary SC

24+deriving instance Binary SC'

25+deriving instance NFData SC'

2526!-}

2627

2728type SC = SC' Term

@@ -33,7 +34,8 @@ data CaseAlt' t = ConCase Name Int [Name] !(SC' t)

3334 | DefaultCase !(SC' t)

3435 deriving (Show, Eq, Ord, Functor)

3536{-!

36−deriving instance Binary CaseAlt

37+deriving instance Binary CaseAlt'

38+deriving instance NFData CaseAlt'

3739!-}

3840

3941type CaseAlt = CaseAlt' Term

src/Idris/Core/DeepSeq.hs+15

@@ -1,6 +1,7 @@

11module Idris.Core.DeepSeq where

33import Idris.Core.TT

4+import Idris.Core.CaseTree

56import Control.DeepSeq

@@ -97,3 +98,17 @@ instance (NFData n) => NFData (TT n) where

9798 rnf Impossible = ()

9899 rnf (TType x1) = rnf x1 `seq` ()

99100

101+instance (NFData t) => NFData (SC' t) where

102+ rnf (Case x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

103+ rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

104+ rnf (STerm x1) = rnf x1 `seq` ()

105+ rnf (UnmatchedCase x1) = rnf x1 `seq` ()

106+ rnf ImpossibleCase = ()

107+

108+instance (NFData t) => NFData (CaseAlt' t) where

109+ rnf (ConCase x1 x2 x3 x4)

110+ = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()

111+ rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()

112+ rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()

113+ rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()

114+ rnf (DefaultCase x1) = rnf x1 `seq` ()

src/Idris/Core/Evaluate.hs+5

@@ -9,6 +9,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

12+ mapDefCtxt,

1213 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

1314 Value(..), Quote(..), initEval, uniqueNameCtxt) where

1415

@@ -696,6 +697,10 @@ data Context = MkContext {

696697-- | The initial empty context

697698initContext = MkContext [] 0 emptyContext

698699

700+mapDefCtxt :: (Def -> Def) -> Context -> Context

701+mapDefCtxt f (MkContext c t defs) = MkContext c t (mapCtxt f' defs)

702+ where f' (d, a, t, m) = f' (f d, a, t, m)

703+

699704-- | Get the definitions from a context

700705ctxtAlist :: Context -> [(Name, Def)]

701706ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

src/Idris/Core/TT.hs+13−1

@@ -23,7 +23,7 @@ module Idris.Core.TT where

2323import Control.Monad.State

2424import Control.Monad.Trans.Error (Error(..))

2525import Debug.Trace

26−import qualified Data.Map as Map

26+import qualified Data.Map.Strict as Map

2727import Data.Char

2828import Data.List

2929import Data.Vector.Unboxed (Vector)

@@ -314,6 +314,9 @@ showCG NErased = "_"

314314type Ctxt a = Map.Map Name (Map.Map Name a)

315315emptyContext = Map.empty

316316

317+mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b

318+mapCtxt = fmap . fmap

319+

317320tcname (UN ('@':_)) = True

318321tcname (NS n _) = tcname n

319322tcname (SN (InstanceN _ _)) = True

@@ -756,6 +759,15 @@ finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))

756759finalise (App f a) = App (finalise f) (finalise a)

757760finalise t = t

758761

762+-- Once we've finished checking everything about a term we no longer need

763+-- the type on the 'P' so erase it so save memory

764+

765+pEraseType :: TT n -> TT n

766+pEraseType (P nt t _) = P nt t Erased

767+pEraseType (App f a) = App (pEraseType f) (pEraseType a)

768+pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)

769+pEraseType t = t

770+

759771subst :: Eq n => n -> TT n -> TT n -> TT n

760772subst n v tm = instantiate v (pToV n tm)

761773

src/Idris/DeepSeq.hs−1

@@ -2,7 +2,6 @@ module Idris.DeepSeq(module Idris.DeepSeq, module Idris.Core.DeepSeq) where

33import Idris.Core.DeepSeq

44import Idris.Core.TT

5−import Idris.AbsSyntax

65import Idris.AbsSyntaxTree

87import Control.DeepSeq

src/Idris/ElabDecls.hs+9−6

@@ -91,8 +91,10 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

9191 let nty' = normalise ctxt [] nty

9292

9393 -- Add normalised type to internals

94− addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))

95− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))

94+ rep <- useREPL

95+ when rep $ do

96+ addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))

97+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))

9698

9799 let (t, _) = unApply (getRetTy nty')

98100 let corec = case t of

@@ -675,8 +677,7 @@ elabTransform info fc safe lhs_in rhs_in

675677 erun fc (build i info False [] (UN "transform") rhs)

676678 erun fc $ psolve lhs_tm

677679 tt <- get_term

678− let (tm, ds) = runState (collectDeferred Nothing tt) []

679− return (tm, ds))

680+ return (runState (collectDeferred Nothing tt) []))

680681 (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

681682 logLvl 3 ("Transform RHS " ++ show crhs_tm)

682683 when safe $ case converts ctxt [] clhs_tm crhs_tm of

@@ -1268,8 +1269,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

12681269

12691270 logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

12701271

1271− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

1272− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

1272+ rep <- useREPL

1273+ when rep $ do

1274+ addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

1275+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

12731276

12741277 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

12751278 -- Elaborate where block

src/Idris/REPL.hs+2

@@ -408,6 +408,7 @@ edit f orig

408408 , idris_colourTheme = idris_colourTheme i

409409 }

410410 loadInputs stdout [f]

411+ clearOrigPats

411412 iucheck

412413 return ()

413414 where getEditor env | Just ed <- lookup "EDITOR" env = ed

@@ -1220,6 +1221,7 @@ idrisMain opts =

12201221 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

12211222

12221223 when (runrepl && not idesl) $ do

1224+ clearOrigPats

12231225 initScript

12241226 startServer orig inputs

12251227 runInputT (replSettings (Just historyFile)) $ repl orig inputs