1d2fc7f · Idris-dev · git.iko.soy

idris.cabal+133−127

compare with master

unifiedsplit

@@ -206,133 +206,139 @@ Extra-source-files:

206 test/reg032/run

207 test/reg032/*.idr

208 test/reg032/expected

209+

209− test/test001/run

210+ test/basic001/run

210− test/test001/*.idr

211+ test/basic001/*.idr

211− test/test001/expected

212+ test/basic001/expected

212− test/test002/run

213+ test/basic002/run

213− test/test002/*.idr

214+ test/basic002/*.idr

214− test/test002/expected

215+ test/basic002/expected

215− test/test003/run

216+ test/basic003/run

216− test/test003/*.lidr

217+ test/basic003/*.idr

217− test/test003/expected

218− test/test004/run

219− test/test004/*.idr

220− test/test004/expected

218+ test/basic003/expected

221− test/test005/run

219+ test/basic004/run

222− test/test005/*.idr

220+ test/basic004/*.idr

223− test/test005/expected

221+ test/basic004/expected

224− test/test006/run

222+ test/basic005/run

225− test/test006/*.idr

223+ test/basic005/*.lidr

226− test/test006/expected

224+ test/basic005/expected

227− test/test007/run

225+ test/basic006/run

228− test/test007/*.idr

226+ test/basic006/*.idr

229− test/test007/expected

227+ test/basic006/expected

230− test/test008/run

228+ test/basic007/run

231− test/test008/*.idr

229+ test/basic007/*.idr

232− test/test008/expected

230+ test/basic007/expected

233− test/test009/run

231+ test/basic008/run

234− test/test009/*.idr

232+ test/basic008/*.idr

235− test/test009/expected

233+ test/basic008/expected

236− test/test010/run

234+ test/basic009/run

237− test/test010/*.idr

235+ test/basic009/*.idr

238− test/test010/expected

236+ test/basic009/expected

239− test/test011/run

237+ test/basic009/B/*.idr

240− test/test011/*.idr

238+

241− test/test011/expected

242− test/test012/run

239+ test/dsl001/run

243− test/test012/*.idr

240+ test/dsl001/*.idr

244− test/test012/expected

241+ test/dsl001/expected

245− test/test013/run

242+ test/dsl002/run

246− test/test013/*.idr

243+ test/dsl002/*.idr

247− test/test013/expected

244+ test/dsl002/expected

245+

248− test/test014/run

246+ test/effects001/run

249− test/test014/*.idr

247+ test/effects001/*.idr

250− test/test014/test

248+ test/effects001/expected

251− test/test014/expected

252− test/test015/run

249+ test/effects002/run

253− test/test015/*.idr

250+ test/effects002/*.idr

254− test/test015/expected

251+ test/effects002/expected

255− test/test016/run

252+

256− test/test016/*.idr

253+ test/error001/run

257− test/test016/expected

258− test/test017/run

259− test/test017/*.idr

254+ test/error001/*.idr

260− test/test017/expected

255+ test/error001/expected

261− test/test018/run

256+ test/error002/run

262− test/test018/*.idr

257+ test/error002/*.idr

263− test/test018/expected

258+ test/error002/expected

264− test/test019/run

259+ test/error003/run

265− test/test019/*.lidr

260+ test/error003/*.idr

266− test/test019/expected

267− test/test020/run

268− test/test020/*.idr

269− test/test020/expected

261+ test/error003/expected

270− test/test021/run

262+ test/error004/run

271− test/test021/*.idr

263+ test/error004/*.idr

272− test/test021/testFile

273− test/test021/expected

264+ test/error004/expected

274− test/test022/run

265+

275− test/test022/*.idr

266+ test/ffi001/run

276− test/test022/expected

277− test/test023/run

278− test/test023/*.idr

267+ test/ffi001/*.idr

279− test/test023/expected

268+ test/ffi001/expected

280− test/test024/run

269+ test/ffi002/run

281− test/test024/*.idr

270+ test/ffi002/*.idr

282− test/test024/input

283− test/test024/expected

271+ test/ffi002/expected

284− test/test025/run

272+ test/ffi003/run

285− test/test025/*.idr

273+ test/ffi003/*.idr

286− test/test025/expected

274+ test/ffi003/expected

287− test/test026/run

275+ test/ffi004/run

288− test/test026/*.idr

276+ test/ffi004/*.idr

289− test/test026/input

277+ test/ffi004/input

290− test/test026/theType

278+ test/ffi004/theType

291− test/test026/theOtherType

279+ test/ffi004/theOtherType

292− test/test026/expected

280+ test/ffi004/expected

281+

293− test/test027/run

282+ test/interactive001/run

294− test/test027/*.idr

283+ test/interactive001/*.idr

295− test/test027/expected

284+ test/interactive001/expected

285+

296− test/test028/run

286+ test/io001/run

297− test/test028/*.idr

287+ test/io001/*.idr

298− test/test028/expected

288+ test/io001/expected

299− test/test029/run

289+ test/io002/run

300− test/test029/*.idr

290+ test/io002/*.idr

301− test/test029/expected

291+ test/io002/expected

302− test/test030/run

292+ test/io003/run

303− test/test030/*.idr

293+ test/io003/*.idr

304− test/test030/expected

294+ test/io003/expected

295+

305− test/test031/run

296+ test/literate001/run

306− test/test031/*.idr

297+ test/literate001/*.lidr

307− test/test031/expected

298+ test/literate001/expected

299+

308− test/test032/run

300+ test/primitives001/run

309− test/test032/*.idr

301+ test/primitives001/*.idr

310− test/test032/input

302+ test/primitives001/expected

311− test/test032/expected

303+ test/primitives002/run

304+ test/primitives002/expected

312− test/test033/run

305+ test/primitives003/run

313− test/test033/*.idr

306+ test/primitives003/*.idr

314− test/test033/expected

307+ test/primitives003/expected

308+

315− test/test034/run

309+ test/proof001/run

310+ test/proof001/*.idr

316− test/test034/expected

311+ test/proof001/expected

317− test/test035/run

312+ test/proof002/run

313+ test/proof002/*.idr

318− test/test035/expected

314+ test/proof002/expected

319− test/test035/*.idr

315+ test/proof003/run

320− test/test036/run

316+ test/proof003/*.idr

321− test/test036/expected

317+ test/proof003/expected

318+ test/proof004/run

322− test/test036/*.idr

319+ test/proof004/*.idr

323− test/test037/run

320+ test/proof004/expected

324− test/test037/expected

321+

325− test/test037/*.idr

322+ test/records001/run

326− test/test038/run

323+ test/records001/*.idr

327− test/test038/expected

324+ test/records001/expected

325+

326+ test/sugar001/run

327+ test/sugar001/*.idr

328+ test/sugar001/expected

329+ test/sugar002/run

328− test/test038/*.idr

330+ test/sugar002/*.idr

329− test/test039/run

331+ test/sugar002/expected

330− test/test039/expected

332+ test/sugar003/run

331− test/test039/*.idr

333+ test/sugar003/*.idr

332− test/test040/run

334+ test/sugar003/expected

333− test/test040/expected

335+

336+ test/totality001/run

334− test/test040/*.idr

337+ test/totality001/*.idr

335− test/test040/B/*.idr

338+ test/totality001/expected

339+ test/totality002/run

340+ test/totality002/*.idr

341+ test/totality002/expected

336

342

337source-repository head

343source-repository head

338 type: git

344 type: git

test/Makefile+2−2

@@ -11,10 +11,10 @@ test_java:

11 perl ./runtest.pl all --codegen Java

12

13test_js:

14− @perl ./runtest.pl without reg029 reg031 test004 test014 test018 test021 test025 test033 --codegen node

14+ @perl ./runtest.pl without reg029 reg031 io001 dsl002 io003 effects001 effects002 basic007 --codegen node

15

16test_llvm:

17− @perl ./runtest.pl without test018 test033 --codegen llvm

17+ @perl ./runtest.pl without io003 basic007 --codegen llvm

18

19update:

20 /usr/bin/env perl ./runtest.pl all -u

test/README+14−39

@@ -1,41 +1,16 @@

1−Tests:

1+Tests are categorised as follows:

2

3−001: Well-typed interpreter

3+basic: Basic language features, some complete programs

4−002: Universe checking

4+dsl: Embedded DSLs and features to support DSL development

5−003: Literate source and string processing

5+effects: Effects package

6−004: File operations

6+error: Error messages and error reflection

7−005: Num class resolution [regression]; span & break; ad-hoc overloading

7+ffi: FFI calls, including type providers

8−006: Provisional definitions; class resolution in patterns

8+interactive: Interactive editing, proof search

9−007: Applicative and idiom brackets

9+io: IO monad

10−008: case and pattern matching let

10+literate: .lidr files; literate programming

11−009: ranges and list monad

11+primitives: Primitive types

12−010: total

12+proof: Theorem proving, tactics

13−011: record projection and update

13+sugar: Syntactic sugar, syntax extensions

14−012: various error regressions

14+totality: Totality checking

15−013: binding syntax

16−014: resource DSL

17−015: verified binary adder

18−016: codata

19−017: mutually recursive totality checking

20−018: Message passing concurrency (raw form)

21−019: magic with

22−020: implicit conversions

23−021: effects

24−022: dynamic C library loading and interpreter IO

25−023: trivial (non-I/O) type providers

26−024: interpreter I/O

27−025: memory effects

28−026: simple file-I/O-based type provider

29−027: class constraints in using block

30−028: hello world with comment and block comment syntax in idr file

31−029: match_refine and apply by type

32−030: %reflection for functions running on syntax

33−031: error reflection

34−032: control idris via stdin

35−033: null pointer creation and check

36−034: presence of floating point primitives in backends

37−

38−regxxx: various regression tests

39−reg020: working strlen

40−reg029: executor doesn’t crash receiving a NULL String from C

41

15

16+reg: Regression tests, covering previous bug fixes

test/basic001/expectednew file+1

@@ -0,0 +1 @@

1+1f4o1b4a1r1b3a1z

test/reg005/reg005.idr → test/basic001/reg005.idrrenamed

The content is the same.

test/basic001/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ reg005.idr -o reg005

3+./reg005

4+rm -f reg005 *.ibc

test/test006/expected → test/basic002/expectedrenamed

The content is the same.

test/test006/run → test/basic002/runrenamed

The content is the same.

test/test006/test006.idr → test/basic002/test006.idrrenamed

The content is the same.

test/test027/expected → test/basic003/expectedrenamed

The content is the same.

test/test027/run → test/basic003/runrenamed

The content is the same.

test/test027/test027.idr → test/basic003/test027.idrrenamed

The content is the same.

test/test016/expected → test/basic004/expectedrenamed

The content is the same.

test/test016/run → test/basic004/runrenamed

The content is the same.

test/test016/test016.idr → test/basic004/test016.idrrenamed

The content is the same.

test/test019/expected → test/basic005/expectedrenamed

The content is the same.

test/test019/run → test/basic005/runrenamed

The content is the same.

test/test019/test019.lidr → test/basic005/test019.lidrrenamed

The content is the same.

test/test020/expected → test/basic006/expectedrenamed

The content is the same.

test/test020/run → test/basic006/runrenamed

The content is the same.

test/test020/test020.idr → test/basic006/test020.idrrenamed

The content is the same.

test/test020/test020a.idr → test/basic006/test020a.idrrenamed

The content is the same.

test/test033/expected → test/basic007/expectedrenamed

The content is the same.

test/test033/run → test/basic007/runrenamed

The content is the same.

test/test033/test033.idr → test/basic007/test033.idrrenamed

The content is the same.

test/test036/expected → test/basic008/expectedrenamed

The content is the same.

test/test036/run → test/basic008/runrenamed

The content is the same.

test/test036/test036.idr → test/basic008/test036.idrrenamed

The content is the same.

test/test040/A.idr → test/basic009/A.idrrenamed

The content is the same.

test/test040/B/C.idr → test/basic009/B/C.idrrenamed

The content is the same.

test/test040/Faulty.idr → test/basic009/Faulty.idrrenamed

The content is the same.

test/test040/Main.idr → test/basic009/Main.idrrenamed

The content is the same.

test/test040/Multiple.idr → test/basic009/Multiple.idrrenamed

The content is the same.

test/test040/expected → test/basic009/expectedrenamed

The content is the same.

test/test040/run → test/basic009/runrenamed

The content is the same.

test/test001/expected → test/dsl001/expectedrenamed

The content is the same.

test/test001/run → test/dsl001/runrenamed

The content is the same.

test/test001/test001.idr → test/dsl001/test001.idrrenamed

The content is the same.

test/test014/Resimp.idr → test/dsl002/Resimp.idrrenamed

The content is the same.

test/test014/expected → test/dsl002/expectedrenamed

The content is the same.

test/test014/run → test/dsl002/runrenamed

The content is the same.

test/test014/test → test/dsl002/testrenamed

The content is the same.

test/test014/test014.idr → test/dsl002/test014.idrrenamed

The content is the same.

test/test021/expected → test/effects001/expectedrenamed

The content is the same.

test/test021/run → test/effects001/runrenamed

The content is the same.

test/test021/test021.idr → test/effects001/test021.idrrenamed

The content is the same.

test/test021/test021a.idr → test/effects001/test021a.idrrenamed

The content is the same.

test/test021/testFile → test/effects001/testFilerenamed

The content is the same.

test/test025/expected → test/effects002/expectedrenamed

The content is the same.

test/test025/run → test/effects002/runrenamed

The content is the same.

test/test025/test025.idr → test/effects002/test025.idrrenamed

The content is the same.

test/test002/expected → test/error001/expectedrenamed

The content is the same.

test/test002/expected_ttquot → test/error001/expected_ttquotrenamed

The content is the same.

test/test002/run → test/error001/runrenamed

The content is the same.

test/test002/test002.idr → test/error001/test002.idrrenamed

The content is the same.

test/test029/expected → test/error002/expectedrenamed

The content is the same.

test/test031/run → test/error002/runrenamed

The content is the same.

test/test031/test031.idr → test/error002/test031.idrrenamed

The content is the same.

test/test037/ErrorReflection.idr → test/error003/ErrorReflection.idrrenamed

The content is the same.

test/test037/expected → test/error003/expectedrenamed

The content is the same.

test/test037/run → test/error003/runrenamed

The content is the same.

test/test038/FunErrTest.idr → test/error004/FunErrTest.idrrenamed

The content is the same.

test/test038/expected → test/error004/expectedrenamed

The content is the same.

test/test038/run → test/error004/runrenamed

The content is the same.

test/test022/expected → test/ffi001/expectedrenamed

The content is the same.

test/test022/run → test/ffi001/runrenamed

The content is the same.

test/test022/test022.idr → test/ffi001/test022.idrrenamed

The content is the same.

test/test023/expected → test/ffi002/expectedrenamed

The content is the same.

test/test023/run → test/ffi002/runrenamed

The content is the same.

test/test023/test023.idr → test/ffi002/test023.idrrenamed

The content is the same.

test/test024/expected → test/ffi003/expectedrenamed

The content is the same.

test/test024/input → test/ffi003/inputrenamed

The content is the same.

test/test024/run → test/ffi003/runrenamed

The content is the same.

test/test024/test024.idr → test/ffi003/test024.idrrenamed

The content is the same.

test/test026/expected → test/ffi004/expectedrenamed

The content is the same.

test/test026/input → test/ffi004/inputrenamed

The content is the same.

test/test026/run → test/ffi004/runrenamed

The content is the same.

test/test026/test026.idr → test/ffi004/test026.idrrenamed

The content is the same.

test/test026/theOtherType → test/ffi004/theOtherTyperenamed

The content is the same.

test/test026/theType → test/ffi004/theTyperenamed

The content is the same.

test/test032/expected → test/interactive001/expectedrenamed

The content is the same.

test/test032/input → test/interactive001/inputrenamed

The content is the same.

test/test032/run → test/interactive001/runrenamed

The content is the same.

test/test032/test032.idr → test/interactive001/test032.idrrenamed

The content is the same.

test/test004/expected → test/io001/expectedrenamed

The content is the same.

test/test004/run → test/io001/runrenamed

The content is the same.

test/test004/test004.idr → test/io001/test004.idrrenamed

The content is the same.

test/test008/expected → test/io002/expectedrenamed

The content is the same.

test/test008/run → test/io002/runrenamed

The content is the same.

test/test008/test008.idr → test/io002/test008.idrrenamed

The content is the same.

test/test018/expected → test/io003/expectedrenamed

The content is the same.

test/test018/run → test/io003/runrenamed

The content is the same.

test/test018/test018.idr → test/io003/test018.idrrenamed

The content is the same.

test/test018/test018a.idr → test/io003/test018a.idrrenamed

The content is the same.

test/test003/Lit.lidr → test/literate001/Lit.lidrrenamed

The content is the same.

test/test003/expected → test/literate001/expectedrenamed

The content is the same.

test/test003/run → test/literate001/runrenamed

The content is the same.

test/test003/test003.lidr → test/literate001/test003.lidrrenamed

The content is the same.

test/test003/test003a.lidr → test/literate001/test003a.lidrrenamed

The content is the same.

test/test005/expected → test/primitives001/expectedrenamed

The content is the same.

test/test005/run → test/primitives001/runrenamed

The content is the same.

test/test005/test005.idr → test/primitives001/test005.idrrenamed

The content is the same.

test/test034/expected → test/primitives002/expectedrenamed

The content is the same.

test/test034/run → test/primitives002/runrenamed

The content is the same.

test/test039/expected → test/primitives003/expectedrenamed

The content is the same.

test/test039/run → test/primitives003/runrenamed

The content is the same.

test/test039/test038.idr → test/primitives003/test038.idrrenamed

The content is the same.

test/test031/expected → test/proof001/expectedrenamed

The content is the same.

test/test029/run → test/proof001/runrenamed

The content is the same.

test/test029/test029.idr → test/proof001/test029.idrrenamed

The content is the same.

test/test030/Reflect.idr → test/proof002/Reflect.idrrenamed

The content is the same.

test/test030/expected → test/proof002/expectedrenamed

The content is the same.

test/test030/run → test/proof002/runrenamed

The content is the same.

test/test030/test030.idr → test/proof002/test030.idrrenamed

The content is the same.

test/test030/test030a.idr → test/proof002/test030a.idrrenamed

The content is the same.

test/test015/Parity.idr → test/proof003/Parity.idrrenamed

The content is the same.

test/test015/expected → test/proof003/expectedrenamed

The content is the same.

test/test015/run → test/proof003/runrenamed

The content is the same.

test/test015/test015.idr → test/proof003/test015.idrrenamed

The content is the same.

test/test035/expected → test/proof004/expectedrenamed

The content is the same.

test/test035/run → test/proof004/runrenamed

The content is the same.

test/test035/test035.idr → test/proof004/test035.idrrenamed

The content is the same.

test/test011/expected → test/records001/expectedrenamed

The content is the same.

test/test011/run → test/records001/runrenamed

The content is the same.

test/test011/test011.idr → test/records001/test011.idrrenamed

The content is the same.

test/reg005/expected−1

@@ -1 +0,0 @@

1−1f4o1b4a1r1b3a1z

test/reg032/reg032.idr → test/reg005/reg032.idrrenamed

The content is the same.

test/reg005/run+2−3

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

1#!/usr/bin/env bash

2−idris $@ reg005.idr -o reg005

2+idris $@ reg032.idr --check

3−./reg005

4−rm -f reg005 *.ibc

3+rm -f *.ibc

test/reg032/expected+1

@@ -0,0 +1 @@

1+hello, world!

test/reg032/run+3−2

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

1#!/usr/bin/env bash

2−idris $@ reg032.idr --check

2+idris $@ test028.idr -o test028

3+./test028

3−rm -f *.ibc

4+rm -f test028 test028.ibc

test/test028/test028.idr → test/reg032/test028.idrrenamed

The content is the same.

test/test007/expected → test/sugar001/expectedrenamed

The content is the same.

test/test007/run → test/sugar001/runrenamed

The content is the same.

test/test007/test007.idr → test/sugar001/test007.idrrenamed

The content is the same.

test/test009/expected → test/sugar002/expectedrenamed

The content is the same.

test/test009/run → test/sugar002/runrenamed

The content is the same.

test/test009/test009.idr → test/sugar002/test009.idrrenamed

The content is the same.

test/test013/expected → test/sugar003/expectedrenamed

The content is the same.

test/test013/run → test/sugar003/runrenamed

The content is the same.

test/test013/test013.idr → test/sugar003/test013.idrrenamed

The content is the same.

test/test012/expecteddeleted−1

@@ -1 +0,0 @@

1−test012a.idr:7:1:x is not an accessible pattern variable

test/test012/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−idris $@ test012a.idr -o test012a

test/test012/test012a.idrdeleted−10

@@ -1,10 +0,0 @@

1−module Main

2−

3−f : Nat -> Nat

4−f x = x + 1

5−

6−foo : Nat -> Nat

7−foo (f x) = x

8−

9−main : IO ()

10−main = putStrLn (show (foo 1))

test/test028/expecteddeleted−1

@@ -1 +0,0 @@

1−hello, world!

test/test028/rundeleted−4

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

1−#!/usr/bin/env bash

2−idris $@ test028.idr -o test028

3−./test028

4−rm -f test028 test028.ibc

test/test010/expected → test/totality001/expectedrenamed

The content is the same.

test/test010/run → test/totality001/runrenamed

The content is the same.

test/test010/test010.idr → test/totality001/test010.idrrenamed

The content is the same.

test/test010/test010a.idr → test/totality001/test010a.idrrenamed

The content is the same.

test/test010/test010b.idr → test/totality001/test010b.idrrenamed

The content is the same.

test/test017/expected → test/totality002/expectedrenamed

The content is the same.

test/test017/run → test/totality002/runrenamed

The content is the same.

test/test017/test017.idr → test/totality002/test017.idrrenamed

The content is the same.

test/test017/test017a.idr → test/totality002/test017a.idrrenamed

The content is the same.

test/test017/test017b.idr → test/totality002/test017b.idrrenamed

The content is the same.