a611deb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix memory leak

a611debEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+12−7

compare with master

unifiedsplit

@@ -238,14 +238,19 @@ resetNameIdx :: Idris ()

238resetNameIdx = do i <- getIState

239 put (i { idris_nameIdx = (0, emptyContext) })

240

241+-- Used to preserve sharing of names

241−addNameIdx :: Name -> Idris Int

242+addNameIdx :: Name -> Idris (Int, Name)

242addNameIdx n = do i <- getIState

243addNameIdx n = do i <- getIState

244+ let (i', x) = addNameIdx' i n

245+ return x

246+

247+addNameIdx' :: IState -> Name -> (IState, (Int, Name))

248+addNameIdx' i n

243− let idxs = snd (idris_nameIdx i)

249+ = let idxs = snd (idris_nameIdx i) in

244− case lookupCtxt n idxs of

250+ case lookupCtxt n idxs of

245− [x] -> return x

251+ [x] -> (i, x)

246− _ -> do let i' = fst (idris_nameIdx i) + 1

252+ _ -> let i' = fst (idris_nameIdx i) + 1 in

247− put (i { idris_nameIdx = (i', addDef n i' idxs) })

253+ (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))

248− return i'

249

254

250getHdrs :: Codegen -> Idris [String]

255getHdrs :: Codegen -> Idris [String]

251getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

256getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -133,7 +133,7 @@ data IState = IState {

133 idris_colourTheme :: ColourTheme,

134 idris_outh :: Handle,

135 idris_errorhandlers :: [Name],

136− idris_nameIdx :: (Int, Ctxt Int)

136+ idris_nameIdx :: (Int, Ctxt (Int, Name))

137 }

138

139data SizeChange = Smaller | Same | Bigger | Unknown

src/Idris/Core/Elaborate.hs+6

@@ -16,7 +16,9 @@ import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Typecheck

18import Idris.Core.Unify

19+import Idris.Core.DeepSeq

21+import Control.DeepSeq

20import Control.Monad.State

22import Control.Monad.State

21import Data.Char

23import Data.Char

22import Data.List

24import Data.List

@@ -125,6 +127,10 @@ elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty

125 (a, ES ps' str _) <- runElab d elab ps

127 (a, ES ps' str _) <- runElab d elab ps

126 return (a, str)

128 return (a, str)

127

129

130+force_term :: Elab' aux ()

131+force_term = do ES (ps, a) l p <- get

132+ put (ES (ps { pterm = force (pterm ps) }, a) l p)

133+

128updateAux :: (aux -> aux) -> Elab' aux ()

134updateAux :: (aux -> aux) -> Elab' aux ()

129updateAux f = do ES (ps, a) l p <- get

135updateAux f = do ES (ps, a) l p <- get

130 put (ES (ps, f a) l p)

136 put (ES (ps, f a) l p)

src/Idris/Core/ProofState.hs+1−1

@@ -740,7 +740,7 @@ keepGiven du (u@(n, _) : us) hs

740keepGiven du (u : us) hs = keepGiven du us hs

741

742updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

743− updateSolved' xs x

743+ updateSolved' xs x

744updateSolved' [] x = x

745updateSolved' xs (Bind n (Hole ty) t)

746 | Just v <- lookup n xs = case xs of

src/Idris/ElabTerm.hs−1

@@ -110,7 +110,6 @@ elab ist info pattern opts fn tm

110 end_unify

111 when pattern -- convert remaining holes to pattern vars

112 (do update_term orderPats

113− tm <- get_term

114 mkPat)

113 mkPat)

115 where

114 where

116 tcgen = Dictionary `elem` opts

115 tcgen = Dictionary `elem` opts

src/Idris/IBC.hs+1−1

@@ -177,7 +177,7 @@ ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

177 update (P t n@(MN _ _) ty) = return (P t n ty)

178 update (P t n@(UN _) ty) = return (P t n ty)

179 update (P t n ty) = do (f, len) <- ST.get

180− i <- lift (addNameIdx n)

180+ (i, _) <- lift (addNameIdx n)

181 when (i >= len) $

182 ST.put (f { symbols = symbols f ++ [n] }, len+1)

183 return (P t (SymRef i) ty)

src/Idris/REPL.hs+31−29

@@ -80,31 +80,33 @@ repl :: IState -- ^ The initial state

80 -> [FilePath] -- ^ The loaded modules

81 -> InputT Idris ()

82repl orig mods

83− = H.catch

83+ = -- H.catch

84− (do let quiet = opt_quiet (idris_options orig)

84+ do let quiet = opt_quiet (idris_options orig)

85− i <- lift getIState

85+ i <- lift getIState

86− let colour = idris_colourRepl i

86+ let colour = idris_colourRepl i

87− let theme = idris_colourTheme i

87+ let theme = idris_colourTheme i

88− let mvs = idris_metavars i

88+ let mvs = idris_metavars i

89− let prompt = if quiet

89+ let prompt = if quiet

90− then ""

90+ then ""

91− else showMVs colour theme mvs ++

91+ else showMVs colour theme mvs ++

92− let str = mkPrompt mods ++ ">" in

92+ let str = mkPrompt mods ++ ">" in

93− (if colour then colourisePrompt theme str else str) ++ " "

93+ (if colour then colourisePrompt theme str else str) ++ " "

94− x <- getInputLine prompt

94+ x <- H.catch (getInputLine prompt)

95+ (ctrlC (return Nothing))

95− case x of

96+ case x of

96− Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

97+ Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

97− return ()

98+ return ()

98− Just input -> H.catch

99+ Just input -> -- H.catch

99− (do ms <- lift $ processInput input orig mods

100+ do ms <- H.catch (lift $ processInput input orig mods)

101+ (ctrlC (return (Just mods)))

100− case ms of

102+ case ms of

101− Just mods -> repl orig mods

103+ Just mods -> repl orig mods

102− Nothing -> return ())

104+ Nothing -> return ()

103− ctrlC)

105+-- ctrlC)

104− ctrlC

106+-- ctrlC

105− where ctrlC :: SomeException -> InputT Idris ()

107+ where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a

106− ctrlC e = do lift $ iputStrLn (show e)

108+ ctrlC act e = do lift $ iputStrLn (show e)

107− repl orig mods

109+ act -- repl orig mods

108

110

109 showMVs c thm [] = ""

111 showMVs c thm [] = ""

110 showMVs c thm ms = "Metavariables: " ++

112 showMVs c thm ms = "Metavariables: " ++

@@ -1193,8 +1195,8 @@ idrisMain opts =

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

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

1194 return ()

1196 return ()

1195 when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner

1197 when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner

1196− ist <- getIState

1197

1198

1199+ orig <- getIState

1198 loadInputs stdout inputs

1200 loadInputs stdout inputs

1199

1201

1200 runIO $ hSetBuffering stdout LineBuffering

1202 runIO $ hSetBuffering stdout LineBuffering

@@ -1219,9 +1221,9 @@ idrisMain opts =

1219

1221

1220 when (runrepl && not idesl) $ do

1222 when (runrepl && not idesl) $ do

1221 initScript

1223 initScript

1222− startServer ist inputs

1224+ startServer orig inputs

1223− runInputT (replSettings (Just historyFile)) $ repl ist inputs

1225+ runInputT (replSettings (Just historyFile)) $ repl orig inputs

1224− when (idesl) $ ideslaveStart ist inputs

1226+ when (idesl) $ ideslaveStart orig inputs

1225 ok <- noErrors

1227 ok <- noErrors

1226 when (not ok) $ runIO (exitWith (ExitFailure 1))

1228 when (not ok) $ runIO (exitWith (ExitFailure 1))

1227 where

1229 where