21124c3 · Idris-dev · git.iko.soy

CHANGELOG+7

compare with master

unifiedsplit

@@ -1,3 +1,9 @@

1+New in 0.9.14:

2+--------------

3+* Support for running tests for a package with the tests section of .ipkg files and the

4+ --testpkg command-line option

5+

6+

1New in 0.9.13:

7New in 0.9.13:

2--------------

8--------------

3* IDE support for retrieving structured information about metavariables

9* IDE support for retrieving structured information about metavariables

@@ -25,6 +31,7 @@ New in 0.9.13:

25* Extend :addclause to add instance bodies as well as definitions

31* Extend :addclause to add instance bodies as well as definitions

26* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.

32* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.

27* Move foldl into Foldable so it can be overridden.

33* Move foldl into Foldable so it can be overridden.

34+* Experimental :search REPL command for finding functions by type

28

35

29Internal changes

36Internal changes

30

37

idris.cabal+10−2

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.12

2+Version: 0.9.13

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -90,6 +90,7 @@ Extra-source-files:

90 libs/base/Language/Reflection/*.idr

91 libs/base/Makefile

92 libs/base/Network/*.idr

93+ libs/base/System/*.idr

93 libs/base/System/Concurrency/*.idr

94 libs/base/System/Concurrency/*.idr

94 libs/base/Syntax/*.idr

95 libs/base/Syntax/*.idr

95

96

@@ -270,6 +271,9 @@ Extra-source-files:

270 test/basic009/*.idr

271 test/basic009/*.idr

271 test/basic009/expected

272 test/basic009/expected

272 test/basic009/B/*.idr

273 test/basic009/B/*.idr

274+ test/basic010/run

275+ test/basic010/*.idr

276+ test/basic010/expected

273

277

274 test/buffer001-disabled/*.idr

278 test/buffer001-disabled/*.idr

275 test/buffer001-disabled/run

279 test/buffer001-disabled/run

@@ -452,6 +456,9 @@ Extra-source-files:

452 test/totality007/*.ipkg

456 test/totality007/*.ipkg

453 test/totality007/src/*.idr

457 test/totality007/src/*.idr

454 test/totality007/expected

458 test/totality007/expected

459+ test/totality008/run

460+ test/totality008/*.idr

461+ test/totality008/expected

455

462

456 test/tutorial001/run

463 test/tutorial001/run

457 test/tutorial001/*.idr

464 test/tutorial001/*.idr

@@ -559,6 +566,7 @@ Library

559 , Idris.REPL

566 , Idris.REPL

560 , Idris.REPLParser

567 , Idris.REPLParser

561 , Idris.Transforms

568 , Idris.Transforms

569+ , Idris.TypeSearch

562 , Idris.Unlit

570 , Idris.Unlit

563 , Idris.WhoCalls

571 , Idris.WhoCalls

564 , Idris.CmdOptions

572 , Idris.CmdOptions

@@ -615,7 +623,7 @@ Library

615 , language-java >= 0.2.6

623 , language-java >= 0.2.6

616 , lens >= 4.1.1

624 , lens >= 4.1.1

617 , mtl

625 , mtl

618− , parsers >= 0.9

626+ , parsers >= 0.9 && < 0.11.0.2

619 , pretty

627 , pretty

620 , process

628 , process

621 , split

629 , split

jsrts/Runtime-browser.js+11

@@ -1,3 +1,14 @@

1var __IDRRT__print = function(s) {

2 console.log(s);

3};

4+

5+

6+var __IDRRT__systemInfo = function(index) {

7+ switch(index) {

8+ case 0:

9+ return "javascript";

10+ case 1:

11+ return navigator.platform;

12+ }

13+ return "";

14+}

jsrts/Runtime-node.js+11

@@ -4,3 +4,14 @@ var __IDRRT__print = (function() {

4 util.print(s);

5 };

6})();

7+

8+var __IDRRT__systemInfo = function(index) {

9+ var os = require('os')

10+ switch(index) {

11+ case 0:

12+ return "node";

13+ case 1:

14+ return os.platform();

15+ }

16+ return "";

17+}

libs/base/Data/Buffer.idr+28−28

@@ -36,15 +36,15 @@ bitsFromFin : Fin n -> Bits64

36bitsFromFin fZ = 0

37bitsFromFin (fS k) = 1 + bitsFromFin k

38

39−-- Allocate an empty Buffer. The size hint can be used to avoid

39+||| Allocate an empty Buffer. The size hint can be used to avoid

40−-- unnecessary reallocations and copies under the hood if the

40+||| unnecessary reallocations and copies under the hood if the

41−-- approximate ultimate size of the Buffer is known. Users can assume

41+||| approximate ultimate size of the Buffer is known. Users can assume

42−-- the new Buffer is word-aligned.

42+||| the new Buffer is word-aligned.

43public

44allocate : ( hint : Nat ) -> Buffer Z

45allocate = MkBuffer Z . prim__allocate . bitsFromNat

46

47−-- Append count repetitions of a Buffer to another Buffer

47+||| Append count repetitions of a Buffer to another Buffer

48%assert_total

49public

50appendBuffer : Buffer n ->

@@ -63,13 +63,13 @@ appendBuffer { n } { m } ( MkBuffer o1 r1 ) c ( MkBuffer o2 r2 ) =

63 off : Bits64

64 off = bitsFromNat o2

65

66−-- Copy a buffer, potentially allowing the (potentially large) space it

66+||| Copy a buffer, potentially allowing the (potentially large) space it

67−-- pointed to to be freed

67+||| pointed to to be freed

68public

69copy : Buffer n -> Buffer n

70copy { n } = replace ( plusZeroRightNeutral n ) . appendBuffer ( allocate n ) 1

71

72−-- Create a view over a buffer

72+||| Create a view over a buffer

73public

74peekBuffer : { n : Nat } -> { offset : Nat } -> Buffer ( n + offset ) -> ( offset : Nat ) -> Buffer n

75peekBuffer ( MkBuffer o r ) off = MkBuffer ( o + off ) r

@@ -93,7 +93,7 @@ appendBits { n } prim ( MkBuffer o r ) count =

93 MkBuffer o . prim r ( bitsFromNat $ n + o ) ( bitsFromNat count )

94

95

96−-- Read a Bits8 from a Buffer starting at offset

96+||| Read a Bits8 from a Buffer starting at offset

97%assert_total

98public

99peekBits8 : Buffer ( 1 + n ) ->

@@ -101,7 +101,7 @@ peekBits8 : Buffer ( 1 + n ) ->

101 Bits8

102peekBits8 = peekBits { m = 1 } prim__peekB8Native

103

104−-- Append count repetitions of a Bits8 to a Buffer

104+||| Append count repetitions of a Bits8 to a Buffer

105%assert_total

106public

107appendBits8 : Buffer n ->

@@ -110,7 +110,7 @@ appendBits8 : Buffer n ->

110 Buffer ( n + count * 1 )

111appendBits8 = appendBits prim__appendB8Native

112

113−-- Read a Bits16 in native byte order from a Buffer starting at offset

113+||| Read a Bits16 in native byte order from a Buffer starting at offset

114%assert_total

115public

116peekBits16Native : Buffer ( 2 + n ) ->

@@ -118,19 +118,19 @@ peekBits16Native : Buffer ( 2 + n ) ->

118 Bits16

119peekBits16Native = peekBits { m = 2 } prim__peekB16Native

120

121−-- Read a little-endian Bits16 from a Buffer starting at offset

121+||| Read a little-endian Bits16 from a Buffer starting at offset

122%assert_total

123public

124peekBits16LE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16

125peekBits16LE = peekBits { m = 2 } prim__peekB16LE

126

127−-- Read a big-endian Bits16 from a Buffer starting at offset

127+||| Read a big-endian Bits16 from a Buffer starting at offset

128%assert_total

129public

130peekBits16BE : Buffer ( 2 + n ) -> ( offset : Fin ( S n ) ) -> Bits16

131peekBits16BE = peekBits { m = 2 } prim__peekB16BE

132

133−-- Append count repetitions of a Bits16 in native byte order to a Buffer

133+||| Append count repetitions of a Bits16 in native byte order to a Buffer

134%assert_total

135public

136appendBits16Native : Buffer n ->

@@ -139,7 +139,7 @@ appendBits16Native : Buffer n ->

139 Buffer ( n + count * 2 )

140appendBits16Native = appendBits prim__appendB16Native

141

142−-- Append count repetitions of a little-endian Bits16 to a Buffer

142+||| Append count repetitions of a little-endian Bits16 to a Buffer

143%assert_total

144public

145appendBits16LE : Buffer n ->

@@ -148,7 +148,7 @@ appendBits16LE : Buffer n ->

148 Buffer ( n + count * 2 )

149appendBits16LE = appendBits prim__appendB16LE

150

151−-- Append count repetitions of a big-endian Bits16 to a Buffer

151+||| Append count repetitions of a big-endian Bits16 to a Buffer

152%assert_total

153public

154appendBits16BE : Buffer n ->

@@ -157,7 +157,7 @@ appendBits16BE : Buffer n ->

157 Buffer ( n + count * 2 )

158appendBits16BE = appendBits prim__appendB16BE

159

160−-- Read a Bits32 in native byte order from a Buffer starting at offset

160+||| Read a Bits32 in native byte order from a Buffer starting at offset

161%assert_total

162public

163peekBits32Native : Buffer ( 4 + n ) ->

@@ -165,19 +165,19 @@ peekBits32Native : Buffer ( 4 + n ) ->

165 Bits32

166peekBits32Native = peekBits { m = 4 } prim__peekB32Native

167

168−-- Read a little-endian Bits32 from a Buffer starting at offset

168+||| Read a little-endian Bits32 from a Buffer starting at offset

169%assert_total

170public

171peekBits32LE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32

172peekBits32LE = peekBits { m = 4 } prim__peekB32LE

173

174−-- Read a big-endian Bits32 from a Buffer starting at offset

174+||| Read a big-endian Bits32 from a Buffer starting at offset

175%assert_total

176public

177peekBits32BE : Buffer ( 4 + n ) -> ( offset : Fin ( S n ) ) -> Bits32

178peekBits32BE = peekBits { m = 4 } prim__peekB32BE

179

180−-- Append count repetitions of a Bits32 in native byte order to a Buffer

180+||| Append count repetitions of a Bits32 in native byte order to a Buffer

181%assert_total

182public

183appendBits32Native : Buffer n ->

@@ -186,7 +186,7 @@ appendBits32Native : Buffer n ->

186 Buffer ( n + count * 4 )

187appendBits32Native = appendBits prim__appendB32Native

188

189−-- Append count repetitions of a little-endian Bits32 to a Buffer

189+||| Append count repetitions of a little-endian Bits32 to a Buffer

190%assert_total

191public

192appendBits32LE : Buffer n ->

@@ -195,7 +195,7 @@ appendBits32LE : Buffer n ->

195 Buffer ( n + count * 4 )

196appendBits32LE = appendBits prim__appendB32LE

197

198−-- Append count repetitions of a big-endian Bits32 to a Buffer

198+||| Append count repetitions of a big-endian Bits32 to a Buffer

199%assert_total

200public

201appendBits32BE : Buffer n ->

@@ -204,7 +204,7 @@ appendBits32BE : Buffer n ->

204 Buffer ( n + count * 4 )

205appendBits32BE = appendBits prim__appendB32BE

206

207−-- Read a Bits64 in native byte order from a Buffer starting at offset

207+||| Read a Bits64 in native byte order from a Buffer starting at offset

208%assert_total

209public

210peekBits64Native : Buffer ( 8 + n ) ->

@@ -212,19 +212,19 @@ peekBits64Native : Buffer ( 8 + n ) ->

212 Bits64

213peekBits64Native = peekBits { m = 8 } prim__peekB64Native

214

215−-- Read a little-endian Bits64 from a Buffer starting at offset

215+||| Read a little-endian Bits64 from a Buffer starting at offset

216%assert_total

217public

218peekBits64LE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64

219peekBits64LE = peekBits { m = 8 } prim__peekB64LE

220

221−-- Read a big-endian Bits64 from a Buffer starting at offset

221+||| Read a big-endian Bits64 from a Buffer starting at offset

222%assert_total

223public

224peekBits64BE : Buffer ( 8 + n ) -> ( offset : Fin ( S n ) ) -> Bits64

225peekBits64BE = peekBits { m = 8 } prim__peekB64BE

226

227−-- Append count repetitions of a Bits64 in native byte order to a Buffer

227+||| Append count repetitions of a Bits64 in native byte order to a Buffer

228%assert_total

229public

230appendBits64Native : Buffer n ->

@@ -233,7 +233,7 @@ appendBits64Native : Buffer n ->

233 Buffer ( n + count * 8 )

234appendBits64Native = appendBits prim__appendB64Native

235

236−-- Append count repetitions of a little-endian Bits64 to a Buffer

236+||| Append count repetitions of a little-endian Bits64 to a Buffer

237%assert_total

238public

239appendBits64LE : Buffer n ->

@@ -242,7 +242,7 @@ appendBits64LE : Buffer n ->

242 Buffer ( n + count * 8 )

243appendBits64LE = appendBits prim__appendB64LE

244

245−-- Append count repetitions of a big-endian Bits64 to a Buffer

245+||| Append count repetitions of a big-endian Bits64 to a Buffer

246%assert_total

247public

248appendBits64BE : Buffer n ->

libs/base/Data/Fun.idr+2−5

@@ -2,9 +2,7 @@ module Data.Fun

2

3%default total

4

5−--------------------------------------------------------------------------------

6−-- Build an n-ary function type from a Vect of Types and a result type

5+||| Build an n-ary function type from a Vect of Types and a result type

7−--------------------------------------------------------------------------------

8Fun : Vect n Type -> Type -> Type

6Fun : Vect n Type -> Type -> Type

9Fun [] r = r

7Fun [] r = r

10Fun (t::ts) r = t -> Fun ts r

8Fun (t::ts) r = t -> Fun ts r

@@ -14,5 +12,4 @@ chain {ts = []} g r = g r

14chain {ts = (_::_)} g f = \ x => chain g (f x)

12chain {ts = (_::_)} g f = \ x => chain g (f x)

15

13

16target : {ts : Vect n Type} -> Fun ts r -> Type

14target : {ts : Vect n Type} -> Fun ts r -> Type

17−target {r} _ = r

15+target {r} _ = r

18−

libs/base/Data/List.idr+7−6

@@ -7,11 +7,15 @@ using (xs : List a)

7 data Elem : a -> List a -> Type where

8 Here : Elem x (x :: xs)

9 There : Elem x xs -> Elem x (y :: xs)

10−

10+

11 instance Uninhabited (Elem {a} x []) where

12 uninhabited Here impossible

13 uninhabited (There p) impossible

14−

14+

15+ ||| Is the given element a member of the given list.

16+ |||

17+ ||| @x The element to be tested.

18+ ||| @xs The list to be checked against

15 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

19 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

16 isElem x [] = No absurd

20 isElem x [] = No absurd

17 isElem x (y :: xs) with (decEq x y)

21 isElem x (y :: xs) with (decEq x y)

@@ -21,10 +25,7 @@ using (xs : List a)

21 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

25 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

22 where

26 where

23 mkNo : {xs' : List a} ->

27 mkNo : {xs' : List a} ->

24− ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

28+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

25 Elem x' (y' :: xs') -> _|_

29 Elem x' (y' :: xs') -> _|_

26 mkNo f g Here = f refl

30 mkNo f g Here = f refl

27 mkNo f g (There x) = g x

31 mkNo f g (There x) = g x

28−

29−

30−

libs/base/Data/Mod2.idr+1−1

@@ -4,7 +4,7 @@ import Data.Bits

4

5%default total

6

7−-- Integers modulo 2^n

7+||| Integers modulo 2^n

8public

9data Mod2 : Nat -> Type where

10 MkMod2 : {n : Nat} -> Bits n -> Mod2 n

libs/base/Data/Rel.idr+2−3

@@ -2,9 +2,8 @@ module Data.Rel

2

3import Data.Fun

4

5−--------------------------------------------------------------------------------

5+

6−-- Build an n-ary relation type from a Vect of Types

6+||| Build an n-ary relation type from a Vect of Types

7−--------------------------------------------------------------------------------

8Rel : Vect n Type -> Type

7Rel : Vect n Type -> Type

9Rel ts = Fun ts Type

8Rel ts = Fun ts Type

10

9

libs/base/Data/Vect.idr+18

@@ -15,6 +15,24 @@ using (xs : Vect k a)

15 Here : Elem x (x::xs)

16 There : Elem x xs -> Elem x (y::xs)

17

18+||| Nothing can be in an empty Vect

19+noEmptyElem : {x : a} -> Elem x [] -> _|_

20+noEmptyElem Here impossible

21+

22+||| An item not in the head and not in the tail is not in the Vect at all

23+neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

24+neitherHereNorThere xneqy xninxs Here = xneqy refl

25+neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs

26+

27+||| A decision procedure for Elem

28+isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

29+isElem x [] = No noEmptyElem

30+isElem x (y :: xs) with (decEq x y)

31+ isElem x (x :: xs) | (Yes refl) = Yes Here

32+ isElem x (y :: xs) | (No xneqy) with (isElem x xs)

33+ isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)

34+ isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)

35+

18||| A tactic for discovering where, if anywhere, an element is in a vector

36||| A tactic for discovering where, if anywhere, an element is in a vector

19||| @ n how many elements to search before giving up

37||| @ n how many elements to search before giving up

20findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic

38findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic

libs/base/System/Concurrency/Process.idr+7−14

@@ -9,9 +9,8 @@ import System.Concurrency.Raw

9abstract

10data ProcID msg = MkPID Ptr

11

12−-- Type safe message passing programs. Parameterised over the type of

12+||| Type safe message passing programs. Parameterised over the type of

13−-- message which can be send, and the return type.

13+||| message which can be send, and the return type.

14−

15data Process : (msgType : Type) -> Type -> Type where

14data Process : (msgType : Type) -> Type -> Type where

16 lift : IO a -> Process msg a

15 lift : IO a -> Process msg a

17

16

@@ -30,31 +29,26 @@ instance Monad (Process msg) where

30run : Process msg x -> IO x

29run : Process msg x -> IO x

31run (lift prog) = prog

30run (lift prog) = prog

32

31

33−-- Get current process ID

32+||| Get current process ID

34−

35myID : Process msg (ProcID msg)

33myID : Process msg (ProcID msg)

36myID = lift (return (MkPID prim__vm))

34myID = lift (return (MkPID prim__vm))

37

35

38−-- Send a message to another process

36+||| Send a message to another process

39−

40send : ProcID msg -> msg -> Process msg ()

37send : ProcID msg -> msg -> Process msg ()

41send (MkPID p) m = lift (sendToThread p (prim__vm, m))

38send (MkPID p) m = lift (sendToThread p (prim__vm, m))

42

39

43−-- Return whether a message is waiting in the queue

40+||| Return whether a message is waiting in the queue

44−

45msgWaiting : Process msg Bool

41msgWaiting : Process msg Bool

46msgWaiting = lift checkMsgs

42msgWaiting = lift checkMsgs

47

43

48−-- Receive a message - blocks if there is no message waiting

44+||| Receive a message - blocks if there is no message waiting

49−

50recv : Process msg msg

45recv : Process msg msg

51recv {msg} = do (senderid, m) <- lift get

46recv {msg} = do (senderid, m) <- lift get

52 return m

47 return m

53 where get : IO (Ptr, msg)

48 where get : IO (Ptr, msg)

54 get = getMsg

49 get = getMsg

55

50

56−-- receive a message, and return with the sender's process ID.

51+||| receive a message, and return with the sender's process ID.

57−

58recvWithSender : Process msg (ProcID msg, msg)

52recvWithSender : Process msg (ProcID msg, msg)

59recvWithSender {msg}

53recvWithSender {msg}

60 = do (senderid, m) <- lift get

54 = do (senderid, m) <- lift get

@@ -65,4 +59,3 @@ recvWithSender {msg}

65create : Process msg () -> Process msg (ProcID msg)

59create : Process msg () -> Process msg (ProcID msg)

66create (lift p) = do ptr <- lift (fork p)

60create (lift p) = do ptr <- lift (fork p)

67 return (MkPID ptr)

61 return (MkPID ptr)

68−

libs/base/System/Concurrency/Raw.idr+3−6

@@ -6,8 +6,7 @@ module System.Concurrency.Raw

6

7import System

8

9−-- Send a message of any type to the thread with the given thread id

9+||| Send a message of any type to the thread with the given thread id

10−

11sendToThread : (thread_id : Ptr) -> a -> IO ()

10sendToThread : (thread_id : Ptr) -> a -> IO ()

12sendToThread {a} dest val

11sendToThread {a} dest val

13 = mkForeign (FFun "idris_sendMessage"

12 = mkForeign (FFun "idris_sendMessage"

@@ -18,10 +17,8 @@ checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessages"

18 [FPtr] FInt) prim__vm

17 [FPtr] FInt) prim__vm

19 return (intToBool msgs)

18 return (intToBool msgs)

20

19

21−-- Check inbox for messages. If there are none, blocks until a message

20+||| Check inbox for messages. If there are none, blocks until a message

22−-- arrives.

21+||| arrives.

23−

24getMsg : IO a

22getMsg : IO a

25getMsg {a} = mkForeign (FFun "idris_recvMessage"

23getMsg {a} = mkForeign (FFun "idris_recvMessage"

26 [FPtr] (FAny a)) prim__vm

24 [FPtr] (FAny a)) prim__vm

27−

libs/base/System/Info.idrnew file+13

@@ -0,0 +1,13 @@

1+module System.Info

2+

3+||| The Idris backend in use

4+backend : String

5+backend = prim__systemInfo 0

6+

7+||| The operating system in use.

8+os : String

9+os = prim__systemInfo 1

10+

11+||| The triple this program was targeted for

12+targetTriple : String

13+targetTriple = prim__systemInfo 2

libs/base/base.ipkg+1

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

6 Network.Cgi, Network.Socket,

7 Debug.Trace,

8

9+ System.Info,

9 System.Concurrency.Raw, System.Concurrency.Process,

10 System.Concurrency.Raw, System.Concurrency.Process,

10

11

11 Decidable.Decidable, Decidable.Order,

12 Decidable.Decidable, Decidable.Order,

libs/effects/Effect/Exception.idr+1−1

@@ -27,7 +27,7 @@ EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

29raise : a -> { [EXCEPTION a ] } Eff m b

30−raise err = Raise err

30+raise err = call $ Raise err

31

32

33

libs/effects/Effect/File.idr+10−15

@@ -101,33 +101,28 @@ FILE_IO t = MkEff t FileIO

101|||

102||| @ fname The file name to be opened.

103||| @ m The file mode.

104−open : Handler FileIO e =>

105− (fname : String)

104+open : (fname : String)

106 -> (m : Mode)

105 -> (m : Mode)

107 -> { [FILE_IO ()] ==> [FILE_IO (if result

106 -> { [FILE_IO ()] ==> [FILE_IO (if result

108 then OpenFile m

107 then OpenFile m

109 else ())] } Eff e Bool

108 else ())] } Eff e Bool

110−open f m = Open f m

109+open f m = call $ Open f m

111

110

112

111

113||| Close a file.

112||| Close a file.

114−close : Handler FileIO e =>

115− { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

113+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

116−close = Close

114+close = call $ Close

117

115

118||| Read a line from the file.

116||| Read a line from the file.

119−readLine : Handler FileIO e =>

120− { [FILE_IO (OpenFile Read)] } Eff e String

117+readLine : { [FILE_IO (OpenFile Read)] } Eff e String

121−readLine = ReadLine

118+readLine = call $ ReadLine

122

119

123||| Write a line to a file.

120||| Write a line to a file.

124−writeLine : Handler FileIO e =>

125− String -> { [FILE_IO (OpenFile Write)] } Eff e ()

121+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff e ()

126−writeLine str = WriteLine str

122+writeLine str = call $ WriteLine str

127

123

128||| End of file?

124||| End of file?

129−eof : Handler FileIO e =>

130− { [FILE_IO (OpenFile Read)] } Eff e Bool

125+eof : { [FILE_IO (OpenFile Read)] } Eff e Bool

131−eof = EOF

126+eof = call $ EOF

132

127

133-- --------------------------------------------------------------------- [ EOF ]

128-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Memory.idr+7−7

@@ -102,7 +102,7 @@ RAW_MEMORY t = MkEff t RawMemory

102

103allocate : (n : Nat) ->

104 Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

105−allocate size = Allocate size

105+allocate size = call $ Allocate size

106

107initialize : {i : Nat} ->

108 {n : Nat} ->

@@ -111,17 +111,17 @@ initialize : {i : Nat} ->

111 so (i + size <= n) ->

112 Eff m () [RAW_MEMORY (MemoryChunk n i)]

113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

114−initialize c size prf = Initialize c size prf

114+initialize c size prf = call $ Initialize c size prf

115

116free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

117−free = Free

117+free = call Free

118

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

122 so (offset + size <= i) ->

123 { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)

124−peek offset size prf = Peek offset size prf

124+peek offset size prf = call $ Peek offset size prf

125

126poke : {n : Nat} ->

127 {i : Nat} ->

@@ -130,11 +130,11 @@ poke : {n : Nat} ->

130 so (offset <= i && offset + size <= n) ->

131 Eff m () [RAW_MEMORY (MemoryChunk n i)]

132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

133−poke offset content prf = Poke offset content prf

133+poke offset content prf = call $ Poke offset content prf

134

135private

136getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)

137−getRawPtr = GetRawPtr

137+getRawPtr = call $ GetRawPtr

138

139private

140move' : {dst_size : Nat} ->

@@ -149,7 +149,7 @@ move' : {dst_size : Nat} ->

149 Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152− = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

152+ = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds

153

154data MoveDescriptor = Dst | Src

155

libs/effects/Effect/Random.idr+4−4

@@ -9,7 +9,7 @@ data Random : Effect where

9using (m : Type -> Type)

10 instance Handler Random m where

11 handle seed getRandom k

12− = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

12+ = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

13 k seed' seed'

14 handle seed (setSeed n) k = k () n

15

@@ -18,14 +18,14 @@ RND = MkEff Integer Random

18

19||| Generates a random Integer in a given range

20rndInt : Integer -> Integer -> { [RND] } Eff m Integer

21−rndInt lower upper = do v <- getRandom

21+rndInt lower upper = do v <- call $ getRandom

22 return (v `prim__sremBigInt` (upper - lower) + lower)

23

24||| Generate a random number in Fin (S `k`)

25|||

26||| Note that rndFin k takes values 0, 1, ..., k.

27rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

28−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))

28+rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

29 return (toFin v)

30 where toFin : Integer -> Fin (S k)

31 toFin x = case integerToFin x (S k) of

@@ -43,5 +43,5 @@ rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43

44||| Sets the random seed

45srand : Integer -> { [RND] } Eff m ()

46−srand n = setSeed n

46+srand n = call $ setSeed n

47

libs/effects/Effect/Select.idr+1−1

@@ -19,5 +19,5 @@ SELECT : EFFECT

19SELECT = MkEff () Selection

20

21select : List a -> { [SELECT] } Eff m a

22−select xs = Select xs

22+select xs = call $ Select xs

23

libs/effects/Effect/State.idr+3−3

@@ -17,13 +17,13 @@ STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19get : { [STATE x] } Eff m x

20−get = Get

20+get = call $ Get

21

22put : x -> { [STATE x] } Eff m ()

23−put val = Put val

23+put val = call $ Put val

24

25putM : y -> { [STATE x] ==> [STATE y] } Eff m ()

26−putM val = Put val

26+putM val = call $ Put val

27

28update : (x -> x) -> { [STATE x] } Eff m ()

29update f = put (f !get)

libs/effects/Effect/StdIO.idr+9−9

@@ -39,22 +39,22 @@ STDIO : EFFECT

39STDIO = MkEff () StdIO

40

41||| Write a string to standard output.

42−putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

42+putStr : String -> { [STDIO] } Eff e ()

43−putStr s = PutStr s

43+putStr s = call $ PutStr s

44

45||| Write a character to standard output.

46−putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

46+putChar : Char -> { [STDIO] } Eff e ()

47−putChar c = PutCh c

47+putChar c = call $ PutCh c

48

49||| Write a string to standard output, terminating with a newline.

50−putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

50+putStrLn : String -> { [STDIO] } Eff e ()

51putStrLn s = putStr (s ++ "\n")

52

53||| Read a string from standard input.

54−getStr : Handler StdIO e => { [STDIO] } Eff e String

54+getStr : { [STDIO] } Eff e String

55−getStr = GetStr

55+getStr = call $ GetStr

56

57||| Read a character from standard input.

58−getChar : Handler StdIO e => { [STDIO] } Eff e Char

58+getChar : { [STDIO] } Eff e Char

59−getChar = GetCh

59+getChar = call $ GetCh

60

libs/effects/Effect/System.idr+3−3

@@ -28,11 +28,11 @@ SYSTEM : EFFECT

28SYSTEM = MkEff () System

29

30getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

31−getArgs = Args

31+getArgs = call Args

32

33time : Handler System e => { [SYSTEM] } Eff e Int

34−time = Time

34+time = call Time

35

36getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

37−getEnv s = GetEnv s

37+getEnv s = call $ GetEnv s

38

libs/effects/Effects.idr+33−19

@@ -31,9 +31,9 @@ class Handler (e : Effect) (m : Type -> Type) where

31 |||

32 ||| @ r The resource being handled.

33 ||| @ eff The effect to be applied.

34− ||| @ ctxt The context in which to handle the effect.

34+ ||| @ k The continuation to pass the result of the effect

35− handle : (r : res) -> (eff : e t res resk) ->

35+ covering handle : (r : res) -> (eff : e t res resk) ->

36− (ctxt : ((x : t) -> resk x -> m a)) -> m a

36+ (k : ((x : t) -> resk x -> m a)) -> m a

37

38||| Get the resource type (handy at the REPL to find out about an effect)

39resourceType : EFFECT -> Type

@@ -144,11 +144,11 @@ data Eff : (m : Type -> Type)

144 Eff m a xs xs'

145 ebind : Eff m a xs xs' ->

146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

147− effect : (prf : EffElem e a xs) ->

147+ callP : (prf : EffElem e a xs) ->

148 (eff : e t a b) ->

149 Eff m t xs (\v => updateResTy v xs prf eff)

150

151− lift : (prf : SubList ys xs) ->

151+ liftP : (prf : SubList ys xs) ->

152 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

153 newInit : Handler e m =>

154 res ->

@@ -166,6 +166,20 @@ data Eff : (m : Type -> Type)

166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

167(>>=) = ebind

168

169+-- namespace SimpleBind

170+-- (>>=) : Eff m a xs (\v => xs) ->

171+-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'

172+-- (>>=) = ebind

173+

174+||| Run a subprogram which results in an effect state the same as the input.

175+staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)

176+staticEff = id

177+

178+||| Explicitly give the expected set of result effects for an effectful

179+||| operation.

180+toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')

181+toEff xs' = id

182+

169return : a -> Eff m a xs (\v => xs)

183return : a -> Eff m a xs (\v => xs)

170return x = value x

184return x = value x

171

185

@@ -204,8 +218,8 @@ eff env (value x) k = k x env

204eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

218eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

205eff env (prog `ebind` c) k

219eff env (prog `ebind` c) k

206 = eff env prog (\p', env' => eff env' (c p') k)

220 = eff env prog (\p', env' => eff env' (c p') k)

207−eff env (effect prf effP) k = execEff env prf effP k

221+eff env (callP prf effP) k = execEff env prf effP k

208−eff env (lift prf effP) k

222+eff env (liftP prf effP) k

209 = let env' = dropEnv env prf in

223 = let env' = dropEnv env prf in

210 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

224 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

211eff env (newInit r prog) k

225eff env (newInit r prog) k

@@ -233,20 +247,20 @@ syntax MkDefaultEnv = with Env

233 [default, default, default, default, default, default, default],

247 [default, default, default, default, default, default, default],

234 [default, default, default, default, default, default, default, default] |)

248 [default, default, default, default, default, default, default, default] |)

235

249

236−implicit

250+call : {a, b: _} -> {e : Effect} ->

237−lift' : Eff m t ys ys' ->

251+ (eff : e t a b) ->

238− {default tactics { search 100; }

252+ {default tactics { search 100; }

239− prf : SubList ys xs} ->

253+ prf : EffElem e a xs} ->

240− Eff m t xs (\v => updateWith (ys' v) xs prf)

254+ Eff m t xs (\v => updateResTy v xs prf eff)

241−lift' e {prf} = lift prf e

255+call e {prf} = callP prf e

242

256

243implicit

257implicit

244−effect' : {a, b: _} -> {e : Effect} ->

258+lift : Eff m t ys ys' ->

245− (eff : e t a b) ->

246− {default tactics { search 100; }

259+ {default tactics { search 100; }

247− prf : EffElem e a xs} ->

260+ prf : SubList ys xs} ->

248− Eff m t xs (\v => updateResTy v xs prf eff)

261+ Eff m t xs (\v => updateWith (ys' v) xs prf)

249−effect' e {prf} = effect prf e

262+lift e {prf} = liftP prf e

263+

250

264

251new : Handler e m =>

265new : Handler e m =>

252 {default default r : res} ->

266 {default default r : res} ->

libs/prelude/Builtins.idr+4−17

@@ -6,16 +6,8 @@

6||| Dependent pairs, in their internal representation

7||| @ a the type of the witness

8||| @ P the type of the proof

9−data Exists : (a : Type) -> (P : a -> Type) -> Type where

9+data Sigma : (a : Type) -> (P : a -> Type) -> Type where

10− Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a P

10+ Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

11−

12−||| The first projection from a dependent pair

13−getWitness : {P : a -> Type} -> Exists a P -> a

14−getWitness (a ** v) = a

15−

16−||| The second projection from a dependent pair

17−getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)

18−getProof (a ** v) = v

19

11

20||| The eliminator for the empty type.

12||| The eliminator for the empty type.

21FalseElim : _|_ -> a

13FalseElim : _|_ -> a

@@ -38,21 +30,16 @@ sym refl = refl

38trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c

30trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c

39trans refl refl = refl

31trans refl refl = refl

40

32

41−lazy : a -> a

42−lazy x = x -- compiled specially

43−

44−force : a -> a

45−force x = x -- compiled specially

46−

47||| There are two types of laziness: that arising from lazy functions, and that

33||| There are two types of laziness: that arising from lazy functions, and that

48||| arising from codata. They differ in their totality condition.

34||| arising from codata. They differ in their totality condition.

49data LazyType = LazyCodata | LazyEval

35data LazyType = LazyCodata | LazyEval

50

36

51||| The underlying implementation of Lazy and Inf.

37||| The underlying implementation of Lazy and Inf.

38+%error_reverse

52data Lazy' : LazyType -> Type -> Type where

39data Lazy' : LazyType -> Type -> Type where

53 ||| A delayed computation.

40 ||| A delayed computation.

54 |||

41 |||

55− |||Delay is inserted automatically by the elaborator where necessary.

42+ ||| Delay is inserted automatically by the elaborator where necessary.

56 |||

43 |||

57 ||| Note that compiled code gives `Delay` special semantics.

44 ||| Note that compiled code gives `Delay` special semantics.

58 ||| @ t whether this is laziness from codata or normal lazy evaluation

45 ||| @ t whether this is laziness from codata or normal lazy evaluation

libs/prelude/Prelude.idr+3−3

@@ -21,6 +21,7 @@ import Prelude.Traversable

21import Prelude.Bits

22import Prelude.Stream

23import Prelude.Uninhabited

24+import Prelude.Pairs

24

25

25import Decidable.Equality

26import Decidable.Equality

26

27

@@ -549,9 +550,9 @@ fgetc : File -> IO Char

549fgetc (FHandle h) = return (cast !(mkForeign (FFun "fgetc" [FPtr] FInt) h))

550fgetc (FHandle h) = return (cast !(mkForeign (FFun "fgetc" [FPtr] FInt) h))

550

551

551fgetc' : File -> IO (Maybe Char)

552fgetc' : File -> IO (Maybe Char)

552−fgetc' (FHandle h)

553+fgetc' (FHandle h)

553 = do x <- mkForeign (FFun "fgetc" [FPtr] FInt) h

554 = do x <- mkForeign (FFun "fgetc" [FPtr] FInt) h

554− if (x < 0) then return Nothing

555+ if (x < 0) then return Nothing

555 else return (Just (cast x))

556 else return (Just (cast x))

556

557

557fflush : File -> IO ()

558fflush : File -> IO ()

@@ -650,4 +651,3 @@ readFile fn = do h <- openFile fn Read

650 if not x then do l <- fread h

651 if not x then do l <- fread h

651 readFile' h (contents ++ l)

652 readFile' h (contents ++ l)

652 else return contents

653 else return contents

653−

libs/prelude/Prelude/Algebra.idr+170−155

@@ -13,24 +13,26 @@ infixl 6 <*>

13-- A modest class hierarchy

14--------------------------------------------------------------------------------

15

16−-- Sets equipped with a single binary operation that is associative. Must

16+||| Sets equipped with a single binary operation that is associative. Must

17−-- satisfy the following laws:

17+||| satisfy the following laws:

18+|||

18−-- Associativity of <+>:

19+||| + Associativity of `<+>`:

19−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

20+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

20class Semigroup a where

21class Semigroup a where

21 (<+>) : a -> a -> a

22 (<+>) : a -> a -> a

22

23

23class Semigroup a => VerifiedSemigroup a where

24class Semigroup a => VerifiedSemigroup a where

24 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

25 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

25

26

26−-- Sets equipped with a single binary operation that is associative, along with

27+||| Sets equipped with a single binary operation that is associative, along with

27−-- a neutral element for that binary operation. Must satisfy the following

28+||| a neutral element for that binary operation. Must satisfy the following

28−-- laws:

29+||| laws:

30+|||

29−-- Associativity of <+>:

31+||| + Associativity of `<+>`:

30−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

32+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

31−-- Neutral for <+>:

33+||| + Neutral for `<+>`:

32−-- forall a, a <+> neutral == a

34+||| forall a, a <+> neutral == a

33−-- forall a, neutral <+> a == a

35+||| forall a, neutral <+> a == a

34class Semigroup a => Monoid a where

36class Semigroup a => Monoid a where

35 neutral : a

37 neutral : a

36

38

@@ -38,17 +40,17 @@ class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

38 total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

40 total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

39 total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

41 total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

40

42

41−-- Sets equipped with a single binary operation that is associative, along with

43+||| Sets equipped with a single binary operation that is associative, along with

42−-- a neutral element for that binary operation and inverses for all elements.

44+||| a neutral element for that binary operation and inverses for all elements.

43−-- Must satisfy the following laws:

45+||| Must satisfy the following laws:

44−-- Associativity of <+>:

46+||| + Associativity of `<+>`:

45−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

47+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

46−-- Neutral for <+>:

48+||| + Neutral for `<+>`:

47−-- forall a, a <+> neutral == a

49+||| forall a, a <+> neutral == a

48−-- forall a, neutral <+> a == a

50+||| forall a, neutral <+> a == a

49−-- Inverse for <+>:

51+||| + Inverse for `<+>`:

50−-- forall a, a <+> inverse a == neutral

52+||| forall a, a <+> inverse a == neutral

51−-- forall a, inverse a <+> a == neutral

53+||| forall a, inverse a <+> a == neutral

52class Monoid a => Group a where

54class Monoid a => Group a where

53 inverse : a -> a

55 inverse : a -> a

54

56

@@ -59,43 +61,45 @@ class (VerifiedMonoid a, Group a) => VerifiedGroup a where

59(<->) : Group a => a -> a -> a

61(<->) : Group a => a -> a -> a

60(<->) left right = left <+> (inverse right)

62(<->) left right = left <+> (inverse right)

61

63

62−-- Sets equipped with a single binary operation that is associative and

64+||| Sets equipped with a single binary operation that is associative and

63−-- commutative, along with a neutral element for that binary operation and

65+||| commutative, along with a neutral element for that binary operation and

64−-- inverses for all elements. Must satisfy the following laws:

66+||| inverses for all elements. Must satisfy the following laws:

67+|||

65−-- Associativity of <+>:

68+||| + Associativity of `<+>`:

66−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

69+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

67−-- Commutativity of <+>:

70+||| + Commutativity of `<+>`:

68−-- forall a b, a <+> b == b <+> a

71+||| forall a b, a <+> b == b <+> a

69−-- Neutral for <+>:

72+||| + Neutral for `<+>`:

70−-- forall a, a <+> neutral == a

73+||| forall a, a <+> neutral == a

71−-- forall a, neutral <+> a == a

74+||| forall a, neutral <+> a == a

72−-- Inverse for <+>:

75+||| + Inverse for `<+>`:

73−-- forall a, a <+> inverse a == neutral

76+||| forall a, a <+> inverse a == neutral

74−-- forall a, inverse a <+> a == neutral

77+||| forall a, inverse a <+> a == neutral

75class Group a => AbelianGroup a where { }

78class Group a => AbelianGroup a where { }

76

79

77class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

80class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

78 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

81 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

79

82

80−-- Sets equipped with two binary operations, one associative and commutative

83+||| Sets equipped with two binary operations, one associative and commutative

81−-- supplied with a neutral element, and the other associative, with

84+||| supplied with a neutral element, and the other associative, with

82−-- distributivity laws relating the two operations. Must satisfy the following

85+||| distributivity laws relating the two operations. Must satisfy the following

83−-- laws:

86+||| laws:

87+|||

84−-- Associativity of <+>:

88+||| + Associativity of `<+>`:

85−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

89+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

86−-- Commutativity of <+>:

90+||| + Commutativity of `<+>`:

87−-- forall a b, a <+> b == b <+> a

91+||| forall a b, a <+> b == b <+> a

88−-- Neutral for <+>:

92+||| + Neutral for `<+>`:

89−-- forall a, a <+> neutral == a

93+||| forall a, a <+> neutral == a

90−-- forall a, neutral <+> a == a

94+||| forall a, neutral <+> a == a

91−-- Inverse for <+>:

95+||| + Inverse for `<+>`:

92−-- forall a, a <+> inverse a == neutral

96+||| forall a, a <+> inverse a == neutral

93−-- forall a, inverse a <+> a == neutral

97+||| forall a, inverse a <+> a == neutral

94−-- Associativity of <*>:

98+||| + Associativity of `<*>`:

95−-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

99+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

96−-- Distributivity of <*> and <->:

100+||| + Distributivity of `<*>` and `<->`:

97−-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

101+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

98−-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

102+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

99class AbelianGroup a => Ring a where

103class AbelianGroup a => Ring a where

100 (<*>) : a -> a -> a

104 (<*>) : a -> a -> a

101

105

@@ -104,28 +108,29 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

104 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

105 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

109 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

106

110

107−-- Sets equipped with two binary operations, one associative and commutative

111+||| Sets equipped with two binary operations, one associative and commutative

108−-- supplied with a neutral element, and the other associative supplied with a

112+||| supplied with a neutral element, and the other associative supplied with a

109−-- neutral element, with distributivity laws relating the two operations. Must

113+||| neutral element, with distributivity laws relating the two operations. Must

110−-- satisfy the following laws:

114+||| satisfy the following laws:

115+|||

111−-- Associativity of <+>:

116+||| + Associativity of `<+>`:

112−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

117+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

113−-- Commutativity of <+>:

118+||| + Commutativity of `<+>`:

114−-- forall a b, a <+> b == b <+> a

119+||| forall a b, a <+> b == b <+> a

115−-- Neutral for <+>:

120+||| + Neutral for `<+>`:

116−-- forall a, a <+> neutral == a

121+||| forall a, a <+> neutral == a

117−-- forall a, neutral <+> a == a

122+||| forall a, neutral <+> a == a

118−-- Inverse for <+>:

123+||| + Inverse for `<+>`:

119−-- forall a, a <+> inverse a == neutral

124+||| forall a, a <+> inverse a == neutral

120−-- forall a, inverse a <+> a == neutral

125+||| forall a, inverse a <+> a == neutral

121−-- Associativity of <*>:

126+||| + Associativity of `<*>a:

122−-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

127+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

123−-- Neutral for <*>:

128+||| + Neutral for `<*>`:

124−-- forall a, a <*> unity == a

129+||| forall a, a <*> unity == a

125−-- forall a, unity <*> a == a

130+||| forall a, unity <*> a == a

126−-- Distributivity of <*> and <->:

131+||| + Distributivity of `<*>` and `<->`:

127−-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

132+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

128−-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

133+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

129class Ring a => RingWithUnity a where

134class Ring a => RingWithUnity a where

130 unity : a

135 unity : a

131

136

@@ -133,15 +138,17 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

133 total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

138 total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

134 total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

139 total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

135

140

136−-- Sets equipped with a binary operation that is commutative, associative and

141+||| Sets equipped with a binary operation that is commutative, associative and

137−-- idempotent. Must satisfy the following laws:

142+||| idempotent. Must satisfy the following laws:

143+|||

138−-- Associativity of join:

144+||| + Associativity of join:

139−-- forall a b c, join a (join b c) == join (join a b) c

145+||| forall a b c, join a (join b c) == join (join a b) c

140−-- Commutativity of join:

146+||| + Commutativity of join:

141−-- forall a b, join a b == join b a

147+||| forall a b, join a b == join b a

142−-- Idempotency of join:

148+||| + Idempotency of join:

143−-- forall a, join a a == a

149+||| forall a, join a a == a

150+|||

144−-- Join semilattices capture the notion of sets with a "least upper bound".

151+||| Join semilattices capture the notion of sets with a "least upper bound".

145class JoinSemilattice a where

152class JoinSemilattice a where

146 join : a -> a -> a

153 join : a -> a -> a

147

154

@@ -150,15 +157,17 @@ class JoinSemilattice a => VerifiedJoinSemilattice a where

150 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

157 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

151 total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

158 total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

152

159

153−-- Sets equipped with a binary operation that is commutative, associative and

160+||| Sets equipped with a binary operation that is commutative, associative and

154−-- idempotent. Must satisfy the following laws:

161+||| idempotent. Must satisfy the following laws:

162+|||

155−-- Associativity of meet:

163+||| + Associativity of meet:

156−-- forall a b c, meet a (meet b c) == meet (meet a b) c

164+||| forall a b c, meet a (meet b c) == meet (meet a b) c

157−-- Commutativity of meet:

165+||| + Commutativity of meet:

158−-- forall a b, meet a b == meet b a

166+||| forall a b, meet a b == meet b a

159−-- Idempotency of meet:

167+||| + Idempotency of meet:

160−-- forall a, meet a a == a

168+||| forall a, meet a a == a

169+|||

161−-- Meet semilattices capture the notion of sets with a "greatest lower bound".

170+||| Meet semilattices capture the notion of sets with a "greatest lower bound".

162class MeetSemilattice a where

171class MeetSemilattice a where

163 meet : a -> a -> a

172 meet : a -> a -> a

164

173

@@ -167,84 +176,90 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where

167 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

176 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

168 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

169

178

170−-- Sets equipped with a binary operation that is commutative, associative and

179+||| Sets equipped with a binary operation that is commutative, associative and

171−-- idempotent and supplied with a neutral element. Must satisfy the following

180+||| idempotent and supplied with a neutral element. Must satisfy the following

172−-- laws:

181+||| laws:

182+|||

173−-- Associativity of join:

183+||| + Associativity of join:

174−-- forall a b c, join a (join b c) == join (join a b) c

184+||| forall a b c, join a (join b c) == join (join a b) c

175−-- Commutativity of join:

185+||| + Commutativity of join:

176−-- forall a b, join a b == join b a

186+||| forall a b, join a b == join b a

177−-- Idempotency of join:

187+||| + Idempotency of join:

178−-- forall a, join a a == a

188+||| forall a, join a a == a

179−-- Bottom:

189+||| + Bottom:

180−-- forall a, join a bottom == bottom

190+||| forall a, join a bottom == bottom

191+|||

181−-- Join semilattices capture the notion of sets with a "least upper bound"

192+||| Join semilattices capture the notion of sets with a "least upper bound"

182−-- equipped with a "bottom" element.

193+||| equipped with a "bottom" element.

183class JoinSemilattice a => BoundedJoinSemilattice a where

194class JoinSemilattice a => BoundedJoinSemilattice a where

184 bottom : a

195 bottom : a

185

196

186class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

187 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

198 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

188

199

189−-- Sets equipped with a binary operation that is commutative, associative and

200+||| Sets equipped with a binary operation that is commutative, associative and

190−-- idempotent and supplied with a neutral element. Must satisfy the following

201+||| idempotent and supplied with a neutral element. Must satisfy the following

191−-- laws:

202+||| laws:

203+|||

192−-- Associativity of meet:

204+||| + Associativity of meet:

193−-- forall a b c, meet a (meet b c) == meet (meet a b) c

205+||| forall a b c, meet a (meet b c) == meet (meet a b) c

194−-- Commutativity of meet:

206+||| + Commutativity of meet:

195−-- forall a b, meet a b == meet b a

207+||| forall a b, meet a b == meet b a

196−-- Idempotency of meet:

208+||| + Idempotency of meet:

197−-- forall a, meet a a == a

209+||| forall a, meet a a == a

198−-- Top:

210+||| + Top:

199−-- forall a, meet a top == top

211+||| forall a, meet a top == top

212+|||

200−-- Meet semilattices capture the notion of sets with a "greatest lower bound"

213+||| Meet semilattices capture the notion of sets with a "greatest lower bound"

201−-- equipped with a "top" element.

214+||| equipped with a "top" element.

202class MeetSemilattice a => BoundedMeetSemilattice a where

215class MeetSemilattice a => BoundedMeetSemilattice a where

203 top : a

216 top : a

204

217

205class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

206 total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

219 total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

207

220

208−-- Sets equipped with two binary operations that are both commutative,

221+||| Sets equipped with two binary operations that are both commutative,

209−-- associative and idempotent, along with absorbtion laws for relating the two

222+||| associative and idempotent, along with absorbtion laws for relating the two

210−-- binary operations. Must satisfy the following:

223+||| binary operations. Must satisfy the following:

224+|||

211−-- Associativity of meet and join:

225+||| + Associativity of meet and join:

212−-- forall a b c, meet a (meet b c) == meet (meet a b) c

226+||| forall a b c, meet a (meet b c) == meet (meet a b) c

213−-- forall a b c, join a (join b c) == join (join a b) c

227+||| forall a b c, join a (join b c) == join (join a b) c

214−-- Commutativity of meet and join:

228+||| + Commutativity of meet and join:

215−-- forall a b, meet a b == meet b a

229+||| forall a b, meet a b == meet b a

216−-- forall a b, join a b == join b a

230+||| forall a b, join a b == join b a

217−-- Idempotency of meet and join:

231+||| + Idempotency of meet and join:

218−-- forall a, meet a a == a

232+||| forall a, meet a a == a

219−-- forall a, join a a == a

233+||| forall a, join a a == a

220−-- Absorbtion laws for meet and join:

234+||| + Absorbtion laws for meet and join:

221−-- forall a b, meet a (join a b) == a

235+||| forall a b, meet a (join a b) == a

222−-- forall a b, join a (meet a b) == a

236+||| forall a b, join a (meet a b) == a

223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

237class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

224

238

225class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

239class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

226 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

240 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

227 total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

241 total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

228

242

229−-- Sets equipped with two binary operations that are both commutative,

243+||| Sets equipped with two binary operations that are both commutative,

230−-- associative and idempotent and supplied with neutral elements, along with

244+||| associative and idempotent and supplied with neutral elements, along with

231−-- absorbtion laws for relating the two binary operations. Must satisfy the

245+||| absorbtion laws for relating the two binary operations. Must satisfy the

232−-- following:

246+||| following:

247+|||

233−-- Associativity of meet and join:

248+||| + Associativity of meet and join:

234−-- forall a b c, meet a (meet b c) == meet (meet a b) c

249+||| forall a b c, meet a (meet b c) == meet (meet a b) c

235−-- forall a b c, join a (join b c) == join (join a b) c

250+||| forall a b c, join a (join b c) == join (join a b) c

236−-- Commutativity of meet and join:

251+||| + Commutativity of meet and join:

237−-- forall a b, meet a b == meet b a

252+||| forall a b, meet a b == meet b a

238−-- forall a b, join a b == join b a

253+||| forall a b, join a b == join b a

239−-- Idempotency of meet and join:

254+||| + Idempotency of meet and join:

240−-- forall a, meet a a == a

255+||| forall a, meet a a == a

241−-- forall a, join a a == a

256+||| forall a, join a a == a

242−-- Absorbtion laws for meet and join:

257+||| + Absorbtion laws for meet and join:

243−-- forall a b, meet a (join a b) == a

258+||| forall a b, meet a (join a b) == a

244−-- forall a b, join a (meet a b) == a

259+||| forall a b, join a (meet a b) == a

245−-- Neutral for meet and join:

260+||| + Neutral for meet and join:

246−-- forall a, meet a top == top

261+||| forall a, meet a top == top

247−-- forall a, join a bottom == bottom

262+||| forall a, join a bottom == bottom

248class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

263class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

249

264

250class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

265class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

libs/prelude/Prelude/Cast.idr+5−3

@@ -1,7 +1,11 @@

1module Prelude.Cast

2

3+||| Type class for transforming a instance of a data type to another type.

3class Cast from to where

4class Cast from to where

5+ ||| Perform a cast operation.

6+ |||

7+ ||| @orig The original type.

4− cast : from -> to

8+ cast : (orig : from) -> to

5

9

6-- String casts

10-- String casts

7

11

@@ -45,5 +49,3 @@ instance Cast Integer String where

45

49

46instance Cast Char Int where

50instance Cast Char Int where

47 cast = prim__charToInt

51 cast = prim__charToInt

48−

49−

libs/prelude/Prelude/List.idr−7

@@ -195,13 +195,6 @@ list nil cons (x::xs) = (Force cons) x xs

195(++) [] right = right

196(++) (x::xs) right = x :: (xs ++ right)

197

198−||| Create an infinite sequence of some item.

199−|||

200−||| Consider using a `Stream` instead.

201−partial

202−repeat : a -> List a

203−repeat x = x :: lazy (repeat x)

204−

205||| Construct a list with `n` copies of `x`

198||| Construct a list with `n` copies of `x`

206||| @ n how many copies

199||| @ n how many copies

207||| @ x the element to replicate

200||| @ x the element to replicate

libs/prelude/Prelude/Pairs.idrnew file+42

@@ -0,0 +1,42 @@

1+module Prelude.Pairs

2+

3+import Builtins

4+

5+%access public

6+%default total

7+

8+using (a : Type, P : a -> Type)

9+

10+ ||| Dependent pair where the first field is erased.

11+ data Exists : (P : a -> Type) -> Type where

12+ evidence : .(x : a) -> (pf : P x) -> Exists P

13+

14+ ||| Dependent pair where the second field is erased.

15+ data Subset : (a : Type) -> (P : a -> Type) -> Type where

16+ element : (x : a) -> .(pf : P x) -> Subset a P

17+

18+ -- Monomorphic projections

19+

20+ namespace Exists

21+ getWitness : Exists {a} P -> a

22+ getWitness (evidence x pf) = x

23+

24+ getProof : (x : Exists {a} P) -> P (getWitness x)

25+ getProof (evidence x pf) = pf

26+

27+ namespace Subset

28+ getWitness : Subset a P -> a

29+ getWitness (element x pf) = x

30+

31+ getProof : (x : Subset a P) -> P (getWitness x)

32+ getProof (element x pf) = pf

33+

34+ namespace Sigma

35+ getWitness : Sigma a P -> a

36+ getWitness (x ** pf) = x

37+

38+ getProof : (x : Sigma a P) -> P (getWitness x)

39+ getProof (x ** pf) = pf

40+

41+ -- Polymorphic (class-based) projections have been removed

42+ -- because type-directed name disambiguation works better.

libs/prelude/Prelude/Vect.idr+16

@@ -68,6 +68,12 @@ index fZ (x::xs) = x

68index (fS k) (x::xs) = index k xs

69index fZ [] impossible

70

71+||| Insert an element at a particular index

72+insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

73+insertAt fZ y xs = y :: xs

74+insertAt (fS k) y (x::xs) = x :: insertAt k y xs

75+insertAt (fS k) y [] = absurd k

76+

71||| Construct a new vector consisting of all but the indicated element

77||| Construct a new vector consisting of all but the indicated element

72deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

78deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

73deleteAt fZ (x::xs) = xs

79deleteAt fZ (x::xs) = xs

@@ -254,6 +260,10 @@ concat : Vect m (Vect n a) -> Vect (m * n) a

254concat [] = []

260concat [] = []

255concat (v::vs) = v ++ concat vs

261concat (v::vs) = v ++ concat vs

256

262

263+||| Fold without seeding the accumulator

264+foldr1 : (t -> t -> t) -> Vect (S n) t -> t

265+foldr1 f (x::xs) = foldr f x xs

266+

257--------------------------------------------------------------------------------

267--------------------------------------------------------------------------------

258-- Scans

268-- Scans

259--------------------------------------------------------------------------------

269--------------------------------------------------------------------------------

@@ -447,6 +457,12 @@ range : Vect n (Fin n)

447range {n=Z} = []

457range {n=Z} = []

448range {n=S _} = fZ :: map fS range

458range {n=S _} = fZ :: map fS range

449

459

460+||| Transpose a Vect of Vects, turning rows into columns and vice versa.

461+|||

462+||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

463+transpose : Vect m (Vect n a) -> Vect n (Vect m a)

464+transpose [] = replicate _ []

465+transpose (x :: xs) = zipWith (::) x (transpose xs)

450

466

451--------------------------------------------------------------------------------

467--------------------------------------------------------------------------------

452-- Properties

468-- Properties

libs/prelude/prelude.ipkg+1−1

@@ -8,7 +8,7 @@ modules = Builtins, Prelude, IO,

8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

9 Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11− Prelude.Uninhabited,

11+ Prelude.Uninhabited, Prelude.Pairs,

12

13 Decidable.Equality

14

main/Main.hs+4

@@ -63,6 +63,10 @@ runIdris opts = do

63 [] -> return ()

64 fs -> do runIO $ mapM_ documentPkg fs

65 runIO $ exitWith ExitSuccess

66+ case opt getPkgTest opts of

67+ [] -> return ()

68+ fs -> do runIO $ mapM_ testPkg fs

69+ runIO $ exitWith ExitSuccess

66 case opt getPkg opts of

70 case opt getPkg opts of

67 [] -> case opt getPkgREPL opts of

71 [] -> case opt getPkgREPL opts of

68 [] -> idrisMain opts

72 [] -> idrisMain opts

rts/Makefile+2−1

@@ -5,7 +5,8 @@ OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \

5HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \

6 idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h

7CFLAGS:=-fPIC $(CFLAGS)

8−CFLAGS += $(GMP_INCLUDE_DIR) $(GMP)

8+CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\""

9+CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\""

9

10

10ifeq ($(OS), windows)

11ifeq ($(OS), windows)

11 OBJS += windows/idris_stdfgn.o windows/idris_net.o

12 OBJS += windows/idris_stdfgn.o windows/idris_net.o

rts/idris_rts.c+13

@@ -506,6 +506,19 @@ VAL idris_strRev(VM* vm, VAL str) {

506 return cl;

507}

508

509+VAL idris_systemInfo(VM* vm, VAL index) {

510+ int i = GETINT(index);

511+ switch(i) {

512+ case 0: // backend

513+ return MKSTR(vm, "c");

514+ case 1:

515+ return MKSTR(vm, IDRIS_TARGET_OS);

516+ case 2:

517+ return MKSTR(vm, IDRIS_TARGET_TRIPLE);

518+ }

519+ return MKSTR(vm, "");

520+}

521+

509VAL MKBUFFERc(VM* vm, Buffer* buf) {

522VAL MKBUFFERc(VM* vm, Buffer* buf) {

510 Closure* cl = allocate(vm, sizeof(Closure) + sizeof *buf + buf->cap, 1);

523 Closure* cl = allocate(vm, sizeof(Closure) + sizeof *buf + buf->cap, 1);

511 SETTY(cl, BUFFER);

524 SETTY(cl, BUFFER);

rts/idris_rts.h+6

@@ -279,6 +279,12 @@ VAL idris_peekB64Native(VM* vm, VAL buf, VAL off);

279VAL idris_peekB64LE(VM* vm, VAL buf, VAL off);

280VAL idris_peekB64BE(VM* vm, VAL buf, VAL off);

281

282+// system infox

283+// used indices:

284+// 0 returns backend

285+// 1 returns OS

286+VAL idris_systemInfo(VM* vm, VAL index);

287+

282// Command line args

288// Command line args

283

289

284extern int __idris_argc;

290extern int __idris_argc;

src/IRTS/CodegenC.hs+2

@@ -493,6 +493,8 @@ doOp v (LChInt ITNative) args = v ++ creg (last args)

493doOp v (LChInt ITChar) args = doOp v (LChInt ITNative) args

494doOp v (LIntCh ITNative) args = v ++ creg (last args)

495doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

496+

497+doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

496doOp v LNoOp args = v ++ creg (last args)

498doOp v LNoOp args = v ++ creg (last args)

497doOp _ op _ = "FAIL /* " ++ show op ++ " */"

499doOp _ op _ = "FAIL /* " ++ show op ++ " */"

498

500

src/IRTS/CodegenJavaScript.hs+2

@@ -2508,6 +2508,8 @@ translateExpression (SOp op vars)

2508 JSNum (JSInt 1),

2509 JSBinOp "-" (JSProj (JSIdent v) "length") (JSNum (JSInt 1))

2510 ]

2511+ | LSystemInfo <- op

2512+ , (arg:_) <- vars = jsCall "__IDRRT__systemInfo" [JSVar arg]

2511 | LNullPtr <- op

2513 | LNullPtr <- op

2512 , (_) <- vars = JSNull

2514 , (_) <- vars = JSNull

2513

2515

src/IRTS/Lang.hs+2

@@ -55,6 +55,8 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

55 -- Buffers

56 | LAllocate

57 | LAppendBuffer

58+ -- system info

59+ | LSystemInfo

58 -- Note that for Bits8 only Native endianness is actually used

60 -- Note that for Bits8 only Native endianness is actually used

59 -- and the user-exposed interface for Bits8 doesn't mention

61 -- and the user-exposed interface for Bits8 doesn't mention

60 -- endianness

62 -- endianness

src/IRTS/Simplified.hs+16−14

@@ -125,15 +125,17 @@ checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)

125 return xs'

126checkDefs ctxt ((n, DFun n' args exp) : xs)

127 = do let sexp = evalState (simplify True exp) (ctxt, 0)

128− (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

128+ (exp', locs) <- runStateT (scopecheck n ctxt (zip args [0..]) sexp) (length args)

129 xs' <- checkDefs ctxt xs

130 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')

131

132lvar v = do i <- get

133 put (max i v)

134

135−scopecheck :: DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp

135+scopecheck :: Name -> DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp

136−scopecheck ctxt envTop tm = sc envTop tm where

136+scopecheck fn ctxt envTop tm = sc envTop tm where

137+ failsc err = fail $ "Codegen error in " ++ show fn ++ ":" ++ err

138+

137 sc env (SV (Glob n)) =

139 sc env (SV (Glob n)) =

138 case lookup n (reverse env) of -- most recent first

140 case lookup n (reverse env) of -- most recent first

139 Just i -> do lvar i; return (SV (Loc i))

141 Just i -> do lvar i; return (SV (Loc i))

@@ -141,20 +143,20 @@ scopecheck ctxt envTop tm = sc envTop tm where

141 Just (DConstructor _ i ar) ->

143 Just (DConstructor _ i ar) ->

142 if True -- ar == 0

144 if True -- ar == 0

143 then return (SCon i n [])

145 then return (SCon i n [])

144− else fail $ "Codegen error: Constructor " ++ show n ++

146+ else failsc $ "Constructor " ++ show n ++

145 " has arity " ++ show ar

147 " has arity " ++ show ar

146 Just _ -> return (SV (Glob n))

148 Just _ -> return (SV (Glob n))

147− Nothing -> fail $ "Codegen error: No such variable " ++ show n

149+ Nothing -> failsc $ "No such variable " ++ show n

148 sc env (SApp tc f args)

150 sc env (SApp tc f args)

149 = do args' <- mapM (scVar env) args

151 = do args' <- mapM (scVar env) args

150 case lookupCtxtExact f ctxt of

152 case lookupCtxtExact f ctxt of

151 Just (DConstructor n tag ar) ->

153 Just (DConstructor n tag ar) ->

152 if True -- (ar == length args)

154 if True -- (ar == length args)

153 then return $ SCon tag n args'

155 then return $ SCon tag n args'

154− else fail $ "Codegen error: Constructor " ++ show f ++

156+ else failsc $ "Constructor " ++ show f ++

155 " has arity " ++ show ar

157 " has arity " ++ show ar

156 Just _ -> return $ SApp tc f args'

158 Just _ -> return $ SApp tc f args'

157− Nothing -> fail $ "Codegen error: No such variable " ++ show f

159+ Nothing -> failsc $ "No such variable " ++ show f

158 sc env (SForeign l ty f args)

160 sc env (SForeign l ty f args)

159 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

161 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

160 return (t, a')) args

162 return (t, a')) args

@@ -165,9 +167,9 @@ scopecheck ctxt envTop tm = sc envTop tm where

165 Just (DConstructor n tag ar) ->

167 Just (DConstructor n tag ar) ->

166 if True -- (ar == length args)

168 if True -- (ar == length args)

167 then return $ SCon tag n args'

169 then return $ SCon tag n args'

168− else fail $ "Codegen error: Constructor " ++ show f ++

170+ else failsc $ "Constructor " ++ show f ++

169− " has arity " ++ show ar

171+ " has arity " ++ show ar

170− _ -> fail $ "Codegen error: No such constructor " ++ show f

172+ _ -> failsc $ "No such constructor " ++ show f

171 sc env (SProj e i)

173 sc env (SProj e i)

172 = do e' <- scVar env e

174 = do e' <- scVar env e

173 return (SProj e' i)

175 return (SProj e' i)

@@ -200,9 +202,9 @@ scopecheck ctxt envTop tm = sc envTop tm where

200 Just i -> do lvar i; return (Loc i)

202 Just i -> do lvar i; return (Loc i)

201 Nothing -> case lookupCtxtExact n ctxt of

203 Nothing -> case lookupCtxtExact n ctxt of

202 Just (DConstructor _ i ar) ->

204 Just (DConstructor _ i ar) ->

203− fail $ "Codegen error : can't pass constructor here"

205+ failsc $ "can't pass constructor here"

204 Just _ -> return (Glob n)

206 Just _ -> return (Glob n)

205− Nothing -> fail $ "Codegen error: No such variable " ++ show n ++

207+ Nothing -> failsc $ "No such variable " ++ show n ++

206 " in " ++ show tm ++ " " ++ show envTop

208 " in " ++ show tm ++ " " ++ show envTop

207 scVar _ x = return x

209 scVar _ x = return x

208

210

@@ -212,9 +214,9 @@ scopecheck ctxt envTop tm = sc envTop tm where

212 Just (DConstructor _ i ar) ->

214 Just (DConstructor _ i ar) ->

213 if True -- (length args == ar)

215 if True -- (length args == ar)

214 then return i

216 then return i

215− else fail $ "Codegen error: Constructor " ++ show n ++

217+ else failsc $ "Constructor " ++ show n ++

216 " has arity " ++ show ar

218 " has arity " ++ show ar

217− _ -> fail $ "Codegen error: No constructor " ++ show n

219+ _ -> failsc $ "No constructor " ++ show n

218 e' <- sc env' e

220 e' <- sc env' e

219 return (SConCase (length env) tag n args e')

221 return (SConCase (length env) tag n args e')

220 scalt env (SConstCase c e) = do e' <- sc env e

222 scalt env (SConstCase c e) = do e' <- sc env e

src/Idris/AbsSyntax.hs+5−3

@@ -1329,9 +1329,11 @@ addImpl' inpat env infns ist ptm

1329 as' = map (fmap (ai env ds)) as in

1330 mkPApp fc 1 f' as'

1331 ai env ds (PCase fc c os)

1332− = let c' = ai env ds c

1332+ = let c' = ai env ds c in

1333− os' = map (pmap (ai env ds)) os in

1333+ -- leave os alone, because they get lifted into a new pattern match

1334+ -- definition which is passed through addImpl again with more scope

1335+ -- information

1334− PCase fc c' os'

1336+ PCase fc c' os

1335 ai env ds (PLam n ty sc)

1337 ai env ds (PLam n ty sc)

1336 = let ty' = ai env ds ty

1338 = let ty' = ai env ds ty

1337 sc' = ai ((n, Just ty):env) ds sc in

1339 sc' = ai ((n, Just ty):env) ds sc in

src/Idris/AbsSyntaxTree.hs+17−9

@@ -339,7 +339,7 @@ data Command = Quit

339 | WhoCalls Name

340 | CallsWho Name

341 | MakeDoc String -- IdrisDoc

342−

342+ | Warranty

343

344data Opt = Filename String

345 | Quiet

@@ -373,6 +373,7 @@ data Opt = Filename String

373 | PkgCheck String

374 | PkgREPL String

375 | PkgMkDoc String -- IdrisDoc

376+ | PkgTest String

376 | WarnOnly

377 | WarnOnly

377 | Pkg String

378 | Pkg String

378 | BCAsm String

379 | BCAsm String

@@ -884,7 +885,8 @@ deriving instance NFData OptInfo

884data TypeInfo = TI { con_names :: [Name],

885data TypeInfo = TI { con_names :: [Name],

885 codata :: Bool,

886 codata :: Bool,

886 data_opts :: DataOpts,

887 data_opts :: DataOpts,

887− param_pos :: [Int] }

888+ param_pos :: [Int],

889+ mutual_types :: [Name] }

888 deriving Show

890 deriving Show

889{-!

891{-!

890deriving instance Binary TypeInfo

892deriving instance Binary TypeInfo

@@ -963,6 +965,7 @@ data SyntaxInfo = Syn { using :: [Using],

963 inPattern :: Bool,

965 inPattern :: Bool,

964 implicitAllowed :: Bool,

966 implicitAllowed :: Bool,

965 maxline :: Maybe Int,

967 maxline :: Maybe Int,

968+ mut_nesting :: Int,

966 dsl_info :: DSL }

969 dsl_info :: DSL }

967 deriving Show

970 deriving Show

968{-!

971{-!

@@ -970,7 +973,7 @@ deriving instance NFData SyntaxInfo

970deriving instance Binary SyntaxInfo

973deriving instance Binary SyntaxInfo

971!-}

974!-}

972

975

973−defaultSyntax = Syn [] [] [] [] id False False Nothing initDSL

976+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL

974

977

975expandNS :: SyntaxInfo -> Name -> Name

978expandNS :: SyntaxInfo -> Name -> Name

976expandNS syn n@(NS _ _) = n

979expandNS syn n@(NS _ _) = n

@@ -1098,8 +1101,8 @@ elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defau

1098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1101 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1099

1102

1100-- Defined in builtins.idr

1103-- Defined in builtins.idr

1101−sigmaTy = sUN "Exists"

1104+sigmaTy = sUN "Sigma"

1102−existsCon = sUN "Ex_intro"

1105+existsCon = sUN "Sg_intro"

1103

1106

1104piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1107piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1105piBind = piBindp expl

1108piBind = piBindp expl

@@ -1157,7 +1160,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1157 colour ItalicText = IdrisColour Nothing True False False True

1160 colour ItalicText = IdrisColour Nothing True False False True

1158

1161

1159-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1162-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1160−prettyImp :: PPOption -- ^^ pretty printing options

1163+prettyImp :: PPOption -- ^^ pretty printing options

1161 -> PTerm -- ^^ the term to pretty-print

1164 -> PTerm -- ^^ the term to pretty-print

1162 -> Doc OutputAnnotation

1165 -> Doc OutputAnnotation

1163prettyImp impl = pprintPTerm impl [] [] []

1166prettyImp impl = pprintPTerm impl [] [] []

@@ -1167,7 +1170,7 @@ prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1167prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1170prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1168

1171

1169-- | Pretty-print a high-level Idris term in some bindings context with infix info

1172-- | Pretty-print a high-level Idris term in some bindings context with infix info

1170−pprintPTerm :: PPOption -- ^^ pretty printing options

1173+pprintPTerm :: PPOption -- ^^ pretty printing options

1171 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1174 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1172 -> [Name] -- ^^ names to always show in pi, even if not used

1175 -> [Name] -- ^^ names to always show in pi, even if not used

1173 -> [FixDecl] -- ^^ Fixity declarations

1176 -> [FixDecl] -- ^^ Fixity declarations

@@ -1338,6 +1341,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1338 prettySe p bnd PImpossible = kwd "impossible"

1341 prettySe p bnd PImpossible = kwd "impossible"

1339 prettySe p bnd Placeholder = text "_"

1342 prettySe p bnd Placeholder = text "_"

1340 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1343 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1344+ prettySe p bnd (PCoerced t) = prettySe p bnd t

1341 prettySe p bnd (PElabError s) = pretty s

1345 prettySe p bnd (PElabError s) = pretty s

1342

1346

1343 prettySe p bnd _ = text "test"

1347 prettySe p bnd _ = text "test"

@@ -1418,6 +1422,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1418 getFixity :: String -> Maybe Fixity

1422 getFixity :: String -> Maybe Fixity

1419 getFixity = flip M.lookup fixities

1423 getFixity = flip M.lookup fixities

1420

1424

1425+prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1426+prettyDocumentedIst ist (name, ty, docs) =

1427+ prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1428+ fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1429+

1421-- | Pretty-printer helper for the binding site of a name

1430-- | Pretty-printer helper for the binding site of a name

1422bindingOf :: Name -- ^^ the bound name

1431bindingOf :: Name -- ^^ the bound name

1423 -> Bool -- ^^ whether the name is implicit

1432 -> Bool -- ^^ whether the name is implicit

@@ -1435,7 +1444,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

1435 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1444 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1436 | otherwise = strName n

1445 | otherwise = strName n

1437 strName n | n == falseTy = "_|_"

1446 strName n | n == falseTy = "_|_"

1438− strName (MN i s) = T.unpack s

1447+ strName (MN i s) = T.unpack s

1439 strName other = show other

1448 strName other = show other

1440

1449

1441

1450

@@ -1694,4 +1703,3 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1694

1703

1695 niTacImp env (TacImp _ _ scr) = ni env scr

1704 niTacImp env (TacImp _ _ scr) = ni env scr

1696 niTacImp _ _ = []

1705 niTacImp _ _ = []

1697−

src/Idris/CaseSplit.hs+3−1

@@ -280,6 +280,8 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

280 nshow t = show t

281

282 -- if there's any {n} replace with {n=n}

283+ -- but don't replace it in comments

284+ expandBraces ('{' : '-' : xs) = '{' : '-' : xs

283 expandBraces ('{' : xs)

285 expandBraces ('{' : xs)

284 = let (brace, (_:rest)) = span (/= '}') xs in

286 = let (brace, (_:rest)) = span (/= '}') xs in

285 if (not ('=' `elem` brace))

287 if (not ('=' `elem` brace))

@@ -298,7 +300,7 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

298 if (before == n && not (isAlphaNum next))

300 if (before == n && not (isAlphaNum next))

299 then addBrackets tm ++ updatePat False n tm after

301 then addBrackets tm ++ updatePat False n tm after

300 else c : updatePat (not (isAlphaNum c)) n tm rest

302 else c : updatePat (not (isAlphaNum c)) n tm rest

301− updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

303+ updatePat start n tm (c:rest) = c : updatePat (not ((isAlphaNum c) || c == '_')) n tm rest

302

304

303 addBrackets tm | ' ' `elem` tm

305 addBrackets tm | ' ' `elem` tm

304 , not (isPrefixOf "(" tm)

306 , not (isPrefixOf "(" tm)

src/Idris/CmdOptions.hs+43−2

@@ -10,10 +10,50 @@ import Options.Applicative

10import Options.Applicative.Arrows

11import Data.Maybe

12

13+import qualified Text.PrettyPrint.ANSI.Leijen as PP

14+

13runArgParser :: IO [Opt]

15runArgParser :: IO [Opt]

14−runArgParser = do opts <- execParser $ info parser $

16+runArgParser = do opts <- execParser $ info parser

15− header ("Idris version " ++ ver ++ ", (C) The Idris Community 2014")

17+ (fullDesc

18+ <> headerDoc (Just idrisHeader)

19+ <> progDescDoc (Just idrisProgDesc)

20+ <> footerDoc (Just idrisFooter)

21+ )

16 return $ preProcOpts opts []

22 return $ preProcOpts opts []

23+ where

24+ idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2014"]

25+ idrisProgDesc = PP.vsep [PP.text "Idris is a general purpose pure functional programming language with dependent",

26+ PP.text "types. Dependent types allow types to be predicated on values, meaning that",

27+ PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",

28+ PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",

29+ PP.text "and ML.",

30+ PP.empty,

31+ PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [

32+ "+ Full dependent types with dependent pattern matching",

33+ "+ where clauses, with rule, simple case expressions",

34+ "+ pattern matching let and lambda bindings",

35+ "+ Type classes, monad comprehensions",

36+ "+ do notation, idiom brackets",

37+ "+ syntactic conveniences for lists, tuples, dependent pairs",

38+ "+ Totality checking",

39+ "+ Coinductive types",

40+ "+ Indentation significant syntax, extensible syntax",

41+ "+ Tactic based theorem proving (influenced by Coq)",

42+ "+ Cumulative universes",

43+ "+ Simple foreign function interface (to C)",

44+ "+ Hugs style interactive environment"

45+ ],

46+ PP.empty]

47+ idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",

48+ PP.text "and project. Thus the tooling provided and resulting programs created",

49+ PP.text "should not necessarily be seen as production ready nor for industrial use.",

50+ PP.empty,

51+ PP.text "More details over Idris can be found online here:",

52+ PP.empty,

53+ PP.indent 4 (PP.text "http://www.idris-lang.org/")]

54+

55+

56+

17

57

18pureArgParser :: [String] -> [Opt]

58pureArgParser :: [String] -> [Opt]

19pureArgParser args = case execParserMaybe (info parser idm) args of

59pureArgParser args = case execParserMaybe (info parser idm) args of

@@ -61,6 +101,7 @@ parseFlags = many $

61 <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

101 <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

62 <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

102 <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

63 <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

103 <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

104+ <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))

64 -- Misc options

105 -- Misc options

65 <|> (BCAsm <$> strOption (long "bytecode"))

106 <|> (BCAsm <$> strOption (long "bytecode"))

66 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

107 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

src/Idris/Core/Elaborate.hs+6−3

@@ -681,11 +681,13 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

681try' t1 t2 proofSearch

682 = do s <- get

683 ps <- get_probs

684+ ulog <- getUnifyLog

684 case prunStateT 999999 False ps t1 s of

685 case prunStateT 999999 False ps t1 s of

685 OK ((v, _, _), s') -> do put s'

686 OK ((v, _, _), s') -> do put s'

686 return $! v

687 return $! v

688+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

687− Error e1 -> if recoverableErr e1 then

689+ if recoverableErr e1 then

688− do case runStateT t2 s of

690+ do case runStateT t2 s of

689 OK (v, s') -> do put s'; return $! v

691 OK (v, s') -> do put s'; return $! v

690 Error e2 -> if score e1 >= score e2

692 Error e2 -> if score e1 >= score e2

691 then lift (tfail e1)

693 then lift (tfail e1)

@@ -695,6 +697,7 @@ try' t1 t2 proofSearch

695 = -- traceWhen r (show err) $

697 = -- traceWhen r (show err) $

696 r || proofSearch

698 r || proofSearch

697 recoverableErr (CantSolveGoal _ _) = False

699 recoverableErr (CantSolveGoal _ _) = False

700+ recoverableErr (ProofSearchFail (Msg _)) = True

698 recoverableErr (ProofSearchFail _) = False

701 recoverableErr (ProofSearchFail _) = False

699 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

702 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700 recoverableErr (At _ e) = recoverableErr e

703 recoverableErr (At _ e) = recoverableErr e

@@ -724,7 +727,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

724 = do s <- get

727 = do s <- get

725 ps <- get_probs

728 ps <- get_probs

726 case prunStateT pmax True ps x s of

729 case prunStateT pmax True ps x s of

727− OK ((v, newps, probs), s') ->

730+ OK ((v, newps, probs), s') ->

728 do let cs' = if (newps < pmax)

731 do let cs' = if (newps < pmax)

729 then [do put s'; return $! v]

732 then [do put s'; return $! v]

730 else (do put s'; return $! v) : cs

733 else (do put s'; return $! v) : cs

src/Idris/Core/Evaluate.hs+9−4

@@ -537,7 +537,7 @@ wknV i t = return t

537convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

538

539convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

540−convEq ctxt holes = ceq [] where

540+convEq ctxt holes topx topy = ceq [] topx topy where

541 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

542 ceq ps (P xt x _) (P yt y _)

543 | x `elem` holes || y `elem` holes = return True

@@ -550,8 +550,12 @@ convEq ctxt holes = ceq [] where

550 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

551 | n == n' = ceq ps x y

552 ceq ps (V x) (V y) = return (x == y)

553− ceq ps (V x) (P _ y _) = return (fst (ps!!x) == y)

553+ ceq ps (V x) (P _ y _)

554+ | x >= 0 && length ps > x = return (fst (ps!!x) == y)

555+ | otherwise = return False

554− ceq ps (P _ x _) (V y) = return (x == snd (ps!!y))

556+ ceq ps (P _ x _) (V y)

557+ | y >= 0 && length ps > y = return (x == snd (ps!!y))

558+ | otherwise = return False

555 ceq ps (Bind n xb xs) (Bind n' yb ys)

559 ceq ps (Bind n xb xs) (Bind n' yb ys)

556 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)

560 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)

557 where

561 where

@@ -678,7 +682,7 @@ data Totality = Total [Int] -- ^ well-founded arguments

678

682

679-- | Reasons why a function may not be total

683-- | Reasons why a function may not be total

680data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

684data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

681− | BelieveMe | Mutual [Name] | NotProductive

685+ | ExternalIO | BelieveMe | Mutual [Name] | NotProductive

682 deriving (Show, Eq)

686 deriving (Show, Eq)

683

687

684instance Show Totality where

688instance Show Totality where

@@ -688,6 +692,7 @@ instance Show Totality where

688 show (Partial Itself) = "possibly not total as it is not well founded"

692 show (Partial Itself) = "possibly not total as it is not well founded"

689 show (Partial NotCovering) = "not total as there are missing cases"

693 show (Partial NotCovering) = "not total as there are missing cases"

690 show (Partial NotPositive) = "not strictly positive"

694 show (Partial NotPositive) = "not strictly positive"

695+ show (Partial ExternalIO) = "an external IO primitive"

691 show (Partial NotProductive) = "not productive"

696 show (Partial NotProductive) = "not productive"

692 show (Partial BelieveMe) = "not total due to use of believe_me in proof"

697 show (Partial BelieveMe) = "not total due to use of believe_me in proof"

693 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

698 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

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

@@ -180,6 +180,19 @@ match_unify' ctxt env topx topy =

180-- -- ++ show (pterm ps)

181-- ++ "\n----------") $

182

183+mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]

184+mergeSolutions env ns = merge [] ns

185+ where

186+ merge acc [] = return (reverse acc)

187+ merge acc ((n, t) : ns)

188+ | Just t' <- lookup n ns

189+ = do ps <- get

190+ let probs = problems ps

191+ put (ps { problems = probs ++ [(t,t',env,Msg "New problem",

192+ [], Unify)] })

193+ merge acc ns

194+ | otherwise = merge ((n, t): acc) ns

195+

183unify' :: Context -> Env -> TT Name -> TT Name ->

196unify' :: Context -> Env -> TT Name -> TT Name ->

184 StateT TState TC [(Name, TT Name)]

197 StateT TState TC [(Name, TT Name)]

185unify' ctxt env topx topy =

198unify' ctxt env topx topy =

@@ -206,17 +219,22 @@ unify' ctxt env topx topy =

206 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

219 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

207-- ++ show (pterm ps)

220-- ++ show (pterm ps)

208 ++ "\n----------") $

221 ++ "\n----------") $

209− do ps <- get

210− let (h, ns) = unified ps

222+ do let (h, ns) = unified ps

223+ -- if a metavar has multiple solutions, make a new unification

224+ -- problem for each.

225+ uns <- mergeSolutions env (u ++ ns)

226+ ps <- get

211− let (ns', probs') = updateProblems (context ps) (u ++ ns)

227+ let (ns', probs') = updateProblems (context ps) uns

212 (fails ++ problems ps)

228 (fails ++ problems ps)

213 (injective ps)

229 (injective ps)

214 (holes ps)

230 (holes ps)

215 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

231 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

232+ traceWhen (unifylog ps)

233+ ("Now solved: " ++ show ns') $

216− put (ps { problems = probs' ++ probs_notu,

234+ put (ps { problems = probs' ++ probs_notu,

217− unified = (h, ns'),

235+ unified = (h, ns'),

218− injective = updateInj u (injective ps),

236+ injective = updateInj u (injective ps),

219− notunified = notu' })

237+ notunified = notu' })

220 return u

238 return u

221 where updateInj ((n, a) : us) inj

239 where updateInj ((n, a) : us) inj

222 | (P _ n' _, _) <- unApply a,

240 | (P _ n' _, _) <- unApply a,

@@ -789,8 +807,9 @@ updateSolved' [] x = x

789updateSolved' xs (Bind n (Hole ty) t)

807updateSolved' xs (Bind n (Hole ty) t)

790 | Just v <- lookup n xs

808 | Just v <- lookup n xs

791 = case xs of

809 = case xs of

792− [_] -> psubst n v t

810+ [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume

811+ -- explicit names

793− _ -> psubst n v (updateSolved' xs t)

812+ _ -> substV v $ psubst n v (updateSolved' xs t)

794updateSolved' xs (Bind n b t)

813updateSolved' xs (Bind n b t)

795 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

814 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

796updateSolved' xs (App f a)

815updateSolved' xs (App f a)

@@ -838,7 +857,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where

838 y' = updateSolved ns y

857 y' = updateSolved ns y

839 err' = updateError ns err

858 err' = updateError ns err

840 env' = updateEnv ns env in

859 env' = updateEnv ns env in

841−-- trace ("Updating " ++ show (x',y')) $

860+-- trace ("Updating " ++ show (x',y')) $

842 case unify ctxt env' x' y' inj holes while of

861 case unify ctxt env' x' y' inj holes while of

843 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

862 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

844 up (ns ++ v) ps

863 up (ns ++ v) ps

src/Idris/Core/TT.hs+9−4

@@ -184,9 +184,12 @@ score :: Err -> Int

184score (CantUnify _ _ _ m _ s) = s + score m

185score (CantResolve _) = 20

186score (NoSuchVariable _) = 1000

187−score (ProofSearchFail _) = 10000

187+score (ProofSearchFail e) = score e

188−score (CantSolveGoal _ _) = 10000

188+score (CantSolveGoal _ _) = 100000

189score (InternalMsg _) = -1

190+score (At _ e) = score e

191+score (ElaboratingArg _ _ _ e) = score e

192+score (Elaborating _ _ e) = score e

190score _ = 0

193score _ = 0

191

194

192instance Show Err where

195instance Show Err where

@@ -203,6 +206,7 @@ instance Show Err where

203 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

206 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

204 show x ++ ": " ++ show e

207 show x ++ ": " ++ show e

205 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

208 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

209+ show (ProofSearchFail e) = "Proof search fail: " ++ show e

206 show _ = "Error"

210 show _ = "Error"

207

211

208instance Pretty Err OutputAnnotation where

212instance Pretty Err OutputAnnotation where

@@ -1056,8 +1060,9 @@ uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

1056

1060

1057uniqueBinders :: [Name] -> TT Name -> TT Name

1061uniqueBinders :: [Name] -> TT Name -> TT Name

1058uniqueBinders ns (Bind n b sc)

1062uniqueBinders ns (Bind n b sc)

1059− = let n' = uniqueName n ns in

1063+ = let n' = uniqueName n ns

1064+ ns' = n' : ns in

1060− Bind n' (fmap (uniqueBinders (n':ns)) b) (uniqueBinders ns sc)

1065+ Bind n' (fmap (uniqueBinders ns') b) (uniqueBinders ns' sc)

1061uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)

1066uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)

1062uniqueBinders ns t = t

1067uniqueBinders ns t = t

1063

1068

src/Idris/Core/Unify.hs+35−9

@@ -69,7 +69,20 @@ match_unify ctxt env topx topy inj holes from =

69 return (map (renameBinders env) (trimSolutions v))

70 _ -> tfail e

71 where

72−

72+ -- This rule is highly dubious... it certainly produces a valid answer

73+ -- but it scares me. However, matching is never guaranteed to give a unique

74+ -- answer, merely a valid one, so perhaps we're okay.

75+ -- In other words: it may vanish without warning some day :)

76+ un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)

77+ | (P (DCon _ _) _ _, _) <- unApply x,

78+ holeIn env f || f `elem` holes

79+ = let n' = uniqueName (sMN 0 "mv") (map fst env) in

80+ checkCycle names (f, Bind n' (Lam t) x)

81+ un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x

82+ | (P (DCon _ _) _ _, _) <- unApply x,

83+ holeIn env f || f `elem` holes

84+ = let n' = uniqueName fn (map fst env) in

85+ checkCycle names (f, Bind n' (Lam t) x)

73

86

74 un names (P _ x _) tm

87 un names (P _ x _) tm

75 | holeIn env x || x `elem` holes

88 | holeIn env x || x `elem` holes

@@ -85,7 +98,7 @@ match_unify ctxt env topx topy inj holes from =

85 | length bnames > i,

98 | length bnames > i,

86 fst (fst (bnames!!i)) == x ||

99 fst (fst (bnames!!i)) == x ||

87 snd (fst (bnames!!i)) == x = do sc 1; return []

100 snd (fst (bnames!!i)) == x = do sc 1; return []

88− un bnames (Bind x bx sx) (Bind y by sy)

101+ un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by

89 = do h1 <- uB bnames bx by

102 = do h1 <- uB bnames bx by

90 h2 <- un (((x, y), binderTy bx) : bnames) sx sy

103 h2 <- un (((x, y), binderTy bx) : bnames) sx sy

91 combine bnames h1 h2

104 combine bnames h1 h2

@@ -119,6 +132,9 @@ match_unify ctxt env topx topy inj holes from =

119 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

132 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

120 return []

133 return []

121

134

135+ notHole (Hole _) = False

136+ notHole _ = True

137+

122 -- TODO: there's an annoying amount of repetition between this and the

138 -- TODO: there's an annoying amount of repetition between this and the

123 -- main unification function. Consider lifting it out.

139 -- main unification function. Consider lifting it out.

124

140

@@ -173,7 +189,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

173 uniqueBinders env (Bind n b sc)

189 uniqueBinders env (Bind n b sc)

174 | n `elem` env

190 | n `elem` env

175 = let n' = uniqueName n env in

191 = let n' = uniqueName n env in

176− Bind n' (fmap (uniqueBinders env) b)

192+ explicitHole $ Bind n' (fmap (uniqueBinders env) b)

177 (uniqueBinders (n':env) (rename n n' sc))

193 (uniqueBinders (n':env) (rename n n' sc))

178 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

194 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

179 (uniqueBinders (n:env) sc)

195 (uniqueBinders (n:env) sc)

@@ -185,6 +201,10 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

185 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

201 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

186 rename n n' t = t

202 rename n n' t = t

187

203

204+ explicitHole (Bind n (Hole ty) sc)

205+ = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

206+ explicitHole t = t

207+

188trimSolutions ns = dropPairs ns

208trimSolutions ns = dropPairs ns

189 where dropPairs [] = []

209 where dropPairs [] = []

190 dropPairs (n@(x, P _ x' _) : ns)

210 dropPairs (n@(x, P _ x' _) : ns)

@@ -204,11 +224,16 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

204 doSubst (_ : env) tm

224 doSubst (_ : env) tm

205 = doSubst env tm

225 = doSubst env tm

206

226

227+hasv (V x) = True

228+hasv (App f a) = hasv f || hasv a

229+hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

230+hasv _ = False

207

231

208unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

232unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

209 TC ([(Name, TT Name)], Fails)

233 TC ([(Name, TT Name)], Fails)

210unify ctxt env topx topy inj holes from =

234unify ctxt env topx topy inj holes from =

235+-- traceWhen (hasv topx || hasv topy)

211−-- trace ("Unifying " ++ show (topx, topy)) $

236+-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

212 -- don't bother if topx and topy are different at the head

237 -- don't bother if topx and topy are different at the head

213 case runStateT (un False [] (renameBindersTm env topx)

238 case runStateT (un False [] (renameBindersTm env topx)

214 (renameBindersTm env topy)) (UI 0 []) of

239 (renameBindersTm env topy)) (UI 0 []) of

@@ -295,7 +320,7 @@ unify ctxt env topx topy inj holes from =

295 | injective ty && not (holeIn env x || x `elem` holes)

320 | injective ty && not (holeIn env x || x `elem` holes)

296 = unifyTmpFail tx ty

321 = unifyTmpFail tx ty

297 un' fn bnames xtm@(P _ x _) tm

322 un' fn bnames xtm@(P _ x _) tm

298− | holeIn env x || x `elem` holes

323+ | pureTerm tm, holeIn env x || x `elem` holes

299 = do UI s f <- get

324 = do UI s f <- get

300 -- injectivity check

325 -- injectivity check

301 x <- checkCycle bnames (x, tm)

326 x <- checkCycle bnames (x, tm)

@@ -305,11 +330,11 @@ unify ctxt env topx topy inj holes from =

305 then unifyTmpFail xtm tm

330 then unifyTmpFail xtm tm

306 else do sc 1

331 else do sc 1

307 return x

332 return x

308− | not (injective xtm) && injective tm

333+ | pureTerm tm, not (injective xtm) && injective tm

309 = do checkCycle bnames (x, tm)

334 = do checkCycle bnames (x, tm)

310 unifyTmpFail xtm tm

335 unifyTmpFail xtm tm

311 un' fn bnames tm ytm@(P _ y _)

336 un' fn bnames tm ytm@(P _ y _)

312− | holeIn env y || y `elem` holes

337+ | pureTerm tm, holeIn env y || y `elem` holes

313 = do UI s f <- get

338 = do UI s f <- get

314 -- injectivity check

339 -- injectivity check

315 x <- checkCycle bnames (y, tm)

340 x <- checkCycle bnames (y, tm)

@@ -319,7 +344,7 @@ unify ctxt env topx topy inj holes from =

319 then unifyTmpFail tm ytm

344 then unifyTmpFail tm ytm

320 else do sc 1

345 else do sc 1

321 return x

346 return x

322− | not (injective ytm) && injective tm

347+ | pureTerm tm, not (injective ytm) && injective tm

323 = do checkCycle bnames (y, tm)

348 = do checkCycle bnames (y, tm)

324 unifyTmpFail tm ytm

349 unifyTmpFail tm ytm

325 un' fn bnames (V i) (P _ x _)

350 un' fn bnames (V i) (P _ x _)

@@ -524,7 +549,7 @@ unify ctxt env topx topy inj holes from =

524 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

549 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

525 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

550 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

526

551

527− checkScope ns (x, tm) =

552+ checkScope ns (x, tm) | pureTerm tm =

528-- case boundVs (envPos x 0 env) tm of

553-- case boundVs (envPos x 0 env) tm of

529-- [] -> return [(x, tm)]

554-- [] -> return [(x, tm)]

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

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

@@ -535,6 +560,7 @@ unify ctxt env topx topy inj holes from =

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

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

536 where inst [] tm = tm

561 where inst [] tm = tm

537 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

562 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

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

538

564

539 bind i ns tm

565 bind i ns tm

540 | i < 0 = tm

566 | i < 0 = tm

src/Idris/Coverage.hs+41−19

@@ -9,7 +9,7 @@ import Idris.Core.CaseTree

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12−import Idris.Output (iWarn)

12+import Idris.Output (iWarn, iputStrLn)

13

14import Data.List

15import Data.Either

@@ -211,7 +211,7 @@ genAll i args

211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

212 let tyn = getTy n (tt_ctxt i)

213 case lookupCtxt tyn (idris_datatypes i) of

214− (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

214+ (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

215 _ -> [p]

216 ops fc n arg o = return Placeholder

217

@@ -255,38 +255,48 @@ checkAllCovering fc done top n | not (n `elem` done)

255 case lookupTotal n (tt_ctxt i) of

256 [tot@(Partial NotCovering)] ->

257 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

258− addIBC (IBCTotCheckErr fc msg)

259 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

258 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

260− _ -> return ()

259+ addIBC (IBCTotCheckErr fc msg)

260+ [Partial _] ->

261− case lookupCtxt n (idris_callgraph i) of

261+ case lookupCtxt n (idris_callgraph i) of

262− [cg] -> mapM_ (checkAllCovering fc (n : done) top)

262+ [cg] -> mapM_ (checkAllCovering fc (n : done) top)

263− (map fst (calls cg))

263+ (map fst (calls cg))

264+ _ -> return ()

264− _ -> return ()

265+ x -> return () -- stop if total

265checkAllCovering _ _ _ _ = return ()

266checkAllCovering _ _ _ _ = return ()

266

267

268+-- Check if, in a given group of type declarations mut_ns,

267−-- Check if, in a given type n, the constructor cn : ty is strictly positive,

269+-- the constructor cn : ty is strictly positive,

268-- and update the context accordingly

270-- and update the context accordingly

269

271

270−checkPositive :: Name -> (Name, Type) -> Idris ()

272+checkPositive :: [Name] -> (Name, Type) -> Idris Totality

271−checkPositive n (cn, ty')

273+checkPositive mut_ns (cn, ty')

272− = do let ty = delazy ty'

274+ = do let ty = delazy' True ty'

273 let p = cp ty

275 let p = cp ty

274 i <- getIState

276 i <- getIState

275 let tot = if p then Total (args ty) else Partial NotPositive

277 let tot = if p then Total (args ty) else Partial NotPositive

276 let ctxt' = setTotal cn tot (tt_ctxt i)

278 let ctxt' = setTotal cn tot (tt_ctxt i)

277 putIState (i { tt_ctxt = ctxt' })

279 putIState (i { tt_ctxt = ctxt' })

278− logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot

280+ logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

279 addIBC (IBCTotal cn tot)

281 addIBC (IBCTotal cn tot)

282+ return tot

280 where

283 where

281 args t = [0..length (getArgTys t)-1]

284 args t = [0..length (getArgTys t)-1]

282

285

283 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

286 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

287+ cp t | (P _ n' _, args) <- unApply t,

288+ n' `elem` mut_ns = all noRec args

284− cp t = True

289+ cp _ = True

285

290

286 posArg (Bind _ (Pi nty) sc)

291 posArg (Bind _ (Pi nty) sc)

287 | (P _ n' _, args) <- unApply nty

292 | (P _ n' _, args) <- unApply nty

288− = n /= n' && posArg sc

293+ = n' `notElem` mut_ns && all noRec args && posArg sc

289− posArg t = True

294+ posArg t | (P _ n' _, args) <- unApply t,

295+ n' `elem` mut_ns = all noRec args

296+ posArg _ = True

297+

298+ noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

299+

290

300

291calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

301calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

292calcProd i fc topn pats

302calcProd i fc topn pats

@@ -334,7 +344,7 @@ calcProd i fc topn pats

334 cotype (DCon _ _) n ty

344 cotype (DCon _ _) n ty

335 | (P _ t _, _) <- unApply (getRetTy ty)

345 | (P _ t _, _) <- unApply (getRetTy ty)

336 = case lookupCtxt t (idris_datatypes i) of

346 = case lookupCtxt t (idris_datatypes i) of

337− [TI _ True _ _] -> True

347+ [TI _ True _ _ _] -> True

338 _ -> False

348 _ -> False

339 cotype nt n ty = False

349 cotype nt n ty = False

340

350

@@ -382,6 +392,14 @@ checkTotality path fc n

382 setTotality n t'

392 setTotality n t'

383 addIBC (IBCTotal n t')

393 addIBC (IBCTotal n t')

384 return t'

394 return t'

395+ [TyDecl (DCon _ _) ty] ->

396+ case unApply (getRetTy ty) of

397+ (P _ tyn _, _) -> do

398+ let ms = case lookupCtxt tyn (idris_datatypes i) of

399+ [TI _ _ _ _ xs@(_:_)] -> xs

400+ ts -> [tyn]

401+ checkPositive ms (n, ty)

402+ _-> return $ Total []

385 _ -> return $ Total []

403 _ -> return $ Total []

386 x -> return x

404 x -> return x

387 case t' of

405 case t' of

@@ -415,6 +433,10 @@ checkDeclTotality (fc, n)

415-- buildSCG (fc, n)

433-- buildSCG (fc, n)

416-- logLvl 2 $ "Built SCG"

434-- logLvl 2 $ "Built SCG"

417 i <- getIState

435 i <- getIState

436+ let opts = case lookupCtxt n (idris_flags i) of

437+ [fs] -> fs

438+ _ -> []

439+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

418 t <- checkTotality [] fc n

440 t <- checkTotality [] fc n

419 case t of

441 case t of

420 -- if it's not total, it can't reduce, to keep

442 -- if it's not total, it can't reduce, to keep

@@ -551,7 +573,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

551

573

552 isInductive (P _ nty _) (P _ nty' _) =

574 isInductive (P _ nty _) (P _ nty' _) =

553 let co = case lookupCtxt nty (idris_datatypes ist) of

575 let co = case lookupCtxt nty (idris_datatypes ist) of

554− [TI _ x _ _] -> x

576+ [TI _ x _ _ _] -> x

555 _ -> False in

577 _ -> False in

556 nty == nty' && not co

578 nty == nty' && not co

557 isInductive _ _ = False

579 isInductive _ _ = False

@@ -634,7 +656,7 @@ checkMP ist i mp = if i > 0

634 = case lookupTotal f (tt_ctxt ist) of

656 = case lookupTotal f (tt_ctxt ist) of

635 [Total _] -> Unchecked -- okay so far

657 [Total _] -> Unchecked -- okay so far

636 [Partial _] -> Partial (Other [f])

658 [Partial _] -> Partial (Other [f])

637− x -> error (show x)

659+ x -> error $ "CAN'T HAPPEN: " ++ (show x)

638 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

660 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

639 = Total []

661 = Total []

640 tryPath desc path (e@(f, args) : es) arg

662 tryPath desc path (e@(f, args) : es) arg

src/Idris/DeepSeq.hs+3−3

@@ -290,7 +290,7 @@ instance NFData OptInfo where

290 = rnf x1 `seq` rnf x2 `seq` ()

291

292instance NFData TypeInfo where

293− rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

293+ rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

294

295instance (NFData t) => NFData (DSL' t) where

296 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

@@ -321,11 +321,11 @@ instance NFData Using where

321

322

323instance NFData SyntaxInfo where

324− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9)

324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

325 = rnf x1 `seq`

326 rnf x2 `seq`

327 rnf x3 `seq`

328− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

328+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

329

330

331

src/Idris/Delaborate.hs+2−2

@@ -93,13 +93,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

93 | n == eqCon = PRefl un (de env [] r)

94 | n == sUN "lazy" = de env [] r

95 deFn env (P _ n _) [ty, Bind x (Lam _) r]

96− | n == sUN "Exists"

96+ | n == sUN "Sigma"

97 = PDPair un IsType (PRef un x) (de env [] ty)

98 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

99 deFn env (P _ n _) [_,_,l,r]

100 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

101 | n == eqTy = PEq un (de env [] l) (de env [] r)

102− | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder

102+ | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

103 (de env [] r)

104 deFn env f@(P _ n _) args

105 | n `elem` map snd env

src/Idris/ElabDecls.hs+31−12

@@ -125,7 +125,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

125 let (t, _) = unApply (getRetTy nty')

126 let corec = case t of

127 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

128− [TI _ True _ _] -> True

128+ [TI _ True _ _ _] -> True

129 _ -> False

130 _ -> False

131 -- Productivity checking now via checking for guarded 'Delay'

@@ -256,8 +256,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

256 let as = map (const Nothing) (getArgTys cty)

257 let params = findParams (map snd cons)

258 logLvl 2 $ "Parameters : " ++ show params

259+ -- TI contains information about mutually declared types - this will

260+ -- be updated when the mutual block is complete

259 putIState (i { idris_datatypes =

261 putIState (i { idris_datatypes =

260− addDef n (TI (map fst cons) codata opts params)

262+ addDef n (TI (map fst cons) codata opts params [n])

261 (idris_datatypes i) })

263 (idris_datatypes i) })

262 addIBC (IBCDef n)

264 addIBC (IBCDef n)

263 addIBC (IBCData n)

265 addIBC (IBCData n)

@@ -269,7 +271,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

269 -- TMP HACK! Make this a data option

271 -- TMP HACK! Make this a data option

270 updateContext (addDatatype (Data n ttag cty cons))

272 updateContext (addDatatype (Data n ttag cty cons))

271 updateContext (setMetaInformation n metainf)

273 updateContext (setMetaInformation n metainf)

274+ mapM_ totcheck (zip (repeat fc) (map fst cons))

272− mapM_ (checkPositive n) cons

275+-- mapM_ (checkPositive n) cons

273

276

274 -- if there's exactly one constructor,

277 -- if there's exactly one constructor,

275 -- mark both the type and the constructor as detaggable

278 -- mark both the type and the constructor as detaggable

@@ -1195,7 +1198,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1195 force (normalisePats ctxt [] y))

1198 force (normalisePats ctxt [] y))

1196 simple_lhs ctxt t = t

1199 simple_lhs ctxt t = t

1197

1200

1198− simple_rt ctxt (p, x, y) = (p, x, force (rt_simplify ctxt [] y))

1201+ simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

1202+ (rt_simplify ctxt [] y)))

1199

1203

1200 -- this is so pattern types are in the right form for erasure

1204 -- this is so pattern types are in the right form for erasure

1201 normalisePats ctxt env (Bind n (PVar t) sc)

1205 normalisePats ctxt env (Bind n (PVar t) sc)

@@ -1616,7 +1620,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1616 rev <- case ret_fam of

1620 rev <- case ret_fam of

1617 P _ rfamn _ ->

1621 P _ rfamn _ ->

1618 case lookupCtxt rfamn (idris_datatypes i) of

1622 case lookupCtxt rfamn (idris_datatypes i) of

1619− [TI _ _ dopts _] ->

1623+ [TI _ _ dopts _ _] ->

1620 return (DataErrRev `elem` dopts)

1624 return (DataErrRev `elem` dopts)

1621 _ -> return False

1625 _ -> return False

1622 _ -> return False

1626 _ -> return False

@@ -2088,19 +2092,19 @@ elabInstance info syn what fc cs n ps t expn ds = do

2088

2092

2089 -- Bring variables in instance head into scope

2093 -- Bring variables in instance head into scope

2090 ist <- getIState

2094 ist <- getIState

2091− let headVars = mapMaybe (\p -> case p of

2095+ let headVars = nub $ mapMaybe (\p -> case p of

2092− PRef _ n ->

2096+ PRef _ n ->

2093− case lookupTy n (tt_ctxt ist) of

2097+ case lookupTy n (tt_ctxt ist) of

2094− [] -> Just n

2098+ [] -> Just n

2095− _ -> Nothing

2099+ _ -> Nothing

2096− _ -> Nothing) ps

2100+ _ -> Nothing) ps

2097-- let lhs = PRef fc iname

2101-- let lhs = PRef fc iname

2098 let lhs = PApp fc (PRef fc iname)

2102 let lhs = PApp fc (PRef fc iname)

2099 (map (\n -> pimp n (PRef fc n) True) headVars)

2103 (map (\n -> pimp n (PRef fc n) True) headVars)

2100 let rhs = PApp fc (PRef fc (instanceName ci))

2104 let rhs = PApp fc (PRef fc (instanceName ci))

2101 (map (pexp . mkMethApp) mtys)

2105 (map (pexp . mkMethApp) mtys)

2102

2106

2103− logLvl 5 $ "Instance LHS " ++ show lhs

2107+ logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

2104 logLvl 5 $ "Instance RHS " ++ show rhs

2108 logLvl 5 $ "Instance RHS " ++ show rhs

2105

2109

2106 let idecls = [PClauses fc [Dictionary] iname

2110 let idecls = [PClauses fc [Dictionary] iname

@@ -2339,6 +2343,11 @@ elabDecl' what info (PMutual f ps)

2339 [p] -> elabDecl what info p

2343 [p] -> elabDecl what info p

2340 _ -> do mapM_ (elabDecl ETypes info) ps

2344 _ -> do mapM_ (elabDecl ETypes info) ps

2341 mapM_ (elabDecl EDefns info) ps

2345 mapM_ (elabDecl EDefns info) ps

2346+ -- record mutually defined data definitions

2347+ let datans = concatMap declared (filter isDataDecl ps)

2348+ mapM_ (setMutData datans) datans

2349+ iLOG $ "Rechecking for positivity " ++ show datans

2350+ mapM_ (\x -> do setTotality x Unchecked) datans

2342 -- Do totality checking after entire mutual block

2351 -- Do totality checking after entire mutual block

2343 i <- get

2352 i <- get

2344 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

2353 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

@@ -2347,6 +2356,16 @@ elabDecl' what info (PMutual f ps)

2347 mapM_ buildSCG (idris_totcheck i)

2356 mapM_ buildSCG (idris_totcheck i)

2348 mapM_ checkDeclTotality (idris_totcheck i)

2357 mapM_ checkDeclTotality (idris_totcheck i)

2349 clear_totcheck

2358 clear_totcheck

2359+ where isDataDecl (PData _ _ _ _ _ _) = True

2360+ isDataDecl _ = False

2361+

2362+ setMutData ns n

2363+ = do i <- getIState

2364+ case lookupCtxt n (idris_datatypes i) of

2365+ [x] -> do let x' = x { mutual_types = ns }

2366+ putIState $ i { idris_datatypes

2367+ = addDef n x' (idris_datatypes i) }

2368+ _ -> return ()

2350

2369

2351elabDecl' what info (PParams f ns ps)

2370elabDecl' what info (PParams f ns ps)

2352 = do i <- getIState

2371 = do i <- getIState

src/Idris/ElabTerm.hs+34−10

@@ -66,15 +66,19 @@ build ist info pattern opts fn tm

66 ctxt <- get_context

67 probs <- get_probs

68 u <- getUnifyLog

69+ hs <- get_holes

69

70

70 when (not pattern) $

71 when (not pattern) $

72+ traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++

71− traceWhen u ("Remaining problems:\n" ++ show probs) $

73+ "Remaining problems:\n" ++ show probs) $

72 do unify_all; matchProblems True; unifyProblems

74 do unify_all; matchProblems True; unifyProblems

75+

73 probs <- get_probs

76 probs <- get_probs

74 case probs of

77 case probs of

75 [] -> return ()

78 [] -> return ()

79+ ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

76− ((_,_,_,e,_,_):es) -> if inf then return ()

80+ if inf then return ()

77− else lift (Error e)

81+ else lift (Error e)

78 is <- getAux

82 is <- getAux

79 tt <- get_term

83 tt <- get_term

80 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

84 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -263,7 +267,8 @@ elab ist info pattern opts fn tm

263 ty <- goal

267 ty <- goal

264 ctxt <- get_context

268 ctxt <- get_context

265 let (tc, _) = unApply ty

269 let (tc, _) = unApply ty

270+ env <- get_env

266− let as' = pruneByType tc ctxt as

271+ let as' = pruneByType (map fst env) tc ctxt as

267-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

272-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

268 tryAll (zip (map (elab' ina) as') (map showHd as'))

273 tryAll (zip (map (elab' ina) as') (map showHd as'))

269 where showHd (PApp _ (PRef _ n) _) = n

274 where showHd (PApp _ (PRef _ n) _) = n

@@ -495,6 +500,7 @@ elab ist info pattern opts fn tm

495 where alt t = case getTm t of

500 where alt t = case getTm t of

496 PAlternative False _ -> 5

501 PAlternative False _ -> 5

497 PAlternative True _ -> 1

502 PAlternative True _ -> 1

503+ PTactics _ -> 150

498 PLam _ _ _ -> 2

504 PLam _ _ _ -> 2

499 PRewrite _ _ _ _ -> 3

505 PRewrite _ _ _ _ -> 3

500 _ -> 0

506 _ -> 0

@@ -692,6 +698,9 @@ elab ist info pattern opts fn tm

692 addImpl ist (PApp fc (PRef fc (sUN "Delay"))

698 addImpl ist (PApp fc (PRef fc (sUN "Delay"))

693 [pexp t])

699 [pexp t])

694

700

701+ -- case is tricky enough without implicit coercions! If they are needed,

702+ -- they can go in the branches separately.

703+ insertCoerce ina t@(PCase _ _ _) = return t

695 insertCoerce ina t =

704 insertCoerce ina t =

696 do ty <- goal

705 do ty <- goal

697 -- Check for possible coercions to get to the goal

706 -- Check for possible coercions to get to the goal

@@ -782,8 +791,21 @@ pruneAlt xs = map prune xs

782

791

783-- Rule out alternatives that don't return the same type as the head of the goal

792-- Rule out alternatives that don't return the same type as the head of the goal

784-- (If there are none left as a result, do nothing)

793-- (If there are none left as a result, do nothing)

785−pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

794+pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]

795+-- if an alternative has a locally bound name at the head, take it

786−pruneByType (P _ n _) c as

796+pruneByType env t c as

797+ | Just a <- locallyBound as = [a]

798+ where

799+ locallyBound [] = Nothing

800+ locallyBound (t:ts)

801+ | Just n <- getName t,

802+ n `elem` env = Just t

803+ | otherwise = locallyBound ts

804+ getName (PRef _ n) = Just n

805+ getName (PApp _ f _) = getName f

806+ getName _ = Nothing

807+

808+pruneByType env (P _ n _) c as

787-- if the goal type is polymorphic, keep e

809-- if the goal type is polymorphic, keep e

788 | [] <- lookupTy n c = as

810 | [] <- lookupTy n c = as

789 | otherwise

811 | otherwise

@@ -809,7 +831,7 @@ pruneByType (P _ n _) c as

809 _ -> False

831 _ -> False

810 _ -> False

832 _ -> False

811

833

812−pruneByType t _ as = as

834+pruneByType _ t _ as = as

813

835

814findInstances :: IState -> Term -> [Name]

836findInstances :: IState -> Term -> [Name]

815findInstances ist t

837findInstances ist t

@@ -822,9 +844,9 @@ findInstances ist t

822trivial' ist

844trivial' ist

823 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

845 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

824proofSearch' ist rec depth prv top n hints

846proofSearch' ist rec depth prv top n hints

847+ = do unifyProblems

825− = proofSearch rec prv depth

848+ proofSearch rec prv depth

826− (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

849+ (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

827−

828

850

829resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

851resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

830resolveTC = resTC' []

852resolveTC = resTC' []

@@ -1632,6 +1654,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

1632 then handle err

1654 then handle err

1633 else applyHandlers err hs

1655 else applyHandlers err hs

1634 return (ElaboratingArg f a prev err')

1656 return (ElaboratingArg f a prev err')

1657+ -- ProofSearchFail is an internal detail - so don't expose it

1658+ handle (ProofSearchFail e) = handle e

1635 -- TODO: argument-specific error handlers go here for ElaboratingArg

1659 -- TODO: argument-specific error handlers go here for ElaboratingArg

1636 handle e = do ist <- getIState

1660 handle e = do ist <- getIState

1637 logLvl 2 "Starting error reflection"

1661 logLvl 2 "Starting error reflection"

src/Idris/Erasure.hs+18−10

@@ -294,7 +294,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

294 -- that the result of this function is used at all

295 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

296 where

297−

298 addTagDep = case alts of

297 addTagDep = case alts of

299 [_] -> id -- single branch, tag not used

298 [_] -> id -- single branch, tag not used

300 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)

299 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)

@@ -329,11 +328,15 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

329 | otherwise = \j -> Nothing

328 | otherwise = \j -> Nothing

330

329

331 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

330 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

332− getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps

331+ getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps

333

332

334 -- named variables introduce dependencies as described in `vs'

333 -- named variables introduce dependencies as described in `vs'

335 getDepsTerm vs bs cd (P _ n _)

334 getDepsTerm vs bs cd (P _ n _)

335+ -- de bruijns (lambda-bound, let-bound vars)

336+ | Just deps <- lookup n bs

337+ = deps cd

338+

336− -- local variables

339+ -- ctor-bound/arg-bound variables

337 | Just var <- M.lookup n vs

340 | Just var <- M.lookup n vs

338 = M.singleton cd (viDeps var)

341 = M.singleton cd (viDeps var)

339

342

@@ -348,18 +351,18 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

348 specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

351 specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

349

352

350 -- dependencies of de bruijn variables are described in `bs'

353 -- dependencies of de bruijn variables are described in `bs'

351− getDepsTerm vs bs cd (V i) = (bs !! i) cd

354+ getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

352

355

353 getDepsTerm vs bs cd (Bind n bdr t)

356 getDepsTerm vs bs cd (Bind n bdr t)

354 -- here we just push IM.empty on the de bruijn stack

357 -- here we just push IM.empty on the de bruijn stack

355 -- the args will be marked as used at the usage site

358 -- the args will be marked as used at the usage site

356− | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

359+ | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

357− | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

360+ | Pi ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

358

361

359 -- let-bound variables can get partially evaluated

362 -- let-bound variables can get partially evaluated

360 -- it is sufficient just to plug the Cond in when the bound names are used

363 -- it is sufficient just to plug the Cond in when the bound names are used

361− | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t

364+ | Let ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

362− | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t

365+ | NLet ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

363 where

366 where

364 var t cd = getDepsTerm vs bs cd t

367 var t cd = getDepsTerm vs bs cd t

365

368

@@ -386,6 +389,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

386 -- a bound variable might draw in additional dependencies,

389 -- a bound variable might draw in additional dependencies,

387 -- think: f x = x 0 <-- here, `x' _is_ used

390 -- think: f x = x 0 <-- here, `x' _is_ used

388 P _ n _

391 P _ n _

392+ -- debruijn-bound name

393+ | Just deps <- lookup n bs

394+ -> deps cd `union` unconditionalDeps args

395+

389 -- local name that refers to a method

396 -- local name that refers to a method

390 | Just var <- M.lookup n vs

397 | Just var <- M.lookup n vs

391 , Just meth <- viMethod var

398 , Just meth <- viMethod var

@@ -402,7 +409,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

402 -> conditionalDeps n args

409 -> conditionalDeps n args

403

410

404 -- TODO: could we somehow infer how bound variables use their arguments?

411 -- TODO: could we somehow infer how bound variables use their arguments?

405− V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)

412+ V i -> snd (bs !! i) cd `union` unconditionalDeps args

406

413

407 -- we interpret applied lambdas as lets in order to reuse code here

414 -- we interpret applied lambdas as lets in order to reuse code here

408 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

415 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

@@ -418,6 +425,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

418

425

419 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

426 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

420 where

427 where

428+ union = M.unionWith $ M.unionWith S.union

421 ins = M.insertWith (M.unionWith S.union) cd

429 ins = M.insertWith (M.unionWith S.union) cd

422

430

423 unconditionalDeps :: [Term] -> Deps

431 unconditionalDeps :: [Term] -> Deps

@@ -441,7 +449,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

441 , viMethod = Nothing

449 , viMethod = Nothing

442 }) | (v, i) <- zip args [0..]]

450 }) | (v, i) <- zip args [0..]]

443 deps i = M.singleton (metameth, Arg i) S.empty

451 deps i = M.singleton (metameth, Arg i) S.empty

444− bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]

452+ bruijns = reverse [(n, \cd -> M.singleton cd (deps i)) | (i, n) <- zip [0..] args]

445 cond = S.singleton (metameth, Result)

453 cond = S.singleton (metameth, Result)

446 metameth = mkFieldName ctorName methNo

454 metameth = mkFieldName ctorName methNo

447 (args, body) = unfoldLams t

455 (args, body) = unfoldLams t

src/Idris/Error.hs+4−2

@@ -43,11 +43,13 @@ idrisCatch = catchError

43setAndReport :: Err -> Idris ()

44setAndReport e = do ist <- getIState

45 let h = idris_outh ist

46− case e of

46+ case (unwrap e) of

47 At fc e -> do setErrSpan fc

48 ihWarn h fc $ pprintErr ist e

49 _ -> do setErrSpan (getErrSpan e)

50− ihputStrLn h $ pshow ist e

50+ ihWarn h emptyFC $ pprintErr ist e

51+ where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor

52+ unwrap e = e

51

53

52ifail :: String -> Idris a

54ifail :: String -> Idris a

53ifail = throwError . Msg

55ifail = throwError . Msg

src/Idris/Help.hs+3−1

@@ -33,6 +33,7 @@ help =

33 ([":doc"], NameArg, "Show internal documentation"),

34 ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),

35 ([":apropos"], NoArg, "Search names, types, and documentation"),

36+ ([":search", ":s"], ExprArg, "Search for values by type"),

36 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

37 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

37 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38 ([":total"], NameArg, "Check the totality of a name"),

39 ([":total"], NameArg, "Check the totality of a name"),

@@ -57,7 +58,8 @@ help =

57 ([":unset"], OptionArg, "Unset an option"),

58 ([":unset"], OptionArg, "Unset an option"),

58 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

59 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

59 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

60 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

60− ([":q",":quit"], NoArg, "Exit the Idris system")

61+ ([":q",":quit"], NoArg, "Exit the Idris system"),

62+ ([":w", ":warranty"], NoArg, "Displays warranty information")

61 ]

63 ]

62

64

63-- | Use these for completion, but don't show them in :help

65-- | Use these for completion, but don't show them in :help

src/Idris/IBC.hs+10−8

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 73

33+ibcVersion = 74

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -1582,7 +1582,7 @@ instance Binary Using where

1582 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1583

1584instance Binary SyntaxInfo where

1585− put (Syn x1 x2 x3 x4 _ x5 x6 _ x7)

1585+ put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7)

1586 = do put x1

1587 put x2

1588 put x3

@@ -1598,7 +1598,7 @@ instance Binary SyntaxInfo where

1598 x5 <- get

1599 x6 <- get

1600 x7 <- get

1601− return (Syn x1 x2 x3 x4 id x5 x6 Nothing x7)

1601+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7)

1602

1603instance (Binary t) => Binary (PClause' t) where

1604 put x

@@ -2152,15 +2152,17 @@ instance Binary OptInfo where

2152 return (Optimise x1 x2)

2153

2154instance Binary TypeInfo where

2155− put (TI x1 x2 x3 x4) = do put x1

2155+ put (TI x1 x2 x3 x4 x5) = do put x1

2156− put x2

2156+ put x2

2157− put x3

2157+ put x3

2158− put x4

2158+ put x4

2159+ put x5

2159 get = do x1 <- get

2160 get = do x1 <- get

2160 x2 <- get

2161 x2 <- get

2161 x3 <- get

2162 x3 <- get

2162 x4 <- get

2163 x4 <- get

2164+ x5 <- get

2163− return (TI x1 x2 x3 x4)

2165+ return (TI x1 x2 x3 x4 x5)

2164

2166

2165instance Binary SynContext where

2167instance Binary SynContext where

2166 put x

2168 put x

src/Idris/Output.hs+35−44

@@ -16,6 +16,7 @@ import Debug.Trace

16import System.IO (stdout, Handle, hPutStrLn)

17

18import Data.List (nub)

19+import Data.Maybe (fromMaybe)

19

20

20pshow :: IState -> Err -> String

21pshow :: IState -> Err -> String

21pshow ist err = displayDecorated (consoleDecorate ist) .

22pshow ist err = displayDecorated (consoleDecorate ist) .

@@ -53,16 +54,6 @@ iRender d = do w <- getWidth

53 | otherwise -> do width <- runIO getScreenWidth

54 | otherwise -> do width <- runIO getScreenWidth

54 return $ renderPretty 0.8 width d

55 return $ renderPretty 0.8 width d

55

56

56−ihPrintResult :: Handle -> String -> Idris ()

57−ihPrintResult h s = do i <- getIState

58− case idris_outputmode i of

59− RawOutput -> case s of

60− "" -> return ()

61− s -> runIO $ hPutStrLn h s

62− IdeSlave n ->

63− let good = SexpList [SymbolAtom "ok", toSExp s] in

64− runIO $ hPutStrLn h $ convSExp "return" good n

65−

66-- | Write a pretty-printed term to the console with semantic coloring

57-- | Write a pretty-printed term to the console with semantic coloring

67consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

58consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

68consoleDisplayAnnotated h output = do ist <- getIState

59consoleDisplayAnnotated h output = do ist <- getIState

@@ -71,23 +62,8 @@ consoleDisplayAnnotated h output = do ist <- getIState

71 displayDecorated (consoleDecorate ist) $

62 displayDecorated (consoleDecorate ist) $

72 rendered

63 rendered

73

64

74−

75−-- | Write pretty-printed output to IDESlave with semantic annotations

76−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

77−ideSlaveReturnAnnotated n h out = do ist <- getIState

78− (str, spans) <- fmap displaySpans .

79− iRender .

80− fmap (fancifyAnnots ist) $

81− out

82− let good = [SymbolAtom "ok", toSExp str, toSExp spans]

83− runIO . hPutStrLn h $ convSExp "return" good n

84−

85ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

65ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

86−ihPrintTermWithType h tm ty = do ist <- getIState

66+ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)

87− let output = tm <+> colon <+> align ty

88− case idris_outputmode ist of

89− RawOutput -> consoleDisplayAnnotated h output

90− IdeSlave n -> ideSlaveReturnAnnotated n h output

91

67

92-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

68-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

93ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

69ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

@@ -96,9 +72,7 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState

96 let ppo = ppOptionIst ist

72 let ppo = ppOptionIst ist

97 let infixes = idris_infixes ist

73 let infixes = idris_infixes ist

98 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

74 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

99− case idris_outputmode ist of

75+ ihRenderResult h output

100− RawOutput -> consoleDisplayAnnotated h output

101− IdeSlave n -> ideSlaveReturnAnnotated n h output

102 where fullName n = prettyName True bnd n

76 where fullName n = prettyName True bnd n

103 ppOverload ppo infixes n tm =

77 ppOverload ppo infixes n tm =

104 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

78 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

@@ -109,28 +83,45 @@ ihRenderResult h d = do ist <- getIState

109 RawOutput -> consoleDisplayAnnotated h d

83 RawOutput -> consoleDisplayAnnotated h d

110 IdeSlave n -> ideSlaveReturnAnnotated n h d

84 IdeSlave n -> ideSlaveReturnAnnotated n h d

111

85

86+ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

87+ideSlaveReturnWithStatus status n h out = do

88+ ist <- getIState

89+ (str, spans) <- fmap displaySpans .

90+ iRender .

91+ fmap (fancifyAnnots ist) $

92+ out

93+ let good = [SymbolAtom status, toSExp str, toSExp spans]

94+ runIO . hPutStrLn h $ convSExp "return" good n

95+

96+

97+-- | Write pretty-printed output to IDESlave with semantic annotations

98+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

99+ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

100+

112-- | Show an error with semantic highlighting

101-- | Show an error with semantic highlighting

113ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

102ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

114ihRenderError h e = do ist <- getIState

103ihRenderError h e = do ist <- getIState

115 case idris_outputmode ist of

104 case idris_outputmode ist of

116 RawOutput -> consoleDisplayAnnotated h e

105 RawOutput -> consoleDisplayAnnotated h e

117− IdeSlave n -> do

106+ IdeSlave n -> ideSlaveReturnWithStatus "error" n h e

118− (str, spans) <- fmap displaySpans .

107+

119− iRender .

108+ihPrintWithStatus :: String -> Handle -> String -> Idris ()

120− fmap (fancifyAnnots ist) $

109+ihPrintWithStatus status h s = do

121− e

110+ i <- getIState

111+ case idris_outputmode i of

112+ RawOutput -> case s of

113+ "" -> return ()

114+ s -> runIO $ hPutStrLn h s

115+ IdeSlave n ->

122− let good = [SymbolAtom "error", toSExp str, toSExp spans]

116+ let good = SexpList [SymbolAtom status, toSExp s] in

123− runIO . hPutStrLn h $ convSExp "return" good n

117+ runIO $ hPutStrLn h $ convSExp "return" good n

118+

119+

120+ihPrintResult :: Handle -> String -> Idris ()

121+ihPrintResult = ihPrintWithStatus "ok"

124

122

125ihPrintError :: Handle -> String -> Idris ()

123ihPrintError :: Handle -> String -> Idris ()

126−ihPrintError h s = do i <- getIState

124+ihPrintError = ihPrintWithStatus "error"

127− case idris_outputmode i of

128− RawOutput -> case s of

129− "" -> return ()

130− s -> runIO $ hPutStrLn h s

131− IdeSlave n ->

132− let good = SexpList [SymbolAtom "error", toSExp s] in

133− runIO . hPutStrLn h $ convSExp "return" good n

134

125

135ihputStrLn :: Handle -> String -> Idris ()

126ihputStrLn :: Handle -> String -> Idris ()

136ihputStrLn h s = do i <- getIState

127ihputStrLn h s = do i <- getIState

src/Idris/Parser.hs+2−2

@@ -163,7 +163,7 @@ decl syn = do fc <- getFC

163 let continue = case maxline syn of

164 Nothing -> True

165 Just l -> if fst (fc_end fc) > l

166− then False

166+ then mut_nesting syn /= 0

167 else True

168 if continue then do notEndBlock

169 declBody

@@ -502,7 +502,7 @@ mutual syn =

502 do reserved "mutual"

503 openBlock

504 let pvars = syn_params syn

505− ds <- many (decl syn)

505+ ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

506 closeBlock

507 fc <- getFC

508 return [PMutual fc (concat ds)]

src/Idris/Primitives.hs+9−6

@@ -28,9 +28,10 @@ ty :: [Const] -> Const -> Type

28ty [] x = Constant x

29ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t)) (ty ts x)

30

31−total, partial :: Totality

31+total, partial, iopartial :: Totality

32total = Total []

33partial = Partial NotCovering

34+iopartial = Partial ExternalIO

34

35

35primitives :: [Prim]

36primitives :: [Prim]

36primitives =

37primitives =

@@ -164,16 +165,16 @@ primitives =

164 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

165 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

165 (1, LStrRev) total,

166 (1, LStrRev) total,

166 Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

167 Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

167− (1, LReadStr) partial,

168+ (1, LReadStr) iopartial,

168 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

169 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

169 (0, LVMPtr) total,

170 (0, LVMPtr) total,

170 -- Streams

171 -- Streams

171 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172− (0, LStdIn) partial,

173+ (0, LStdIn) iopartial,

173 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

174 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

174− (0, LStdOut) partial,

175+ (0, LStdOut) iopartial,

175 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

176 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

176− (0, LStdErr) partial,

177+ (0, LStdErr) iopartial,

177 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

178 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

178 (0, LNullPtr) total,

179 (0, LNullPtr) total,

179 -- Managed pointer registration

180 -- Managed pointer registration

@@ -183,7 +184,9 @@ primitives =

183 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_allocate)

184 Prim (sUN "prim__allocate") (ty [AType (ATInt (ITFixed IT64))] BufferType) 1 (p_allocate)

184 (1, LAllocate) total,

185 (1, LAllocate) total,

185 Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_appendBuffer)

186 Prim (sUN "prim__appendBuffer") (ty [BufferType, AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), AType (ATInt (ITFixed IT64)), BufferType] BufferType) 6 (p_appendBuffer)

186− (6, LAppendBuffer) partial

187+ (6, LAppendBuffer) partial,

188+ Prim (sUN "prim__systemInfo") (ty [AType (ATInt ITNative)] StrType) 1 (p_cantreduce)

189+ (1, LSystemInfo) total

187 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

190 ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

188 ++ concatMap vecOps vecTypes

191 ++ concatMap vecOps vecTypes

189 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes

192 ++ concatMap fixedOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64] -- ITNative, ITChar, ATFloat ] ++ vecTypes

src/Idris/REPL.hs+38−20

@@ -32,6 +32,7 @@ import Idris.DeepSeq

32import Idris.Output

33import Idris.Interactive

34import Idris.WhoCalls

35+import Idris.TypeSearch (searchByType)

35

36

36import Paths_idris

37import Paths_idris

37import Version_idris (gitHash)

38import Version_idris (gitHash)

@@ -109,7 +110,7 @@ repl orig mods

109 return ()

110 return ()

110 Just input -> -- H.catch

111 Just input -> -- H.catch

111 do ms <- H.catch (lift $ processInput input orig mods)

112 do ms <- H.catch (lift $ processInput input orig mods)

112− (ctrlC (return (Just mods)))

113+ (ctrlC (return (Just mods)))

113 case ms of

114 case ms of

114 Just mods -> repl orig mods

115 Just mods -> repl orig mods

115 Nothing -> return ()

116 Nothing -> return ()

@@ -120,7 +121,7 @@ repl orig mods

120 act -- repl orig mods

121 act -- repl orig mods

121

122

122 showMVs c thm [] = ""

123 showMVs c thm [] = ""

123− showMVs c thm ms = "Metavariables: " ++

124+ showMVs c thm ms = "Metavariables: " ++

124 show' 4 c thm (map fst ms) ++ "\n"

125 show' 4 c thm (map fst ms) ++ "\n"

125

126

126 show' 0 c thm ms = let l = length ms in

127 show' 0 c thm ms = let l = length ms in

@@ -128,7 +129,7 @@ repl orig mods

128 ++ " other"

129 ++ " other"

129 ++ if l == 1 then ")" else "s)"

130 ++ if l == 1 then ")" else "s)"

130 show' n c thm [m] = showM c thm m

131 show' n c thm [m] = showM c thm m

131− show' n c thm (m : ms) = showM c thm m ++ ", " ++

132+ show' n c thm (m : ms) = showM c thm m ++ ", " ++

132 show' (n - 1) c thm ms

133 show' (n - 1) c thm ms

133

134

134 showM c thm n = if c then colouriseFun thm (show n)

135 showM c thm n = if c then colouriseFun thm (show n)

@@ -387,6 +388,7 @@ splitName s = case reverse $ splitOn "." s of

387 (n:ns) -> Right $ sNS (sUN n) ns

388 (n:ns) -> Right $ sNS (sUN n) ns

388

389

389ideslaveProcess :: FilePath -> Command -> Idris ()

390ideslaveProcess :: FilePath -> Command -> Idris ()

391+ideslaveProcess fn Warranty = process stdout fn Warranty

390ideslaveProcess fn Help = process stdout fn Help

392ideslaveProcess fn Help = process stdout fn Help

391ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

393ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

392 iPrintResult "changed directory to"

394 iPrintResult "changed directory to"

@@ -563,6 +565,7 @@ insertScript prf (x : xs) = x : insertScript prf xs

563

565

564process :: Handle -> FilePath -> Command -> Idris ()

566process :: Handle -> FilePath -> Command -> Idris ()

565process h fn Help = iPrintResult displayHelp

567process h fn Help = iPrintResult displayHelp

568+process h fn Warranty = iPrintResult warranty

566process h fn (ChangeDirectory f)

569process h fn (ChangeDirectory f)

567 = do runIO $ setCurrentDirectory f

570 = do runIO $ setCurrentDirectory f

568 return ()

571 return ()

@@ -707,8 +710,8 @@ process h fn (DebugInfo n)

707 iputStrLn $ "Size change: " ++ show sc

710 iputStrLn $ "Size change: " ++ show sc

708 when (not (null cg')) $ do iputStrLn "Call graph:\n"

711 when (not (null cg')) $ do iputStrLn "Call graph:\n"

709 iputStrLn (show cg')

712 iputStrLn (show cg')

710−process h fn (Search t) = iPrintError "Not implemented"

713+process h fn (Search t) = searchByType h t

711−process h fn (CaseSplitAt updatefile l n)

714+process h fn (CaseSplitAt updatefile l n)

712 = caseSplitAt h fn updatefile l n

715 = caseSplitAt h fn updatefile l n

713process h fn (AddClauseFrom updatefile l n)

716process h fn (AddClauseFrom updatefile l n)

714 = addClauseFrom h fn updatefile l n

717 = addClauseFrom h fn updatefile l n

@@ -848,7 +851,7 @@ process h fn (Missing n)

848 = do i <- getIState

851 = do i <- getIState

849 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

852 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

850 case lookupCtxt n (idris_patdefs i) of

853 case lookupCtxt n (idris_patdefs i) of

851− [] -> return ()

854+ [] -> ihPrintError h $ "Unknown operator " ++ show n

852 [(_, tms)] ->

855 [(_, tms)] ->

853 iPrintResult (showSep "\n" (map (showTm i') tms))

856 iPrintResult (showSep "\n" (map (showTm i') tms))

854 _ -> iPrintError $ "Ambiguous name"

857 _ -> iPrintError $ "Ambiguous name"

@@ -903,10 +906,9 @@ process h fn ColourOff

903 putIState $ ist { idris_colourRepl = False }

906 putIState $ ist { idris_colourRepl = False }

904process h fn ListErrorHandlers =

907process h fn ListErrorHandlers =

905 do ist <- getIState

908 do ist <- getIState

906− case idris_errorhandlers ist of

909+ iPrintResult $ case idris_errorhandlers ist of

907− [] -> iPrintResult "No registered error handlers"

910+ [] -> "No registered error handlers"

908− handlers ->

909− iPrintResult $ "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

911+ handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

910process h fn (SetConsoleWidth w) = setWidth w

912process h fn (SetConsoleWidth w) = setWidth w

911

913

912process h fn (Apropos a) =

914process h fn (Apropos a) =

@@ -916,11 +918,8 @@ process h fn (Apropos a) =

916 delabTy ist n,

918 delabTy ist n,

917 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

919 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

918 | n <- sort names, isUN n ]

920 | n <- sort names, isUN n ]

919− ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)

921+ ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)

920− where renderApropos ist (name, ty, docs) =

921− prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

922− fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

923− isUN (UN _) = True

922+ where isUN (UN _) = True

924 isUN (NS n _) = isUN n

923 isUN (NS n _) = isUN n

925 isUN _ = False

924 isUN _ = False

926

925

@@ -1025,10 +1024,10 @@ loadInputs h inputs toline -- furthest line to read in input source files

1025 let ifiles = getModuleFiles modTree

1024 let ifiles = getModuleFiles modTree

1026 iLOG ("MODULE TREE : " ++ show modTree)

1025 iLOG ("MODULE TREE : " ++ show modTree)

1027 iLOG ("RELOAD: " ++ show ifiles)

1026 iLOG ("RELOAD: " ++ show ifiles)

1028− when (not (all ibc ifiles) || loadCode) $

1027+ when (not (all ibc ifiles) || loadCode) $

1029 tryLoad False (filter (not . ibc) ifiles)

1028 tryLoad False (filter (not . ibc) ifiles)

1030 -- return the files that need rechecking

1029 -- return the files that need rechecking

1031− return ifiles)

1030+ return ifiles)

1032 ninputs

1031 ninputs

1033 inew <- getIState

1032 inew <- getIState

1034 let tidata = idris_tyinfodata inew

1033 let tidata = idris_tyinfodata inew

@@ -1353,6 +1352,11 @@ getPkgMkDoc :: Opt -- ^ Opt to extract

1353getPkgMkDoc (PkgMkDoc str) = Just str

1352getPkgMkDoc (PkgMkDoc str) = Just str

1354getPkgMkDoc _ = Nothing

1353getPkgMkDoc _ = Nothing

1355

1354

1355+getPkgTest :: Opt -- ^ the option to extract

1356+ -> Maybe String -- ^ the package file to test

1357+getPkgTest (PkgTest f) = Just f

1358+getPkgTest _ = Nothing

1359+

1356getCodegen :: Opt -> Maybe Codegen

1360getCodegen :: Opt -> Maybe Codegen

1357getCodegen (UseCodegen x) = Just x

1361getCodegen (UseCodegen x) = Just x

1358getCodegen _ = Nothing

1362getCodegen _ = Nothing

@@ -1398,6 +1402,20 @@ banner = " ____ __ _ \n" ++

1398 " / _/___/ /____(_)____ \n" ++

1402 " / _/___/ /____(_)____ \n" ++

1399 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1403 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1400 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

1404 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

1401− " /___/\\__,_/_/ /_/____/ Type :? for help \n"

1405+ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++

1402−

1406+ "\n" ++

1403−

1407+ "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++

1408+ "For details type :warranty."

1409+

1410+warranty = "\n" ++

1411+ "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++

1412+ "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++

1413+ "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++

1414+ "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++

1415+ "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++

1416+ "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++

1417+ "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++

1418+ "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++

1419+ "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++

1420+ "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++

1421+ "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"

src/Idris/REPLParser.hs+6−4

@@ -33,6 +33,7 @@ cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) x

33pCmd :: P.IdrisParser Command

34pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

35 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

36+ <|> try (do cmd ["w", "warranty"]; eof; return Warranty)

36 <|> try (do cmd ["r", "reload"]; eof; return Reload)

37 <|> try (do cmd ["r", "reload"]; eof; return Reload)

37 <|> try (do cmd ["module"]; f <- P.identifier; eof;

38 <|> try (do cmd ["module"]; f <- P.identifier; eof;

38 return (ModImport (toPath f)))

39 return (ModImport (toPath f)))

@@ -48,11 +49,11 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

48 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

49 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

49 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

50 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

50 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

51 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

51− <|> try (do cmd ["lto", "loadto"];

52+ <|> try (do cmd ["lto", "loadto"];

52 toline <- P.natural

53 toline <- P.natural

53− f <- many anyChar;

54+ f <- many anyChar;

54 return (Load f (Just (fromInteger toline))))

55 return (Load f (Just (fromInteger toline))))

55− <|> try (do cmd ["l", "load"]; f <- many anyChar;

56+ <|> try (do cmd ["l", "load"]; f <- many anyChar;

56 return (Load f Nothing))

57 return (Load f Nothing))

57 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

58 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

58 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

59 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

@@ -71,7 +72,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

71 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

72 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

72 <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

73 <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

73 <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

74 <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

74− <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

75+ <|> try (do cmd ["s", "search"]; P.whiteSpace;

76+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))

75 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

76 upd <- option False (do P.lchar '!'; return True)

78 upd <- option False (do P.lchar '!'; return True)

77 l <- P.natural; n <- P.name;

79 l <- P.natural; n <- P.name;

src/Idris/TypeSearch.hsnew file+303

@@ -0,0 +1,303 @@

1+module Idris.TypeSearch (

2+ searchByType, searchPred, defaultScoreFunction

3+) where

4+

5+import Control.Applicative ((<$>), (<*>), (<|>))

6+import Control.Arrow (first, second, (&&&))

7+import Control.Monad (forM_, guard)

8+

9+import Data.Function (on)

10+import Data.List (find, minimumBy, sortBy, (\\))

11+import Data.Map (Map)

12+import qualified Data.Map as M

13+import Data.Maybe (catMaybes, fromMaybe, isJust)

14+import Data.Monoid (Monoid (mempty, mappend))

15+import Data.Set (Set)

16+import qualified Data.Set as S

17+

18+import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

19+import Idris.AbsSyntaxTree (class_instances, defaultSyntax, Idris,

20+ IState (idris_classes, idris_docstrings, tt_ctxt),

21+ implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

22+import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

23+import Idris.Core.TT

24+import Idris.Core.Unify (match_unify)

25+import Idris.Delaborate (delab, delabTy)

26+import Idris.Docstrings (noDocs, overview)

27+import Idris.ElabDecls (elabType')

28+import Idris.Output (ihRenderResult, ihPrintResult, ihPrintFunTypes)

29+

30+import System.IO (Handle)

31+

32+import Util.Pretty (text, vsep, char, (<>), Doc)

33+

34+searchByType :: Handle -> PTerm -> Idris ()

35+searchByType h pterm = do

36+ pterm' <- addUsingConstraints syn emptyFC pterm

37+ pterm'' <- implicit toplevel syn n pterm'

38+ i <- getIState

39+ let pterm''' = addImpl i pterm''

40+ ty <- elabType' False toplevel syn (fst noDocs) (snd noDocs) emptyFC [] n pterm'

41+ putIState i -- don't actually make any changes

42+ let names = searchUsing searchPred i ty

43+ let names' = take numLimit . takeWhile ((< scoreLimit) . getScore) $

44+ sortBy (compare `on` getScore) names

45+ let docs =

46+ [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

47+ displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

48+ | (n, (_,score)) <- names']

49+ ihRenderResult h $ vsep docs

50+ where

51+ getScore = defaultScoreFunction . snd . snd

52+ numLimit = 50

53+ scoreLimit = 100

54+ syn = defaultSyntax { implicitAllowed = True } -- syntax

55+ n = sMN 0 "searchType" -- name

56+

57+

58+searchUsing :: (IState -> Type -> Type -> Maybe a) -> IState -> Type -> [(Name, (Type, a))]

59+searchUsing pred istate ty =

60+ concat . M.elems $ M.mapWithKey (\key -> M.toAscList . M.mapMaybe (f key)) (definitions ctxt)

61+ where

62+ ctxt = tt_ctxt istate

63+ f k x = do

64+ guard $ not (special k)

65+ y <- get (fst4 x)

66+ let ny = normaliseC ctxt [] y

67+ -- traceShow k False `seq` return ()

68+ val <- pred istate nty ny

69+ return (y, val)

70+ nty = normaliseC ctxt [] ty

71+ fst4 :: (a,b,c,d) -> a

72+ fst4 (w,x,y,z) = w

73+ get :: Def -> Maybe Type

74+ get (Function ty tm) = Just ty

75+ get (TyDecl _ ty) = Just ty

76+ -- get (Operator ty _ _) = Just ty

77+ get (CaseOp _ ty _ _ _ _) = Just ty

78+ get _ = Nothing

79+ special :: Name -> Bool

80+ special (SN _) = True

81+ special _ = False

82+

83+

84+tcToMaybe :: TC' e a -> Maybe a

85+tcToMaybe (OK x) = Just x

86+tcToMaybe (Error _) = Nothing

87+

88+

89+

90+searchPred :: IState -> Type -> Type -> Maybe Score

91+searchPred istate ty1 = \ty2 -> case matcher ty2 of

92+ Nothing -> Nothing

93+ Just xs -> guard (not (null xs)) >> return (minimumBy (compare `on` defaultScoreFunction) xs)

94+ where

95+ matcher = unifyWithHoles True istate ty1

96+

97+

98+

99+

100+reverseDag :: Ord k => [((k, a), Set k)] -> [((k, a), Set k)]

101+reverseDag xs = map f xs where

102+ f ((k, v), _) = ((k, v), S.fromList . map (fst . fst) $ filter (S.member k . snd) xs)

103+

104+-- run vToP first!

105+-- returns [(the name and type of the bound variable

106+-- the names in the type of the bound variable)]

107+computeDagP :: Ord n => TT n -> ([((n, TT n), Set n)], TT n)

108+computeDagP t = (reverse (map f args), retTy) where

109+

110+ f (n, t) = ((n, t), M.keysSet (usedVars t))

111+

112+ (numArgs, args, retTy) = go 0 [] t

113+

114+ -- NOTE : args are in reverse order

115+ go k args (Bind n (Pi t) sc) = go (succ k) ( (n, t) : args ) sc

116+ go k args retTy = (k, args, retTy)

117+

118+

119+usedVars :: Ord n => TT n -> Map n (TT n)

120+usedVars (V j) = error "unexpected! run vToP first"

121+usedVars (P Bound n t) = M.singleton n t `M.union` usedVars t

122+usedVars (Bind n binder t2) = (M.delete n (usedVars t2) `M.union`) $ case binder of

123+ Let t v -> usedVars t `M.union` usedVars v

124+ Guess t v -> usedVars t `M.union` usedVars v

125+ b -> usedVars (binderTy b)

126+usedVars (App t1 t2) = usedVars t1 `M.union` usedVars t2

127+usedVars (Proj t _) = usedVars t

128+usedVars _ = M.empty

129+

130+deleteFromDag :: Ord n => n -> [((n, TT n), (a, Set n))] -> [((n, TT n), (a, Set n))]

131+deleteFromDag name [] = []

132+deleteFromDag name (((name2, ty), (ix, set)) : xs) = (if name == name2

133+ then id

134+ else (((name2, ty) , (ix, S.delete name set)) :) ) (deleteFromDag name xs)

135+

136+

137+data Score = Score

138+ { transposition :: Int

139+ , leftApplied :: Int

140+ , rightApplied :: Int

141+ , leftTypeClass :: Int

142+ , rightTypeClass :: Int } deriving (Eq, Show)

143+

144+displayScore :: Score -> Doc a

145+displayScore (Score trans lapp rapp lclass rclass) = text $ case (lt, gt) of

146+ (True , True ) -> "="

147+ (True , False) -> "<"

148+ (False, True ) -> ">"

149+ (False, False) -> " "

150+ where lt = lapp + lclass == 0

151+ gt = rapp + rclass == 0

152+

153+

154+scoreCriterion :: Score -> Bool

155+scoreCriterion (Score a b c d e) = True {- not

156+ ( (b > 0 && c > 0) || (b + c) > 2 ) -}

157+

158+defaultScoreFunction :: Score -> Int

159+defaultScoreFunction (Score a b c d e) = a + 9*b + 3*c + 12*d + 4*e + 100*(2*b + d)*(2*c + e)

160+ -- it's very bad to have *both* upcasting and downcasting

161+

162+instance Monoid Score where

163+ mempty = Score 0 0 0 0 0

164+ (Score a b c d e) `mappend` (Score a' b' c' d' e') = Score (a + a') (b + b') (c + c') (d + d') (e + e')

165+

166+

167+type ArgsDAG = [((Name, Type), (Int, Set Name))]

168+type ResType = ( [Name] , ArgsDAG , ArgsDAG )

169+

170+data State = State

171+ { holes :: ![Name]

172+ , args1 :: !ArgsDAG

173+ , args2 :: !ArgsDAG

174+ , score :: !Score

175+ }

176+

177+

178+--DONT run vToP first!

179+unifyWithHoles :: Bool -> IState -> Type -> Type -> Maybe [Score]

180+unifyWithHoles debugParam istate type1 = \type2 -> let

181+ (dag2, retTy2) = makeDag (uniqueBinders argNames1 type2)

182+ argNames2 = map (fst . fst) dag2

183+ startingHoles = argNames1 ++ argNames2

184+

185+ startingTypes = (retTy1, retTy2) : []

186+ in do

187+ state <- go (State startingHoles dag1 dag2 mempty) startingTypes

188+ return $ processDags state

189+ where

190+ ctxt = tt_ctxt istate

191+ classInfo = idris_classes istate

192+ (dag1, retTy1) = makeDag type1

193+ argNames1 = map (fst . fst) dag1

194+ makeDag = first (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) . computeDagP . vToP

195+

196+ matchf :: (Name, Term) -> Maybe (Name, Name)

197+ matchf (name, P Bound name2 _) = Just (name, name2)

198+ matchf _ = Nothing

199+

200+ -- update our state with the unification resolutions

201+ updateDags :: [(Name, Type)] -> ResType -> Maybe (ResType, [(Type, Type)], Score)

202+ updateDags [] res = Just (res, [], mempty)

203+ updateDags ((name, term@(P Bound name2 _)) : xs) (holes, args1, args2) | isJust findArgs = do

204+ ((ty1, ix1), (ty2, ix2)) <- findArgs

205+

206+ (res, queue, score) <- updateDags xs (holes', args1'', args2'')

207+ --traceShow (ty1, ty2) False `seq` return ()

208+ return $ (res, (ty1, ty2) : queue , score { transposition = transposition score + abs (ix2 - ix1) })

209+ where

210+ findArgs = ((,) <$> mgetType name args1 <*> mgetType name2 args2) <|>

211+ ((,) <$> mgetType name2 args1 <*> mgetType name args2)

212+ matchnames = [name, name2]

213+ holes' = holes \\ matchnames

214+ substf = deleteFromDag name . deleteFromDag name2

215+ args1' = substf args1

216+ args2' = substf args2

217+ args1'' = map (first . second $ subst name term) args1'

218+ args2'' = map (first . second $ subst name term) args2'

219+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs

220+

221+ updateDags ((name, term) : xs) (holes, args1, args2) = case (mgetType name args1, mgetType name args2) of

222+ (Just (_,ix), Nothing) -> thrd (\score -> score { leftApplied = succ (leftApplied score) }) <$> nextStep

223+ (Nothing, Just (_, ix)) -> thrd (\score -> score { rightApplied = succ (rightApplied score) }) <$> nextStep

224+ (Nothing, Nothing) -> nextStep

225+ _ -> error ("Shouldn't happen. Watch the alpha conversion!\n" ++ show args1 ++ "\n\n" ++ show args2)

226+ where

227+ varsInTy = map fst $ M.toList (usedVars term)

228+ deleteMany = foldr (.) id $ map deleteFromDag (name : varsInTy)

229+ thrd f (a,b,c) = (a,b,f c)

230+ nextStep = updateDags xs (holes \\ [name], updatef args1, updatef args2 )

231+ updatef = map (first . second $ subst name term) . deleteMany

232+ mgetType name xs = fmap ((snd . fst) &&& (fst . snd)) . find ((name ==) . fst . fst) $ xs

233+

234+

235+ go :: State -> [(Type, Type)] -> Maybe State

236+ --go (State holes args1 args2 score) queue | trace ("go\n\t" ++ show holes ++ "\n\t" ++ show args1 ++ "\n\t" ++ show args2 ++ "\n\t" ++ show queue) False = undefined

237+ go state [] = return state

238+ go (State holes args1 args2 score) ((ty1, ty2) : queue) = do

239+ res <- tcToMaybe $ match_unify ctxt [] ty1 ty2 [] holes []

240+ --trace ("UnifyResult: " ++ show (ty1, ty2, res, errors)) False `seq` return ()

241+ --guard (null errors)

242+ ((holes', args1', args2'), queueAdditions, scoreAdditions) <- updateDags res (holes, args1, args2)

243+ let newScore = score `mappend` scoreAdditions

244+ guard $ scoreCriterion newScore

245+ go (State holes' args1' args2' newScore) (queue ++ queueAdditions)

246+

247+

248+ processDags :: State -> [Score]

249+ processDags (State [] [] [] scoreAcc) = [scoreAcc]

250+ --processDags (State holes (_:_) [] scoreAcc) = []

251+ --processDags (State holes [] (_:_) scoreAcc) = []

252+ processDags (State holes dag1 dag2 scoreAcc) = concat [ processDags state | state <- allResults ] where

253+

254+ results = catMaybes [ go (State (holes \\ (map nameOf [ty1, ty2])) (deleteFromDag (nameOf ty1) dag1)

255+ (inArgTys (psubst (nameOf ty2) (P Bound (nameOf ty1) (typeOf ty1))) $ deleteFromDag (nameOf ty2) dag2) scoreAcc) [(typeOf ty1, typeOf ty2)]

256+ | ty1 <- canBeFirst dag1, ty2 <- canBeFirst dag2 {-, exactTypeEquality ctxt (typeOf ty1) (typeOf ty2) -} ]

257+

258+ results2 = [ State (holes \\ [nameOf ty])

259+ (deleteFromDag (nameOf ty) dag1) dag2

260+ (scoreAcc `mappend` (mempty { leftTypeClass = 1 }))

261+ | ty <- typeClassArgs1 ]

262+

263+ typeClassArgs1 = filter (isSaturatedClass . typeOf) dag1

264+ typeClassArgs2 = filter (isSaturatedClass . typeOf) dag2

265+

266+

267+ results3 = [ State (holes \\ [nameOf ty])

268+ dag1 (deleteFromDag (nameOf ty) dag2)

269+ (scoreAcc `mappend` (mempty { rightTypeClass = 1 }))

270+ | ty <- typeClassArgs2 ]

271+

272+ allResults :: [State]

273+ allResults = {- (if not (null typeClasses) then (traceShow typeClasses False `seq` id) else id ) -}

274+ (results ++ results2 ++ results3)

275+ where

276+ typeClasses = filter (isSaturatedClass . typeOf) (dag1 ++ dag2)

277+

278+

279+ -- check if the canBeFirst thing is losing any possibilities

280+

281+

282+ inArgTys = map . first . second

283+ typeOf ((name, ty), set) = ty

284+ nameOf ((name, ty), set) = name

285+

286+ -- XXX : debug stuff

287+ canBeFirst = if debugParam then filter (S.null . snd . snd) else id

288+ holes = map (fst . fst) dag1 ++ map (fst . fst) dag2

289+

290+ deleteIdx _ [] = []

291+ deleteIdx idx l@(x@(i,_,_) : xs) = if i == idx then xs else x : deleteIdx idx xs

292+

293+ isSaturatedClass :: Type -> Bool

294+ isSaturatedClass ty = fromMaybe False $ do

295+ className <- getClassName clss

296+ let possInstances = concatMap class_instances $ lookupCtxt className classInfo

297+ return $ (SN (sInstanceN className (map argToName args))) `elem` possInstances

298+ where

299+ (clss, args) = unApply ty

300+ getClassName (P (TCon _ _) className _) = Just className

301+ getClassName _ = Nothing

302+ argToName arg = show (delab istate arg)

303+

src/Pkg/PParser.hs+7−2

@@ -26,7 +26,8 @@ data PkgDesc = PkgDesc { pkgname :: String,

26 sourcedir :: String,

27 modules :: [Name],

28 idris_main :: Name,

29− execout :: Maybe String

29+ execout :: Maybe String,

30+ idris_tests :: [Name]

30 }

31 }

31 deriving Show

32 deriving Show

32

33

@@ -34,7 +35,7 @@ instance TokenParsing PParser where

34 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

35 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

35

36

37

37−defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing

38+defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing []

38

39

39parseDesc :: FilePath -> IO PkgDesc

40parseDesc :: FilePath -> IO PkgDesc

40parseDesc fp = do p <- readFile fp

41parseDesc fp = do p <- readFile fp

@@ -85,4 +86,8 @@ pClause = do reserved "executable"; lchar '=';

85 mk <- iName []

86 mk <- iName []

86 st <- get

87 st <- get

87 put (st { makefile = Just (show mk) })

88 put (st { makefile = Just (show mk) })

89+ <|> do reserved "tests"; lchar '=';

90+ ts <- sepBy1 (iName []) (lchar ',')

91+ st <- get

92+ put st { idris_tests = idris_tests st ++ ts }

88

93

src/Pkg/Package.hs+37−1

@@ -5,7 +5,7 @@ import System.Process

5import System.Directory

6import System.Exit

7import System.IO

8−import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory)

8+import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory, normalise)

9import System.Directory (createDirectoryIfMissing, copyFile)

10

11import Util.System

@@ -159,6 +159,42 @@ documentPkg fp =

159 Left msg -> do putStrLn msg

160 exitWith (ExitFailure 1)

161

162+-- | Build a package with a sythesized main function that runs the tests

163+testPkg :: FilePath -> IO ()

164+testPkg fp

165+ = do pkgdesc <- parseDesc fp

166+ ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)

167+ when (and ok) $

168+ do dir <- getCurrentDirectory

169+ setCurrentDirectory $ dir </> sourcedir pkgdesc

170+ make (makefile pkgdesc)

171+ -- Get a temporary file to save the tests' source in

172+ (tmpn, tmph) <- tempIdr

173+ hPutStrLn tmph $

174+ "module Test_______\n" ++

175+ concat ["import " ++ show m ++ "\n"

176+ | m <- modules pkgdesc] ++

177+ "namespace Main\n" ++

178+ " main : IO ()\n" ++

179+ " main = do " ++

180+ concat [show t ++ "\n "

181+ | t <- idris_tests pkgdesc]

182+ hClose tmph

183+ (tmpn', tmph') <- tempfile

184+ hClose tmph'

185+ m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)

186+ system tmpn'

187+ setCurrentDirectory dir

188+ case m_ist of

189+ Nothing -> exitWith (ExitFailure 1)

190+ Just ist -> do

191+ -- Quit with error code if problem building

192+ case errSpan ist of

193+ Just _ -> exitWith (ExitFailure 1)

194+ _ -> return ()

195+ where tempIdr :: IO (FilePath, Handle)

196+ tempIdr = do dir <- getTemporaryDirectory

197+ openTempFile (normalise dir) "idristests.idr"

162

198

163-- | Install package

199-- | Install package

164installPkg :: PkgDesc -> IO ()

200installPkg :: PkgDesc -> IO ()

test/basic006/expected+2−2

@@ -1,5 +1,5 @@

1−When elaborating right hand side of foo:

1+test020a.idr:14:18:When elaborating right hand side of foo:

2−test020a.idr:14:18:When elaborating an application of function Prelude.List.reverse:

2+When elaborating an application of function Prelude.List.reverse:

3 Can't unify

4 Vect n a

5 with

test/basic010/Main.idrnew file+43

@@ -0,0 +1,43 @@

1+module Main

2+

3+%default total

4+

5+-- An expensive function.

6+qib : Nat -> Nat

7+qib Z = 1

8+qib (S Z) = 2

9+qib (S (S n)) = qib n * qib (S n)

10+

11+-- An equality whose size reflects the size of numbers.

12+data equals : Nat -> Nat -> Type where

13+ eqZ : Z `equals` Z

14+ eqS : m `equals` n -> S m `equals` S n

15+

16+eq_refl : {n : Nat} -> n `equals` n

17+eq_refl {n = Z} = eqZ

18+eq_refl {n = S n} = eqS eq_refl

19+

20+-- Here, the proof is very expensive to compute.

21+-- We add a recursive argument to prevent Idris from inlining the function.

22+f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)

23+f Z n = element n eq_refl

24+f (S r) n = f r n

25+

26+-- A (contrived) relation, just to have something to show.

27+data represents : Nat -> Nat -> Type where

28+ axiom : (n : Nat) -> qib n `represents` n

29+

30+-- Here, the witness is very expensive to compute.

31+-- We add a recursive argument to prevent Idris from inlining the function.

32+g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)

33+g Z n = evidence (qib n) (axiom n)

34+g (S r) n = g r n

35+

36+fmt : qib n `represents` n -> String

37+fmt (axiom n) = "axiom " ++ show n

38+

39+main : IO ()

40+main = do

41+ n <- map (const 10000) (putStrLn "*oink*")

42+ putStrLn . show $ getWitness (f 4 n)

43+ putStrLn . fmt $ getProof (g 4 n)

test/basic010/expectednew file+3

@@ -0,0 +1,3 @@

1+*oink*

2+10000

3+axiom 10000

test/basic010/runnew file+35

@@ -0,0 +1,35 @@

1+#!/usr/bin/env bash

2+

3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting

4+# Here copied from reg039.

5+#

6+# Executes command with a timeout

7+# Params:

8+# $1 timeout in seconds

9+# $2 command

10+# Returns 1 if timed out 0 otherwise

11+timeout() {

12+

13+ time=$1

14+

15+ # start the command in a subshell to avoid problem with pipes

16+ # (spawn accepts one command)

17+ command="/bin/sh -c \"$2\""

18+

19+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

20+

21+ if [ $? = 1 ] ; then

22+ echo "Timeout after ${time} seconds"

23+ fi

24+

25+}

26+

27+declare -a extraargs

28+for arg in "$@"

29+do

30+ extraargs=("${extraargs[@]}" "'$arg'")

31+done

32+

33+timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"

34+timeout 5 "./basic010"

35+rm -f *.ibc basic010

test/reg014/reg014.idr+6−6

@@ -3,10 +3,10 @@ module reg014

3Matrix : Type -> Nat -> Nat -> Type

4Matrix a n m = Vect n (Vect m a)

5

6−transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

6+mytranspose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

7−transpose ((x:: []) :: []) = [[x]]

7+mytranspose ((x:: []) :: []) = [[x]]

8−transpose [x :: y :: xs] = [x] :: (transpose [y :: xs])

8+mytranspose [x :: y :: xs] = [x] :: (mytranspose [y :: xs])

9−transpose (x :: y :: xs)

9+mytranspose (x :: y :: xs)

10− = let tx = transpose [x] in

10+ = let tx = mytranspose [x] in

11− let ux = transpose (y :: xs) in zipWith (++) tx ux

11+ let ux = mytranspose (y :: xs) in zipWith (++) tx ux

12

test/reg030/reg030.idr+1−1

@@ -8,7 +8,7 @@ isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)

8

9class Set univ => HasPower univ where

10 Powerset : (a : univ) ->

11− Exists univ (\Pa => (c : univ) ->

11+ Sigma univ (\Pa => (c : univ) ->

12 (isSubsetOf c a) -> member c Pa)

13

14powerset : HasPower univ => univ -> univ

test/totality008/expectednew file+1

@@ -0,0 +1 @@

1+totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.c2

test/totality008/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ totality008.idr --check

3+rm -f *.ibc

test/totality008/totality008.idrnew file+8

@@ -0,0 +1,8 @@

1+ data T : Type -> Type where

2+ c1 : T Nat

3+ c2 : T (T Nat)

4+

5+total

6+ElimT : (A : Type) -> T A -> A

7+ElimT _ c1 = 3

8+ElimT _ c2 = c1