a33b4c2 · Idris-dev · git.iko.soy

lib/Makefile+3

compare with master

unifiedsplit

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

16 rm -f prelude/*.ibc

17 rm -f network/*.ibc

18

19+linecount: .PHONY

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

21+

19.PHONY:

22.PHONY:

src/Idris/AbsSyntax.hs+8−1

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

108 put (i { tt_ctxt = ctxt })

109

110addIBC :: IBCWrite -> Idris ()

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

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

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

112

119

113clearIBC :: Idris ()

120clearIBC :: Idris ()

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

121clearIBC = 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)

253 let wname = MN windex (show fname)

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

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

256+ addIBC (IBCDef wname)

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

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

257 addDeferred def'

258 addDeferred def'

258

259

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

586elabDecl' info (PDirective i) = i

587elabDecl' info (PDirective i) = i

587

588

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

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

590+ = do addIBC (IBCDef n)

589− = elabDecl' info d

591+ elabDecl' info d

590

592

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

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

592

594