26cb165 · Idris-dev · git.iko.soy

CHANGELOG.md+15−2

@@ -1,7 +1,20 @@

11# New in 1.1.*

22

3−+ Addition of `Text.Literate`, a module for working with literate

4− source files.

3+## Language updates

4+

5++ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side

6+ of any definitions in `where` clauses, provided the left-hand side of the

7+ definition does not shadow it.

8+

9+

10+## Library Updates

11+

12++ Added `Text.Literate`, a module for working with literate source files.

13++ Added `Data.IORef`, for working with mutable references in `IO`.

14+

15+## Tool Updates

16++ Private functions are no longer visible in the REPL except for modules

17+ that are explicitly loaded.

518

619# New in 1.1.1

720

codegen/idris-codegen-c/Main.hs−3

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

11module Main where

22

33import Idris.AbsSyntax

4−import Idris.Core.TT

54import Idris.ElabDecls

65import Idris.Main

76import Idris.Options

@@ -10,8 +9,6 @@ import IRTS.Compiler

109

1110import Util.System

1211

13−import Paths_idris

14−

1512import Control.Monad

1613import System.Environment

1714import System.Exit

codegen/idris-codegen-javascript/Main.hs−3

@@ -1,15 +1,12 @@

11module Main where

22

33import Idris.AbsSyntax

4−import Idris.Core.TT

54import Idris.ElabDecls

65import Idris.Main

76import Idris.Options

87import IRTS.CodegenJavaScript

98import IRTS.Compiler

109

11−import Paths_idris

12−

1310import System.Environment

1411import System.Exit

1512

codegen/idris-codegen-node/Main.hs+1−1

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

11module Main where

22

33import Idris.AbsSyntax

4−import Idris.Core.TT

54import Idris.ElabDecls

65import Idris.Main

76import Idris.Options

@@ -11,6 +10,7 @@ import IRTS.Compiler

1110import Paths_idris

1211

1312import Control.Monad

13+

1414import System.Environment

1515import System.Exit

1616

idris.cabal−1

@@ -226,7 +226,6 @@ Library

226226 , Idris.WhoCalls

227227 , Idris.CmdOptions

228228

229− , IRTS.BCImp

230229 , IRTS.Bytecode

231230 , IRTS.CodegenC

232231 , IRTS.CodegenCommon

libs/base/Data/IORef.idrnew file+28

@@ -0,0 +1,28 @@

1+module Data.IORef

2+

3+export

4+data IORef a = MkIORef a

5+

6+export

7+newIORef : a -> IO (IORef a)

8+newIORef val

9+ = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)

10+ pure (MkIORef ref)

11+

12+export

13+readIORef : IORef a -> IO a

14+readIORef (MkIORef ref)

15+ = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)

16+ pure val

17+

18+export

19+writeIORef : IORef a -> a -> IO ()

20+writeIORef (MkIORef old) val

21+ = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())

22+ (MkRaw old) (MkRaw val)

23+

24+export

25+modifyIORef : IORef a -> (a -> a) -> IO ()

26+modifyIORef ref fn

27+ = do val <- readIORef ref

28+ writeIORef ref (fn val)

libs/base/base.ipkg+1

@@ -21,6 +21,7 @@ modules = System,

2121 Data.HVect,

2222 Data.Complex,

2323 Data.Erased,

24+ Data.IORef,

2425 Data.List,

2526 Data.List.Views,

2627 Data.List.Quantifiers,

libs/contrib/Text/Lexer.idr+88−20

@@ -9,7 +9,7 @@ export

99data Recognise : (consumes : Bool) -> Type where

1010 Empty : Recognise False

1111 Fail : Recognise c

12− Expect : Recognise c -> Recognise False

12+ Lookahead : (positive : Bool) -> Recognise c -> Recognise False

1313 Pred : (Char -> Bool) -> Recognise True

1414 SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True

1515 SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)

@@ -47,18 +47,12 @@ fail = Fail

4747||| Positive lookahead. Never consumes input.

4848export

4949expect : Recognise c -> Recognise False

50−expect = Expect

50+expect = Lookahead True

5151

5252||| Negative lookahead. Never consumes input.

5353export

5454reject : Recognise c -> Recognise False

55−reject Empty = Fail

56−reject Fail = Empty

57−reject (Expect x) = reject x

58−reject (Pred f) = Expect (Pred (not . f))

59−reject (SeqEat r1 r2) = reject r1 <|> Expect (SeqEat r1 (reject r2))

60−reject (SeqEmpty r1 r2) = reject r1 <|> Expect (SeqEmpty r1 (reject r2))

61−reject (Alt r1 r2) = reject r1 <+> reject r2

55+reject = Lookahead False

6256

6357||| Recognise a specific character

6458export

@@ -113,11 +107,25 @@ export

113107many : Lexer -> Recognise False

114108many l = opt (some l)

115109

116−||| Recognise the first matching lexer from a non-empty list.

110+||| Recognise the first matching lexer from a Foldable. Always consumes input

111+||| if one of the options succeeds. Fails if the foldable is empty.

117112export

118−choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer

119−choice (x :: []) = x

120−choice (x :: xs@(_ :: _)) = x <|> choice xs

113+choice : Foldable t => t Lexer -> Lexer

114+choice xs = foldr Alt Fail xs

115+

116+||| Repeat the sub-lexer `l` zero or more times until the lexer

117+||| `stopBefore` is encountered. `stopBefore` will not be consumed.

118+||| Not guaranteed to consume input.

119+export

120+manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False

121+manyUntil stopBefore l = many (reject stopBefore <+> l)

122+

123+||| Repeat the sub-lexer `l` zero or more times until the lexer

124+||| `stopAfter` is encountered, and consume it. Guaranteed to

125+||| consume if `stopAfter` consumes.

126+export

127+manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c

128+manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter

121129

122130||| Recognise many instances of `l` until an instance of `end` is

123131||| encountered.

@@ -126,6 +134,36 @@ choice (x :: xs@(_ :: _)) = x <|> choice xs

126134export

127135manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False

128136manyTill l end = end <|> opt (l <+> manyTill l end)

137+%deprecate manyTill

138+ "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."

139+

140+||| Recognise a sub-lexer at least `min` times. Consumes input unless

141+||| min is zero.

142+export

143+atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)

144+atLeast Z l = many l

145+atLeast (S min) l = l <+> atLeast min l

146+

147+||| Recognise a sub-lexer at most `max` times. Not guaranteed to

148+||| consume input.

149+export

150+atMost : (max : Nat) -> (l : Lexer) -> Recognise False

151+atMost Z _ = Empty

152+atMost (S k) l = atMost k l <+> opt l

153+

154+||| Recognise a sub-lexer repeated between `min` and `max` times. Fails

155+||| if the inputs are out of order. Consumes input unless min is zero.

156+export

157+between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)

158+between Z max l = atMost max l

159+between (S min) Z _ = Fail

160+between (S min) (S max) l = l <+> between min max l

161+

162+||| Recognise exactly `count` repeated occurrences of a sub-lexer.

163+||| Consumes input unless count is zero.

164+export

165+exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)

166+exactly n l = between n n l

129167

130168||| Recognise any character

131169export

@@ -175,10 +213,10 @@ strTail start (MkStrLen str len)

175213scan : Recognise c -> Nat -> StrLen -> Maybe Nat

176214scan Empty idx str = pure idx

177215scan Fail idx str = Nothing

178−scan (Expect r) idx str

179− = case scan r idx str of

180− Just _ => pure idx

181− Nothing => Nothing

216+scan (Lookahead positive r) idx str

217+ = if isJust (scan r idx str) == positive

218+ then Just idx

219+ else Nothing

182220scan (Pred f) idx str

183221 = do c <- strIndex str idx

184222 if f c

@@ -220,7 +258,7 @@ digits = some digit

220258||| Recognise a single hexidecimal digit

221259export

222260hexDigit : Lexer

223−hexDigit = digit <|> oneOf "abcdefABCDEF"

261+hexDigit = pred isHexDigit

224262

225263||| Recognise one or more hexidecimal digits

226264export

@@ -277,6 +315,17 @@ export

277315spaces : Lexer

278316spaces = some space

279317

318+||| Recognise a single newline sequence. Understands CRLF, CR, and LF

319+export

320+newline : Lexer

321+newline = let crlf = "\r\n" in

322+ exact crlf <|> oneOf crlf

323+

324+||| Recognise one or more newline sequences. Understands CRLF, CR, and LF

325+export

326+newlines : Lexer

327+newlines = some newline

328+

280329||| Recognise a single non-whitespace, non-alphanumeric character

281330export

282331symbol : Lexer

@@ -291,7 +340,7 @@ symbols = some symbol

291340||| delimiting lexers

292341export

293342surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer

294−surround start end l = start <+> manyTill l end

343+surround start end l = start <+> manyThen end l

295344

296345||| Recognise zero or more occurrences of a sub-lexer surrounded

297346||| by the same quote lexer on both sides (useful for strings)

@@ -325,7 +374,26 @@ intLit = opt (is '-') <+> digits

325374||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"

326375export

327376hexLit : Lexer

328−hexLit = is '0' <+> oneOf "xX" <+> hexDigits

377+hexLit = approx "0x" <+> hexDigits

378+

379+||| Recognise `start`, then recognise all input until a newline is encountered,

380+||| and consume the newline. Will succeed if end-of-input is encountered before

381+||| a newline.

382+export

383+lineComment : (start : Lexer) -> Lexer

384+lineComment start = start <+> manyUntil newline any <+> opt newline

385+

386+||| Recognise all input between `start` and `end` lexers.

387+||| Supports balanced nesting.

388+|||

389+||| For block comments that don't support nesting (such as C-style comments),

390+||| use `surround`.

391+export

392+blockComment : (start : Lexer) -> (end : Lexer) -> Lexer

393+blockComment start end = start <+> middle <+> end

394+ where

395+ middle : Recognise False

396+ middle = manyUntil end (blockComment start end <|> any)

329397

330398||| A mapping from lexers to the tokens they produce.

331399||| This is a list of pairs `(Lexer, String -> tokenType)`

libs/contrib/Text/Literate.idr+2−2

@@ -30,13 +30,13 @@ import Data.List.Views

3030%default total

3131

3232untilEOL : Recognise False

33−untilEOL = manyTill any (is '\n')

33+untilEOL = manyUntil (is '\n') any

3434

3535line : String -> Lexer

3636line s = exact s <+> space <+> untilEOL

3737

3838block : String -> String -> Lexer

39−block s e = exact s <+> manyTill any (exact e)

39+block s e = exact s <+> manyUntil (exact e) any

4040

4141data Token = CodeBlock String String String

4242 | Any String

libs/contrib/Text/Parser.idr+69−8

@@ -40,18 +40,72 @@ inf False t = t

4040||| consumed and therefore the input is smaller)

4141export %inline

4242(>>=) : {c1 : Bool} ->

43− Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->

43+ Grammar tok c1 a ->

44+ inf c1 (a -> Grammar tok c2 b) ->

4445 Grammar tok (c1 || c2) b

4546(>>=) {c1 = False} = SeqEmpty

4647(>>=) {c1 = True} = SeqEat

4748

49+||| Sequence a grammar followed by the grammar it returns.

50+export

51+join : {c1 : Bool} ->

52+ Grammar tok c1 (Grammar tok c2 a) ->

53+ Grammar tok (c1 || c2) a

54+join {c1 = False} p = SeqEmpty p id

55+join {c1 = True} p = SeqEat p id

56+

4857||| Give two alternative grammars. If both consume, the combination is

4958||| guaranteed to consume.

5059export

51−(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->

60+(<|>) : Grammar tok c1 ty ->

61+ Grammar tok c2 ty ->

5262 Grammar tok (c1 && c2) ty

5363(<|>) = Alt

5464

65+||| Allows the result of a grammar to be mapped to a different value.

66+export

67+Functor (Grammar tok c) where

68+ map f (Empty val) = Empty (f val)

69+ map f (Fail msg) = Fail msg

70+ map f (Terminal g) = Terminal (\t => map f (g t))

71+ map f (Alt x y) = Alt (map f x) (map f y)

72+ map f (SeqEat act next)

73+ = SeqEat act (\val => map f (next val))

74+ map f (SeqEmpty act next)

75+ = SeqEmpty act (\val => map f (next val))

76+ -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,

77+ -- so a sequence must be used.

78+ map {c = False} f p = SeqEmpty p (Empty . f)

79+

80+||| Sequence a grammar with value type `a -> b` and a grammar

81+||| with value type `a`. If both succeed, apply the function

82+||| from the first grammar to the value from the second grammar.

83+||| Guaranteed to consume if either grammar consumes.

84+export

85+(<*>) : {c1 : Bool} ->

86+ Grammar tok c1 (a -> b) ->

87+ inf c1 (Grammar tok c2 a) ->

88+ Grammar tok (c1 || c2) b

89+(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)

90+(<*>) {c1 = True} x y = SeqEat x (\f => map f y)

91+

92+||| Sequence two grammars. If both succeed, use the value of the first one.

93+||| Guaranteed to consume if either grammar consumes.

94+export

95+(<*) : Grammar tok c1 a ->

96+ inf c1 (Grammar tok c2 b) ->

97+ Grammar tok (c1 || c2) a

98+(<*) x y = map const x <*> y

99+

100+||| Sequence two grammars. If both succeed, use the value of the second one.

101+||| Guaranteed to consume if either grammar consumes.

102+export

103+(*>) : Grammar tok c1 a ->

104+ inf c1 (Grammar tok c2 b) ->

105+ Grammar tok (c1 || c2) b

106+(*>) x y = map (const id) x <*> y

107+

108+||| Always succeed with the given value.

55109export

56110pure : (val : ty) -> Grammar tok False ty

57111pure = Empty

@@ -98,12 +152,16 @@ data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where

98152 (val : ty) -> (more : List tok) ->

99153 ParseResult (x :: xs ++ more) c ty

100154

155+-- Take the result of an alternative branch, reset the commit flag to

156+-- the commit flag from the outer alternative, and weaken the 'consumes'

157+-- flag to take both alternatives into account

101158weakenRes : {whatever, c : Bool} -> {xs : List tok} ->

102− ParseResult xs c ty -> ParseResult xs (whatever && c) ty

103−weakenRes (Failure com msg ts) = Failure com msg ts

104−weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs

105−weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs

106−weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more

159+ (com' : Bool) ->

160+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty

161+weakenRes com' (Failure com msg ts) = Failure com' msg ts

162+weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs

163+weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs

164+weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more

107165

108166shorter : (more : List tok) -> .(ys : List tok) ->

109167 LTE (S (length more)) (S (length (ys ++ more)))

@@ -138,7 +196,7 @@ doParse com xs act with (sizeAccessible xs)

138196 = if com' -- If the alternative had committed, don't try the

139197 -- other branch (and reset commit flag)

140198 then Failure com msg ts

141− else weakenRes (doParse False xs y | sml)

199+ else weakenRes com (doParse False xs y | sml)

142200 -- Successfully parsed the first option, so use the outer commit flag

143201 doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)

144202 = EmptyRes com val xs

@@ -226,6 +284,9 @@ optional : Grammar tok True a -> (ifNothing : a) ->

226284 Grammar tok False a

227285optional p def = p <|> pure def

228286

287+||| Fold over a list of grammars until the first one succeeds.

288+choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a

289+choice xs = foldr Alt (Fail "No more options") xs

229290

230291||| Parse an instance of `p` that is between `left` and `right`.

231292export

main/Main.hs+1−6

@@ -2,9 +2,7 @@ module Main where

22

33import System.Exit (ExitCode(..), exitSuccess, exitWith)

44

5−import Control.Monad (unless, when, (>=>))

6−import Data.Foldable (foldrM)

7−import Data.Maybe (fromMaybe)

5+import Control.Monad (unless, when)

86

97import Idris.AbsSyntax

108import Idris.CmdOptions

@@ -16,9 +14,6 @@ import Idris.Package

1614

1715import Util.System (setupBundledCC)

1816

19−import System.Exit (ExitCode(..), exitWith)

20−import Util.System (setupBundledCC)

21−

2217processShowOptions :: [Opt] -> Idris ()

2318processShowOptions opts = runIO $ do

2419 when (ShowAll `elem` opts) $ showExitIdrisInfo

rts/idris_gc.c+7−1

@@ -50,6 +50,9 @@ VAL copy(VM* vm, VAL x) {

5050 case CT_BITS64:

5151 cl = idris_b64CopyForGC(vm, x);

5252 break;

53+ case CT_REF:

54+ cl = idris_newRefLock((VAL)(x->info.ptr), 1);

55+ break;

5356 case CT_FWD:

5457 return x->info.ptr;

5558 case CT_RAWDATA:

@@ -79,7 +82,7 @@ void cheney(VM *vm) {

7982 while(scan < vm->heap.next) {

8083 size_t inc = *((size_t*)scan);

8184 VAL heap_item = (VAL)(scan+sizeof(size_t));

82− // If it's a CT_CON or CT_STROFFSET, copy its arguments

85+ // If it's a CT_CON, CT_REF or CT_STROFFSET, copy its arguments

8386 switch(GETTY(heap_item)) {

8487 case CT_CON:

8588 ar = ARITY(heap_item);

@@ -88,6 +91,9 @@ void cheney(VM *vm) {

8891 heap_item->info.c.args[i] = newptr;

8992 }

9093 break;

94+ case CT_REF:

95+ heap_item->info.ptr = copy(vm, (VAL)(heap_item->info.ptr));

96+ break;

9197 case CT_STROFFSET:

9298 heap_item->info.str_offset->str

9399 = copy(vm, heap_item->info.str_offset->str);

rts/idris_rts.c+20

@@ -776,6 +776,26 @@ VAL idris_strRev(VM* vm, VAL str) {

776776 return cl;

777777}

778778

779+VAL idris_newRefLock(VAL x, int outerlock) {

780+ Closure* cl = allocate(sizeof(Closure), outerlock);

781+ SETTY(cl, CT_REF);

782+ cl->info.ptr = (void*)x;

783+ return cl;

784+}

785+

786+VAL idris_newRef(VAL x) {

787+ return idris_newRefLock(x, 0);

788+}

789+

790+void idris_writeRef(VAL ref, VAL x) {

791+ ref->info.ptr = (void*)x;

792+ SETTY(ref, CT_REF);

793+}

794+

795+VAL idris_readRef(VAL ref) {

796+ return (VAL)(ref->info.ptr);

797+}

798+

779799VAL idris_systemInfo(VM* vm, VAL index) {

780800 int i = GETINT(index);

781801 switch(i) {

rts/idris_rts.h+8−2

@@ -26,8 +26,8 @@

2626// Closures

2727typedef enum {

2828 CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,

29− CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_FWD,

30− CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

29+ CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_REF,

30+ CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

3131} ClosureType;

3232

3333typedef struct Closure *VAL;

@@ -401,6 +401,12 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i);

401401VAL idris_strRev(VM* vm, VAL str);

402402VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str);

403403

404+// Support for IORefs

405+VAL idris_newRefLock(VAL x, int outerlock);

406+VAL idris_newRef(VAL x);

407+void idris_writeRef(VAL ref, VAL x);

408+VAL idris_readRef(VAL ref);

409+

404410// system infox

405411// used indices:

406412// 0 returns backend

src/IRTS/BCImp.hsdeleted−23

@@ -1,23 +0,0 @@

1−{-|

2−Module : IRTS.BCImp

3−Description : Bytecode for a register/variable based VM (e.g. for generating code in an imperative language where we let the language deal with GC)

4−Copyright :

5−License : BSD3

6−Maintainer : The Idris Community.

7−-}

8−module IRTS.BCImp where

9−

10−import Idris.Core.TT

11−import IRTS.Lang

12−import IRTS.Simplified

13−

14−data Reg = RVal | L Int

15−

16−data BC = NOP

17−

18−toBC :: (Name, SDecl) -> (Name, [BC])

19−toBC (n, SFun n' args locs exp)

20− = (n, bc RVal exp)

21−

22−bc :: Reg -> SExp -> [BC]

23−bc = undefined

src/IRTS/Bytecode.hs−1

@@ -23,7 +23,6 @@ module IRTS.Bytecode where

2323

2424import Idris.Core.TT

2525import IRTS.Defunctionalise

26−import IRTS.Lang

2726import IRTS.Simplified

2827

2928import Data.Maybe

src/IRTS/CodegenC.hs+1−16

@@ -9,12 +9,10 @@ Maintainer : The Idris Community.

99

1010module IRTS.CodegenC (codegenC) where

1111

12−import Idris.AbsSyntax

1312import Idris.Core.TT

1413import IRTS.Bytecode

1514import IRTS.CodegenCommon

1615import IRTS.Defunctionalise

17−import IRTS.Lang

1816import IRTS.Simplified

1917import IRTS.System

2018

@@ -24,9 +22,7 @@ import Control.Monad

2422import Data.Bits

2523import Data.Char

2624import Data.List (intercalate, nubBy)

27−import Debug.Trace

2825import Numeric

29−import System.Directory

3026import System.Exit

3127import System.FilePath ((<.>), (</>))

3228import System.IO

@@ -205,11 +201,7 @@ bcc i (MKCON l loc tag args)

205201 = indent i ++ alloc loc tag ++

206202 indent i ++ setArgs 0 args ++ "\n" ++

207203 indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

208−

209−-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++

210−-- show (length args) ++ concatMap showArg args ++ ");\n"

211− where showArg r = ", " ++ creg r

212− setArgs i [] = ""

204+ where setArgs i [] = ""

213205 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++

214206 "); " ++ setArgs (i + 1) xs

215207 alloc Nothing tag

@@ -305,13 +297,6 @@ bcc i (CONSTCASE r code def)

305297 iCase v (B64 w, bc) =

306298 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

307299 ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

308− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"

309− ++ concatMap (bcc (i+1)) bc ++

310− indent (i + 1) ++ "break;\n"

311− showDef i Nothing = ""

312− showDef i (Just c) = indent i ++ "default:\n"

313− ++ concatMap (bcc (i+1)) c ++

314− indent (i + 1) ++ "break;\n"

315300 showDefS i Nothing = ""

316301 showDefS i (Just c) = concatMap (bcc (i+1)) c

317302

src/IRTS/Compiler.hs+3−11

@@ -10,7 +10,6 @@ Maintainer : The Idris Community.

1010module IRTS.Compiler(compile, generate) where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

1413import Idris.ASTUtils

1514import Idris.Core.CaseTree

1615import Idris.Core.Evaluate

@@ -21,33 +20,24 @@ import Idris.Options

2120import Idris.Output

2221import IRTS.CodegenC

2322import IRTS.CodegenCommon

24−import IRTS.CodegenJavaScript

2523import IRTS.Defunctionalise

2624import IRTS.DumpBC

2725import IRTS.Exports

2826import IRTS.Inliner

29−import IRTS.Lang

3027import IRTS.LangOpts

3128import IRTS.Portable

3229import IRTS.Simplified

3330

3431import Prelude hiding (id, (.))

3532

36−import Control.Applicative

3733import Control.Category

3834import Control.Monad.State

39−import Data.IntSet (IntSet)

40−import qualified Data.IntSet as IS

4135import Data.List

4236import qualified Data.Map as M

43−import Data.Maybe

4437import Data.Ord

4538import qualified Data.Set as S

46−import Debug.Trace

4739import System.Directory

48−import System.Environment

4940import System.Exit

50−import System.FilePath (addTrailingPathSeparator, (</>))

5141import System.IO

5242import System.Process

5343

@@ -516,7 +506,9 @@ doForeign vs env (ret : fname : world : args)

516506 = do let l' = toFDesc l

517507 r' <- irTerm (sMN 0 "__foreignCall") vs env r

518508 return (l', r')

519− splitArg _ = ifail "Badly formed foreign function call"

509+ splitArg _ = ifail $ "Badly formed foreign function call: " ++

510+ show (ret : fname : world : args)

511+

520512

521513 toFDesc (Constant (Str str)) = FStr str

522514 toFDesc tm

src/IRTS/Defunctionalise.hs+1−52

@@ -32,7 +32,6 @@ import Control.Monad

3232import Control.Monad.State

3333import Data.List

3434import Data.Maybe

35−import Debug.Trace

3635

3736data DExp = DV Name

3837 | DApp Bool Name [DExp] -- True = tail call

@@ -165,32 +164,6 @@ addApps defs (n, LFun _ _ args e)

165164-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as

166165 chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as

167166

168− -- if anything in the DExp is projected from, we'll need to evaluate it,

169− -- but we only want to do it once, rather than every time we project.

170−

171− preEval [] t = t

172− preEval (x : xs) t

173− | needsEval x t = DLet x (DV x) (preEval xs t)

174− | otherwise = preEval xs t

175−

176− needsEval x (DApp _ _ args) = any (needsEval x) args

177− needsEval x (DC _ _ _ args) = any (needsEval x) args

178− needsEval x (DCase up e alts) = needsEval x e || any nec alts

179− where nec (DConCase _ _ _ e) = needsEval x e

180− nec (DConstCase _ e) = needsEval x e

181− nec (DDefaultCase e) = needsEval x e

182− needsEval x (DChkCase e alts) = needsEval x e || any nec alts

183− where nec (DConCase _ _ _ e) = needsEval x e

184− nec (DConstCase _ e) = needsEval x e

185− nec (DDefaultCase e) = needsEval x e

186− needsEval x (DLet n v e)

187− | x == n = needsEval x v

188− | otherwise = needsEval x v || needsEval x e

189− needsEval x (DForeign _ _ args) = any (needsEval x) (map snd args)

190− needsEval x (DOp op args) = any (needsEval x) args

191− needsEval x (DProj (DV x') _) = x == x'

192− needsEval x _ = False

193−

194167eEVAL x = DApp False (sMN 0 "EVAL") [x]

195168

196169data EvalApply a = EvalCase (Name -> a)

@@ -222,7 +195,6 @@ toConsA ns (n, i)

222195-- (DApp False n (map DV (take i (genArgs 0))))))))

223196 = mkApplyCase n ar i

224197 | otherwise = []

225− where dupdate tlarg x = x

226198

227199mkApplyCase fname n ar | n == ar = []

228200mkApplyCase fname n ar

@@ -331,30 +303,7 @@ instance Show DExp where

331303-- 'max' branches

332304mkBigCase cn max arg branches

333305 | length branches <= max = DChkCase arg branches

334− | otherwise = -- DChkCase arg branches -- until I think of something...

335− -- divide the branches into groups of at most max (by tag),

336− -- generate a new case and shrink, recursively

337− let bs = sortBy tagOrd branches

338− (all, def) = case (last bs) of

339− DDefaultCase t -> (init all, Just (DDefaultCase t))

340− _ -> (all, Nothing)

341− bss = groupsOf max all

342− cs = map mkCase bss in

343− DChkCase arg branches

344−

345− where mkCase bs = DChkCase arg bs

346−

347− tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'

348− tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'

349− tagOrd (DDefaultCase _) (DDefaultCase _) = EQ

350−

351− tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT

352− tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT

353− tagOrd (DConstCase _ _) (DDefaultCase _) = LT

354−

355− tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT

356− tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT

357− tagOrd (DDefaultCase _) (DConstCase _ _) = GT

306+ | otherwise = DChkCase arg branches

358307

359308groupsOf :: Int -> [DAlt] -> [[DAlt]]

360309groupsOf x [] = []

src/IRTS/DumpBC.hs−1

@@ -9,7 +9,6 @@ module IRTS.DumpBC where

99

1010import Idris.Core.TT

1111import IRTS.Bytecode

12−import IRTS.Lang

1312import IRTS.Simplified

1413

1514import Data.List

src/IRTS/JavaScript/LangTransforms.hs−10

@@ -12,23 +12,18 @@ module IRTS.JavaScript.LangTransforms( removeDeadCode

1212 ) where

1313

1414

15−import Control.DeepSeq

16−import Control.Monad.Trans.State

1715import Data.List

1816import Data.Map.Strict (Map)

1917import qualified Data.Map.Strict as Map

2018import Data.Maybe

2119import Data.Set (Set)

2220import qualified Data.Set as Set

23−import Data.Text (Text)

24−import qualified Data.Text as T

2521import Idris.Core.CaseTree

2622import Idris.Core.TT

2723import IRTS.Lang

2824

2925import Data.Data

3026import Data.Generics.Uniplate.Data

31−import GHC.Generics (Generic)

3227

3328deriving instance Typeable FDesc

3429deriving instance Data FDesc

@@ -49,11 +44,6 @@ deriving instance Data LOpt

4944restrictKeys :: Ord k => Map k a -> Set k -> Map k a

5045restrictKeys m s = Map.filterWithKey (\k _ -> k `Set.member` s) m

5146

52−mapMapListKeys :: Ord k => (a->a) -> [k] -> Map k a -> Map k a

53−mapMapListKeys _ [] x = x

54−mapMapListKeys f (t:r) x = mapMapListKeys f r $ Map.adjust f t x

55−

56−

5747extractGlobs :: Map Name LDecl -> LDecl -> [Name]

5848extractGlobs defs (LConstructor _ _ _) = []

5949extractGlobs defs (LFun _ _ _ e) =

src/IRTS/JavaScript/Name.hs−3

@@ -20,12 +20,9 @@ module IRTS.JavaScript.Name

2020 ) where

2121

2222import Data.Char

23−import Data.List

24−import qualified Data.Map.Strict as Map

2523import Data.Text (Text)

2624import qualified Data.Text as T

2725import Idris.Core.TT

28−import IRTS.JavaScript.AST

2926

3027jsEscape :: String -> String

3128jsEscape = concatMap jschar

src/IRTS/JavaScript/PrimOp.hs−4

@@ -16,11 +16,7 @@ module IRTS.JavaScript.PrimOp

1616 , jsPrimCoerce

1717 ) where

1818

19−import Data.Char

20−import Data.List

2119import qualified Data.Map.Strict as Map

22−import Data.Text (Text)

23−import qualified Data.Text as T

2420import Idris.Core.TT

2521import IRTS.JavaScript.AST

2622import IRTS.Lang

src/IRTS/JavaScript/Specialize.hs−14

@@ -17,10 +17,7 @@ module IRTS.JavaScript.Specialize

1717 , qualifyN

1818 ) where

1919

20−import Data.Char

21−import Data.List

2220import qualified Data.Map.Strict as Map

23−import Data.Text (Text)

2421import qualified Data.Text as T

2522import Idris.Core.TT

2623import IRTS.JavaScript.AST

@@ -62,23 +59,12 @@ constructorOptimizeDB =

6259 ]

6360 -- constructors

6461 where

65− nil = const $ JsArray []

66− cons [h, t] = JsMethod (JsArray [h]) "concat" [t]

67− -- tests

68− --trueTest e = JsUniOp (T.pack "!") $ JsUniOp (T.pack "!") e

6962 trueTest = id

7063 falseTest e = JsUniOp (T.pack "!") e

71− emptyList e = JsBinOp "===" (JsProp e "length") (JsInt 0)

72− fillList e = JsBinOp ">" (JsProp e "length") (JsInt 0)

7364 ltTest e = JsBinOp "<" e (JsInt 0)

7465 eqTest e = JsBinOp "===" e (JsInt 0)

7566 gtTest e = JsBinOp ">" e (JsInt 0)

76− noneTest e = JsBinOp "===" e JsUndefined

77− notNoneTest e = JsBinOp "!==" e JsUndefined

7867 -- projections

79− justProj x n = x

80− uncons x 1 = JsArrayProj (JsInt 0) x

81− uncons x 2 = JsMethod x "slice" [JsInt 1]

8268 cantProj x j = error $ "This type should be projected"

8369 item :: String

8470 -> String

src/IRTS/Lang.hs−2

@@ -13,12 +13,10 @@ module IRTS.Lang where

1313import Idris.Core.CaseTree

1414import Idris.Core.TT

1515

16−import Control.Applicative hiding (Const)

1716import Control.Monad.State hiding (lift)

1817import Data.Data (Data)

1918import Data.List

2019import Data.Typeable (Typeable)

21−import Debug.Trace

2220import GHC.Generics (Generic)

2321

2422data Endianness = Native | BE | LE deriving (Show, Eq)

src/IRTS/LangOpts.hs−4

@@ -9,14 +9,10 @@ Maintainer : The Idris Community.

99

1010module IRTS.LangOpts where

1111

12−import Idris.Core.CaseTree

1312import Idris.Core.TT

1413import IRTS.Lang

1514

16−import Control.Applicative hiding (Const)

1715import Control.Monad.State hiding (lift)

18−import Data.List

19−import Debug.Trace

2016

2117inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]

2218inlineAll lds = let defs = addAlist lds emptyContext in

src/IRTS/Portable.hs−2

@@ -14,12 +14,10 @@ import Idris.Core.TT

1414import IRTS.Bytecode

1515import IRTS.CodegenCommon

1616import IRTS.Defunctionalise

17−import IRTS.Lang

1817import IRTS.Simplified

1918

2019import Data.Aeson

2120import qualified Data.ByteString.Lazy as B

22−import qualified Data.Text as T

2321import System.IO

2422

2523data CodegenFile = CGFile {

src/IRTS/Simplified.hs−3

@@ -10,12 +10,9 @@ module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where

1010

1111import Idris.Core.CaseTree

1212import Idris.Core.TT

13−import Idris.Core.Typecheck

1413import IRTS.Defunctionalise

1514

1615import Control.Monad.State

17−import Data.Maybe

18−import Debug.Trace

1916

2017data SExp = SV LVar

2118 | SApp Bool Name [LVar]

src/Idris/ASTUtils.hs−1

@@ -52,7 +52,6 @@ import Idris.Options

5252

5353import Prelude hiding (id, (.))

5454

55−import Control.Applicative

5655import Control.Category

5756import Control.Monad.State.Class

5857import Data.Maybe

src/Idris/AbsSyntax.hs+4−34

@@ -7,6 +7,7 @@ Maintainer : The Idris Community.

77-}

88

99{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

1011

1112module Idris.AbsSyntax(

1213 module Idris.AbsSyntax

@@ -39,7 +40,6 @@ import System.IO.Error (tryIOError)

3940

4041import Data.Generics.Uniplate.Data (descend, descendM)

4142

42−import Debug.Trace

4343import Util.DynamicLinker

4444import Util.Pretty

4545import Util.System

@@ -597,7 +597,7 @@ getHdrs :: Codegen -> Idris [String]

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

598598

599599getImported :: Idris [(FilePath, Bool)]

600−getImported = do i <- getIState; return (idris_imported i)

600+getImported = idris_imported `fmap` getIState

601601

602602setErrSpan :: FC -> Idris ()

603603setErrSpan x = do i <- getIState;

@@ -1465,28 +1465,7 @@ expandImplementationScope ist dec ps ns d = d

14651465-- * if there's a function type, next (2)

14661466-- * finally, everything else (3)

14671467getPriority :: IState -> PTerm -> Int

1468−getPriority i tm = 1 -- pri tm

1469− where

1470− pri (PRef _ _ n) =

1471− case lookupP n (tt_ctxt i) of

1472− ((P (DCon _ _ _) _ _):_) -> 1

1473− ((P (TCon _ _) _ _):_) -> 1

1474− ((P Ref _ _):_) -> 1

1475− [] -> 0 -- must be locally bound, if it's not an error...

1476− pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))

1477− pri (PTrue _ _) = 0

1478− pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))

1479− pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

1480− pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

1481− pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))

1482− pri (PTyped l r) = pri l

1483− pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))

1484− pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1485− pri (PAlternative _ a as) = maximum (map pri as)

1486− pri (PConstant _ _) = 0

1487− pri Placeholder = 1

1488− pri _ = 3

1489−

1468+getPriority i tm = 1

14901469

14911470addStatics :: Name -> Term -> PTerm -> Idris ()

14921471addStatics n tm ptm =

@@ -2013,9 +1992,6 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []

20131992 unqualified (NS _ _) = False

20141993 unqualified _ = True

20151994

2016− constructor (TyDecl (DCon _ _ _) _) = True

2017− constructor _ = False

2018−

20191995 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia

20201996

20211997 vname (UN n) = True -- non qualified

@@ -2202,12 +2178,8 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

22022178 -- check will not necessarily fully resolve constructor names,

22032179 -- and these bare names will otherwise get in the way of

22042180 -- impossbility checking.

2205− | -- Just fn <- getFn f,

2206− canBeDConName fn ctxt

2181+ | canBeDConName fn ctxt

22072182 = PApp fc f (fmap (fmap su) args)

2208− where getFn (PRef _ _ fn) = Just fn

2209− getFn (PApp _ f args) = getFn f

2210− getFn _ = Nothing

22112183 su (PApp fc f args)

22122184 = PHidden (PApp fc f args)

22132185 su (PAlternative ms b alts)

@@ -2264,8 +2236,6 @@ findStatics ist tm = let (ns, ss) = fs tm

22642236 (ns, ss)

22652237 fs _ = ([], [])

22662238

2267− inOne n ns = length (filter id (map (elem n) ns)) == 1

2268−

22692239 pos ns ss (PPi p n fc t sc)

22702240 | elem n ss = do sc' <- pos ns ss sc

22712241 spos <- get

src/Idris/AbsSyntaxTree.hs−16

@@ -46,7 +46,6 @@ import qualified Data.Text as T

4646import Data.Traversable (Traversable)

4747import Data.Typeable

4848import GHC.Generics (Generic)

49−import Network.Socket (PortNumber)

5049

5150

5251data ElabWhat = ETypes | EDefns | EAll

@@ -2201,7 +2200,6 @@ showName ist bnd ppo colour n = case ist of

22012200 showbasic (MN i s) = str s

22022201 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

22032202 showbasic (SN s) = show s

2204− fst3 (x, _, _) = x

22052203 colourise n t = let ctxt' = fmap tt_ctxt ist in

22062204 case ctxt' of

22072205 Nothing -> name

@@ -2349,20 +2347,6 @@ implicitNamesIn uvars ist tm

23492347 addFn n = do (imps, fns) <- get

23502348 put (imps, n: fns)

23512349

2352− notCAF [] = False

2353− notCAF (PExp _ _ _ _ : _) = True

2354− notCAF (_ : xs) = notCAF xs

2355−

2356− notHidden (n, _) = case getAccessibility n of

2357− Hidden -> False

2358− Private -> False

2359− _ -> True

2360−

2361− getAccessibility n

2362− = case lookupDefAccExact n False (tt_ctxt ist) of

2363− Just (n,t) -> t

2364− _ -> Public

2365−

23662350 ni 0 env (PRef _ _ n@(NS _ _))

23672351 | not (n `elem` env)

23682352 -- Never implicitly bind if there's a namespace

src/Idris/Apropos.hs+1−7

@@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where

1111import Idris.AbsSyntax

1212import Idris.Core.Evaluate (Def(..), ctxtAlist)

1313import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),

14− Type, lookupCtxtExact, toAlist)

14+ toAlist)

1515import Idris.Docstrings (DocTerm, Docstring, containsText)

1616

1717import Data.List (intersperse, nub, nubBy)

@@ -104,9 +104,3 @@ instance (Apropos a) => Apropos (Maybe a) where

104104

105105instance (Apropos a) => Apropos [a] where

106106 isApropos str xs = any (isApropos str) xs

107−

108−defType :: Def -> Type

109−defType (Function t _) = t

110−defType (TyDecl _ t) = t

111−defType (Operator t _ _) = t

112−defType (CaseOp _ t _ _ _ _) = t

src/Idris/Chaser.hs+1−8

@@ -16,19 +16,15 @@ module Idris.Chaser(

1616import Idris.AbsSyntax

1717import Idris.Core.TT

1818import Idris.Error

19−import Idris.IBC

2019import Idris.Imports

2120import Idris.Parser

2221import Idris.Unlit

2322

2423import Control.Monad.State

25−import Control.Monad.Trans

2624import Data.List

2725import Data.Time.Clock

28−import Debug.Trace

2926import System.Directory

30−import System.FilePath

31−import Util.System (readSource, writeSource)

27+import Util.System (readSource)

3228

3329data ModuleTree = MTree { mod_path :: IFileType,

3430 mod_needsRecheck :: Bool,

@@ -62,9 +58,6 @@ getModuleFiles ts = nub $ execState (modList ts) [] where

6258-- when (not (ibc p) || rechk) $

6359 mapM_ (modTree (getSrc p : path)) deps

6460

65− ibc (IBC _ _) = True

66− ibc _ = False

67−

6861 chkReload False p = p

6962 chkReload True (IBC fn src) = chkReload True src

7063 chkReload True p = p

src/Idris/Completion.hs+11−10

@@ -5,12 +5,16 @@ Copyright :

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

9+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

11+

812module Idris.Completion (replCompletion, proverCompletion) where

913

10−import Idris.AbsSyntax (runIO)

14+import Idris.AbsSyntax (getIState, runIO)

1115import Idris.AbsSyntaxTree

1216import Idris.Colours

13−import Idris.Core.Evaluate (ctxtAlist, definitions)

17+import Idris.Core.Evaluate (ctxtAlist, visibleDefinitions)

1418import Idris.Core.TT

1519import Idris.Help

1620import Idris.Imports (installedPackages)

@@ -28,19 +32,21 @@ import qualified Data.Text as T

2832import System.Console.ANSI (Color)

2933import System.Console.Haskeline

3034

35+commands :: [String]

3136commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

3237

3338tacticArgs :: [(String, Maybe TacticArg)]

3439tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics

3540 , name <- names ]

41+

42+tactics :: [String]

3643tactics = map fst tacticArgs

3744

3845-- | Get the user-visible names from the current interpreter state.

3946names :: Idris [String]

40−names = do i <- get

41− let ctxt = tt_ctxt i

47+names = do ctxt <- tt_ctxt <$> getIState

4248 return $

43− mapMaybe nameString (allNames $ definitions ctxt) ++

49+ mapMaybe nameString (allNames $ visibleDefinitions ctxt) ++

4450 "Type" : map fst Idris.Parser.Expr.constants

4551 where

4652 -- We need both fully qualified names and identifiers that map to them

@@ -61,11 +67,6 @@ metavars :: Idris [String]

6167metavars = do i <- get

6268 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs

6369

64−

65−modules :: Idris [String]

66−modules = do i <- get

67− return $ map show $ imported i

68−

6970namespaces :: Idris [String]

7071namespaces = do

7172 ctxt <- fmap tt_ctxt get

src/Idris/Core/Binary.hs−4

@@ -13,14 +13,10 @@ module Idris.Core.Binary where

1313import Idris.Core.TT

1414

1515import Control.Applicative ((<$>), (<*>))

16−import Control.DeepSeq (($!!))

1716import Control.Monad (liftM2)

1817import Data.Binary

1918import Data.Binary.Get

2019import Data.Binary.Put

21−import qualified Data.Text as T

22−import qualified Data.Text.Encoding as E

23−import Data.Vector.Binary

2420

2521instance Binary ErrorReportPart where

2622 put (TextPart msg) = do putWord8 0 ; put msg

src/Idris/Core/CaseTree.hs+1−61

@@ -31,14 +31,11 @@ module Idris.Core.CaseTree (

3131

3232import Idris.Core.TT

3333

34−import Control.Applicative hiding (Const)

3534import Control.Monad.Reader

3635import Control.Monad.State

3736import Data.List hiding (partition)

3837import qualified Data.List (partition)

39−import Data.Maybe

4038import qualified Data.Set as S

41−import Debug.Trace

4239import GHC.Generics (Generic)

4340

4441data CaseDef = CaseDef [Name] !SC [Term]

@@ -125,7 +122,7 @@ instance TermSize CaseAlt where

125122small :: Name -> [Name] -> SC -> Bool

126123small n args t = let as = findAllUsedArgs t args in

127124 length as == length (nub as) &&

128− termsize n t < 10

125+ termsize n t < 20

129126

130127namesUsed :: SC -> [Name]

131128namesUsed sc = nub $ nu' [] sc where

@@ -271,7 +268,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

271268 = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []

272269 sc' tc defcase phase fc cs

273270 = let proj = phase == RunTime

274− vnames = fstT (head cs)

275271 pats = map (\ (avs, l, r) ->

276272 (avs, toPats reflect tc l, (l, r))) cs

277273 chkPats = mapM chkAccessible pats in

@@ -288,10 +284,7 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

288284 else return t

289285 Error err -> Error (At fc err)

290286 where args = map (\i -> sMN i "e") [0..]

291− defaultCase True = STerm Erased

292− defaultCase False = UnmatchedCase "Error"

293287 fstT (x, _, _) = x

294− lstT (_, _, x) = x

295288

296289 -- Check that all pattern variables are reachable by a case split

297290 -- Otherwise, they won't make sense on the RHS.

@@ -306,48 +299,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

306299 acc (PSuc p : xs) n = acc (p : xs) n

307300 acc (_ : xs) n = acc xs n

308301

309−-- For each 'Case', make sure every choice is in the same type family,

310−-- as directed by the variable type (i.e. there is no implicit type casing

311−-- going on).

312−

313−checkSameTypes :: [(Name, Type)] -> SC -> Bool

314−checkSameTypes tys (Case _ n alts)

315− = case lookup n tys of

316− Just t -> and (map (checkAlts t) alts)

317− _ -> and (map ((checkSameTypes tys).getSC) alts)

318− where

319− checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc

320− checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc

321− checkAlts _ (ConstCase c sc) = False

322− checkAlts _ _ = True

323−

324− getSC (ConCase _ _ _ sc) = sc

325− getSC (FnCase _ _ sc) = sc

326− getSC (ConstCase _ sc) = sc

327− getSC (SucCase _ sc) = sc

328− getSC (DefaultCase sc) = sc

329−checkSameTypes _ _ = True

330−

331−-- FIXME: All we're actually doing here is checking that we haven't arrived

332−-- at a specific constructor for a polymorphic argument. I *think* this

333−-- is sufficient, but if it turns out not to be, fix it!

334−--

335−-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718

336−isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

337−isType n t | (P Ref _ _, _) <- unApply t = True

338−isType n t = False

339−

340−isConstType (I _) (AType (ATInt ITNative)) = True

341−isConstType (BI _) (AType (ATInt ITBig)) = True

342−isConstType (Fl _) (AType ATFloat) = True

343−isConstType (Ch _) (AType (ATInt ITChar)) = True

344−isConstType (Str _) StrType = True

345−isConstType (B8 _) (AType (ATInt _)) = True

346−isConstType (B16 _) (AType (ATInt _)) = True

347−isConstType (B32 _) (AType (ATInt _)) = True

348−isConstType (B64 _) (AType (ATInt _)) = True

349−isConstType _ _ = False

350−

351302data Pat = PCon Bool Name Int [Pat]

352303 | PConst Const

353304 | PInferred Pat

@@ -403,12 +354,6 @@ toPat reflect tc = map $ toPat' []

403354

404355 toPat' _ t = PAny

405356

406− fixedN IT8 = "Bits8"

407− fixedN IT16 = "Bits16"

408− fixedN IT32 = "Bits32"

409− fixedN IT64 = "Bits64"

410−

411−

412357data Partition = Cons [Clause]

413358 | Vars [Clause]

414359 deriving Show

@@ -666,9 +611,6 @@ argsToAlt inacc rs@((r, m) : rest) = do

666611 where

667612 (acc, inacc) = partitionAcc r

668613

669− uniq i (UN n) = MN i n

670− uniq i n = n

671−

672614getVar :: String -> CaseBuilder Name

673615getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)

674616

@@ -872,5 +814,3 @@ mkForce = mkForceSC

872814 = SucCase sn (mkForceSC n arg rhs)

873815 mkForceAlt n arg (DefaultCase rhs)

874816 = DefaultCase (mkForceSC n arg rhs)

875−

876− forceTm n arg t = subst n arg t

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

@@ -8,15 +8,13 @@ Maintainer : The Idris Community.

88-}

99module Idris.Core.Constraints ( ucheck ) where

1010

11−import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),

12− UConstraint(..), UExp(..))

11+import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),

12+ UExp(..))

1313

14−import Control.Applicative

1514import Control.Monad.State.Strict

1615import Data.List (partition)

1716import qualified Data.Map.Strict as M

1817import qualified Data.Set as S

19−import Debug.Trace

2018

2119-- | Check that a list of universe constraints can be satisfied.

2220ucheck :: S.Set ConstraintFC -> TC ()

src/Idris/Core/Elaborate.hs−19

@@ -16,7 +16,6 @@ module Idris.Core.Elaborate (

1616 , module Idris.Core.ProofState

1717 ) where

1818

19−import Idris.Core.DeepSeq

2019import Idris.Core.Evaluate

2120import Idris.Core.ProofState

2221import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,

@@ -24,15 +23,9 @@ import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,

2423import Idris.Core.TT

2524import Idris.Core.Typecheck

2625import Idris.Core.Unify

27−import Idris.Core.WHNF

2826

29−import Util.Pretty hiding (fill)

30−

31−import Control.DeepSeq

3227import Control.Monad.State.Strict

33−import Data.Char

3428import Data.List

35−import Debug.Trace

3629

3730data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

3831 deriving Show

@@ -614,9 +607,6 @@ prepare_apply fn imps =

614607 lift $ tfail $ TooManyArguments n

615608 | otherwise = fail $ "Too many arguments for " ++ show fn

616609

617− doClaim ((i, _), n, t) = do claim n t

618− when i (movelast n)

619−

620610 mkMN n@(MN i _) = n

621611 mkMN n@(UN x) = MN 99999 x

622612 mkMN n@(SN s) = sMN 99999 (show s)

@@ -673,8 +663,6 @@ apply' fillt fn imps =

673663 | i = getNonUnify acc is as

674664 | otherwise = getNonUnify (t : acc) is as

675665

676−-- getNonUnify imps args = map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

677−

678666

679667apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

680668apply2 fn elabs =

@@ -682,7 +670,6 @@ apply2 fn elabs =

682670 fill (raw_apply fn (map (Var . snd) args))

683671 elabArgs (map snd args) elabs

684672 ES (p, a) s prev <- get

685− let (n, hs) = unified p

686673 end_unify

687674 solve

688675 where elabArgs [] [] = return $! ()

@@ -700,16 +687,10 @@ apply_elab n args =

700687 env <- get_env

701688 claims <- doClaims (normalise ctxt env ty) args []

702689 prep_fill n (map fst claims)

703− let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

704690 elabClaims [] False claims

705691 complete_fill

706692 end_unify

707693 where

708− priOrder Nothing Nothing = EQ

709− priOrder Nothing _ = LT

710− priOrder _ Nothing = GT

711− priOrder (Just (x, _)) (Just (y, _)) = compare x y

712−

713694 doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =

714695 do n <- unique_hole (mkMN n')

715696 when (null claims) (start_unify n)

src/Idris/Core/Evaluate.hs+14−46

@@ -5,9 +5,11 @@ Copyright :

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

89{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

910 MultiParamTypeClasses, PatternGuards #-}

1011{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

12+{-# OPTIONS_GHC -fwarn-unused-imports #-}

1113

1214module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

1315 normaliseAll, normaliseBlocking, toValue, quoteTerm,

@@ -28,20 +30,19 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

2830 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

2931 conGuarded,

3032 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

33+ visibleDefinitions,

3134 isUniverse, linearCheck, linearCheckArg) where

3235

3336import Idris.Core.CaseTree

3437import Idris.Core.TT

3538

36−import Control.Applicative hiding (Const)

3739import Control.Monad.State

38−import Data.Binary hiding (get, put)

39−import qualified Data.Binary as B

4040import Data.List

4141import Data.Maybe (listToMaybe)

42−import Debug.Trace

4342import GHC.Generics (Generic)

4443

44+import qualified Data.Map.Strict as Map

45+

4546data EvalState = ES { limited :: [(Name, Int)],

4647 nexthole :: Int,

4748 blocking :: Bool }

@@ -205,16 +206,6 @@ unfold ctxt env ns t

205206finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))

206207finalEntry (n, r, b) = (n, r, fmap finalise b)

207208

208−bindEnv :: EnvTT n -> TT n -> TT n

209−bindEnv [] tm = tm

210−bindEnv ((n, r, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)

211−bindEnv ((n, r, b):bs) tm = Bind n b (bindEnv bs tm)

212−

213−unbindEnv :: EnvTT n -> TT n -> TT n

214−unbindEnv [] tm = tm

215−unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

216−unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."

217−

218209usable :: Bool -- specialising

219210 -> Bool -- unfolding only

220211 -> Int -- Reduction depth limit (when simplifying/at REPL)

@@ -392,22 +383,6 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

392383 evApply ntimes stk top env args f

393384 = apply ntimes stk top env f args

394385

395− reapply ntimes stk top env f@(VP Ref n ty) args

396− = let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in

397− case val of

398− Just (CaseOp ci _ _ _ _ cd, acc) ->

399− let (ns, tree) = getCases cd in

400− do c <- evCase ntimes n (n:stk) top env ns args tree

401− case c of

402− (Nothing, _) -> return $ unload env (VP Ref n ty) args

403− (Just v, rest) -> evApply ntimes stk top env rest v

404− _ -> case args of

405− (a : as) -> return $ unload env f (a : as)

406− [] -> return f

407− reapply ntimes stk top env (VApp f a) args

408− = reapply ntimes stk top env f (a : args)

409− reapply ntimes stk top env v args = return v

410−

411386 apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)

412387 = do a' <- sc a

413388 app <- apply ntimes stk top env a' as

@@ -740,13 +715,6 @@ convEq ctxt holes topx topy = ceq [] topx topy where

740715 (caseeq ((x,y):ps) xdef ydef)

741716 _ -> return False

742717

743−-- SPECIALISATION -----------------------------------------------------------

744−-- We need too much control to be able to do this by tweaking the main

745−-- evaluator

746−

747−spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)

748−spec ctxt statics genv tm = error "spec undefined"

749−

750718-- CONTEXTS -----------------------------------------------------------------

751719

752720{-| A definition is either a simple function (just an expression with a type),

@@ -983,8 +951,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

983951 ( CaseDef args_ct sc_ct _,

984952 CaseDef args_rt sc_rt _) ->

985953 let inl = alwaysInline -- tcdict

986− inlc = (inl || small n args_ct sc_ct) && (not asserted)

987− inlr = inl || small n args_rt sc_rt

954+ inlc = (inl || small n args_rt sc_rt) && (not asserted)

988955 cdef = CaseDefs (args_ct, sc_ct)

989956 (args_rt, sc_rt)

990957 op = (CaseOp (ci { case_inlinable = inlc })

@@ -1152,6 +1119,14 @@ conGuarded ctxt n tm = guarded n tm

11521119 isConName f ctxt = any (guarded n) as

11531120 guarded _ _ = False

11541121

1122+visibleDefinitions :: Context -> Ctxt TTDecl

1123+visibleDefinitions ctxt =

1124+ Map.filter (\m -> length m > 0) . Map.map onlyVisible . definitions $ ctxt

1125+ where

1126+ onlyVisible = Map.filter visible

1127+ visible (_def, _rigCount, _injectivity, accessibility, _totality, _metaInformation) =

1128+ accessibility `notElem` [Hidden, Private]

1129+

11551130lookupP :: Name -> Context -> [Term]

11561131lookupP = lookupP_all False False

11571132

@@ -1240,13 +1215,6 @@ linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

12401215 tfail $ Msg $ show f ++ " can only appear in a linear binding"

12411216 _ -> return ()

12421217

1243− checkArgs (Bind n (Pi RigW _ ty _) sc)

1244− = do mapM_ checkNameOK (allTTNames ty)

1245− checkArgs (substV (P Bound n Erased) sc)

1246− checkArgs (Bind n (Pi _ _ _ _) sc)

1247− = checkArgs (substV (P Bound n Erased) sc)

1248− checkArgs _ = return ()

1249−

12501218-- Check if a name is reducible in the type checker. Partial definitions

12511219-- are not reducible (so treated as a constant)

12521220tcReducible :: Name -> Context -> Bool

src/Idris/Core/Execute.hs+2−39

@@ -11,7 +11,6 @@ Maintainer : The Idris Community.

1111module Idris.Core.Execute (execute) where

1212

1313import Idris.AbsSyntax

14−import Idris.AbsSyntaxTree

1514import Idris.Core.CaseTree

1615import Idris.Core.Evaluate

1716import Idris.Core.TT

@@ -22,15 +21,11 @@ import IRTS.Lang (FDesc(..), FType(..))

2221import Util.DynamicLinker

2322import Util.System

2423

25−import Control.Applicative hiding (Const)

2624import Control.Exception

27−import Control.Monad hiding (forM)

2825import Control.Monad.Trans

2926import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)

3027import Control.Monad.Trans.State.Strict

31−import Data.Bits

3228import Data.IORef

33−import qualified Data.Map as M

3429import Data.Maybe

3530import Data.Time.Clock.POSIX (getPOSIXTime)

3631import Data.Traversable (forM)

@@ -42,7 +37,6 @@ import System.IO.Unsafe

4237#ifdef IDRIS_FFI

4338import Foreign.C.String

4439import Foreign.LibFFI

45−import Foreign.Marshal.Alloc (free)

4640import Foreign.Ptr

4741#endif

4842

@@ -51,10 +45,6 @@ execute :: Term -> Idris Term

5145execute tm = fail "libffi not supported, rebuild Idris with -f FFI"

5246#else

5347-- else is rest of file

54−readMay :: (Read a) => String -> Maybe a

55−readMay s = case reads s of

56− [(x, "")] -> Just x

57− _ -> Nothing

5848

5949data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

6050

@@ -170,9 +160,6 @@ runExec ex st = fst <$> runStateT (runExceptT ex) st

170160getExecState :: Exec ExecState

171161getExecState = lift get

172162

173−putExecState :: ExecState -> Exec ()

174−putExecState = lift . put

175−

176163execFail :: Err -> Exec a

177164execFail = throwE

178165

@@ -481,8 +468,8 @@ execForeign env ctxt arity ty fn xs onfail

481468execForeign env ctxt arity ty fn xs onfail

482469 = case foreignFromTT arity ty fn xs of

483470 Just ffun@(FFun f argTs retT) | length xs >= arity ->

484− do let (args', xs') = (take arity xs, -- foreign args

485− drop arity xs) -- rest

471+ do let (_, xs') = (take arity xs, -- foreign args

472+ drop arity xs) -- rest

486473 res <- call ffun (map snd argTs)

487474 case res of

488475 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

@@ -710,26 +697,6 @@ foreignFromTT arity ty (EConstant (Str name)) args

710697 return $ FFun name argFTyVals (toFDesc ty)

711698foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing

712699

713−getFTy :: ExecVal -> Maybe FType

714−getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))

715− | fi == txt "FIntT" =

716− case str intTy of

717− "ITNative" -> Just (FArith (ATInt ITNative))

718− "ITChar" -> Just (FArith (ATInt ITChar))

719− "IT8" -> Just (FArith (ATInt (ITFixed IT8)))

720− "IT16" -> Just (FArith (ATInt (ITFixed IT16)))

721− "IT32" -> Just (FArith (ATInt (ITFixed IT32)))

722− "IT64" -> Just (FArith (ATInt (ITFixed IT64)))

723− _ -> Nothing

724−getFTy (EP _ (UN t) _) =

725− case str t of

726− "FFloat" -> Just (FArith ATFloat)

727− "FString" -> Just FString

728− "FPtr" -> Just FPtr

729− "FUnit" -> Just FUnit

730− _ -> Nothing

731−getFTy _ = Nothing

732−

733700unEList :: ExecVal -> Maybe [ExecVal]

734701unEList tm = case unApplyV tm of

735702 (nil, [_]) -> Just []

@@ -739,10 +706,6 @@ unEList tm = case unApplyV tm of

739706 (f, args) -> Nothing

740707

741708

742−toConst :: Term -> Maybe Const

743−toConst (Constant c) = Just c

744−toConst _ = Nothing

745−

746709mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]

747710mapMaybeM f [] = return []

748711mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

src/Idris/Core/ProofState.hs+10−58

@@ -28,11 +28,9 @@ import Idris.Core.WHNF

2828

2929import Util.Pretty hiding (fill)

3030

31−import Control.Applicative hiding (empty)

3231import Control.Arrow ((***))

3332import Control.Monad.State.Strict

3433import Data.List

35−import Debug.Trace

3634

3735data ProofState = PS { thname :: Name,

3836 holes :: [Name], -- ^ holes still to be solved

@@ -181,7 +179,6 @@ match_unify' :: Context -> Env ->

181179match_unify' ctxt env (topx, xfrom) (topy, yfrom) =

182180 do ps <- get

183181 let while = while_elaborating ps

184− let dont = dontunify ps

185182 let inj = injective ps

186183 traceWhen (unifylog ps)

187184 ("Matching " ++ show (topx, topy) ++

@@ -494,15 +491,6 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

494491 Nothing -> error ("deferType can't find " ++ show n)

495492deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."

496493

497−regret :: RunTactic

498−regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

499− do action (\ps -> let hs = holes ps in

500− ps { holes = hs \\ [x] })

501− return sc

502−regret ctxt env (Bind x (Hole t) _)

503− = fail $ show x ++ " : " ++ show t ++ " is not solved..."

504−regret _ _ _ = fail "The current focus is not a hole."

505−

506494unifyGoal :: Raw -> RunTactic

507495unifyGoal tm ctxt env h@(Bind x b sc) =

508496 do (tmv, _) <- lift $ check ctxt env tm

@@ -529,14 +517,8 @@ exact _ _ _ _ = fail "Can't fill here."

529517fill :: Raw -> RunTactic

530518fill guess ctxt env (Bind x (Hole ty) sc) =

531519 do (val, valty) <- lift $ check ctxt env guess

532−-- let valtyn = normalise ctxt env valty

533−-- let tyn = normalise ctxt env ty

534− ns <- unify' ctxt env (valty, Just $ SourceTerm val)

535− (ty, Just (chkPurpose val ty))

536− ps <- get

537− let (uh, uns) = unified ps

538−-- put (ps { unified = (uh, uns ++ ns) })

539−-- addLog (show (uh, uns ++ ns))

520+ unify' ctxt env (valty, Just $ SourceTerm val)

521+ (ty, Just (chkPurpose val ty))

540522 return $ Bind x (Guess ty val) sc

541523 where

542524 -- some expected types show up commonly in errors and indicate a

@@ -552,14 +534,8 @@ fill _ _ _ _ = fail "Can't fill here."

552534match_fill :: Raw -> RunTactic

553535match_fill guess ctxt env (Bind x (Hole ty) sc) =

554536 do (val, valty) <- lift $ check ctxt env guess

555−-- let valtyn = normalise ctxt env valty

556−-- let tyn = normalise ctxt env ty

557− ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)

558− (ty, Just ExpectedType)

559− ps <- get

560− let (uh, uns) = unified ps

561−-- put (ps { unified = (uh, uns ++ ns) })

562−-- addLog (show (uh, uns ++ ns))

537+ match_unify' ctxt env (valty, Just $ SourceTerm val)

538+ (ty, Just ExpectedType)

563539 return $ Bind x (Guess ty val) sc

564540match_fill _ _ _ _ = fail "Can't fill here."

565541

@@ -573,11 +549,8 @@ complete_fill :: RunTactic

573549complete_fill ctxt env (Bind x (Guess ty val) sc) =

574550 do let guess = forget val

575551 (val', valty) <- lift $ check ctxt env guess

576− ns <- unify' ctxt env (valty, Just $ SourceTerm val')

577− (ty, Just ExpectedType)

578− ps <- get

579− let (uh, uns) = unified ps

580−-- put (ps { unified = (uh, uns ++ ns) })

552+ unify' ctxt env (valty, Just $ SourceTerm val')

553+ (ty, Just ExpectedType)

581554 return $ Bind x (Guess ty val) sc

582555complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

583556

@@ -588,7 +561,6 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

588561solve :: RunTactic

589562solve ctxt env (Bind x (Guess ty val) sc)

590563 = do ps <- get

591− let (uh, uns) = unified ps

592564 dropdots <-

593565 case lookup x (notunified ps) of

594566 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

@@ -605,7 +577,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

605577 recents = x : recents ps,

606578 implementations = implementations ps \\ [x],

607579 dotted = dropUnified dropdots (dotted ps) })

608− let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

580+ let (locked, _) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

609581 return locked

610582 where dropUnified ddots [] = []

611583 dropUnified ddots ((x, es) : ds)

@@ -630,7 +602,6 @@ solve ctxt env (Bind x (Guess ty val) sc)

630602 (Bind n (Let ty' val') sc', tyl && vall && scl)

631603 tryLock hs t@(Bind n b sc)

632604 = let (bt', btl) = tryLock hs (binderTy b)

633− (val', vall) = tryLock hs val

634605 (sc', scl) = tryLock hs sc in

635606 (Bind n (b { binderTy = bt' }) sc', btl && scl)

636607 tryLock hs t = (t, True)

@@ -656,13 +627,9 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

656627 x@(Bind y (Pi _ _ s _) _) -> x

657628 _ -> normalise ctxt env t

658629 (tyv, tyt) <- lift $ check ctxt env ty

659−-- ns <- lift $ unify ctxt env tyv t'

660630 case t' of

661631 Bind y (Pi rig _ s _) t -> let t' = updsubst y (P Bound n s) t in

662− do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

663− ps <- get

664− let (uh, uns) = unified ps

665−-- put (ps { unified = (uh, uns ++ ns) })

632+ do unify' ctxt env (s, Nothing) (tyv, Nothing)

666633 return $ Bind n (Lam rig tyv) (Bind x (Hole t') (P Bound x t'))

667634 _ -> lift $ tfail $ CantIntroduce t'

668635introTy ty n ctxt env _ = fail "Can't introduce here."

@@ -760,7 +727,7 @@ casetac :: Raw -> Bool -> RunTactic

760727casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

761728 (tmv, tmt) <- lift $ check ctxt env tm

762729 let tmt' = normalise ctxt env tmt

763− let (tacn, tacstr, tactt) = if induction

730+ let (tacn, tacstr, _) = if induction

764731 then (ElimN, "eliminator", "Induction")

765732 else (CaseN (FC' emptyFC), "case analysis", "Case analysis")

766733 case unApply tmt' of

@@ -773,13 +740,9 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

773740 _ -> return []

774741 let (params, indicies) = splitTyArgs param_pos tyargs

775742 let args = getArgTys elimTy

776− let pmargs = take (length params) args

777743 let args' = drop (length params) args

778− let propTy = head args'

779744 let restargs = init $ tail args'

780745 let consargs = take (length restargs - length indicies) restargs

781− let indxargs = drop (length restargs - length indicies) restargs

782− let scr = last $ tail args'

783746 let indxnames = makeIndexNames indicies

784747 currentNames <- query $ allTTNames . getProofTerm . pterm

785748 let tmnm = case tm of

@@ -801,8 +764,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

801764 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

802765 _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")

803766 tmt'

804− where scname = sMN 0 "scarg"

805− makeConsArg (nm, ty) = P Bound nm ty

767+ where makeConsArg (nm, ty) = P Bound nm ty

806768 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

807769 bindConsArgs [] v = v

808770 addConsHole (nm, ty) =

@@ -881,8 +843,6 @@ start_unify :: Name -> RunTactic

881843start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })

882844 return tm

883845

884−tmap f (a, b, c) = (f a, b, c)

885−

886846solve_unified :: RunTactic

887847solve_unified ctxt env tm =

888848 do ps <- get

@@ -931,14 +891,6 @@ updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

931891 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

932892updateError ns e = e

933893

934−updateRes ns [] = []

935−updateRes ns ((x, t) : ts) = (x, updateSolvedTerm ns t) : updateRes ns ts

936−

937−solveInProblems x val [] = []

938−solveInProblems x val ((l, r, env, err) : ps)

939− = ((psubst x val l, psubst x val r,

940− updateEnv [(x, val)] env, err) : solveInProblems x val ps)

941−

942894mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)

943895mergeNotunified env holes ns = mnu ns [] [] where

944896 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

src/Idris/Core/ProofTerm.hs−13

@@ -18,11 +18,8 @@ module Idris.Core.ProofTerm(

1818

1919import Idris.Core.Evaluate

2020import Idris.Core.TT

21−import Idris.Core.Typecheck

2221

2322import Control.Monad.State.Strict

24−import Data.List

25−import Debug.Trace

2623

2724-- | A zipper over terms, in order to efficiently update proof terms.

2825data TermPath = Top

@@ -198,16 +195,6 @@ updateSolvedTerm' xs x = updateSolved' xs x where

198195 updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in

199196 if u then (b { binderTy = ty' }, u) else (b, False)

200197

201− noneOf ns (P _ n _) | n `elem` ns = False

202− noneOf ns (App s f a) = noneOf ns a && noneOf ns f

203− noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t

204− noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b

205− where

206− noneOfB ns (Let t v) = noneOf ns t && noneOf ns v

207− noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v

208− noneOfB ns b = noneOf ns (binderTy b)

209− noneOf ns _ = True

210−

211198-- | As 'subst', in TT, but takes advantage of knowing not to substitute

212199-- under Complete applications.

213200updsubst :: Eq n => n {-^ The id to replace -} ->

src/Idris/Core/TT.hs+2−25

@@ -60,31 +60,25 @@ import Util.Pretty hiding (Str)

6060-- Work around AMP without CPP

6161import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,

6262 Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),

63− Read(..), Show(..), String, div, error, flip, fst, mod, not,

64− otherwise, read, snd, ($), (&&), (.), (||))

63+ Show(..), String, div, error, fst, mod, not, otherwise, read,

64+ snd, ($), (&&), (.), (||))

6565

6666import Control.Applicative (Alternative, Applicative(..))

6767import qualified Control.Applicative as A (Alternative(..))

6868import Control.DeepSeq (($!!))

6969import Control.Monad.State.Strict

70−import Control.Monad.Trans.Except (Except(..))

7170import Data.Binary hiding (get, put)

72−import qualified Data.Binary as B

7371import Data.Char

7472import Data.Data (Data)

7573import Data.Foldable (Foldable)

7674import Data.List hiding (group, insert)

7775import qualified Data.Map.Strict as Map

7876import Data.Maybe (listToMaybe)

79−import Data.Monoid (mconcat)

8077import Data.Set (Set, fromList, insert, member)

8178import qualified Data.Text as T

8279import Data.Traversable (Traversable)

8380import Data.Typeable (Typeable)

84−import Data.Vector.Unboxed (Vector)

85−import qualified Data.Vector.Unboxed as V

8681import Debug.Trace

87−import Foreign.Storable (sizeOf)

8882import GHC.Generics (Generic)

8983import Numeric (showIntAtBase)

9084import Numeric.IEEE (IEEE(identicalIEEE))

@@ -436,13 +430,6 @@ instance Show a => Show (TC a) where

436430tfail :: Err -> TC a

437431tfail e = Error e

438432

439−failMsg :: String -> TC a

440−failMsg str = Error (Msg str)

441−

442−trun :: FC -> TC a -> TC a

443−trun fc (OK a) = OK a

444−trun fc (Error e) = Error (At fc e)

445−

446433discard :: Monad m => m a -> m ()

447434discard f = f >> return ()

448435

@@ -515,9 +502,6 @@ deriving instance Binary SpecialName

515502sImplementationN :: Name -> [String] -> SpecialName

516503sImplementationN n ss = ImplementationN n (map T.pack ss)

517504

518−sParentN :: Name -> String -> SpecialName

519−sParentN n s = ParentN n (T.pack s)

520−

521505instance Sized Name where

522506 size (UN n) = 1

523507 size (NS n els) = 1 + length els

@@ -704,13 +688,6 @@ nativeTyWidth IT16 = 16

704688nativeTyWidth IT32 = 32

705689nativeTyWidth IT64 = 64

706690

707−{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}

708−intTyWidth :: IntTy -> Int

709−intTyWidth (ITFixed n) = nativeTyWidth n

710−intTyWidth ITNative = 8 * sizeOf (0 :: Int)

711−intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"

712−intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

713−

714691data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

715692 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

716693 | AType ArithTy | StrType

src/Idris/Core/Typecheck.hs−34

@@ -13,11 +13,8 @@ module Idris.Core.Typecheck where

1313

1414import Idris.Core.Evaluate

1515import Idris.Core.TT

16−import Idris.Core.WHNF

1716

1817import Control.Monad.State

19−import qualified Data.Vector.Unboxed as V (length)

20−import Debug.Trace

2118

2219-- To check conversion, normalise each term wrt the current environment.

2320-- Since we haven't converted everything to de Bruijn indices yet, we'll have to

@@ -208,12 +205,6 @@ check' holes tcns ctxt env top

208205 Just v' -> v'

209206 (tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t

210207

211−-- convertsC ctxt env st (TType maxu)

212−-- convertsC ctxt env tt (TType maxu)

213−-- when holes $ put (v, cs)

214−-- return (Bind n (Pi i (uniqueBinders (map fst env) sv) (TType maxu))

215−-- (pToV n tv), TType maxu)

216−

217208 case (normalise ctxt env st, normalise ctxt env tt) of

218209 (TType su, TType tu) -> do

219210 when (not holes) $ do (v, cs) <- get

@@ -227,21 +218,6 @@ check' holes tcns ctxt env top

227218 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

228219 (pToV n tv), k', sns ++ tns)

229220

230− where mkUniquePi kv (Bind n (Pi rig i s k) sc)

231− = let k' = smaller kv k in

232− Bind n (Pi rig i s k') (mkUniquePi k' sc)

233− mkUniquePi kv (Bind n (Lam rig t) sc)

234− = Bind n (Lam rig (mkUniquePi kv t)) (mkUniquePi kv sc)

235− mkUniquePi kv (Bind n (Let t v) sc)

236− = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

237− mkUniquePi kv t = t

238−

239− -- Kind of the whole thing is the kind of the most unique thing

240− -- in the environment (because uniqueness taints everything...)

241− mostUnique [] k = k

242− mostUnique (Pi _ _ _ pk : es) k = mostUnique es (smaller pk k)

243− mostUnique (_ : es) k = mostUnique es k

244−

245221 chk rigc u lvl env (RBind n b sc)

246222 = do (b', bt', bns) <- checkBinder b

247223 (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc

@@ -264,7 +240,6 @@ check' holes tcns ctxt env top

264240

265241 checkBinder (Lam rig t)

266242 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

267− let tv' = normalise ctxt env tv

268243 convType tcns ctxt env tt

269244 return (Lam rig tv, tt, [])

270245 checkBinder (Let t v)

@@ -273,14 +248,12 @@ check' holes tcns ctxt env top

273248 -- (or rather, like an application of a lambda, multiply)

274249 -- (Consider: adding a single use let?)

275250 (vv, vt, vns) <- chk (rigMult rigc RigW) u Nothing env v

276− let tv' = normalise ctxt env tv

277251 convertsC ctxt env vt tv

278252 convType tcns ctxt env tt

279253 return (Let tv vv, tt, vns)

280254 checkBinder (NLet t v)

281255 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

282256 (vv, vt, vns) <- chk rigc u Nothing env v

283− let tv' = normalise ctxt env tv

284257 convertsC ctxt env vt tv

285258 convType tcns ctxt env tt

286259 return (NLet tv vv, tt, vns)

@@ -288,12 +261,10 @@ check' holes tcns ctxt env top

288261 | not holes = lift $ tfail (IncompleteTerm undefined)

289262 | otherwise

290263 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

291− let tv' = normalise ctxt env tv

292264 convType tcns ctxt env tt

293265 return (Hole tv, tt, [])

294266 checkBinder (GHole i ns t)

295267 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

296− let tv' = normalise ctxt env tv

297268 convType tcns ctxt env tt

298269 return (GHole i ns tv, tt, [])

299270 checkBinder (Guess t v)

@@ -301,20 +272,15 @@ check' holes tcns ctxt env top

301272 | otherwise

302273 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

303274 (vv, vt, vns) <- chk rigc u Nothing env v

304− let tv' = normalise ctxt env tv

305275 convertsC ctxt env vt tv

306276 convType tcns ctxt env tt

307277 return (Guess tv vv, tt, vns)

308278 checkBinder (PVar rig t)

309279 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

310− let tv' = normalise ctxt env tv

311280 convType tcns ctxt env tt

312− -- Normalised version, for erasure purposes (it's easier

313− -- to tell if it's a collapsible variable)

314281 return (PVar rig tv, tt, [])

315282 checkBinder (PVTy t)

316283 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

317− let tv' = normalise ctxt env tv

318284 convType tcns ctxt env tt

319285 return (PVTy tv, tt, [])

320286

src/Idris/Core/Unify.hs−90

@@ -22,11 +22,9 @@ module Idris.Core.Unify(

2222import Idris.Core.Evaluate

2323import Idris.Core.TT

2424

25−import Control.Monad

2625import Control.Monad.State.Strict

2726import Data.List

2827import Data.Maybe

29−import Debug.Trace

3028

3129-- terms which need to be injective, with the things we're trying to unify

3230-- at the time

@@ -39,7 +37,6 @@ data FailContext = FailContext { fail_sourceloc :: FC,

3937 }

4038 deriving (Eq, Show)

4139

42−type Injs = [(TT Name, TT Name, TT Name)]

4340type Fails = [(TT Name, TT Name, -- unification error

4441 Bool, -- ready to retry yet

4542 Env, Err, [FailContext], FailAt)]

@@ -57,10 +54,6 @@ unrecoverable = any bad

5754data UInfo = UI Int Fails

5855 deriving Show

5956

60−data UResult a = UOK a

61− | UPartOK a

62− | UFail Err

63−

6457-- | Smart constructor for unification errors that takes into account the FailContext

6558cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t

6659cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

@@ -191,16 +184,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

191184 | otherwise = checkScope ns (x, tm)

192185

193186 checkScope ns (x, tm) =

194−-- case boundVs (envPos x 0 env) tm of

195−-- [] -> return [(x, tm)]

196−-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

197−-- (impl ns tm) (errEnv env))

198187 let v = highV (-1) tm in

199188 if v >= length ns

200189 then lift $ tfail (Msg "SCOPE ERROR")

201190 else return [(x, bind v ns tm)]

202− where impl [] tm = tm

203− impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

204191

205192 bind i ns tm

206193 | i < 0 = tm

@@ -257,20 +244,6 @@ trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPa

257244 followSols vs (n : ns) = do ns' <- followSols vs ns

258245 return $ n : ns'

259246

260−expandLets env (x, tm) = (x, doSubst (reverse env) tm)

261− where

262− doSubst [] tm = tm

263− doSubst ((n, Let v t) : env) tm

264− = doSubst env (subst n v tm)

265− doSubst (_ : env) tm

266− = doSubst env tm

267−

268−hasv :: TT Name -> Bool

269−hasv (V x) = True

270−hasv (App _ f a) = hasv f || hasv a

271−hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

272−hasv _ = False

273−

274247unify :: Context -> Env ->

275248 (TT Name, Maybe Provenance) ->

276249 (TT Name, Maybe Provenance) ->

@@ -297,10 +270,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

297270-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

298271 Error e -> tfail e

299272 where

300− headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

301− headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

302− headDiff _ _ = False

303−

304273 injective (P (DCon _ _ _) _ _) = True

305274 injective (P (TCon _ _) _ _) = True

306275-- injective (P Ref n _)

@@ -327,10 +296,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

327296 sc i = do UI s f <- get

328297 put (UI (s+i) f)

329298

330− errors :: StateT UInfo TC Bool

331− errors = do UI s f <- get

332− return (not (null f))

333−

334299 uplus u1 u2 = do UI s f <- get

335300 r <- u1

336301 UI s f' <- get

@@ -342,12 +307,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

342307 StateT UInfo

343308 TC [(Name, TT Name)]

344309 un = un' env

345−-- un fn names x y

346−-- = let (xf, _) = unApply x

347−-- (yf, _) = unApply y in

348−-- if headDiff xf yf then unifyFail x y else

349−-- uplus (un' fn names x y)

350−-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

351310

352311 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

353312 StateT UInfo

@@ -577,26 +536,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

577536 = unifyFail appx appy

578537 checkHeads _ _ = return []

579538

580− numArgs tm = let (f, args) = unApply tm in length args

581−

582539 metavarApp tm = let (f, args) = unApply tm in

583540 (metavar f &&

584541 all (\x -> metavarApp x) args

585542 && nub args == args) ||

586543 globmetavar tm

587− metavarArgs tm = let (f, args) = unApply tm in

588− all (\x -> metavar x || inenv x) args

589− && nub args == args

590− metavarApp' tm = let (f, args) = unApply tm in

591− all (\x -> pat x || metavar x) (f : args)

592− && nub args == args

593−

594− rigid (P (DCon _ _ _) _ _) = True

595− rigid (P (TCon _ _) _ _) = True

596− rigid t@(P Ref _ _) = inenv t || globmetavar t

597− rigid (Constant _) = True

598− rigid (App _ f a) = rigid f && rigid a

599− rigid t = not (metavar t) || globmetavar t

600544

601545 globmetavar t = case unApply t of

602546 (P _ x _, _) ->

@@ -610,14 +554,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

610554 (x `elem` holes || holeIn env x))

611555 || globmetavar t

612556 _ -> False

613− pat t = case t of

614− P _ x _ -> x `elem` holes || patIn env x

615− _ -> False

616− inenv t = case t of

617− P _ x _ -> x `elem` (map fstEnv env)

618− _ -> False

619−

620− notFn t = injective t || metavar t || inenv t

621557

622558 injectiveTC t@(P Ref n _) t'@(P Ref n' _)

623559 | Just ni <- lookupInjectiveExact n ctxt,

@@ -682,16 +618,10 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

682618 | otherwise = checkScope ns (x, tm)

683619

684620 checkScope ns (x, tm) | pureTerm tm =

685−-- case boundVs (envPos x 0 env) tm of

686−-- [] -> return [(x, tm)]

687−-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

688−-- (impl ns tm) (errEnv env))

689621 let v = highV (-1) tm in

690622 if v >= length ns

691623 then lift $ tfail (Msg "SCOPE ERROR")

692624 else return [(x, bind v ns tm)]

693− where impl [] tm = tm

694− impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

695625 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

696626

697627 bind i ns tm

@@ -710,15 +640,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

710640 sc 1

711641 combine env bnames as (ns' ++ bs)

712642

713−boundVs :: Int -> Term -> [Int]

714−boundVs i (V j) | j < i = []

715− | otherwise = [j]

716−boundVs i (Bind n b sc) = boundVs (i + 1) sc

717−boundVs i (App _ f x) = let fs = boundVs i f

718− xs = boundVs i x in

719− nub (fs ++ xs)

720−boundVs i _ = []

721−

722643highV :: Int -> Term -> Int

723644highV i (V j) | j > i = j

724645 | otherwise = i

@@ -726,11 +647,6 @@ highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]

726647highV i (App _ f x) = max (highV i f) (highV i x)

727648highV i _ = i

728649

729−envPos x i [] = 0

730−envPos x i ((y, _) : ys) | x == y = i

731− | otherwise = envPos x (i + 1) ys

732−

733−

734650-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

735651-- more work may help.

736652-- FIXME: Depending on how overloading gets used, this may cause problems. Better

@@ -796,9 +712,3 @@ holeIn env n = case lookupBinder n env of

796712 Just (Hole _) -> True

797713 Just (Guess _ _) -> True

798714 _ -> False

799−

800−patIn :: Env -> Name -> Bool

801−patIn env n = case lookupBinder n env of

802− Just (PVar _ _) -> True

803− Just (PVTy _) -> True

804− _ -> False

src/Idris/Core/WHNF.hs−3

@@ -12,11 +12,8 @@ module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where

1212

1313import Idris.Core.CaseTree

1414import Idris.Core.Evaluate hiding (quote)

15−import qualified Idris.Core.Evaluate as Evaluate

1615import Idris.Core.TT

1716

18−import Debug.Trace

19−

2017-- | A stack entry consists of a term and the environment it is to be

2118-- evaluated in (i.e. it's a thunk)

2219type StackEntry = (Term, WEnv)

src/Idris/Coverage.hs−10

@@ -16,14 +16,11 @@ import Idris.Core.TT

1616import Idris.Delaborate

1717import Idris.Elab.Utils

1818import Idris.Error

19−import Idris.Output (iWarn, iputStrLn)

2019

2120import Control.Monad.State.Strict

2221import Data.Char

23−import Data.Either

2422import Data.List

2523import Data.Maybe

26−import Debug.Trace

2724

2825-- | Generate a pattern from an 'impossible' LHS.

2926--

@@ -284,10 +281,6 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)

284281 collectConsts (ConstCase c sc) = Just c

285282 collectConsts _ = Nothing

286283

287− hasDefault (DefaultCase (UnmatchedCase _)) = False

288− hasDefault (DefaultCase _) = True

289− hasDefault _ = False

290−

291284 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)

292285 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of

293286 (P _ tyn _, _) -> Just tyn

@@ -336,9 +329,6 @@ trimOverlapping sc = trim [] [] sc

336329 trimAlts cs nots vn (DefaultCase sc : rest)

337330 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest

338331

339− isConMatch c (ConCase cn t args sc) = c == cn

340− isConMatch _ _ = False

341−

342332 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]

343333 substMatch ca [] = []

344334 substMatch (c,args) (ConCase cn t args' sc : _)

src/Idris/DSL.hs+1−4

@@ -11,12 +11,10 @@ Maintainer : The Idris Community.

1111module Idris.DSL where

1212

1313import Idris.AbsSyntax

14−import Idris.Core.Evaluate

1514import Idris.Core.TT

1615

1716import Control.Monad.State.Strict

1817import Data.Generics.Uniplate.Data (transform)

19−import Debug.Trace

2018

2119debindApp :: SyntaxInfo -> PTerm -> PTerm

2220debindApp syn t = debind (dsl_bind (dsl_info syn)) t

@@ -169,8 +167,7 @@ var dsl n t i = v' i t where

169167 setFC fc t = t

170168

171169unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

172−unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

173− mkap (getFn e)

170+unIdiom ap pure fc e@(PApp _ _ _) = mkap (getFn e)

174171 where

175172 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

176173 getFn f = (f, [])

src/Idris/DataOpts.hs−6

@@ -10,14 +10,8 @@ Maintainer : The Idris Community.

1010module Idris.DataOpts(applyOpts) where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

1413import Idris.Core.TT

1514

16−import Control.Applicative

17−import Data.List

18−import Data.Maybe

19−import Debug.Trace

20−

2115class Optimisable term where

2216 applyOpts :: term -> Idris term

2317

src/Idris/DeepSeq.hs−1

@@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..))

2424

2525import Util.DynamicLinker

2626

27−import qualified Cheapskate.Types as CT

2827import Control.DeepSeq

2928import Network.Socket (PortNumber)

3029

src/Idris/Delaborate.hs+2−10

@@ -26,10 +26,9 @@ import Prelude hiding ((<$>))

2626import Control.Applicative (Alternative((<|>)))

2727import Control.Monad.State

2828import Data.Generics.Uniplate.Data (transform)

29−import Data.List (intersperse, nub)

29+import Data.List (nub)

3030import Data.Maybe (mapMaybe)

3131import qualified Data.Text as T

32−import Debug.Trace

3332

3433bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

3534

@@ -192,13 +191,6 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

192191 de tys env _ (TType i) = PType un

193192 de tys env _ (UType u) = PUniverse un u

194193

195− dens x | fullname = x

196− dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

197− [_] -> n -- just one thing

198− [] -> n -- metavariables have no implicits

199− _ -> ns

200− dens n = n

201−

202194 deFn tys env (App _ f a) args = deFn tys env f (a:args)

203195 deFn tys env (P _ n _) [l,r]

204196 | n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)

@@ -354,7 +346,7 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

354346 then text "Unification failure" <$> showSc i sc

355347 else empty

356348pprintErr' i (CantConvert x_in y_in env) =

357− let (x_ns, y_ns, nms) = renameMNs x_in y_in

349+ let (x_ns, y_ns, _) = renameMNs x_in y_in

358350 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

359351 (delabSugared i (flagUnique y_ns)) in

360352 text "Type mismatch between" <>

src/Idris/Directives.hs−1

@@ -8,7 +8,6 @@ Maintainer : The Idris Community.

88module Idris.Directives(directiveAction) where

99

1010import Idris.AbsSyntax

11−import Idris.ASTUtils

1211import Idris.Core.Evaluate

1312import Idris.Core.TT

1413import Idris.Imports

src/Idris/Docs.hs−4

@@ -240,10 +240,6 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

240240 updateRef nm (PRef fc _ _) = PRef fc [] nm

241241 updateRef _ pt = pt

242242

243− isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'

244− isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

245− isSubInterface _ = False

246−

247243 prettyConstraints =

248244 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

249245

src/Idris/Elab/AsPat.hs+21−10

@@ -10,20 +10,31 @@ module Idris.Elab.AsPat(desugarAs) where

1010import Idris.AbsSyntax

1111import Idris.Core.TT

1212

13−import Control.Applicative

1413import Control.Monad.State.Strict

15−import Data.Generics.Uniplate.Data (transformM)

14+import Data.Generics.Uniplate.Data (transformM, universe)

1615

1716-- | Desugar by changing x@y on lhs to let x = y in ... or rhs

18−desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)

19−desugarAs lhs rhs

20− = let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in

21− (lhs', bindPats pats rhs)

17+desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])

18+desugarAs lhs rhs whereblock

19+ = (lhs', bindOnRight rhs pats, map (bindInWhereDecl pats) whereblock)

2220 where

23− bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm

24− bindPats [] rhs = rhs

25− bindPats ((n, fc, tm) : ps) rhs

26− = PLet fc n NoFC Placeholder tm (bindPats ps rhs)

21+ (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []

22+

23+ bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm

24+ bindOnRight = foldr (\(n, fc, tm) -> PLet fc n NoFC Placeholder tm)

25+

26+ bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl

27+ bindInWhereDecl pats (PClauses fc opts n clauses)

28+ = PClauses fc opts n $ map (bindInWhereClause pats) clauses

29+ bindInWhereDecl _ d = d

30+

31+ bindInWhereClause :: [(Name, FC, PTerm)] -> PClause -> PClause

32+ bindInWhereClause pats (PClause fc n lhs ws rhs wb)

33+ = let bound = [ n | (PRef _ _ n) <- universe lhs ]

34+ pats' = filter (not . (`elem` bound) . \(n,_,_) -> n) pats

35+ rhs' = bindOnRight rhs pats' in

36+ PClause fc n lhs ws rhs' $ map (bindInWhereDecl pats') wb

37+ bindInWhereClause _ c = c

2738

2839collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm

2940collectAs (PAs fc n tm) = do tm' <- collectAs tm

src/Idris/Elab/Clause.hs+8−52

@@ -13,51 +13,37 @@ import Idris.ASTUtils

1313import Idris.Core.CaseTree

1414import Idris.Core.Elaborate hiding (Tactic(..))

1515import Idris.Core.Evaluate

16−import Idris.Core.Execute

1716import Idris.Core.TT

1817import Idris.Core.Typecheck

1918import Idris.Core.WHNF

2019import Idris.Coverage

2120import Idris.DataOpts

22−import Idris.DeepSeq

21+import Idris.DeepSeq ()

2322import Idris.Delaborate

2423import Idris.Docstrings hiding (Unchecked)

25−import Idris.DSL

2624import Idris.Elab.AsPat

2725import Idris.Elab.Term

2826import Idris.Elab.Transform

2927import Idris.Elab.Type

3028import Idris.Elab.Utils

3129import Idris.Error

32−import Idris.Imports

33−import Idris.Inliner

3430import Idris.Options

35−import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)

31+import Idris.Output (iputStrLn, pshow, sendHighlighting)

3632import Idris.PartialEval

37−import Idris.Primitives

38−import Idris.Providers

3933import Idris.Termination

4034import Idris.Transforms

41−import IRTS.Lang

4235

4336import Util.Pretty hiding ((<$>))

44−import Util.Pretty (pretty, text)

4537

4638import Prelude hiding (id, (.))

4739

48−import Control.Applicative hiding (Const)

4940import Control.Category

5041import Control.DeepSeq

5142import Control.Monad

5243import qualified Control.Monad.State.Lazy as LState

5344import Control.Monad.State.Strict as State

54−import Data.Char (isLetter, toLower)

5545import Data.List

56−import Data.List.Split (splitOn)

57−import qualified Data.Map as Map

5846import Data.Maybe

59−import qualified Data.Set as S

60−import qualified Data.Text as T

6147import Data.Word

6248import Debug.Trace

6349import Numeric

@@ -153,12 +139,6 @@ elabClauses info' fc opts n_in cs =

153139 -- optimisation applied to LHS

154140 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

155141 map debind pats_forced

156− -- pdef_cov is the pattern definition without forcing, which

157− -- we feed to the coverage checker (we need to know what the

158− -- programmer wrote before forcing erasure)

159− let pdef_cov

160− = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

161− map debind pats_raw

162142 -- pdef_pe is the one which will get further optimised

163143 -- for run-time, with no forcing optimisation of the LHS because

164144 -- the affects erasure. Also, it's partially evaluated

@@ -173,8 +153,6 @@ elabClauses info' fc opts n_in cs =

173153 -- help with later inlinings.

174154

175155 ist <- getIState

176− let pdef_inl = inlineDef ist pdef

177−

178156 numArgs <- tclift $ sameLength pdef

179157

180158 case specNames opts of

@@ -197,7 +175,6 @@ elabClauses info' fc opts n_in cs =

197175 missing' <- checkPossibles info fc True n missing

198176 -- Filter out the ones which match one of the

199177 -- given cases (including impossible ones)

200− let clhs = map getLHS pdef

201178 logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++

202179 showSep "\n" (map showTmImpls missing') ++

203180 "\nAgainst: " ++

@@ -245,7 +222,6 @@ elabClauses info' fc opts n_in cs =

245222 logElab 3 $ "Optimised: " ++ show tree'

246223 ctxt <- getContext

247224 ist <- getIState

248− let opt = idris_optimisation ist

249225 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

250226 (idris_patdefs ist) })

251227 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

@@ -315,15 +291,6 @@ elabClauses info' fc opts n_in cs =

315291 return ()

316292

317293 where

318− noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of

319− Right _ -> False

320− Left miss -> True) cs

321− where

322− trim_matchClause i (PApp fcl fl ls) (PApp fcr fr rs)

323− = let args = min (length ls) (length rs) in

324− matchClause i (PApp fcl fl (take args ls))

325− (PApp fcr fr (take args rs))

326−

327294 checkUndefined n ctxt = case lookupDef n ctxt of

328295 [] -> return ()

329296 [TyDecl _ _] -> return ()

@@ -371,7 +338,7 @@ elabClauses info' fc opts n_in cs =

371338

372339 sameLength ((_, x, _) : xs)

373340 = do l <- sameLength xs

374− let (f, as) = unApply x

341+ let (_, as) = unApply x

375342 if (null xs || l == length as) then return (length as)

376343 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

377344 sameLength [] = return 0

@@ -683,11 +650,10 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

683650 logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++

684651 "\n" ++ show ptm

685652 return (Left ptm, lhs)

686−elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)

687− = do let tcgen = Dictionary `elem` opts

688− push_estack fname False

653+elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)

654+ = do push_estack fname False

689655 ctxt <- getContext

690− let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

656+ let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as

691657

692658 -- Build the LHS as an "Infer", and pull out its type and

693659 -- pattern bindings

@@ -916,8 +882,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

916882 pinfo info ns ds i

917883 = let newps = params info ++ ns

918884 dsParams = map (\n -> (n, map fst newps)) ds

919− newb = addAlist dsParams (inblock info)

920− l = liftname info in

885+ newb = addAlist dsParams (inblock info) in

921886 info { params = newps,

922887 inblock = newb,

923888 liftname = id -- (\n -> case lookupCtxt n newb of

@@ -966,8 +931,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

966931 isOutsideWith _ = True

967932

968933elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

969− = do let tcgen = Dictionary `elem` opts

970− ctxt <- getContext

934+ = do ctxt <- getContext

971935 -- Build the LHS as an "Infer", and pull out its type and

972936 -- pattern bindings

973937 i <- getIState

@@ -1189,9 +1153,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

11891153 mkAux pn wname toplhs ns ns' c

11901154 = ifail $ show fc ++ ":badly formed with clause"

11911155

1192− addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

1193− addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]

1194−

11951156 -- ns, arguments which don't depend on the with argument

11961157 -- ns', arguments which do

11971158 updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

@@ -1215,11 +1176,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

12151176 updateWithTerm ist pn wname toplhs ns_in ns_in' tm

12161177 = mapPT updateApp tm

12171178 where

1218− arity (PApp _ _ as) = length as

1219− arity _ = 0

1220−

1221− lhs_arity = arity toplhs

1222−

12231179 currentFn fname (PAlternative _ _ as)

12241180 | Just tm <- getApp as = tm

12251181 where getApp (tm@(PApp _ (PRef _ _ f) _) : as)

src/Idris/Elab/Data.hs+4−40

@@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where

1010

1111import Idris.AbsSyntax

1212import Idris.ASTUtils

13−import Idris.Core.CaseTree

14−import Idris.Core.Elaborate hiding (Tactic(..))

1513import Idris.Core.Evaluate

16−import Idris.Core.Execute

1714import Idris.Core.TT

1815import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

2216import Idris.Delaborate

2317import Idris.Docstrings

24−import Idris.DSL

2518import Idris.Elab.Rewrite

26−import Idris.Elab.Term

2719import Idris.Elab.Type

2820import Idris.Elab.Utils

2921import Idris.Elab.Value

3022import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

23+import Idris.Output (iWarn, sendHighlighting)

3824

3925import Util.Pretty

4026

4127import Prelude hiding (id, (.))

4228

43−import Control.Applicative hiding (Const)

4429import Control.Category

45−import Control.DeepSeq

4630import Control.Monad

4731import Control.Monad.State.Strict as State

4832import Data.Char (isLetter, toLower)

4933import Data.List

50−import Data.List.Split (splitOn)

5134import qualified Data.Map as Map

5235import Data.Maybe

53−import qualified Data.Set as S

5436import qualified Data.Text as T

55−import Debug.Trace

5637

5738warnLC :: FC -> Name -> Idris ()

5839warnLC fc n

@@ -61,8 +42,7 @@ warnLC fc n

6142

6243elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

6344elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

64− = do let codata = Codata `elem` opts

65− logElab 1 (show (fc, doc))

45+ = do logElab 1 (show (fc, doc))

6646 checkUndefined fc n

6747 when (implicitable (nsroot n)) $ warnLC fc n

6848 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

@@ -92,7 +72,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

9272 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

9373 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

9474 ttag <- getName

95− let as = map (const (Left (Msg ""))) (getArgTys cty)

9675

9776 ctxt <- getContext

9877 let params = findParams n (normalise ctxt [] cty) (map snd cons)

@@ -170,8 +149,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

170149 cinfo info ds

171150 = let newps = params info

172151 dsParams = map (\n -> (n, [])) ds

173− newb = addAlist dsParams (inblock info)

174− l = liftname info in

152+ newb = addAlist dsParams (inblock info) in

175153 info { params = newps,

176154 inblock = newb,

177155 liftname = id -- Is this appropriate?

@@ -245,12 +223,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

245223 getTyName (PRef _ _ n) = n == nsroot tn

246224 getTyName _ = False

247225

248−

249− getNamePos :: Int -> PTerm -> Name -> Maybe Int

250− getNamePos i (PPi _ n _ _ sc) x | n == x = Just i

251− | otherwise = getNamePos (i + 1) sc x

252− getNamePos _ _ _ = Nothing

253−

254226 -- if the constructor is a UniqueType, the datatype must be too

255227 -- (AnyType is fine, since that is checked for uniqueness too)

256228 -- if hte contructor is AnyType, the datatype must be at least AnyType

@@ -358,7 +330,7 @@ elabCaseFun ind paramPos n ty cons info = do

358330 elimLog "Elaborating case function"

359331 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

360332 let (cnstrs, _) = splitPi ty

361− let (splittedTy@(pms, idxs)) = splitPms cnstrs

333+ let (pms, idxs) = splitPms cnstrs

362334 generalParams <- namePis False pms

363335 motiveIdxs <- namePis False idxs

364336 let motive = mkMotive n paramPos generalParams motiveIdxs

@@ -396,10 +368,6 @@ elabCaseFun ind paramPos n ty cons info = do

396368 elimDeclName :: Name

397369 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

398370

399− applyNS :: Name -> [String] -> Name

400− applyNS n [] = n

401− applyNS n ns = sNS n ns

402−

403371 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

404372 splitPi = splitPi' []

405373 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

@@ -440,10 +408,6 @@ elabCaseFun ind paramPos n ty cons info = do

440408 simpleName (MN i n) = str n ++ show i

441409 simpleName n = show n

442410

443− nameSpaces :: Name -> [String]

444− nameSpaces (NS _ ns) = map str ns

445− nameSpaces _ = []

446−

447411 freshName :: String -> EliminatorState Name

448412 freshName key = do

449413 nameMap <- get

src/Idris/Elab/Implementation.hs+2−29

@@ -9,50 +9,27 @@ Maintainer : The Idris Community.

99module Idris.Elab.Implementation(elabImplementation) where

1010

1111import Idris.AbsSyntax

12−import Idris.ASTUtils

1312import Idris.Core.CaseTree

1413import Idris.Core.Elaborate hiding (Tactic(..))

1514import Idris.Core.Evaluate

16−import Idris.Core.Execute

1715import Idris.Core.TT

18−import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

2216import Idris.Delaborate

2317import Idris.Docstrings

24−import Idris.DSL

25−import Idris.Elab.Data

2618import Idris.Elab.Term

2719import Idris.Elab.Type

2820import Idris.Elab.Utils

2921import Idris.Error

30−import Idris.Imports

31−import Idris.Inliner

32−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

33−import Idris.PartialEval

34−import Idris.Primitives

35−import Idris.Providers

36−import IRTS.Lang

22+import Idris.Output (iWarn, sendHighlighting)

3723

38−import Util.Pretty (pretty, text)

24+import Util.Pretty (text)

3925

4026import Prelude hiding (id, (.))

4127

42−import Control.Applicative hiding (Const)

4328import Control.Category

44−import Control.DeepSeq

4529import Control.Monad

46−import Control.Monad.State.Strict as State

47−import Data.Char (isLetter, toLower)

4830import Data.List

49−import Data.List.Split (splitOn)

50−import qualified Data.Map as Map

5131import Data.Maybe

52−import qualified Data.Set as S

5332import qualified Data.Text as T

54−import Debug.Trace

55−

5633

5734elabImplementation :: ElabInfo

5835 -> SyntaxInfo

@@ -79,7 +56,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

7956 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

8057 cs -> tclift $ tfail $ At fc

8158 (CantResolveAlts (map fst cs))

82− let constraint = PApp fc (PRef fc [] n) (map pexp ps)

8359 let iname = mkiname n (namespace info) ps expn

8460 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

8561 ist <- getIState

@@ -167,7 +143,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

167143 let wbVals_orig = map (decorateid (decorate ns iname)) ds'

168144 ist <- getIState

169145 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

170− let wb = wbTys ++ wbVals

171146

172147 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

173148 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))

@@ -300,8 +275,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

300275 mkMethApp ps (n, _, _, ty)

301276 = lamBind 0 ty (papp fc (PRef fc [] n)

302277 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

303− where

304− needed is p = pname p `elem` map pname is

305278

306279 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

307280 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

src/Idris/Elab/Interface.hs+2−45

@@ -10,51 +10,22 @@ Maintainer : The Idris Community.

1010module Idris.Elab.Interface(elabInterface) where

1111

1212import Idris.AbsSyntax

13−import Idris.ASTUtils

14−import Idris.Core.CaseTree

15−import Idris.Core.Elaborate hiding (Tactic(..))

1613import Idris.Core.Evaluate

17−import Idris.Core.Execute

1814import Idris.Core.TT

19−import Idris.Core.Typecheck

20−import Idris.Coverage

21−import Idris.DataOpts

22−import Idris.DeepSeq

2315import Idris.Delaborate

2416import Idris.Docstrings

25−import Idris.DSL

2617import Idris.Elab.Data

27−import Idris.Elab.Term

28−import Idris.Elab.Type

2918import Idris.Elab.Utils

3019import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

38−

39−import Util.Pretty (pretty, text)

20+import Idris.Output (sendHighlighting)

4021

4122import Prelude hiding (id, (.))

4223

43−import Control.Applicative hiding (Const)

4424import Control.Category

45−import Control.DeepSeq

4625import Control.Monad

47−import Control.Monad.State.Strict as State

48−import Data.Char (isLetter, toLower)

4926import Data.Generics.Uniplate.Data (transform)

5027import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

5328import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

56−import Debug.Trace

57−

5829

5930data MArgTy = IA Name | EA Name | CA deriving Show

6031

@@ -123,8 +94,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

12394 ims <- mapM (tdecl impps mnames) mdecls

12495 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

12596 (filter clause ds)

126− let (methods, imethods)

127− = unzip (map (\ (x, y, z) -> (x, y)) ims)

97+ let imethods = map (\ (x, y, z) -> y) ims

12898 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

12999

130100 addInterface tn (CI cn (map nodoc imethods) defaults idecls

@@ -396,13 +366,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

396366 return (PTy doc [] syn fc o m mfc ty',

397367 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

398368

399− updateIMethod :: [(Name, PTerm)] ->

400− (Name, (a, b, c, d, PTerm)) ->

401− (Name, (a, b, c, d, PTerm))

402− updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))

403− | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))

404− | otherwise = tm

405−

406369 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

407370 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

408371 getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc

@@ -452,12 +415,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

452415 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

453416 toExp ns e sc = sc

454417

455−-- | Get the method declaration name corresponding to a user-provided name

456−mdec :: Name -> Name

457−mdec (UN n) = SN (MethodN (UN n))

458−mdec (NS x n) = NS (mdec x) n

459−mdec x = x

460−

461418-- | Get the docstring corresponding to a member, if one exists

462419memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

463420memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

src/Idris/Elab/Provider.hs−27

@@ -9,51 +9,24 @@ Maintainer : The Idris Community.

99module Idris.Elab.Provider(elabProvider) where

1010

1111import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

14−import Idris.Core.Elaborate hiding (Tactic(..))

1512import Idris.Core.Evaluate

1613import Idris.Core.Execute

1714import Idris.Core.TT

1815import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

2216import Idris.Delaborate

2317import Idris.Docstrings

24−import Idris.DSL

2518import Idris.Elab.Clause

2619import Idris.Elab.Term

2720import Idris.Elab.Type

28−import Idris.Elab.Utils

2921import Idris.Elab.Value

3022import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

3323import Idris.Options

34−import Idris.Output (iWarn, iputStrLn, pshow)

35−import Idris.PartialEval

36−import Idris.Primitives

3724import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

4125

4226import Prelude hiding (id, (.))

4327

44−import Control.Applicative hiding (Const)

4528import Control.Category

46−import Control.DeepSeq

4729import Control.Monad

48−import Control.Monad.State.Strict as State

49−import Data.Char (isLetter, toLower)

50−import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

53−import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

56−import Debug.Trace

5730

5831-- | Elaborate a type provider

5932elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()

src/Idris/Elab/Record.hs+1−40

@@ -11,25 +11,11 @@ module Idris.Elab.Record(elabRecord) where

1111import Idris.AbsSyntax

1212import Idris.Core.Evaluate

1313import Idris.Core.TT

14−import Idris.Coverage

15−import Idris.DataOpts

16−import Idris.DeepSeq

1714import Idris.Delaborate

1815import Idris.Docstrings

1916import Idris.Elab.Data

20−import Idris.Elab.Data

21−import Idris.Elab.Term

22−import Idris.Elab.Type

23−import Idris.Elab.Utils

2417import Idris.Error

25−import Idris.Imports

26−import Idris.Inliner

27−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

28−import Idris.Parser.Expr (tryFullExpr)

29−import Idris.PartialEval

30−import Idris.Primitives

31−import Idris.Providers

32−import IRTS.Lang

18+import Idris.Output (sendHighlighting)

3319

3420import Control.Monad

3521import Data.List

@@ -225,15 +211,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

225211 isFieldOrParam' :: (Name, a) -> Bool

226212 isFieldOrParam' = isFieldOrParam . fst

227213

228− isField :: Name -> Bool

229− isField = flip elem fieldNames

230−

231− isField' :: (Name, a, b, c, d, f) -> Bool

232− isField' (n, _, _, _, _, _) = isField n

233−

234− fieldTerms :: [PTerm]

235− fieldTerms = [t | (_, _, _, t, _) <- fields]

236−

237214 -- Delabs the TT to PTerm

238215 -- This is not good.

239216 -- However, for machine generated implicits, there seems to be no PTerm available.

@@ -252,13 +229,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

252229 freeName (NS n s) = NS (freeName n) s

253230 freeName n = n

254231

255− -- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.

256− zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]

257− zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')

258− zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])

259− where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring

260− zipParams _ [] [] = []

261−

262232 paramName :: Name -> Name

263233 paramName (UN n) = sUN ("param_" ++ str n)

264234 paramName (MN i n) = sMN i ("param_" ++ str n)

@@ -295,15 +265,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

295265 fieldDep :: Name -> PTerm -> (Name, [Name])

296266 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

297267

298− -- | A list of fields depending on another field.

299− dependentFields :: [Name]

300− dependentFields = filter depends fieldNames

301− where

302− depends :: Name -> Bool

303− depends n = case lookup n fieldDependencies of

304− Just xs -> not $ null xs

305− Nothing -> False

306−

307268 -- | A list of fields depended on by other fields.

308269 dependedOn :: [Name]

309270 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

src/Idris/Elab/Rewrite.hs−3

@@ -10,7 +10,6 @@ Maintainer : The Idris Community.

1010module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

1413import Idris.Core.Elaborate

1514import Idris.Core.Evaluate

1615import Idris.Core.TT

@@ -20,8 +19,6 @@ import Idris.Error

2019

2120import Control.Monad

2221import Control.Monad.State.Strict

23−import Data.List

24−import Debug.Trace

2522

2623elabRewrite :: (PTerm -> ElabD ()) -> IState ->

2724 FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

src/Idris/Elab/RunElab.hs+1−3

@@ -9,14 +9,12 @@ module Idris.Elab.RunElab (elabRunElab) where

99

1010import Idris.AbsSyntax

1111import Idris.Core.Elaborate hiding (Tactic(..))

12−import Idris.Core.Evaluate

13−import Idris.Core.Execute

1412import Idris.Core.TT

1513import Idris.Core.Typecheck

1614import Idris.Elab.Term

1715import Idris.Elab.Value (elabVal)

1816import Idris.Error

19−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

17+import Idris.Output (sendHighlighting)

2018

2119elabScriptTy :: Type

2220elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)

src/Idris/Elab/Term.hs+5−61

@@ -10,40 +10,34 @@ Maintainer : The Idris Community.

1010module Idris.Elab.Term where

1111

1212import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14−import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)

13+import Idris.Core.CaseTree (SC'(STerm), findCalls)

1514import Idris.Core.Elaborate hiding (Tactic(..))

1615import Idris.Core.Evaluate

1716import Idris.Core.ProofTerm (getProofTerm)

1817import Idris.Core.TT

1918import Idris.Core.Typecheck (check, converts, isType, recheck)

2019import Idris.Core.Unify

21−import Idris.Core.WHNF (whnf, whnfArgs)

22−import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)

20+import Idris.Core.WHNF (whnf)

21+import Idris.Coverage (genClauses, recoverableCoverage)

2322import Idris.Delaborate

24−import Idris.DSL

2523import Idris.Elab.Quasiquote (extractUnquotes)

2624import Idris.Elab.Rewrite

2725import Idris.Elab.Utils

2826import Idris.Error

2927import Idris.ErrReverse (errReverse)

3028import Idris.Options

31−import Idris.Output (pshow)

3229import Idris.ProofSearch

3330import Idris.Reflection

3431import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)

3532

36−import qualified Util.Pretty as U

37−

3833import Control.Applicative ((<$>))

3934import Control.Monad

4035import Control.Monad.State.Strict

4136import Data.Foldable (for_)

4237import Data.List

4338import qualified Data.Map as M

44−import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)

39+import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

4540import qualified Data.Set as S

46−import qualified Data.Text as T

4741import Debug.Trace

4842

4943data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS

@@ -85,7 +79,6 @@ build :: IState

8579 -> ElabD ElabResult

8680build ist info emode opts fn tm

8781 = do elab ist info emode opts fn tm

88− let tmIn = tm

8982 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

9083 [TIPartial] -> True

9184 _ -> False

@@ -163,8 +156,7 @@ buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

163156 PTerm ->

164157 ElabD ElabResult

165158buildTC ist info emode opts fn ns tm

166− = do let tmIn = tm

167− let inf = case lookupCtxt fn (idris_tyinfodata ist) of

159+ = do let inf = case lookupCtxt fn (idris_tyinfodata ist) of

168160 [TIPartial] -> True

169161 _ -> False

170162 -- set name supply to begin after highest index in tm

@@ -190,7 +182,6 @@ buildTC ist info emode opts fn ns tm

190182 if (log /= "")

191183 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

192184 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

193− where pattern = emode == ELHS || emode == EImpossible

194185

195186-- | return whether arguments of the given constructor name can be

196187-- matched on. If they're polymorphic, no, unless the type has beed

@@ -247,7 +238,6 @@ elab ist info emode opts fn tm

247238 = do let loglvl = opt_logLevel (idris_options ist)

248239 when (loglvl > 5) $ unifyLog True

249240 compute -- expand type synonyms, etc

250− let fc = maybe "(unknown)"

251241 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

252242 est <- getAux

253243 sequence_ (get_delayed_elab est)

@@ -283,14 +273,6 @@ elab ist info emode opts fn tm

283273 Placeholder -> (True, priority arg)

284274 tm -> (False, priority arg)

285275

286− toElab ina arg = case getTm arg of

287− Placeholder -> Nothing

288− v -> Just (priority arg, elabE ina (elabFC info) v)

289−

290− toElab' ina arg = case getTm arg of

291− Placeholder -> Nothing

292− v -> Just (elabE ina (elabFC info) v)

293−

294276 mkPat = do hs <- get_holes

295277 tm <- get_term

296278 case hs of

@@ -356,18 +338,6 @@ elab ist info emode opts fn tm

356338 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

357339 notDelay _ = True

358340

359− local f = do e <- get_env

360− return (f `elem` map fstEnv e)

361−

362− -- | Is a constant a type?

363− constType :: Const -> Bool

364− constType (AType _) = True

365− constType StrType = True

366− constType VoidType = True

367− constType _ = False

368−

369− -- "guarded" means immediately under a constructor, to help find patvars

370−

371341 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

372342 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

373343 -> PTerm -- ^ The term to elaborate

@@ -603,13 +573,6 @@ elab ist info emode opts fn tm

603573 (P _ n' _, _) -> n == n'

604574 _ -> False

605575

606− showQuick (CantUnify _ (l, _) (r, _) _ _ _)

607− = show (l, r)

608− showQuick (ElaboratingArg _ _ _ e) = showQuick e

609− showQuick (At _ e) = showQuick e

610− showQuick (ProofSearchFail (Msg _)) = "search fail"

611− showQuick _ = "No chance"

612−

613576 elab' ina _ (PPatvar fc n) | bindfree

614577 = do patvar n

615578 update_term liftPats

@@ -627,8 +590,6 @@ elab ist info emode opts fn tm

627590 = do ty <- goal

628591 testImplicitWarning fc n ty

629592 let ina = e_inarg ec

630− guarded = e_guarded ec

631− inty = e_intype ec

632593 ctxt <- get_context

633594 env <- get_env

634595

@@ -890,7 +851,6 @@ elab ist info emode opts fn tm

890851 _ -> do mapM_ setInjective (map getTm args)

891852 -- maybe more things are solvable now

892853 unifyProblems

893− let guarded = isConName f ctxt

894854-- trace ("args is " ++ show args) $ return ()

895855 ns <- apply (Var f) (map isph args)

896856-- trace ("ns is " ++ show ns) $ return ()

@@ -1000,10 +960,6 @@ elab ist info emode opts fn tm

1000960 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

1001961 | otherwise = getDets (i + 1) ds as

1002962

1003− tacTm (PTactics _) = True

1004− tacTm (PProof _) = True

1005− tacTm _ = False

1006−

1007963 setInjective (PRef _ _ n) = setinj n

1008964 setInjective (PApp _ (PRef _ _ n) _) = setinj n

1009965 setInjective _ = return ()

@@ -1078,7 +1034,6 @@ elab ist info emode opts fn tm

10781034 matchProblems True

10791035 args <- get_env

10801036 envU <- mapM (getKind args) args

1081− let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

10821037

10831038 -- Drop the unique arguments used in the term already

10841039 -- and in the scrutinee (since it's

@@ -1156,12 +1111,6 @@ elab ist info emode opts fn tm

11561111 UType AllTypes -> return (n, True)

11571112 _ -> return (n, False)

11581113

1159− tcName tm | (P _ n _, _) <- unApply tm

1160− = case lookupCtxt n (idris_interfaces ist) of

1161− [_] -> True

1162− _ -> False

1163− tcName _ = False

1164−

11651114 isNotLift env n

11661115 = case lookupBinder n env of

11671116 Just ty ->

@@ -1170,10 +1119,6 @@ elab ist info emode opts fn tm

11701119 _ -> False

11711120 _ -> False

11721121

1173− usedIn ns (n, b)

1174− = n `elem` ns

1175− || any (\x -> x `elem` ns) (allTTNames (binderTy b))

1176−

11771122 elab' ina fc (PUnifyLog t) = do unifyLog True

11781123 elab' ina fc t

11791124 unifyLog False

@@ -2716,7 +2661,6 @@ processTacticDecls info steps =

27162661

27172662 RDatatypeDefnInstrs tyn tyconTy ctors ->

27182663 do let cn (n, _, _) = n

2719− cimpls (_, impls, _) = impls

27202664 cty (_, _, t) = t

27212665 addIBC (IBCDef tyn)

27222666 mapM_ (addIBC . IBCDef . cn) ctors

src/Idris/Elab/Transform.hs+1−30

@@ -9,47 +9,19 @@ Maintainer : The Idris Community.

99module Idris.Elab.Transform where

1010

1111import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

1412import Idris.Core.Elaborate hiding (Tactic(..))

15−import Idris.Core.Evaluate

16−import Idris.Core.Execute

1713import Idris.Core.TT

1814import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22−import Idris.Delaborate

23−import Idris.Docstrings

24−import Idris.DSL

2515import Idris.Elab.Term

2616import Idris.Elab.Utils

2717import Idris.Error

28−import Idris.Imports

29−import Idris.Inliner

30−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

31−import Idris.PartialEval

32−import Idris.Primitives

33−import Idris.Providers

34−import IRTS.Lang

35−

36−import Util.Pretty (pretty, text)

18+import Idris.Output (sendHighlighting)

3719

3820import Prelude hiding (id, (.))

3921

40−import Control.Applicative hiding (Const)

4122import Control.Category

42−import Control.DeepSeq

4323import Control.Monad

4424import Control.Monad.State.Strict as State

45−import Data.Char (isLetter, toLower)

46−import Data.List

47−import Data.List.Split (splitOn)

48−import qualified Data.Map as Map

49−import Data.Maybe

50−import qualified Data.Set as S

51−import qualified Data.Text as T

52−import Debug.Trace

5325

5426elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

5527elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

@@ -66,7 +38,6 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

6638 sendHighlighting highlights

6739 updateIState $ \i -> i { idris_name = newGName }

6840 let lhs_tm = orderPats (getInferTerm lhs')

69− let lhs_ty = getInferType lhs'

7041 let newargs = pvars i lhs_tm

7142

7243 (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

src/Idris/Elab/Type.hs+1−41

@@ -13,50 +13,23 @@ module Idris.Elab.Type (

1313

1414import Idris.AbsSyntax

1515import Idris.ASTUtils

16−import Idris.Core.CaseTree

1716import Idris.Core.Elaborate hiding (Tactic(..))

1817import Idris.Core.Evaluate

19−import Idris.Core.Execute

2018import Idris.Core.TT

21−import Idris.Core.Typecheck

2219import Idris.Core.WHNF

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

2720import Idris.Docstrings (Docstring)

28−import Idris.DSL

2921import Idris.Elab.Term

3022import Idris.Elab.Utils

3123import Idris.Elab.Value

3224import Idris.Error

33−import Idris.Imports

34−import Idris.Inliner

3525import Idris.Options

36−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

37−import Idris.PartialEval

38−import Idris.Primitives

39−import Idris.Providers

40−import IRTS.Lang

41−

42−import Util.Pretty (pretty, text)

26+import Idris.Output (sendHighlighting)

4327

4428import Prelude hiding (id, (.))

4529

46−import Control.Applicative hiding (Const)

4730import Control.Category

48−import Control.DeepSeq

4931import Control.Monad

50−import Control.Monad.State.Strict as State

51−import Data.Char (isLetter, toLower)

52−import Data.List

53−import Data.List.Split (splitOn)

54−import qualified Data.Map as Map

55−import Data.Maybe

5632import qualified Data.Set as S

57−import qualified Data.Text as T

58−import qualified Data.Traversable as Traversable

59−import Debug.Trace

6033

6134buildType :: ElabInfo

6235 -> SyntaxInfo

@@ -196,11 +169,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

196169 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

197170

198171 let (fam, _) = unApply (getRetTy nty')

199− let corec = case fam of

200− P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

201− [TI _ True _ _ _ _] -> True

202− _ -> False

203− _ -> False

204172 -- Productivity checking now via checking for guarded 'Delay'

205173 let opts' = opts -- if corec then (Coinductive : opts) else opts

206174 let usety = if norm then nty' else nty

@@ -251,14 +219,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

251219 _ -> return ()

252220 return usety

253221 where

254− -- for making an internalapp, we only want the explicit ones, and don't

255− -- want the parameters, so just take the arguments which correspond to the

256− -- user declared explicit ones

257− mergeTy (PPi e n fc ty sc) (PPi e' n' _ _ sc')

258− | e == e' = PPi e n fc ty (mergeTy sc sc')

259− | otherwise = mergeTy sc sc'

260− mergeTy _ sc = sc

261−

262222 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

263223

264224 err = txt "Err"

src/Idris/Elab/Utils.hs+1−6

@@ -14,7 +14,6 @@ import Idris.Core.Evaluate

1414import Idris.Core.TT

1515import Idris.Core.Typecheck

1616import Idris.Core.WHNF

17−import Idris.DeepSeq

1817import Idris.Delaborate

1918import Idris.Docstrings

2019import Idris.Error

@@ -22,14 +21,11 @@ import Idris.Output

2221

2322import Util.Pretty

2423

25−import Control.Applicative hiding (Const)

2624import Control.Monad

2725import Control.Monad.State

2826import Data.List

2927import qualified Data.Map as Map

3028import Data.Maybe

31−import qualified Data.Traversable as Traversable

32−import Debug.Trace

3329

3430recheckC = recheckC_borrowing False True []

3531

@@ -122,7 +118,6 @@ elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

122118elabCaseBlock info opts d@(PClauses f o n ps)

123119 = do addIBC (IBCDef n)

124120 logElab 5 $ "CASE BLOCK: " ++ show (n, d)

125− let opts' = nub (o ++ opts)

126121 -- propagate totality assertion to the new definitions

127122 let opts' = filter propagatable opts

128123 setFlags n opts'

@@ -750,7 +745,7 @@ pruneByType _ _ t _ _ as = as

750745-- to it later - just returns 'var' for now. EB)

751746isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

752747isPlausible ist var env n ty

753− = let (hvar, interfaces) = collectConstraints [] [] ty in

748+ = let (hvar, _) = collectConstraints [] [] ty in

754749 case hvar of

755750 Nothing -> True

756751 Just rth -> var -- trace (show (rth, interfaces)) var

src/Idris/Elab/Value.hs+2−30

@@ -13,48 +13,20 @@ module Idris.Elab.Value(

1313 ) where

1414

1515import Idris.AbsSyntax

16−import Idris.ASTUtils

17−import Idris.Core.CaseTree

1816import Idris.Core.Elaborate hiding (Tactic(..))

1917import Idris.Core.Evaluate hiding (Unchecked)

20−import Idris.Core.Execute

2118import Idris.Core.TT

22−import Idris.Core.Typecheck

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

2719import Idris.Docstrings

28−import Idris.DSL

2920import Idris.Elab.Term

3021import Idris.Elab.Utils

3122import Idris.Error

32−import Idris.Imports

33−import Idris.Inliner

34−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

35−import Idris.PartialEval

36−import Idris.Primitives

37−import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

23+import Idris.Output (sendHighlighting)

4124

4225import Prelude hiding (id, (.))

4326

44−import Control.Applicative hiding (Const)

4527import Control.Category

46−import Control.DeepSeq

47−import Control.Monad

48−import Control.Monad.State.Strict as State

49−import Data.Char (isLetter, toLower)

50−import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

53−import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

28+import Data.Char (toLower)

5629import qualified Data.Traversable as Traversable

57−import Debug.Trace

5830

5931-- | Elaborate a value, returning any new bindings created (this will only

6032-- happen if elaborating as a pattern clause)

src/Idris/ElabDecls.hs+3−32

@@ -12,20 +12,10 @@ Maintainer : The Idris Community.

1212module Idris.ElabDecls where

1313

1414import Idris.AbsSyntax

15−import Idris.ASTUtils

16−import Idris.Core.CaseTree

17−import Idris.Core.Elaborate hiding (Tactic(..))

1815import Idris.Core.Evaluate

19−import Idris.Core.Execute

2016import Idris.Core.TT

21−import Idris.Core.Typecheck

22−import Idris.Coverage

23−import Idris.DataOpts

24−import Idris.DeepSeq

25−import Idris.Delaborate

2617import Idris.Directives

2718import Idris.Docstrings hiding (Unchecked)

28−import Idris.DSL

2919import Idris.Elab.Clause

3020import Idris.Elab.Data

3121import Idris.Elab.Implementation

@@ -36,36 +26,21 @@ import Idris.Elab.RunElab

3626import Idris.Elab.Term

3727import Idris.Elab.Transform

3828import Idris.Elab.Type

39−import Idris.Elab.Utils

4029import Idris.Elab.Value

4130import Idris.Error

42−import Idris.Imports

43−import Idris.Inliner

4431import Idris.Options

45−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

46−import Idris.PartialEval

32+import Idris.Output (sendHighlighting)

4733import Idris.Primitives

48−import Idris.Providers

4934import Idris.Termination

5035import IRTS.Lang

5136

52−import Util.Pretty (pretty, text)

53−

5437import Prelude hiding (id, (.))

5538

56−import Control.Applicative hiding (Const)

5739import Control.Category

58−import Control.DeepSeq

5940import Control.Monad

6041import Control.Monad.State.Strict as State

61−import Data.Char (isLetter, toLower)

62−import Data.List

63−import Data.List.Split (splitOn)

64−import qualified Data.Map as Map

6542import Data.Maybe

66−import qualified Data.Set as S

6743import qualified Data.Text as T

68−import Debug.Trace

6944

7045-- | Top level elaborator info, supporting recursive elaboration

7146recinfo :: FC -> ElabInfo

@@ -269,12 +244,6 @@ elabDecl' what info (PParams f ns ps)

269244 let nblock = pblock i

270245 mapM_ (elabDecl' what info) nblock

271246 where

272− pinfo = let ds = concatMap tldeclared ps

273− newps = params info ++ ns

274− dsParams = map (\n -> (n, map fst newps)) ds

275− newb = addAlist dsParams (inblock info) in

276− info { params = newps,

277− inblock = newb }

278247 pblock i = map (expandParamsD False i id ns

279248 (concatMap tldeclared ps)) ps

280249

@@ -311,6 +280,8 @@ elabDecl' _ info (PDSL n dsl)

311280 ifail "You must turn on the DSLNotation extension to use a dsl block"

312281 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

313282 addIBC (IBCDSL n)

283+elabDecl' what info (PDirective i@(DLogging _))

284+ = directiveAction i

314285elabDecl' what info (PDirective i)

315286 | what /= EDefns = directiveAction i

316287elabDecl' what info (PProvider doc syn fc nfc provWhat n)

src/Idris/Erasure.hs−7

@@ -20,7 +20,6 @@ import Idris.Primitives

2020

2121import Prelude hiding (id, (.))

2222

23−import Control.Applicative

2423import Control.Arrow

2524import Control.Category

2625import Control.Monad.State

@@ -36,8 +35,6 @@ import Data.Set (Set)

3635import qualified Data.Set as S

3736import Data.Text (pack)

3837import qualified Data.Text as T

39−import Debug.Trace

40−import System.IO.Unsafe

4138

4239-- | UseMap maps names to the set of used (reachable) argument

4340-- positions.

@@ -290,7 +287,6 @@ buildDepMap ci used externs ctx startNames

290287 -- mini-DSL for postulates

291288 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

292289 it n is = [(sUN n, Arg i) | i <- is]

293− mn n is = [(MN 0 $ pack n, Arg i) | i <- is]

294290

295291 -- believe_me is special because it does not use all its arguments

296292 specialPrims = S.fromList [sUN "prim__believe_me"]

@@ -627,9 +623,6 @@ buildDepMap ci used externs ctx startNames

627623 union :: Deps -> Deps -> Deps

628624 union = M.unionWith (M.unionWith S.union)

629625

630− unions :: [Deps] -> Deps

631− unions = M.unionsWith (M.unionWith S.union)

632−

633626 unionMap :: (a -> Deps) -> [a] -> Deps

634627 unionMap f = M.unionsWith (M.unionWith S.union) . map f

635628

src/Idris/ErrReverse.hs−12

@@ -12,10 +12,8 @@ module Idris.ErrReverse(errReverse) where

1212import Idris.AbsSyntax

1313import Idris.Core.Evaluate (unfold)

1414import Idris.Core.TT

15−import Util.Pretty

1615

1716import Data.List

18−import Debug.Trace

1917

2018-- | For display purposes, apply any 'error reversal' transformations

2119-- so that errors will be more readable,

@@ -73,13 +71,3 @@ errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)

7371 Just (fs ++ as)

7472 -- no matching Binds, for now...

7573 match' ns x y = if x == y then Just [] else Nothing

76−

77− -- if the term under a lambda is huge, there's no much point in showing

78− -- it as it won't be very enlightening.

79−

80− elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

81− elideLambdas (Bind n (Lam _ t) sc)

82− | size sc > 200 = P Ref (sUN "...") Erased

83− elideLambdas (Bind n b sc)

84− = Bind n (fmap elideLambdas b) (elideLambdas sc)

85− elideLambdas t = t

src/Idris/Error.hs−7

@@ -14,23 +14,16 @@ import Idris.AbsSyntax

1414import Idris.Core.Constraints

1515import Idris.Core.Evaluate (ctxtAlist)

1616import Idris.Core.TT

17−import Idris.Core.Typecheck

1817import Idris.Delaborate

1918import Idris.Output

2019

2120import Prelude hiding (catch)

2221

2322import Control.Monad (when)

24−import Control.Monad.State.Strict

25−import Data.Char

2623import qualified Data.Foldable as Foldable

2724import Data.List (intercalate, isPrefixOf)

2825import qualified Data.Set as S

2926import qualified Data.Text as T

30−import qualified Data.Traversable as Traversable

31−import Data.Typeable

32−import System.Console.Haskeline

33−import System.Console.Haskeline.MonadException

3427import System.IO.Error (ioeGetErrorString, isUserError)

3528

3629iucheck :: Idris ()

src/Idris/IBC.hs+26−31

@@ -5,20 +5,20 @@ Copyright :

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

89{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}

910{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11+{-# OPTIONS_GHC -fwarn-unused-imports #-}

1012

1113module Idris.IBC (loadIBC, loadPkgIndex,

1214 writeIBC, writePkgIndex,

1315 hasValidIBCVersion, IBCPhase(..)) where

1416

1517import Idris.AbsSyntax

16−import Idris.Core.Binary

1718import Idris.Core.CaseTree

1819import Idris.Core.Evaluate

1920import Idris.Core.TT

20−import Idris.DeepSeq

21−import Idris.Delaborate

21+import Idris.DeepSeq ()

2222import Idris.Docstrings (Docstring)

2323import qualified Idris.Docstrings as D

2424import Idris.Error

@@ -27,23 +27,15 @@ import Idris.Options

2727import Idris.Output

2828import IRTS.System (getIdrisLibDir)

2929

30−import Paths_idris

31−

3230import qualified Cheapskate.Types as CT

3331import Codec.Archive.Zip

3432import Control.DeepSeq

3533import Control.Monad

36−import Control.Monad.State.Strict hiding (get, put)

37−import qualified Control.Monad.State.Strict as ST

3834import Data.Binary

3935import Data.ByteString.Lazy as B hiding (elem, length, map)

40−import Data.Functor

4136import Data.List as L

4237import Data.Maybe (catMaybes)

4338import qualified Data.Set as S

44−import qualified Data.Text as T

45−import Data.Vector.Binary

46−import Debug.Trace

4739import System.Directory

4840import System.FilePath

4941

@@ -59,7 +51,6 @@ data IBCPhase = IBC_Building -- ^ when building the module tree

5951data IBCFile = IBCFile {

6052 ver :: Word16

6153 , sourcefile :: FilePath

62− , ibc_reachablenames :: ![Name]

6354 , ibc_imports :: ![(Bool, FilePath)]

6455 , ibc_importdirs :: ![FilePath]

6556 , ibc_sourcedirs :: ![FilePath]

@@ -116,7 +107,7 @@ deriving instance Binary IBCFile

116107!-}

117108

118109initIBC :: IBCFile

119−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

110+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

120111

121112hasValidIBCVersion :: FilePath -> Idris Bool

122113hasValidIBCVersion fp = do

@@ -131,7 +122,9 @@ loadIBC :: Bool -- ^ True = reexport, False = make everything private

131122 -> IBCPhase

132123 -> FilePath -> Idris ()

133124loadIBC reexport phase fp

134− = do imps <- getImported

125+ = do logIBC 1 $ "loadIBC (reexport, phase, fp)" ++ show (reexport, phase, fp)

126+ imps <- getImported

127+ logIBC 3 $ "loadIBC imps" ++ show imps

135128 case lookup fp imps of

136129 Nothing -> load True

137130 Just p -> if (not p && reexport) then load False else return ()

@@ -517,13 +510,16 @@ processImports reexp phase fname ar = do

517510 ibcsd <- valIBCSubDir i

518511 ids <- rankedImportDirs fname

519512 putIState (i { imported = f : imported i })

520− let phase' = case phase of

521− IBC_REPL _ -> IBC_REPL False

522− p -> p

513+ let (phase', reexp') =

514+ case phase of

515+ IBC_REPL True -> (IBC_REPL False, reexp)

516+ IBC_REPL False -> (IBC_Building, reexp && re)

517+ p -> (p, reexp && re)

523518 fp <- findIBC ids ibcsd f

519+ logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')

524520 case fp of

525521 Nothing -> do logIBC 2 $ "Failed to load ibc " ++ f

526− Just fn -> do loadIBC (reexp && re) phase' fn) fs

522+ Just fn -> do loadIBC reexp' phase' fn) fs

527523

528524processImplicits :: Archive -> Idris ()

529525processImplicits ar = do

@@ -639,6 +635,7 @@ processPatternDefs ar = do

639635processDefs :: Archive -> Idris ()

640636processDefs ar = do

641637 ds <- getEntry [] "ibc_defs" ar

638+ logIBC 4 $ "processDefs ds" ++ show ds

642639 mapM_ (\ (n, d) -> do

643640 d' <- updateDef d

644641 case d' of

@@ -735,8 +732,11 @@ processAccess :: Bool -- ^ Reexporting?

735732 -> IBCPhase

736733 -> Archive -> Idris ()

737734processAccess reexp phase ar = do

735+ logIBC 3 $ "processAccess (reexp, phase)" ++ show (reexp, phase)

738736 ds <- getEntry [] "ibc_access" ar

737+ logIBC 3 $ "processAccess ds" ++ show ds

739738 mapM_ (\ (n, a_in) -> do

739+

740740 let a = if reexp then a_in else Hidden

741741 logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

742742 updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })

@@ -745,10 +745,15 @@ processAccess reexp phase ar = do

745745 then do

746746 logIBC 2 $ "Not exporting " ++ show n

747747 setAccessibility n Hidden

748− else logIBC 2 $ "Exporting " ++ show n

748+ else

749+ logIBC 2 $ "Exporting " ++ show n

750+

749751 -- Everything should be available at the REPL from

750− -- things imported publicly

751− when (phase == IBC_REPL True) $ setAccessibility n Public) ds

752+ -- things imported publicly.

753+ when (phase == IBC_REPL True) $ do

754+ logIBC 2 $ "Top level, exporting " ++ show n

755+ setAccessibility n Public

756+ ) ds

752757

753758processFlags :: Archive -> Idris ()

754759processFlags ar = do

@@ -1117,16 +1122,6 @@ instance Binary Accessibility where

11171122 3 -> return Hidden

11181123 _ -> error "Corrupted binary data for Accessibility"

11191124

1120−safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

1121−safeToEnum label x' = result

1122− where

1123− x = fromIntegral x'

1124− result

1125− | x < fromEnum (minBound `asTypeOf` result)

1126− || x > fromEnum (maxBound `asTypeOf` result)

1127− = error $ label ++ ": corrupted binary representation in IBC"

1128− | otherwise = toEnum x

1129−

11301125instance Binary PReason where

11311126 put x

11321127 = case x of

src/Idris/IdeMode.hs+1−4

@@ -11,7 +11,7 @@ Maintainer : The Idris Community.

1111

1212module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where

1313

14−import Idris.Core.Binary

14+import Idris.Core.Binary ()

1515import Idris.Core.TT

1616

1717import Control.Applicative hiding (Const)

@@ -176,9 +176,6 @@ instance SExpable OutputAnnotation where

176176encodeName :: Name -> String

177177encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

178178

179−decodeName :: String -> Name

180−decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

181−

182179encodeTerm :: [(Name, Bool)] -> Term -> String

183180encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

184181 (bnd, tm)

src/Idris/IdrisDoc.hs+4−16

@@ -10,11 +10,10 @@ Maintainer : The Idris Community.

1010module Idris.IdrisDoc (generateDocs) where

1111

1212import Idris.AbsSyntax

13−import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName,

14− isFnName, isTConName, lookupDefAcc)

15−import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),

16− TextFormatting(..), constIsType, nsroot, sUN, str,

17− toAlist, txt)

13+import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName,

14+ isTConName, lookupDefAcc)

15+import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..),

16+ constIsType, nsroot, sUN, str, toAlist, txt)

1817import Idris.Docs

1918import Idris.Docstrings (nullDocstring)

2019import qualified Idris.Docstrings as Docstrings

@@ -26,17 +25,13 @@ import Control.Applicative ((<|>))

2625import Control.Monad (forM_)

2726import Control.Monad.Trans.Except

2827import Control.Monad.Trans.State.Strict

29−import qualified Data.ByteString as BS

3028import qualified Data.ByteString.Lazy as BS2

3129import qualified Data.List as L

32−import qualified Data.List.Split as LS

3330import qualified Data.Map as M hiding ((!))

3431import Data.Maybe

3532import Data.Monoid (mempty)

36−import qualified Data.Ord (compare)

3733import qualified Data.Set as S

3834import qualified Data.Text as T

39−import qualified Data.Text.Encoding as E

4035import System.Directory

4136import System.FilePath

4237import System.IO

@@ -253,13 +248,6 @@ getAccess ist n =

253248 [(_, acc)] -> acc

254249 _ -> Private

255250

256−-- | Simple predicate for whether an NsItem has Docs

257−hasDoc :: NsItem -- ^ The NsItem to test

258− -> Bool -- ^ The result

259−hasDoc (_, Just _, _) = True

260−hasDoc _ = False

261−

262−

263251-- | Predicate saying whether a Name possibly may have docs defined

264252-- Without this, getDocs from Idris.Docs may fail a pattern match.

265253mayHaveDocs :: Name -- ^ The Name to test

src/Idris/Imports.hs+2−3

@@ -13,7 +13,6 @@ module Idris.Imports(

1313import Idris.AbsSyntax

1414import Idris.Core.TT

1515import Idris.Error

16−import Idris.Output

1716import IRTS.System (getIdrisLibDir)

1817

1918import Control.Applicative ((<$>))

@@ -30,13 +29,13 @@ pkgIndex :: String -> FilePath

3029pkgIndex s = "00" ++ s ++ "-idx.ibc"

3130

3231srcPath :: FilePath -> FilePath

33−srcPath fp = let (n, ext) = splitExtension fp in

32+srcPath fp = let (_, ext) = splitExtension fp in

3433 case ext of

3534 ".idr" -> fp

3635 _ -> fp ++ ".idr"

3736

3837lsrcPath :: FilePath -> FilePath

39−lsrcPath fp = let (n, ext) = splitExtension fp in

38+lsrcPath fp = let (_, ext) = splitExtension fp in

4039 case ext of

4140 ".lidr" -> fp

4241 _ -> fp ++ ".lidr"

src/Idris/Info.hs−1

@@ -29,7 +29,6 @@ import Idris.Imports (installedPackages)

2929import Idris.Options (loggingCatsStr)

3030import qualified IRTS.System as S

3131

32−import Paths_idris

3332import Version_idris (gitHash)

3433

3534import Data.Version

src/Idris/Interactive.hs+1−3

@@ -382,9 +382,7 @@ makeLemma fn updatefile l n

382382 StringAtom lem_app]]]

383383 in runIO . hPutStrLn h $ convSExp "return" good n

384384

385− where getIndent s = length (takeWhile isSpace s)

386−

387− appArgs skip 0 _ = ""

385+ where appArgs skip 0 _ = ""

388386 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)

389387 | (thead c /= '_' && n `notElem` skip)

390388 = " " ++ show n ++ appArgs skip (i - 1) sc

src/Idris/ModeCommon.hs+22−23

@@ -4,6 +4,11 @@ Description : Common utilities used by all modes.

44License : BSD3

55Maintainer : The Idris Community.

66-}

7+

8+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

9+{-# OPTIONS_GHC -fwarn-unused-binds #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

11+

712module Idris.ModeCommon where

813

914import Idris.AbsSyntax

@@ -25,16 +30,11 @@ import Prelude hiding (id, (.), (<$>))

2530import Control.Category

2631import Control.DeepSeq

2732import Control.Monad

28−import Control.Monad.Trans.State.Strict (get)

29−import Data.List hiding (group)

30−import Data.Maybe

3133import Network.Socket (PortNumber)

32−import System.Directory

3334

3435defaultPort :: PortNumber

3536defaultPort = fromIntegral 4294

3637

37−

3838loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

3939loadInputs inputs toline -- furthest line to read in input source files

4040 = idrisCatch

@@ -49,6 +49,8 @@ loadInputs inputs toline -- furthest line to read in input source files

4949 [] -> not (NoREPL `elem` opts)

5050 _ -> True

5151

52+ logParser 3 $ show "loadInputs loadCode" ++ show loadCode

53+

5254 -- For each ifile list, check it and build ibcs in the same clean IState

5355 -- so that they don't interfere with each other when checking

5456

@@ -59,6 +61,7 @@ loadInputs inputs toline -- furthest line to read in input source files

5961 let ninputs = zip [1..] inputs

6062 ifiles <- mapWhileOK (\(num, input) ->

6163 do putIState ist

64+ logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)

6265 modTree <- buildTree

6366 (map snd (take (num-1) ninputs))

6467 importlists

@@ -77,9 +80,18 @@ loadInputs inputs toline -- furthest line to read in input source files

7780 case errSpan inew of

7881 Nothing ->

7982 do putIState $!! ist { idris_tyinfodata = tidata }

80− ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))

81−-- logLvl 0 $ "Loading from " ++ show ibcfiles

82− tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)

83+ logParser 3 $ "loadInputs ifiles" ++ show ifiles

84+

85+ let fileToIFileType :: FilePath -> Idris IFileType

86+ fileToIFileType file = do

87+ ibcsd <- valIBCSubDir ist

88+ ids <- rankedImportDirs file

89+ findImport ids ibcsd file

90+

91+ ibcfiles <- mapM fileToIFileType inputs

92+ logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles

93+

94+ tryLoad True (IBC_REPL True) ibcfiles

8395 _ -> return ()

8496 exports <- findExports

8597

@@ -103,6 +115,8 @@ loadInputs inputs toline -- furthest line to read in input source files

103115 tryLoad keepstate phase [] = warnTotality >> return ()

104116 tryLoad keepstate phase (f : fs)

105117 = do ist <- getIState

118+ logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++

119+ show (keepstate, phase, f : fs)

106120 let maxline

107121 = case toline of

108122 Nothing -> Nothing

@@ -142,21 +156,6 @@ loadInputs inputs toline -- furthest line to read in input source files

142156 fmatch xs ('.':'/':ys) = fmatch xs ys

143157 fmatch xs ys = xs == ys

144158

145− findNewIBC :: IFileType -> Idris (Maybe IFileType)

146− findNewIBC i@(IBC _ _) = return (Just i)

147− findNewIBC s@(IDR f) = do ist <- get

148− ibcsd <- valIBCSubDir ist

149− let ibc = ibcPathNoFallback ibcsd f

150− ok <- runIO $ doesFileExist ibc

151− if ok then return (Just (IBC ibc s))

152− else return Nothing

153− findNewIBC s@(LIDR f) = do ist <- get

154− ibcsd <- valIBCSubDir ist

155− let ibc = ibcPathNoFallback ibcsd f

156− ok <- runIO $ doesFileExist ibc

157− if ok then return (Just (IBC ibc s))

158− else return Nothing

159−

160159 -- Like mapM, but give up when there's an error

161160 mapWhileOK f [] = return []

162161 mapWhileOK f (x : xs) = do x' <- f x

src/Idris/Output.hs+2−3

@@ -13,7 +13,7 @@ module Idris.Output where

1313

1414import Idris.AbsSyntax

1515import Idris.Colours (hEndColourise, hStartColourise)

16−import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)

16+import Idris.Core.Evaluate (normaliseAll)

1717import Idris.Core.TT

1818import Idris.Delaborate

1919import Idris.Docstrings

@@ -27,13 +27,12 @@ import Util.System (isATTY)

2727import Prelude hiding ((<$>))

2828

2929import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

30−import Data.Char (isAlpha)

3130import Data.List (intersperse, nub)

3231import Data.Maybe (fromMaybe)

3332import System.Console.Haskeline.MonadException (MonadException(controlIO),

3433 RunIO(RunIO))

3534import System.FilePath (replaceExtension)

36−import System.IO (Handle, hPutStr, hPutStrLn, stdout)

35+import System.IO (Handle, hPutStr, hPutStrLn)

3736

3837instance MonadException m => MonadException (ExceptT Err m) where

3938 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

src/Idris/Package.hs+1−6

@@ -12,7 +12,7 @@ import System.Directory

1212import System.Directory (copyFile, createDirectoryIfMissing)

1313import System.Exit

1414import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,

15− hasExtension, normalise, takeDirectory, takeExtension,

15+ hasExtension, takeDirectory, takeExtension,

1616 takeFileName, (</>))

1717import System.IO

1818import System.Process

@@ -23,10 +23,8 @@ import Control.Monad

2323import Control.Monad.Trans.Except (runExceptT)

2424import Control.Monad.Trans.State.Strict (execStateT)

2525import Data.Either (partitionEithers)

26−import Data.Either (partitionEithers)

2726import Data.List

2827import Data.List.Split (splitOn)

29−import Data.Maybe (fromMaybe)

3028

3129import Idris.AbsSyntax

3230import Idris.Core.TT

@@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain)

3836import Idris.Options

3937import Idris.Output

4038import Idris.Parser (loadModule)

41−import Idris.REPL

4239

4340import Idris.Package.Common

4441import Idris.Package.Parser

@@ -336,11 +333,9 @@ auditPackage True ipkg = do

336333 getIdrisFiles :: FilePath -> IO [FilePath]

337334 getIdrisFiles dir = do

338335 contents <- getDirectoryContents dir

339− let contents' = filter (\fname -> fname /= "." && fname /= "..") contents

340336

341337 -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.

342338

343−

344339 files <- forM contents (findRest dir)

345340 return $ filter (isIdrisFile) (concat files)

346341

src/Idris/Package/Parser.hs−6

@@ -8,19 +8,13 @@ Maintainer : The Idris Community.

88{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}

99module Idris.Package.Parser where

1010

11−import Idris.AbsSyntaxTree

1211import Idris.CmdOptions

13−import Idris.Core.TT

1412import Idris.Package.Common

1513import Idris.Parser.Helpers hiding (stringLiteral)

16−import Idris.REPL

17−

18−import Util.System

1914

2015import Control.Applicative

2116import Control.Monad.State.Strict

2217import Data.List (union)

23−import Data.Maybe (fromJust, isNothing)

2418import System.Directory (doesFileExist)

2519import System.Exit

2620import System.FilePath (isValid, takeExtension, takeFileName)

src/Idris/Parser.hs+7−31

@@ -5,9 +5,13 @@ Copyright :

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

89{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

910 PatternGuards #-}

1011{-# OPTIONS_GHC -O0 #-}

12+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

13+{-# OPTIONS_GHC -fwarn-unused-imports #-}

14+

1115module Idris.Parser(module Idris.Parser,

1216 module Idris.Parser.Expr,

1317 module Idris.Parser.Data,

@@ -17,11 +21,9 @@ module Idris.Parser(module Idris.Parser,

1721import Idris.AbsSyntax hiding (namespace, params)

1822import Idris.Core.Evaluate

1923import Idris.Core.TT

20−import Idris.Coverage

2124import Idris.Delaborate

2225import Idris.Docstrings hiding (Unchecked)

2326import Idris.DSL

24−import Idris.Elab.Term

2527import Idris.Elab.Value

2628import Idris.ElabDecls

2729import Idris.Error

@@ -33,15 +35,11 @@ import Idris.Parser.Data

3335import Idris.Parser.Expr

3436import Idris.Parser.Helpers

3537import Idris.Parser.Ops

36−import Idris.Providers

3738import Idris.Termination

3839import Idris.Unlit

3940

40−import Util.DynamicLinker

4141import qualified Util.Pretty as P

42−import Util.System (readSource, writeSource)

43−

44−import Paths_idris

42+import Util.System (readSource)

4543

4644import Prelude hiding (pi)

4745

@@ -53,24 +51,14 @@ import Data.Char

5351import Data.Foldable (asum)

5452import Data.Function

5553import Data.Generics.Uniplate.Data (descendM)

56−import qualified Data.HashSet as HS

5754import Data.List

5855import qualified Data.List.Split as Spl

5956import qualified Data.Map as M

6057import Data.Maybe

61−import Data.Monoid

6258import Data.Ord

63−import qualified Data.Set as S

6459import qualified Data.Text as T

65−import Debug.Trace

6660import qualified System.Directory as Dir (makeAbsolute)

6761import System.FilePath

68−import System.IO

69−import qualified Text.Parser.Char as Chr

70−import Text.Parser.Expression

71−import Text.Parser.LookAhead

72−import qualified Text.Parser.Token as Tok

73−import qualified Text.Parser.Token.Highlight as Hi

7462import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

7563import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

7664import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

@@ -806,7 +794,6 @@ mutual :: SyntaxInfo -> IdrisParser [PDecl]

806794mutual syn =

807795 do reservedHL "mutual"

808796 openBlock

809− let pvars = syn_params syn

810797 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

811798 closeBlock

812799 fc <- getFC

@@ -1157,7 +1144,6 @@ clause syn

11571144 Just t -> return t

11581145 Nothing -> fail "Invalid clause"

11591146 (do r <- rhs syn n

1160− let ctxt = tt_ctxt ist

11611147 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

11621148 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

11631149 popIndent

@@ -1181,8 +1167,6 @@ clause syn

11811167 fc <- getFC

11821168 n_in <- fst <$> fnName; let n = expandNS syn n_in

11831169 r <- rhs syn n

1184− ist <- get

1185− let ctxt = tt_ctxt ist

11861170 let wsyn = syn { syn_namespace = [] }

11871171 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

11881172 popIndent

@@ -1239,8 +1223,6 @@ clause syn

12391223 wargs <- many (wExpr syn)

12401224 let capp = PApp fc (PRef nfc [nfc] n) args

12411225 (do r <- rhs syn n

1242− ist <- get

1243− let ctxt = tt_ctxt ist

12441226 let wsyn = syn { syn_namespace = [] }

12451227 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

12461228 popIndent

@@ -1585,11 +1567,6 @@ parseImports fname input

15851567 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

15861568 return ((mdoc, mname, ps, mrk'), annots, i)

15871569

1588− imp m = ImportInfo False (toPath m)

1589− Nothing [] NoFC NoFC

1590− ns = Spl.splitOn "."

1591− toPath = foldl1' (</>) . ns

1592−

15931570 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

15941571 addPath [] _ = []

15951572 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

@@ -1685,6 +1662,7 @@ loadModule' f phase

16851662loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

16861663loadFromIFile reexp phase i@(IBC fn src) maxline

16871664 = do logParser 1 $ "Skipping " ++ getSrcFile i

1665+ logParser 3 $ "loadFromIFile i" ++ show i

16881666 idrisCatch (loadIBC reexp phase fn)

16891667 (\err -> ierror $ LoadingFailed fn err)

16901668 where

@@ -1893,8 +1871,6 @@ loadSource lidr f toline

18931871

18941872{-| Adds names to hide list -}

18951873addHides :: Ctxt Accessibility -> Idris ()

1896−addHides xs = do i <- getIState

1897− let defh = default_access i

1898− mapM_ doHide (toAlist xs)

1874+addHides xs = mapM_ doHide (toAlist xs)

18991875 where doHide (n, a) = do setAccessibility n a

19001876 addIBC (IBCAccess n a)

src/Idris/Parser/Data.hs−25

@@ -9,10 +9,8 @@ Maintainer : The Idris Community.

99module Idris.Parser.Data where

1010

1111import Idris.AbsSyntax

12−import Idris.Core.Evaluate

1312import Idris.Core.TT

1413import Idris.Docstrings

15−import Idris.DSL

1614import Idris.Options

1715import Idris.Parser.Expr

1816import Idris.Parser.Helpers

@@ -21,25 +19,11 @@ import Idris.Parser.Ops

2119import Prelude hiding (pi)

2220

2321import Control.Applicative

24−import Control.Monad

2522import Control.Monad.State.Strict

26−import qualified Data.ByteString.UTF8 as UTF8

27−import Data.Char

28−import qualified Data.HashSet as HS

2923import Data.List

30−import qualified Data.List.Split as Spl

3124import Data.Maybe

32−import Data.Monoid

33−import qualified Data.Text as T

34−import Debug.Trace

35−import qualified Text.Parser.Char as Chr

36−import Text.Parser.Expression

37−import Text.Parser.LookAhead

38−import qualified Text.Parser.Token as Tok

39−import qualified Text.Parser.Token.Highlight as Hi

4025import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

4126 stringLiteral, symbol, whiteSpace)

42−import Text.Trifecta.Delta

4327

4428{- | Parses a record type declaration

4529Record ::=

@@ -70,18 +54,9 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

7054 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

7155 <?> "record type declaration"

7256 where

73− getRecNames :: SyntaxInfo -> PTerm -> [Name]

74− getRecNames syn (PPi _ n _ _ sc) = [expandNS syn n, expandNS syn (mkType n)]

75− ++ getRecNames syn sc

76− getRecNames _ _ = []

77−

7857 getName (Just (n, _), _, _, _) = Just n

7958 getName _ = Nothing

8059

81− toFreeze :: Maybe Accessibility -> Maybe Accessibility

82− toFreeze (Just Frozen) = Just Private

83− toFreeze x = x

84−

8560 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

8661 recordBody syn tyn = do

8762 ist <- get

src/Idris/Parser/Expr.hs−12

@@ -21,24 +21,12 @@ import Prelude hiding (pi)

2121import Control.Applicative

2222import Control.Monad

2323import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

25−import Data.Char

2624import Data.Function (on)

27−import qualified Data.HashSet as HS

2825import Data.List

29−import qualified Data.List.Split as Spl

3026import Data.Maybe

31−import Data.Monoid

32−import qualified Data.Text as T

33−import Debug.Trace

34−import qualified Text.Parser.Char as Chr

3527import Text.Parser.Expression

36−import Text.Parser.LookAhead

37−import qualified Text.Parser.Token as Tok

38−import qualified Text.Parser.Token.Highlight as Hi

3928import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

4029 stringLiteral, symbol, whiteSpace)

41−import Text.Trifecta.Delta

4230

4331-- | Allow implicit type declarations

4432allowImp :: SyntaxInfo -> SyntaxInfo

src/Idris/Parser/Helpers.hs−6

@@ -18,8 +18,6 @@ import Idris.Docstrings

1818import Idris.Options

1919import Idris.Output (iWarn)

2020

21−import qualified Util.Pretty as Pretty (text)

22−

2321import Prelude hiding (pi)

2422

2523import Control.Applicative

@@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8

2927import Data.Char

3028import qualified Data.HashSet as HS

3129import Data.List

32−import qualified Data.List.Split as Spl

3330import qualified Data.Map as M

3431import Data.Maybe

35−import Data.Monoid

3632import qualified Data.Text as T

37−import Debug.Trace

3833import System.FilePath

3934import qualified Text.Parser.Char as Chr

40−import Text.Parser.Expression

4135import Text.Parser.LookAhead

4236import qualified Text.Parser.Token as Tok

4337import qualified Text.Parser.Token.Highlight as Hi

src/Idris/Parser/Ops.hs−13

@@ -18,23 +18,10 @@ import Prelude hiding (pi)

1818import Control.Applicative

1919import Control.Monad

2020import Control.Monad.State.Strict

21−import qualified Data.ByteString.UTF8 as UTF8

22−import Data.Char

23−import qualified Data.HashSet as HS

2421import Data.List

25−import qualified Data.List.Split as Spl

26−import Data.Maybe

27−import Data.Monoid

28−import qualified Data.Text as T

29−import Debug.Trace

30−import qualified Text.Parser.Char as Chr

3122import Text.Parser.Expression

32−import Text.Parser.LookAhead

33−import qualified Text.Parser.Token as Tok

34−import qualified Text.Parser.Token.Highlight as Hi

3523import Text.Trifecta hiding (char, charLiteral, natural, span, string,

3624 stringLiteral, symbol, whiteSpace)

37−import Text.Trifecta.Delta

3825

3926-- | Creates table for fixity declarations to build expression parser

4027-- using pre-build and user-defined operator/fixity declarations

src/Idris/PartialEval.hs−7

@@ -19,10 +19,7 @@ import Idris.Core.Evaluate

1919import Idris.Core.TT

2020import Idris.Delaborate

2121

22−import Control.Applicative

2322import Control.Monad.State

24−import Data.Maybe

25−import Debug.Trace

2623

2724-- | Data type representing binding-time annotations for partial evaluation of arguments

2825data PEArgType = ImplicitS Name -- ^ Implicit static argument

@@ -261,10 +258,6 @@ mkNewPats ist d ns newname sname lhs rhs =

261258 mkRHSargs (_ : ns) as = mkRHSargs ns as

262259 mkRHSargs _ _ = []

263260

264− mkSubst :: (Term, Term) -> Maybe (Name, Term)

265− mkSubst (P _ n _, t) = Just (n, t)

266− mkSubst _ = Nothing

267−

268261-- | Creates a new declaration for a specialised function application.

269262-- Simple version at the moment: just create a version which is a direct

270263-- application of the function to be specialised.

src/Idris/Primitives.hs+1−41

@@ -9,7 +9,6 @@ Maintainer : The Idris Community.

99

1010module Idris.Primitives(primitives, Prim(..)) where

1111

12−import Idris.AbsSyntax

1312import Idris.Core.Evaluate

1413import Idris.Core.TT

1514import IRTS.Lang

@@ -18,9 +17,6 @@ import Data.Bits

1817import Data.Char

1918import Data.Function (on)

2019import Data.Int

21−import qualified Data.Vector.Unboxed as V

22−import Data.Word

23−import Debug.Trace

2420

2521data Prim = Prim { p_name :: Name,

2622 p_type :: Type,

@@ -34,10 +30,9 @@ ty :: [Const] -> Const -> Type

3430ty [] x = Constant x

3531ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

3632

37−total, partial, iopartial :: Totality

33+total, partial :: Totality

3834total = Total []

3935partial = Partial NotCovering

40−iopartial = Partial ExternalIO

4136

4237primitives :: [Prim]

4338primitives =

@@ -235,36 +230,6 @@ intConv ity =

235230 (1, LFloatInt ity) total

236231 ]

237232

238−bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim

239−bitcastPrim from to impl prim =

240− Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)

241− (1, prim) total

242−

243−concatWord8 :: (Word8, Word8) -> Word16

244−concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)

245−

246−concatWord16 :: (Word16, Word16) -> Word32

247−concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)

248−

249−concatWord32 :: (Word32, Word32) -> Word64

250−concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)

251−

252−truncWord16 :: Bool -> Word16 -> Word8

253−truncWord16 True x = fromIntegral (x `shiftR` 8)

254−truncWord16 False x = fromIntegral x

255−

256−truncWord32 :: Bool -> Word32 -> Word16

257−truncWord32 True x = fromIntegral (x `shiftR` 16)

258−truncWord32 False x = fromIntegral x

259−

260−truncWord64 :: Bool -> Word64 -> Word32

261−truncWord64 True x = fromIntegral (x `shiftR` 32)

262−truncWord64 False x = fromIntegral x

263−

264−aTyName :: ArithTy -> String

265−aTyName (ATInt t) = intTyName t

266−aTyName ATFloat = "Float"

267−

268233iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

269234iCmp ity op self impl irop totality

270235 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

@@ -295,11 +260,6 @@ bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in

295260 Just $ I i

296261bfBin _ _ = Nothing

297262

298−bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const

299−bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in

300− Just $ I i

301−bcBin _ _ = Nothing

302−

303263bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const

304264bsBin op [Str x, Str y]

305265 = let i = (if op x y then 1 else 0) in

src/Idris/ProofSearch.hs+1−17

@@ -16,21 +16,17 @@ module Idris.ProofSearch(

1616 ) where

1717

1818import Idris.AbsSyntax

19−import Idris.Core.CaseTree

2019import Idris.Core.Elaborate hiding (Tactic(..))

2120import Idris.Core.Evaluate

2221import Idris.Core.TT

23−import Idris.Core.Typecheck

2422import Idris.Core.Unify

2523import Idris.Delaborate

26−import Idris.Error

2724

2825import Control.Applicative ((<$>))

2926import Control.Monad

3027import Control.Monad.State.Strict

3128import Data.List

3229import qualified Data.Set as S

33−import Debug.Trace

3430

3531-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

3632

@@ -52,7 +48,6 @@ trivialHoles psnames ok elab ist

5248 tryAll ((x, _, b):xs)

5349 = do -- if type of x has any holes in it, move on

5450 hs <- get_holes

55− let badhs = hs -- filter (flip notElem holesOK) hs

5651 g <- goal

5752 -- anywhere but the top is okay for a hole, if holesOK set

5853 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

@@ -88,7 +83,6 @@ trivialTCs ok elab ist

8883 tryAll ((x, _, b):xs)

8984 = do -- if type of x has any holes in it, move on

9085 hs <- get_holes

91− let badhs = hs -- filter (flip notElem holesOK) hs

9286 g <- goal

9387 env <- get_env

9488 -- anywhere but the top is okay for a hole, if holesOK set

@@ -233,9 +227,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

233227 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs

234228 notHole _ _ = True

235229

236− inHS hs (P _ n _) = n `elem` hs

237− isHS _ _ = False

238−

239230 toUN t@(P nt (MN i n) ty)

240231 | ('_':xs) <- str n = t

241232 | otherwise = P nt (UN n) ty

@@ -444,12 +435,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

444435 isMeta ns (P _ n _) = n `elem` ns

445436 isMeta _ _ = False

446437

447− notHole hs (P _ n _, c)

448− | (P _ cn _, _) <- unApply (getRetTy c),

449− n `elem` hs && isConName cn (tt_ctxt ist) = False

450− | Constant _ <- c = not (n `elem` hs)

451− notHole _ _ = True

452−

453438 numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

454439

455440 addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn

@@ -487,7 +472,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

487472 | otherwise

488473 = do lams <- introImps

489474 t <- goal

490− let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

491475-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

492476-- else do

493477 -- if there's a hole in the goal, don't even try

@@ -505,7 +489,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

505489-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

506490 mapM_ (\ (_,n) -> do focus n

507491 t' <- goal

508− let (tc', ttype) = unApply (getRetTy t')

492+ let (tc', _) = unApply (getRetTy t')

509493 let got = fst (unApply (getRetTy t))

510494 let depth' = if tc' `elem` tcs

511495 then depth - 1 else depth

src/Idris/Prover.hs+4−7

@@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where

1111-- Hack for GHC 7.10 and earlier compat without CPP or warnings

1212-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

1313import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,

14− concatMap, elem, error, flip, foldl, foldr, fst, id, init,

15− length, lines, map, not, null, repeat, reverse, tail, zip, ($),

16− (&&), (++), (.), (||))

14+ concatMap, elem, error, foldl, foldr, fst, id, init, length,

15+ lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),

16+ (++), (.), (||))

1717

1818import Idris.AbsSyntax

19−import Idris.AbsSyntaxTree

2019import Idris.Completion

2120import Idris.Core.CaseTree

2221import Idris.Core.Elaborate hiding (Tactic(..))

@@ -41,7 +40,6 @@ import Util.Pretty

4140

4241import Control.DeepSeq

4342import Control.Monad.State.Strict

44−import Debug.Trace

4543import System.Console.Haskeline

4644import System.Console.Haskeline.History

4745import System.IO (Handle, hPutStrLn, stdin, stdout)

@@ -166,7 +164,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

166164 iputGoal rendered

167165

168166 where

169− (h : hs) = holes ps -- apparently the pattern guards don't give us this

167+ (h : _) = holes ps -- apparently the pattern guards don't give us this

170168

171169 ppo = ppOptionIst ist

172170

@@ -502,7 +500,6 @@ checkType e prf t = do

502500 putIState ist { tt_ctxt = ctxt' }

503501 (tm, ty) <- elabVal (recinfo proverfc) ERHS t

504502 let ppo = ppOptionIst ist

505− ty' = normaliseC ctxt [] ty

506503 infixes = idris_infixes ist

507504 action = case tm of

508505 TType _ ->

src/Idris/Providers.hs−2

@@ -13,8 +13,6 @@ module Idris.Providers (

1313 ) where

1414

1515import Idris.AbsSyntax

16−import Idris.AbsSyntaxTree

17−import Idris.Core.Evaluate

1816import Idris.Core.TT

1917import Idris.Error

2018

src/Idris/REPL.hs+8−21

@@ -6,6 +6,8 @@ Maintainer : The Idris Community.

66-}

77

88{-# LANGUAGE FlexibleContexts, PatternGuards #-}

9+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

911

1012module Idris.REPL

1113 ( idemodeStart

@@ -49,7 +51,6 @@ import Idris.Core.Execute (execute)

4951import Idris.Core.TT

5052import Idris.Core.Unify

5153import Idris.Core.WHNF

52−import Idris.Coverage

5354import Idris.DataOpts

5455import Idris.Delaborate

5556import Idris.Docs

@@ -99,8 +100,6 @@ import Util.Pretty hiding ((</>))

99100import Util.System

100101import Version_idris (gitHash)

101102

102−import Debug.Trace

103−

104103-- | Run the REPL

105104repl :: IState -- ^ The initial state

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

@@ -404,7 +403,6 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

404403 | (n, (_, i, _, _, _)) <- idris_metavars ist

405404 , not (n `elem` primDefs)

406405 ]

407− let ppo = ppOptionIst ist

408406 -- splitMvs is a list of pairs of names and their split types

409407 let splitMvs = [ (n, (premises, concl, tm))

410408 | (n, i, ty) <- mvTys ist mvs

@@ -422,14 +420,11 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

422420 runIO . hPutStrLn h $

423421 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

424422 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

425− firstOfThree (x, y, z) = x

426− mapThird f xs = map (\(x, y, z) -> (x, y, f z)) xs

427−

428423 -- | Split a function type into a pair of premises, conclusion.

429424 -- Each maintains both the original and delaborated versions.

430425 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

431426 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

432− let (hs, c, pc) = splitPi ist (i - 1) rest in

427+ let (hs, c, _) = splitPi ist (i - 1) rest in

433428 ((n, t, delabTy' ist [] [] t False False True):hs,

434429 c, delabTy' ist [] [] c False False True)

435430 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

@@ -982,7 +977,7 @@ process fn (Check (PRef _ _ n))

982977 = do ctxt <- getContext

983978 ist <- getIState

984979 let ppo = ppOptionIst ist

985− case lookupNames n ctxt of

980+ case lookupVisibleNames n ctxt of

986981 ts@(t:_) ->

987982 case lookup t (idris_metavars ist) of

988983 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

@@ -990,6 +985,9 @@ process fn (Check (PRef _ _ n))

990985 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

991986 [] -> iPrintError $ "No such variable " ++ show n

992987 where

988+ lookupVisibleNames :: Name -> Context -> [Name]

989+ lookupVisibleNames n ctxt = map fst $ lookupCtxtName n (visibleDefinitions ctxt)

990+

993991 showMetavarInfo ppo ist n i

994992 = case lookupTy n (tt_ctxt ist) of

995993 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

@@ -1020,8 +1018,7 @@ process fn (Check t)

10201018 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

10211019 ctxt <- getContext

10221020 ist <- getIState

1023− let ppo = ppOptionIst ist

1024− ty' = if opt_evaltypes (idris_options ist)

1021+ let ty' = if opt_evaltypes (idris_options ist)

10251022 then normaliseC ctxt [] ty

10261023 else ty

10271024 case tm of

@@ -1126,7 +1123,6 @@ process fn (DebugInfo n)

11261123 when (not (null imps)) $ iputStrLn (show imps)

11271124 let d = lookupDefAcc n False (tt_ctxt i)

11281125 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1129− let cg = lookupCtxtName n (idris_callgraph i)

11301126 i <- getIState

11311127 let cg' = lookupCtxtName n (idris_callgraph i)

11321128 sc <- checkSizeChange n

@@ -1457,12 +1453,6 @@ process fn (TransformInfo n)

14571453 ts' = showTrans i ts in

14581454 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

14591455

1460−-- iRenderOutput (pretty lhs)

1461−-- iputStrLn " ==> "

1462−-- iPrintTermWithType (pprintDelab i rhs)

1463−-- iputStrLn "---------------"

1464−-- showTrans i ts

1465−

14661456process fn (PPrint fmt width (PRef _ _ n))

14671457 = do outs <- pprintDef False n

14681458 iPrintResult =<< renderExternal fmt width (vsep outs)

@@ -1470,10 +1460,7 @@ process fn (PPrint fmt width (PRef _ _ n))

14701460

14711461process fn (PPrint fmt width t)

14721462 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1473− ctxt <- getContext

14741463 ist <- getIState

1475− let ppo = ppOptionIst ist

1476− ty' = normaliseC ctxt [] ty

14771464 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

14781465

14791466

src/Idris/REPL/Parser.hs+1−6

@@ -21,17 +21,14 @@ import Idris.REPL.Commands

2121

2222import Control.Applicative

2323import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

2524import Data.Char (isSpace, toLower)

2625import Data.List

2726import Data.List.Split (splitOn)

28−import Debug.Trace

2927import System.Console.ANSI (Color(..))

3028import System.FilePath ((</>))

3129import Text.Parser.Char (anyChar, oneOf)

3230import Text.Parser.Combinators

33−import Text.Trifecta (Result, parseString)

34−import Text.Trifecta.Delta

31+import Text.Trifecta (Result)

3532

3633parseCmd :: IState -> String -> String -> Result (Either String Command)

3734parseCmd i inputname = P.runparser pCmd i inputname . trim

@@ -181,8 +178,6 @@ namespaceArgCmd names command doc =

181178 (names, NamespaceArg, doc, namespaceArg command)

182179exprArgCmd names command doc =

183180 (names, ExprArg, doc, exprArg command)

184−metavarArgCmd names command doc =

185− (names, MetaVarArg, doc, fnNameArg command)

186181optArgCmd names command doc =

187182 (names, OptionArg, doc, optArg command)

188183proofArgCmd names command doc =

src/Idris/Termination.hs+3−11

@@ -15,10 +15,9 @@ import Idris.Core.TT

1515import Idris.Delaborate

1616import Idris.Error

1717import Idris.Options

18−import Idris.Output (iWarn, iputStrLn)

18+import Idris.Output (iWarn)

1919

2020import Control.Monad.State.Strict

21−import Data.Char

2221import Data.Either

2322import Data.List

2423import Data.Maybe

@@ -143,9 +142,6 @@ checkPositive mut_ns (cn, ty')

143142calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

144143calcTotality fc n pats

145144 = do i <- getIState

146− let opts = case lookupCtxt n (idris_flags i) of

147− [fs] -> fs

148− _ -> []

149145 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

150146 (failure : _) -> return failure

151147 _ -> checkSizeChange n

@@ -302,7 +298,7 @@ buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]

302298buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

303299 scgPat (lhs, rhs) = let lhs' = delazy lhs

304300 rhs' = delazy rhs

305− (f, pargs) = unApply (dePat lhs') in

301+ (_, pargs) = unApply (dePat lhs') in

306302 findCalls [] Toplevel (dePat rhs') (patvars lhs')

307303 (zip pargs [0..])

308304

@@ -393,7 +389,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

393389 fccPat cases pvs pargs args g (lhs, rhs)

394390 = let lhs' = delazy lhs

395391 rhs' = delazy rhs

396− (f, pargs_case) = unApply (dePat lhs')

392+ (_, pargs_case) = unApply (dePat lhs')

397393 -- pargs is a pair of a term, and the argument position that

398394 -- term appears in. If any of the arguments to the case block

399395 -- are also on the lhs, we also want those patterns to appear

@@ -545,10 +541,6 @@ checkMP ist topfn i mp = if i > 0

545541 collapse paths

546542 else tryPath 0 [] mp 0

547543 where

548− tryPath' d path mp arg

549− = let res = tryPath d path mp arg in

550− trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res

551−

552544 mkBig (e, d) = (e, 10000)

553545

554546 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

src/Idris/Transforms.hs−3

@@ -16,11 +16,8 @@ module Idris.Transforms(

1616 ) where

1717

1818import Idris.AbsSyntax

19−import Idris.Core.CaseTree

2019import Idris.Core.TT

2120

22−import Debug.Trace

23−

2421transformPats :: IState -> [Either Term (Term, Term)] ->

2522 [Either Term (Term, Term)]

2623transformPats ist ps = map tClause ps where

src/Idris/TypeSearch.hs+2−6

@@ -13,8 +13,7 @@ module Idris.TypeSearch (

1313 , defaultScoreFunction

1414 ) where

1515

16−import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,

17− logLvl, putIState)

16+import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)

1817import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

1918 Idris, InterfaceInfo, OutputMode(..), PTerm,

2019 defaultSyntax, eqTy, implicitAllowed,

@@ -58,7 +57,6 @@ searchByType pkgs pterm = do

5857 mapM_ loadPkgIndex pkgs

5958 pterm' <- addUsingConstraints syn emptyFC pterm

6059 pterm'' <- implicit toplevel syn name pterm'

61− let pterm''' = addImpl [] i pterm''

6260 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

6361 let names = searchUsing searchPred i ty

6462 let names' = take numLimit names

@@ -304,7 +302,7 @@ interfaceUnify interfaceInfo ctxt ty tyTry = do

304302

305303isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

306304isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

307− (clss, args) = unApply ty

305+ (clss, _) = unApply ty

308306 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

309307 getInterfaceName _ = []

310308

@@ -358,8 +356,6 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

358356 usedns = map fst startingHoles

359357 startingHoles = argNames1 ++ argNames2

360358

361− startingTypes = [(retTy1, retTy2)]

362−

363359

364360 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

365361 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types

src/Util/DynamicLinker.hs+16−9

@@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..)

1313 ) where

1414

1515#ifdef IDRIS_FFI

16−import Foreign.LibFFI

17−import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)

1816import System.Directory

19−#ifndef mingw32_HOST_OS

17+#ifdef mingw32_HOST_OS

18+import qualified Control.Exception as Exception (IOException, catch)

19+import Foreign.Ptr (FunPtr, castPtrToFunPtr, nullFunPtr, nullPtr)

20+import System.FilePath.Windows ((</>))

21+import System.Win32.DLL

22+import System.Win32.Types

23+#else

2024import Control.Exception (IOException, throwIO, try)

21−import Data.Array (Array, bounds, inRange, (!))

25+import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)

26+#ifdef linux_HOST_OS

27+import Data.Array (bounds, inRange, (!))

2228import Data.Functor ((<$>))

2329import Data.Maybe (catMaybes)

30+#else

31+import Data.Array (bounds, (!))

32+#endif

2433import System.FilePath.Posix ((</>))

2534import System.Posix.DynamicLinker

2635import Text.Regex.TDFA

27−#else

28−import qualified Control.Exception as Exception (IOException, catch)

29−import System.FilePath.Windows ((</>))

30−import System.Win32.DLL

31−import System.Win32.Types

36+#endif

37+

38+#ifdef mingw32_HOST_OS

3239type DL = HMODULE

3340#endif

3441

stack.yaml+3

@@ -9,6 +9,9 @@ flags:

99 FFI: true

1010 GMP: true

1111

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

1215extra-deps:

1316 - binary-0.8.5.1

1417 - cheapskate-0.1.1

test/TestData.hs+8−2

@@ -71,7 +71,9 @@ testFamiliesData = [

7171 ( 16, ANY ),

7272 ( 17, ANY ),

7373 ( 18, ANY ),

74− ( 19, ANY )]),

74+ ( 19, ANY ),

75+ ( 20, ANY ),

76+ ( 21, ANY )]),

7577 ("bignum", "Bignum",

7678 [ ( 1, ANY ),

7779 ( 2, ANY )]),

@@ -157,7 +159,11 @@ testFamiliesData = [

157159 ( 13, ANY ),

158160 ( 14, C_CG ),

159161 ( 15, ANY ),

160− ( 16, ANY )]),

162+ ( 16, ANY ),

163+-- FIXME: Re-enable interactive017 once it works with and without node.

164+-- FIXME: See https://github.com/idris-lang/Idris-dev/pull/4046#issuecomment-326910042

165+-- ( 17, ANY ),

166+ ( 18, ANY )]),

161167 ("interfaces", "Interfaces",

162168 [ ( 1, ANY ),

163169 ( 2, ANY ),

test/basic020/basic020.idrnew file+42

@@ -0,0 +1,42 @@

1+%default total

2+

3+data Ty = Ctor Int

4+

5+fn : Ty -> Ty

6+fn m@(Ctor _) = y

7+ where

8+ y = m -- from @ pattern

9+

10+asPatternVisibleInWhere : fn (Ctor 42) = Ctor 42

11+asPatternVisibleInWhere = Refl

12+

13+fn2 : Ty -> Ty

14+fn2 m@(Ctor _) = y (Ctor 99)

15+ where

16+ y m = m -- should be the arg `m`, not the @ pattern

17+

18+lhsVariablesShadowAsPattern : fn2 (Ctor 42) = Ctor 99

19+lhsVariablesShadowAsPattern = Refl

20+

21+fn3 : Ty -> Ty

22+fn3 m@(Ctor _) = y (Ctor 99)

23+ where

24+ y m = z

25+ where

26+ z = m -- should be y's arg `m`, not @ pattern

27+

28+nestedWhereShadowsAsPattern : fn3 (Ctor 42) = Ctor 99

29+nestedWhereShadowsAsPattern = Refl

30+

31+fn4 : Ty -> Ty

32+fn4 m@(Ctor _) = y (Ctor 99)

33+ where

34+ y _ = z

35+ where

36+ z = m -- should be @ pattern

37+

38+nestedWhereExposesAsPattern : fn4 (Ctor 42) = Ctor 42

39+nestedWhereExposesAsPattern = Refl

40+

41+main : IO ()

42+main = putStrLn "OK"

test/basic020/expectednew file+1

@@ -0,0 +1 @@

1+OK

test/basic020/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic020.idr -o basic020

3+./basic020

4+rm -f basic020 *.ibc

test/basic021/basic021.idrnew file+13

@@ -0,0 +1,13 @@

1+import Data.IORef

2+

3+count : Nat -> IORef Integer -> IO ()

4+count Z ref

5+ = do x <- readIORef ref

6+ printLn x

7+count (S k) ref

8+ = do modifyIORef ref (+1)

9+ count k ref

10+

11+main : IO ()

12+main = do r <- newIORef 0

13+ count 1000000 r

test/basic021/expectednew file+1

@@ -0,0 +1 @@

1+1000000

test/basic021/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic021.idr -o basic021

3+./basic021

4+rm -f basic021 *.ibc

test/interactive017/runmode 100644 → 100755+1−1

@@ -6,4 +6,4 @@ PATH="../../scripts:$PATH"

66./shebang-node.idr

77./shebang-args.idr aaa

88./shebang-args.idr bbb aaa

9−./shebang-import.idr

9+./shebang-import.idr

test/interactive017/shebang-args.idrmode 100644 → 100755

Only the mode changed.

test/interactive017/shebang-import.idrmode 100644 → 100755

Only the mode changed.

test/interactive017/shebang-node.idrmode 100644 → 100755

Only the mode changed.

test/interactive017/shebang.idrmode 100644 → 100755

Only the mode changed.

test/interactive018/Imported1.idrnew file+10

@@ -0,0 +1,10 @@

1+module Imported1

2+

3+import Imported2

4+

5+imported1_private : a -> a

6+imported1_private = imported2_visible

7+

8+export

9+imported1_visible : a -> a

10+imported1_visible = imported1_private

test/interactive018/Imported2.idrnew file+8

@@ -0,0 +1,8 @@

1+module Imported1

2+

3+imported2_private : a -> a

4+imported2_private a = a

5+

6+export

7+imported2_visible : a -> a

8+imported2_visible a = a

test/interactive018/Public1.idrnew file+10

@@ -0,0 +1,10 @@

1+module Public1

2+

3+import public Public2

4+

5+public1_private : a -> a

6+public1_private a = a

7+

8+export

9+public1_visible : a -> a

10+public1_visible = public1_private

test/interactive018/Public2.idrnew file+8

@@ -0,0 +1,8 @@

1+module Public2

2+

3+public2_private : a -> a

4+public2_private a = a

5+

6+export

7+public2_visible : a -> a

8+public2_visible = public2_private

test/interactive018/Top.idrnew file+11

@@ -0,0 +1,11 @@

1+module Top

2+

3+import Imported1

4+import public Public1

5+

6+top_private : a -> a

7+top_private = imported1_visible

8+

9+export

10+top_visible : a -> a

11+top_visible = public2_visible

test/interactive018/expectednew file+20

@@ -0,0 +1,20 @@

1+1 : Integer

2+top_private : a -> a

3+1 : Integer

4+top_visible : a -> a

5+No such variable imported1_private

6+No such variable imported1_private

7+1 : Integer

8+imported1_visible : a -> a

9+No such variable imported2_private

10+No such variable imported2_private

11+No such variable imported2_visible

12+No such variable imported2_visible

13+No such variable public1_private

14+No such variable public1_private

15+1 : Integer

16+public1_visible : a -> a

17+No such variable public2_private

18+No such variable public2_private

19+1 : Integer

20+public2_visible : a -> a

test/interactive018/inputnew file+20

@@ -0,0 +1,20 @@

1+top_private 1

2+:t top_private

3+top_visible 1

4+:t top_visible

5+imported1_private 1

6+:t imported1_private

7+imported1_visible 1

8+:t imported1_visible

9+imported2_private 1

10+:t imported2_private

11+imported2_visible 1

12+:t imported2_visible

13+public1_private 1

14+:t public1_private

15+public1_visible 1

16+:t public1_visible

17+public2_private 1

18+:t public2_private

19+public2_visible 1

20+:t public2_visible

test/interactive018/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none Top.idr < input

3+rm -f *.ibc