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

CHANGELOG.md+15−2

compare with master

unifiedsplit

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

1# New in 1.1.*

2

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+

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

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

4− 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.

5

18

6# New in 1.1.1

19# New in 1.1.1

7

20

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

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

1module Main where

2

3import Idris.AbsSyntax

4−import Idris.Core.TT

5import Idris.ElabDecls

4import Idris.ElabDecls

6import Idris.Main

5import Idris.Main

7import Idris.Options

6import Idris.Options

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

10

9

11import Util.System

10import Util.System

12

11

13−import Paths_idris

14−

15import Control.Monad

12import Control.Monad

16import System.Environment

13import System.Environment

17import System.Exit

14import System.Exit

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

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

1module Main where

2

3import Idris.AbsSyntax

4−import Idris.Core.TT

5import Idris.ElabDecls

4import Idris.ElabDecls

6import Idris.Main

5import Idris.Main

7import Idris.Options

6import Idris.Options

8import IRTS.CodegenJavaScript

7import IRTS.CodegenJavaScript

9import IRTS.Compiler

8import IRTS.Compiler

10

9

11−import Paths_idris

12−

13import System.Environment

10import System.Environment

14import System.Exit

11import System.Exit

15

12

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

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

1module Main where

2

3import Idris.AbsSyntax

4−import Idris.Core.TT

5import Idris.ElabDecls

4import Idris.ElabDecls

6import Idris.Main

5import Idris.Main

7import Idris.Options

6import Idris.Options

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

11import Paths_idris

10import Paths_idris

12

11

13import Control.Monad

12import Control.Monad

13+

14import System.Environment

15import System.Exit

16

idris.cabal−1

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

226 , Idris.WhoCalls

227 , Idris.CmdOptions

228

229− , IRTS.BCImp

230 , IRTS.Bytecode

229 , IRTS.Bytecode

231 , IRTS.CodegenC

230 , IRTS.CodegenC

232 , IRTS.CodegenCommon

231 , 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,

21 Data.HVect,

22 Data.Complex,

23 Data.Erased,

24+ Data.IORef,

24 Data.List,

25 Data.List,

25 Data.List.Views,

26 Data.List.Views,

26 Data.List.Quantifiers,

27 Data.List.Quantifiers,

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

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

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

10 Empty : Recognise False

11 Fail : Recognise c

12− Expect : Recognise c -> Recognise False

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

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

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

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

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

47||| Positive lookahead. Never consumes input.

48export

49expect : Recognise c -> Recognise False

50−expect = Expect

50+expect = Lookahead True

51

52||| Negative lookahead. Never consumes input.

53export

54reject : Recognise c -> Recognise False

55−reject Empty = Fail

55+reject = Lookahead False

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

62

56

63||| Recognise a specific character

57||| Recognise a specific character

64export

58export

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

113many : Lexer -> Recognise False

107many : Lexer -> Recognise False

114many l = opt (some l)

108many l = opt (some l)

115

109

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.

117export

112export

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

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

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

114+choice xs = foldr Alt Fail xs

120−choice (x :: xs@(_ :: _)) = x <|> choice 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

121

129

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

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

123||| encountered.

131||| encountered.

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

126export

134export

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

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

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

136manyTill 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

129

167

130||| Recognise any character

168||| Recognise any character

131export

169export

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

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

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

176scan Empty idx str = pure idx

214scan Empty idx str = pure idx

177scan Fail idx str = Nothing

215scan Fail idx str = Nothing

178−scan (Expect r) idx str

216+scan (Lookahead positive r) idx str

179− = case scan r idx str of

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

180− Just _ => pure idx

218+ then Just idx

181− Nothing => Nothing

219+ else Nothing

182scan (Pred f) idx str

220scan (Pred f) idx str

183 = do c <- strIndex str idx

221 = do c <- strIndex str idx

184 if f c

222 if f c

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

220||| Recognise a single hexidecimal digit

258||| Recognise a single hexidecimal digit

221export

259export

222hexDigit : Lexer

260hexDigit : Lexer

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

261+hexDigit = pred isHexDigit

224

262

225||| Recognise one or more hexidecimal digits

263||| Recognise one or more hexidecimal digits

226export

264export

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

277spaces : Lexer

315spaces : Lexer

278spaces = some space

316spaces = some space

279

317

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+

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

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

281export

330export

282symbol : Lexer

331symbol : Lexer

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

291||| delimiting lexers

340||| delimiting lexers

292export

341export

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

342surround : (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

295

344

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

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

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

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

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

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

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

326export

375export

327hexLit : Lexer

376hexLit : 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)

329

397

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

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

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

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

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

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

30%default total

31

32untilEOL : Recognise False

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

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

34

35line : String -> Lexer

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

37

38block : String -> String -> Lexer

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

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

40

41data Token = CodeBlock String String String

42 | Any String

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

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

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

41export %inline

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

43+ Grammar tok c1 a ->

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

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

44 Grammar tok (c1 || c2) b

45 Grammar tok (c1 || c2) b

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

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

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

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

47

48

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+

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

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

49||| guaranteed to consume.

58||| guaranteed to consume.

50export

59export

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

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

61+ Grammar tok c2 ty ->

52 Grammar tok (c1 && c2) ty

62 Grammar tok (c1 && c2) ty

53(<|>) = Alt

63(<|>) = Alt

54

64

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.

55export

109export

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

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

57pure = Empty

111pure = Empty

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

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

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

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

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

100

154

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

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

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

159+ (com' : Bool) ->

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

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

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

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

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

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

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

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

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

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

107

165

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

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

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

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

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

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

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

139 -- other branch (and reset commit flag)

197 -- other branch (and reset commit flag)

140 then Failure com msg ts

198 then Failure com msg ts

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

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

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

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

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

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

144 = EmptyRes com val xs

202 = EmptyRes com val xs

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

226 Grammar tok False a

284 Grammar tok False a

227optional p def = p <|> pure def

285optional p def = p <|> pure def

228

286

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

229

290

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

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

231export

292export

main/Main.hs+1−6

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

2

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

4

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

5+import Control.Monad (unless, when)

6−import Data.Foldable (foldrM)

7−import Data.Maybe (fromMaybe)

8

6

9import Idris.AbsSyntax

7import Idris.AbsSyntax

10import Idris.CmdOptions

8import Idris.CmdOptions

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

16

14

17import Util.System (setupBundledCC)

15import Util.System (setupBundledCC)

18

16

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

20−import Util.System (setupBundledCC)

21−

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

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

23processShowOptions opts = runIO $ do

18processShowOptions opts = runIO $ do

24 when (ShowAll `elem` opts) $ showExitIdrisInfo

19 when (ShowAll `elem` opts) $ showExitIdrisInfo

rts/idris_gc.c+7−1

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

50 case CT_BITS64:

51 cl = idris_b64CopyForGC(vm, x);

52 break;

53+ case CT_REF:

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

55+ break;

53 case CT_FWD:

56 case CT_FWD:

54 return x->info.ptr;

57 return x->info.ptr;

55 case CT_RAWDATA:

58 case CT_RAWDATA:

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

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

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

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

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

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

84 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

83 switch(GETTY(heap_item)) {

86 switch(GETTY(heap_item)) {

84 case CT_CON:

87 case CT_CON:

85 ar = ARITY(heap_item);

88 ar = ARITY(heap_item);

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

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

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

89 }

92 }

90 break;

93 break;

94+ case CT_REF:

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

96+ break;

91 case CT_STROFFSET:

97 case CT_STROFFSET:

92 heap_item->info.str_offset->str

98 heap_item->info.str_offset->str

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

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

rts/idris_rts.c+20

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

776 return cl;

777}

778

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+

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

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

780 int i = GETINT(index);

800 int i = GETINT(index);

781 switch(i) {

801 switch(i) {

rts/idris_rts.h+8−2

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

26// Closures

27typedef enum {

28 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,

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

30− CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

30+ CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA

31} ClosureType;

32

33typedef struct Closure *VAL;

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

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

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

403

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+

404// system infox

410// system infox

405// used indices:

411// used indices:

406// 0 returns backend

412// 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

23

24import Idris.Core.TT

25import IRTS.Defunctionalise

26−import IRTS.Lang

27import IRTS.Simplified

26import IRTS.Simplified

28

27

29import Data.Maybe

28import Data.Maybe

src/IRTS/CodegenC.hs+1−16

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

9

10module IRTS.CodegenC (codegenC) where

11

12−import Idris.AbsSyntax

13import Idris.Core.TT

12import Idris.Core.TT

14import IRTS.Bytecode

13import IRTS.Bytecode

15import IRTS.CodegenCommon

14import IRTS.CodegenCommon

16import IRTS.Defunctionalise

15import IRTS.Defunctionalise

17−import IRTS.Lang

18import IRTS.Simplified

16import IRTS.Simplified

19import IRTS.System

17import IRTS.System

20

18

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

24import Data.Bits

22import Data.Bits

25import Data.Char

23import Data.Char

26import Data.List (intercalate, nubBy)

24import Data.List (intercalate, nubBy)

27−import Debug.Trace

28import Numeric

25import Numeric

29−import System.Directory

30import System.Exit

26import System.Exit

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

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

32import System.IO

28import System.IO

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

205 = indent i ++ alloc loc tag ++

201 = indent i ++ alloc loc tag ++

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

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

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

203 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 [] = ""

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

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

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

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

215 alloc Nothing tag

207 alloc Nothing tag

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

305 iCase v (B64 w, bc) =

297 iCase v (B64 w, bc) =

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

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

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

299 ++ 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"

315 showDefS i Nothing = ""

300 showDefS i Nothing = ""

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

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

317

302

src/IRTS/Compiler.hs+3−11

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

10module IRTS.Compiler(compile, generate) where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14import Idris.ASTUtils

13import Idris.ASTUtils

15import Idris.Core.CaseTree

14import Idris.Core.CaseTree

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

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

21import Idris.Output

20import Idris.Output

22import IRTS.CodegenC

21import IRTS.CodegenC

23import IRTS.CodegenCommon

22import IRTS.CodegenCommon

24−import IRTS.CodegenJavaScript

25import IRTS.Defunctionalise

23import IRTS.Defunctionalise

26import IRTS.DumpBC

24import IRTS.DumpBC

27import IRTS.Exports

25import IRTS.Exports

28import IRTS.Inliner

26import IRTS.Inliner

29−import IRTS.Lang

30import IRTS.LangOpts

27import IRTS.LangOpts

31import IRTS.Portable

28import IRTS.Portable

32import IRTS.Simplified

29import IRTS.Simplified

33

30

34import Prelude hiding (id, (.))

31import Prelude hiding (id, (.))

35

32

36−import Control.Applicative

37import Control.Category

33import Control.Category

38import Control.Monad.State

34import Control.Monad.State

39−import Data.IntSet (IntSet)

40−import qualified Data.IntSet as IS

41import Data.List

35import Data.List

42import qualified Data.Map as M

36import qualified Data.Map as M

43−import Data.Maybe

44import Data.Ord

37import Data.Ord

45import qualified Data.Set as S

38import qualified Data.Set as S

46−import Debug.Trace

47import System.Directory

39import System.Directory

48−import System.Environment

49import System.Exit

40import System.Exit

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

51import System.IO

41import System.IO

52import System.Process

42import System.Process

53

43

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

516 = do let l' = toFDesc l

506 = do let l' = toFDesc l

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

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

518 return (l', r')

508 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+

520

512

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

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

522 toFDesc tm

514 toFDesc tm

src/IRTS/Defunctionalise.hs+1−52

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

32import Control.Monad.State

33import Data.List

34import Data.Maybe

35−import Debug.Trace

36

35

37data DExp = DV Name

36data DExp = DV Name

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

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

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

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

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

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

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

167

166

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−

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

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

195

168

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

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

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

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

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

223 = mkApplyCase n ar i

196 = mkApplyCase n ar i

224 | otherwise = []

197 | otherwise = []

225− where dupdate tlarg x = x

226

198

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

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

228mkApplyCase fname n ar

200mkApplyCase fname n ar

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

331-- 'max' branches

303-- 'max' branches

332mkBigCase cn max arg branches

304mkBigCase cn max arg branches

333 | length branches <= max = DChkCase arg branches

305 | 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

306+ | otherwise = 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

358

307

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

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

360groupsOf x [] = []

309groupsOf x [] = []

src/IRTS/DumpBC.hs−1

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

9

10import Idris.Core.TT

11import IRTS.Bytecode

12−import IRTS.Lang

13import IRTS.Simplified

12import IRTS.Simplified

14

13

15import Data.List

14import Data.List

src/IRTS/JavaScript/LangTransforms.hs−10

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

12 ) where

13

14

15−import Control.DeepSeq

16−import Control.Monad.Trans.State

17import Data.List

15import Data.List

18import Data.Map.Strict (Map)

16import Data.Map.Strict (Map)

19import qualified Data.Map.Strict as Map

17import qualified Data.Map.Strict as Map

20import Data.Maybe

18import Data.Maybe

21import Data.Set (Set)

19import Data.Set (Set)

22import qualified Data.Set as Set

20import qualified Data.Set as Set

23−import Data.Text (Text)

24−import qualified Data.Text as T

25import Idris.Core.CaseTree

21import Idris.Core.CaseTree

26import Idris.Core.TT

22import Idris.Core.TT

27import IRTS.Lang

23import IRTS.Lang

28

24

29import Data.Data

25import Data.Data

30import Data.Generics.Uniplate.Data

26import Data.Generics.Uniplate.Data

31−import GHC.Generics (Generic)

32

27

33deriving instance Typeable FDesc

28deriving instance Typeable FDesc

34deriving instance Data FDesc

29deriving instance Data FDesc

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

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

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

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

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

51

46

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−

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

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

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

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

59extractGlobs defs (LFun _ _ _ e) =

49extractGlobs defs (LFun _ _ _ e) =

src/IRTS/JavaScript/Name.hs−3

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

20 ) where

21

22import Data.Char

23−import Data.List

24−import qualified Data.Map.Strict as Map

25import Data.Text (Text)

23import Data.Text (Text)

26import qualified Data.Text as T

24import qualified Data.Text as T

27import Idris.Core.TT

25import Idris.Core.TT

28−import IRTS.JavaScript.AST

29

26

30jsEscape :: String -> String

27jsEscape :: String -> String

31jsEscape = concatMap jschar

28jsEscape = concatMap jschar

src/IRTS/JavaScript/PrimOp.hs−4

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

16 , jsPrimCoerce

17 ) where

18

19−import Data.Char

20−import Data.List

21import qualified Data.Map.Strict as Map

19import qualified Data.Map.Strict as Map

22−import Data.Text (Text)

23−import qualified Data.Text as T

24import Idris.Core.TT

20import Idris.Core.TT

25import IRTS.JavaScript.AST

21import IRTS.JavaScript.AST

26import IRTS.Lang

22import IRTS.Lang

src/IRTS/JavaScript/Specialize.hs−14

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

17 , qualifyN

18 ) where

19

20−import Data.Char

21−import Data.List

22import qualified Data.Map.Strict as Map

20import qualified Data.Map.Strict as Map

23−import Data.Text (Text)

24import qualified Data.Text as T

21import qualified Data.Text as T

25import Idris.Core.TT

22import Idris.Core.TT

26import IRTS.JavaScript.AST

23import IRTS.JavaScript.AST

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

62 ]

59 ]

63 -- constructors

60 -- constructors

64 where

61 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

69 trueTest = id

62 trueTest = id

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

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

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

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

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

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

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

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

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

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

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

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

78 -- projections

67 -- projections

79− justProj x n = x

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

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

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

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

83 item :: String

69 item :: String

84 -> String

70 -> String

src/IRTS/Lang.hs−2

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

13import Idris.Core.CaseTree

14import Idris.Core.TT

15

16−import Control.Applicative hiding (Const)

17import Control.Monad.State hiding (lift)

16import Control.Monad.State hiding (lift)

18import Data.Data (Data)

17import Data.Data (Data)

19import Data.List

18import Data.List

20import Data.Typeable (Typeable)

19import Data.Typeable (Typeable)

21−import Debug.Trace

22import GHC.Generics (Generic)

20import GHC.Generics (Generic)

23

21

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

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

src/IRTS/LangOpts.hs−4

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

9

10module IRTS.LangOpts where

11

12−import Idris.Core.CaseTree

13import Idris.Core.TT

12import Idris.Core.TT

14import IRTS.Lang

13import IRTS.Lang

15

14

16−import Control.Applicative hiding (Const)

17import Control.Monad.State hiding (lift)

15import Control.Monad.State hiding (lift)

18−import Data.List

19−import Debug.Trace

20

16

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

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

22inlineAll lds = let defs = addAlist lds emptyContext in

18inlineAll lds = let defs = addAlist lds emptyContext in

src/IRTS/Portable.hs−2

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

14import IRTS.Bytecode

15import IRTS.CodegenCommon

16import IRTS.Defunctionalise

17−import IRTS.Lang

18import IRTS.Simplified

17import IRTS.Simplified

19

18

20import Data.Aeson

19import Data.Aeson

21import qualified Data.ByteString.Lazy as B

20import qualified Data.ByteString.Lazy as B

22−import qualified Data.Text as T

23import System.IO

21import System.IO

24

22

25data CodegenFile = CGFile {

23data CodegenFile = CGFile {

src/IRTS/Simplified.hs−3

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

10

11import Idris.Core.CaseTree

12import Idris.Core.TT

13−import Idris.Core.Typecheck

14import IRTS.Defunctionalise

13import IRTS.Defunctionalise

15

14

16import Control.Monad.State

15import Control.Monad.State

17−import Data.Maybe

18−import Debug.Trace

19

16

20data SExp = SV LVar

17data SExp = SV LVar

21 | SApp Bool Name [LVar]

18 | SApp Bool Name [LVar]

src/Idris/ASTUtils.hs−1

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

52

53import Prelude hiding (id, (.))

54

55−import Control.Applicative

56import Control.Category

55import Control.Category

57import Control.Monad.State.Class

56import Control.Monad.State.Class

58import Data.Maybe

57import Data.Maybe

src/Idris/AbsSyntax.hs+4−34

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

7-}

8

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

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

10

11

11module Idris.AbsSyntax(

12module Idris.AbsSyntax(

12 module Idris.AbsSyntax

13 module Idris.AbsSyntax

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

39

40

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

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

41

42

42−import Debug.Trace

43import Util.DynamicLinker

44import Util.Pretty

45import Util.System

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

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

598

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

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

600+getImported = idris_imported `fmap` getIState

601

602setErrSpan :: FC -> Idris ()

603setErrSpan x = do i <- getIState;

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

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

1466-- * finally, everything else (3)

1467getPriority :: IState -> PTerm -> Int

1468−getPriority i tm = 1 -- pri tm

1468+getPriority i tm = 1

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−

1490

1469

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

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

1492addStatics n tm ptm =

1471addStatics n tm ptm =

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

2013 unqualified (NS _ _) = False

1992 unqualified (NS _ _) = False

2014 unqualified _ = True

1993 unqualified _ = True

2015

1994

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

2017− constructor _ = False

2018−

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

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

2020

1996

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

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

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

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

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

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

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

2204 -- impossbility checking.

2180 -- impossbility checking.

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

2206− canBeDConName fn ctxt

2181+ | canBeDConName fn ctxt

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

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

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

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

2210− getFn _ = Nothing

2211 su (PApp fc f args)

2183 su (PApp fc f args)

2212 = PHidden (PApp fc f args)

2184 = PHidden (PApp fc f args)

2213 su (PAlternative ms b alts)

2185 su (PAlternative ms b alts)

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

2264 (ns, ss)

2236 (ns, ss)

2265 fs _ = ([], [])

2237 fs _ = ([], [])

2266

2238

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

2268−

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

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

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

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

2271 spos <- get

2241 spos <- get

src/Idris/AbsSyntaxTree.hs−16

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

46import Data.Traversable (Traversable)

47import Data.Typeable

48import GHC.Generics (Generic)

49−import Network.Socket (PortNumber)

50

49

51

50

52data ElabWhat = ETypes | EDefns | EAll

51data ElabWhat = ETypes | EDefns | EAll

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

2201 showbasic (MN i s) = str s

2200 showbasic (MN i s) = str s

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

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

2203 showbasic (SN s) = show s

2202 showbasic (SN s) = show s

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

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

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

2206 case ctxt' of

2204 case ctxt' of

2207 Nothing -> name

2205 Nothing -> name

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

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

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

2350 put (imps, n: fns)

2348 put (imps, n: fns)

2351

2349

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−

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

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

2367 | not (n `elem` env)

2351 | not (n `elem` env)

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

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

src/Idris/Apropos.hs+1−7

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

11import Idris.AbsSyntax

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

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

14− Type, lookupCtxtExact, toAlist)

14+ toAlist)

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

16

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

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

104

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

106 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(

16import Idris.AbsSyntax

17import Idris.Core.TT

18import Idris.Error

19−import Idris.IBC

20import Idris.Imports

19import Idris.Imports

21import Idris.Parser

20import Idris.Parser

22import Idris.Unlit

21import Idris.Unlit

23

22

24import Control.Monad.State

23import Control.Monad.State

25−import Control.Monad.Trans

26import Data.List

24import Data.List

27import Data.Time.Clock

25import Data.Time.Clock

28−import Debug.Trace

29import System.Directory

26import System.Directory

30−import System.FilePath

31−import Util.System (readSource, writeSource)

27+import Util.System (readSource)

32

28

33data ModuleTree = MTree { mod_path :: IFileType,

29data ModuleTree = MTree { mod_path :: IFileType,

34 mod_needsRecheck :: Bool,

30 mod_needsRecheck :: Bool,

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

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

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

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

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

64

60

65− ibc (IBC _ _) = True

66− ibc _ = False

67−

68 chkReload False p = p

61 chkReload False p = p

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

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

70 chkReload True p = p

63 chkReload True p = p

src/Idris/Completion.hs+11−10

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

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

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

11+

8module Idris.Completion (replCompletion, proverCompletion) where

12module Idris.Completion (replCompletion, proverCompletion) where

9

13

10−import Idris.AbsSyntax (runIO)

14+import Idris.AbsSyntax (getIState, runIO)

11import Idris.AbsSyntaxTree

15import Idris.AbsSyntaxTree

12import Idris.Colours

16import Idris.Colours

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

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

14import Idris.Core.TT

18import Idris.Core.TT

15import Idris.Help

19import Idris.Help

16import Idris.Imports (installedPackages)

20import Idris.Imports (installedPackages)

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

28import System.Console.ANSI (Color)

32import System.Console.ANSI (Color)

29import System.Console.Haskeline

33import System.Console.Haskeline

30

34

35+commands :: [String]

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

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

32

37

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

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

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

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

35 , name <- names ]

40 , name <- names ]

41+

42+tactics :: [String]

36tactics = map fst tacticArgs

43tactics = map fst tacticArgs

37

44

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

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

39names :: Idris [String]

46names :: Idris [String]

40−names = do i <- get

41− let ctxt = tt_ctxt i

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

42 return $

48 return $

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

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

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

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

45 where

51 where

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

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

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

61metavars = do i <- get

67metavars = do i <- get

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

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

63

69

64−

65−modules :: Idris [String]

66−modules = do i <- get

67− return $ map show $ imported i

68−

69namespaces :: Idris [String]

70namespaces :: Idris [String]

70namespaces = do

71namespaces = do

71 ctxt <- fmap tt_ctxt get

72 ctxt <- fmap tt_ctxt get

src/Idris/Core/Binary.hs−4

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

13import Idris.Core.TT

14

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

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

17import Control.Monad (liftM2)

16import Control.Monad (liftM2)

18import Data.Binary

17import Data.Binary

19import Data.Binary.Get

18import Data.Binary.Get

20import Data.Binary.Put

19import Data.Binary.Put

21−import qualified Data.Text as T

22−import qualified Data.Text.Encoding as E

23−import Data.Vector.Binary

24

20

25instance Binary ErrorReportPart where

21instance Binary ErrorReportPart where

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

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

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

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

31

32import Idris.Core.TT

33

34−import Control.Applicative hiding (Const)

35import Control.Monad.Reader

34import Control.Monad.Reader

36import Control.Monad.State

35import Control.Monad.State

37import Data.List hiding (partition)

36import Data.List hiding (partition)

38import qualified Data.List (partition)

37import qualified Data.List (partition)

39−import Data.Maybe

40import qualified Data.Set as S

38import qualified Data.Set as S

41−import Debug.Trace

42import GHC.Generics (Generic)

39import GHC.Generics (Generic)

43

40

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

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

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

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

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

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

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

127 length as == length (nub as) &&

124 length as == length (nub as) &&

128− termsize n t < 10

125+ termsize n t < 20

129

126

130namesUsed :: SC -> [Name]

127namesUsed :: SC -> [Name]

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

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

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

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

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

272 sc' tc defcase phase fc cs

269 sc' tc defcase phase fc cs

273 = let proj = phase == RunTime

270 = let proj = phase == RunTime

274− vnames = fstT (head cs)

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

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

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

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

277 chkPats = mapM chkAccessible pats in

273 chkPats = mapM chkAccessible pats in

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

288 else return t

284 else return t

289 Error err -> Error (At fc err)

285 Error err -> Error (At fc err)

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

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

291− defaultCase True = STerm Erased

292− defaultCase False = UnmatchedCase "Error"

293 fstT (x, _, _) = x

287 fstT (x, _, _) = x

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

295

288

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

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

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

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

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

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

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

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

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

308

301

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−

351data Pat = PCon Bool Name Int [Pat]

302data Pat = PCon Bool Name Int [Pat]

352 | PConst Const

303 | PConst Const

353 | PInferred Pat

304 | PInferred Pat

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

403

354

404 toPat' _ t = PAny

355 toPat' _ t = PAny

405

356

406− fixedN IT8 = "Bits8"

407− fixedN IT16 = "Bits16"

408− fixedN IT32 = "Bits32"

409− fixedN IT64 = "Bits64"

410−

411−

412data Partition = Cons [Clause]

357data Partition = Cons [Clause]

413 | Vars [Clause]

358 | Vars [Clause]

414 deriving Show

359 deriving Show

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

666 where

611 where

667 (acc, inacc) = partitionAcc r

612 (acc, inacc) = partitionAcc r

668

613

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

670− uniq i n = n

671−

672getVar :: String -> CaseBuilder Name

614getVar :: String -> CaseBuilder Name

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

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

674

616

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

872 = SucCase sn (mkForceSC n arg rhs)

814 = SucCase sn (mkForceSC n arg rhs)

873 mkForceAlt n arg (DefaultCase rhs)

815 mkForceAlt n arg (DefaultCase rhs)

874 = DefaultCase (mkForceSC n arg rhs)

816 = 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.

8-}

9module Idris.Core.Constraints ( ucheck ) where

10

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

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

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

12+ UExp(..))

13

14−import Control.Applicative

15import Control.Monad.State.Strict

14import Control.Monad.State.Strict

16import Data.List (partition)

15import Data.List (partition)

17import qualified Data.Map.Strict as M

16import qualified Data.Map.Strict as M

18import qualified Data.Set as S

17import qualified Data.Set as S

19−import Debug.Trace

20

18

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

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

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

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

src/Idris/Core/Elaborate.hs−19

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

16 , module Idris.Core.ProofState

17 ) where

18

19−import Idris.Core.DeepSeq

20import Idris.Core.Evaluate

19import Idris.Core.Evaluate

21import Idris.Core.ProofState

20import Idris.Core.ProofState

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

21import 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,

24import Idris.Core.TT

23import Idris.Core.TT

25import Idris.Core.Typecheck

24import Idris.Core.Typecheck

26import Idris.Core.Unify

25import Idris.Core.Unify

27−import Idris.Core.WHNF

28

26

29−import Util.Pretty hiding (fill)

30−

31−import Control.DeepSeq

32import Control.Monad.State.Strict

27import Control.Monad.State.Strict

33−import Data.Char

34import Data.List

28import Data.List

35−import Debug.Trace

36

29

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

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

38 deriving Show

31 deriving Show

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

614 lift $ tfail $ TooManyArguments n

607 lift $ tfail $ TooManyArguments n

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

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

616

609

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

618− when i (movelast n)

619−

620 mkMN n@(MN i _) = n

610 mkMN n@(MN i _) = n

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

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

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

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

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

673 | i = getNonUnify acc is as

663 | i = getNonUnify acc is as

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

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

675

665

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

677−

678

666

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

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

680apply2 fn elabs =

668apply2 fn elabs =

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

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

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

683 elabArgs (map snd args) elabs

671 elabArgs (map snd args) elabs

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

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

685− let (n, hs) = unified p

686 end_unify

673 end_unify

687 solve

674 solve

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

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

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

700 env <- get_env

687 env <- get_env

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

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

702 prep_fill n (map fst claims)

689 prep_fill n (map fst claims)

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

704 elabClaims [] False claims

690 elabClaims [] False claims

705 complete_fill

691 complete_fill

706 end_unify

692 end_unify

707 where

693 where

708− priOrder Nothing Nothing = EQ

709− priOrder Nothing _ = LT

710− priOrder _ Nothing = GT

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

712−

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

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

714 do n <- unique_hole (mkMN n')

695 do n <- unique_hole (mkMN n')

715 when (null claims) (start_unify n)

696 when (null claims) (start_unify n)

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

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

8{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

9{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

9 MultiParamTypeClasses, PatternGuards #-}

10 MultiParamTypeClasses, PatternGuards #-}

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

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

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

11

13

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

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

13 normaliseAll, normaliseBlocking, toValue, quoteTerm,

15 normaliseAll, normaliseBlocking, toValue, quoteTerm,

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

28 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

30 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

29 conGuarded,

31 conGuarded,

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

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

33+ visibleDefinitions,

31 isUniverse, linearCheck, linearCheckArg) where

34 isUniverse, linearCheck, linearCheckArg) where

32

35

33import Idris.Core.CaseTree

36import Idris.Core.CaseTree

34import Idris.Core.TT

37import Idris.Core.TT

35

38

36−import Control.Applicative hiding (Const)

37import Control.Monad.State

39import Control.Monad.State

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

39−import qualified Data.Binary as B

40import Data.List

41import Data.Maybe (listToMaybe)

42−import Debug.Trace

43import GHC.Generics (Generic)

42import GHC.Generics (Generic)

44

43

44+import qualified Data.Map.Strict as Map

45+

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

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

46 nexthole :: Int,

47 nexthole :: Int,

47 blocking :: Bool }

48 blocking :: Bool }

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

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

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

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

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

207

208

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−

218usable :: Bool -- specialising

209usable :: Bool -- specialising

219 -> Bool -- unfolding only

210 -> Bool -- unfolding only

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

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

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

392 evApply ntimes stk top env args f

383 evApply ntimes stk top env args f

393 = apply ntimes stk top env f args

384 = apply ntimes stk top env f args

394

385

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−

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

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

412 = do a' <- sc a

387 = do a' <- sc a

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

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

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

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

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

741 _ -> return False

716 _ -> return False

742

717

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−

750-- CONTEXTS -----------------------------------------------------------------

718-- CONTEXTS -----------------------------------------------------------------

751

719

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

720{-| 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)

983 ( CaseDef args_ct sc_ct _,

951 ( CaseDef args_ct sc_ct _,

984 CaseDef args_rt sc_rt _) ->

952 CaseDef args_rt sc_rt _) ->

985 let inl = alwaysInline -- tcdict

953 let inl = alwaysInline -- tcdict

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

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

987− inlr = inl || small n args_rt sc_rt

988 cdef = CaseDefs (args_ct, sc_ct)

955 cdef = CaseDefs (args_ct, sc_ct)

989 (args_rt, sc_rt)

956 (args_rt, sc_rt)

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

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

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

1152 isConName f ctxt = any (guarded n) as

1119 isConName f ctxt = any (guarded n) as

1153 guarded _ _ = False

1120 guarded _ _ = False

1154

1121

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+

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

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

1156lookupP = lookupP_all False False

1131lookupP = lookupP_all False False

1157

1132

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

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

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

1241 _ -> return ()

1216 _ -> return ()

1242

1217

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−

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

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

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

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

1252tcReducible :: Name -> Context -> Bool

1220tcReducible :: Name -> Context -> Bool

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

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

11module Idris.Core.Execute (execute) where

12

13import Idris.AbsSyntax

14−import Idris.AbsSyntaxTree

15import Idris.Core.CaseTree

14import Idris.Core.CaseTree

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

17import Idris.Core.TT

16import Idris.Core.TT

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

22import Util.DynamicLinker

21import Util.DynamicLinker

23import Util.System

22import Util.System

24

23

25−import Control.Applicative hiding (Const)

26import Control.Exception

24import Control.Exception

27−import Control.Monad hiding (forM)

28import Control.Monad.Trans

25import Control.Monad.Trans

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

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

30import Control.Monad.Trans.State.Strict

27import Control.Monad.Trans.State.Strict

31−import Data.Bits

32import Data.IORef

28import Data.IORef

33−import qualified Data.Map as M

34import Data.Maybe

29import Data.Maybe

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

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

36import Data.Traversable (forM)

31import Data.Traversable (forM)

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

42#ifdef IDRIS_FFI

37#ifdef IDRIS_FFI

43import Foreign.C.String

38import Foreign.C.String

44import Foreign.LibFFI

39import Foreign.LibFFI

45−import Foreign.Marshal.Alloc (free)

46import Foreign.Ptr

40import Foreign.Ptr

47#endif

41#endif

48

42

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

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

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

52#else

46#else

53-- else is rest of file

47-- 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

58

48

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

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

60

50

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

170getExecState :: Exec ExecState

160getExecState :: Exec ExecState

171getExecState = lift get

161getExecState = lift get

172

162

173−putExecState :: ExecState -> Exec ()

174−putExecState = lift . put

175−

176execFail :: Err -> Exec a

163execFail :: Err -> Exec a

177execFail = throwE

164execFail = throwE

178

165

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

481execForeign env ctxt arity ty fn xs onfail

468execForeign env ctxt arity ty fn xs onfail

482 = case foreignFromTT arity ty fn xs of

469 = case foreignFromTT arity ty fn xs of

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

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

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

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

485− drop arity xs) -- rest

472+ drop arity xs) -- rest

486 res <- call ffun (map snd argTs)

473 res <- call ffun (map snd argTs)

487 case res of

474 case res of

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

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

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

710 return $ FFun name argFTyVals (toFDesc ty)

697 return $ FFun name argFTyVals (toFDesc ty)

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

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

712

699

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−

733unEList :: ExecVal -> Maybe [ExecVal]

700unEList :: ExecVal -> Maybe [ExecVal]

734unEList tm = case unApplyV tm of

701unEList tm = case unApplyV tm of

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

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

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

739 (f, args) -> Nothing

706 (f, args) -> Nothing

740

707

741

708

742−toConst :: Term -> Maybe Const

743−toConst (Constant c) = Just c

744−toConst _ = Nothing

745−

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

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

747mapMaybeM f [] = return []

710mapMaybeM f [] = return []

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

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

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

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

28

29import Util.Pretty hiding (fill)

30

31−import Control.Applicative hiding (empty)

32import Control.Arrow ((***))

31import Control.Arrow ((***))

33import Control.Monad.State.Strict

32import Control.Monad.State.Strict

34import Data.List

33import Data.List

35−import Debug.Trace

36

34

37data ProofState = PS { thname :: Name,

35data ProofState = PS { thname :: Name,

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

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

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

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

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

182 do ps <- get

180 do ps <- get

183 let while = while_elaborating ps

181 let while = while_elaborating ps

184− let dont = dontunify ps

185 let inj = injective ps

182 let inj = injective ps

186 traceWhen (unifylog ps)

183 traceWhen (unifylog ps)

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

184 ("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' =

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

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

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

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

496

493

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−

506unifyGoal :: Raw -> RunTactic

494unifyGoal :: Raw -> RunTactic

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

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

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

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

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

529fill :: Raw -> RunTactic

517fill :: Raw -> RunTactic

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

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

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

519 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)

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

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

521+ (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))

540 return $ Bind x (Guess ty val) sc

522 return $ Bind x (Guess ty val) sc

541 where

523 where

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

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

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

552match_fill :: Raw -> RunTactic

534match_fill :: Raw -> RunTactic

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

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

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

536 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)

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

558− (ty, Just ExpectedType)

538+ (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))

563 return $ Bind x (Guess ty val) sc

539 return $ Bind x (Guess ty val) sc

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

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

565

541

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

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

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

574 do let guess = forget val

550 do let guess = forget val

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

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

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

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

577− (ty, Just ExpectedType)

553+ (ty, Just ExpectedType)

578− ps <- get

579− let (uh, uns) = unified ps

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

581 return $ Bind x (Guess ty val) sc

554 return $ Bind x (Guess ty val) sc

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

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

583

556

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

588solve :: RunTactic

561solve :: RunTactic

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

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

590 = do ps <- get

563 = do ps <- get

591− let (uh, uns) = unified ps

592 dropdots <-

564 dropdots <-

593 case lookup x (notunified ps) of

565 case lookup x (notunified ps) of

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

566 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)

605 recents = x : recents ps,

577 recents = x : recents ps,

606 implementations = implementations ps \\ [x],

578 implementations = implementations ps \\ [x],

607 dotted = dropUnified dropdots (dotted ps) })

579 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

609 return locked

581 return locked

610 where dropUnified ddots [] = []

582 where dropUnified ddots [] = []

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

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

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

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

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

631 tryLock hs t@(Bind n b sc)

603 tryLock hs t@(Bind n b sc)

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

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

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

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

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

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

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

636 tryLock hs t = (t, True)

607 tryLock hs t = (t, True)

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

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

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

657 _ -> normalise ctxt env t

628 _ -> normalise ctxt env t

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

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

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

660 case t' of

630 case t' of

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

631 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)

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

663− ps <- get

664− let (uh, uns) = unified ps

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

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

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

667 _ -> lift $ tfail $ CantIntroduce t'

634 _ -> lift $ tfail $ CantIntroduce t'

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

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

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

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

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

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

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

762 let tmt' = normalise ctxt env tmt

729 let tmt' = normalise ctxt env tmt

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

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

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

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

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

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

766 case unApply tmt' of

733 case unApply tmt' of

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

773 _ -> return []

740 _ -> return []

774 let (params, indicies) = splitTyArgs param_pos tyargs

741 let (params, indicies) = splitTyArgs param_pos tyargs

775 let args = getArgTys elimTy

742 let args = getArgTys elimTy

776− let pmargs = take (length params) args

777 let args' = drop (length params) args

743 let args' = drop (length params) args

778− let propTy = head args'

779 let restargs = init $ tail args'

744 let restargs = init $ tail args'

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

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

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

782− let scr = last $ tail args'

783 let indxnames = makeIndexNames indicies

746 let indxnames = makeIndexNames indicies

784 currentNames <- query $ allTTNames . getProofTerm . pterm

747 currentNames <- query $ allTTNames . getProofTerm . pterm

785 let tmnm = case tm of

748 let tmnm = case tm of

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

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

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

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

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

803 tmt'

766 tmt'

804− where scname = sMN 0 "scarg"

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

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

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

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

807 bindConsArgs [] v = v

769 bindConsArgs [] v = v

808 addConsHole (nm, ty) =

770 addConsHole (nm, ty) =

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

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

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

882 return tm

844 return tm

883

845

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

885−

886solve_unified :: RunTactic

846solve_unified :: RunTactic

887solve_unified ctxt env tm =

847solve_unified ctxt env tm =

888 do ps <- get

848 do ps <- get

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

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

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

932updateError ns e = e

892updateError ns e = e

933

893

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−

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

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

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

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

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

896 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(

18

19import Idris.Core.Evaluate

20import Idris.Core.TT

21−import Idris.Core.Typecheck

22

21

23import Control.Monad.State.Strict

22import Control.Monad.State.Strict

24−import Data.List

25−import Debug.Trace

26

23

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

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

28data TermPath = Top

25data TermPath = Top

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

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

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

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

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

200

197

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−

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

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

212-- under Complete applications.

199-- under Complete applications.

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

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

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

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

60-- Work around AMP without CPP

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

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

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

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

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

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

65

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

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

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

69import Control.Monad.State.Strict

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

71import Data.Binary hiding (get, put)

70import Data.Binary hiding (get, put)

72−import qualified Data.Binary as B

73import Data.Char

71import Data.Char

74import Data.Data (Data)

72import Data.Data (Data)

75import Data.Foldable (Foldable)

73import Data.Foldable (Foldable)

76import Data.List hiding (group, insert)

74import Data.List hiding (group, insert)

77import qualified Data.Map.Strict as Map

75import qualified Data.Map.Strict as Map

78import Data.Maybe (listToMaybe)

76import Data.Maybe (listToMaybe)

79−import Data.Monoid (mconcat)

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

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

81import qualified Data.Text as T

78import qualified Data.Text as T

82import Data.Traversable (Traversable)

79import Data.Traversable (Traversable)

83import Data.Typeable (Typeable)

80import Data.Typeable (Typeable)

84−import Data.Vector.Unboxed (Vector)

85−import qualified Data.Vector.Unboxed as V

86import Debug.Trace

81import Debug.Trace

87−import Foreign.Storable (sizeOf)

88import GHC.Generics (Generic)

82import GHC.Generics (Generic)

89import Numeric (showIntAtBase)

83import Numeric (showIntAtBase)

90import Numeric.IEEE (IEEE(identicalIEEE))

84import Numeric.IEEE (IEEE(identicalIEEE))

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

436tfail :: Err -> TC a

430tfail :: Err -> TC a

437tfail e = Error e

431tfail e = Error e

438

432

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−

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

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

447discard f = f >> return ()

434discard f = f >> return ()

448

435

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

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

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

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

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

517

504

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

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

520−

521instance Sized Name where

505instance Sized Name where

522 size (UN n) = 1

506 size (UN n) = 1

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

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

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

704nativeTyWidth IT32 = 32

688nativeTyWidth IT32 = 32

705nativeTyWidth IT64 = 64

689nativeTyWidth IT64 = 64

706

690

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−

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

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

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

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

716 | AType ArithTy | StrType

693 | AType ArithTy | StrType

src/Idris/Core/Typecheck.hs−34

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

13

14import Idris.Core.Evaluate

15import Idris.Core.TT

16−import Idris.Core.WHNF

17

16

18import Control.Monad.State

17import Control.Monad.State

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

20−import Debug.Trace

21

18

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

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

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

20-- 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

208 Just v' -> v'

205 Just v' -> v'

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

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

210

207

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−

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

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

218 (TType su, TType tu) -> do

209 (TType su, TType tu) -> do

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

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

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

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

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

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

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

229

220

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−

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

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

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

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

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

223 (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

264

240

265 checkBinder (Lam rig t)

241 checkBinder (Lam rig t)

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

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

267− let tv' = normalise ctxt env tv

268 convType tcns ctxt env tt

243 convType tcns ctxt env tt

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

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

270 checkBinder (Let t v)

245 checkBinder (Let t v)

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

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

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

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

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

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

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

276− let tv' = normalise ctxt env tv

277 convertsC ctxt env vt tv

251 convertsC ctxt env vt tv

278 convType tcns ctxt env tt

252 convType tcns ctxt env tt

279 return (Let tv vv, tt, vns)

253 return (Let tv vv, tt, vns)

280 checkBinder (NLet t v)

254 checkBinder (NLet t v)

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

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

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

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

283− let tv' = normalise ctxt env tv

284 convertsC ctxt env vt tv

257 convertsC ctxt env vt tv

285 convType tcns ctxt env tt

258 convType tcns ctxt env tt

286 return (NLet tv vv, tt, vns)

259 return (NLet tv vv, tt, vns)

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

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

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

289 | otherwise

262 | otherwise

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

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

291− let tv' = normalise ctxt env tv

292 convType tcns ctxt env tt

264 convType tcns ctxt env tt

293 return (Hole tv, tt, [])

265 return (Hole tv, tt, [])

294 checkBinder (GHole i ns t)

266 checkBinder (GHole i ns t)

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

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

296− let tv' = normalise ctxt env tv

297 convType tcns ctxt env tt

268 convType tcns ctxt env tt

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

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

299 checkBinder (Guess t v)

270 checkBinder (Guess t v)

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

301 | otherwise

272 | otherwise

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

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

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

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

304− let tv' = normalise ctxt env tv

305 convertsC ctxt env vt tv

275 convertsC ctxt env vt tv

306 convType tcns ctxt env tt

276 convType tcns ctxt env tt

307 return (Guess tv vv, tt, vns)

277 return (Guess tv vv, tt, vns)

308 checkBinder (PVar rig t)

278 checkBinder (PVar rig t)

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

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

310− let tv' = normalise ctxt env tv

311 convType tcns ctxt env tt

280 convType tcns ctxt env tt

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

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

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

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

315 checkBinder (PVTy t)

282 checkBinder (PVTy t)

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

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

317− let tv' = normalise ctxt env tv

318 convType tcns ctxt env tt

284 convType tcns ctxt env tt

319 return (PVTy tv, tt, [])

285 return (PVTy tv, tt, [])

320

286

src/Idris/Core/Unify.hs−90

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

22import Idris.Core.Evaluate

23import Idris.Core.TT

24

25−import Control.Monad

26import Control.Monad.State.Strict

25import Control.Monad.State.Strict

27import Data.List

26import Data.List

28import Data.Maybe

27import Data.Maybe

29−import Debug.Trace

30

28

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

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

32-- at the time

30-- at the time

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

39 }

37 }

40 deriving (Eq, Show)

38 deriving (Eq, Show)

41

39

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

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

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

44 Bool, -- ready to retry yet

41 Bool, -- ready to retry yet

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

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

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

57data UInfo = UI Int Fails

54data UInfo = UI Int Fails

58 deriving Show

55 deriving Show

59

56

60−data UResult a = UOK a

61− | UPartOK a

62− | UFail Err

63−

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

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

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

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

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

59cantUnify [] 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 =

191 | otherwise = checkScope ns (x, tm)

184 | otherwise = checkScope ns (x, tm)

192

185

193 checkScope ns (x, tm) =

186 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))

198 let v = highV (-1) tm in

187 let v = highV (-1) tm in

199 if v >= length ns

188 if v >= length ns

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

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

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

190 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)

204

191

205 bind i ns tm

192 bind i ns tm

206 | i < 0 = tm

193 | i < 0 = tm

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

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

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

258 return $ n : ns'

245 return $ n : ns'

259

246

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−

274unify :: Context -> Env ->

247unify :: Context -> Env ->

275 (TT Name, Maybe Provenance) ->

248 (TT Name, Maybe Provenance) ->

276 (TT Name, Maybe Provenance) ->

249 (TT Name, Maybe Provenance) ->

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

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

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

298 Error e -> tfail e

271 Error e -> tfail e

299 where

272 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−

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

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

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

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

306-- injective (P Ref n _)

275-- injective (P Ref n _)

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

327 sc i = do UI s f <- get

296 sc i = do UI s f <- get

328 put (UI (s+i) f)

297 put (UI (s+i) f)

329

298

330− errors :: StateT UInfo TC Bool

331− errors = do UI s f <- get

332− return (not (null f))

333−

334 uplus u1 u2 = do UI s f <- get

299 uplus u1 u2 = do UI s f <- get

335 r <- u1

300 r <- u1

336 UI s f' <- get

301 UI s f' <- get

@@ -342,12 +307,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

342 StateT UInfo

307 StateT UInfo

343 TC [(Name, TT Name)]

308 TC [(Name, TT Name)]

344 un = un' env

309 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))

351

310

352 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

311 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

353 StateT UInfo

312 StateT UInfo

@@ -577,26 +536,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

577 = unifyFail appx appy

536 = unifyFail appx appy

578 checkHeads _ _ = return []

537 checkHeads _ _ = return []

579

538

580− numArgs tm = let (f, args) = unApply tm in length args

581−

582 metavarApp tm = let (f, args) = unApply tm in

539 metavarApp tm = let (f, args) = unApply tm in

583 (metavar f &&

540 (metavar f &&

584 all (\x -> metavarApp x) args

541 all (\x -> metavarApp x) args

585 && nub args == args) ||

542 && nub args == args) ||

586 globmetavar tm

543 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

600

544

601 globmetavar t = case unApply t of

545 globmetavar t = case unApply t of

602 (P _ x _, _) ->

546 (P _ x _, _) ->

@@ -610,14 +554,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

610 (x `elem` holes || holeIn env x))

554 (x `elem` holes || holeIn env x))

611 || globmetavar t

555 || globmetavar t

612 _ -> False

556 _ -> 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

621

557

622 injectiveTC t@(P Ref n _) t'@(P Ref n' _)

558 injectiveTC t@(P Ref n _) t'@(P Ref n' _)

623 | Just ni <- lookupInjectiveExact n ctxt,

559 | Just ni <- lookupInjectiveExact n ctxt,

@@ -682,16 +618,10 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

682 | otherwise = checkScope ns (x, tm)

618 | otherwise = checkScope ns (x, tm)

683

619

684 checkScope ns (x, tm) | pureTerm tm =

620 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))

689 let v = highV (-1) tm in

621 let v = highV (-1) tm in

690 if v >= length ns

622 if v >= length ns

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

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

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

624 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)

695 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

625 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

696

626

697 bind i ns tm

627 bind i ns tm

@@ -710,15 +640,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

710 sc 1

640 sc 1

711 combine env bnames as (ns' ++ bs)

641 combine env bnames as (ns' ++ bs)

712

642

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−

722highV :: Int -> Term -> Int

643highV :: Int -> Term -> Int

723highV i (V j) | j > i = j

644highV i (V j) | j > i = j

724 | otherwise = i

645 | otherwise = i

@@ -726,11 +647,6 @@ highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]

726highV i (App _ f x) = max (highV i f) (highV i x)

647highV i (App _ f x) = max (highV i f) (highV i x)

727highV i _ = i

648highV i _ = i

728

649

729−envPos x i [] = 0

730−envPos x i ((y, _) : ys) | x == y = i

731− | otherwise = envPos x (i + 1) ys

732−

733−

734-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

650-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

735-- more work may help.

651-- more work may help.

736-- FIXME: Depending on how overloading gets used, this may cause problems. Better

652-- FIXME: Depending on how overloading gets used, this may cause problems. Better

@@ -796,9 +712,3 @@ holeIn env n = case lookupBinder n env of

796 Just (Hole _) -> True

712 Just (Hole _) -> True

797 Just (Guess _ _) -> True

713 Just (Guess _ _) -> True

798 _ -> False

714 _ -> 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

12

13import Idris.Core.CaseTree

14import Idris.Core.Evaluate hiding (quote)

15−import qualified Idris.Core.Evaluate as Evaluate

16import Idris.Core.TT

15import Idris.Core.TT

17

16

18−import Debug.Trace

19−

20-- | A stack entry consists of a term and the environment it is to be

17-- | A stack entry consists of a term and the environment it is to be

21-- evaluated in (i.e. it's a thunk)

18-- evaluated in (i.e. it's a thunk)

22type StackEntry = (Term, WEnv)

19type StackEntry = (Term, WEnv)

src/Idris/Coverage.hs−10

@@ -16,14 +16,11 @@ import Idris.Core.TT

16import Idris.Delaborate

17import Idris.Elab.Utils

18import Idris.Error

19−import Idris.Output (iWarn, iputStrLn)

20

19

21import Control.Monad.State.Strict

20import Control.Monad.State.Strict

22import Data.Char

21import Data.Char

23−import Data.Either

24import Data.List

22import Data.List

25import Data.Maybe

23import Data.Maybe

26−import Debug.Trace

27

24

28-- | Generate a pattern from an 'impossible' LHS.

25-- | Generate a pattern from an 'impossible' LHS.

29--

26--

@@ -284,10 +281,6 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)

284 collectConsts (ConstCase c sc) = Just c

281 collectConsts (ConstCase c sc) = Just c

285 collectConsts _ = Nothing

282 collectConsts _ = Nothing

286

283

287− hasDefault (DefaultCase (UnmatchedCase _)) = False

288− hasDefault (DefaultCase _) = True

289− hasDefault _ = False

290−

291 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)

284 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)

292 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of

285 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of

293 (P _ tyn _, _) -> Just tyn

286 (P _ tyn _, _) -> Just tyn

@@ -336,9 +329,6 @@ trimOverlapping sc = trim [] [] sc

336 trimAlts cs nots vn (DefaultCase sc : rest)

329 trimAlts cs nots vn (DefaultCase sc : rest)

337 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest

330 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest

338

331

339− isConMatch c (ConCase cn t args sc) = c == cn

340− isConMatch _ _ = False

341−

342 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]

332 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]

343 substMatch ca [] = []

333 substMatch ca [] = []

344 substMatch (c,args) (ConCase cn t args' sc : _)

334 substMatch (c,args) (ConCase cn t args' sc : _)

src/Idris/DSL.hs+1−4

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

11module Idris.DSL where

12

13import Idris.AbsSyntax

14−import Idris.Core.Evaluate

15import Idris.Core.TT

14import Idris.Core.TT

16

15

17import Control.Monad.State.Strict

16import Control.Monad.State.Strict

18import Data.Generics.Uniplate.Data (transform)

17import Data.Generics.Uniplate.Data (transform)

19−import Debug.Trace

20

18

21debindApp :: SyntaxInfo -> PTerm -> PTerm

19debindApp :: SyntaxInfo -> PTerm -> PTerm

22debindApp syn t = debind (dsl_bind (dsl_info syn)) t

20debindApp syn t = debind (dsl_bind (dsl_info syn)) t

@@ -169,8 +167,7 @@ var dsl n t i = v' i t where

169 setFC fc t = t

167 setFC fc t = t

170

168

171unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

169unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

172−unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

170+unIdiom ap pure fc e@(PApp _ _ _) = mkap (getFn e)

173− mkap (getFn e)

174 where

171 where

175 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

172 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

176 getFn f = (f, [])

173 getFn f = (f, [])

src/Idris/DataOpts.hs−6

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

10module Idris.DataOpts(applyOpts) where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14import Idris.Core.TT

13import Idris.Core.TT

15

14

16−import Control.Applicative

17−import Data.List

18−import Data.Maybe

19−import Debug.Trace

20−

21class Optimisable term where

15class Optimisable term where

22 applyOpts :: term -> Idris term

16 applyOpts :: term -> Idris term

23

17

src/Idris/DeepSeq.hs−1

@@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..))

24

25import Util.DynamicLinker

26

27−import qualified Cheapskate.Types as CT

28import Control.DeepSeq

27import Control.DeepSeq

29import Network.Socket (PortNumber)

28import Network.Socket (PortNumber)

30

29

src/Idris/Delaborate.hs+2−10

@@ -26,10 +26,9 @@ import Prelude hiding ((<$>))

26import Control.Applicative (Alternative((<|>)))

27import Control.Monad.State

28import Data.Generics.Uniplate.Data (transform)

29−import Data.List (intersperse, nub)

29+import Data.List (nub)

30import Data.Maybe (mapMaybe)

31import qualified Data.Text as T

32−import Debug.Trace

33

32

34bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

33bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

35

34

@@ -192,13 +191,6 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

192 de tys env _ (TType i) = PType un

191 de tys env _ (TType i) = PType un

193 de tys env _ (UType u) = PUniverse un u

192 de tys env _ (UType u) = PUniverse un u

194

193

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−

202 deFn tys env (App _ f a) args = deFn tys env f (a:args)

194 deFn tys env (App _ f a) args = deFn tys env f (a:args)

203 deFn tys env (P _ n _) [l,r]

195 deFn tys env (P _ n _) [l,r]

204 | n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)

196 | 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) =

354 then text "Unification failure" <$> showSc i sc

346 then text "Unification failure" <$> showSc i sc

355 else empty

347 else empty

356pprintErr' i (CantConvert x_in y_in env) =

348pprintErr' 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

358 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

350 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

359 (delabSugared i (flagUnique y_ns)) in

351 (delabSugared i (flagUnique y_ns)) in

360 text "Type mismatch between" <>

352 text "Type mismatch between" <>

src/Idris/Directives.hs−1

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

8module Idris.Directives(directiveAction) where

9

10import Idris.AbsSyntax

11−import Idris.ASTUtils

12import Idris.Core.Evaluate

11import Idris.Core.Evaluate

13import Idris.Core.TT

12import Idris.Core.TT

14import Idris.Imports

13import Idris.Imports

src/Idris/Docs.hs−4

@@ -240,10 +240,6 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

240 updateRef nm (PRef fc _ _) = PRef fc [] nm

241 updateRef _ pt = pt

242

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−

247 prettyConstraints =

243 prettyConstraints =

248 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

244 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

249

245

src/Idris/Elab/AsPat.hs+21−10

@@ -10,20 +10,31 @@ module Idris.Elab.AsPat(desugarAs) where

10import Idris.AbsSyntax

11import Idris.Core.TT

12

13−import Control.Applicative

14import Control.Monad.State.Strict

13import Control.Monad.State.Strict

15−import Data.Generics.Uniplate.Data (transformM)

14+import Data.Generics.Uniplate.Data (transformM, universe)

16

15

17-- | Desugar by changing x@y on lhs to let x = y in ... or rhs

16-- | Desugar by changing x@y on lhs to let x = y in ... or rhs

18−desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)

17+desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])

19−desugarAs lhs rhs

18+desugarAs lhs rhs whereblock

20− = let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in

19+ = (lhs', bindOnRight rhs pats, map (bindInWhereDecl pats) whereblock)

21− (lhs', bindPats pats rhs)

22 where

20 where

21+ (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []

22+

23− bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm

23+ bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm

24− bindPats [] rhs = rhs

25− bindPats ((n, fc, tm) : ps) rhs

26− = PLet fc n NoFC Placeholder tm (bindPats ps rhs)

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

27

38

28collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm

39collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm

29collectAs (PAs fc n tm) = do tm' <- collectAs tm

40collectAs (PAs fc n tm) = do tm' <- collectAs tm

src/Idris/Elab/Clause.hs+8−52

@@ -13,51 +13,37 @@ import Idris.ASTUtils

13import Idris.Core.CaseTree

14import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

16import Idris.Core.TT

18import Idris.Core.Typecheck

17import Idris.Core.Typecheck

19import Idris.Core.WHNF

18import Idris.Core.WHNF

20import Idris.Coverage

19import Idris.Coverage

21import Idris.DataOpts

20import Idris.DataOpts

22−import Idris.DeepSeq

21+import Idris.DeepSeq ()

23import Idris.Delaborate

22import Idris.Delaborate

24import Idris.Docstrings hiding (Unchecked)

23import Idris.Docstrings hiding (Unchecked)

25−import Idris.DSL

26import Idris.Elab.AsPat

24import Idris.Elab.AsPat

27import Idris.Elab.Term

25import Idris.Elab.Term

28import Idris.Elab.Transform

26import Idris.Elab.Transform

29import Idris.Elab.Type

27import Idris.Elab.Type

30import Idris.Elab.Utils

28import Idris.Elab.Utils

31import Idris.Error

29import Idris.Error

32−import Idris.Imports

33−import Idris.Inliner

34import Idris.Options

30import Idris.Options

35−import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)

31+import Idris.Output (iputStrLn, pshow, sendHighlighting)

36import Idris.PartialEval

32import Idris.PartialEval

37−import Idris.Primitives

38−import Idris.Providers

39import Idris.Termination

33import Idris.Termination

40import Idris.Transforms

34import Idris.Transforms

41−import IRTS.Lang

42

35

43import Util.Pretty hiding ((<$>))

36import Util.Pretty hiding ((<$>))

44−import Util.Pretty (pretty, text)

45

37

46import Prelude hiding (id, (.))

38import Prelude hiding (id, (.))

47

39

48−import Control.Applicative hiding (Const)

49import Control.Category

40import Control.Category

50import Control.DeepSeq

41import Control.DeepSeq

51import Control.Monad

42import Control.Monad

52import qualified Control.Monad.State.Lazy as LState

43import qualified Control.Monad.State.Lazy as LState

53import Control.Monad.State.Strict as State

44import Control.Monad.State.Strict as State

54−import Data.Char (isLetter, toLower)

55import Data.List

45import Data.List

56−import Data.List.Split (splitOn)

57−import qualified Data.Map as Map

58import Data.Maybe

46import Data.Maybe

59−import qualified Data.Set as S

60−import qualified Data.Text as T

61import Data.Word

47import Data.Word

62import Debug.Trace

48import Debug.Trace

63import Numeric

49import Numeric

@@ -153,12 +139,6 @@ elabClauses info' fc opts n_in cs =

153 -- optimisation applied to LHS

139 -- optimisation applied to LHS

154 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

140 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

155 map debind pats_forced

141 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

162 -- pdef_pe is the one which will get further optimised

142 -- pdef_pe is the one which will get further optimised

163 -- for run-time, with no forcing optimisation of the LHS because

143 -- for run-time, with no forcing optimisation of the LHS because

164 -- the affects erasure. Also, it's partially evaluated

144 -- the affects erasure. Also, it's partially evaluated

@@ -173,8 +153,6 @@ elabClauses info' fc opts n_in cs =

173 -- help with later inlinings.

153 -- help with later inlinings.

174

154

175 ist <- getIState

155 ist <- getIState

176− let pdef_inl = inlineDef ist pdef

177−

178 numArgs <- tclift $ sameLength pdef

156 numArgs <- tclift $ sameLength pdef

179

157

180 case specNames opts of

158 case specNames opts of

@@ -197,7 +175,6 @@ elabClauses info' fc opts n_in cs =

197 missing' <- checkPossibles info fc True n missing

175 missing' <- checkPossibles info fc True n missing

198 -- Filter out the ones which match one of the

176 -- Filter out the ones which match one of the

199 -- given cases (including impossible ones)

177 -- given cases (including impossible ones)

200− let clhs = map getLHS pdef

201 logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++

178 logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++

202 showSep "\n" (map showTmImpls missing') ++

179 showSep "\n" (map showTmImpls missing') ++

203 "\nAgainst: " ++

180 "\nAgainst: " ++

@@ -245,7 +222,6 @@ elabClauses info' fc opts n_in cs =

245 logElab 3 $ "Optimised: " ++ show tree'

222 logElab 3 $ "Optimised: " ++ show tree'

246 ctxt <- getContext

223 ctxt <- getContext

247 ist <- getIState

224 ist <- getIState

248− let opt = idris_optimisation ist

249 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

225 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

250 (idris_patdefs ist) })

226 (idris_patdefs ist) })

251 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

227 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

@@ -315,15 +291,6 @@ elabClauses info' fc opts n_in cs =

315 return ()

291 return ()

316

292

317 where

293 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−

327 checkUndefined n ctxt = case lookupDef n ctxt of

294 checkUndefined n ctxt = case lookupDef n ctxt of

328 [] -> return ()

295 [] -> return ()

329 [TyDecl _ _] -> return ()

296 [TyDecl _ _] -> return ()

@@ -371,7 +338,7 @@ elabClauses info' fc opts n_in cs =

371

338

372 sameLength ((_, x, _) : xs)

339 sameLength ((_, x, _) : xs)

373 = do l <- sameLength xs

340 = do l <- sameLength xs

374− let (f, as) = unApply x

341+ let (_, as) = unApply x

375 if (null xs || l == length as) then return (length as)

342 if (null xs || l == length as) then return (length as)

376 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

343 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

377 sameLength [] = return 0

344 sameLength [] = return 0

@@ -683,11 +650,10 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

683 logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++

650 logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++

684 "\n" ++ show ptm

651 "\n" ++ show ptm

685 return (Left ptm, lhs)

652 return (Left ptm, lhs)

686−elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)

653+elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)

687− = do let tcgen = Dictionary `elem` opts

688− push_estack fname False

654+ = do push_estack fname False

689 ctxt <- getContext

655 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

691

657

692 -- Build the LHS as an "Infer", and pull out its type and

658 -- Build the LHS as an "Infer", and pull out its type and

693 -- pattern bindings

659 -- pattern bindings

@@ -916,8 +882,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

916 pinfo info ns ds i

882 pinfo info ns ds i

917 = let newps = params info ++ ns

883 = let newps = params info ++ ns

918 dsParams = map (\n -> (n, map fst newps)) ds

884 dsParams = map (\n -> (n, map fst newps)) ds

919− newb = addAlist dsParams (inblock info)

885+ newb = addAlist dsParams (inblock info) in

920− l = liftname info in

921 info { params = newps,

886 info { params = newps,

922 inblock = newb,

887 inblock = newb,

923 liftname = id -- (\n -> case lookupCtxt n newb of

888 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

966 isOutsideWith _ = True

931 isOutsideWith _ = True

967

932

968elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

933elabClause 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

971 -- Build the LHS as an "Infer", and pull out its type and

935 -- Build the LHS as an "Infer", and pull out its type and

972 -- pattern bindings

936 -- pattern bindings

973 i <- getIState

937 i <- getIState

@@ -1189,9 +1153,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1189 mkAux pn wname toplhs ns ns' c

1153 mkAux pn wname toplhs ns ns' c

1190 = ifail $ show fc ++ ":badly formed with clause"

1154 = ifail $ show fc ++ ":badly formed with clause"

1191

1155

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−

1195 -- ns, arguments which don't depend on the with argument

1156 -- ns, arguments which don't depend on the with argument

1196 -- ns', arguments which do

1157 -- ns', arguments which do

1197 updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

1158 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)

1215 updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1176 updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1216 = mapPT updateApp tm

1177 = mapPT updateApp tm

1217 where

1178 where

1218− arity (PApp _ _ as) = length as

1219− arity _ = 0

1220−

1221− lhs_arity = arity toplhs

1222−

1223 currentFn fname (PAlternative _ _ as)

1179 currentFn fname (PAlternative _ _ as)

1224 | Just tm <- getApp as = tm

1180 | Just tm <- getApp as = tm

1225 where getApp (tm@(PApp _ (PRef _ _ f) _) : as)

1181 where getApp (tm@(PApp _ (PRef _ _ f) _) : as)

src/Idris/Elab/Data.hs+4−40

@@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

13−import Idris.Core.CaseTree

14−import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.Evaluate

13import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

14import Idris.Core.TT

18import Idris.Core.Typecheck

15import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22import Idris.Delaborate

16import Idris.Delaborate

23import Idris.Docstrings

17import Idris.Docstrings

24−import Idris.DSL

25import Idris.Elab.Rewrite

18import Idris.Elab.Rewrite

26−import Idris.Elab.Term

27import Idris.Elab.Type

19import Idris.Elab.Type

28import Idris.Elab.Utils

20import Idris.Elab.Utils

29import Idris.Elab.Value

21import Idris.Elab.Value

30import Idris.Error

22import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

23+import Idris.Output (iWarn, sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

38

24

39import Util.Pretty

25import Util.Pretty

40

26

41import Prelude hiding (id, (.))

27import Prelude hiding (id, (.))

42

28

43−import Control.Applicative hiding (Const)

44import Control.Category

29import Control.Category

45−import Control.DeepSeq

46import Control.Monad

30import Control.Monad

47import Control.Monad.State.Strict as State

31import Control.Monad.State.Strict as State

48import Data.Char (isLetter, toLower)

32import Data.Char (isLetter, toLower)

49import Data.List

33import Data.List

50−import Data.List.Split (splitOn)

51import qualified Data.Map as Map

34import qualified Data.Map as Map

52import Data.Maybe

35import Data.Maybe

53−import qualified Data.Set as S

54import qualified Data.Text as T

36import qualified Data.Text as T

55−import Debug.Trace

56

37

57warnLC :: FC -> Name -> Idris ()

38warnLC :: FC -> Name -> Idris ()

58warnLC fc n

39warnLC fc n

@@ -61,8 +42,7 @@ warnLC fc n

61

42

62elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

43elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

63elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

44elabData 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))

66 checkUndefined fc n

46 checkUndefined fc n

67 when (implicitable (nsroot n)) $ warnLC fc n

47 when (implicitable (nsroot n)) $ warnLC fc n

68 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

48 (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)

92 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

72 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

93 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

73 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

94 ttag <- getName

74 ttag <- getName

95− let as = map (const (Left (Msg ""))) (getArgTys cty)

96

75

97 ctxt <- getContext

76 ctxt <- getContext

98 let params = findParams n (normalise ctxt [] cty) (map snd cons)

77 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)

170 cinfo info ds

149 cinfo info ds

171 = let newps = params info

150 = let newps = params info

172 dsParams = map (\n -> (n, [])) ds

151 dsParams = map (\n -> (n, [])) ds

173− newb = addAlist dsParams (inblock info)

152+ newb = addAlist dsParams (inblock info) in

174− l = liftname info in

175 info { params = newps,

153 info { params = newps,

176 inblock = newb,

154 inblock = newb,

177 liftname = id -- Is this appropriate?

155 liftname = id -- Is this appropriate?

@@ -245,12 +223,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

245 getTyName (PRef _ _ n) = n == nsroot tn

223 getTyName (PRef _ _ n) = n == nsroot tn

246 getTyName _ = False

224 getTyName _ = False

247

225

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−

254 -- if the constructor is a UniqueType, the datatype must be too

226 -- if the constructor is a UniqueType, the datatype must be too

255 -- (AnyType is fine, since that is checked for uniqueness too)

227 -- (AnyType is fine, since that is checked for uniqueness too)

256 -- if hte contructor is AnyType, the datatype must be at least AnyType

228 -- if hte contructor is AnyType, the datatype must be at least AnyType

@@ -358,7 +330,7 @@ elabCaseFun ind paramPos n ty cons info = do

358 elimLog "Elaborating case function"

330 elimLog "Elaborating case function"

359 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

331 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

360 let (cnstrs, _) = splitPi ty

332 let (cnstrs, _) = splitPi ty

361− let (splittedTy@(pms, idxs)) = splitPms cnstrs

333+ let (pms, idxs) = splitPms cnstrs

362 generalParams <- namePis False pms

334 generalParams <- namePis False pms

363 motiveIdxs <- namePis False idxs

335 motiveIdxs <- namePis False idxs

364 let motive = mkMotive n paramPos generalParams motiveIdxs

336 let motive = mkMotive n paramPos generalParams motiveIdxs

@@ -396,10 +368,6 @@ elabCaseFun ind paramPos n ty cons info = do

396 elimDeclName :: Name

368 elimDeclName :: Name

397 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

369 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

398

370

399− applyNS :: Name -> [String] -> Name

400− applyNS n [] = n

401− applyNS n ns = sNS n ns

402−

403 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

371 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

404 splitPi = splitPi' []

372 splitPi = splitPi' []

405 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

373 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

@@ -440,10 +408,6 @@ elabCaseFun ind paramPos n ty cons info = do

440 simpleName (MN i n) = str n ++ show i

408 simpleName (MN i n) = str n ++ show i

441 simpleName n = show n

409 simpleName n = show n

442

410

443− nameSpaces :: Name -> [String]

444− nameSpaces (NS _ ns) = map str ns

445− nameSpaces _ = []

446−

447 freshName :: String -> EliminatorState Name

411 freshName :: String -> EliminatorState Name

448 freshName key = do

412 freshName key = do

449 nameMap <- get

413 nameMap <- get

src/Idris/Elab/Implementation.hs+2−29

@@ -9,50 +9,27 @@ Maintainer : The Idris Community.

9module Idris.Elab.Implementation(elabImplementation) where

10

11import Idris.AbsSyntax

12−import Idris.ASTUtils

13import Idris.Core.CaseTree

12import Idris.Core.CaseTree

14import Idris.Core.Elaborate hiding (Tactic(..))

13import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.Evaluate

14import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

15import Idris.Core.TT

18−import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22import Idris.Delaborate

16import Idris.Delaborate

23import Idris.Docstrings

17import Idris.Docstrings

24−import Idris.DSL

25−import Idris.Elab.Data

26import Idris.Elab.Term

18import Idris.Elab.Term

27import Idris.Elab.Type

19import Idris.Elab.Type

28import Idris.Elab.Utils

20import Idris.Elab.Utils

29import Idris.Error

21import Idris.Error

30−import Idris.Imports

31−import Idris.Inliner

32−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

22+import Idris.Output (iWarn, sendHighlighting)

33−import Idris.PartialEval

34−import Idris.Primitives

35−import Idris.Providers

36−import IRTS.Lang

37

23

38−import Util.Pretty (pretty, text)

24+import Util.Pretty (text)

39

25

40import Prelude hiding (id, (.))

26import Prelude hiding (id, (.))

41

27

42−import Control.Applicative hiding (Const)

43import Control.Category

28import Control.Category

44−import Control.DeepSeq

45import Control.Monad

29import Control.Monad

46−import Control.Monad.State.Strict as State

47−import Data.Char (isLetter, toLower)

48import Data.List

30import Data.List

49−import Data.List.Split (splitOn)

50−import qualified Data.Map as Map

51import Data.Maybe

31import Data.Maybe

52−import qualified Data.Set as S

53import qualified Data.Text as T

32import qualified Data.Text as T

54−import Debug.Trace

55−

56

33

57elabImplementation :: ElabInfo

34elabImplementation :: ElabInfo

58 -> SyntaxInfo

35 -> SyntaxInfo

@@ -79,7 +56,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

79 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

56 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

80 cs -> tclift $ tfail $ At fc

57 cs -> tclift $ tfail $ At fc

81 (CantResolveAlts (map fst cs))

58 (CantResolveAlts (map fst cs))

82− let constraint = PApp fc (PRef fc [] n) (map pexp ps)

83 let iname = mkiname n (namespace info) ps expn

59 let iname = mkiname n (namespace info) ps expn

84 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

60 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

85 ist <- getIState

61 ist <- getIState

@@ -167,7 +143,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

167 let wbVals_orig = map (decorateid (decorate ns iname)) ds'

143 let wbVals_orig = map (decorateid (decorate ns iname)) ds'

168 ist <- getIState

144 ist <- getIState

169 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

145 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

170− let wb = wbTys ++ wbVals

171

146

172 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

147 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

173 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))

148 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

300 mkMethApp ps (n, _, _, ty)

275 mkMethApp ps (n, _, _, ty)

301 = lamBind 0 ty (papp fc (PRef fc [] n)

276 = lamBind 0 ty (papp fc (PRef fc [] n)

302 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

277 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

303− where

304− needed is p = pname p `elem` map pname is

305

278

306 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

279 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

307 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

280 = 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.

10module Idris.Elab.Interface(elabInterface) where

11

12import Idris.AbsSyntax

13−import Idris.ASTUtils

14−import Idris.Core.CaseTree

15−import Idris.Core.Elaborate hiding (Tactic(..))

16import Idris.Core.Evaluate

13import Idris.Core.Evaluate

17−import Idris.Core.Execute

18import Idris.Core.TT

14import Idris.Core.TT

19−import Idris.Core.Typecheck

20−import Idris.Coverage

21−import Idris.DataOpts

22−import Idris.DeepSeq

23import Idris.Delaborate

15import Idris.Delaborate

24import Idris.Docstrings

16import Idris.Docstrings

25−import Idris.DSL

26import Idris.Elab.Data

17import Idris.Elab.Data

27−import Idris.Elab.Term

28−import Idris.Elab.Type

29import Idris.Elab.Utils

18import Idris.Elab.Utils

30import Idris.Error

19import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

20+import Idris.Output (sendHighlighting)

34−import Idris.PartialEval

35−import Idris.Primitives

36−import Idris.Providers

37−import IRTS.Lang

38−

39−import Util.Pretty (pretty, text)

40

21

41import Prelude hiding (id, (.))

22import Prelude hiding (id, (.))

42

23

43−import Control.Applicative hiding (Const)

44import Control.Category

24import Control.Category

45−import Control.DeepSeq

46import Control.Monad

25import Control.Monad

47−import Control.Monad.State.Strict as State

48−import Data.Char (isLetter, toLower)

49import Data.Generics.Uniplate.Data (transform)

26import Data.Generics.Uniplate.Data (transform)

50import Data.List

27import Data.List

51−import Data.List.Split (splitOn)

52−import qualified Data.Map as Map

53import Data.Maybe

28import Data.Maybe

54−import qualified Data.Set as S

55−import qualified Data.Text as T

56−import Debug.Trace

57−

58

29

59data MArgTy = IA Name | EA Name | CA deriving Show

30data MArgTy = IA Name | EA Name | CA deriving Show

60

31

@@ -123,8 +94,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

123 ims <- mapM (tdecl impps mnames) mdecls

94 ims <- mapM (tdecl impps mnames) mdecls

124 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

95 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

125 (filter clause ds)

96 (filter clause ds)

126− let (methods, imethods)

97+ let imethods = map (\ (x, y, z) -> y) ims

127− = unzip (map (\ (x, y, z) -> (x, y)) ims)

128 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

98 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

129

99

130 addInterface tn (CI cn (map nodoc imethods) defaults idecls

100 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

396 return (PTy doc [] syn fc o m mfc ty',

366 return (PTy doc [] syn fc o m mfc ty',

397 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

367 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

398

368

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−

406 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

369 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

407 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

370 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

408 getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc

371 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

452 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

415 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

453 toExp ns e sc = sc

416 toExp ns e sc = sc

454

417

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−

461-- | Get the docstring corresponding to a member, if one exists

418-- | Get the docstring corresponding to a member, if one exists

462memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

419memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

463memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

420memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

src/Idris/Elab/Provider.hs−27

@@ -9,51 +9,24 @@ Maintainer : The Idris Community.

9module Idris.Elab.Provider(elabProvider) where

10

11import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

14−import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.Evaluate

12import Idris.Core.Evaluate

16import Idris.Core.Execute

13import Idris.Core.Execute

17import Idris.Core.TT

14import Idris.Core.TT

18import Idris.Core.Typecheck

15import Idris.Core.Typecheck

19−import Idris.Coverage

20−import Idris.DataOpts

21−import Idris.DeepSeq

22import Idris.Delaborate

16import Idris.Delaborate

23import Idris.Docstrings

17import Idris.Docstrings

24−import Idris.DSL

25import Idris.Elab.Clause

18import Idris.Elab.Clause

26import Idris.Elab.Term

19import Idris.Elab.Term

27import Idris.Elab.Type

20import Idris.Elab.Type

28−import Idris.Elab.Utils

29import Idris.Elab.Value

21import Idris.Elab.Value

30import Idris.Error

22import Idris.Error

31−import Idris.Imports

32−import Idris.Inliner

33import Idris.Options

23import Idris.Options

34−import Idris.Output (iWarn, iputStrLn, pshow)

35−import Idris.PartialEval

36−import Idris.Primitives

37import Idris.Providers

24import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

41

25

42import Prelude hiding (id, (.))

26import Prelude hiding (id, (.))

43

27

44−import Control.Applicative hiding (Const)

45import Control.Category

28import Control.Category

46−import Control.DeepSeq

47import Control.Monad

29import 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

57

30

58-- | Elaborate a type provider

31-- | Elaborate a type provider

59elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()

32elabProvider :: 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

11import Idris.AbsSyntax

12import Idris.Core.Evaluate

13import Idris.Core.TT

14−import Idris.Coverage

15−import Idris.DataOpts

16−import Idris.DeepSeq

17import Idris.Delaborate

14import Idris.Delaborate

18import Idris.Docstrings

15import Idris.Docstrings

19import Idris.Elab.Data

16import Idris.Elab.Data

20−import Idris.Elab.Data

21−import Idris.Elab.Term

22−import Idris.Elab.Type

23−import Idris.Elab.Utils

24import Idris.Error

17import Idris.Error

25−import Idris.Imports

26−import Idris.Inliner

27−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

18+import Idris.Output (sendHighlighting)

28−import Idris.Parser.Expr (tryFullExpr)

29−import Idris.PartialEval

30−import Idris.Primitives

31−import Idris.Providers

32−import IRTS.Lang

33

19

34import Control.Monad

20import Control.Monad

35import Data.List

21import Data.List

@@ -225,15 +211,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

225 isFieldOrParam' :: (Name, a) -> Bool

211 isFieldOrParam' :: (Name, a) -> Bool

226 isFieldOrParam' = isFieldOrParam . fst

212 isFieldOrParam' = isFieldOrParam . fst

227

213

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−

237 -- Delabs the TT to PTerm

214 -- Delabs the TT to PTerm

238 -- This is not good.

215 -- This is not good.

239 -- However, for machine generated implicits, there seems to be no PTerm available.

216 -- 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

252 freeName (NS n s) = NS (freeName n) s

229 freeName (NS n s) = NS (freeName n) s

253 freeName n = n

230 freeName n = n

254

231

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−

262 paramName :: Name -> Name

232 paramName :: Name -> Name

263 paramName (UN n) = sUN ("param_" ++ str n)

233 paramName (UN n) = sUN ("param_" ++ str n)

264 paramName (MN i n) = sMN i ("param_" ++ str n)

234 paramName (MN i n) = sMN i ("param_" ++ str n)

@@ -295,15 +265,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

295 fieldDep :: Name -> PTerm -> (Name, [Name])

265 fieldDep :: Name -> PTerm -> (Name, [Name])

296 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

266 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

297

267

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−

307 -- | A list of fields depended on by other fields.

268 -- | A list of fields depended on by other fields.

308 dependedOn :: [Name]

269 dependedOn :: [Name]

309 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

270 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

src/Idris/Elab/Rewrite.hs−3

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

10module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14import Idris.Core.Elaborate

13import Idris.Core.Elaborate

15import Idris.Core.Evaluate

14import Idris.Core.Evaluate

16import Idris.Core.TT

15import Idris.Core.TT

@@ -20,8 +19,6 @@ import Idris.Error

20

19

21import Control.Monad

20import Control.Monad

22import Control.Monad.State.Strict

21import Control.Monad.State.Strict

23−import Data.List

24−import Debug.Trace

25

22

26elabRewrite :: (PTerm -> ElabD ()) -> IState ->

23elabRewrite :: (PTerm -> ElabD ()) -> IState ->

27 FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

24 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

9

10import Idris.AbsSyntax

11import Idris.Core.Elaborate hiding (Tactic(..))

12−import Idris.Core.Evaluate

13−import Idris.Core.Execute

14import Idris.Core.TT

12import Idris.Core.TT

15import Idris.Core.Typecheck

13import Idris.Core.Typecheck

16import Idris.Elab.Term

14import Idris.Elab.Term

17import Idris.Elab.Value (elabVal)

15import Idris.Elab.Value (elabVal)

18import Idris.Error

16import Idris.Error

19−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

17+import Idris.Output (sendHighlighting)

20

18

21elabScriptTy :: Type

19elabScriptTy :: Type

22elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)

20elabScriptTy = 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.

10module Idris.Elab.Term where

11

12import Idris.AbsSyntax

13−import Idris.AbsSyntaxTree

14−import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)

13+import Idris.Core.CaseTree (SC'(STerm), findCalls)

15import Idris.Core.Elaborate hiding (Tactic(..))

14import Idris.Core.Elaborate hiding (Tactic(..))

16import Idris.Core.Evaluate

15import Idris.Core.Evaluate

17import Idris.Core.ProofTerm (getProofTerm)

16import Idris.Core.ProofTerm (getProofTerm)

18import Idris.Core.TT

17import Idris.Core.TT

19import Idris.Core.Typecheck (check, converts, isType, recheck)

18import Idris.Core.Typecheck (check, converts, isType, recheck)

20import Idris.Core.Unify

19import Idris.Core.Unify

21−import Idris.Core.WHNF (whnf, whnfArgs)

20+import Idris.Core.WHNF (whnf)

22−import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)

21+import Idris.Coverage (genClauses, recoverableCoverage)

23import Idris.Delaborate

22import Idris.Delaborate

24−import Idris.DSL

25import Idris.Elab.Quasiquote (extractUnquotes)

23import Idris.Elab.Quasiquote (extractUnquotes)

26import Idris.Elab.Rewrite

24import Idris.Elab.Rewrite

27import Idris.Elab.Utils

25import Idris.Elab.Utils

28import Idris.Error

26import Idris.Error

29import Idris.ErrReverse (errReverse)

27import Idris.ErrReverse (errReverse)

30import Idris.Options

28import Idris.Options

31−import Idris.Output (pshow)

32import Idris.ProofSearch

29import Idris.ProofSearch

33import Idris.Reflection

30import Idris.Reflection

34import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)

31import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)

35

32

36−import qualified Util.Pretty as U

37−

38import Control.Applicative ((<$>))

33import Control.Applicative ((<$>))

39import Control.Monad

34import Control.Monad

40import Control.Monad.State.Strict

35import Control.Monad.State.Strict

41import Data.Foldable (for_)

36import Data.Foldable (for_)

42import Data.List

37import Data.List

43import qualified Data.Map as M

38import qualified Data.Map as M

44−import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)

39+import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

45import qualified Data.Set as S

40import qualified Data.Set as S

46−import qualified Data.Text as T

47import Debug.Trace

41import Debug.Trace

48

42

49data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS

43data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS

@@ -85,7 +79,6 @@ build :: IState

85 -> ElabD ElabResult

79 -> ElabD ElabResult

86build ist info emode opts fn tm

80build ist info emode opts fn tm

87 = do elab ist info emode opts fn tm

81 = do elab ist info emode opts fn tm

88− let tmIn = tm

89 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

82 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

90 [TIPartial] -> True

83 [TIPartial] -> True

91 _ -> False

84 _ -> False

@@ -163,8 +156,7 @@ buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

163 PTerm ->

156 PTerm ->

164 ElabD ElabResult

157 ElabD ElabResult

165buildTC ist info emode opts fn ns tm

158buildTC 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

168 [TIPartial] -> True

160 [TIPartial] -> True

169 _ -> False

161 _ -> False

170 -- set name supply to begin after highest index in tm

162 -- set name supply to begin after highest index in tm

@@ -190,7 +182,6 @@ buildTC ist info emode opts fn ns tm

190 if (log /= "")

182 if (log /= "")

191 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

183 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

192 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

184 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

193− where pattern = emode == ELHS || emode == EImpossible

194

185

195-- | return whether arguments of the given constructor name can be

186-- | return whether arguments of the given constructor name can be

196-- matched on. If they're polymorphic, no, unless the type has beed

187-- matched on. If they're polymorphic, no, unless the type has beed

@@ -247,7 +238,6 @@ elab ist info emode opts fn tm

247 = do let loglvl = opt_logLevel (idris_options ist)

238 = do let loglvl = opt_logLevel (idris_options ist)

248 when (loglvl > 5) $ unifyLog True

239 when (loglvl > 5) $ unifyLog True

249 compute -- expand type synonyms, etc

240 compute -- expand type synonyms, etc

250− let fc = maybe "(unknown)"

251 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

241 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

252 est <- getAux

242 est <- getAux

253 sequence_ (get_delayed_elab est)

243 sequence_ (get_delayed_elab est)

@@ -283,14 +273,6 @@ elab ist info emode opts fn tm

283 Placeholder -> (True, priority arg)

273 Placeholder -> (True, priority arg)

284 tm -> (False, priority arg)

274 tm -> (False, priority arg)

285

275

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−

294 mkPat = do hs <- get_holes

276 mkPat = do hs <- get_holes

295 tm <- get_term

277 tm <- get_term

296 case hs of

278 case hs of

@@ -356,18 +338,6 @@ elab ist info emode opts fn tm

356 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

338 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

357 notDelay _ = True

339 notDelay _ = True

358

340

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−

371 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

341 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

372 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

342 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

373 -> PTerm -- ^ The term to elaborate

343 -> PTerm -- ^ The term to elaborate

@@ -603,13 +573,6 @@ elab ist info emode opts fn tm

603 (P _ n' _, _) -> n == n'

573 (P _ n' _, _) -> n == n'

604 _ -> False

574 _ -> False

605

575

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−

613 elab' ina _ (PPatvar fc n) | bindfree

576 elab' ina _ (PPatvar fc n) | bindfree

614 = do patvar n

577 = do patvar n

615 update_term liftPats

578 update_term liftPats

@@ -627,8 +590,6 @@ elab ist info emode opts fn tm

627 = do ty <- goal

590 = do ty <- goal

628 testImplicitWarning fc n ty

591 testImplicitWarning fc n ty

629 let ina = e_inarg ec

592 let ina = e_inarg ec

630− guarded = e_guarded ec

631− inty = e_intype ec

632 ctxt <- get_context

593 ctxt <- get_context

633 env <- get_env

594 env <- get_env

634

595

@@ -890,7 +851,6 @@ elab ist info emode opts fn tm

890 _ -> do mapM_ setInjective (map getTm args)

851 _ -> do mapM_ setInjective (map getTm args)

891 -- maybe more things are solvable now

852 -- maybe more things are solvable now

892 unifyProblems

853 unifyProblems

893− let guarded = isConName f ctxt

894-- trace ("args is " ++ show args) $ return ()

854-- trace ("args is " ++ show args) $ return ()

895 ns <- apply (Var f) (map isph args)

855 ns <- apply (Var f) (map isph args)

896-- trace ("ns is " ++ show ns) $ return ()

856-- trace ("ns is " ++ show ns) $ return ()

@@ -1000,10 +960,6 @@ elab ist info emode opts fn tm

1000 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

960 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

1001 | otherwise = getDets (i + 1) ds as

961 | otherwise = getDets (i + 1) ds as

1002

962

1003− tacTm (PTactics _) = True

1004− tacTm (PProof _) = True

1005− tacTm _ = False

1006−

1007 setInjective (PRef _ _ n) = setinj n

963 setInjective (PRef _ _ n) = setinj n

1008 setInjective (PApp _ (PRef _ _ n) _) = setinj n

964 setInjective (PApp _ (PRef _ _ n) _) = setinj n

1009 setInjective _ = return ()

965 setInjective _ = return ()

@@ -1078,7 +1034,6 @@ elab ist info emode opts fn tm

1078 matchProblems True

1034 matchProblems True

1079 args <- get_env

1035 args <- get_env

1080 envU <- mapM (getKind args) args

1036 envU <- mapM (getKind args) args

1081− let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

1082

1037

1083 -- Drop the unique arguments used in the term already

1038 -- Drop the unique arguments used in the term already

1084 -- and in the scrutinee (since it's

1039 -- and in the scrutinee (since it's

@@ -1156,12 +1111,6 @@ elab ist info emode opts fn tm

1156 UType AllTypes -> return (n, True)

1111 UType AllTypes -> return (n, True)

1157 _ -> return (n, False)

1112 _ -> return (n, False)

1158

1113

1159− tcName tm | (P _ n _, _) <- unApply tm

1160− = case lookupCtxt n (idris_interfaces ist) of

1161− [_] -> True

1162− _ -> False

1163− tcName _ = False

1164−

1165 isNotLift env n

1114 isNotLift env n

1166 = case lookupBinder n env of

1115 = case lookupBinder n env of

1167 Just ty ->

1116 Just ty ->

@@ -1170,10 +1119,6 @@ elab ist info emode opts fn tm

1170 _ -> False

1119 _ -> False

1171 _ -> False

1120 _ -> False

1172

1121

1173− usedIn ns (n, b)

1174− = n `elem` ns

1175− || any (\x -> x `elem` ns) (allTTNames (binderTy b))

1176−

1177 elab' ina fc (PUnifyLog t) = do unifyLog True

1122 elab' ina fc (PUnifyLog t) = do unifyLog True

1178 elab' ina fc t

1123 elab' ina fc t

1179 unifyLog False

1124 unifyLog False

@@ -2716,7 +2661,6 @@ processTacticDecls info steps =

2716

2661

2717 RDatatypeDefnInstrs tyn tyconTy ctors ->

2662 RDatatypeDefnInstrs tyn tyconTy ctors ->

2718 do let cn (n, _, _) = n

2663 do let cn (n, _, _) = n

2719− cimpls (_, impls, _) = impls

2720 cty (_, _, t) = t

2664 cty (_, _, t) = t

2721 addIBC (IBCDef tyn)

2665 addIBC (IBCDef tyn)

2722 mapM_ (addIBC . IBCDef . cn) ctors

2666 mapM_ (addIBC . IBCDef . cn) ctors

src/Idris/Elab/Transform.hs+1−30

@@ -9,47 +9,19 @@ Maintainer : The Idris Community.

9module Idris.Elab.Transform where

10

11import Idris.AbsSyntax

12−import Idris.ASTUtils

13−import Idris.Core.CaseTree

14import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.Elaborate hiding (Tactic(..))

15−import Idris.Core.Evaluate

16−import Idris.Core.Execute

17import Idris.Core.TT

13import Idris.Core.TT

18import Idris.Core.Typecheck

14import 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

25import Idris.Elab.Term

15import Idris.Elab.Term

26import Idris.Elab.Utils

16import Idris.Elab.Utils

27import Idris.Error

17import Idris.Error

28−import Idris.Imports

29−import Idris.Inliner

30−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

18+import Idris.Output (sendHighlighting)

31−import Idris.PartialEval

32−import Idris.Primitives

33−import Idris.Providers

34−import IRTS.Lang

35−

36−import Util.Pretty (pretty, text)

37

19

38import Prelude hiding (id, (.))

20import Prelude hiding (id, (.))

39

21

40−import Control.Applicative hiding (Const)

41import Control.Category

22import Control.Category

42−import Control.DeepSeq

43import Control.Monad

23import Control.Monad

44import Control.Monad.State.Strict as State

24import 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

53

25

54elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

26elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

55elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

27elabTransform 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

66 sendHighlighting highlights

38 sendHighlighting highlights

67 updateIState $ \i -> i { idris_name = newGName }

39 updateIState $ \i -> i { idris_name = newGName }

68 let lhs_tm = orderPats (getInferTerm lhs')

40 let lhs_tm = orderPats (getInferTerm lhs')

69− let lhs_ty = getInferType lhs'

70 let newargs = pvars i lhs_tm

41 let newargs = pvars i lhs_tm

71

42

72 (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

43 (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 (

13

14import Idris.AbsSyntax

15import Idris.ASTUtils

16−import Idris.Core.CaseTree

17import Idris.Core.Elaborate hiding (Tactic(..))

16import Idris.Core.Elaborate hiding (Tactic(..))

18import Idris.Core.Evaluate

17import Idris.Core.Evaluate

19−import Idris.Core.Execute

20import Idris.Core.TT

18import Idris.Core.TT

21−import Idris.Core.Typecheck

22import Idris.Core.WHNF

19import Idris.Core.WHNF

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

27import Idris.Docstrings (Docstring)

20import Idris.Docstrings (Docstring)

28−import Idris.DSL

29import Idris.Elab.Term

21import Idris.Elab.Term

30import Idris.Elab.Utils

22import Idris.Elab.Utils

31import Idris.Elab.Value

23import Idris.Elab.Value

32import Idris.Error

24import Idris.Error

33−import Idris.Imports

34−import Idris.Inliner

35import Idris.Options

25import Idris.Options

36−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

26+import Idris.Output (sendHighlighting)

37−import Idris.PartialEval

38−import Idris.Primitives

39−import Idris.Providers

40−import IRTS.Lang

41−

42−import Util.Pretty (pretty, text)

43

27

44import Prelude hiding (id, (.))

28import Prelude hiding (id, (.))

45

29

46−import Control.Applicative hiding (Const)

47import Control.Category

30import Control.Category

48−import Control.DeepSeq

49import Control.Monad

31import 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

56import qualified Data.Set as S

32import qualified Data.Set as S

57−import qualified Data.Text as T

58−import qualified Data.Traversable as Traversable

59−import Debug.Trace

60

33

61buildType :: ElabInfo

34buildType :: ElabInfo

62 -> SyntaxInfo

35 -> SyntaxInfo

@@ -196,11 +169,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

196 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

169 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

197

170

198 let (fam, _) = unApply (getRetTy nty')

171 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

204 -- Productivity checking now via checking for guarded 'Delay'

172 -- Productivity checking now via checking for guarded 'Delay'

205 let opts' = opts -- if corec then (Coinductive : opts) else opts

173 let opts' = opts -- if corec then (Coinductive : opts) else opts

206 let usety = if norm then nty' else nty

174 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

251 _ -> return ()

219 _ -> return ()

252 return usety

220 return usety

253 where

221 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−

262 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

222 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

263

223

264 err = txt "Err"

224 err = txt "Err"

src/Idris/Elab/Utils.hs+1−6

@@ -14,7 +14,6 @@ import Idris.Core.Evaluate

14import Idris.Core.TT

15import Idris.Core.Typecheck

16import Idris.Core.WHNF

17−import Idris.DeepSeq

18import Idris.Delaborate

17import Idris.Delaborate

19import Idris.Docstrings

18import Idris.Docstrings

20import Idris.Error

19import Idris.Error

@@ -22,14 +21,11 @@ import Idris.Output

22

21

23import Util.Pretty

22import Util.Pretty

24

23

25−import Control.Applicative hiding (Const)

26import Control.Monad

24import Control.Monad

27import Control.Monad.State

25import Control.Monad.State

28import Data.List

26import Data.List

29import qualified Data.Map as Map

27import qualified Data.Map as Map

30import Data.Maybe

28import Data.Maybe

31−import qualified Data.Traversable as Traversable

32−import Debug.Trace

33

29

34recheckC = recheckC_borrowing False True []

30recheckC = recheckC_borrowing False True []

35

31

@@ -122,7 +118,6 @@ elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

122elabCaseBlock info opts d@(PClauses f o n ps)

118elabCaseBlock info opts d@(PClauses f o n ps)

123 = do addIBC (IBCDef n)

119 = do addIBC (IBCDef n)

124 logElab 5 $ "CASE BLOCK: " ++ show (n, d)

120 logElab 5 $ "CASE BLOCK: " ++ show (n, d)

125− let opts' = nub (o ++ opts)

126 -- propagate totality assertion to the new definitions

121 -- propagate totality assertion to the new definitions

127 let opts' = filter propagatable opts

122 let opts' = filter propagatable opts

128 setFlags n opts'

123 setFlags n opts'

@@ -750,7 +745,7 @@ pruneByType _ _ t _ _ as = as

750-- to it later - just returns 'var' for now. EB)

745-- to it later - just returns 'var' for now. EB)

751isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

746isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

752isPlausible ist var env n ty

747isPlausible ist var env n ty

753− = let (hvar, interfaces) = collectConstraints [] [] ty in

748+ = let (hvar, _) = collectConstraints [] [] ty in

754 case hvar of

749 case hvar of

755 Nothing -> True

750 Nothing -> True

756 Just rth -> var -- trace (show (rth, interfaces)) var

751 Just rth -> var -- trace (show (rth, interfaces)) var

src/Idris/Elab/Value.hs+2−30

@@ -13,48 +13,20 @@ module Idris.Elab.Value(

13 ) where

14

15import Idris.AbsSyntax

16−import Idris.ASTUtils

17−import Idris.Core.CaseTree

18import Idris.Core.Elaborate hiding (Tactic(..))

16import Idris.Core.Elaborate hiding (Tactic(..))

19import Idris.Core.Evaluate hiding (Unchecked)

17import Idris.Core.Evaluate hiding (Unchecked)

20−import Idris.Core.Execute

21import Idris.Core.TT

18import Idris.Core.TT

22−import Idris.Core.Typecheck

23−import Idris.Coverage

24−import Idris.DataOpts

25−import Idris.DeepSeq

26−import Idris.Delaborate

27import Idris.Docstrings

19import Idris.Docstrings

28−import Idris.DSL

29import Idris.Elab.Term

20import Idris.Elab.Term

30import Idris.Elab.Utils

21import Idris.Elab.Utils

31import Idris.Error

22import Idris.Error

32−import Idris.Imports

33−import Idris.Inliner

34−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

23+import Idris.Output (sendHighlighting)

35−import Idris.PartialEval

36−import Idris.Primitives

37−import Idris.Providers

38−import IRTS.Lang

39−

40−import Util.Pretty (pretty, text)

41

24

42import Prelude hiding (id, (.))

25import Prelude hiding (id, (.))

43

26

44−import Control.Applicative hiding (Const)

45import Control.Category

27import Control.Category

46−import Control.DeepSeq

47−import Control.Monad

48−import Control.Monad.State.Strict as State

49−import Data.Char (isLetter, toLower)

28+import Data.Char (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

56import qualified Data.Traversable as Traversable

29import qualified Data.Traversable as Traversable

57−import Debug.Trace

58

30

59-- | Elaborate a value, returning any new bindings created (this will only

31-- | Elaborate a value, returning any new bindings created (this will only

60-- happen if elaborating as a pattern clause)

32-- happen if elaborating as a pattern clause)

src/Idris/ElabDecls.hs+3−32

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

12module Idris.ElabDecls where

13

14import Idris.AbsSyntax

15−import Idris.ASTUtils

16−import Idris.Core.CaseTree

17−import Idris.Core.Elaborate hiding (Tactic(..))

18import Idris.Core.Evaluate

15import Idris.Core.Evaluate

19−import Idris.Core.Execute

20import Idris.Core.TT

16import Idris.Core.TT

21−import Idris.Core.Typecheck

22−import Idris.Coverage

23−import Idris.DataOpts

24−import Idris.DeepSeq

25−import Idris.Delaborate

26import Idris.Directives

17import Idris.Directives

27import Idris.Docstrings hiding (Unchecked)

18import Idris.Docstrings hiding (Unchecked)

28−import Idris.DSL

29import Idris.Elab.Clause

19import Idris.Elab.Clause

30import Idris.Elab.Data

20import Idris.Elab.Data

31import Idris.Elab.Implementation

21import Idris.Elab.Implementation

@@ -36,36 +26,21 @@ import Idris.Elab.RunElab

36import Idris.Elab.Term

26import Idris.Elab.Term

37import Idris.Elab.Transform

27import Idris.Elab.Transform

38import Idris.Elab.Type

28import Idris.Elab.Type

39−import Idris.Elab.Utils

40import Idris.Elab.Value

29import Idris.Elab.Value

41import Idris.Error

30import Idris.Error

42−import Idris.Imports

43−import Idris.Inliner

44import Idris.Options

31import Idris.Options

45−import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

32+import Idris.Output (sendHighlighting)

46−import Idris.PartialEval

47import Idris.Primitives

33import Idris.Primitives

48−import Idris.Providers

49import Idris.Termination

34import Idris.Termination

50import IRTS.Lang

35import IRTS.Lang

51

36

52−import Util.Pretty (pretty, text)

53−

54import Prelude hiding (id, (.))

37import Prelude hiding (id, (.))

55

38

56−import Control.Applicative hiding (Const)

57import Control.Category

39import Control.Category

58−import Control.DeepSeq

59import Control.Monad

40import Control.Monad

60import Control.Monad.State.Strict as State

41import 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

65import Data.Maybe

42import Data.Maybe

66−import qualified Data.Set as S

67import qualified Data.Text as T

43import qualified Data.Text as T

68−import Debug.Trace

69

44

70-- | Top level elaborator info, supporting recursive elaboration

45-- | Top level elaborator info, supporting recursive elaboration

71recinfo :: FC -> ElabInfo

46recinfo :: FC -> ElabInfo

@@ -269,12 +244,6 @@ elabDecl' what info (PParams f ns ps)

269 let nblock = pblock i

244 let nblock = pblock i

270 mapM_ (elabDecl' what info) nblock

245 mapM_ (elabDecl' what info) nblock

271 where

246 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 }

278 pblock i = map (expandParamsD False i id ns

247 pblock i = map (expandParamsD False i id ns

279 (concatMap tldeclared ps)) ps

248 (concatMap tldeclared ps)) ps

280

249

@@ -311,6 +280,8 @@ elabDecl' _ info (PDSL n dsl)

311 ifail "You must turn on the DSLNotation extension to use a dsl block"

280 ifail "You must turn on the DSLNotation extension to use a dsl block"

312 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

281 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

313 addIBC (IBCDSL n)

282 addIBC (IBCDSL n)

283+elabDecl' what info (PDirective i@(DLogging _))

284+ = directiveAction i

314elabDecl' what info (PDirective i)

285elabDecl' what info (PDirective i)

315 | what /= EDefns = directiveAction i

286 | what /= EDefns = directiveAction i

316elabDecl' what info (PProvider doc syn fc nfc provWhat n)

287elabDecl' what info (PProvider doc syn fc nfc provWhat n)

src/Idris/Erasure.hs−7

@@ -20,7 +20,6 @@ import Idris.Primitives

20

21import Prelude hiding (id, (.))

22

23−import Control.Applicative

24import Control.Arrow

23import Control.Arrow

25import Control.Category

24import Control.Category

26import Control.Monad.State

25import Control.Monad.State

@@ -36,8 +35,6 @@ import Data.Set (Set)

36import qualified Data.Set as S

35import qualified Data.Set as S

37import Data.Text (pack)

36import Data.Text (pack)

38import qualified Data.Text as T

37import qualified Data.Text as T

39−import Debug.Trace

40−import System.IO.Unsafe

41

38

42-- | UseMap maps names to the set of used (reachable) argument

39-- | UseMap maps names to the set of used (reachable) argument

43-- positions.

40-- positions.

@@ -290,7 +287,6 @@ buildDepMap ci used externs ctx startNames

290 -- mini-DSL for postulates

287 -- mini-DSL for postulates

291 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

288 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

292 it n is = [(sUN n, Arg i) | i <- is]

289 it n is = [(sUN n, Arg i) | i <- is]

293− mn n is = [(MN 0 $ pack n, Arg i) | i <- is]

294

290

295 -- believe_me is special because it does not use all its arguments

291 -- believe_me is special because it does not use all its arguments

296 specialPrims = S.fromList [sUN "prim__believe_me"]

292 specialPrims = S.fromList [sUN "prim__believe_me"]

@@ -627,9 +623,6 @@ buildDepMap ci used externs ctx startNames

627 union :: Deps -> Deps -> Deps

623 union :: Deps -> Deps -> Deps

628 union = M.unionWith (M.unionWith S.union)

624 union = M.unionWith (M.unionWith S.union)

629

625

630− unions :: [Deps] -> Deps

631− unions = M.unionsWith (M.unionWith S.union)

632−

633 unionMap :: (a -> Deps) -> [a] -> Deps

626 unionMap :: (a -> Deps) -> [a] -> Deps

634 unionMap f = M.unionsWith (M.unionWith S.union) . map f

627 unionMap f = M.unionsWith (M.unionWith S.union) . map f

635

628

src/Idris/ErrReverse.hs−12

@@ -12,10 +12,8 @@ module Idris.ErrReverse(errReverse) where

12import Idris.AbsSyntax

13import Idris.Core.Evaluate (unfold)

14import Idris.Core.TT

15−import Util.Pretty

16

15

17import Data.List

16import Data.List

18−import Debug.Trace

19

17

20-- | For display purposes, apply any 'error reversal' transformations

18-- | For display purposes, apply any 'error reversal' transformations

21-- so that errors will be more readable,

19-- so that errors will be more readable,

@@ -73,13 +71,3 @@ errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)

73 Just (fs ++ as)

71 Just (fs ++ as)

74 -- no matching Binds, for now...

72 -- no matching Binds, for now...

75 match' ns x y = if x == y then Just [] else Nothing

73 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

14import Idris.Core.Constraints

15import Idris.Core.Evaluate (ctxtAlist)

16import Idris.Core.TT

17−import Idris.Core.Typecheck

18import Idris.Delaborate

17import Idris.Delaborate

19import Idris.Output

18import Idris.Output

20

19

21import Prelude hiding (catch)

20import Prelude hiding (catch)

22

21

23import Control.Monad (when)

22import Control.Monad (when)

24−import Control.Monad.State.Strict

25−import Data.Char

26import qualified Data.Foldable as Foldable

23import qualified Data.Foldable as Foldable

27import Data.List (intercalate, isPrefixOf)

24import Data.List (intercalate, isPrefixOf)

28import qualified Data.Set as S

25import qualified Data.Set as S

29import qualified Data.Text as T

26import 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

34import System.IO.Error (ioeGetErrorString, isUserError)

27import System.IO.Error (ioeGetErrorString, isUserError)

35

28

36iucheck :: Idris ()

29iucheck :: Idris ()

src/Idris/IBC.hs+26−31

@@ -5,20 +5,20 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

8{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}

9{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}

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

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

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

10

12

11module Idris.IBC (loadIBC, loadPkgIndex,

13module Idris.IBC (loadIBC, loadPkgIndex,

12 writeIBC, writePkgIndex,

14 writeIBC, writePkgIndex,

13 hasValidIBCVersion, IBCPhase(..)) where

15 hasValidIBCVersion, IBCPhase(..)) where

14

16

15import Idris.AbsSyntax

17import Idris.AbsSyntax

16−import Idris.Core.Binary

17import Idris.Core.CaseTree

18import Idris.Core.CaseTree

18import Idris.Core.Evaluate

19import Idris.Core.Evaluate

19import Idris.Core.TT

20import Idris.Core.TT

20−import Idris.DeepSeq

21+import Idris.DeepSeq ()

21−import Idris.Delaborate

22import Idris.Docstrings (Docstring)

23import qualified Idris.Docstrings as D

24import Idris.Error

@@ -27,23 +27,15 @@ import Idris.Options

27import Idris.Output

28import IRTS.System (getIdrisLibDir)

29

30−import Paths_idris

31−

32import qualified Cheapskate.Types as CT

30import qualified Cheapskate.Types as CT

33import Codec.Archive.Zip

31import Codec.Archive.Zip

34import Control.DeepSeq

32import Control.DeepSeq

35import Control.Monad

33import Control.Monad

36−import Control.Monad.State.Strict hiding (get, put)

37−import qualified Control.Monad.State.Strict as ST

38import Data.Binary

34import Data.Binary

39import Data.ByteString.Lazy as B hiding (elem, length, map)

35import Data.ByteString.Lazy as B hiding (elem, length, map)

40−import Data.Functor

41import Data.List as L

36import Data.List as L

42import Data.Maybe (catMaybes)

37import Data.Maybe (catMaybes)

43import qualified Data.Set as S

38import qualified Data.Set as S

44−import qualified Data.Text as T

45−import Data.Vector.Binary

46−import Debug.Trace

47import System.Directory

39import System.Directory

48import System.FilePath

40import System.FilePath

49

41

@@ -59,7 +51,6 @@ data IBCPhase = IBC_Building -- ^ when building the module tree

59data IBCFile = IBCFile {

51data IBCFile = IBCFile {

60 ver :: Word16

52 ver :: Word16

61 , sourcefile :: FilePath

53 , sourcefile :: FilePath

62− , ibc_reachablenames :: ![Name]

63 , ibc_imports :: ![(Bool, FilePath)]

54 , ibc_imports :: ![(Bool, FilePath)]

64 , ibc_importdirs :: ![FilePath]

55 , ibc_importdirs :: ![FilePath]

65 , ibc_sourcedirs :: ![FilePath]

56 , ibc_sourcedirs :: ![FilePath]

@@ -116,7 +107,7 @@ deriving instance Binary IBCFile

116!-}

107!-}

117

108

118initIBC :: IBCFile

109initIBC :: IBCFile

119−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

110+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

120

111

121hasValidIBCVersion :: FilePath -> Idris Bool

112hasValidIBCVersion :: FilePath -> Idris Bool

122hasValidIBCVersion fp = do

113hasValidIBCVersion fp = do

@@ -131,7 +122,9 @@ loadIBC :: Bool -- ^ True = reexport, False = make everything private

131 -> IBCPhase

122 -> IBCPhase

132 -> FilePath -> Idris ()

123 -> FilePath -> Idris ()

133loadIBC reexport phase fp

124loadIBC reexport phase fp

125+ = do logIBC 1 $ "loadIBC (reexport, phase, fp)" ++ show (reexport, phase, fp)

134− = do imps <- getImported

126+ imps <- getImported

127+ logIBC 3 $ "loadIBC imps" ++ show imps

135 case lookup fp imps of

128 case lookup fp imps of

136 Nothing -> load True

129 Nothing -> load True

137 Just p -> if (not p && reexport) then load False else return ()

130 Just p -> if (not p && reexport) then load False else return ()

@@ -517,13 +510,16 @@ processImports reexp phase fname ar = do

517 ibcsd <- valIBCSubDir i

510 ibcsd <- valIBCSubDir i

518 ids <- rankedImportDirs fname

511 ids <- rankedImportDirs fname

519 putIState (i { imported = f : imported i })

512 putIState (i { imported = f : imported i })

513+ let (phase', reexp') =

520− let phase' = case phase of

514+ case phase of

521− IBC_REPL _ -> IBC_REPL False

515+ IBC_REPL True -> (IBC_REPL False, reexp)

522− p -> p

516+ IBC_REPL False -> (IBC_Building, reexp && re)

517+ p -> (p, reexp && re)

523 fp <- findIBC ids ibcsd f

518 fp <- findIBC ids ibcsd f

519+ logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')

524 case fp of

520 case fp of

525 Nothing -> do logIBC 2 $ "Failed to load ibc " ++ f

521 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

527

523

528processImplicits :: Archive -> Idris ()

524processImplicits :: Archive -> Idris ()

529processImplicits ar = do

525processImplicits ar = do

@@ -639,6 +635,7 @@ processPatternDefs ar = do

639processDefs :: Archive -> Idris ()

635processDefs :: Archive -> Idris ()

640processDefs ar = do

636processDefs ar = do

641 ds <- getEntry [] "ibc_defs" ar

637 ds <- getEntry [] "ibc_defs" ar

638+ logIBC 4 $ "processDefs ds" ++ show ds

642 mapM_ (\ (n, d) -> do

639 mapM_ (\ (n, d) -> do

643 d' <- updateDef d

640 d' <- updateDef d

644 case d' of

641 case d' of

@@ -735,8 +732,11 @@ processAccess :: Bool -- ^ Reexporting?

735 -> IBCPhase

732 -> IBCPhase

736 -> Archive -> Idris ()

733 -> Archive -> Idris ()

737processAccess reexp phase ar = do

734processAccess reexp phase ar = do

735+ logIBC 3 $ "processAccess (reexp, phase)" ++ show (reexp, phase)

738 ds <- getEntry [] "ibc_access" ar

736 ds <- getEntry [] "ibc_access" ar

737+ logIBC 3 $ "processAccess ds" ++ show ds

739 mapM_ (\ (n, a_in) -> do

738 mapM_ (\ (n, a_in) -> do

739+

740 let a = if reexp then a_in else Hidden

741 logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

742 updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })

@@ -745,10 +745,15 @@ processAccess reexp phase ar = do

745 then do

746 logIBC 2 $ "Not exporting " ++ show n

747 setAccessibility n Hidden

748+ else

748− else logIBC 2 $ "Exporting " ++ show n

749+ logIBC 2 $ "Exporting " ++ show n

750+

749 -- Everything should be available at the REPL from

751 -- Everything should be available at the REPL from

750− -- things imported publicly

752+ -- things imported publicly.

753+ when (phase == IBC_REPL True) $ do

754+ logIBC 2 $ "Top level, exporting " ++ show n

751− when (phase == IBC_REPL True) $ setAccessibility n Public) ds

755+ setAccessibility n Public

756+ ) ds

752

757

753processFlags :: Archive -> Idris ()

758processFlags :: Archive -> Idris ()

754processFlags ar = do

759processFlags ar = do

@@ -1117,16 +1122,6 @@ instance Binary Accessibility where

1117 3 -> return Hidden

1122 3 -> return Hidden

1118 _ -> error "Corrupted binary data for Accessibility"

1123 _ -> error "Corrupted binary data for Accessibility"

1119

1124

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−

1130instance Binary PReason where

1125instance Binary PReason where

1131 put x

1126 put x

1132 = case x of

1127 = case x of

src/Idris/IdeMode.hs+1−4

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

11

12module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where

13

14−import Idris.Core.Binary

14+import Idris.Core.Binary ()

15import Idris.Core.TT

16

17import Control.Applicative hiding (Const)

@@ -176,9 +176,6 @@ instance SExpable OutputAnnotation where

176encodeName :: Name -> String

177encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

178

179−decodeName :: String -> Name

180−decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

181−

182encodeTerm :: [(Name, Bool)] -> Term -> String

179encodeTerm :: [(Name, Bool)] -> Term -> String

183encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

180encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

184 (bnd, tm)

181 (bnd, tm)

src/Idris/IdrisDoc.hs+4−16

@@ -10,11 +10,10 @@ Maintainer : The Idris Community.

10module Idris.IdrisDoc (generateDocs) where

11

12import Idris.AbsSyntax

13−import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName,

13+import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName,

14− isFnName, isTConName, lookupDefAcc)

14+ isTConName, lookupDefAcc)

15−import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),

15+import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..),

16− TextFormatting(..), constIsType, nsroot, sUN, str,

16+ constIsType, nsroot, sUN, str, toAlist, txt)

17− toAlist, txt)

18import Idris.Docs

17import Idris.Docs

19import Idris.Docstrings (nullDocstring)

18import Idris.Docstrings (nullDocstring)

20import qualified Idris.Docstrings as Docstrings

19import qualified Idris.Docstrings as Docstrings

@@ -26,17 +25,13 @@ import Control.Applicative ((<|>))

26import Control.Monad (forM_)

25import Control.Monad (forM_)

27import Control.Monad.Trans.Except

26import Control.Monad.Trans.Except

28import Control.Monad.Trans.State.Strict

27import Control.Monad.Trans.State.Strict

29−import qualified Data.ByteString as BS

30import qualified Data.ByteString.Lazy as BS2

28import qualified Data.ByteString.Lazy as BS2

31import qualified Data.List as L

29import qualified Data.List as L

32−import qualified Data.List.Split as LS

33import qualified Data.Map as M hiding ((!))

30import qualified Data.Map as M hiding ((!))

34import Data.Maybe

31import Data.Maybe

35import Data.Monoid (mempty)

32import Data.Monoid (mempty)

36−import qualified Data.Ord (compare)

37import qualified Data.Set as S

33import qualified Data.Set as S

38import qualified Data.Text as T

34import qualified Data.Text as T

39−import qualified Data.Text.Encoding as E

40import System.Directory

35import System.Directory

41import System.FilePath

36import System.FilePath

42import System.IO

37import System.IO

@@ -253,13 +248,6 @@ getAccess ist n =

253 [(_, acc)] -> acc

248 [(_, acc)] -> acc

254 _ -> Private

249 _ -> Private

255

250

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−

263-- | Predicate saying whether a Name possibly may have docs defined

251-- | Predicate saying whether a Name possibly may have docs defined

264-- Without this, getDocs from Idris.Docs may fail a pattern match.

252-- Without this, getDocs from Idris.Docs may fail a pattern match.

265mayHaveDocs :: Name -- ^ The Name to test

253mayHaveDocs :: Name -- ^ The Name to test

src/Idris/Imports.hs+2−3

@@ -13,7 +13,6 @@ module Idris.Imports(

13import Idris.AbsSyntax

14import Idris.Core.TT

15import Idris.Error

16−import Idris.Output

17import IRTS.System (getIdrisLibDir)

16import IRTS.System (getIdrisLibDir)

18

17

19import Control.Applicative ((<$>))

18import Control.Applicative ((<$>))

@@ -30,13 +29,13 @@ pkgIndex :: String -> FilePath

30pkgIndex s = "00" ++ s ++ "-idx.ibc"

29pkgIndex s = "00" ++ s ++ "-idx.ibc"

31

30

32srcPath :: FilePath -> FilePath

31srcPath :: FilePath -> FilePath

33−srcPath fp = let (n, ext) = splitExtension fp in

32+srcPath fp = let (_, ext) = splitExtension fp in

34 case ext of

33 case ext of

35 ".idr" -> fp

34 ".idr" -> fp

36 _ -> fp ++ ".idr"

35 _ -> fp ++ ".idr"

37

36

38lsrcPath :: FilePath -> FilePath

37lsrcPath :: FilePath -> FilePath

39−lsrcPath fp = let (n, ext) = splitExtension fp in

38+lsrcPath fp = let (_, ext) = splitExtension fp in

40 case ext of

39 case ext of

41 ".lidr" -> fp

40 ".lidr" -> fp

42 _ -> fp ++ ".lidr"

41 _ -> fp ++ ".lidr"

src/Idris/Info.hs−1

@@ -29,7 +29,6 @@ import Idris.Imports (installedPackages)

29import Idris.Options (loggingCatsStr)

30import qualified IRTS.System as S

31

32−import Paths_idris

33import Version_idris (gitHash)

32import Version_idris (gitHash)

34

33

35import Data.Version

34import Data.Version

src/Idris/Interactive.hs+1−3

@@ -382,9 +382,7 @@ makeLemma fn updatefile l n

382 StringAtom lem_app]]]

383 in runIO . hPutStrLn h $ convSExp "return" good n

384

385− where getIndent s = length (takeWhile isSpace s)

386−

387− appArgs skip 0 _ = ""

385+ where appArgs skip 0 _ = ""

388 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)

386 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)

389 | (thead c /= '_' && n `notElem` skip)

387 | (thead c /= '_' && n `notElem` skip)

390 = " " ++ show n ++ appArgs skip (i - 1) sc

388 = " " ++ show n ++ appArgs skip (i - 1) sc

src/Idris/ModeCommon.hs+22−23

@@ -4,6 +4,11 @@ Description : Common utilities used by all modes.

4License : BSD3

5Maintainer : The Idris Community.

6-}

7+

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

9+{-# OPTIONS_GHC -fwarn-unused-binds #-}

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

11+

7module Idris.ModeCommon where

12module Idris.ModeCommon where

8

13

9import Idris.AbsSyntax

14import Idris.AbsSyntax

@@ -25,16 +30,11 @@ import Prelude hiding (id, (.), (<$>))

25import Control.Category

30import Control.Category

26import Control.DeepSeq

31import Control.DeepSeq

27import Control.Monad

32import Control.Monad

28−import Control.Monad.Trans.State.Strict (get)

29−import Data.List hiding (group)

30−import Data.Maybe

31import Network.Socket (PortNumber)

33import Network.Socket (PortNumber)

32−import System.Directory

33

34

34defaultPort :: PortNumber

35defaultPort :: PortNumber

35defaultPort = fromIntegral 4294

36defaultPort = fromIntegral 4294

36

37

37−

38loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

39loadInputs inputs toline -- furthest line to read in input source files

40 = idrisCatch

@@ -49,6 +49,8 @@ loadInputs inputs toline -- furthest line to read in input source files

49 [] -> not (NoREPL `elem` opts)

50 _ -> True

51

52+ logParser 3 $ show "loadInputs loadCode" ++ show loadCode

53+

52 -- For each ifile list, check it and build ibcs in the same clean IState

54 -- For each ifile list, check it and build ibcs in the same clean IState

53 -- so that they don't interfere with each other when checking

55 -- so that they don't interfere with each other when checking

54

56

@@ -59,6 +61,7 @@ loadInputs inputs toline -- furthest line to read in input source files

59 let ninputs = zip [1..] inputs

61 let ninputs = zip [1..] inputs

60 ifiles <- mapWhileOK (\(num, input) ->

62 ifiles <- mapWhileOK (\(num, input) ->

61 do putIState ist

63 do putIState ist

64+ logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)

62 modTree <- buildTree

65 modTree <- buildTree

63 (map snd (take (num-1) ninputs))

66 (map snd (take (num-1) ninputs))

64 importlists

67 importlists

@@ -77,9 +80,18 @@ loadInputs inputs toline -- furthest line to read in input source files

77 case errSpan inew of

80 case errSpan inew of

78 Nothing ->

81 Nothing ->

79 do putIState $!! ist { idris_tyinfodata = tidata }

82 do putIState $!! ist { idris_tyinfodata = tidata }

80− ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))

83+ logParser 3 $ "loadInputs ifiles" ++ show ifiles

81−-- logLvl 0 $ "Loading from " ++ show ibcfiles

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+

82− tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)

94+ tryLoad True (IBC_REPL True) ibcfiles

83 _ -> return ()

95 _ -> return ()

84 exports <- findExports

96 exports <- findExports

85

97

@@ -103,6 +115,8 @@ loadInputs inputs toline -- furthest line to read in input source files

103 tryLoad keepstate phase [] = warnTotality >> return ()

115 tryLoad keepstate phase [] = warnTotality >> return ()

104 tryLoad keepstate phase (f : fs)

116 tryLoad keepstate phase (f : fs)

105 = do ist <- getIState

117 = do ist <- getIState

118+ logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++

119+ show (keepstate, phase, f : fs)

106 let maxline

120 let maxline

107 = case toline of

121 = case toline of

108 Nothing -> Nothing

122 Nothing -> Nothing

@@ -142,21 +156,6 @@ loadInputs inputs toline -- furthest line to read in input source files

142 fmatch xs ('.':'/':ys) = fmatch xs ys

156 fmatch xs ('.':'/':ys) = fmatch xs ys

143 fmatch xs ys = xs == ys

157 fmatch xs ys = xs == ys

144

158

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−

160 -- Like mapM, but give up when there's an error

159 -- Like mapM, but give up when there's an error

161 mapWhileOK f [] = return []

160 mapWhileOK f [] = return []

162 mapWhileOK f (x : xs) = do x' <- f x

161 mapWhileOK f (x : xs) = do x' <- f x

src/Idris/Output.hs+2−3

@@ -13,7 +13,7 @@ module Idris.Output where

13

14import Idris.AbsSyntax

15import Idris.Colours (hEndColourise, hStartColourise)

16−import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)

16+import Idris.Core.Evaluate (normaliseAll)

17import Idris.Core.TT

18import Idris.Delaborate

19import Idris.Docstrings

@@ -27,13 +27,12 @@ import Util.System (isATTY)

27import Prelude hiding ((<$>))

28

29import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

30−import Data.Char (isAlpha)

31import Data.List (intersperse, nub)

30import Data.List (intersperse, nub)

32import Data.Maybe (fromMaybe)

31import Data.Maybe (fromMaybe)

33import System.Console.Haskeline.MonadException (MonadException(controlIO),

32import System.Console.Haskeline.MonadException (MonadException(controlIO),

34 RunIO(RunIO))

33 RunIO(RunIO))

35import System.FilePath (replaceExtension)

34import System.FilePath (replaceExtension)

36−import System.IO (Handle, hPutStr, hPutStrLn, stdout)

35+import System.IO (Handle, hPutStr, hPutStrLn)

37

36

38instance MonadException m => MonadException (ExceptT Err m) where

37instance MonadException m => MonadException (ExceptT Err m) where

39 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

38 controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

src/Idris/Package.hs+1−6

@@ -12,7 +12,7 @@ import System.Directory

12import System.Directory (copyFile, createDirectoryIfMissing)

13import System.Exit

14import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,

15− hasExtension, normalise, takeDirectory, takeExtension,

15+ hasExtension, takeDirectory, takeExtension,

16 takeFileName, (</>))

17import System.IO

18import System.Process

@@ -23,10 +23,8 @@ import Control.Monad

23import Control.Monad.Trans.Except (runExceptT)

24import Control.Monad.Trans.State.Strict (execStateT)

25import Data.Either (partitionEithers)

26−import Data.Either (partitionEithers)

27import Data.List

26import Data.List

28import Data.List.Split (splitOn)

27import Data.List.Split (splitOn)

29−import Data.Maybe (fromMaybe)

30

28

31import Idris.AbsSyntax

29import Idris.AbsSyntax

32import Idris.Core.TT

30import Idris.Core.TT

@@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain)

38import Idris.Options

36import Idris.Options

39import Idris.Output

37import Idris.Output

40import Idris.Parser (loadModule)

38import Idris.Parser (loadModule)

41−import Idris.REPL

42

39

43import Idris.Package.Common

40import Idris.Package.Common

44import Idris.Package.Parser

41import Idris.Package.Parser

@@ -336,11 +333,9 @@ auditPackage True ipkg = do

336 getIdrisFiles :: FilePath -> IO [FilePath]

333 getIdrisFiles :: FilePath -> IO [FilePath]

337 getIdrisFiles dir = do

334 getIdrisFiles dir = do

338 contents <- getDirectoryContents dir

335 contents <- getDirectoryContents dir

339− let contents' = filter (\fname -> fname /= "." && fname /= "..") contents

340

336

341 -- [ 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.

337 -- [ 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.

342

338

343−

344 files <- forM contents (findRest dir)

339 files <- forM contents (findRest dir)

345 return $ filter (isIdrisFile) (concat files)

340 return $ filter (isIdrisFile) (concat files)

346

341

src/Idris/Package/Parser.hs−6

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

8{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}

9module Idris.Package.Parser where

10

11−import Idris.AbsSyntaxTree

12import Idris.CmdOptions

11import Idris.CmdOptions

13−import Idris.Core.TT

14import Idris.Package.Common

12import Idris.Package.Common

15import Idris.Parser.Helpers hiding (stringLiteral)

13import Idris.Parser.Helpers hiding (stringLiteral)

16−import Idris.REPL

17−

18−import Util.System

19

14

20import Control.Applicative

15import Control.Applicative

21import Control.Monad.State.Strict

16import Control.Monad.State.Strict

22import Data.List (union)

17import Data.List (union)

23−import Data.Maybe (fromJust, isNothing)

24import System.Directory (doesFileExist)

18import System.Directory (doesFileExist)

25import System.Exit

19import System.Exit

26import System.FilePath (isValid, takeExtension, takeFileName)

20import System.FilePath (isValid, takeExtension, takeFileName)

src/Idris/Parser.hs+7−31

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

8{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

9{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

9 PatternGuards #-}

10 PatternGuards #-}

10{-# OPTIONS_GHC -O0 #-}

11{-# OPTIONS_GHC -O0 #-}

12+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

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

14+

11module Idris.Parser(module Idris.Parser,

15module Idris.Parser(module Idris.Parser,

12 module Idris.Parser.Expr,

16 module Idris.Parser.Expr,

13 module Idris.Parser.Data,

17 module Idris.Parser.Data,

@@ -17,11 +21,9 @@ module Idris.Parser(module Idris.Parser,

17import Idris.AbsSyntax hiding (namespace, params)

21import Idris.AbsSyntax hiding (namespace, params)

18import Idris.Core.Evaluate

22import Idris.Core.Evaluate

19import Idris.Core.TT

23import Idris.Core.TT

20−import Idris.Coverage

21import Idris.Delaborate

24import Idris.Delaborate

22import Idris.Docstrings hiding (Unchecked)

25import Idris.Docstrings hiding (Unchecked)

23import Idris.DSL

26import Idris.DSL

24−import Idris.Elab.Term

25import Idris.Elab.Value

27import Idris.Elab.Value

26import Idris.ElabDecls

28import Idris.ElabDecls

27import Idris.Error

29import Idris.Error

@@ -33,15 +35,11 @@ import Idris.Parser.Data

33import Idris.Parser.Expr

35import Idris.Parser.Expr

34import Idris.Parser.Helpers

36import Idris.Parser.Helpers

35import Idris.Parser.Ops

37import Idris.Parser.Ops

36−import Idris.Providers

37import Idris.Termination

38import Idris.Termination

38import Idris.Unlit

39import Idris.Unlit

39

40

40−import Util.DynamicLinker

41import qualified Util.Pretty as P

42−import Util.System (readSource, writeSource)

42+import Util.System (readSource)

43−

44−import Paths_idris

45

43

46import Prelude hiding (pi)

44import Prelude hiding (pi)

47

45

@@ -53,24 +51,14 @@ import Data.Char

53import Data.Foldable (asum)

51import Data.Foldable (asum)

54import Data.Function

52import Data.Function

55import Data.Generics.Uniplate.Data (descendM)

53import Data.Generics.Uniplate.Data (descendM)

56−import qualified Data.HashSet as HS

57import Data.List

54import Data.List

58import qualified Data.List.Split as Spl

55import qualified Data.List.Split as Spl

59import qualified Data.Map as M

56import qualified Data.Map as M

60import Data.Maybe

57import Data.Maybe

61−import Data.Monoid

62import Data.Ord

58import Data.Ord

63−import qualified Data.Set as S

64import qualified Data.Text as T

59import qualified Data.Text as T

65−import Debug.Trace

66import qualified System.Directory as Dir (makeAbsolute)

60import qualified System.Directory as Dir (makeAbsolute)

67import System.FilePath

61import 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

74import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

62import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

75import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

63import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

76import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

64import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

@@ -806,7 +794,6 @@ mutual :: SyntaxInfo -> IdrisParser [PDecl]

806mutual syn =

794mutual syn =

807 do reservedHL "mutual"

795 do reservedHL "mutual"

808 openBlock

796 openBlock

809− let pvars = syn_params syn

810 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

797 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

811 closeBlock

798 closeBlock

812 fc <- getFC

799 fc <- getFC

@@ -1157,7 +1144,6 @@ clause syn

1157 Just t -> return t

1144 Just t -> return t

1158 Nothing -> fail "Invalid clause"

1145 Nothing -> fail "Invalid clause"

1159 (do r <- rhs syn n

1146 (do r <- rhs syn n

1160− let ctxt = tt_ctxt ist

1161 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1147 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1162 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1148 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1163 popIndent

1149 popIndent

@@ -1181,8 +1167,6 @@ clause syn

1181 fc <- getFC

1167 fc <- getFC

1182 n_in <- fst <$> fnName; let n = expandNS syn n_in

1168 n_in <- fst <$> fnName; let n = expandNS syn n_in

1183 r <- rhs syn n

1169 r <- rhs syn n

1184− ist <- get

1185− let ctxt = tt_ctxt ist

1186 let wsyn = syn { syn_namespace = [] }

1170 let wsyn = syn { syn_namespace = [] }

1187 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1171 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1188 popIndent

1172 popIndent

@@ -1239,8 +1223,6 @@ clause syn

1239 wargs <- many (wExpr syn)

1223 wargs <- many (wExpr syn)

1240 let capp = PApp fc (PRef nfc [nfc] n) args

1224 let capp = PApp fc (PRef nfc [nfc] n) args

1241 (do r <- rhs syn n

1225 (do r <- rhs syn n

1242− ist <- get

1243− let ctxt = tt_ctxt ist

1244 let wsyn = syn { syn_namespace = [] }

1226 let wsyn = syn { syn_namespace = [] }

1245 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1227 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1246 popIndent

1228 popIndent

@@ -1585,11 +1567,6 @@ parseImports fname input

1585 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

1567 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

1586 return ((mdoc, mname, ps, mrk'), annots, i)

1568 return ((mdoc, mname, ps, mrk'), annots, i)

1587

1569

1588− imp m = ImportInfo False (toPath m)

1589− Nothing [] NoFC NoFC

1590− ns = Spl.splitOn "."

1591− toPath = foldl1' (</>) . ns

1592−

1593 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

1570 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

1594 addPath [] _ = []

1571 addPath [] _ = []

1595 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

1572 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

@@ -1685,6 +1662,7 @@ loadModule' f phase

1685loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1662loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1686loadFromIFile reexp phase i@(IBC fn src) maxline

1663loadFromIFile reexp phase i@(IBC fn src) maxline

1687 = do logParser 1 $ "Skipping " ++ getSrcFile i

1664 = do logParser 1 $ "Skipping " ++ getSrcFile i

1665+ logParser 3 $ "loadFromIFile i" ++ show i

1688 idrisCatch (loadIBC reexp phase fn)

1666 idrisCatch (loadIBC reexp phase fn)

1689 (\err -> ierror $ LoadingFailed fn err)

1667 (\err -> ierror $ LoadingFailed fn err)

1690 where

1668 where

@@ -1893,8 +1871,6 @@ loadSource lidr f toline

1893

1871

1894{-| Adds names to hide list -}

1872{-| Adds names to hide list -}

1895addHides :: Ctxt Accessibility -> Idris ()

1873addHides :: 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)

1899 where doHide (n, a) = do setAccessibility n a

1875 where doHide (n, a) = do setAccessibility n a

1900 addIBC (IBCAccess n a)

1876 addIBC (IBCAccess n a)

src/Idris/Parser/Data.hs−25

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

9module Idris.Parser.Data where

10

11import Idris.AbsSyntax

12−import Idris.Core.Evaluate

13import Idris.Core.TT

12import Idris.Core.TT

14import Idris.Docstrings

13import Idris.Docstrings

15−import Idris.DSL

16import Idris.Options

14import Idris.Options

17import Idris.Parser.Expr

15import Idris.Parser.Expr

18import Idris.Parser.Helpers

16import Idris.Parser.Helpers

@@ -21,25 +19,11 @@ import Idris.Parser.Ops

21import Prelude hiding (pi)

19import Prelude hiding (pi)

22

20

23import Control.Applicative

21import Control.Applicative

24−import Control.Monad

25import Control.Monad.State.Strict

22import Control.Monad.State.Strict

26−import qualified Data.ByteString.UTF8 as UTF8

27−import Data.Char

28−import qualified Data.HashSet as HS

29import Data.List

23import Data.List

30−import qualified Data.List.Split as Spl

31import Data.Maybe

24import 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

40import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

25import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

41 stringLiteral, symbol, whiteSpace)

26 stringLiteral, symbol, whiteSpace)

42−import Text.Trifecta.Delta

43

27

44{- | Parses a record type declaration

28{- | Parses a record type declaration

45Record ::=

29Record ::=

@@ -70,18 +54,9 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

70 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

54 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

71 <?> "record type declaration"

55 <?> "record type declaration"

72 where

56 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−

78 getName (Just (n, _), _, _, _) = Just n

57 getName (Just (n, _), _, _, _) = Just n

79 getName _ = Nothing

58 getName _ = Nothing

80

59

81− toFreeze :: Maybe Accessibility -> Maybe Accessibility

82− toFreeze (Just Frozen) = Just Private

83− toFreeze x = x

84−

85 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

60 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

86 recordBody syn tyn = do

61 recordBody syn tyn = do

87 ist <- get

62 ist <- get

src/Idris/Parser/Expr.hs−12

@@ -21,24 +21,12 @@ import Prelude hiding (pi)

21import Control.Applicative

22import Control.Monad

23import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

25−import Data.Char

26import Data.Function (on)

24import Data.Function (on)

27−import qualified Data.HashSet as HS

28import Data.List

25import Data.List

29−import qualified Data.List.Split as Spl

30import Data.Maybe

26import 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

35import Text.Parser.Expression

27import 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

39import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

28import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

40 stringLiteral, symbol, whiteSpace)

29 stringLiteral, symbol, whiteSpace)

41−import Text.Trifecta.Delta

42

30

43-- | Allow implicit type declarations

31-- | Allow implicit type declarations

44allowImp :: SyntaxInfo -> SyntaxInfo

32allowImp :: SyntaxInfo -> SyntaxInfo

src/Idris/Parser/Helpers.hs−6

@@ -18,8 +18,6 @@ import Idris.Docstrings

18import Idris.Options

19import Idris.Output (iWarn)

20

21−import qualified Util.Pretty as Pretty (text)

22−

23import Prelude hiding (pi)

21import Prelude hiding (pi)

24

22

25import Control.Applicative

23import Control.Applicative

@@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8

29import Data.Char

27import Data.Char

30import qualified Data.HashSet as HS

28import qualified Data.HashSet as HS

31import Data.List

29import Data.List

32−import qualified Data.List.Split as Spl

33import qualified Data.Map as M

30import qualified Data.Map as M

34import Data.Maybe

31import Data.Maybe

35−import Data.Monoid

36import qualified Data.Text as T

32import qualified Data.Text as T

37−import Debug.Trace

38import System.FilePath

33import System.FilePath

39import qualified Text.Parser.Char as Chr

34import qualified Text.Parser.Char as Chr

40−import Text.Parser.Expression

41import Text.Parser.LookAhead

35import Text.Parser.LookAhead

42import qualified Text.Parser.Token as Tok

36import qualified Text.Parser.Token as Tok

43import qualified Text.Parser.Token.Highlight as Hi

37import qualified Text.Parser.Token.Highlight as Hi

src/Idris/Parser/Ops.hs−13

@@ -18,23 +18,10 @@ import Prelude hiding (pi)

18import Control.Applicative

19import Control.Monad

20import Control.Monad.State.Strict

21−import qualified Data.ByteString.UTF8 as UTF8

22−import Data.Char

23−import qualified Data.HashSet as HS

24import Data.List

21import 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

31import Text.Parser.Expression

22import 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

35import Text.Trifecta hiding (char, charLiteral, natural, span, string,

23import Text.Trifecta hiding (char, charLiteral, natural, span, string,

36 stringLiteral, symbol, whiteSpace)

24 stringLiteral, symbol, whiteSpace)

37−import Text.Trifecta.Delta

38

25

39-- | Creates table for fixity declarations to build expression parser

26-- | Creates table for fixity declarations to build expression parser

40-- using pre-build and user-defined operator/fixity declarations

27-- using pre-build and user-defined operator/fixity declarations

src/Idris/PartialEval.hs−7

@@ -19,10 +19,7 @@ import Idris.Core.Evaluate

19import Idris.Core.TT

20import Idris.Delaborate

21

22−import Control.Applicative

23import Control.Monad.State

22import Control.Monad.State

24−import Data.Maybe

25−import Debug.Trace

26

23

27-- | Data type representing binding-time annotations for partial evaluation of arguments

24-- | Data type representing binding-time annotations for partial evaluation of arguments

28data PEArgType = ImplicitS Name -- ^ Implicit static argument

25data PEArgType = ImplicitS Name -- ^ Implicit static argument

@@ -261,10 +258,6 @@ mkNewPats ist d ns newname sname lhs rhs =

261 mkRHSargs (_ : ns) as = mkRHSargs ns as

258 mkRHSargs (_ : ns) as = mkRHSargs ns as

262 mkRHSargs _ _ = []

259 mkRHSargs _ _ = []

263

260

264− mkSubst :: (Term, Term) -> Maybe (Name, Term)

265− mkSubst (P _ n _, t) = Just (n, t)

266− mkSubst _ = Nothing

267−

268-- | Creates a new declaration for a specialised function application.

261-- | Creates a new declaration for a specialised function application.

269-- Simple version at the moment: just create a version which is a direct

262-- Simple version at the moment: just create a version which is a direct

270-- application of the function to be specialised.

263-- application of the function to be specialised.

src/Idris/Primitives.hs+1−41

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

9

10module Idris.Primitives(primitives, Prim(..)) where

11

12−import Idris.AbsSyntax

13import Idris.Core.Evaluate

12import Idris.Core.Evaluate

14import Idris.Core.TT

13import Idris.Core.TT

15import IRTS.Lang

14import IRTS.Lang

@@ -18,9 +17,6 @@ import Data.Bits

18import Data.Char

17import Data.Char

19import Data.Function (on)

18import Data.Function (on)

20import Data.Int

19import Data.Int

21−import qualified Data.Vector.Unboxed as V

22−import Data.Word

23−import Debug.Trace

24

20

25data Prim = Prim { p_name :: Name,

21data Prim = Prim { p_name :: Name,

26 p_type :: Type,

22 p_type :: Type,

@@ -34,10 +30,9 @@ ty :: [Const] -> Const -> Type

34ty [] x = Constant x

30ty [] x = Constant x

35ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

31ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

36

32

37−total, partial, iopartial :: Totality

33+total, partial :: Totality

38total = Total []

34total = Total []

39partial = Partial NotCovering

35partial = Partial NotCovering

40−iopartial = Partial ExternalIO

41

36

42primitives :: [Prim]

37primitives :: [Prim]

43primitives =

38primitives =

@@ -235,36 +230,6 @@ intConv ity =

235 (1, LFloatInt ity) total

230 (1, LFloatInt ity) total

236 ]

231 ]

237

232

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−

268iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

233iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

269iCmp ity op self impl irop totality

234iCmp ity op self impl irop totality

270 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

235 = 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

295 Just $ I i

260 Just $ I i

296bfBin _ _ = Nothing

261bfBin _ _ = Nothing

297

262

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−

303bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const

263bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const

304bsBin op [Str x, Str y]

264bsBin op [Str x, Str y]

305 = let i = (if op x y then 1 else 0) in

265 = let i = (if op x y then 1 else 0) in

src/Idris/ProofSearch.hs+1−17

@@ -16,21 +16,17 @@ module Idris.ProofSearch(

16 ) where

17

18import Idris.AbsSyntax

19−import Idris.Core.CaseTree

20import Idris.Core.Elaborate hiding (Tactic(..))

19import Idris.Core.Elaborate hiding (Tactic(..))

21import Idris.Core.Evaluate

20import Idris.Core.Evaluate

22import Idris.Core.TT

21import Idris.Core.TT

23−import Idris.Core.Typecheck

24import Idris.Core.Unify

22import Idris.Core.Unify

25import Idris.Delaborate

23import Idris.Delaborate

26−import Idris.Error

27

24

28import Control.Applicative ((<$>))

25import Control.Applicative ((<$>))

29import Control.Monad

26import Control.Monad

30import Control.Monad.State.Strict

27import Control.Monad.State.Strict

31import Data.List

28import Data.List

32import qualified Data.Set as S

29import qualified Data.Set as S

33−import Debug.Trace

34

30

35-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

31-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

36

32

@@ -52,7 +48,6 @@ trivialHoles psnames ok elab ist

52 tryAll ((x, _, b):xs)

48 tryAll ((x, _, b):xs)

53 = do -- if type of x has any holes in it, move on

49 = do -- if type of x has any holes in it, move on

54 hs <- get_holes

50 hs <- get_holes

55− let badhs = hs -- filter (flip notElem holesOK) hs

56 g <- goal

51 g <- goal

57 -- anywhere but the top is okay for a hole, if holesOK set

52 -- anywhere but the top is okay for a hole, if holesOK set

58 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

53 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

@@ -88,7 +83,6 @@ trivialTCs ok elab ist

88 tryAll ((x, _, b):xs)

83 tryAll ((x, _, b):xs)

89 = do -- if type of x has any holes in it, move on

84 = do -- if type of x has any holes in it, move on

90 hs <- get_holes

85 hs <- get_holes

91− let badhs = hs -- filter (flip notElem holesOK) hs

92 g <- goal

86 g <- goal

93 env <- get_env

87 env <- get_env

94 -- anywhere but the top is okay for a hole, if holesOK set

88 -- 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

233 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs

227 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs

234 notHole _ _ = True

228 notHole _ _ = True

235

229

236− inHS hs (P _ n _) = n `elem` hs

237− isHS _ _ = False

238−

239 toUN t@(P nt (MN i n) ty)

230 toUN t@(P nt (MN i n) ty)

240 | ('_':xs) <- str n = t

231 | ('_':xs) <- str n = t

241 | otherwise = P nt (UN n) ty

232 | otherwise = P nt (UN n) ty

@@ -444,12 +435,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

444 isMeta ns (P _ n _) = n `elem` ns

435 isMeta ns (P _ n _) = n `elem` ns

445 isMeta _ _ = False

436 isMeta _ _ = False

446

437

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−

453 numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

438 numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

454

439

455 addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn

440 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

487 | otherwise

472 | otherwise

488 = do lams <- introImps

473 = do lams <- introImps

489 t <- goal

474 t <- goal

490− let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

491-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

475-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

492-- else do

476-- else do

493 -- if there's a hole in the goal, don't even try

477 -- 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

505-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

489-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

506 mapM_ (\ (_,n) -> do focus n

490 mapM_ (\ (_,n) -> do focus n

507 t' <- goal

491 t' <- goal

508− let (tc', ttype) = unApply (getRetTy t')

492+ let (tc', _) = unApply (getRetTy t')

509 let got = fst (unApply (getRetTy t))

493 let got = fst (unApply (getRetTy t))

510 let depth' = if tc' `elem` tcs

494 let depth' = if tc' `elem` tcs

511 then depth - 1 else depth

495 then depth - 1 else depth

src/Idris/Prover.hs+4−7

@@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where

11-- Hack for GHC 7.10 and earlier compat without CPP or warnings

12-- This exludes (<$>) as fmap, because wl-pprint uses it for newline

13import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,

14− concatMap, elem, error, flip, foldl, foldr, fst, id, init,

14+ concatMap, elem, error, foldl, foldr, fst, id, init, length,

15− length, lines, map, not, null, repeat, reverse, tail, zip, ($),

15+ lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),

16− (&&), (++), (.), (||))

16+ (++), (.), (||))

17

18import Idris.AbsSyntax

19−import Idris.AbsSyntaxTree

20import Idris.Completion

19import Idris.Completion

21import Idris.Core.CaseTree

20import Idris.Core.CaseTree

22import Idris.Core.Elaborate hiding (Tactic(..))

21import Idris.Core.Elaborate hiding (Tactic(..))

@@ -41,7 +40,6 @@ import Util.Pretty

41

40

42import Control.DeepSeq

41import Control.DeepSeq

43import Control.Monad.State.Strict

42import Control.Monad.State.Strict

44−import Debug.Trace

45import System.Console.Haskeline

43import System.Console.Haskeline

46import System.Console.Haskeline.History

44import System.Console.Haskeline.History

47import System.IO (Handle, hPutStrLn, stdin, stdout)

45import System.IO (Handle, hPutStrLn, stdin, stdout)

@@ -166,7 +164,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

166 iputGoal rendered

164 iputGoal rendered

167

165

168 where

166 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

170

168

171 ppo = ppOptionIst ist

169 ppo = ppOptionIst ist

172

170

@@ -502,7 +500,6 @@ checkType e prf t = do

502 putIState ist { tt_ctxt = ctxt' }

500 putIState ist { tt_ctxt = ctxt' }

503 (tm, ty) <- elabVal (recinfo proverfc) ERHS t

501 (tm, ty) <- elabVal (recinfo proverfc) ERHS t

504 let ppo = ppOptionIst ist

502 let ppo = ppOptionIst ist

505− ty' = normaliseC ctxt [] ty

506 infixes = idris_infixes ist

503 infixes = idris_infixes ist

507 action = case tm of

504 action = case tm of

508 TType _ ->

505 TType _ ->

src/Idris/Providers.hs−2

@@ -13,8 +13,6 @@ module Idris.Providers (

13 ) where

14

15import Idris.AbsSyntax

16−import Idris.AbsSyntaxTree

17−import Idris.Core.Evaluate

18import Idris.Core.TT

16import Idris.Core.TT

19import Idris.Error

17import Idris.Error

20

18

src/Idris/REPL.hs+8−21

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

6-}

7

8{-# LANGUAGE FlexibleContexts, PatternGuards #-}

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

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

9

11

10module Idris.REPL

12module Idris.REPL

11 ( idemodeStart

13 ( idemodeStart

@@ -49,7 +51,6 @@ import Idris.Core.Execute (execute)

49import Idris.Core.TT

51import Idris.Core.TT

50import Idris.Core.Unify

52import Idris.Core.Unify

51import Idris.Core.WHNF

53import Idris.Core.WHNF

52−import Idris.Coverage

53import Idris.DataOpts

54import Idris.DataOpts

54import Idris.Delaborate

55import Idris.Delaborate

55import Idris.Docs

56import Idris.Docs

@@ -99,8 +100,6 @@ import Util.Pretty hiding ((</>))

99import Util.System

100import Util.System

100import Version_idris (gitHash)

101import Version_idris (gitHash)

101

102

102−import Debug.Trace

103−

104-- | Run the REPL

103-- | Run the REPL

105repl :: IState -- ^ The initial state

104repl :: IState -- ^ The initial state

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

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

@@ -404,7 +403,6 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

404 | (n, (_, i, _, _, _)) <- idris_metavars ist

403 | (n, (_, i, _, _, _)) <- idris_metavars ist

405 , not (n `elem` primDefs)

404 , not (n `elem` primDefs)

406 ]

405 ]

407− let ppo = ppOptionIst ist

408 -- splitMvs is a list of pairs of names and their split types

406 -- splitMvs is a list of pairs of names and their split types

409 let splitMvs = [ (n, (premises, concl, tm))

407 let splitMvs = [ (n, (premises, concl, tm))

410 | (n, i, ty) <- mvTys ist mvs

408 | (n, i, ty) <- mvTys ist mvs

@@ -422,14 +420,11 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

422 runIO . hPutStrLn h $

420 runIO . hPutStrLn h $

423 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

421 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

424 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

422 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−

428 -- | Split a function type into a pair of premises, conclusion.

423 -- | Split a function type into a pair of premises, conclusion.

429 -- Each maintains both the original and delaborated versions.

424 -- Each maintains both the original and delaborated versions.

430 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

425 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

431 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

426 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

433 ((n, t, delabTy' ist [] [] t False False True):hs,

428 ((n, t, delabTy' ist [] [] t False False True):hs,

434 c, delabTy' ist [] [] c False False True)

429 c, delabTy' ist [] [] c False False True)

435 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

430 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

@@ -982,7 +977,7 @@ process fn (Check (PRef _ _ n))

982 = do ctxt <- getContext

977 = do ctxt <- getContext

983 ist <- getIState

978 ist <- getIState

984 let ppo = ppOptionIst ist

979 let ppo = ppOptionIst ist

985− case lookupNames n ctxt of

980+ case lookupVisibleNames n ctxt of

986 ts@(t:_) ->

981 ts@(t:_) ->

987 case lookup t (idris_metavars ist) of

982 case lookup t (idris_metavars ist) of

988 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

983 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

@@ -990,6 +985,9 @@ process fn (Check (PRef _ _ n))

990 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

985 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

991 [] -> iPrintError $ "No such variable " ++ show n

986 [] -> iPrintError $ "No such variable " ++ show n

992 where

987 where

988+ lookupVisibleNames :: Name -> Context -> [Name]

989+ lookupVisibleNames n ctxt = map fst $ lookupCtxtName n (visibleDefinitions ctxt)

990+

993 showMetavarInfo ppo ist n i

991 showMetavarInfo ppo ist n i

994 = case lookupTy n (tt_ctxt ist) of

992 = case lookupTy n (tt_ctxt ist) of

995 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

993 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

@@ -1020,8 +1018,7 @@ process fn (Check t)

1020 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1018 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1021 ctxt <- getContext

1019 ctxt <- getContext

1022 ist <- getIState

1020 ist <- getIState

1023− let ppo = ppOptionIst ist

1024− ty' = if opt_evaltypes (idris_options ist)

1021+ let ty' = if opt_evaltypes (idris_options ist)

1025 then normaliseC ctxt [] ty

1022 then normaliseC ctxt [] ty

1026 else ty

1023 else ty

1027 case tm of

1024 case tm of

@@ -1126,7 +1123,6 @@ process fn (DebugInfo n)

1126 when (not (null imps)) $ iputStrLn (show imps)

1123 when (not (null imps)) $ iputStrLn (show imps)

1127 let d = lookupDefAcc n False (tt_ctxt i)

1124 let d = lookupDefAcc n False (tt_ctxt i)

1128 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1125 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1129− let cg = lookupCtxtName n (idris_callgraph i)

1130 i <- getIState

1126 i <- getIState

1131 let cg' = lookupCtxtName n (idris_callgraph i)

1127 let cg' = lookupCtxtName n (idris_callgraph i)

1132 sc <- checkSizeChange n

1128 sc <- checkSizeChange n

@@ -1457,12 +1453,6 @@ process fn (TransformInfo n)

1457 ts' = showTrans i ts in

1453 ts' = showTrans i ts in

1458 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

1454 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

1459

1455

1460−-- iRenderOutput (pretty lhs)

1461−-- iputStrLn " ==> "

1462−-- iPrintTermWithType (pprintDelab i rhs)

1463−-- iputStrLn "---------------"

1464−-- showTrans i ts

1465−

1466process fn (PPrint fmt width (PRef _ _ n))

1456process fn (PPrint fmt width (PRef _ _ n))

1467 = do outs <- pprintDef False n

1457 = do outs <- pprintDef False n

1468 iPrintResult =<< renderExternal fmt width (vsep outs)

1458 iPrintResult =<< renderExternal fmt width (vsep outs)

@@ -1470,10 +1460,7 @@ process fn (PPrint fmt width (PRef _ _ n))

1470

1460

1471process fn (PPrint fmt width t)

1461process fn (PPrint fmt width t)

1472 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1462 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1473− ctxt <- getContext

1474 ist <- getIState

1463 ist <- getIState

1475− let ppo = ppOptionIst ist

1476− ty' = normaliseC ctxt [] ty

1477 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

1464 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

1478

1465

1479

1466

src/Idris/REPL/Parser.hs+1−6

@@ -21,17 +21,14 @@ import Idris.REPL.Commands

21

22import Control.Applicative

23import Control.Monad.State.Strict

24−import qualified Data.ByteString.UTF8 as UTF8

25import Data.Char (isSpace, toLower)

24import Data.Char (isSpace, toLower)

26import Data.List

25import Data.List

27import Data.List.Split (splitOn)

26import Data.List.Split (splitOn)

28−import Debug.Trace

29import System.Console.ANSI (Color(..))

27import System.Console.ANSI (Color(..))

30import System.FilePath ((</>))

28import System.FilePath ((</>))

31import Text.Parser.Char (anyChar, oneOf)

29import Text.Parser.Char (anyChar, oneOf)

32import Text.Parser.Combinators

30import Text.Parser.Combinators

33−import Text.Trifecta (Result, parseString)

31+import Text.Trifecta (Result)

34−import Text.Trifecta.Delta

35

32

36parseCmd :: IState -> String -> String -> Result (Either String Command)

33parseCmd :: IState -> String -> String -> Result (Either String Command)

37parseCmd i inputname = P.runparser pCmd i inputname . trim

34parseCmd i inputname = P.runparser pCmd i inputname . trim

@@ -181,8 +178,6 @@ namespaceArgCmd names command doc =

181 (names, NamespaceArg, doc, namespaceArg command)

178 (names, NamespaceArg, doc, namespaceArg command)

182exprArgCmd names command doc =

179exprArgCmd names command doc =

183 (names, ExprArg, doc, exprArg command)

180 (names, ExprArg, doc, exprArg command)

184−metavarArgCmd names command doc =

185− (names, MetaVarArg, doc, fnNameArg command)

186optArgCmd names command doc =

181optArgCmd names command doc =

187 (names, OptionArg, doc, optArg command)

182 (names, OptionArg, doc, optArg command)

188proofArgCmd names command doc =

183proofArgCmd names command doc =

src/Idris/Termination.hs+3−11

@@ -15,10 +15,9 @@ import Idris.Core.TT

15import Idris.Delaborate

16import Idris.Error

17import Idris.Options

18−import Idris.Output (iWarn, iputStrLn)

18+import Idris.Output (iWarn)

19

20import Control.Monad.State.Strict

21−import Data.Char

22import Data.Either

21import Data.Either

23import Data.List

22import Data.List

24import Data.Maybe

23import Data.Maybe

@@ -143,9 +142,6 @@ checkPositive mut_ns (cn, ty')

143calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

142calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

144calcTotality fc n pats

143calcTotality fc n pats

145 = do i <- getIState

144 = do i <- getIState

146− let opts = case lookupCtxt n (idris_flags i) of

147− [fs] -> fs

148− _ -> []

149 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

145 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

150 (failure : _) -> return failure

146 (failure : _) -> return failure

151 _ -> checkSizeChange n

147 _ -> checkSizeChange n

@@ -302,7 +298,7 @@ buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]

302buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

298buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

303 scgPat (lhs, rhs) = let lhs' = delazy lhs

299 scgPat (lhs, rhs) = let lhs' = delazy lhs

304 rhs' = delazy rhs

300 rhs' = delazy rhs

305− (f, pargs) = unApply (dePat lhs') in

301+ (_, pargs) = unApply (dePat lhs') in

306 findCalls [] Toplevel (dePat rhs') (patvars lhs')

302 findCalls [] Toplevel (dePat rhs') (patvars lhs')

307 (zip pargs [0..])

303 (zip pargs [0..])

308

304

@@ -393,7 +389,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

393 fccPat cases pvs pargs args g (lhs, rhs)

389 fccPat cases pvs pargs args g (lhs, rhs)

394 = let lhs' = delazy lhs

390 = let lhs' = delazy lhs

395 rhs' = delazy rhs

391 rhs' = delazy rhs

396− (f, pargs_case) = unApply (dePat lhs')

392+ (_, pargs_case) = unApply (dePat lhs')

397 -- pargs is a pair of a term, and the argument position that

393 -- pargs is a pair of a term, and the argument position that

398 -- term appears in. If any of the arguments to the case block

394 -- term appears in. If any of the arguments to the case block

399 -- are also on the lhs, we also want those patterns to appear

395 -- are also on the lhs, we also want those patterns to appear

@@ -545,10 +541,6 @@ checkMP ist topfn i mp = if i > 0

545 collapse paths

541 collapse paths

546 else tryPath 0 [] mp 0

542 else tryPath 0 [] mp 0

547 where

543 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−

552 mkBig (e, d) = (e, 10000)

544 mkBig (e, d) = (e, 10000)

553

545

554 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

546 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

src/Idris/Transforms.hs−3

@@ -16,11 +16,8 @@ module Idris.Transforms(

16 ) where

17

18import Idris.AbsSyntax

19−import Idris.Core.CaseTree

20import Idris.Core.TT

19import Idris.Core.TT

21

20

22−import Debug.Trace

23−

24transformPats :: IState -> [Either Term (Term, Term)] ->

21transformPats :: IState -> [Either Term (Term, Term)] ->

25 [Either Term (Term, Term)]

22 [Either Term (Term, Term)]

26transformPats ist ps = map tClause ps where

23transformPats ist ps = map tClause ps where

src/Idris/TypeSearch.hs+2−6

@@ -13,8 +13,7 @@ module Idris.TypeSearch (

13 , defaultScoreFunction

14 ) where

15

16−import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,

16+import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)

17− logLvl, putIState)

18import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

17import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

19 Idris, InterfaceInfo, OutputMode(..), PTerm,

18 Idris, InterfaceInfo, OutputMode(..), PTerm,

20 defaultSyntax, eqTy, implicitAllowed,

19 defaultSyntax, eqTy, implicitAllowed,

@@ -58,7 +57,6 @@ searchByType pkgs pterm = do

58 mapM_ loadPkgIndex pkgs

57 mapM_ loadPkgIndex pkgs

59 pterm' <- addUsingConstraints syn emptyFC pterm

58 pterm' <- addUsingConstraints syn emptyFC pterm

60 pterm'' <- implicit toplevel syn name pterm'

59 pterm'' <- implicit toplevel syn name pterm'

61− let pterm''' = addImpl [] i pterm''

62 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

60 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

63 let names = searchUsing searchPred i ty

61 let names = searchUsing searchPred i ty

64 let names' = take numLimit names

62 let names' = take numLimit names

@@ -304,7 +302,7 @@ interfaceUnify interfaceInfo ctxt ty tyTry = do

304

302

305isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

303isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

306isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

304isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

307− (clss, args) = unApply ty

305+ (clss, _) = unApply ty

308 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

306 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

309 getInterfaceName _ = []

307 getInterfaceName _ = []

310

308

@@ -358,8 +356,6 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

358 usedns = map fst startingHoles

356 usedns = map fst startingHoles

359 startingHoles = argNames1 ++ argNames2

357 startingHoles = argNames1 ++ argNames2

360

358

361− startingTypes = [(retTy1, retTy2)]

362−

363

359

364 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

360 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

365 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types

361 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types

src/Util/DynamicLinker.hs+16−9

@@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..)

13 ) where

14

15#ifdef IDRIS_FFI

16−import Foreign.LibFFI

17−import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)

18import System.Directory

16import 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

20import Control.Exception (IOException, throwIO, try)

24import Control.Exception (IOException, throwIO, try)

25+import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)

26+#ifdef linux_HOST_OS

21−import Data.Array (Array, bounds, inRange, (!))

27+import Data.Array (bounds, inRange, (!))

22import Data.Functor ((<$>))

28import Data.Functor ((<$>))

23import Data.Maybe (catMaybes)

29import Data.Maybe (catMaybes)

30+#else

31+import Data.Array (bounds, (!))

32+#endif

24import System.FilePath.Posix ((</>))

33import System.FilePath.Posix ((</>))

25import System.Posix.DynamicLinker

34import System.Posix.DynamicLinker

26import Text.Regex.TDFA

35import Text.Regex.TDFA

27−#else

36+#endif

28−import qualified Control.Exception as Exception (IOException, catch)

37+

29−import System.FilePath.Windows ((</>))

38+#ifdef mingw32_HOST_OS

30−import System.Win32.DLL

31−import System.Win32.Types

32type DL = HMODULE

39type DL = HMODULE

33#endif

40#endif

34

41

stack.yaml+3

@@ -9,6 +9,9 @@ flags:

9 FFI: true

10 GMP: true

11

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

12extra-deps:

15extra-deps:

13 - binary-0.8.5.1

16 - binary-0.8.5.1

14 - cheapskate-0.1.1

17 - cheapskate-0.1.1

test/TestData.hs+8−2

@@ -71,7 +71,9 @@ testFamiliesData = [

71 ( 16, ANY ),

72 ( 17, ANY ),

73 ( 18, ANY ),

74− ( 19, ANY )]),

74+ ( 19, ANY ),

75+ ( 20, ANY ),

76+ ( 21, ANY )]),

75 ("bignum", "Bignum",

77 ("bignum", "Bignum",

76 [ ( 1, ANY ),

78 [ ( 1, ANY ),

77 ( 2, ANY )]),

79 ( 2, ANY )]),

@@ -157,7 +159,11 @@ testFamiliesData = [

157 ( 13, ANY ),

159 ( 13, ANY ),

158 ( 14, C_CG ),

160 ( 14, C_CG ),

159 ( 15, ANY ),

161 ( 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 )]),

161 ("interfaces", "Interfaces",

167 ("interfaces", "Interfaces",

162 [ ( 1, ANY ),

168 [ ( 1, ANY ),

163 ( 2, ANY ),

169 ( 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"

6./shebang-node.idr

7./shebang-args.idr aaa

8./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