20e6028 · Idris-dev · git.iko.soy

.travis.yml+6

compare with master

unifiedsplit

@@ -1,4 +1,10 @@

1language: haskell

2+ghc:

3+ # Idris won't build on 7.4 and earlier due to dependency

4+ # problems. 7.10 isn't yet supported on Travis.

5+ - 7.6

6+ - 7.8

7+

2before_install:

8before_install:

3 - sudo add-apt-repository --yes ppa:h-rayflood/llvm

9 - sudo add-apt-repository --yes ppa:h-rayflood/llvm

4 - sudo apt-get update -qq

10 - sudo apt-get update -qq

CHANGELOG+12−1

@@ -8,7 +8,18 @@ New in 0.9.17:

8* Quasiquotation supports the generation of Language.Reflection.Raw terms

9 in addition to Language.Reflection.TT. Types are used for disambiguation,

10 defaulting to TT at the REPL.

11−

11+* Library operators have been renamed for consistency with Haskell. In

12+ particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is

13+ now an alias for Functor.map. Correspondingly, ($>) and (<$) have

14+ been renamed to (<*) and (*>). The cascading effects of this rename

15+ are that Algebra.(<*>) has been renamed to Algebra.(<.>) and

16+ Matrix.(<.>) is now Matrix.(<:>).

17+* Binding forms in DSL notation are now given an extra argument: a

18+ reflected representation of the name that the user chose.

19+ Specifically, the rewritten lambda, pi, and let binders will now get

20+ an extra argument of type TTName. This allows more understandable

21+ dynamic errors in DSL code and more readable code generation results.

22+

12New in 0.9.16:

23New in 0.9.16:

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

24--------------

14* Inductive-inductive definitions are now supported (i.e. simultaneously

25* Inductive-inductive definitions are now supported (i.e. simultaneously

CITATION.mdnew file+29

@@ -0,0 +1,29 @@

1+# Citing `Idris`

2+

3+If you use `Idris` in your work we would prefer it if you would use the following reference in your work.

4+

5+## BibTeX

6+

7+```bibtex

8+@article{JFP:9060502,

9+ author = {BRADY,EDWIN},

10+ title = {Idris, a general-purpose dependently typed programming language: Design and implementation},

11+ journal = {Journal of Functional Programming},

12+ volume = {23},

13+ issue = {05},

14+ month = {9},

15+ year = {2013},

16+ issn = {1469-7653},

17+ pages = {552--593},

18+ numpages = {42},

19+ doi = {10.1017/S095679681300018X},

20+ URL = {http://journals.cambridge.org/article_S095679681300018X},

21+}

22+```

23+

24+## Textual

25+

26+ EDWIN BRADY (2013). Idris, a general-purpose dependently typed

27+ programming language: Design and implementation. Journal of

28+ Functional Programming, 23, pp

29+ 552-593. doi:10.1017/S095679681300018X.

contribs/lib/SQLite3/Makefile+2−3

@@ -7,10 +7,9 @@ sqltest : testunit.idr Sqlite3.idr sqlite3api.o

7 idris testunit.idr -o sqltest

8

9sqlite3api.o : sqlite3api.c

10− gcc -c sqlite3api.c

10+ gcc -I . -c sqlite3api.c

11

12sqlite3api.so: sqlite3api.c

13− gcc -fPIC -o sqlite3api.so -shared sqlite3api.c

13+ gcc -I . -fPIC -o sqlite3api.so -shared sqlite3api.c

14

15all : sqltest sqlite3api.o

16−

contribs/lib/SQLite3/Sqlite3.idr+43−49

@@ -1,8 +1,9 @@

1module Sqlite3

2−import Sqlexpr

2+import public Sqlexpr

3−

4

3

5%lib C "sqlite3"

4%lib C "sqlite3"

5+-- %link C "sqlite3.o"

6+-- %include C "sqlite3.h"

6%link C "sqlite3api.o"

7%link C "sqlite3api.o"

7%include C "sqlite3api.h"

8%include C "sqlite3api.h"

8

9

@@ -47,7 +48,7 @@ instance Functor DB where

47

48

48instance Applicative DB where

49instance Applicative DB where

49 pure = MkDB . return . Right

50 pure = MkDB . return . Right

50− (MkDB f) <$> (MkDB x) = MkDB (do f' <- f

51+ (MkDB f) <*> (MkDB x) = MkDB (do f' <- f

51 case f' of

52 case f' of

52 Left err => return (Left err)

53 Left err => return (Left err)

53 Right op => x >>= (return . map op))

54 Right op => x >>= (return . map op))

@@ -59,7 +60,7 @@ instance Monad DB where

59 Left err => return (Left err)

60 Left err => return (Left err)

60 Right v => case k v of

61 Right v => case k v of

61 MkDB k' => k')

62 MkDB k' => k')

62− return x = MkDB (return (Right x))

63+ --return x = MkDB (return (Right x))

63

64

64fail : String -> DB a

65fail : String -> DB a

65fail err = MkDB (return (Left err))

66fail err = MkDB (return (Left err))

@@ -83,7 +84,7 @@ runDB (MkDB f) = do f' <- f

83-----------------------------------------------------------------------------

84-----------------------------------------------------------------------------

84

85

85open_db : String -> DB DBPointer

86open_db : String -> DB DBPointer

86−open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr) name)

87+open_db name = do x <- liftIO (foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) name)

87 return (MkDBPointer x)

88 return (MkDBPointer x)

88

89

89-----------------------------------------------------------------------------

90-----------------------------------------------------------------------------

@@ -91,7 +92,7 @@ open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr

91-----------------------------------------------------------------------------

92-----------------------------------------------------------------------------

92

93

93close_db : DBPointer -> DB Int

94close_db : DBPointer -> DB Int

94−close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt) pointer)

95+close_db (MkDBPointer pointer) = liftIO (foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) pointer)

95

96

96-----------------------------------------------------------------------------

97-----------------------------------------------------------------------------

97-- | Wrapper around prepare, step and finalize.

98-- | Wrapper around prepare, step and finalize.

@@ -99,7 +100,7 @@ close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FP

99

100

100exec_db : DBPointer -> String -> DB Int

101exec_db : DBPointer -> String -> DB Int

101exec_db (MkDBPointer pointer) stmt = do

102exec_db (MkDBPointer pointer) stmt = do

102− x <- liftIO (mkForeign (FFun "sqlite3_exec_idr" [FPtr, FString] FInt) pointer stmt)

103+ x <- liftIO (foreign FFI_C "sqlite3_exec_idr" (Ptr -> String -> IO Int) pointer stmt)

103 if (x == 1)

104 if (x == 1)

104 then fail "Could not execute."

105 then fail "Could not execute."

105 else return x

106 else return x

@@ -110,7 +111,7 @@ exec_db (MkDBPointer pointer) stmt = do

110

111

111exec_db_v2 : StmtPtr -> DB Int

112exec_db_v2 : StmtPtr -> DB Int

112exec_db_v2 (MkStmtPtr pointer) = do

113exec_db_v2 (MkStmtPtr pointer) = do

113− x <- liftIO (mkForeign (FFun "exec_db" [FPtr] FInt) pointer)

114+ x <- liftIO (foreign FFI_C "exec_db" (Ptr -> IO Int) pointer)

114 if (x == 21)

115 if (x == 21)

115 then fail "No data returned."

116 then fail "No data returned."

116 else return x

117 else return x

@@ -122,8 +123,7 @@ exec_db_v2 (MkStmtPtr pointer) = do

122-----------------------------------------------------------------------------

123-----------------------------------------------------------------------------

123

124

124get_error : DBPointer -> IO String

125get_error : DBPointer -> IO String

125−get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer

126+get_error (MkDBPointer pointer) = foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer

126−

127

128-----------------------------------------------------------------------------

129-- | Compiles the query inot a byte-code program in order to execute it.

@@ -133,7 +133,7 @@ get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FSt

133

134prepare_db : DBPointer -> String -> DB StmtPtr

135prepare_db (MkDBPointer pointer) cmd = do

136− result <- liftIO (mkForeign (FFun "sqlite3_prepare_idr" [FPtr, FString] FPtr) pointer cmd)

136+ result <- liftIO (foreign FFI_C "sqlite3_prepare_idr" (Ptr -> String -> IO Ptr) pointer cmd)

137 flag <- liftIO (nullPtr result)

138 if flag

139 then fail "Error occured while preparing"

@@ -147,8 +147,8 @@ prepare_db (MkDBPointer pointer) cmd = do

147

148step_db : StmtPtr -> DB Int

149step_db (MkStmtPtr pointer)= do

150− x <- liftIO (mkForeign (FFun "sqlite3_step_idr" [FPtr] FInt)pointer)

150+ x <- liftIO (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) pointer)

151− if ( x == 101)

151+ if (x == 101)

152 then fail "SQLITE_DONE"

153 else return x

154

@@ -159,7 +159,7 @@ step_db (MkStmtPtr pointer)= do

159

160finalize_db : StmtPtr -> DB Int

161finalize_db (MkStmtPtr pointer) = do

162− x <- liftIO (mkForeign (FFun "sqlite3_finalize_idr" [FPtr] FInt) pointer)

162+ x <- liftIO (foreign FFI_C "sqlite3_finalize_idr" (Ptr -> IO Int) pointer)

163 if (x /= 0)

164 then fail "Could not finalize"

165 else return x

@@ -170,7 +170,7 @@ finalize_db (MkStmtPtr pointer) = do

170

171reset_db : StmtPtr -> DB Int

172reset_db (MkStmtPtr pointer) = do

173− x <- liftIO (mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt) pointer)

173+ x <- liftIO (foreign FFI_C "sqlite3_reset_idr" (Ptr -> IO Int) pointer)

174 if (x /= 0)

175 then fail "Could not reset"

176 else return x

@@ -181,38 +181,34 @@ reset_db (MkStmtPtr pointer) = do

181

182column_count : DBPointer -> IO (Either String Int)

183column_count (MkDBPointer pointer) = do

184− x <- mkForeign (FFun "sqlite3_column_count_idr" [FPtr] FInt) pointer

184+ x <- foreign FFI_C "sqlite3_column_count_idr" (Ptr -> IO Int) pointer

185− return $ if (x == 0 )

185+ return $ if (x == 0)

186 then Left "No Data"

187 else (Right x)

188

189column_name : DBPointer -> Int -> IO String

190column_name (MkDBPointer pointer) iCol =

191− mkForeign (FFun "sqlite3_column_name_idr" [FPtr, FInt] FString) pointer iCol

191+ foreign FFI_C "sqlite3_column_name_idr" (Ptr -> Int -> IO String) pointer iCol

192

193column_decltype : DBPointer -> Int -> IO String

194column_decltype (MkDBPointer pointer) iCol =

195− mkForeign (FFun "sqlite3_column_decltype_idr" [FPtr, FInt] FString) pointer iCol

195+ foreign FFI_C "sqlite3_column_decltype_idr" (Ptr -> Int -> IO String) pointer iCol

196−

197

196

198column_bytes : DBPointer -> Int -> IO Int

197column_bytes : DBPointer -> Int -> IO Int

199column_bytes (MkDBPointer pointer) iCol =

198column_bytes (MkDBPointer pointer) iCol =

200− mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt) pointer iCol

199+ foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) pointer iCol

201−

202

200

203column_blob : DBPointer -> Int -> IO String

201column_blob : DBPointer -> Int -> IO String

204column_blob (MkDBPointer pointer) iCol =

202column_blob (MkDBPointer pointer) iCol =

205− mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FString) pointer iCol

203+ foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO String) pointer iCol

206−

207

204

208column_text : DBPointer -> Int -> IO String

205column_text : DBPointer -> Int -> IO String

209column_text (MkDBPointer pointer) iCol =

206column_text (MkDBPointer pointer) iCol =

210− mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString) pointer iCol

207+ foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) pointer iCol

211−

212

208

213column_Int : DBPointer -> Int -> IO Int

209column_Int : DBPointer -> Int -> IO Int

214column_Int (MkDBPointer pointer) iCol =

210column_Int (MkDBPointer pointer) iCol =

215− mkForeign (FFun "sqlite3_column_int_idr" [FPtr, FInt] FInt) pointer iCol

211+ foreign FFI_C "sqlite3_column_int_idr" (Ptr -> Int -> IO Int) pointer iCol

216

212

217-----------------------------------------------------------------------------

213-----------------------------------------------------------------------------

218-- | These routines support some of SQLite backup functions.

214-- | These routines support some of SQLite backup functions.

@@ -220,22 +216,21 @@ column_Int (MkDBPointer pointer) iCol =

220

216

221backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer

217backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer

222backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =

218backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =

223− do x <- mkForeign (FFun "sqlite3_backup_init_idr" [FPtr,FString, FPtr, FString] FPtr)

219+ do x <- foreign FFI_C "sqlite3_backup_init_idr" (Ptr -> String -> Ptr -> String -> IO Ptr)

224 des_pointer destName src_pointer srcName

220 des_pointer destName src_pointer srcName

225 return (MkDBPointer x)

221 return (MkDBPointer x)

226

222

227backup_step : DBPointer -> Int -> IO Int

223backup_step : DBPointer -> Int -> IO Int

228backup_step (MkDBPointer pointer) nPage =

224backup_step (MkDBPointer pointer) nPage =

229− mkForeign (FFun "sqlite3_backup_step_idr" [FPtr, FInt] FInt) pointer nPage

225+ foreign FFI_C "sqlite3_backup_step_idr" (Ptr -> Int -> IO Int) pointer nPage

230

226

231backup_finish : DBPointer -> IO Int

227backup_finish : DBPointer -> IO Int

232backup_finish (MkDBPointer pointer) =

228backup_finish (MkDBPointer pointer) =

233− mkForeign (FFun "sqlite3_backup_finish_idr" [FPtr] FInt) pointer

229+ foreign FFI_C "sqlite3_backup_finish_idr" (Ptr -> IO Int) pointer

234

230

235backup_remaining : DBPointer -> IO Int

231backup_remaining : DBPointer -> IO Int

236backup_remaining (MkDBPointer pointer) =

232backup_remaining (MkDBPointer pointer) =

237− mkForeign (FFun "sqlite3_backup_remaining_idr" [FPtr] FInt) pointer

233+ foreign FFI_C "sqlite3_backup_remaining_idr" (Ptr -> IO Int) pointer

238−

239

234

240-----------------------------------------------------------------------------

235-----------------------------------------------------------------------------

241-- | Use of this interface is not recommended.

236-- | Use of this interface is not recommended.

@@ -246,19 +241,18 @@ backup_remaining (MkDBPointer pointer) =

246

241

247get_table : DBPointer -> String -> DB TBPointer

242get_table : DBPointer -> String -> DB TBPointer

248get_table (MkDBPointer pointer) name = do

243get_table (MkDBPointer pointer) name = do

249− x <- liftIO(mkForeign (FFun "sqlite3_get_table_idr" [FPtr, FString] FPtr) pointer name)

244+ x <- liftIO(foreign FFI_C "sqlite3_get_table_idr" (Ptr -> String -> IO Ptr) pointer name)

250 flag <- liftIO (nullPtr x)

245 flag <- liftIO (nullPtr x)

251 if flag

246 if flag

252 then do x <- liftIO(get_error_table pointer) ; fail x

247 then do x <- liftIO(get_error_table pointer) ; fail x

253 else return (MkTBPointer x)

248 else return (MkTBPointer x)

254 where

249 where

255 get_error_table : Ptr-> IO String

250 get_error_table : Ptr-> IO String

256− get_error_table pointer = do x <- mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer

251+ get_error_table pointer = do x <- foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer

257 return x

252 return x

258

253

259−

260free_table : TBPointer -> IO ()

254free_table : TBPointer -> IO ()

261−free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_idr" [FPtr] FUnit) pointer

255+free_table (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_free_table_idr" (Ptr -> IO ()) pointer

262 return ()

256 return ()

263

257

264-----------------------------------------------------------------------------

258-----------------------------------------------------------------------------

@@ -267,11 +261,11 @@ free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_i

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

261-----------------------------------------------------------------------------

268

262

269num_row : TBPointer -> IO Int

263num_row : TBPointer -> IO Int

270−num_row (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row" [FPtr] FInt) pointer

264+num_row (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row" (Ptr -> IO Int) pointer

271 return x

265 return x

272

266

273num_col : TBPointer -> IO Int

267num_col : TBPointer -> IO Int

274−num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [FPtr] FInt) pointer

268+num_col (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col" (Ptr -> IO Int) pointer

275 return x

269 return x

276

270

277-----------------------------------------------------------------------------

271-----------------------------------------------------------------------------

@@ -280,11 +274,11 @@ num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [F

280-----------------------------------------------------------------------------

274-----------------------------------------------------------------------------

281

275

282num_row_v2 : DBPointer -> IO Int

276num_row_v2 : DBPointer -> IO Int

283−num_row_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row_v2" [FPtr] FInt) pointer

277+num_row_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row_v2" (Ptr -> IO Int) pointer

284 return x

278 return x

285

279

286num_col_v2 : DBPointer -> IO Int

280num_col_v2 : DBPointer -> IO Int

287−num_col_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col_v2" [FPtr] FInt) pointer

281+num_col_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col_v2" (Ptr -> IO Int) pointer

288 return x

282 return x

289

283

290-----------------------------------------------------------------------------

284-----------------------------------------------------------------------------

@@ -299,18 +293,18 @@ get_data (MkDBPointer pointer) row col = do

299 helper ty

293 helper ty

300 where get_data_type : Ptr ->Int -> Int -> IO Int

294 where get_data_type : Ptr ->Int -> Int -> IO Int

301 get_data_type pointer row col =

295 get_data_type pointer row col =

302− mkForeign (FFun "sqlite3_get_data_type" [FPtr, FInt, FInt] FInt) pointer row col

296+ foreign FFI_C "sqlite3_get_data_type" (Ptr -> Int -> Int -> IO Int) pointer row col

303 get_data_val_int : Ptr -> Int -> IO Int

297 get_data_val_int : Ptr -> Int -> IO Int

304 get_data_val_int pointer col =

298 get_data_val_int pointer col =

305− mkForeign (FFun "sqlite3_get_val_int" [FPtr,FInt] FInt) pointer col

299+ foreign FFI_C "sqlite3_get_val_int" (Ptr -> Int -> IO Int) pointer col

306

300

307 get_data_val_text : Ptr -> Int -> IO String

301 get_data_val_text : Ptr -> Int -> IO String

308 get_data_val_text pointer col =

302 get_data_val_text pointer col =

309− mkForeign (FFun "sqlite3_get_val_text" [FPtr, FInt] FString) pointer col

303+ foreign FFI_C "sqlite3_get_val_text" (Ptr -> Int -> IO String) pointer col

310

304

311 get_data_val_float : Ptr -> Int -> IO Float

305 get_data_val_float : Ptr -> Int -> IO Float

312 get_data_val_float pointer col =

306 get_data_val_float pointer col =

313− mkForeign (FFun "sqlite3_get_float" [FPtr, FInt] FFloat) pointer col

307+ foreign FFI_C "sqlite3_get_float" (Ptr -> Int -> IO Float) pointer col

314

308

315 helper : Int -> IO DBVal

309 helper : Int -> IO DBVal

316 helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)

310 helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)

@@ -360,7 +354,7 @@ strcat str1 str2 = str1 ++ str2

360

354

361bind_int : StmtPtr -> Int -> Int -> DB StmtPtr

355bind_int : StmtPtr -> Int -> Int -> DB StmtPtr

362bind_int (MkStmtPtr pointer) indexval val = do

356bind_int (MkStmtPtr pointer) indexval val = do

363− x <- liftIO (mkForeign (FFun "sqlite3_bind_int_idr" [FPtr, FInt, FInt] FPtr) pointer indexval val)

357+ x <- liftIO (foreign FFI_C "sqlite3_bind_int_idr" (Ptr -> Int -> Int -> IO Ptr) pointer indexval val)

364 flag <- liftIO (nullPtr x)

358 flag <- liftIO (nullPtr x)

365 if flag

359 if flag

366 then fail "Could not bind int."

360 then fail "Could not bind int."

@@ -369,7 +363,7 @@ bind_int (MkStmtPtr pointer) indexval val = do

369

363

370bind_float : StmtPtr -> Int -> Float -> DB StmtPtr

364bind_float : StmtPtr -> Int -> Float -> DB StmtPtr

371bind_float (MkStmtPtr pointer) indexval val = do

365bind_float (MkStmtPtr pointer) indexval val = do

372− x <- liftIO (mkForeign (FFun "sqlite3_bind_float_idr" [FPtr, FInt, FFloat] FPtr) pointer indexval val)

366+ x <- liftIO (foreign FFI_C "sqlite3_bind_float_idr" (Ptr -> Int -> Float -> IO Ptr) pointer indexval val)

373 flag <- liftIO (nullPtr x)

367 flag <- liftIO (nullPtr x)

374 if flag

368 if flag

375 then fail "Could not bind float."

369 then fail "Could not bind float."

@@ -377,7 +371,7 @@ bind_float (MkStmtPtr pointer) indexval val = do

377

371

378bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr

372bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr

379bind_text (MkStmtPtr pointer) text indexval lengthval = do

373bind_text (MkStmtPtr pointer) text indexval lengthval = do

380− x <- liftIO (mkForeign (FFun "sqlite3_bind_text_idr" [FPtr, FString, FInt, FInt] FPtr)

374+ x <- liftIO (foreign FFI_C "sqlite3_bind_text_idr" (Ptr -> String -> Int -> Int -> IO Ptr)

381 pointer text indexval lengthval)

375 pointer text indexval lengthval)

382 flag <- liftIO(nullPtr x)

376 flag <- liftIO(nullPtr x)

383 if flag

377 if flag

@@ -386,7 +380,7 @@ bind_text (MkStmtPtr pointer) text indexval lengthval = do

386

380

387bind_null : StmtPtr -> Int -> DB StmtPtr

381bind_null : StmtPtr -> Int -> DB StmtPtr

388bind_null (MkStmtPtr pointer) indexval = do

382bind_null (MkStmtPtr pointer) indexval = do

389− x <- liftIO (mkForeign (FFun "sqlite3_bind_null_idr" [FPtr, FInt] FPtr) pointer indexval)

383+ x <- liftIO (foreign FFI_C "sqlite3_bind_null_idr" (Ptr -> Int -> IO Ptr) pointer indexval)

390 flag <- liftIO (nullPtr x)

384 flag <- liftIO (nullPtr x)

391 if flag

385 if flag

392 then fail "Could not bind null."

386 then fail "Could not bind null."

@@ -397,7 +391,7 @@ bind_null (MkStmtPtr pointer) indexval = do

397-----------------------------------------------------------------------------

391-----------------------------------------------------------------------------

398

392

399strlen : String -> DB Int

393strlen : String -> DB Int

400−strlen str = liftIO (mkForeign (FFun "strLength" [FString] FInt) str)

394+strlen str = liftIO (foreign FFI_C "strLength" (String -> IO Int) str)

401

395

402instance Show DBVal where

396instance Show DBVal where

403 show (DBInt i) = "Int val: " ++ show i ++ "\n"

397 show (DBInt i) = "Int val: " ++ show i ++ "\n"

contribs/lib/SimpleParser/SimpleParser.idr+1−1

@@ -30,7 +30,7 @@ instance Functor Parser where

30

31instance Applicative Parser where

32 pure v = P (\inp => Right (v, inp))

33− a <$> b = P (\inp => do (f, rest) <- parse a inp

33+ a <*> b = P (\inp => do (f, rest) <- parse a inp

34 (x, rest') <- parse b rest

35 pure ((f x), rest'))

36

libs/base/Control/Arrow.idr+1−1

@@ -95,7 +95,7 @@ instance Arrow a => Functor (ArrowMonad a) where

95

96instance Arrow a => Applicative (ArrowMonad a) where

97 pure x = MkArrowMonad $ arrow $ \_ => x

98− (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

98+ (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

99

100instance ArrowApply a => Monad (ArrowMonad a) where

101 (MkArrowMonad m) >>= f =

libs/base/Control/IOExcept.idr+2−2

@@ -10,8 +10,8 @@ instance Functor (IOExcept e) where

10

11instance Applicative (IOExcept e) where

12 pure x = ioM (pure (pure x))

13− (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a

13+ (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a

14− return (f' <$> a'))

14+ return (f' <*> a'))

15

16instance Monad (IOExcept e) where

17 (ioM x) >>= k = ioM (do x' <- x;

libs/base/Control/Monad/Identity.idr+1−1

@@ -9,7 +9,7 @@ instance Functor Identity where

9instance Applicative Identity where

10 pure x = Id x

11

12− (Id f) <$> (Id g) = Id (f g)

12+ (Id f) <*> (Id g) = Id (f g)

13

14instance Monad Identity where

15 (Id x) >>= k = k x

libs/base/Control/Monad/RWS.idr+1−1

@@ -21,7 +21,7 @@ instance Monad m => Functor (RWST r w s m) where

21

22instance (Monoid w, Monad m) => Applicative (RWST r w s m) where

23 pure a = MkRWST $ \_,s => return (a, s, neutral)

24− (MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

24+ (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

25 (fn, ss, w') <- f r s

26 return (fn a, ss, w <+> w)

27

libs/base/Control/Monad/Reader.idr+1−1

@@ -27,7 +27,7 @@ instance Functor f => Functor (ReaderT r f) where

27

28instance Applicative m => Applicative (ReaderT r m) where

29 pure = liftReaderT . pure

30− (RD f) <$> (RD v) = RD $ \r => f r <$> v r

30+ (RD f) <*> (RD v) = RD $ \r => f r <*> v r

31

32instance Alternative m => Alternative (ReaderT r m) where

33 empty = liftReaderT empty

libs/base/Control/Monad/State.idr+1−1

@@ -25,7 +25,7 @@ instance Functor f => Functor (StateT s f) where

25instance Monad f => Applicative (StateT s f) where

26 pure x = ST (\st => pure (x, st))

27

28− (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st

28+ (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st

29 (b, t) <- a r

30 return (g b, t))

31

libs/base/Control/Monad/Writer.idr+1−1

@@ -25,7 +25,7 @@ instance Functor f => Functor (WriterT w f) where

25

26instance (Monoid w, Applicative m) => Applicative (WriterT w m) where

27 pure a = WR $ pure (a, neutral)

28− (WR f) <$> (WR v) = WR $ liftA2 merge f v where

28+ (WR f) <*> (WR v) = WR $ liftA2 merge f v where

29 merge (fn, w) (a, w') = (fn a, w <+> w')

30

31instance (Monoid w, Alternative m) => Alternative (WriterT w m) where

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

@@ -16,7 +16,7 @@ instance Functor Erased where

16

17instance Applicative Erased where

18 pure = Erase

19− (<$>) (Erase f) (Erase x) = Erase (f x)

19+ (<*>) (Erase f) (Erase x) = Erase (f x)

20

21instance Monad Erased where

22 (>>=) (Erase x) f = f x

libs/base/Data/Matrix.idr+29−29

@@ -7,13 +7,13 @@ import Data.Vect

7

8%default total

9

10−infixr 2 <.> -- vector inner product

10+infixr 2 <:> -- vector inner product

11infixr 2 >< -- vector outer product

12infixr 2 <<>> -- matrix commutator

13infixr 2 >><< -- matrix anticommutator

14infixl 3 <\> -- row times a matrix

15infixr 4 </> -- matrix times a column

16−infixr 5 <> -- matrix multiplication

16+infixr 5 <> -- matrix multiplication

17infixr 7 \&\ -- vector tensor product

18infixr 7 <&> -- matrix tensor product

19

@@ -26,14 +26,14 @@ instance Semigroup a => Semigroup (Vect n a) where

26

27instance Monoid a => Monoid (Vect n a) where

28 neutral {n} = replicate n neutral

29−

29+

30instance Group a => Group (Vect n a) where

31 inverse = map inverse

32

33instance AbelianGroup a => AbelianGroup (Vect n a) where {}

34

35instance Ring a => Ring (Vect n a) where

36− (<*>) v w = zipWith (<*>) v w

36+ (<.>) v w = zipWith (<.>) v w

37

38instance RingWithUnity a => RingWithUnity (Vect n a) where

39 unity {n} = replicate n unity

@@ -42,7 +42,7 @@ instance Field a => Field (Vect n a) where

42 inverseM = map inverseM

43

44instance RingWithUnity a => Module a (Vect n a) where

45− (<#>) r v = map (r <*>) v

45+ (<#>) r v = map (r <.>) v

46

47instance RingWithUnity a => Module a (Vect n (Vect l a)) where

48 (<#>) r m = map (r <#>) m

@@ -53,12 +53,12 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where

53-----------------------------------------------------------------------

54

55||| Inner product of ring vectors

56−(<.>) : Ring a => Vect n a -> Vect n a -> a

56+(<:>) : Ring a => Vect n a -> Vect n a -> a

57−(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)

57+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)

58

59||| Tensor multiply (⊗) ring vectors

60(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a

61−(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where

61+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where

62 orep : (n : Nat) -> Vect m a -> Vect (n * m) a

63 orep n v = concat $ replicate n v

64 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a

@@ -90,15 +90,15 @@ indices f1 f2 m = index f2 (index f1 m)

90

91||| Matrix times a column vector

92(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a

93−(</>) m v = map (v <.>) m

93+(</>) m v = map (v <:>) m

94

95||| Matrix times a row vector

96(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a

97−(<\>) r m = map (r <.>) $ transpose m

97+(<\>) r m = map (r <:>) $ transpose m

98

99||| Matrix multiplication

100−(<>) : Ring a => Matrix n k a ->

100+(<>) : Ring a => Matrix n k a ->

101− Matrix k m a ->

101+ Matrix k m a ->

102 Matrix n m a

103(<>) m1 m2 = map (<\> m2) m1

104

@@ -110,11 +110,11 @@ indices f1 f2 m = index f2 (index f1 m)

110 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a

111 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2

112

113−||| Cast a vector from a standard Vect to a proper n x 1 matrix

113+||| Cast a vector from a standard Vect to a proper n x 1 matrix

114col : Vect n a -> Matrix n 1 a

115col v = map (\x => [x]) v

116

117−||| Cast a row from a standard Vect to a proper 1 x n matrix

117+||| Cast a row from a standard Vect to a proper 1 x n matrix

118row : Vect n a -> Matrix 1 n a

119row r = [r]

120

@@ -157,11 +157,11 @@ instance Monoid Integer where

157

158instance Group Integer where

159 inverse = (* -1)

160−

160+

161instance AbelianGroup Integer

162

163−instance Ring Integer where

163+instance Ring Integer where

164− (<*>) = (*)

164+ (<.>) = (*)

165

166instance RingWithUnity Integer where

167 unity = 1

@@ -175,11 +175,11 @@ instance Monoid Int where

175

176instance Group Int where

177 inverse = (* -1)

178−

178+

179instance AbelianGroup Int

180

181−instance Ring Int where

181+instance Ring Int where

182− (<*>) = (*)

182+ (<.>) = (*)

183

184instance RingWithUnity Int where

185 unity = 1

@@ -193,11 +193,11 @@ instance Monoid Float where

193

194instance Group Float where

195 inverse = (* -1)

196−

196+

197instance AbelianGroup Float

198

199−instance Ring Float where

199+instance Ring Float where

200− (<*>) = (*)

200+ (<.>) = (*)

201

202instance RingWithUnity Float where

203 unity = 1

@@ -211,7 +211,7 @@ instance Semigroup Nat where

211

212instance Monoid Nat where

213 neutral = 0

214−

214+

215instance VerifiedSemigroup Nat where

216 semigroupOpIsAssociative = plusAssociative

217

@@ -228,12 +228,12 @@ instance Monoid ZZ where

228

229instance Group ZZ where

230 inverse = (* -1)

231−

231+

232instance AbelianGroup ZZ

233

234−instance Ring ZZ where

234+instance Ring ZZ where

235− (<*>) = (*)

235+ (<.>) = (*)

236−

236+

237instance RingWithUnity ZZ where

238 unity = 1

239

@@ -250,7 +250,7 @@ instance Group a => Group (Complex a) where

250instance Ring a => AbelianGroup (Complex a) where {}

251

252instance Ring a => Ring (Complex a) where

253− (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)

253+ (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)

254

255instance RingWithUnity a => RingWithUnity (Complex a) where

256 unity = (unity :+ neutral)

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

@@ -25,7 +25,7 @@ instance Functor (Morphism r) where

25

26instance Applicative (Morphism r) where

27 pure a = Mor $ const a

28− (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r

28+ (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r

29

30instance Monad (Morphism r) where

31 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r

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

@@ -529,7 +529,7 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

529instance Applicative (Vect k) where

530 pure = replicate _

531

532− fs <$> vs = zipWith apply fs vs

532+ fs <*> vs = zipWith apply fs vs

533

534instance Monad (Vect n) where

535 m >>= f = diag (map f m)

libs/base/Network/Cgi.idr+1−1

@@ -36,7 +36,7 @@ instance Functor CGI where

36instance Applicative CGI where

37 pure v = MkCGI (\s => return (v, s))

38

39− (MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

39+ (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

40 (c, j) <- b i

41 return (f c, j))

42

libs/base/Providers.idr+3−3

@@ -17,9 +17,9 @@ instance Functor Provider where

17 map f (Error err) = Error err

18

19instance Applicative Provider where

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

20+ (Provide f) <*> (Provide x) = Provide (f x)

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

21+ (Provide f) <*> (Error err) = Error err

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

22+ (Error err) <*> _ = Error err

23 pure = Provide

24

25instance Monad Provider where

libs/base/System/Concurrency/Process.idr+1−1

@@ -19,7 +19,7 @@ instance Functor (Process msg) where

19

20instance Applicative (Process msg) where

21 pure = Lift . return

22− (Lift f) <$> (Lift a) = Lift (f <$> a)

22+ (Lift f) <*> (Lift a) = Lift (f <*> a)

23

24instance Monad (Process msg) where

25 (Lift io) >>= k = Lift (do x <- io

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

@@ -24,11 +24,11 @@ data RawMemory : Effect where

24 (size : Nat) ->

25 So (offset + size <= i) ->

26 RawMemory (Vect size Bits8)

27− (MemoryChunk n i) (\v => MemoryChunk n i)

27+ (MemoryChunk n i) (\v => MemoryChunk n i)

28 Poke : (offset : Nat) ->

29 (Vect size Bits8) ->

30 So (offset <= i && offset + size <= n) ->

31− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

31+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

32 Move : (src : MemoryChunk src_size src_init) ->

33 (dst_offset : Nat) ->

34 (src_offset : Nat) ->

@@ -36,8 +36,8 @@ data RawMemory : Effect where

36 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

37 So (src_offset + size <= src_init) ->

38 RawMemory () (MemoryChunk dst_size dst_init)

39− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

39+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

40− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

40+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

41

42private

43do_malloc : Nat -> IOExcept String Ptr

@@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where

84 = do ptr <- do_malloc n

85 k () (CH ptr)

86 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k

87− = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)

87+ = ioe_lift (do_memset ptr i c size) *> k () (CH ptr)

88 handle (CH ptr) (Free) k

89− = ioe_lift (do_free ptr) $> k () ()

89+ = ioe_lift (do_free ptr) *> k () ()

90 handle (CH ptr) (Peek offset size _) k

91 = do res <- ioe_lift (do_peek ptr offset size)

92 k res (CH ptr)

@@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where

102RAW_MEMORY : Type -> EFFECT

103RAW_MEMORY t = MkEff t RawMemory

104

105−allocate : (n : Nat) ->

105+allocate : (n : Nat) ->

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

107allocate size = call $ Allocate size

108

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

111 Bits8 ->

112 (size : Nat) ->

113 So (i + size <= n) ->

114− Eff () [RAW_MEMORY (MemoryChunk n i)]

114+ Eff () [RAW_MEMORY (MemoryChunk n i)]

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

116initialize c size prf = call $ Initialize c size prf

117

@@ -122,7 +122,7 @@ peek : {i : Nat} ->

122 (offset : Nat) ->

123 (size : Nat) ->

124 So (offset + size <= i) ->

125− { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

125+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

126peek offset size prf = call $ Peek offset size prf

127

128poke : {n : Nat} ->

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

130 (offset : Nat) ->

131 Vect size Bits8 ->

132 So (offset <= i && offset + size <= n) ->

133− Eff () [RAW_MEMORY (MemoryChunk n i)]

133+ Eff () [RAW_MEMORY (MemoryChunk n i)]

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

135poke offset content prf = call $ Poke offset content prf

136

137private

138−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)

138+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)

139getRawPtr = call $ GetRawPtr

140

141private

@@ -173,5 +173,5 @@ move : {dst_size : Nat} ->

173move dst_offset src_offset size dst_bounds src_bounds

174 = do src_ptr <- Src :- getRawPtr

175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

176− return ()

176+ return ()

177

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

@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)

11

12 instance Applicative (\a => EffM m a xs (\v => xs)) where

13 pure = value

14− (<$>) f a = do f' <- f

14+ (<*>) f a = do f' <- f

15 a' <- a

16 value (f' a')

17

libs/effects/Effects.idr+3−3

@@ -174,7 +174,7 @@ return x = value x

174

175-- ------------------------------------------------------ [ for idiom brackets ]

176

177−infixl 2 <$>

177+infixl 2 <*>

178

179pure : a -> Eff a xs (\v => xs)

180pure = value

@@ -182,9 +182,9 @@ pure = value

182pureM : (val : a) -> Eff a (xs val) xs

183pureM = value

184

185−(<$>) : Eff (a -> b) xs (\v => xs) ->

185+(<*>) : Eff (a -> b) xs (\v => xs) ->

186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)

187−(<$>) prog v = do fn <- prog

187+(<*>) prog v = do fn <- prog

188 arg <- v

189 return (fn arg)

190

libs/oldeffects/Effect/Monad.idr+1−1

@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)

11

12 instance Applicative (\a => EffM m a xs (\v => xs)) where

13 pure = value

14− (<$>) f a = do f' <- f

14+ (<*>) f a = do f' <- f

15 a' <- a

16 value (f' a')

17

libs/oldeffects/Effects.idr+3−3

@@ -185,16 +185,16 @@ return x = value x

185

186-- ------------------------------------------------------ [ for idiom brackets ]

187

188−infixl 2 <$>

188+infixl 2 <*>

189

190pure : a -> Eff m a xs (\v => xs)

191pure = value

192

193syntax pureM [val] = with_val val (pure ())

194

195−(<$>) : Eff m (a -> b) xs (\v => xs) ->

195+(<*>) : Eff m (a -> b) xs (\v => xs) ->

196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

197−(<$>) prog v = do fn <- prog

197+(<*>) prog v = do fn <- prog

198 arg <- v

199 return (fn arg)

200

libs/prelude/Language/Reflection/Tactical.idr+1−1

@@ -45,7 +45,7 @@ instance Functor Tactical where

45

46instance Applicative Tactical where

47 pure x = prim__PureTactical x

48− f <$> x = prim__BindTactical f $ \g =>

48+ f <*> x = prim__BindTactical f $ \g =>

49 prim__BindTactical x $ \y =>

50 prim__PureTactical $ g y

51

libs/prelude/Prelude.idr+8−8

@@ -249,31 +249,31 @@ instance Functor (Either e) where

249instance Applicative PrimIO where

250 pure = prim_io_return

251

252− am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

252+ am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

253

254instance Applicative (IO' ffi) where

255 pure x = io_return x

256− f <$> a = io_bind f (\f' =>

256+ f <*> a = io_bind f (\f' =>

257 io_bind a (\a' =>

258 io_return (f' a')))

259

260instance Applicative Maybe where

261 pure = Just

262

263− (Just f) <$> (Just a) = Just (f a)

263+ (Just f) <*> (Just a) = Just (f a)

264− _ <$> _ = Nothing

264+ _ <*> _ = Nothing

265

266instance Applicative (Either e) where

267 pure = Right

268

269− (Left a) <$> _ = Left a

269+ (Left a) <*> _ = Left a

270− (Right f) <$> (Right r) = Right (f r)

270+ (Right f) <*> (Right r) = Right (f r)

271− (Right _) <$> (Left l) = Left l

271+ (Right _) <*> (Left l) = Left l

272

273instance Applicative List where

274 pure x = [x]

275

276− fs <$> vs = concatMap (\f => map f vs) fs

276+ fs <*> vs = concatMap (\f => map f vs) fs

277

278---- Alternative instances

279

libs/prelude/Prelude/Algebra.idr+37−37

@@ -5,7 +5,7 @@ import Builtins

5-- XXX: change?

6infixl 6 <->

7infixl 6 <+>

8−infixl 6 <*>

8+infixl 6 <.>

9infixl 5 <#>

10

11%access public

@@ -96,18 +96,18 @@ class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

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

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

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

99−||| + Associativity of `<*>`:

99+||| + Associativity of `<.>`:

100−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

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

101−||| + Distributivity of `<*>` and `<->`:

101+||| + Distributivity of `<.>` and `<->`:

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

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

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

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

104class AbelianGroup a => Ring a where

105− (<*>) : a -> a -> a

105+ (<.>) : a -> a -> a

106

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

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

108+ total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r

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

109+ total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

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

110+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

111

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

113||| supplied with a neutral element, and the other associative supplied with a

@@ -124,20 +124,20 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

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

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

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

127−||| + Associativity of `<*>`:

127+||| + Associativity of `<.>`:

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

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

129−||| + Neutral for `<*>`:

129+||| + Neutral for `<.>`:

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

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

131−||| forall a, unity <*> a == a

131+||| forall a, unity <.> a == a

132−||| + Distributivity of `<*>` and `<->`:

132+||| + Distributivity of `<.>` and `<->`:

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

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

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

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

135class Ring a => RingWithUnity a where

136 unity : a

137

138class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

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

139+ total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l

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

140+ total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r

141

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

143||| idempotent. Must satisfy the following laws:

@@ -281,31 +281,31 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif

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

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

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

284−||| + Associativity of `<*>`:

284+||| + Associativity of `<.>`:

285−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

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

286−||| + Unity for `<*>`:

286+||| + Unity for `<.>`:

287−||| forall a, a <*> unity == a

287+||| forall a, a <.> unity == a

288−||| forall a, unity <*> a == a

288+||| forall a, unity <.> a == a

289−||| + InverseM of `<*>`:

289+||| + InverseM of `<.>`:

290−||| forall a, a <*> inverseM a == unity

290+||| forall a, a <.> inverseM a == unity

291−||| forall a, inverseM a <*> a == unity

291+||| forall a, inverseM a <.> a == unity

292−||| + Distributivity of `<*>` and `<->`:

292+||| + Distributivity of `<.>` and `<->`:

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

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

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

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

295class RingWithUnity a => Field a where

296 inverseM : a -> a

297

298class (VerifiedRing a, Field a) => VerifiedField a where

299− total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity

299+ total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity

300− total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity

300+ total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity

301

302||| A module over a ring is an additive abelian group of 'vectors' endowed with a

303−||| scale operation multiplying vectors by ring elements, and distributivity laws

303+||| scale operation multiplying vectors by ring elements, and distributivity laws

304−||| relating the scale operation to both ring addition and module addition.

304+||| relating the scale operation to both ring addition and module addition.

305||| Must satisfy the following laws:

306|||

307||| + Compatibility of scalar multiplication with ring multiplication:

308−||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v

308+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v

309||| + Ring unity is the identity element of scalar multiplication:

310||| forall v, unity <#> v = v

311||| + Distributivity of `<#>` and `<+>`:

@@ -315,7 +315,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where

315 (<#>) : a -> b -> b

316

317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

318− total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v

318+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

319 total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v

320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

libs/prelude/Prelude/Applicative.idr+17−17

@@ -9,46 +9,46 @@ import Prelude.Functor

9

10---- Applicative functors/Idioms

11

12−infixl 2 <$>

12+infixl 2 <*>

13

14class Functor f => Applicative (f : Type -> Type) where

15 pure : a -> f a

16− (<$>) : f (a -> b) -> f a -> f b

16+ (<*>) : f (a -> b) -> f a -> f b

17

18instance Applicative id where

19 pure a = a

20− f <$> a = f a

20+ f <*> a = f a

21

22class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

23 applicativeMap : (x : f a) -> (g : a -> b) ->

24− map g x = pure g <$> x

24+ map g x = pure g <*> x

25− applicativeIdentity : (x : f a) -> pure id <$> x = x

25+ applicativeIdentity : (x : f a) -> pure id <*> x = x

26 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

27− ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)

27+ ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

28 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

29− (<$>) {f} (pure g) (pure x) = pure {f} (g x)

29+ (<*>) {f} (pure g) (pure x) = pure {f} (g x)

30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

31− g <$> pure x = pure (\g' : a -> b => g' x) <$> g

31+ g <*> pure x = pure (\g' : a -> b => g' x) <*> g

32

33−infixl 2 <$

33+infixl 2 <*

34−(<$) : Applicative f => f a -> f b -> f a

34+(<*) : Applicative f => f a -> f b -> f a

35−a <$ b = map const a <$> b

35+a <* b = map const a <*> b

36

37−infixl 2 $>

37+infixl 2 *>

38−($>) : Applicative f => f a -> f b -> f b

38+(*>) : Applicative f => f a -> f b -> f b

39−a $> b = map (const id) a <$> b

39+a *> b = map (const id) a <*> b

40

41||| Lift a function to an applicative

42liftA : Applicative f => (a -> b) -> f a -> f b

43−liftA f a = pure f <$> a

43+liftA f a = pure f <*> a

44

45||| Lift a two-argument function to an applicative

46liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

47−liftA2 f a b = (map f a) <$> b

47+liftA2 f a b = (map f a) <*> b

48

49||| Lift a three-argument function to an applicative

50liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

51−liftA3 f a b c = (map f a) <$> b <$> c

51+liftA3 f a b c = (map f a) <*> b <*> c

52

53infixl 3 <|>

54class Applicative f => Alternative (f : Type -> Type) where

libs/prelude/Prelude/Functor.idr+8

@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where

10 ||| @ m the morphism

11 map : (m : a -> b) -> f a -> f b

12

13+infixl 4 <$>

14+

15+||| An infix alias for `map`: the action of a functor on morphisms.

16+||| @ f the functor

17+||| @ m the morphism

18+(<$>) : Functor f => (m : a -> b) -> f a -> f b

19+m <$> x = map m x

20+

13class Functor f => VerifiedFunctor (f : Type -> Type) where

21class Functor f => VerifiedFunctor (f : Type -> Type) where

14 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x

22 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x

15 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

23 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

libs/prelude/Prelude/Monad.idr+1−1

@@ -16,7 +16,7 @@ class Applicative m => Monad (m : Type -> Type) where

16

17class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

18 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

19− mf <$> mx = mf >>= \f =>

19+ mf <*> mx = mf >>= \f =>

20 mx >>= \x =>

21 pure (f x)

22 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

libs/prelude/Prelude/Stream.idr+1−1

@@ -111,7 +111,7 @@ scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs

111

112instance Applicative Stream where

113 pure = repeat

114− (<$>) = zipWith apply

114+ (<*>) = zipWith apply

115

116instance Monad Stream where

117 s >>= f = diag (map f s)

libs/prelude/Prelude/Traversable.idr+2−2

@@ -8,10 +8,10 @@ import Prelude.Foldable

8import Prelude.Functor

9

10traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()

11−traverse_ f = foldr (($>) . f) (pure ())

11+traverse_ f = foldr ((*>) . f) (pure ())

12

13sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()

14−sequence_ = foldr ($>) (pure ())

14+sequence_ = foldr (*>) (pure ())

15

16for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()

17for_ = flip traverse_

rts/Makefile+1−1

@@ -18,7 +18,7 @@ endif

18endif

19

20ifeq ($(OS), windows)

21− OBJS += windows/idris_stdfgn.o windows/idris_net.o

21+ OBJS += windows/idris_stdfgn.o windows/idris_net.o windows/win_utils.o

22else

23 OBJS += idris_stdfgn.o idris_net.o

24endif

rts/windows/idris_stdfgn.c+10−3

@@ -5,9 +5,12 @@

5#include <fcntl.h>

6#include <stdio.h>

7#include <time.h>

8+#include <io.h>

8

9

9extern char** environ;

10extern char** environ;

10

11

12+int win_fpoll(void* h);

13+

11void putStr(char* str) {

14void putStr(char* str) {

12 printf("%s", str);

15 printf("%s", str);

13}

16}

@@ -32,14 +35,18 @@ int fileError(void* h) {

32 return ferror(f);

35 return ferror(f);

33}

36}

34

37

35−void fputStr(void* h, char* str) {

38+int idris_writeStr(void* h, char* str) {

36 FILE* f = (FILE*)h;

39 FILE* f = (FILE*)h;

37− fputs(str, f);

40+ if (fputs(str, f)) {

41+ return 0;

42+ } else {

43+ return -1;

44+ }

38}

45}

39

46

40int fpoll(void* h)

47int fpoll(void* h)

41{

48{

42− return 0;

49+ return win_fpoll(h);

43}

50}

44

51

45void* do_popen(const char* cmd, const char* mode) {

52void* do_popen(const char* cmd, const char* mode) {

rts/windows/win_utils.cnew file+21

@@ -0,0 +1,21 @@

1+#include <windows.h>

2+#include <io.h>

3+#include <stdio.h>

4+

5+// THis file exists to avoid clashes between windows.h and idris_rts.h

6+//

7+

8+int win_fpoll(void* h)

9+{

10+ HANDLE wh =(HANDLE) _get_osfhandle(_fileno((FILE*)h));

11+ if (wh == INVALID_HANDLE_VALUE) {

12+ return -1;

13+ }

14+ DWORD ret = WaitForSingleObject(wh, 1000);

15+ // Imitate the return values of select()

16+ if (ret == WAIT_OBJECT_0)

17+ return 1;

18+ if (ret == WAIT_TIMEOUT)

19+ return 0;

20+ return -1;

21+}

samples/interp.idr+2−2

@@ -37,8 +37,8 @@ using (G : Vect n Ty)

37 index_first = stop

38 index_next = pop

39

40− (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

40+ (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

41− (<$>) = \f, a => App f a

41+ (<*>) = \f, a => App f a

42

43 pure : Expr G a -> Expr G a

44 pure = id

src/Idris/AbsSyntax.hs+8−1

@@ -1714,6 +1714,10 @@ stripLinear i tm = evalState (sl tm) [] where

1714 return (a' : as')

1715 slAlts ns [] = return []

1716 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1717+ sl (PDPair fc p l t r) = do l' <- sl l

1718+ t' <- sl t

1719+ r' <- sl r

1720+ return (PDPair fc p l' t' r')

1717 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1721 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1718 args' <- mapM slA args

1722 args' <- mapM slA args

1719 return $ PApp fc fn args'

1723 return $ PApp fc fn args'

@@ -1978,8 +1982,11 @@ shadow :: Name -> Name -> PTerm -> PTerm

1978shadow n n' t = sm t where

1982shadow n n' t = sm t where

1979 sm (PRef fc x) | n == x = PRef fc n'

1983 sm (PRef fc x) | n == x = PRef fc n'

1980 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)

1984 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)

1985+ | otherwise = PLam fc x (sm t) sc

1981− sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)

1986+ sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)

1987+ | otherwise = PPi p x (sm t) sc

1982 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)

1988 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)

1989+ | otherwise = PLet fc x (sm t) (sm v) sc

1983 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1990 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1984 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1991 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1985 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1992 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1157,7 +1157,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

1157

1158initDSL = DSL (PRef f (sUN ">>="))

1159 (PRef f (sUN "return"))

1160− (PRef f (sUN "<$>"))

1160+ (PRef f (sUN "<*>"))

1161 (PRef f (sUN "pure"))

1162 Nothing

1163 Nothing

src/Idris/CmdOptions.hs+1−1

@@ -26,7 +26,7 @@ runArgParser = do opts <- execParser $ info parser

26 idrisProgDesc = PP.vsep [PP.empty,

27 PP.text "Idris is a general purpose pure functional programming language with dependent",

28 PP.text "types. Dependent types allow types to be predicated on values, meaning that",

29− PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",

29+ PP.text "some aspects of a program's behaviour can be specified precisely in the type.",

30 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",

31 PP.text "and ML.",

32 PP.empty,

src/Idris/DSL.hs+28−6

@@ -17,21 +17,43 @@ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

17desugar syn i t = let t' = expandDo (dsl_info syn) t in

18 t' -- addImpl i t'

19

20+mkTTName :: FC -> Name -> PTerm

21+mkTTName fc n =

22+ let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])

23+ mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))

24+ [ pexp (stringC x)

25+ , pexp (mkList fc xs)]

26+ stringC = PConstant . Str . str

27+ intC = PConstant . I

28+ reflm n = sNS (sUN n) ["Reflection", "Language"]

29+ in case n of

30+ UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]

31+ NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)

32+ , pexp (mkList fc ns)]

33+ MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)

34+ , pexp (stringC nm)]

35+ otherwise -> PRef fc $ reflm "NErased"

36+

20expandDo :: DSL -> PTerm -> PTerm

37expandDo :: DSL -> PTerm -> PTerm

21expandDo dsl (PLam fc n ty tm)

38expandDo dsl (PLam fc n ty tm)

22 | Just lam <- dsl_lambda dsl

39 | Just lam <- dsl_lambda dsl

40+ = let sc = PApp fc lam [ pexp (mkTTName fc n)

23− = let sc = PApp fc lam [pexp (var dsl n tm 0)] in

41+ , pexp (var dsl n tm 0)]

24− expandDo dsl sc

42+ in expandDo dsl sc

25expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

43expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

26expandDo dsl (PLet fc n ty v tm)

44expandDo dsl (PLet fc n ty v tm)

27 | Just letb <- dsl_let dsl

45 | Just letb <- dsl_let dsl

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

46+ = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

47+ , pexp v

48+ , pexp (var dsl n tm 0)]

29− expandDo dsl sc

49+ in expandDo dsl sc

30expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

50expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

31expandDo dsl (PPi p n ty tm)

51expandDo dsl (PPi p n ty tm)

32 | Just pi <- dsl_pi dsl

52 | Just pi <- dsl_pi dsl

53+ = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

54+ , pexp ty

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

55+ , pexp (var dsl n tm 0)]

34− expandDo dsl sc

56+ in expandDo dsl sc

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

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

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

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

37 (map (fmap (expandDo dsl)) args)

59 (map (fmap (expandDo dsl)) args)

src/Idris/Elab/Clause.hs+3−3

@@ -648,9 +648,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

648 -- Now build the RHS, using the type of the LHS as the goal.

649 i <- getIState -- new implicits from where block

650 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

651− let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

651+ let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)

652 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

653− logLvl 2 $ "RHS: " ++ showTmImpls rhs

653+ logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

654 ctxt <- getContext -- new context with where block added

655 logLvl 5 "STARTING CHECK"

656 ((rhs', defer, is, probs), _) <-

@@ -673,7 +673,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

673 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

674

675 logLvl 5 "DONE CHECK"

676− logLvl 2 $ "---> " ++ show rhs'

676+ logLvl 4 $ "---> " ++ show rhs'

677 when (not (null defer)) $ iLOG $ "DEFERRED " ++

678 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

679 def' <- checkDef fc defer

src/Idris/Elab/Data.hs+4−2

@@ -316,11 +316,13 @@ elabCaseFun ind paramPos n ty cons info = do

316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

318 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

319− State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl) (\err -> return ())

319+ State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)

320+ (ierror . Elaborating "type declaration of " elimDeclName)

320 -- Do not elaborate clauses if there aren't any

321 -- Do not elaborate clauses if there aren't any

321 case eliminatorClauses of

322 case eliminatorClauses of

322 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type

323 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type

323− _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef) (\err -> return ())

324+ _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

325+ (ierror . Elaborating "clauses of " elimDeclName)

324 where elimLog :: String -> EliminatorState ()

326 where elimLog :: String -> EliminatorState ()

325 elimLog s = State.lift (logLvl 2 s)

327 elimLog s = State.lift (logLvl 2 s)

326

328

src/Idris/ElabTerm.hs+9−1

@@ -893,9 +893,17 @@ elab ist info emode opts fn tm

893 -- Drop the unique arguments used in the term already

894 -- and in the scrutinee (since it's

895 -- not valid to use them again anyway)

896+ --

897+ -- Also drop unique arguments which don't appear explicitly

898+ -- in either case branch so they don't count as used

899+ -- unnecessarily (can only do this for unique things, since we

900+ -- assume they don't appear implicitly in types)

896 ptm <- get_term

901 ptm <- get_term

902+ let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

903+

897 let argsDropped = filter (isUnique envU)

904 let argsDropped = filter (isUnique envU)

898− (nub $ allNamesIn scr ++ inApp ptm)

905+ (nub $ allNamesIn scr ++ inApp ptm ++

906+ inOpts)

899

907

900 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args

901

909

src/Idris/ParseHelpers.hs+8−10

@@ -105,30 +105,28 @@ isEol :: Char -> Bool

105isEol '\n' = True

106isEol _ = False

107

108+-- | A parser that succeeds at the end of the line

108eol :: MonadicParsing m => m ()

109eol :: MonadicParsing m => m ()

109eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

110eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

110

111

111{- | Consumes a single-line comment

112{- | Consumes a single-line comment

112

113

113@

114@

114− SingleLineComment_t ::= '--' EOL_t

115+ SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;

115− | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

116− ;

117@

116@

118 -}

117 -}

119singleLineComment :: MonadicParsing m => m ()

118singleLineComment :: MonadicParsing m => m ()

120−singleLineComment = try (string "--" *> eol *> pure ())

119+singleLineComment = (string "--" *>

121− <|> try (string "--" *> many simpleWhiteSpace *>

122− many (satisfy (not . isEol)) *>

120+ many (satisfy (not . isEol)) *>

123− eol *> pure ())

121+ eol *> pure ())

124− <?> ""

122+ <?> "single-line comment"

125

123

126{- | Consumes a multi-line comment

124{- | Consumes a multi-line comment

127

125

128@

126@

129 MultiLineComment_t ::=

127 MultiLineComment_t ::=

130 '{ -- }'

128 '{ -- }'

131− | '{ -' ~DocCommentMarker_t InCommentChars_t

129+ | '{ -' InCommentChars_t

132 ;

130 ;

133@

131@

134

132

@@ -154,7 +152,7 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

154 startEnd :: String

152 startEnd :: String

155 startEnd = "{}-"

153 startEnd = "{}-"

156

154

157−{-| Parses a documentation comment (similar to haddock) given a marker character

155+{-| Parses a documentation comment

158

156

159@

157@

160 DocComment_t ::= '|||' ~EOL_t* EOL_t

158 DocComment_t ::= '|||' ~EOL_t* EOL_t

src/Idris/Parser.hs+16

@@ -1311,8 +1311,24 @@ loadSource lidr f toline

1311 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]

1312 let syntax = defaultSyntax{ syn_namespace = reverse mname,

1313 maxline = toline }

1314+ ist <- getIState

1315+ -- Save the span from parsing the module header, because

1316+ -- an empty program parse might obliterate it.

1317+ let oldSpan = idris_parsedSpan ist

1314 ds' <- parseProg syntax f file pos

1318 ds' <- parseProg syntax f file pos

1315

1319

1320+ case (ds', oldSpan) of

1321+ ([], Just fc) ->

1322+ -- If no program elements were parsed, we dind't

1323+ -- get a loaded region in the IBC file. That

1324+ -- means we need to add it back.

1325+ do ist <- getIState

1326+ putIState ist { idris_parsedSpan = oldSpan

1327+ , ibc_write = IBCParsedRegion fc :

1328+ ibc_write ist

1329+ }

1330+ _ -> return ()

1331+

1316 -- Parsing done, now process declarations

1332 -- Parsing done, now process declarations

1317

1333

1318 let ds = namespaces mname ds'

1334 let ds = namespaces mname ds'

src/Idris/REPL.hs+4−2

@@ -821,7 +821,7 @@ process fn (Undefine names) = undefine names

821 -- Keep track of which names you've removed so you can

822 -- print them out to the user afterward

823 undefine names = undefine' names []

824− undefine' [] list = do iRenderOutput $ printUndefinedNames list

824+ undefine' [] list = do iRenderResult $ printUndefinedNames list

825 return ()

826 undefine' (n:names) already = do

827 allDefined <- idris_repl_defs `fmap` get

@@ -1104,10 +1104,12 @@ process fn Execute

1104 (tmpn, tmph) <- runIO tempfile

1105 runIO $ hClose tmph

1106 t <- codegen

1107+ -- gcc adds .exe when it builds windows programs

1108+ progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1107 ir <- compile t tmpn m

1109 ir <- compile t tmpn m

1108 runIO $ generate t (fst (head (idris_imported ist))) ir

1110 runIO $ generate t (fst (head (idris_imported ist))) ir

1109 case idris_outputmode ist of

1111 case idris_outputmode ist of

1110− RawOutput h -> do runIO $ rawSystem tmpn []

1112+ RawOutput h -> do runIO $ rawSystem progName []

1111 return ()

1113 return ()

1112 IdeMode n h -> runIO . hPutStrLn h $

1114 IdeMode n h -> runIO . hPutStrLn h $

1113 IdeMode.convSExp "run-program" tmpn n)

1115 IdeMode.convSExp "run-program" tmpn n)

src/Pkg/PParser.hs+2−2

@@ -16,7 +16,7 @@ import Idris.CmdOptions

16import Control.Monad.State.Strict

17import Control.Applicative

18

19−import System.Info (os)

19+import Util.System

20

21

22type PParser = StateT PkgDesc IdrisInnerParser

@@ -63,7 +63,7 @@ pClause :: PParser ()

63pClause = do reserved "executable"; lchar '=';

64 exec <- iName []

65 st <- get

66− put (st { execout = Just (if os `elem` ["win32", "mingw32", "cygwin32"]

66+ put (st { execout = Just (if isWindows

67 then ((show exec) ++ ".exe")

68 else ( show exec )

69 ) })

src/Util/System.hs+5−1

@@ -1,4 +1,4 @@

1−module Util.System(tempfile,withTempdir,rmFile,catchIO) where

1+module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows) where

2

3-- System helper functions.

4import Control.Monad (when)

@@ -9,6 +9,7 @@ import System.Directory (getTemporaryDirectory

9 )

10import System.FilePath ((</>), normalise)

11import System.IO

12+import System.Info

12import System.IO.Error

13import System.IO.Error

13import Control.Exception as CE

14import Control.Exception as CE

14

15

@@ -18,6 +19,9 @@ catchIO = CE.catch

18throwIO :: IOError -> IO a

19throwIO :: IOError -> IO a

19throwIO = CE.throw

20throwIO = CE.throw

20

21

22+isWindows :: Bool

23+isWindows = os `elem` ["win32", "mingw32", "cygwin32"]

24+

21tempfile :: IO (FilePath, Handle)

25tempfile :: IO (FilePath, Handle)

22tempfile = do dir <- getTemporaryDirectory

26tempfile = do dir <- getTemporaryDirectory

23 openTempFile (normalise dir) "idris"

27 openTempFile (normalise dir) "idris"

test/dsl001/test001.idr+4−1

@@ -35,8 +35,11 @@ using (G : Vect n Ty)

35 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

36 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

37

38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)

39+ lam_ _ = Lam

40+

38 dsl expr

41 dsl expr

39− lambda = Lam

42+ lambda = lam_

40 variable = Var

43 variable = Var

41 index_first = stop

44 index_first = stop

42 index_next = pop

45 index_next = pop

test/dsl002/Resimp.idr+6−1

@@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

156 = interp env v (\env', v' => do n <- v'

157 interp env' (f n) k)

158

159+ let_ : _ -> Creator (interpTy a) ->

160+ Res (a :: gam) (Val () :: gam') (R t) ->

161+ Res gam gam' (R t)

162+ let_ _ = Let

163+

159-- run : {static} Res [] [] (R t) -> IO t

164-- run : {static} Res [] [] (R t) -> IO t

160-- run prog = interp [] prog (\env, res => res)

165-- run prog = interp [] prog (\env, res => res)

161

166

@@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)

163

168

164dsl res

169dsl res

165 variable = id

170 variable = id

166− let = Let

171+ let = let_

167 index_first = stop

172 index_first = stop

168 index_next = pop

173 index_next = pop

169

174

test/dsl003/DSLPi.idr+8−2

@@ -5,8 +5,11 @@ import Data.Vect

5

6data Ty = BOOL | INT | UNIT | ARR Ty Ty

7

8+arr_ : _ -> Ty -> Ty -> Ty

9+arr_ _ = ARR

10+

8dsl simple_type

11dsl simple_type

9− pi = ARR

12+ pi = arr_

10

13

11test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

14test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

12test1 = Refl

15test1 = Refl

@@ -25,8 +28,11 @@ using (vars : Vect n Ty)

25 implicit exprSpec : Expr vars BOOL -> Spec vars

28 implicit exprSpec : Expr vars BOOL -> Spec vars

26 exprSpec = ItHolds

29 exprSpec = ItHolds

27

30

31+ forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars

32+ forall_ _ = ForAll

33+

28dsl specs

34dsl specs

29− pi = ForAll

35+ pi = forall_

30 variable = Var

36 variable = Var

31 index_first = FZ

37 index_first = FZ

32 index_next = FS

38 index_next = FS

test/reg027/reg027.idr+1−1

@@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where

14

15instance Applicative (\x => Int -> x) where

16 pure v = \x => v

17− (<$>) f a = \x => f x (a x)

17+ (<*>) f a = \x => f x (a x)

18

19instance Monad IntFn where

20 f >>= k = \x => k (f x) x

test/reg050/expected+8−7

@@ -12,17 +12,18 @@ When elaborating an application of function Prelude.Monad.>>=:

12 \{uv0} => argTy -> uv

13./baddoublebang.idr:6:26: error: not

14 a terminator, expected: "$",

15− "$>", "&&", "*", "+", "++", "-",

15+ "&&", "*", "*>", "+", "++", "-",

16 "->", ".", "/", "/=", "::", ";",

17− "<", "<#>", "<$", "<$>", "<*>",

17+ "<", "<#>", "<$>", "<*", "<*>",

18− "<+>", "<->", "<<", "<=", "<|>",

18+ "<+>", "<->", "<.>", "<<", "<=",

19− "=", "==", ">", ">=", ">>",

19+ "<|>", "=", "==", ">", ">=",

20− ">>=", "\\\\", "`", "in", "||",

20+ ">>", ">>=", "\\\\", "`", "in",

21− "~=~",

21+ "||", "~=~",

22 ambiguous use of a left-associative operator,

23 ambiguous use of a non-associative operator,

24 ambiguous use of a right-associative operator,

25 end of input, function argument,

26− matching application expression

26+ matching application expression,

27+ single-line comment

27doubleBang mmn = do pure !!mmn

28doubleBang mmn = do pure !!mmn

28 ^

29 ^

test/reg053/four.idr+1−1

@@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y

5traverseFourFunctor : Applicative f ->

6 (x -> f b) -> FourFunctor x -> f (FourFunctor b)

7traverseFourFunctor constr f (Four w x y z)

8− = pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)

8+ = pure Four <*> (f w) <*> (f x) <*> (f y) <*> (f z)

9

test/sourceLocation001/SourceLoc.idr+3−1

@@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)

54 run (App f x) env = !(run f env) !(run x env)

55 run (Die {loc}) _ = Left loc

56

57+ lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

58+ lam_ _ = Lam

57

59

58exec : Tm [] t -> IO ()

60exec : Tm [] t -> IO ()

59exec tm = case run tm [] of

61exec tm = case run tm [] of

@@ -64,7 +66,7 @@ dsl lang

64 variable = Var

66 variable = Var

65 index_first = FZ

67 index_first = FZ

66 index_next = FS

68 index_next = FS

67− lambda = Lam

69+ lambda = lam_

68

70

69testTerm1 : Tm [] (Arr U U)

71testTerm1 : Tm [] (Arr U U)

70testTerm1 = lang (\x=>Die)

72testTerm1 = lang (\x=>Die)

test/sourceLocation001/expected+2−2

@@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)

3Testing using inline tactics

4FileLoc "SourceLoc.idr" (20, 17) (20, 17)

5Testing using metavariable with later definition

6−FileLoc "SourceLoc.idr" (96, 16) (96, 16)

6+FileLoc "SourceLoc.idr" (98, 16) (98, 16)

7-----------------------

8Success!

9−Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)

9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)

10Success!

11Success!

test/sugar001/test007.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

21

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where

23 appAux : Maybe (a -> b) -> Maybe a -> Maybe b

24 appAux (Just fx) (Just gx) = Just (fx gx)

25 appAux _ _ = Nothing

test/tutorial003/tutorial003.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

21

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

23 app : Maybe (a -> b) -> Maybe a -> Maybe b

24 app (Just fx) (Just gx) = Just (fx gx)

25 app _ _ = Nothing