4833cb3 · Idris-dev · git.iko.soy

CHANGELOG+7

compare with master

unifiedsplit

@@ -1,6 +1,13 @@

1New in 0.9.14:

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

2* Tactic for case analysis in proofs

3* Tactic for case analysis in proofs

3* Induction and case tactic now work on expressions

4* Induction and case tactic now work on expressions

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

6+ --testpkg command-line option

7+* Clearly distinguish between type providers and postulate providers at the use site

8+* Allow dependent function syntax to be overridden in dsl blocks, similarly to

9+ functions and let. The keyword for this is "pi".

10+

4

11

5New in 0.9.13:

12New in 0.9.13:

6--------------

13--------------

CONTRIBUTORS+1

@@ -3,6 +3,7 @@ Thanks to the following for their help and contributions:

3Ozgur Akgun

4Ahmad Salim Al-Sibahi

5Edward Chadwick Amsden

6+Jan Bessai

6Nicola Botta

7Nicola Botta

7Edwin Brady

8Edwin Brady

8David Raymond Christiansen

9David Raymond Christiansen

config.mk+1−2

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

1CC ?=cc

2CABAL :=cabal

3−CFLAGS :=-O2 -Wall $(CFLAGS)

3+CFLAGS :=-O2 -Wall -DHAS_PTHREAD $(CFLAGS)

4#CABALFLAGS :=

5## Disable building of Effects

6#CABALFLAGS :=-f NoEffects

@@ -35,4 +35,3 @@ else

35 SHLIB_SUFFIX :=.so

36endif

37endif

38−

idris.cabal+11−2

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

1Name: idris

2−Version: 0.9.12

2+Version: 0.9.13.1

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -242,6 +242,9 @@ Extra-source-files:

242 test/reg044/run

243 test/reg044/*.idr

244 test/reg044/expected

245+ test/reg045/run

246+ test/reg045/*.idr

247+ test/reg045/expected

245

248

246 test/basic001/run

249 test/basic001/run

247 test/basic001/*.idr

250 test/basic001/*.idr

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

271 test/basic009/*.idr

274 test/basic009/*.idr

272 test/basic009/expected

275 test/basic009/expected

273 test/basic009/B/*.idr

276 test/basic009/B/*.idr

277+ test/basic010/run

278+ test/basic010/*.idr

279+ test/basic010/expected

274

280

275 test/buffer001-disabled/*.idr

281 test/buffer001-disabled/*.idr

276 test/buffer001-disabled/run

282 test/buffer001-disabled/run

@@ -283,6 +289,9 @@ Extra-source-files:

283 test/dsl002/test

289 test/dsl002/test

284 test/dsl002/*.idr

290 test/dsl002/*.idr

285 test/dsl002/expected

291 test/dsl002/expected

292+ test/dsl003/run

293+ test/dsl003/*.idr

294+ test/dsl003/expected

286

295

287 test/effects001/run

296 test/effects001/run

288 test/effects001/*.idr

297 test/effects001/*.idr

@@ -636,7 +645,7 @@ Library

636 , xml

645 , xml

637 , deepseq

646 , deepseq

638 , zlib

647 , zlib

639− , optparse-applicative

648+ , optparse-applicative >= 0.8

640 Extensions: MultiParamTypeClasses

649 Extensions: MultiParamTypeClasses

641 , FunctionalDependencies

650 , FunctionalDependencies

642 , FlexibleContexts

651 , FlexibleContexts

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/Providers.idr−9

@@ -11,26 +11,17 @@ data Provider : (a : Type) -> Type where

11 ||| @ msg the error message

12 Error : (msg : String) -> Provider a

13

14− ||| Postulate the goal type

15− Postulate : Provider a

16−

17-- instances

14-- instances

18instance Functor Provider where

15instance Functor Provider where

19 map f (Provide a) = Provide (f a)

16 map f (Provide a) = Provide (f a)

20 map f (Error err) = Error err

17 map f (Error err) = Error err

21− map f Postulate = Postulate

22

18

23instance Applicative Provider where

19instance Applicative Provider where

24 (Provide f) <$> (Provide x) = Provide (f x)

20 (Provide f) <$> (Provide x) = Provide (f x)

25 (Provide f) <$> (Error err) = Error err

21 (Provide f) <$> (Error err) = Error err

26− (Provide f) <$> Postulate = Postulate

27 (Error err) <$> _ = Error err

22 (Error err) <$> _ = Error err

28− Postulate <$> (Error err) = Error err

29− Postulate <$> _ = Postulate

30 pure = Provide

23 pure = Provide

31

24

32−-- is this correct for Postulate?

33instance Monad Provider where

25instance Monad Provider where

34 (Provide x) >>= f = f x

26 (Provide x) >>= f = f x

35 (Error err) >>= _ = Error err

27 (Error err) >>= _ = Error err

36− Postulate >>= f = Postulate

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/effects/Effect/File.idr+5−10

@@ -101,8 +101,7 @@ 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

@@ -111,23 +110,19 @@ 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 ()

116close = call $ Close

114close = 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

121readLine = call $ ReadLine

118readLine = 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 ()

126writeLine str = call $ WriteLine str

122writeLine 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

131eof = call $ EOF

126eof = call $ EOF

132

127

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

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

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

@@ -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 ()

43putStr 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 ()

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

55getStr = 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

59getChar = call $ GetCh

60

libs/prelude/Builtins.idr+3−11

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

@@ -47,7 +39,7 @@ data LazyType = LazyCodata | LazyEval

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

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

48 ||| A delayed computation.

40 ||| A delayed computation.

49 |||

41 |||

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

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

51 |||

43 |||

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

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

53 ||| @ 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+171−156

@@ -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,73 +61,76 @@ 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

102class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

106class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

103 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

107 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

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) <+> (c <*> r)

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

@@ -579,6 +579,9 @@ isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

579isSuffixOf : Eq a => List a -> List a -> Bool

580isSuffixOf = isSuffixOfBy (==)

581

582+isInfixOf : Eq a => List a -> List a -> Bool

583+isInfixOf n h = any (isPrefixOf n) (tails h)

584+

582--------------------------------------------------------------------------------

585--------------------------------------------------------------------------------

583-- Sorting

586-- Sorting

584--------------------------------------------------------------------------------

587--------------------------------------------------------------------------------

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/Strings.idr+5−1

@@ -218,9 +218,13 @@ lines s = map pack $ lines' $ unpack s

218

219partial

220foldr1 : (a -> a -> a) -> List a -> a

221−foldr1 f [x] = x

221+foldr1 _ [x] = x

222foldr1 f (x::xs) = f x (foldr1 f xs)

223

224+partial

225+foldl1 : (a -> a -> a) -> List a -> a

226+foldl1 f (x::xs) = foldl f x xs

227+

224||| Joins the character lists by spaces into a single character list.

228||| Joins the character lists by spaces into a single character list.

225|||

229|||

226||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]

230||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]

libs/prelude/Prelude/Vect.idr+4−1

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

260concat [] = []

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

262

263−||| Fold without seeding the accumulator

263+||| Foldr without seeding the accumulator

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

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

266

267+||| Foldl without seeding the accumulator

268+foldl1 : (t -> t -> t) -> Vect (S n) t -> t

269+foldl1 f (x::xs) = foldl f x xs

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

270--------------------------------------------------------------------------------

268-- Scans

271-- Scans

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

272--------------------------------------------------------------------------------

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/idris_gc.c+11−2

@@ -103,7 +103,14 @@ void idris_gc(VM* vm) {

103 free(vm->heap.old);

104

105 vm->heap.heap = newheap;

106+#ifdef FORCE_ALIGNMENT

107+ if (((i_int)(vm->heap.heap)&1) == 1) {

106− vm->heap.next = newheap;

108+ vm->heap.next = newheap + 1;

109+ } else

110+#endif

111+ {

112+ vm->heap.next = newheap;

113+ }

107 vm->heap.end = newheap + vm->heap.size;

114 vm->heap.end = newheap + vm->heap.size;

108

115

109 VAL* root;

116 VAL* root;

@@ -111,10 +118,12 @@ void idris_gc(VM* vm) {

111 for(root = vm->valstack; root < vm->valstack_top; ++root) {

118 for(root = vm->valstack; root < vm->valstack_top; ++root) {

112 *root = copy(vm, *root);

119 *root = copy(vm, *root);

113 }

120 }

121+

122+#ifdef HAS_PTHREAD

114 for(root = vm->inbox_ptr; root < vm->inbox_write; ++root) {

123 for(root = vm->inbox_ptr; root < vm->inbox_write; ++root) {

115 *root = copy(vm, *root);

124 *root = copy(vm, *root);

116 }

125 }

117−

126+#endif

118 vm->ret = copy(vm, vm->ret);

127 vm->ret = copy(vm, vm->ret);

119 vm->reg1 = copy(vm, vm->reg1);

128 vm->reg1 = copy(vm, vm->reg1);

120

129

rts/idris_heap.c+8−1

@@ -16,7 +16,14 @@ void alloc_heap(Heap * h, size_t heap_size)

16 }

17

18 h->heap = mem;

19+#ifdef FORCE_ALIGNMENT

20+ if (((i_int)(h->heap)&1) == 1) {

19− h->next = h->heap;

21+ h->next = h->heap + 1;

22+ } else

23+#endif

24+ {

25+ h->next = h->heap;

26+ }

20 h->end = h->heap + heap_size;

27 h->end = h->heap + heap_size;

21

28

22 h->size = heap_size;

29 h->size = heap_size;

rts/idris_rts.c+23−11

@@ -1,10 +1,11 @@

1#include <stdlib.h>

2#include <stdio.h>

3#include <string.h>

4−#include <unistd.h>

5#include <stdarg.h>

4#include <stdarg.h>

6#include <assert.h>

5#include <assert.h>

6+#ifdef HAS_PTHREAD

7#include <pthread.h>

8+#endif

8

9

9#include "idris_rts.h"

10#include "idris_rts.h"

10#include "idris_gc.h"

11#include "idris_gc.h"

@@ -30,7 +31,7 @@ VM* init_vm(int stack_size, size_t heap_size,

30

31

31 vm->ret = NULL;

32 vm->ret = NULL;

32 vm->reg1 = NULL;

33 vm->reg1 = NULL;

33−

34+#ifdef HAS_PTHREAD

34 vm->inbox = malloc(1024*sizeof(VAL));

35 vm->inbox = malloc(1024*sizeof(VAL));

35 memset(vm->inbox, 0, 1024*sizeof(VAL));

36 memset(vm->inbox, 0, 1024*sizeof(VAL));

36 vm->inbox_end = vm->inbox + 1024;

37 vm->inbox_end = vm->inbox + 1024;

@@ -53,7 +54,7 @@ VM* init_vm(int stack_size, size_t heap_size,

53

54

54 vm->max_threads = max_threads;

55 vm->max_threads = max_threads;

55 vm->processes = 0;

56 vm->processes = 0;

56−

57+#endif

57 STATS_LEAVE_INIT(vm->stats)

58 STATS_LEAVE_INIT(vm->stats)

58 return vm;

59 return vm;

59}

60}

@@ -61,14 +62,16 @@ VM* init_vm(int stack_size, size_t heap_size,

61Stats terminate(VM* vm) {

62Stats terminate(VM* vm) {

62 Stats stats = vm->stats;

63 Stats stats = vm->stats;

63 STATS_ENTER_EXIT(stats)

64 STATS_ENTER_EXIT(stats)

64−

65+#ifdef HAS_PTHREAD

65 free(vm->inbox);

66 free(vm->inbox);

67+#endif

66 free(vm->valstack);

68 free(vm->valstack);

67 free_heap(&(vm->heap));

69 free_heap(&(vm->heap));

68−

70+#ifdef HAS_PTHREAD

69 pthread_mutex_destroy(&(vm -> inbox_lock));

71 pthread_mutex_destroy(&(vm -> inbox_lock));

70 pthread_mutex_destroy(&(vm -> inbox_block));

72 pthread_mutex_destroy(&(vm -> inbox_block));

71 pthread_cond_destroy(&(vm -> inbox_waiting));

73 pthread_cond_destroy(&(vm -> inbox_waiting));

74+#endif

72 free(vm);

75 free(vm);

73

76

74 STATS_LEAVE_EXIT(stats)

77 STATS_LEAVE_EXIT(stats)

@@ -79,18 +82,21 @@ void idris_requireAlloc(VM* vm, size_t size) {

79 if (!(vm->heap.next + size < vm->heap.end)) {

82 if (!(vm->heap.next + size < vm->heap.end)) {

80 idris_gc(vm);

83 idris_gc(vm);

81 }

84 }

82−

85+#ifdef HAS_PTHREAD

83 int lock = vm->processes > 0;

86 int lock = vm->processes > 0;

84 if (lock) { // We only need to lock if we're in concurrent mode

87 if (lock) { // We only need to lock if we're in concurrent mode

85 pthread_mutex_lock(&vm->alloc_lock);

88 pthread_mutex_lock(&vm->alloc_lock);

86 }

89 }

90+#endif

87}

91}

88

92

89void idris_doneAlloc(VM* vm) {

93void idris_doneAlloc(VM* vm) {

94+#ifdef HAS_PTHREAD

90 int lock = vm->processes > 0;

95 int lock = vm->processes > 0;

91 if (lock) { // We only need to lock if we're in concurrent mode

96 if (lock) { // We only need to lock if we're in concurrent mode

92 pthread_mutex_unlock(&vm->alloc_lock);

97 pthread_mutex_unlock(&vm->alloc_lock);

93 }

98 }

99+#endif

94}

100}

95

101

96int space(VM* vm, size_t size) {

102int space(VM* vm, size_t size) {

@@ -99,16 +105,18 @@ int space(VM* vm, size_t size) {

99

105

100void* allocate(VM* vm, size_t size, int outerlock) {

106void* allocate(VM* vm, size_t size, int outerlock) {

101// return malloc(size);

107// return malloc(size);

108+#ifdef HAS_PTHREAD

102 int lock = vm->processes > 0 && !outerlock;

109 int lock = vm->processes > 0 && !outerlock;

103

110

104 if (lock) { // not message passing

111 if (lock) { // not message passing

105 pthread_mutex_lock(&vm->alloc_lock);

112 pthread_mutex_lock(&vm->alloc_lock);

106 }

113 }

114+#endif

107

115

108 if ((size & 7)!=0) {

116 if ((size & 7)!=0) {

109 size = 8 + ((size >> 3) << 3);

117 size = 8 + ((size >> 3) << 3);

110 }

118 }

111−

119+

112 size_t chunk_size = size + sizeof(size_t);

120 size_t chunk_size = size + sizeof(size_t);

113

121

114 if (vm->heap.next + chunk_size < vm->heap.end) {

122 if (vm->heap.next + chunk_size < vm->heap.end) {

@@ -120,16 +128,19 @@ void* allocate(VM* vm, size_t size, int outerlock) {

120 assert(vm->heap.next <= vm->heap.end);

128 assert(vm->heap.next <= vm->heap.end);

121

129

122 memset(ptr, 0, size);

130 memset(ptr, 0, size);

123−

131+#ifdef HAS_PTHREAD

124 if (lock) { // not message passing

132 if (lock) { // not message passing

125 pthread_mutex_unlock(&vm->alloc_lock);

133 pthread_mutex_unlock(&vm->alloc_lock);

126 }

134 }

135+#endif

127 return ptr;

136 return ptr;

128 } else {

137 } else {

129 idris_gc(vm);

138 idris_gc(vm);

139+#ifdef HAS_PTHREAD

130 if (lock) { // not message passing

140 if (lock) { // not message passing

131 pthread_mutex_unlock(&vm->alloc_lock);

141 pthread_mutex_unlock(&vm->alloc_lock);

132 }

142 }

143+#endif

133 return allocate(vm, size, 0);

144 return allocate(vm, size, 0);

134 }

145 }

135

146

@@ -187,7 +198,7 @@ VAL MKPTR(VM* vm, void* ptr) {

187 return cl;

198 return cl;

188}

199}

189

200

190−VAL MKMPTR(VM* vm, void* ptr, int size) {

201+VAL MKMPTR(VM* vm, void* ptr, size_t size) {

191 Closure* cl = allocate(vm, sizeof(Closure) +

202 Closure* cl = allocate(vm, sizeof(Closure) +

192 sizeof(ManagedPtr) + size, 0);

203 sizeof(ManagedPtr) + size, 0);

193 SETTY(cl, MANAGEDPTR);

204 SETTY(cl, MANAGEDPTR);

@@ -222,7 +233,7 @@ VAL MKPTRc(VM* vm, void* ptr) {

222 return cl;

233 return cl;

223}

234}

224

235

225−VAL MKMPTRc(VM* vm, void* ptr, int size) {

236+VAL MKMPTRc(VM* vm, void* ptr, size_t size) {

226 Closure* cl = allocate(vm, sizeof(Closure) +

237 Closure* cl = allocate(vm, sizeof(Closure) +

227 sizeof(ManagedPtr) + size, 1);

238 sizeof(ManagedPtr) + size, 1);

228 SETTY(cl, MANAGEDPTR);

239 SETTY(cl, MANAGEDPTR);

@@ -760,6 +771,7 @@ typedef struct {

760 VAL arg;

771 VAL arg;

761} ThreadData;

772} ThreadData;

762

773

774+#ifdef HAS_PTHREAD

763void* runThread(void* arg) {

775void* runThread(void* arg) {

764 ThreadData* td = (ThreadData*)arg;

776 ThreadData* td = (ThreadData*)arg;

765 VM* vm = td->vm;

777 VM* vm = td->vm;

@@ -949,7 +961,7 @@ VAL idris_recvMessage(VM* vm) {

949

961

950 return msg;

962 return msg;

951}

963}

952−

964+#endif

953int __idris_argc;

965int __idris_argc;

954char **__idris_argv;

966char **__idris_argv;

955

967

rts/idris_rts.h+13−9

@@ -4,9 +4,10 @@

4#include <stdlib.h>

5#include <stdio.h>

6#include <string.h>

7−#include <unistd.h>

8#include <stdarg.h>

7#include <stdarg.h>

8+#ifdef HAS_PTHREAD

9#include <pthread.h>

10+#endif

10#include <stdint.h>

11#include <stdint.h>

11

12

12#include "idris_heap.h"

13#include "idris_heap.h"

@@ -23,13 +24,13 @@ typedef enum {

23typedef struct Closure *VAL;

24typedef struct Closure *VAL;

24

25

25typedef struct {

26typedef struct {

26− int tag_arity;

27+ uint32_t tag_arity;

27 VAL args[];

28 VAL args[];

28} con;

29} con;

29

30

30typedef struct {

31typedef struct {

31 VAL str;

32 VAL str;

32− int offset;

33+ size_t offset;

33} StrOffset;

34} StrOffset;

34

35

35typedef struct {

36typedef struct {

@@ -49,7 +50,10 @@ typedef struct {

49typedef struct Closure {

50typedef struct Closure {

50// Use top 16 bits of ty for saying which heap value is in

51// Use top 16 bits of ty for saying which heap value is in

51// Bottom 16 bits for closure type

52// Bottom 16 bits for closure type

52− ClosureType ty;

53+//

54+// NOTE: ty can not have type ClosureType because ty must be a

55+// uint32_t but enum is platform dependent

56+ uint32_t ty;

53 union {

57 union {

54 con c;

58 con c;

55 int i;

59 int i;

@@ -73,7 +77,7 @@ typedef struct {

73 VAL* stack_max;

77 VAL* stack_max;

74

78

75 Heap heap;

79 Heap heap;

76−

80+#ifdef HAS_PTHREAD

77 pthread_mutex_t inbox_lock;

81 pthread_mutex_t inbox_lock;

78 pthread_mutex_t inbox_block;

82 pthread_mutex_t inbox_block;

79 pthread_mutex_t alloc_lock;

83 pthread_mutex_t alloc_lock;

@@ -87,7 +91,7 @@ typedef struct {

87

91

88 int processes; // Number of child processes

92 int processes; // Number of child processes

89 int max_threads; // maximum number of threads to run in parallel

93 int max_threads; // maximum number of threads to run in parallel

90−

94+#endif

91 Stats stats;

95 Stats stats;

92

96

93 VAL ret;

97 VAL ret;

@@ -170,7 +174,7 @@ typedef intptr_t i_int;

170VAL MKFLOAT(VM* vm, double val);

174VAL MKFLOAT(VM* vm, double val);

171VAL MKSTR(VM* vm, const char* str);

175VAL MKSTR(VM* vm, const char* str);

172VAL MKPTR(VM* vm, void* ptr);

176VAL MKPTR(VM* vm, void* ptr);

173−VAL MKMPTR(VM* vm, void* ptr, int size);

177+VAL MKMPTR(VM* vm, void* ptr, size_t size);

174VAL MKB8(VM* vm, uint8_t b);

178VAL MKB8(VM* vm, uint8_t b);

175VAL MKB16(VM* vm, uint16_t b);

179VAL MKB16(VM* vm, uint16_t b);

176VAL MKB32(VM* vm, uint32_t b);

180VAL MKB32(VM* vm, uint32_t b);

@@ -181,7 +185,7 @@ VAL MKFLOATc(VM* vm, double val);

181VAL MKSTROFFc(VM* vm, StrOffset* off);

185VAL MKSTROFFc(VM* vm, StrOffset* off);

182VAL MKSTRc(VM* vm, char* str);

186VAL MKSTRc(VM* vm, char* str);

183VAL MKPTRc(VM* vm, void* ptr);

187VAL MKPTRc(VM* vm, void* ptr);

184−VAL MKMPTRc(VM* vm, void* ptr, int size);

188+VAL MKMPTRc(VM* vm, void* ptr, size_t size);

185VAL MKBUFFERc(VM* vm, Buffer* buf);

189VAL MKBUFFERc(VM* vm, Buffer* buf);

186

190

187char* GETSTROFF(VAL stroff);

191char* GETSTROFF(VAL stroff);

@@ -208,7 +212,7 @@ void idris_doneAlloc(VM* vm);

208#define allocCon(cl, vm, t, a, o) \

212#define allocCon(cl, vm, t, a, o) \

209 cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*a, o); \

213 cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*a, o); \

210 SETTY(cl, CON); \

214 SETTY(cl, CON); \

211− cl->info.c.tag_arity = ((t) << 8) + (a);

215+ cl->info.c.tag_arity = ((t) << 8) | (a);

212

216

213void* vmThread(VM* callvm, func f, VAL arg);

217void* vmThread(VM* callvm, func f, VAL arg);

214

218

src/IRTS/CodegenJava.hs+8−5

@@ -169,7 +169,7 @@ jarHeader =

169 ++ "if test -n \"$JAVA_HOME\"; then\n"

170 ++ " java=\"$JAVA_HOME/bin/java\"\n"

171 ++ "fi\n"

172− ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\""

172+ ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\"\n"

173 ++ "exit 1\n"

174

175-----------------------------------------------------------------------

@@ -312,6 +312,7 @@ mkCompilationUnit globalInit defs hdrs out = do

312 , ImportDecl True idrisPrelude True

313 , ImportDecl False bigInteger False

314 , ImportDecl False runtimeException False

315+ , ImportDecl False byteBuffer False

315 ] ++ otherHdrs

316 ] ++ otherHdrs

316 )

317 )

317 <$> mkTypeDecl clsName globalInit defs

318 <$> mkTypeDecl clsName globalInit defs

@@ -320,6 +321,7 @@ mkCompilationUnit globalInit defs hdrs out = do

320 idrisPrelude = J.Name $ map Ident ["org", "idris", "rts", "Prelude"]

321 idrisPrelude = J.Name $ map Ident ["org", "idris", "rts", "Prelude"]

321 bigInteger = J.Name $ map Ident ["java", "math", "BigInteger"]

322 bigInteger = J.Name $ map Ident ["java", "math", "BigInteger"]

322 runtimeException = J.Name $ map Ident ["java", "lang", "RuntimeException"]

323 runtimeException = J.Name $ map Ident ["java", "lang", "RuntimeException"]

324+ byteBuffer = J.Name $ map Ident ["java", "nio", "ByteBuffer"]

323 otherHdrs = map ( (\ name -> ImportDecl False name False)

325 otherHdrs = map ( (\ name -> ImportDecl False name False)

324 . J.Name

326 . J.Name

325 . map (Ident . T.unpack)

327 . map (Ident . T.unpack)

@@ -386,9 +388,7 @@ mkMainMethod =

386 "main"

388 "main"

387 [FormalParam [] (array stringType) False (VarId $ Ident "args")]

389 [FormalParam [] (array stringType) False (VarId $ Ident "args")]

388 $ Block [ BlockStmt . ExpStmt

390 $ Block [ BlockStmt . ExpStmt

389− $ call "idris_initArgs" [ (threadType ~> "currentThread") []

391+ $ call "idris_initArgs" [ jConst "args" ]

390− , jConst "args"

391− ]

392 , BlockStmt . ExpStmt $ call (mangle' (sMN 0 "runMain")) []

393 ]

394

@@ -484,6 +484,8 @@ mkExp pp (SOp LFork [arg]) =

484 (mkThread arg) >>= ppExp pp

485mkExp pp (SOp LPar [arg]) =

486 (Nothing <>@! arg) >>= ppExp pp

487+mkExp pp (SOp LRegisterPtr [ptr, i]) =

488+ (Nothing <>@! ptr) >>= ppExp pp

487mkExp pp (SOp LNoOp args) =

489mkExp pp (SOp LNoOp args) =

488 (Nothing <>@! (last args)) >>= ppExp pp

490 (Nothing <>@! (last args)) >>= ppExp pp

489mkExp pp (SOp LNullPtr args) =

491mkExp pp (SOp LNullPtr args) =

@@ -707,6 +709,7 @@ mkConstant c@(AType x) = ClassLit (Just $ box (constType c))

707mkConstant c@(StrType ) = ClassLit (Just $ stringType)

709mkConstant c@(StrType ) = ClassLit (Just $ stringType)

708mkConstant c@(PtrType ) = ClassLit (Just $ objectType)

710mkConstant c@(PtrType ) = ClassLit (Just $ objectType)

709mkConstant c@(ManagedPtrType) = ClassLit (Just $ objectType)

711mkConstant c@(ManagedPtrType) = ClassLit (Just $ objectType)

712+mkConstant c@(BufferType) = ClassLit (Just $ bufferType)

710mkConstant c@(VoidType ) = ClassLit (Just $ voidType)

713mkConstant c@(VoidType ) = ClassLit (Just $ voidType)

711mkConstant c@(Forgot ) = ClassLit (Just $ objectType)

714mkConstant c@(Forgot ) = ClassLit (Just $ objectType)

712

715

@@ -744,7 +747,7 @@ mkForeign pp (LANG_JAVA callType) resTy text params

744

747

745mkPrimitiveFunction :: PrimFn -> [LVar] -> CodeGeneration Exp

748mkPrimitiveFunction :: PrimFn -> [LVar] -> CodeGeneration Exp

746mkPrimitiveFunction op args =

749mkPrimitiveFunction op args =

747− (\ args -> (primFnType ~> opName op) args)

750+ (\ args -> (primFnType ~> opName op) (endiannessArguments op ++ args))

748 <$> sequence (zipWith (\ a t -> (Just t) <>@! a) args (sourceTypes op))

751 <$> sequence (zipWith (\ a t -> (Just t) <>@! a) args (sourceTypes op))

749

752

750mkThread :: LVar -> CodeGeneration Exp

753mkThread :: LVar -> CodeGeneration Exp

src/IRTS/Java/JTypes.hs+31

@@ -33,6 +33,9 @@ doubleType = PrimType DoubleT

33array :: J.Type -> J.Type

34array t = RefType . ArrayType $ t

35

36+addressType :: J.Type

37+addressType = longType

38+

36-----------------------------------------------------------------------

39-----------------------------------------------------------------------

37-- Boxed types

40-- Boxed types

38

41

@@ -48,6 +51,10 @@ stringType :: J.Type

48stringType =

51stringType =

49 RefType . ClassRefType $ ClassType [(Ident "String", [])]

52 RefType . ClassRefType $ ClassType [(Ident "String", [])]

50

53

54+bufferType :: J.Type

55+bufferType =

56+ RefType . ClassRefType $ ClassType [(Ident "ByteBuffer", [])]

57+

51threadType :: J.Type

58threadType :: J.Type

52threadType =

59threadType =

53 RefType . ClassRefType $ ClassType [(Ident "Thread", [])]

60 RefType . ClassRefType $ ClassType [(Ident "Thread", [])]

@@ -132,6 +139,9 @@ runtimeExceptionType :: J.Type

132runtimeExceptionType =

139runtimeExceptionType =

133 RefType . ClassRefType $ ClassType [(Ident "RuntimeException", [])]

140 RefType . ClassRefType $ ClassType [(Ident "RuntimeException", [])]

134

141

142+-----------------------------------------------------------------------

143+-- Integer types

144+

135nativeTyToJType :: NativeTy -> J.Type

145nativeTyToJType :: NativeTy -> J.Type

136nativeTyToJType IT8 = byteType

146nativeTyToJType IT8 = byteType

137nativeTyToJType IT16 = shortType

147nativeTyToJType IT16 = shortType

@@ -219,6 +229,7 @@ opName x

219 | (LFloatInt to) <- x = "LFloatInt" ++ (suffixFor to)

229 | (LFloatInt to) <- x = "LFloatInt" ++ (suffixFor to)

220 | (LStrInt to) <- x = "LStrInt" ++ (suffixFor to)

230 | (LStrInt to) <- x = "LStrInt" ++ (suffixFor to)

221 | (LChInt to) <- x = "LChInt" ++ (suffixFor to)

231 | (LChInt to) <- x = "LChInt" ++ (suffixFor to)

232+ | (LPeek to _) <- x = "LPeek" ++ (suffixFor to)

222 | otherwise = takeWhile ((/=) ' ') $ show x

233 | otherwise = takeWhile ((/=) ' ') $ show x

223 where

234 where

224 suffixFor (ITFixed nt) = show nt

235 suffixFor (ITFixed nt) = show nt

@@ -291,10 +302,30 @@ sourceTypes (LStrRev) = [stringType]

291sourceTypes (LStdIn) = []

302sourceTypes (LStdIn) = []

292sourceTypes (LStdOut) = []

303sourceTypes (LStdOut) = []

293sourceTypes (LStdErr) = []

304sourceTypes (LStdErr) = []

305+sourceTypes (LAllocate) = [addressType]

306+sourceTypes (LAppendBuffer) =

307+ [bufferType, addressType, addressType, addressType, addressType, bufferType]

308+sourceTypes (LSystemInfo) = [integerType]

309+sourceTypes (LAppend nt _) = [bufferType, addressType, addressType, intTyToJType nt]

310+sourceTypes (LPeek _ _) = [bufferType, addressType]

294sourceTypes (LFork) = [objectType]

311sourceTypes (LFork) = [objectType]

295sourceTypes (LPar) = [objectType]

312sourceTypes (LPar) = [objectType]

296sourceTypes (LVMPtr) = []

313sourceTypes (LVMPtr) = []

297sourceTypes (LNullPtr) = [objectType]

314sourceTypes (LNullPtr) = [objectType]

298sourceTypes (LNoOp) = repeat objectType

315sourceTypes (LNoOp) = repeat objectType

299

316

317+-----------------------------------------------------------------------

318+-- Endianess markers

300

319

320+endiannessConstant :: Endianness -> Exp

321+endiannessConstant c =

322+ ExpName . Name . map Ident $ ["java", "nio", "ByteOrder", endiannessConstant' c]

323+ where

324+ endiannessConstant' BE = "BIG_ENDIAN"

325+ endiannessConstant' LE = "LITTLE_ENDIAN"

326+ endiannessConstant' (IRTS.Lang.Native) = endiannessConstant' BE

327+

328+endiannessArguments :: PrimFn -> [Exp]

329+endiannessArguments (LAppend _ end) = [endiannessConstant end]

330+endiannessArguments (LPeek _ end) = [endiannessConstant end]

331+endiannessArguments _ = []

src/IRTS/Java/Pom.hs+7−1

@@ -3,6 +3,9 @@ module IRTS.Java.Pom (pomString) where

3import Data.List (unfoldr)

4import Text.XML.Light

5

6+-----------------------------------------------------------------------

7+-- String <-> XML processing

8+

6uattr :: String -> String -> Attr

9uattr :: String -> String -> Attr

7uattr k v = Attr (QName k Nothing Nothing) v

10uattr k v = Attr (QName k Nothing Nothing) v

8

11

@@ -31,6 +34,9 @@ groupArtifactVersion g a v = [

31pomString :: String -> String -> [String] -> String

34pomString :: String -> String -> [String] -> String

32pomString c a d = ppElement $ pom c a d

35pomString c a d = ppElement $ pom c a d

33

36

37+-----------------------------------------------------------------------

38+-- The pom template for idris projects

39+

34pom :: String -> String -> [String] -> Element

40pom :: String -> String -> [String] -> Element

35pom clsName artifactName dependencies = unode "project" ([

41pom clsName artifactName dependencies = unode "project" ([

36 uattr "xmlns" "http://maven.apache.org/POM/4.0.0",

42 uattr "xmlns" "http://maven.apache.org/POM/4.0.0",

@@ -49,7 +55,7 @@ pom clsName artifactName dependencies = unode "project" ([

49 unode "skipTest" "true"

55 unode "skipTest" "true"

50 ],

56 ],

51 unode "dependencies" (

57 unode "dependencies" (

52− dependency "org.idris-lang" "idris" "0.9.10-alpha-2" :

58+ dependency "org.idris-lang" "idris" "0.9.14" :

53 map parseToDep dependencies

59 map parseToDep dependencies

54 ),

60 ),

55 unode "build" [

61 unode "build" [

src/Idris/AbsSyntax.hs+9−8

@@ -278,7 +278,7 @@ addNameHint ty n

278 ty' <- case lookupCtxtName ty (idris_implicits i) of

279 [(tyn, _)] -> return tyn

280 [] -> throwError (NoSuchVariable ty)

281− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))

281+ tyns -> throwError (CantResolveAlts (map fst tyns))

282 let ns' = case lookupCtxt ty' (idris_namehints i) of

283 [ns] -> ns ++ [n]

284 _ -> [n]

@@ -778,13 +778,14 @@ setColour :: ColourType -> IdrisColour -> Idris ()

778setColour ct c = do i <- getIState

779 let newTheme = setColour' ct c (idris_colourTheme i)

780 putIState $ i { idris_colourTheme = newTheme }

781− where setColour' KeywordColour c t = t { keywordColour = c }

781+ where setColour' KeywordColour c t = t { keywordColour = c }

782− setColour' BoundVarColour c t = t { boundVarColour = c }

782+ setColour' BoundVarColour c t = t { boundVarColour = c }

783− setColour' ImplicitColour c t = t { implicitColour = c }

783+ setColour' ImplicitColour c t = t { implicitColour = c }

784− setColour' FunctionColour c t = t { functionColour = c }

784+ setColour' FunctionColour c t = t { functionColour = c }

785− setColour' TypeColour c t = t { typeColour = c }

785+ setColour' TypeColour c t = t { typeColour = c }

786− setColour' DataColour c t = t { dataColour = c }

786+ setColour' DataColour c t = t { dataColour = c }

787− setColour' PromptColour c t = t { promptColour = c }

787+ setColour' PromptColour c t = t { promptColour = c }

788+ setColour' PostulateColour c t = t { postulateColour = c }

788

789

789logLvl :: Int -> String -> Idris ()

790logLvl :: Int -> String -> Idris ()

790logLvl l str = do i <- getIState

791logLvl l str = do i <- getIState

src/Idris/AbsSyntaxTree.hs+25−18

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

@@ -493,10 +494,11 @@ data DataOpt = Codata -- ^ Set if the the data-type is coinductive

493type DataOpts = [DataOpt]

494type DataOpts = [DataOpt]

494

495

495-- | Type provider - what to provide

496-- | Type provider - what to provide

496−data ProvideWhat = ProvTerm -- ^ only allow providing terms

497+data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

497− | ProvPostulate -- ^ only allow postulates

498+ | ProvPostulate t -- ^ goal type must be Type, so only term

498− | ProvAny -- ^ either is ok

499− deriving (Show, Eq)

499+ deriving (Show, Eq, Functor)

500+

501+type ProvideWhat = ProvideWhat' PTerm

500

502

501-- | Top-level declarations such as compiler directives, definitions,

503-- | Top-level declarations such as compiler directives, definitions,

502-- datatypes and typeclasses.

504-- datatypes and typeclasses.

@@ -530,7 +532,7 @@ data PDecl' t

530 | PSyntax FC Syntax -- ^ Syntax definition

532 | PSyntax FC Syntax -- ^ Syntax definition

531 | PMutual FC [PDecl' t] -- ^ Mutual block

533 | PMutual FC [PDecl' t] -- ^ Mutual block

532 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

534 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

533− | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term

535+ | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

534 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

536 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

535 -- bool is True, lhs and rhs must be convertible

537 -- bool is True, lhs and rhs must be convertible

536 deriving Functor

538 deriving Functor

@@ -904,7 +906,8 @@ data DSL' t = DSL { dsl_bind :: t,

904 index_first :: Maybe t,

906 index_first :: Maybe t,

905 index_next :: Maybe t,

907 index_next :: Maybe t,

906 dsl_lambda :: Maybe t,

908 dsl_lambda :: Maybe t,

907− dsl_let :: Maybe t

909+ dsl_let :: Maybe t,

910+ dsl_pi :: Maybe t

908 }

911 }

909 deriving (Show, Functor)

912 deriving (Show, Functor)

910{-!

913{-!

@@ -948,6 +951,7 @@ initDSL = DSL (PRef f (sUN ">>="))

948 Nothing

951 Nothing

949 Nothing

952 Nothing

950 Nothing

953 Nothing

954+ Nothing

951 where f = fileFC "(builtin)"

955 where f = fileFC "(builtin)"

952

956

953data Using = UImplicit Name PTerm

957data Using = UImplicit Name PTerm

@@ -1102,8 +1106,8 @@ elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defau

1102 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1106 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1103

1107

1104-- Defined in builtins.idr

1108-- Defined in builtins.idr

1105−sigmaTy = sUN "Exists"

1109+sigmaTy = sUN "Sigma"

1106−existsCon = sUN "Ex_intro"

1110+existsCon = sUN "Sg_intro"

1107

1111

1108piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1112piBind :: [(Name, PTerm)] -> PTerm -> PTerm

1109piBind = piBindp expl

1113piBind = piBindp expl

@@ -1150,18 +1154,22 @@ consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1150consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist

1154consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist

1151 theme = idris_colourTheme ist

1155 theme = idris_colourTheme ist

1152 in case () of

1156 in case () of

1153− _ | isDConName n ctxt -> colouriseData theme

1157+ _ | isDConName n ctxt -> colouriseData theme

1154− _ | isFnName n ctxt -> colouriseFun theme

1158+ _ | isFnName n ctxt -> colouriseFun theme

1155− _ | isTConName n ctxt -> colouriseType theme

1159+ _ | isTConName n ctxt -> colouriseType theme

1160+ _ | isPostulateName n ist -> colourisePostulate theme

1156− _ | otherwise -> id -- don't colourise unknown names

1161+ _ | otherwise -> id -- don't colourise unknown names

1157consoleDecorate ist (AnnFC _) = id

1162consoleDecorate ist (AnnFC _) = id

1158consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1163consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1159 where colour BoldText = IdrisColour Nothing True False True False

1164 where colour BoldText = IdrisColour Nothing True False True False

1160 colour UnderlineText = IdrisColour Nothing True True False False

1165 colour UnderlineText = IdrisColour Nothing True True False False

1161 colour ItalicText = IdrisColour Nothing True False False True

1166 colour ItalicText = IdrisColour Nothing True False False True

1162

1167

1168+isPostulateName :: Name -> IState -> Bool

1169+isPostulateName n ist = S.member n (idris_postulates ist)

1170+

1163-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1171-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1164−prettyImp :: PPOption -- ^^ pretty printing options

1172+prettyImp :: PPOption -- ^^ pretty printing options

1165 -> PTerm -- ^^ the term to pretty-print

1173 -> PTerm -- ^^ the term to pretty-print

1166 -> Doc OutputAnnotation

1174 -> Doc OutputAnnotation

1167prettyImp impl = pprintPTerm impl [] [] []

1175prettyImp impl = pprintPTerm impl [] [] []

@@ -1171,7 +1179,7 @@ prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1171prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1179prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1172

1180

1173-- | Pretty-print a high-level Idris term in some bindings context with infix info

1181-- | Pretty-print a high-level Idris term in some bindings context with infix info

1174−pprintPTerm :: PPOption -- ^^ pretty printing options

1182+pprintPTerm :: PPOption -- ^^ pretty printing options

1175 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1183 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1176 -> [Name] -- ^^ names to always show in pi, even if not used

1184 -> [Name] -- ^^ names to always show in pi, even if not used

1177 -> [FixDecl] -- ^^ Fixity declarations

1185 -> [FixDecl] -- ^^ Fixity declarations

@@ -1424,7 +1432,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1424 getFixity = flip M.lookup fixities

1432 getFixity = flip M.lookup fixities

1425

1433

1426prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1434prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1427−prettyDocumentedIst ist (name, ty, docs) =

1435+prettyDocumentedIst ist (name, ty, docs) =

1428 prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1436 prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1429 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1437 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1430

1438

@@ -1445,7 +1453,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

1445 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1453 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1446 | otherwise = strName n

1454 | otherwise = strName n

1447 strName n | n == falseTy = "_|_"

1455 strName n | n == falseTy = "_|_"

1448− strName (MN i s) = T.unpack s

1456+ strName (MN i s) = T.unpack s

1449 strName other = show other

1457 strName other = show other

1450

1458

1451

1459

@@ -1704,4 +1712,3 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1704

1712

1705 niTacImp env (TacImp _ _ scr) = ni env scr

1713 niTacImp env (TacImp _ _ scr) = ni env scr

1706 niTacImp _ _ = []

1714 niTacImp _ _ = []

1707−

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/Colours.hs+15−8

@@ -2,7 +2,7 @@ module Idris.Colours (

2 IdrisColour(..),

3 ColourTheme(..),

4 defaultTheme,

5− colouriseKwd, colouriseBound, colouriseImplicit,

5+ colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,

6 colouriseType, colouriseFun, colouriseData, colouriseKeyword,

7 colourisePrompt, colourise, ColourType(..)) where

8

@@ -19,13 +19,14 @@ data IdrisColour = IdrisColour { colour :: Maybe Color

19mkColour :: Color -> IdrisColour

20mkColour c = IdrisColour (Just c) True False False False

21

22−data ColourTheme = ColourTheme { keywordColour :: IdrisColour

22+data ColourTheme = ColourTheme { keywordColour :: IdrisColour

23− , boundVarColour :: IdrisColour

23+ , boundVarColour :: IdrisColour

24− , implicitColour :: IdrisColour

24+ , implicitColour :: IdrisColour

25− , functionColour :: IdrisColour

25+ , functionColour :: IdrisColour

26− , typeColour :: IdrisColour

26+ , typeColour :: IdrisColour

27− , dataColour :: IdrisColour

27+ , dataColour :: IdrisColour

28− , promptColour :: IdrisColour

28+ , promptColour :: IdrisColour

29+ , postulateColour :: IdrisColour

29 }

30 }

30 deriving (Eq, Show)

31 deriving (Eq, Show)

31

32

@@ -38,6 +39,7 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True

38 , typeColour = mkColour Blue

39 , typeColour = mkColour Blue

39 , dataColour = mkColour Red

40 , dataColour = mkColour Red

40 , promptColour = IdrisColour Nothing True False True False

41 , promptColour = IdrisColour Nothing True False True False

42+ , postulateColour = IdrisColour (Just Green) True False True False

41 }

43 }

42

44

43-- | Set the colour of a string using POSIX escape codes

45-- | Set the colour of a string using POSIX escape codes

@@ -74,6 +76,10 @@ colourisePrompt t = colourise (promptColour t)

74colouriseKeyword :: ColourTheme -> String -> String

76colouriseKeyword :: ColourTheme -> String -> String

75colouriseKeyword t = colourise (keywordColour t)

77colouriseKeyword t = colourise (keywordColour t)

76

78

79+colourisePostulate :: ColourTheme -> String -> String

80+colourisePostulate t = colourise (postulateColour t)

81+

82+

77data ColourType = KeywordColour

83data ColourType = KeywordColour

78 | BoundVarColour

84 | BoundVarColour

79 | ImplicitColour

85 | ImplicitColour

@@ -81,4 +87,5 @@ data ColourType = KeywordColour

81 | TypeColour

87 | TypeColour

82 | DataColour

88 | DataColour

83 | PromptColour

89 | PromptColour

90+ | PostulateColour

84 deriving (Eq, Show, Bounded, Enum)

91 deriving (Eq, Show, Bounded, Enum)

src/Idris/Core/CaseTree.hs+3

@@ -336,6 +336,9 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

336toPat :: Bool -> Bool -> [Term] -> [Pat]

337toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

338 where

339+ toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]

340+ | n == txt "Delay" = do arg' <- toPat' arg []

341+ return $ PCon nm t [PAny, PAny, arg']

339 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

342 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

340 return $ PCon n t args'

343 return $ PCon n t args'

341 -- n + 1

344 -- n + 1

src/Idris/Core/Elaborate.hs+2−2

@@ -712,7 +712,7 @@ tryWhen False a b = a

712

713

714-- Try a selection of tactics. Exactly one must work, all others must fail

715−tryAll :: [(Elab' aux a, String)] -> Elab' aux a

715+tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

716tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

717 where

718 cantResolve :: Elab' aux a

@@ -721,7 +721,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

721 tryAll' :: [Elab' aux a] -> -- successes

722 Int -> -- most problems

723 (Elab' aux a, Int) -> -- smallest failure

724− [(Elab' aux a, String)] -> -- still to try

724+ [(Elab' aux a, Name)] -> -- still to try

725 Elab' aux a

726 tryAll' [res] pmax _ [] = res

727 tryAll' (_:_) pmax _ [] = cantResolve

src/Idris/Core/Evaluate.hs+10−5

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTyName, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

@@ -868,14 +868,19 @@ lookupNames n ctxt

868 = let ns = lookupCtxtName n (definitions ctxt) in

869 map fst ns

870

871−lookupTy :: Name -> Context -> [Type]

871+lookupTyName :: Name -> Context -> [(Name, Type)]

872−lookupTy n ctxt

872+lookupTyName n ctxt = do

873− = do def <- lookupCtxt n (definitions ctxt)

873+ (name, def) <- lookupCtxtName n (definitions ctxt)

874− case tfst def of

874+ ty <- case tfst def of

875 (Function ty _) -> return ty

876 (TyDecl _ ty) -> return ty

877 (Operator ty _ _) -> return ty

878 (CaseOp _ ty _ _ _ _) -> return ty

879+ return (name, ty)

880+

881+

882+lookupTy :: Name -> Context -> [Type]

883+lookupTy n ctxt = map snd (lookupTyName n ctxt)

879

884

880isConName :: Name -> Context -> Bool

885isConName :: Name -> Context -> Bool

881isConName n ctxt = isTConName n ctxt || isDConName n ctxt

886isConName n ctxt = isTConName n ctxt || isDConName n ctxt

src/Idris/Core/ProofState.hs+4

@@ -832,6 +832,10 @@ updateEnv ns [] = []

832updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env

833

834updateError [] err = err

835+updateError ns (At f e) = At f (updateError ns e)

836+updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

837+updateError ns (ElaboratingArg f a env e)

838+ = ElaboratingArg f a env (updateError ns e)

835updateError ns (CantUnify b l r e xs sc)

839updateError ns (CantUnify b l r e xs sc)

836 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc

840 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc

837updateError ns e = e

841updateError ns e = e

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

@@ -83,7 +83,7 @@ instance Show FC where

83 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec

84

85-- | Output annotation for pretty-printed name - decides colour

86−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput

86+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput

87

88-- | Text formatting output

89data TextFormatting = BoldText | ItalicText | UnderlineText

@@ -133,7 +133,7 @@ data Err' t

133 | NoTypeDecl Name

134 | NotInjective t t t

135 | CantResolve t

136− | CantResolveAlts [String]

136+ | CantResolveAlts [Name]

137 | IncompleteTerm t

138 | UniverseError

139 | ProgramLineComment

src/Idris/DSL.hs+8−1

@@ -29,6 +29,10 @@ expandDo dsl (PLet n ty v tm)

29 = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

30 expandDo dsl sc

31expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

32+expandDo dsl (PPi p n ty tm)

33+ | Just pi <- dsl_pi dsl

34+ = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in

35+ expandDo dsl sc

32expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

36expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

33expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

37expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

34 (map (fmap (expandDo dsl)) args)

38 (map (fmap (expandDo dsl)) args)

@@ -88,7 +92,10 @@ var dsl n t i = v' i t where

88 | Nothing <- dsl_let dsl

92 | Nothing <- dsl_let dsl

89 = PLet n (v' i ty) (v' i val) (v' i sc)

93 = PLet n (v' i ty) (v' i val) (v' i sc)

90 | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)

94 | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)

95+ v' i (PPi p n ty sc)

96+ | Nothing <- dsl_pi dsl

91− v' i (PPi p n ty sc) = PPi p n (v' i ty) (v' i sc)

97+ = PPi p n (v' i ty) (v' i sc)

98+ | otherwise = PPi p n (v' i ty) (v' (i+1) sc)

92 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

99 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

93 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

100 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

94 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

101 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

src/Idris/DeepSeq.hs+8−9

@@ -157,16 +157,14 @@ instance (NFData t) => NFData (PDecl' t) where

157 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

158 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

159 rnf (PDirective x1) = ()

160− rnf (PProvider x1 x2 x3 x4 x5 x6)

160+ rnf (PProvider x1 x2 x3 x4)

161− = rnf x1 `seq`

162− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

161+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

163 rnf (PTransform x1 x2 x3 x4)

162 rnf (PTransform x1 x2 x3 x4)

164 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

163 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

165

164

166−instance NFData ProvideWhat where

165+instance NFData t => NFData (ProvideWhat' t) where

167− rnf ProvAny = ()

166+ rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()

168− rnf ProvTerm = ()

169− rnf ProvPostulate = ()

167+ rnf (ProvPostulate tm) = rnf tm `seq` ()

170

168

171instance NFData PunInfo where

169instance NFData PunInfo where

172 rnf x = x `seq` ()

170 rnf x = x `seq` ()

@@ -295,12 +293,13 @@ instance NFData TypeInfo where

295 rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

293 rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

296

294

297instance (NFData t) => NFData (DSL' t) where

295instance (NFData t) => NFData (DSL' t) where

298− rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

296+ rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

299 = rnf x1 `seq`

297 = rnf x1 `seq`

300 rnf x2 `seq`

298 rnf x2 `seq`

301 rnf x3 `seq`

299 rnf x3 `seq`

302 rnf x4 `seq`

300 rnf x4 `seq`

301+ rnf x5 `seq`

303− rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

302+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

304

303

305instance NFData SynContext where

304instance NFData SynContext where

306 rnf PatternSyntax = ()

305 rnf PatternSyntax = ()

src/Idris/Delaborate.hs+29−4

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

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where

2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintErr) where

3

4-- Convert core TT back into high level syntax, primarily for display

5-- purposes.

@@ -9,6 +9,7 @@ import Util.Pretty

9import Idris.AbsSyntax

10import Idris.Core.TT

11import Idris.Core.Evaluate

12+import Idris.Docstrings (overview, renderDocstring)

12import Idris.ErrReverse

13import Idris.ErrReverse

13

14

14import Data.List (intersperse)

15import Data.List (intersperse)

@@ -92,13 +93,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

92 | n == eqCon = PRefl un (de env [] r)

93 | n == eqCon = PRefl un (de env [] r)

93 | n == sUN "lazy" = de env [] r

94 | n == sUN "lazy" = de env [] r

94 deFn env (P _ n _) [ty, Bind x (Lam _) r]

95 deFn env (P _ n _) [ty, Bind x (Lam _) r]

95− | n == sUN "Exists"

96+ | n == sUN "Sigma"

96 = PDPair un IsType (PRef un x) (de env [] ty)

97 = PDPair un IsType (PRef un x) (de env [] ty)

97 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

98 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

98 deFn env (P _ n _) [_,_,l,r]

99 deFn env (P _ n _) [_,_,l,r]

99 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

100 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

100 | n == eqTy = PEq un (de env [] l) (de env [] r)

101 | n == eqTy = PEq un (de env [] l) (de env [] r)

101− | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder

102+ | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

102 (de env [] r)

103 (de env [] r)

103 deFn env f@(P _ n _) args

104 deFn env f@(P _ n _) args

104 | n `elem` map snd env

105 | n `elem` map snd env

@@ -195,7 +196,7 @@ pprintErr' i (NotInjective p x y) =

195 pprintTerm i (delab i y)

196 pprintTerm i (delab i y)

196pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

197pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

197pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

198pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

198− align (cat (punctuate (comma <> space) (map text as)))

199+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

199pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

200pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

200pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

201pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

201pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

202pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

@@ -258,6 +259,30 @@ annName n = annName' n (showbasic n)

258annName' :: Name -> String -> Doc OutputAnnotation

259annName' :: Name -> String -> Doc OutputAnnotation

259annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

260annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

260

261

262+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

263+fancifyAnnots ist annot@(AnnName n _ _ _) =

264+ do let ctxt = tt_ctxt ist

265+ docs = docOverview ist n

266+ ty = Just (getTy ist n)

267+ case () of

268+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

269+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

270+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

271+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

272+ _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

273+ _ | otherwise -> annot

274+ where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

275+ docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

276+ let o = overview (fst docs)

277+ -- TODO make width configurable

278+ out = displayS . renderPretty 1.0 50 $ renderDocstring o

279+ return (out "")

280+ getTy :: IState -> Name -> String -- fails if name not already extant!

281+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

282+ delabTy ist n

283+ in (displayS . renderPretty 1.0 50 $ theTy) ""

284+fancifyAnnots _ annot = annot

285+

261showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

286showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

262showSc i [] = empty

287showSc i [] = empty

263showSc i xs = line <> line <> text "In context:" <>

288showSc i xs = line <> line <> text "In context:" <>

src/Idris/ElabDecls.hs+15−13

@@ -687,8 +687,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)

687

688

689-- | Elaborate a type provider

690−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()

690+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

691−elabProvider info syn fc what n ty tm

691+elabProvider info syn fc what n

692 = do i <- getIState

693 -- Ensure that the experimental extension is enabled

694 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -698,12 +698,17 @@ elabProvider info syn fc what n ty tm

698 ctxt <- getContext

699

700 -- First elaborate the expected type (and check that it's a type)

701+ -- The goal type for a postulate is always Type.

702+ (ty', typ) <- case what of

701− (ty', typ) <- elabVal toplevel False ty

703+ ProvTerm ty p -> elabVal toplevel False ty

704+ ProvPostulate _ -> elabVal toplevel False PType

702 unless (isTType typ) $

705 unless (isTType typ) $

703 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

706 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

704

707

705 -- Elaborate the provider term to TT and check that the type matches

708 -- Elaborate the provider term to TT and check that the type matches

709+ (e, et) <- case what of

710+ ProvTerm _ tm -> elabVal toplevel False tm

706− (e, et) <- elabVal toplevel False tm

711+ ProvPostulate tm -> elabVal toplevel False tm

707 unless (isProviderOf (normalise ctxt [] ty') et) $

712 unless (isProviderOf (normalise ctxt [] ty') et) $

708 ifail $ "Expected provider type IO (Provider (" ++

713 ifail $ "Expected provider type IO (Provider (" ++

709 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

714 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

@@ -721,17 +726,14 @@ elabProvider info syn fc what n ty tm

721

726

722 case provided of

727 case provided of

723 Provide tm

728 Provide tm

724− | what `elem` [ProvTerm, ProvAny] ->

729+ | ProvTerm ty _ <- what ->

725 do -- Finally add a top-level definition of the provided term

730 do -- Finally add a top-level definition of the provided term

726 elabType info syn emptyDocstring [] fc [] n ty

731 elabType info syn emptyDocstring [] fc [] n ty

727 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

732 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

728 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

733 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

729− | otherwise ->

730− ierror . Msg $ "Attempted to provide a term where a postulate was expected."

731− Postulate

732− | what `elem` [ProvPostulate, ProvAny] ->

734+ | ProvPostulate _ <- what ->

733 do -- Add the postulate

735 do -- Add the postulate

734− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty

736+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

735 logLvl 3 $ "Elaborated provided postulate " ++ show n

737 logLvl 3 $ "Elaborated provided postulate " ++ show n

736 | otherwise ->

738 | otherwise ->

737 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

739 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

@@ -2048,7 +2050,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2048 [c] -> return c

2050 [c] -> return c

2049 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

2051 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

2050 cs -> tclift $ tfail $ At fc

2052 cs -> tclift $ tfail $ At fc

2051− (CantResolveAlts (map (show . fst) cs))

2053+ (CantResolveAlts (map fst cs))

2052 let constraint = PApp fc (PRef fc n) (map pexp ps)

2054 let constraint = PApp fc (PRef fc n) (map pexp ps)

2053 let iname = mkiname n ps expn

2055 let iname = mkiname n ps expn

2054 let emptyclass = null (class_methods ci)

2056 let emptyclass = null (class_methods ci)

@@ -2414,10 +2416,10 @@ elabDecl' _ info (PDSL n dsl)

2414 addIBC (IBCDSL n)

2416 addIBC (IBCDSL n)

2415elabDecl' what info (PDirective i)

2417elabDecl' what info (PDirective i)

2416 | what /= EDefns = i

2418 | what /= EDefns = i

2417−elabDecl' what info (PProvider syn fc provWhat n tp tm)

2419+elabDecl' what info (PProvider syn fc provWhat n)

2418 | what /= EDefns

2420 | what /= EDefns

2419 = do iLOG $ "Elaborating type provider " ++ show n

2421 = do iLOG $ "Elaborating type provider " ++ show n

2420− elabProvider info syn fc provWhat n tp tm

2422+ elabProvider info syn fc provWhat n

2421elabDecl' what info (PTransform fc safety old new)

2423elabDecl' what info (PTransform fc safety old new)

2422 = elabTransform info fc safety old new

2424 = elabTransform info fc safety old new

2423elabDecl' _ _ _ = return () -- skipped this time

2425elabDecl' _ _ _ = return () -- skipped this time

src/Idris/ElabTerm.hs+9−9

@@ -70,7 +70,7 @@ build ist info pattern opts fn tm

70

71 when (not pattern) $

72 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++

73− "Remaining problems:\n" ++ show probs) $

73+ "Remaining problems:\n" ++ qshow probs) $

74 do unify_all; matchProblems True; unifyProblems

75

76 probs <- get_probs

@@ -271,10 +271,10 @@ elab ist info pattern opts fn tm

271 let as' = pruneByType (map fst env) tc ctxt as

272-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

273 tryAll (zip (map (elab' ina) as') (map showHd as'))

274− where showHd (PApp _ (PRef _ n) _) = show n

274+ where showHd (PApp _ (PRef _ n) _) = n

275− showHd (PRef _ n) = show n

275+ showHd (PRef _ n) = n

276− showHd (PApp _ h _) = show h

276+ showHd (PApp _ h _) = showHd h

277− showHd x = show x

277+ showHd x = NErased -- We probably should do something better than this here

278 elab' ina (PAlternative False as)

279 = trySeq as

280 where -- if none work, take the error from the first

@@ -1009,7 +1009,7 @@ runTac autoSolve ist fn tac

1009 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)

1010 let tacs = map (\ (fn', imps) ->

1011 (match_apply (Var fn') (map (\x -> (x, 0)) imps),

1012− show fn')) fnimps

1012+ fn')) fnimps

1013 tryAll tacs

1014 when autoSolve solveAll

1015 where envArgs n = do e <- get_env

@@ -1025,7 +1025,7 @@ runTac autoSolve ist fn tac

1025 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)

1026 let tacs = map (\ (fn', imps) ->

1027 (apply (Var fn') (map (\x -> (x, 0)) imps),

1028− show fn')) fnimps

1028+ fn')) fnimps

1029 tryAll tacs

1030 when autoSolve solveAll

1031 where isImp (PImp _ _ _ _ _) = True

@@ -1629,8 +1629,8 @@ reflectErr (NotInjective t1 t2 t3) =

1629 ]

1630reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

1631reflectErr (CantResolveAlts ss) =

1632− raw_apply (Var $ reflErrName "CantResolve")

1632+ raw_apply (Var $ reflErrName "CantResolveAlts")

1633− [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]

1633+ [rawList (Var $ (sUN "String")) (map Var ss)]

1634reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

1635reflectErr UniverseError = Var $ reflErrName "UniverseError"

1636reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

src/Idris/Erasure.hs+1−1

@@ -109,7 +109,7 @@ performUsageAnalysis = do

109 getMainName ist = case lookupCtxtName n (idris_implicits ist) of

110 [(n', _)] -> Right n'

111 [] -> Left (NoSuchVariable n)

112− more -> Left (CantResolveAlts (map (show . fst) more))

112+ more -> Left (CantResolveAlts (map fst more))

113 where

114 n = sNS (sUN "main") ["Main"]

115

src/Idris/Help.hs+2−1

@@ -58,7 +58,8 @@ help =

58 ([":unset"], OptionArg, "Unset an option"),

59 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

60 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

61− ([":q",":quit"], NoArg, "Exit the Idris system")

61+ ([":q",":quit"], NoArg, "Exit the Idris system"),

62+ ([":w", ":warranty"], NoArg, "Displays warranty information")

62 ]

63 ]

63

64

64-- | 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+4−2

@@ -2197,7 +2197,7 @@ instance Binary Syntax where

2197 return (Rule x1 x2 x3)

2198

2199instance (Binary t) => Binary (DSL' t) where

2200− put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

2200+ put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2201 = do put x1

2202 put x2

2203 put x3

@@ -2207,6 +2207,7 @@ instance (Binary t) => Binary (DSL' t) where

2207 put x7

2208 put x8

2209 put x9

2210+ put x10

2210 get

2211 get

2211 = do x1 <- get

2212 = do x1 <- get

2212 x2 <- get

2213 x2 <- get

@@ -2217,7 +2218,8 @@ instance (Binary t) => Binary (DSL' t) where

2217 x7 <- get

2218 x7 <- get

2218 x8 <- get

2219 x8 <- get

2219 x9 <- get

2220 x9 <- get

2221+ x10 <- get

2220− return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

2222+ return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2221

2223

2222instance Binary SSymbol where

2224instance Binary SSymbol where

2223 put x

2225 put x

src/Idris/IdeSlave.hs+5−4

@@ -74,10 +74,11 @@ instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>

74 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]

75

76instance SExpable NameOutput where

77− toSExp TypeOutput = SymbolAtom "type"

77+ toSExp TypeOutput = SymbolAtom "type"

78− toSExp FunOutput = SymbolAtom "function"

78+ toSExp FunOutput = SymbolAtom "function"

79− toSExp DataOutput = SymbolAtom "data"

79+ toSExp DataOutput = SymbolAtom "data"

80− toSExp MetavarOutput = SymbolAtom "metavar"

80+ toSExp MetavarOutput = SymbolAtom "metavar"

81+ toSExp PostulateOutput = SymbolAtom "postulate"

81

82

82maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

83maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

83maybeProps [] = []

84maybeProps [] = []

src/Idris/Interactive.hs+4−4

@@ -162,7 +162,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

162 mn <- case lookupNames n ctxt of

163 [x] -> return x

164 [] -> return n

165− ns -> ierror (CantResolveAlts (map show ns))

165+ ns -> ierror (CantResolveAlts ns)

166 i <- getIState

167 let (top, envlen, _) = case lookup mn (idris_metavars i) of

168 Just (t, e, False) -> (t, e, False)

@@ -242,10 +242,10 @@ makeLemma h fn updatefile l n

242 let isProv = checkProv tyline (show n)

243

244 ctxt <- getContext

245− mty <- case lookupTy n ctxt of

245+ mty <- case lookupTyName n ctxt of

246− [t] -> return t

246+ [(_,t)] -> return t

247 [] -> ierror (NoSuchVariable n)

248− ns -> ierror (CantResolveAlts (map show ns))

248+ ns -> ierror (CantResolveAlts (map fst ns))

249 i <- getIState

250

251 if (not isProv) then do

src/Idris/Output.hs−32

@@ -83,38 +83,6 @@ ihRenderResult h d = do ist <- getIState

83 RawOutput -> consoleDisplayAnnotated h d

84 IdeSlave n -> ideSlaveReturnAnnotated n h d

85

86−makeAnnName :: IState -> Name -> Maybe OutputAnnotation

87−makeAnnName ist n

88− | isDConName n ctxt = annName DataOutput

89− | isFnName n ctxt = annName FunOutput

90− | isTConName n ctxt = annName TypeOutput

91− | isMetavarName n ist = annName MetavarOutput

92− | otherwise = Nothing

93− where ctxt = tt_ctxt ist

94− docs = docOverview ist n

95− ty = Just (getTy ist n)

96−

97− annName :: NameOutput -> Maybe OutputAnnotation

98− annName nameType = Just (AnnName n (Just nameType) docs ty)

99− docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

100− docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

101− let o = overview (fst docs)

102− -- TODO make width configurable

103− out = displayS . renderPretty 1.0 50 $ renderDocstring o

104− return (out "")

105− getTy :: IState -> Name -> String -- fails if name not already extant!

106− getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

107− delabTy ist n

108− in (displayS . renderPretty 1.0 50 $ theTy) ""

109−

110−

111−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

112−fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of

113− Just fancyAnnot -> fancyAnnot

114− Nothing -> annot

115−fancifyAnnots _ annot = annot

116−

117−

118ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

86ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

119ideSlaveReturnWithStatus status n h out = do

87ideSlaveReturnWithStatus status n h out = do

120 ist <- getIState

88 ist <- getIState

src/Idris/ParseData.hs+5−3

@@ -210,12 +210,14 @@ dsl syn = do reserved "dsl"

210 first = lookup "index_first" bs

211 next = lookup "index_next" bs

212 leto = lookup "let" bs

213− lambda = lookup "lambda" bs in

213+ lambda = lookup "lambda" bs

214+ pi = lookup "pi" bs in

214 initDSL { dsl_var = var,

215 initDSL { dsl_var = var,

215 index_first = first,

216 index_first = first,

216 index_next = next,

217 index_next = next,

217 dsl_lambda = lambda,

218 dsl_lambda = lambda,

218− dsl_let = leto }

219+ dsl_let = leto,

220+ dsl_pi = pi }

219

221

220{- | Checks DSL for errors -}

222{- | Checks DSL for errors -}

221-- FIXME: currently does nothing, check if DSL is really sane

223-- FIXME: currently does nothing, check if DSL is really sane

@@ -236,6 +238,6 @@ overload syn = do o <- identifier <|> do reserved "let"

236 t <- expr syn

238 t <- expr syn

237 return (o, t)

239 return (o, t)

238 <?> "dsl overload declaratioN"

240 <?> "dsl overload declaratioN"

239− where overloadable = ["let","lambda","index_first","index_next","variable"]

241+ where overloadable = ["let","lambda","pi","index_first","index_next","variable"]

240

242

241

243

src/Idris/Parser.hs+14−13

@@ -1034,7 +1034,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1034 case lookupCtxtName n (idris_implicits i) of

1035 [(n', _)] -> return n'

1036 [] -> throwError (NoSuchVariable n)

1037− more -> throwError (CantResolveAlts (map (show . fst) more))

1037+ more -> throwError (CantResolveAlts (map fst more))

1038

1039pLangExt :: IdrisParser LanguageExt

1040pLangExt = (reserved "TypeProviders" >> return TypeProviders)

@@ -1061,19 +1061,20 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1061 -}

1062provider :: SyntaxInfo -> IdrisParser [PDecl]

1063provider syn = do try (lchar '%' *> reserved "provide");

1064− what <- provideWhat

1064+ provideTerm <|> providePostulate

1065− lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1066− fc <- getFC

1067− reserved "with"

1068− e <- expr syn

1069− return [PProvider syn fc what n t e]

1070 <?> "type provider"

1065 <?> "type provider"

1071− where provideWhat :: IdrisParser ProvideWhat

1066+ where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1072− provideWhat = option ProvAny

1067+ fc <- getFC

1073− ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>

1068+ reserved "with"

1074− pure ProvTerm)

1069+ e <- expr syn <?> "provider expression"

1070+ return [PProvider syn fc (ProvTerm t e) n]

1075− <|> (reserved "postulate" *> pure ProvPostulate)

1071+ providePostulate = do reserved "postulate"

1076− <?> "provider variety")

1072+ n <- fnName

1073+ fc <- getFC

1074+ reserved "with"

1075+ e <- expr syn <?> "provider expression"

1076+ return [PProvider syn fc (ProvPostulate e) n]

1077+

1077{- | Parses a transform

1078{- | Parses a transform

1078

1079

1079@

1080@

src/Idris/Prover.hs+92−82

@@ -63,9 +63,10 @@ prove opt ctxt lit n ty

63 ideslavePutSExp "start-proof-mode" n

64 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

65 iLOG $ "Adding " ++ show tm

66− iputStrLn $ showProof lit n prf

67 i <- getIState

66 i <- getIState

67+ case idris_outputmode i of

68− ideslavePutSExp "end-proof-mode" n

68+ IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

69+ _ -> iputStrLn $ showProof lit n prf

69 let proofs = proof_list i

70 let proofs = proof_list i

70 putIState (i { proof_list = (n, prf) : proofs })

71 putIState (i { proof_list = (n, prf) : proofs })

71 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

72 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

@@ -85,6 +86,11 @@ prove opt ctxt lit n ty

85 [([], P Ref n ty, ptm)]

86 [([], P Ref n ty, ptm)]

86 [([], P Ref n ty, ptm')] ty)

87 [([], P Ref n ty, ptm')] ty)

87 solveDeferred n

88 solveDeferred n

89+ case idris_outputmode i of

90+ IdeSlave n ->

91+ runIO . putStrLn $

92+ convSExp "return" (SymbolAtom "ok", "") n

93+ _ -> return ()

88

94

89elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

95elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

90elabStep st e = case runStateT eCheck st of

96elabStep st e = case runStateT eCheck st of

@@ -171,7 +177,7 @@ receiveInput e =

171 ideslavePutSExp "return" good

177 ideslavePutSExp "return" good

172 receiveInput e

178 receiveInput e

173 Just (Interpret cmd) -> return (Just cmd)

179 Just (Interpret cmd) -> return (Just cmd)

174− Nothing -> return Nothing

180+ _ -> return Nothing

175

181

176ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

182ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

177ploop fn d prompt prf e h

183ploop fn d prompt prf e h

@@ -198,91 +204,95 @@ ploop fn d prompt prf e h

198 case cmd of

204 case cmd of

199 Success Abandon -> do iPrintError ""; ifail "Abandoned"

205 Success Abandon -> do iPrintError ""; ifail "Abandoned"

200 _ -> return ()

206 _ -> return ()

201− (d, st, done, prf') <- idrisCatch

207+ (d, st, done, prf', res) <- idrisCatch

202 (case cmd of

208 (case cmd of

203− Failure err -> do iPrintError (show err)

204− return (False, e, False, prf)

209+ Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

205 Success Undo -> do (_, st) <- elabStep e loadState

210 Success Undo -> do (_, st) <- elabStep e loadState

206− iPrintResult ""

207− return (True, st, False, init prf)

211+ return (True, st, False, init prf, Right "")

208− Success ProofState -> do iPrintResult ""

209− return (True, e, False, prf)

212+ Success ProofState -> return (True, e, False, prf, Right "")

210 Success ProofTerm -> do tm <- lifte e get_term

213 Success ProofTerm -> do tm <- lifte e get_term

211− iPrintResult $ "TT: " ++ show tm ++ "\n"

214+ iputStrLn $ "TT: " ++ show tm ++ "\n"

212− return (False, e, False, prf)

215+ return (False, e, False, prf, Right "")

213 Success Qed -> do hs <- lifte e get_holes

216 Success Qed -> do hs <- lifte e get_holes

214 when (not (null hs)) $ ifail "Incomplete proof"

217 when (not (null hs)) $ ifail "Incomplete proof"

215− iPrintResult "Proof completed!"

218+ iputStrLn "Proof completed!"

216− return (False, e, True, prf)

219+ return (False, e, True, prf, Right "")

217− Success (TCheck (PRef _ n)) ->

220+ Success (TCheck (PRef _ n)) -> checkNameType n

218− do ctxt <- getContext

219− ist <- getIState

220− imp <- impShow

221− idrisCatch (do

222− let h = idris_outh ist

223− OK env = envAtFocus (proof e)

224− ctxt' = envCtxt env ctxt

225− bnd = map (\x -> (fst x, False)) env

226− ist' = ist { tt_ctxt = ctxt' }

227− putIState ist'

228− -- Unlike the REPL, metavars have no special treatment, to

229− -- make it easier to see how to prove with them.

230− case lookupNames n ctxt' of

231− [] -> ihPrintError h $ "No such variable " ++ show n

232− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

233− putIState ist

234− return (False, e, False, prf))

235− (\err -> do putIState ist ; ierror err)

236− Success (TCheck t) ->

221+ Success (TCheck t) -> checkType t

237− do ist <- getIState

238− ctxt <- getContext

239− idrisCatch (do

240− let OK env = envAtFocus (proof e)

241− ctxt' = envCtxt env ctxt

242− putIState ist { tt_ctxt = ctxt' }

243− (tm, ty) <- elabVal toplevel False t

244− let ppo = ppOptionIst ist

245− ty' = normaliseC ctxt [] ty

246− h = idris_outh ist

247− infixes = idris_infixes ist

248− case tm of

249− TType _ ->

250− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

251− _ -> let bnd = map (\x -> (fst x, False)) env in

252− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

253− (pprintPTerm ppo bnd [] infixes (delab ist ty))

254− putIState ist

255− return (False, e, False, prf))

256− (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

257− Success (TEval t) -> withErrorReflection $

222+ Success (TEval t) -> evalTerm t e

258− do ctxt <- getContext

259− ist <- getIState

260− idrisCatch (do

261− let OK env = envAtFocus (proof e)

262− ctxt' = envCtxt env ctxt

263− ist' = ist { tt_ctxt = ctxt' }

264− bnd = map (\x -> (fst x, False)) env

265− putIState ist'

266− (tm, ty) <- elabVal toplevel False t

267− let tm' = force (normaliseAll ctxt' env tm)

268− ty' = force (normaliseAll ctxt' env ty)

269− ppo = ppOption (idris_options ist')

270− infixes = idris_infixes ist

271− tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

272− tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

273− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

274− putIState ist

275− return (False, e, False, prf))

276− (\err -> do putIState ist ; ierror err)

277 Success tac -> do (_, e) <- elabStep e saveState

223 Success tac -> do (_, e) <- elabStep e saveState

278 (_, st) <- elabStep e (runTac autoSolve i fn tac)

224 (_, st) <- elabStep e (runTac autoSolve i fn tac)

279−-- trace (show (problems (proof st))) $

280− iPrintResult ""

281− return (True, st, False, prf ++ [step]))

225+ return (True, st, False, prf ++ [step], Right ""))

282− (\err -> do iPrintError (pshow i err)

283− return (False, e, False, prf))

226+ (\err -> return (False, e, False, prf, Left err))

284 ideslavePutSExp "write-proof-state" (prf', length prf')

227 ideslavePutSExp "write-proof-state" (prf', length prf')

228+ case res of

229+ Left err -> do iPrintError (pshow i err)

230+ ploop fn d prompt prf' st h'

231+ Right ok ->

285− if done then do (tm, _) <- elabStep st get_term

232+ if done then do (tm, _) <- elabStep st get_term

286− return (tm, prf')

233+ return (tm, prf')

234+ else do iPrintResult ok

287− else ploop fn d prompt prf' st h'

235+ ploop fn d prompt prf' st h'

288 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

236 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

237+ checkNameType n = do

238+ ctxt <- getContext

239+ ist <- getIState

240+ imp <- impShow

241+ idrisCatch (do

242+ let h = idris_outh ist

243+ OK env = envAtFocus (proof e)

244+ ctxt' = envCtxt env ctxt

245+ bnd = map (\x -> (fst x, False)) env

246+ ist' = ist { tt_ctxt = ctxt' }

247+ putIState ist'

248+ -- Unlike the REPL, metavars have no special treatment, to

249+ -- make it easier to see how to prove with them.

250+ case lookupNames n ctxt' of

251+ [] -> ihPrintError h $ "No such variable " ++ show n

252+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

253+ putIState ist

254+ return (False, e, False, prf, Right ""))

255+ (\err -> do putIState ist ; ierror err)

256+

257+ checkType t = do

258+ ist <- getIState

259+ ctxt <- getContext

260+ idrisCatch (do

261+ let OK env = envAtFocus (proof e)

262+ ctxt' = envCtxt env ctxt

263+ putIState ist { tt_ctxt = ctxt' }

264+ (tm, ty) <- elabVal toplevel False t

265+ let ppo = ppOptionIst ist

266+ ty' = normaliseC ctxt [] ty

267+ h = idris_outh ist

268+ infixes = idris_infixes ist

269+ case tm of

270+ TType _ ->

271+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

272+ _ -> let bnd = map (\x -> (fst x, False)) env in

273+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

274+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

275+ putIState ist

276+ return (False, e, False, prf, Right ""))

277+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

278+

279+ evalTerm t e = withErrorReflection $

280+ do ctxt <- getContext

281+ ist <- getIState

282+ idrisCatch (do

283+ let OK env = envAtFocus (proof e)

284+ ctxt' = envCtxt env ctxt

285+ ist' = ist { tt_ctxt = ctxt' }

286+ bnd = map (\x -> (fst x, False)) env

287+ putIState ist'

288+ (tm, ty) <- elabVal toplevel False t

289+ let tm' = force (normaliseAll ctxt' env tm)

290+ ty' = force (normaliseAll ctxt' env ty)

291+ ppo = ppOption (idris_options ist')

292+ infixes = idris_infixes ist

293+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

294+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

295+ ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

296+ putIState ist

297+ return (False, e, False, prf, Right ""))

298+ (\err -> do putIState ist ; ierror err)

src/Idris/Providers.hs+1−7

@@ -11,16 +11,14 @@ import Debug.Trace

11

12-- | Wrap a type provider in the type of type providers

13providerTy :: FC -> PTerm -> PTerm

14−providerTy fc tm

14+providerTy fc tm

15 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]

16

17ioret = sUN "prim_io_return"

18ermod = sNS (sUN "Error") ["Providers"]

19prmod = sNS (sUN "Provide") ["Providers"]

20−posmod = sNS (sUN "Postulate") ["Providers"]

21

20

22data Provided a = Provide a

21data Provided a = Provide a

23− | Postulate

24 deriving (Show, Eq, Functor)

22 deriving (Show, Eq, Functor)

25

23

26-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

24-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

@@ -35,10 +33,6 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

35 , (P _ nm _, [_, res]) <- unApply result

33 , (P _ nm _, [_, res]) <- unApply result

36 , pioret == ioret && nm == prmod

34 , pioret == ioret && nm == prmod

37 = return . Provide $ res

35 = return . Provide $ res

38− | (P _ pioret _, [tp, result]) <- unApply tm

39− , (P _ nm _, [_]) <- unApply result

40− , pioret == ioret && nm == posmod

41− = return Postulate

42 | otherwise = ifail $ "Internal type provider error: result was not " ++

36 | otherwise = ifail $ "Internal type provider error: result was not " ++

43 "IO (Provider a), or perhaps missing normalisation."

37 "IO (Provider a), or perhaps missing normalisation."

44

38

src/Idris/REPL.hs+51−16

@@ -110,7 +110,7 @@ repl orig mods

110 return ()

111 Just input -> -- H.catch

112 do ms <- H.catch (lift $ processInput input orig mods)

113− (ctrlC (return (Just mods)))

113+ (ctrlC (return (Just mods)))

114 case ms of

115 Just mods -> repl orig mods

116 Nothing -> return ()

@@ -121,7 +121,7 @@ repl orig mods

121 act -- repl orig mods

122

123 showMVs c thm [] = ""

124− showMVs c thm ms = "Metavariables: " ++

124+ showMVs c thm ms = "Metavariables: " ++

125 show' 4 c thm (map fst ms) ++ "\n"

126

127 show' 0 c thm ms = let l = length ms in

@@ -129,7 +129,7 @@ repl orig mods

129 ++ " other"

130 ++ if l == 1 then ")" else "s)"

131 show' n c thm [m] = showM c thm m

132− show' n c thm (m : ms) = showM c thm m ++ ", " ++

132+ show' n c thm (m : ms) = showM c thm m ++ ", " ++

133 show' (n - 1) c thm ms

134

135 showM c thm n = if c then colouriseFun thm (show n)

@@ -240,11 +240,25 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

240 i <- getIState

241 case parseCmd i "(input)" cmd of

242 Failure err -> iPrintError $ show (fixColour c err)

243− Success (Prove n') -> do iPrintResult ""

243+ Success (Prove n') ->

244− idrisCatch

244+ idrisCatch

245− (process stdout fn (Prove n'))

245+ (do process stdout fn (Prove n')

246+ isetPrompt (mkPrompt mods)

247+ case idris_outputmode i of

248+ IdeSlave n -> -- signal completion of proof to ide

249+ runIO . hPutStrLn stdout $

250+ IdeSlave.convSExp "return"

251+ (IdeSlave.SymbolAtom "ok", "")

252+ n

253+ _ -> return ())

254+ (\e -> do ist <- getIState

255+ isetPrompt (mkPrompt mods)

256+ case idris_outputmode i of

257+ IdeSlave n ->

258+ runIO . hPutStrLn stdout $

259+ IdeSlave.convSExp "abandon-proof" "Abandoned" n

260+ _ -> return ()

246− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

261+ ihRenderError stdout $ pprintErr ist e)

247− isetPrompt (mkPrompt mods)

248 Success cmd -> idrisCatch

262 Success cmd -> idrisCatch

249 (ideslaveProcess fn cmd)

263 (ideslaveProcess fn cmd)

250 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

264 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

@@ -388,6 +402,7 @@ splitName s = case reverse $ splitOn "." s of

388 (n:ns) -> Right $ sNS (sUN n) ns

402 (n:ns) -> Right $ sNS (sUN n) ns

389

403

390ideslaveProcess :: FilePath -> Command -> Idris ()

404ideslaveProcess :: FilePath -> Command -> Idris ()

405+ideslaveProcess fn Warranty = process stdout fn Warranty

391ideslaveProcess fn Help = process stdout fn Help

406ideslaveProcess fn Help = process stdout fn Help

392ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

407ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

393 iPrintResult "changed directory to"

408 iPrintResult "changed directory to"

@@ -511,7 +526,7 @@ resolveProof n'

511 n <- case lookupNames n' ctxt of

526 n <- case lookupNames n' ctxt of

512 [x] -> return x

527 [x] -> return x

513 [] -> return n'

528 [] -> return n'

514− ns -> ierror (CantResolveAlts (map show ns))

529+ ns -> ierror (CantResolveAlts ns)

515 return n

530 return n

516

531

517removeProof :: Name -> Idris ()

532removeProof :: Name -> Idris ()

@@ -564,6 +579,7 @@ insertScript prf (x : xs) = x : insertScript prf xs

564

579

565process :: Handle -> FilePath -> Command -> Idris ()

580process :: Handle -> FilePath -> Command -> Idris ()

566process h fn Help = iPrintResult displayHelp

581process h fn Help = iPrintResult displayHelp

582+process h fn Warranty = iPrintResult warranty

567process h fn (ChangeDirectory f)

583process h fn (ChangeDirectory f)

568 = do runIO $ setCurrentDirectory f

584 = do runIO $ setCurrentDirectory f

569 return ()

585 return ()

@@ -709,7 +725,7 @@ process h fn (DebugInfo n)

709 when (not (null cg')) $ do iputStrLn "Call graph:\n"

725 when (not (null cg')) $ do iputStrLn "Call graph:\n"

710 iputStrLn (show cg')

726 iputStrLn (show cg')

711process h fn (Search t) = searchByType h t

727process h fn (Search t) = searchByType h t

712−process h fn (CaseSplitAt updatefile l n)

728+process h fn (CaseSplitAt updatefile l n)

713 = caseSplitAt h fn updatefile l n

729 = caseSplitAt h fn updatefile l n

714process h fn (AddClauseFrom updatefile l n)

730process h fn (AddClauseFrom updatefile l n)

715 = addClauseFrom h fn updatefile l n

731 = addClauseFrom h fn updatefile l n

@@ -793,7 +809,7 @@ process h fn (Prove n')

793 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

809 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

794 [(n, (_,_,False))] -> return n

810 [(n, (_,_,False))] -> return n

795 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

811 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")

796− ns -> ierror (CantResolveAlts (map show ns))

812+ ns -> ierror (CantResolveAlts (map fst ns))

797 prover (lit fn) n

813 prover (lit fn) n

798 -- recheck totality

814 -- recheck totality

799 i <- getIState

815 i <- getIState

@@ -1022,10 +1038,10 @@ loadInputs h inputs toline -- furthest line to read in input source files

1022 let ifiles = getModuleFiles modTree

1038 let ifiles = getModuleFiles modTree

1023 iLOG ("MODULE TREE : " ++ show modTree)

1039 iLOG ("MODULE TREE : " ++ show modTree)

1024 iLOG ("RELOAD: " ++ show ifiles)

1040 iLOG ("RELOAD: " ++ show ifiles)

1025− when (not (all ibc ifiles) || loadCode) $

1041+ when (not (all ibc ifiles) || loadCode) $

1026 tryLoad False (filter (not . ibc) ifiles)

1042 tryLoad False (filter (not . ibc) ifiles)

1027 -- return the files that need rechecking

1043 -- return the files that need rechecking

1028− return ifiles)

1044+ return ifiles)

1029 ninputs

1045 ninputs

1030 inew <- getIState

1046 inew <- getIState

1031 let tidata = idris_tyinfodata inew

1047 let tidata = idris_tyinfodata inew

@@ -1350,6 +1366,11 @@ getPkgMkDoc :: Opt -- ^ Opt to extract

1350getPkgMkDoc (PkgMkDoc str) = Just str

1366getPkgMkDoc (PkgMkDoc str) = Just str

1351getPkgMkDoc _ = Nothing

1367getPkgMkDoc _ = Nothing

1352

1368

1369+getPkgTest :: Opt -- ^ the option to extract

1370+ -> Maybe String -- ^ the package file to test

1371+getPkgTest (PkgTest f) = Just f

1372+getPkgTest _ = Nothing

1373+

1353getCodegen :: Opt -> Maybe Codegen

1374getCodegen :: Opt -> Maybe Codegen

1354getCodegen (UseCodegen x) = Just x

1375getCodegen (UseCodegen x) = Just x

1355getCodegen _ = Nothing

1376getCodegen _ = Nothing

@@ -1395,6 +1416,20 @@ banner = " ____ __ _ \n" ++

1395 " / _/___/ /____(_)____ \n" ++

1416 " / _/___/ /____(_)____ \n" ++

1396 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1417 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

1397 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

1418 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

1398− " /___/\\__,_/_/ /_/____/ Type :? for help \n"

1419+ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++

1399−

1420+ "\n" ++

1400−

1421+ "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++

1422+ "For details type :warranty."

1423+

1424+warranty = "\n" ++

1425+ "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++

1426+ "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++

1427+ "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++

1428+ "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++

1429+ "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++

1430+ "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++

1431+ "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++

1432+ "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++

1433+ "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++

1434+ "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++

1435+ "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"

src/Idris/REPLParser.hs+6−5

@@ -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,7 @@ 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;

75+ <|> try (do cmd ["s", "search"]; P.whiteSpace;

75 t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))

76 t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))

76 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 upd <- option False (do P.lchar '!'; return True)

78 upd <- option False (do P.lchar '!'; return True)

@@ -183,7 +184,7 @@ pColourMod = try (P.symbol "vivid" >> return doVivid)

183 doNoItalic i = i { italic = False }

184 doNoItalic i = i { italic = False }

184 doSetColour c i = i { colour = c }

185 doSetColour c i = i { colour = c }

185

186

186−

187+-- | Generate the colour type names using the default Show instance.

187colourTypes :: [(String, ColourType)]

188colourTypes :: [(String, ColourType)]

188colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

189colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

189 enumFromTo minBound maxBound

190 enumFromTo minBound maxBound

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/Makefile+1−1

@@ -8,7 +8,7 @@ test: $(TESTS)

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

9

10test_java:

11− perl ./runtest.pl without sugar004 buffer001 --codegen Java

11+ @perl ./runtest.pl without --codegen Java

12

13test_js:

14 @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 --codegen node

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/dsl003/DSLPi.idrnew file+38

@@ -0,0 +1,38 @@

1+module DSLPi

2+

3+data Ty = BOOL | INT | UNIT | ARR Ty Ty

4+

5+dsl simple_type

6+ pi = ARR

7+

8+test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

9+test1 = refl

10+

11+using (vars : Vect n Ty)

12+ infix 2 ===

13+

14+ data Expr : Vect n Ty -> Ty -> Type where

15+ Var : (i : Fin n) -> Expr vars (index i vars)

16+ (===) : Expr vars t -> Expr vars t -> Expr vars BOOL

17+

18+ data Spec : Vect n Ty -> Type where

19+ ForAll : (t : Ty) -> Spec (t :: vars) -> Spec vars

20+ ItHolds : Expr vars BOOL -> Spec vars

21+

22+ implicit exprSpec : Expr vars BOOL -> Spec vars

23+ exprSpec = ItHolds

24+

25+dsl specs

26+ pi = ForAll

27+ variable = Var

28+ index_first = fZ

29+ index_next = fS

30+

31+test2 : Spec []

32+test2 = specs ((x, y : INT) -> x === y)

33+

34+test3 : Spec []

35+test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ

36+

37+test4 : test2 = test3

38+test4 = refl

test/dsl003/expectednew file+2

@@ -0,0 +1,2 @@

1+ForAll INT (ForAll INT (ItHolds (Var (fS fZ) === Var fZ))) : Spec []

2+refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)

test/dsl003/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --nocolour --check DSLPi.idr -e test1 -e test2

3+rm -f *.ibc

test/ffi005/Postulate.idr+3−3

@@ -4,10 +4,10 @@ import Providers

4

5%language TypeProviders

6

7−bad : IO (Provider _|_)

7+bad : IO (Provider Type)

8−bad = pure Postulate

8+bad = return $ pure _|_

9

10−%provide (oops : _|_) with bad

10+%provide postulate oops with bad

11

12main : IO ()

13main = putStrLn "oops"

test/ffi005/Postulate2.idrdeleted−13

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

1−module Main

2−

3−import Providers

4−

5−%language TypeProviders

6−

7−bad : IO (Provider _|_)

8−bad = pure Postulate

9−

10−%provide postulate (oops : _|_) with bad

11−

12−main : IO ()

13−main = putStrLn "oops"

test/ffi005/Postulate3.idrdeleted−13

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

1−module Main

2−

3−import Providers

4−

5−%language TypeProviders

6−

7−bad : IO (Provider _|_)

8−bad = pure Postulate

9−

10−%provide term (oops : _|_) with bad

11−

12−main : IO ()

13−main = putStrLn "oops"

test/ffi005/expected−2

@@ -1,3 +1 @@

1oops

2−oops

3−Attempted to provide a postulate where a term was expected.

test/ffi005/run−7

@@ -3,10 +3,3 @@

3idris $@ Postulate.idr -o postulate

4./postulate

5rm -f postulate *.ibc

6−

7−idris $@ Postulate2.idr -o postulate

8−./postulate

9−rm -f postulate *.ibc

10−

11−idris $@ Postulate3.idr -o postulate

12−rm -f postulate *.ibc

test/reg029/Reg029Wrapper.javanew file+17

@@ -0,0 +1,17 @@

1+import java.util.Map;

2+

3+/**

4+ * The Java back end uses properties

5+ * instead of environment variables.

6+ * This wrapper loads the env variables

7+ * into the standard set of properties.

8+ */

9+public class Reg029Wrapper {

10+ public static void main(String args[]) {

11+ Map<String, String> env = System.getenv();

12+ for (String key : env.keySet()) {

13+ System.setProperty(key, env.get(key));

14+ }

15+ reg029.main(args);

16+ }

17+}

test/reg029/reg029.idr+1

@@ -2,6 +2,7 @@ module Main

2

3import System

4

5+-- necessary to find the getenv symbol

5%dynamic "libm"

6%dynamic "libm"

6

7

7main : IO ()

8main : IO ()

test/reg029/run+12−2

@@ -1,7 +1,17 @@

1#!/usr/bin/env bash

2+

2idris $@ reg029.idr -o reg029

3idris $@ reg029.idr -o reg029

3unset IDRIS_REG029_NONEXISTENT_VAR

4unset IDRIS_REG029_NONEXISTENT_VAR

4export IDRIS_REG029_EXISTENT_VAR='exists!'

5export IDRIS_REG029_EXISTENT_VAR='exists!'

6+

7+IsJava=`echo "$@" | grep -E "\-\-codegen([[:space:]]+)Java\>"`

8+if [ -z "$IsJava" ]

9+then

5−./reg029

10+ ./reg029

11+else

12+ javac -cp reg029:. Reg029Wrapper.java

13+ java -cp reg029:. Reg029Wrapper

14+fi

6idris $@ reg029.idr --execute

15idris $@ reg029.idr --execute

7−rm -f reg029 *.ibc

16+rm -f reg029 *.ibc *.class

17+

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/reg034/expected+2−2

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

1reg034.idr:6:5:When elaborating left hand side of bar:

2When elaborating an application of main.bar:

3 Can't unify

4− [95mx[0m [94m=[0m [95mx[0m

4+ [92mlength[0m [95mys[0m [94m=[0m [92mlength[0m [95mys[0m

5 with

6 [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m [95mys[0m

7

@@ -13,7 +13,7 @@ When elaborating an application of main.bar:

13reg034.idr:9:5:When elaborating left hand side of foo:

14When elaborating an application of main.foo:

15 Can't unify

16− [95mx[0m [94m=[0m [95mx[0m

16+ [95mf[0m [95my[0m [94m=[0m [95mf[0m [95my[0m

17 with

18 [95mf[0m [95mx[0m [94m=[0m [95mf[0m [95my[0m

19

test/reg045/expectednew file+1

@@ -0,0 +1 @@

1+[1, 2, 3]

test/reg045/reg045.idrnew file+19

@@ -0,0 +1,19 @@

1+module Main

2+

3+data ListZ : Type -> Type where

4+ (::) : a -> Lazy (ListZ a) -> ListZ a

5+ Nil : ListZ a

6+

7+instance Show a => Show (ListZ a) where

8+ show xs = "[" ++ show' "" xs ++ "]"

9+ where

10+ show' acc Nil = acc

11+ show' acc (x :: Nil) = acc ++ show x

12+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

13+

14+foo : ListZ Nat

15+foo = (1 :: 2 :: 3 :: Nil)

16+

17+main : IO ()

18+main = print foo

19+

test/reg045/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ reg045.idr -o reg045

3+./reg045

4+rm -f reg045 *.ibc

test/tutorial006/expected+2−2

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

1tutorial006a.idr:3:23:When elaborating right hand side of vapp:

2When elaborating argument [95mxs[0m to constructor [91mPrelude.Vect.::[0m:

3 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mm[0m) [95ma[0m

4+ [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m

5 with

6 [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m

7

8 Specifically:

9 Can't unify

10− [92mplus[0m [95mn[0m [95mm[0m

10+ [92mplus[0m [95mn[0m [95mn[0m

11 with

12 [92mplus[0m [95mn[0m [95mm[0m

13tutorial006b.idr:10:10:When elaborating right hand side of Main.parity: