a33b4c2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Avoid adding duplicate information to .ibc => quicker load time

commita33b4c295a2525b5ec4cc7fe55b117c7e89dbaa6 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 14:09 (15 years ago) parent201ade9

3 files changed+14−2

compare with master

unifiedsplit

lib/Makefile+3 src/Idris/AbsSyntax.hs+8−1 src/Idris/ElabDecls.hs+3−1

lib/Makefile+3

@@ -16,4 +16,7 @@ clean: .PHONY

1616 rm -f prelude/*.ibc

1717 rm -f network/*.ibc

1818

19+linecount: .PHONY

20+ wc -l *.idr network/*.idr prelude/*.idr

21+

1922.PHONY:

src/Idris/AbsSyntax.hs+8−1

@@ -108,7 +108,14 @@ setAccessibility n a

108108 put (i { tt_ctxt = ctxt })

109109

110110addIBC :: IBCWrite -> Idris ()

111−addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

111+addIBC ibc@(IBCDef n)

112+ = do i <- get

113+ when (notDef (ibc_write i)) $

114+ put (i { ibc_write = ibc : ibc_write i })

115+ where notDef [] = True

116+ notDef (IBCDef n': is) | n == n' = False

117+ notDef (_ : is) = notDef is

118+addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

112119

113120clearIBC :: Idris ()

114121clearIBC = do i <- get; put (i { ibc_write = [] })

src/Idris/ElabDecls.hs+3−1

@@ -253,6 +253,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

253253 let wname = MN windex (show fname)

254254 let imps = getImps wtype -- add to implicits context

255255 put (i { idris_implicits = addDef wname imps (idris_implicits i) })

256+ addIBC (IBCDef wname)

256257 def' <- checkDef fc [(wname, wtype)]

257258 addDeferred def'

258259

@@ -586,7 +587,8 @@ elabDecl' info (PInstance s f cs n ps t ds)

586587elabDecl' info (PDirective i) = i

587588

588589elabCaseBlock info d@(PClauses f o n ps)

589− = elabDecl' info d

590+ = do addIBC (IBCDef n)

591+ elabDecl' info d

590592

591593-- elabDecl' info (PImport i) = loadModule i

592594