cad3b02 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Eat less memory by sharing names

cad3b02Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+8

compare with master

unifiedsplit

@@ -390,6 +390,14 @@ addNameIdx' i n

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

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

392

393+getSymbol :: Name -> Idris Name

394+getSymbol n = do i <- getIState

395+ case M.lookup n (idris_symbols i) of

396+ Just n' -> return n'

397+ Nothing -> do let sym' = M.insert n n (idris_symbols i)

398+ put (i { idris_symbols = sym' })

399+ return n

400+

393getHdrs :: Codegen -> Idris [String]

401getHdrs :: Codegen -> Idris [String]

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

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

395

403

src/Idris/AbsSyntaxTree.hs+4−4

@@ -24,9 +24,8 @@ import Control.Monad.Trans.Except

24import Data.Function (on)

25import Data.List hiding (group)

26import Data.Char

27−import qualified Data.Map as M

27+import qualified Data.Map.Strict as M

28import qualified Data.Text as T

29−import qualified Data.Map as M

30import Data.Either

29import Data.Either

31import qualified Data.Set as S

30import qualified Data.Set as S

32import Data.Word (Word)

31import Data.Word (Word)

@@ -215,7 +214,8 @@ data IState = IState {

215 idris_whocalls :: Maybe (M.Map Name [Name]),

214 idris_whocalls :: Maybe (M.Map Name [Name]),

216 idris_callswho :: Maybe (M.Map Name [Name]),

215 idris_callswho :: Maybe (M.Map Name [Name]),

217 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

216 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

218− elab_stack :: [Name] -- ^ Stack of names currently being elaborated

217+ elab_stack :: [Name], -- ^ Stack of names currently being elaborated

218+ idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

219 }

220

221-- Required for parsers library, and therefore trifecta

@@ -296,7 +296,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

296 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

297 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

299− AutomaticWidth S.empty Nothing Nothing [] []

299+ AutomaticWidth S.empty Nothing Nothing [] [] M.empty

300

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

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

src/Idris/IBC.hs+48−71

@@ -191,66 +191,11 @@ ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

191ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

192ibc i (IBCDef n) f

193 = do f' <- case lookupDefExact n (tt_ctxt i) of

194− Just v -> do -- (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

195− return f { ibc_defs = (n,v) : ibc_defs f }

194+ Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

196 _ -> ifail "IBC write failed"

195 _ -> ifail "IBC write failed"

197 case lookupCtxtExact n (idris_patdefs i) of

196 case lookupCtxtExact n (idris_patdefs i) of

198 Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f }

197 Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f }

199 _ -> return f' -- Not a pattern definition

198 _ -> return f' -- Not a pattern definition

200− where

201− updateDef :: Def -> StateT (IBCFile, Int) Idris Def

202− updateDef (CaseOp c t args o s cd)

203− = do o' <- mapM updateOrig o

204− cd' <- updateCD cd

205− return (CaseOp c t args o' s cd')

206− updateDef t = return t

207−

208− updateOrig (Left t) = do t' <- update t

209− return (Left t')

210− updateOrig (Right (l,r)) = do l' <- update l

211− r' <- update r

212− return (Right (l', r'))

213−

214− updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

215− = do c' <- updateSC c; r' <- updateSC r

216− return (CaseDefs (ts, t) (cs, c') (is, i) (rs, r'))

217−

218− updateSC (Case up n alts) = do alts' <- mapM updateAlt alts

219− return (Case up n alts')

220− updateSC (ProjCase t alts) = do t' <- update t

221− alts' <- mapM updateAlt alts

222− return (ProjCase t' alts')

223− updateSC (STerm t) = do t' <- update t

224− return (STerm t')

225− updateSC t = return t

226−

227− updateAlt (ConCase n i a sc) = do sc' <- updateSC sc

228− return (ConCase n i a sc')

229− updateAlt (FnCase n a sc) = do sc' <- updateSC sc

230− return (FnCase n a sc')

231− updateAlt (ConstCase i sc) = do sc' <- updateSC sc

232− return (ConstCase i sc')

233− updateAlt (SucCase n sc) = do sc' <- updateSC sc

234− return (SucCase n sc')

235− updateAlt (DefaultCase sc) = do sc' <- updateSC sc

236− return (DefaultCase sc')

237−

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

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

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

241− (i, _) <- lift (addNameIdx n)

242− when (i >= len) $

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

244− return (P t (SymRef i) ty)

245− update (App f a) = do f' <- update f; a' <- update a

246− return (App f' a')

247− update (Bind n b sc) = do b' <- fmapMB update b

248− sc' <- update sc

249− return (Bind n b' sc')

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

251− return (Proj t' i)

252− update t = return t

253−

254

199

255ibc i (IBCDoc n) f = case lookupCtxtExact n (idris_docstrings i) of

200ibc i (IBCDoc n) f = case lookupCtxtExact n (idris_docstrings i) of

256 Just v -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

201 Just v -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

@@ -470,7 +415,7 @@ pPatdefs ds

470pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

415pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

471pDefs reexp syms ds

416pDefs reexp syms ds

472 = mapM_ (\ (n, d) ->

417 = mapM_ (\ (n, d) ->

473− do let d' = force d -- (updateDef d)

418+ do d' <- updateDef d

474 case d' of

419 case d' of

475 TyDecl _ _ -> return ()

420 TyDecl _ _ -> return ()

476 _ -> do iLOG $ "SOLVING " ++ show n

421 _ -> do iLOG $ "SOLVING " ++ show n

@@ -483,23 +428,55 @@ pDefs reexp syms ds

483 else iLOG $ "Exporting " ++ show n) ds

428 else iLOG $ "Exporting " ++ show n) ds

484 where

429 where

485 updateDef (CaseOp c t args o s cd)

430 updateDef (CaseOp c t args o s cd)

431+ = do o' <- mapM updateOrig o

432+ cd' <- updateCD cd

486− = CaseOp c t args (map updateOrig o) s (updateCD cd)

433+ return $ CaseOp c t args o' s cd'

487− updateDef t = t

434+ updateDef t = return t

488

435

489− updateOrig (Left t) = Left (update t)

436+ updateOrig (Left t) = liftM Left (update t)

490− updateOrig (Right (l, r)) = Right (update l, update r)

437+ updateOrig (Right (l, r)) = do l' <- update l

438+ r' <- update r

439+ return $ Right (l', r')

491

440

492 updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

441 updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

442+ = do t' <- updateSC t

443+ c' <- updateSC c

444+ i' <- updateSC i

445+ r' <- updateSC r

493− = CaseDefs (ts, fmap update t)

446+ return $ CaseDefs (ts, t') (cs, c') (is, i') (rs, r')

494− (cs, fmap update c)

447+

495− (is, fmap update i)

448+ updateSC (Case t n alts) = do alts' <- mapM updateAlt alts

496− (rs, fmap update r)

449+ return (Case t n alts')

497−

450+ updateSC (ProjCase t alts) = do alts' <- mapM updateAlt alts

498− update (P t (SymRef i) ty) = P t (syms!!i) ty

451+ return (ProjCase t alts')

452+ updateSC (STerm t) = do t' <- update t

453+ return (STerm t')

454+ updateSC c = return c

455+

456+ updateAlt (ConCase n i ns t) = do t' <- updateSC t

457+ return (ConCase n i ns t')

458+ updateAlt (FnCase n ns t) = do t' <- updateSC t

459+ return (FnCase n ns t')

460+ updateAlt (ConstCase c t) = do t' <- updateSC t

461+ return (ConstCase c t')

462+ updateAlt (SucCase n t) = do t' <- updateSC t

463+ return (SucCase n t')

464+ updateAlt (DefaultCase t) = do t' <- updateSC t

465+ return (DefaultCase t')

466+

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

468+ return $ P t n' ty

499− update (App f a) = App (update f) (update a)

469+ update (App f a) = liftM2 App (update f) (update a)

500− update (Bind n b sc) = Bind n (fmap update b) (update sc)

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

471+ sc' <- update sc

472+ return $ Bind n b' sc'

473+ where

474+ updateB (Let t v) = liftM2 Let (update t) (update v)

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

476+ return (b { binderTy = ty' })

501− update (Proj t i) = Proj (update t) i

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

478+ return $ Proj t' i

502− update t = t

479+ update t = return t

503

480

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

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

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

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