cc7ef9a · Idris-dev · git.iko.soy

CHANGELOG.md+12−7

compare with master

unifiedsplit

@@ -1,17 +1,22 @@

1−# New in 1.2.*

1+# New in 1.3.*

2

3−+ REPL now prints an error message if program compiled by `:exec` terminates

3+## Language updates

4− abnormally.

4++ Old 'induction' tactics and eliminator generation functionality ('%elim', '%case', 'elim_for') is no longer supported.

5+ Please, rely on the ones provided by Pruviloj and elaborator reflection instead.

6+

7+## Library updates

8+

9++ changed rndInt in Effect.Random so that it does not alternate between odd

10+ and even.

5+ Additions to `contrib`:

11+ Additions to `contrib`:

6 * `Data.SortedBag`: Bag (or Multiset) implemention based on `Data.SortedMap`.

12 * `Data.SortedBag`: Bag (or Multiset) implemention based on `Data.SortedMap`.

7 * `Data.PosNat`: A `Nat` paired with a proof that it is positive.

13 * `Data.PosNat`: A `Nat` paired with a proof that it is positive.

8 * `Data.Chain`: A function with an arbitrary number of arguments, plus

14 * `Data.Chain`: A function with an arbitrary number of arguments, plus

9 combinators for working with them.

15 combinators for working with them.

10

16

11−## Library Updates

17+## Tool updates

12−

18++ REPL now prints an error message if program compiled by `:exec` terminates

13−+ changed rndInt in Effect.Random so that it does not alternate between odd

19+ abnormally.

14− and even.

15

20

16# New in 1.2.0

21# New in 1.2.0

17

22

docs/reference/tactics.rst−13

@@ -173,19 +173,6 @@ rewrite

173 Vect Z a

174 -lemma>

175

176−induction

177−---------

178−

179−- ``induction`` - (``Note that this is still experimental`` and you may

180− get strange results and error messages. We are aware of these and

181− will finish the implementation eventually!) Prove the goal by

182− induction. Each constructor of the datatype becomes a goal.

183− Constructors with recursive arguments become induction steps, while

184− simple constructors become base cases. Note that this only works for

185− datatypes that have eliminators: a datatype definition must have the

186− ``%elim`` modifier.

187−

188−

189sourceLocation

176sourceLocation

190--------------

177--------------

191

178

libs/base/Data/Vect.idr−1

@@ -11,7 +11,6 @@ infixr 7 ::

11||| Vectors: Generic lists with explicit length in the type

12||| @ len the length of the list

13||| @ elem the type of elements

14−%elim

15data Vect : (len : Nat) -> (elem : Type) -> Type where

14data Vect : (len : Nat) -> (elem : Type) -> Type where

16 ||| Empty vector

15 ||| Empty vector

17 Nil : Vect Z elem

16 Nil : Vect Z elem

libs/base/Language/Reflection/Utils.idr−3

@@ -91,7 +91,6 @@ mutual

91 showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s

92 showPrec d (MethodN n) = showCon d "MethodN" $ showArg n

93 showPrec d (CaseN fc n) = showCon d "CaseN" $ showArg fc ++ showArg n

94− showPrec d (ElimN n) = showCon d "ElimN" $ showArg n

95 showPrec d (ImplementationCtorN n) = showCon d "ImplementationCtorN" $ showArg n

94 showPrec d (ImplementationCtorN n) = showCon d "ImplementationCtorN" $ showArg n

96 showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta

95 showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta

97

96

@@ -116,7 +115,6 @@ mutual

116 (ParentN n s) == (ParentN n' s') = n == n' && s == s'

115 (ParentN n s) == (ParentN n' s') = n == n' && s == s'

117 (MethodN n) == (MethodN n') = n == n'

116 (MethodN n) == (MethodN n') = n == n'

118 (CaseN fc n) == (CaseN fc' n') = fc == fc' && n == n'

117 (CaseN fc n) == (CaseN fc' n') = fc == fc' && n == n'

119− (ElimN n) == (ElimN n') = n == n'

120 (ImplementationCtorN n) == (ImplementationCtorN n') = n == n'

118 (ImplementationCtorN n) == (ImplementationCtorN n') = n == n'

121 (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'

119 (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'

122 _ == _ = False

120 _ == _ = False

@@ -336,7 +334,6 @@ implementation Show Err where

336 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs

334 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs

337 showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs

335 showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs

338 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm

336 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm

339− showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm

340 showPrec d UniverseError = "UniverseError"

337 showPrec d UniverseError = "UniverseError"

341 showPrec d ProgramLineComment = "ProgramLineComment"

338 showPrec d ProgramLineComment = "ProgramLineComment"

342 showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n

339 showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n

libs/base/base.ipkg+1−1

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

1package base

2

3−opts = "--nobasepkgs --total --no-elim-deprecation-warnings --partial-eval -i ../prelude"

3+opts = "--nobasepkgs --total --partial-eval -i ../prelude"

4

5modules = Control.Arrow

6 , Control.Catchable

libs/prelude/Builtins.idr+3−3

@@ -7,7 +7,7 @@

7

8||| The canonical single-element type, also known as the trivially

9||| true proposition.

10−%elim data Unit =

10+data Unit =

11 ||| The trivial constructor for `()`.

12 MkUnit

13

@@ -15,7 +15,7 @@ namespace Builtins

15 ||| The non-dependent pair type, also known as conjunction.

16 ||| @A the type of the left elements in the pair

17 ||| @B the type of the right elements in the pair

18− %elim data Pair : (A : Type) -> (B : Type) -> Type where

18+ data Pair : (A : Type) -> (B : Type) -> Type where

19 ||| A pair of elements

20 ||| @a the left element of the pair

21 ||| @b the right element of the pair

@@ -54,7 +54,7 @@ namespace Builtins

54||| The empty type, also known as the trivially false proposition.

55|||

56||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope.

57−%elim data Void : Type where

57+data Void : Type where

58

59||| The eliminator for the `Void` type.

60void : Void -> a

libs/prelude/Language/Reflection.idr−76

@@ -69,7 +69,6 @@ mutual

69 | ParentN TTName String

70 | MethodN TTName

71 | CaseN SourceLocation TTName

72− | ElimN TTName

73 | ImplementationCtorN TTName

72 | ImplementationCtorN TTName

74 | MetaN TTName TTName

73 | MetaN TTName TTName

75 %name SpecialName sn, sn'

74 %name SpecialName sn, sn'

@@ -129,9 +128,6 @@ implementation Uninhabited ((WhereN x n n') = (MethodN y)) where

129implementation Uninhabited ((WhereN x n n') = (CaseN loc y)) where

128implementation Uninhabited ((WhereN x n n') = (CaseN loc y)) where

130 uninhabited Refl impossible

129 uninhabited Refl impossible

131

130

132−implementation Uninhabited ((WhereN x n n') = (ElimN y)) where

133− uninhabited Refl impossible

134−

135implementation Uninhabited ((WhereN x n n') = (ImplementationCtorN y)) where

131implementation Uninhabited ((WhereN x n n') = (ImplementationCtorN y)) where

136 uninhabited Refl impossible

132 uninhabited Refl impossible

137

133

@@ -153,9 +149,6 @@ implementation Uninhabited ((WithN x n) = (MethodN n')) where

153implementation Uninhabited ((WithN x n) = (CaseN loc n')) where

149implementation Uninhabited ((WithN x n) = (CaseN loc n')) where

154 uninhabited Refl impossible

150 uninhabited Refl impossible

155

151

156−implementation Uninhabited ((WithN x n) = (ElimN n')) where

157− uninhabited Refl impossible

158−

159implementation Uninhabited ((WithN x n) = (ImplementationCtorN n')) where

152implementation Uninhabited ((WithN x n) = (ImplementationCtorN n')) where

160 uninhabited Refl impossible

153 uninhabited Refl impossible

161

154

@@ -177,9 +170,6 @@ implementation Uninhabited ((ImplementationN n xs) = (MethodN n')) where

177implementation Uninhabited ((ImplementationN n xs) = (CaseN loc n')) where

170implementation Uninhabited ((ImplementationN n xs) = (CaseN loc n')) where

178 uninhabited Refl impossible

171 uninhabited Refl impossible

179

172

180−implementation Uninhabited ((ImplementationN n xs) = (ElimN n')) where

181− uninhabited Refl impossible

182−

183implementation Uninhabited ((ImplementationN n xs) = (ImplementationCtorN n')) where

173implementation Uninhabited ((ImplementationN n xs) = (ImplementationCtorN n')) where

184 uninhabited Refl impossible

174 uninhabited Refl impossible

185

175

@@ -201,9 +191,6 @@ implementation Uninhabited ((ParentN n x) = (MethodN n')) where

201implementation Uninhabited ((ParentN n x) = (CaseN loc n')) where

191implementation Uninhabited ((ParentN n x) = (CaseN loc n')) where

202 uninhabited Refl impossible

192 uninhabited Refl impossible

203

193

204−implementation Uninhabited ((ParentN n x) = (ElimN n')) where

205− uninhabited Refl impossible

206−

207implementation Uninhabited ((ParentN n x) = (ImplementationCtorN n')) where

194implementation Uninhabited ((ParentN n x) = (ImplementationCtorN n')) where

208 uninhabited Refl impossible

195 uninhabited Refl impossible

209

196

@@ -225,9 +212,6 @@ implementation Uninhabited ((MethodN n) = (ParentN n' x)) where

225implementation Uninhabited ((MethodN n) = (CaseN loc n')) where

212implementation Uninhabited ((MethodN n) = (CaseN loc n')) where

226 uninhabited Refl impossible

213 uninhabited Refl impossible

227

214

228−implementation Uninhabited ((MethodN n) = (ElimN n')) where

229− uninhabited Refl impossible

230−

231implementation Uninhabited ((MethodN n) = (ImplementationCtorN n')) where

215implementation Uninhabited ((MethodN n) = (ImplementationCtorN n')) where

232 uninhabited Refl impossible

216 uninhabited Refl impossible

233

217

@@ -249,39 +233,12 @@ implementation Uninhabited ((CaseN loc n) = (ParentN n' x)) where

249implementation Uninhabited ((CaseN loc n) = (MethodN n')) where

233implementation Uninhabited ((CaseN loc n) = (MethodN n')) where

250 uninhabited Refl impossible

234 uninhabited Refl impossible

251

235

252−implementation Uninhabited ((CaseN loc n) = (ElimN n')) where

253− uninhabited Refl impossible

254−

255implementation Uninhabited ((CaseN loc n) = (ImplementationCtorN n')) where

236implementation Uninhabited ((CaseN loc n) = (ImplementationCtorN n')) where

256 uninhabited Refl impossible

237 uninhabited Refl impossible

257

238

258implementation Uninhabited ((CaseN loc n) = (MetaN n' x)) where

239implementation Uninhabited ((CaseN loc n) = (MetaN n' x)) where

259 uninhabited Refl impossible

240 uninhabited Refl impossible

260

241

261−implementation Uninhabited ((ElimN n) = (WhereN x n' y)) where

262− uninhabited Refl impossible

263−

264−implementation Uninhabited ((ElimN n) = (WithN x n')) where

265− uninhabited Refl impossible

266−

267−implementation Uninhabited ((ElimN n) = (ImplementationN n' xs)) where

268− uninhabited Refl impossible

269−

270−implementation Uninhabited ((ElimN n) = (ParentN n' x)) where

271− uninhabited Refl impossible

272−

273−implementation Uninhabited ((ElimN n) = (MethodN n')) where

274− uninhabited Refl impossible

275−

276−implementation Uninhabited ((ElimN n) = (CaseN loc n')) where

277− uninhabited Refl impossible

278−

279−implementation Uninhabited ((ElimN n) = (ImplementationCtorN n')) where

280− uninhabited Refl impossible

281−

282−implementation Uninhabited ((ElimN n) = (MetaN n' x)) where

283− uninhabited Refl impossible

284−

285implementation Uninhabited ((ImplementationCtorN n) = (WhereN x n' y)) where

242implementation Uninhabited ((ImplementationCtorN n) = (WhereN x n' y)) where

286 uninhabited Refl impossible

243 uninhabited Refl impossible

287

244

@@ -300,9 +257,6 @@ implementation Uninhabited ((ImplementationCtorN n) = (MethodN n')) where

300implementation Uninhabited ((ImplementationCtorN n) = (CaseN loc n')) where

257implementation Uninhabited ((ImplementationCtorN n) = (CaseN loc n')) where

301 uninhabited Refl impossible

258 uninhabited Refl impossible

302

259

303−implementation Uninhabited ((ImplementationCtorN n) = (ElimN n')) where

304− uninhabited Refl impossible

305−

306implementation Uninhabited ((ImplementationCtorN n) = (MetaN n' x)) where

260implementation Uninhabited ((ImplementationCtorN n) = (MetaN n' x)) where

307 uninhabited Refl impossible

261 uninhabited Refl impossible

308

262

@@ -324,9 +278,6 @@ implementation Uninhabited ((MetaN n n') = (MethodN x)) where

324implementation Uninhabited ((MetaN n n') = (CaseN loc x)) where

278implementation Uninhabited ((MetaN n n') = (CaseN loc x)) where

325 uninhabited Refl impossible

279 uninhabited Refl impossible

326

280

327−implementation Uninhabited ((MetaN n n') = (ElimN x)) where

328− uninhabited Refl impossible

329−

330implementation Uninhabited ((MetaN n n') = (ImplementationCtorN x)) where

281implementation Uninhabited ((MetaN n n') = (ImplementationCtorN x)) where

331 uninhabited Refl impossible

282 uninhabited Refl impossible

332

283

@@ -415,10 +366,6 @@ mutual

415 caseNInj : (CaseN loc n = CaseN loc' n') -> (loc = loc', n = n')

366 caseNInj : (CaseN loc n = CaseN loc' n') -> (loc = loc', n = n')

416 caseNInj Refl = (Refl, Refl)

367 caseNInj Refl = (Refl, Refl)

417

368

418− private

419− elimNInj : (ElimN n = ElimN n') -> n = n'

420− elimNInj Refl = Refl

421−

422 private

369 private

423 implementationCtorNInj : (ImplementationCtorN n = ImplementationCtorN n') -> n = n'

370 implementationCtorNInj : (ImplementationCtorN n = ImplementationCtorN n') -> n = n'

424 implementationCtorNInj Refl = Refl

371 implementationCtorNInj Refl = Refl

@@ -445,7 +392,6 @@ mutual

445 decSNEq (WhereN x n n') (ParentN y z) = No absurd

392 decSNEq (WhereN x n n') (ParentN y z) = No absurd

446 decSNEq (WhereN x n n') (MethodN y) = No absurd

393 decSNEq (WhereN x n n') (MethodN y) = No absurd

447 decSNEq (WhereN x n n') (CaseN loc y) = No absurd

394 decSNEq (WhereN x n n') (CaseN loc y) = No absurd

448− decSNEq (WhereN x n n') (ElimN y) = No absurd

449 decSNEq (WhereN x n n') (ImplementationCtorN y) = No absurd

395 decSNEq (WhereN x n n') (ImplementationCtorN y) = No absurd

450 decSNEq (WhereN x n n') (MetaN y z) = No absurd

396 decSNEq (WhereN x n n') (MetaN y z) = No absurd

451 decSNEq (WithN x n) (WhereN y n' z) = No absurd

397 decSNEq (WithN x n) (WhereN y n' z) = No absurd

@@ -461,7 +407,6 @@ mutual

461 decSNEq (WithN x n) (ParentN n' y) = No absurd

407 decSNEq (WithN x n) (ParentN n' y) = No absurd

462 decSNEq (WithN x n) (MethodN n') = No absurd

408 decSNEq (WithN x n) (MethodN n') = No absurd

463 decSNEq (WithN x n) (CaseN loc n') = No absurd

409 decSNEq (WithN x n) (CaseN loc n') = No absurd

464− decSNEq (WithN x n) (ElimN n') = No absurd

465 decSNEq (WithN x n) (ImplementationCtorN n') = No absurd

410 decSNEq (WithN x n) (ImplementationCtorN n') = No absurd

466 decSNEq (WithN x n) (MetaN n' y) = No absurd

411 decSNEq (WithN x n) (MetaN n' y) = No absurd

467 decSNEq (ImplementationN n xs) (WhereN x n' y) = No absurd

412 decSNEq (ImplementationN n xs) (WhereN x n' y) = No absurd

@@ -477,7 +422,6 @@ mutual

477 decSNEq (ImplementationN n xs) (ParentN n' x) = No absurd

422 decSNEq (ImplementationN n xs) (ParentN n' x) = No absurd

478 decSNEq (ImplementationN n xs) (MethodN n') = No absurd

423 decSNEq (ImplementationN n xs) (MethodN n') = No absurd

479 decSNEq (ImplementationN n xs) (CaseN loc n') = No absurd

424 decSNEq (ImplementationN n xs) (CaseN loc n') = No absurd

480− decSNEq (ImplementationN n xs) (ElimN n') = No absurd

481 decSNEq (ImplementationN n xs) (ImplementationCtorN n') = No absurd

425 decSNEq (ImplementationN n xs) (ImplementationCtorN n') = No absurd

482 decSNEq (ImplementationN n xs) (MetaN n' x) = No absurd

426 decSNEq (ImplementationN n xs) (MetaN n' x) = No absurd

483 decSNEq (ParentN n x) (WhereN y n' z) = No absurd

427 decSNEq (ParentN n x) (WhereN y n' z) = No absurd

@@ -493,7 +437,6 @@ mutual

493 No $ contra . fst . parentNInj

437 No $ contra . fst . parentNInj

494 decSNEq (ParentN n x) (MethodN n') = No absurd

438 decSNEq (ParentN n x) (MethodN n') = No absurd

495 decSNEq (ParentN n x) (CaseN loc n') = No absurd

439 decSNEq (ParentN n x) (CaseN loc n') = No absurd

496− decSNEq (ParentN n x) (ElimN n') = No absurd

497 decSNEq (ParentN n x) (ImplementationCtorN n') = No absurd

440 decSNEq (ParentN n x) (ImplementationCtorN n') = No absurd

498 decSNEq (ParentN n x) (MetaN n' y) = No absurd

441 decSNEq (ParentN n x) (MetaN n' y) = No absurd

499 decSNEq (MethodN n) (WhereN x n' y) = No absurd

442 decSNEq (MethodN n) (WhereN x n' y) = No absurd

@@ -506,7 +449,6 @@ mutual

506 decSNEq (MethodN n) (MethodN n') | No contra =

449 decSNEq (MethodN n) (MethodN n') | No contra =

507 No $ contra . methodNInj

450 No $ contra . methodNInj

508 decSNEq (MethodN n) (CaseN loc n') = No absurd

451 decSNEq (MethodN n) (CaseN loc n') = No absurd

509− decSNEq (MethodN n) (ElimN n') = No absurd

510 decSNEq (MethodN n) (ImplementationCtorN n') = No absurd

452 decSNEq (MethodN n) (ImplementationCtorN n') = No absurd

511 decSNEq (MethodN n) (MetaN n' x) = No absurd

453 decSNEq (MethodN n) (MetaN n' x) = No absurd

512 decSNEq (CaseN loc n) (WhereN x n' y) = No absurd

454 decSNEq (CaseN loc n) (WhereN x n' y) = No absurd

@@ -522,29 +464,14 @@ mutual

522 No $ contra . snd . caseNInj

464 No $ contra . snd . caseNInj

523 decSNEq (CaseN loc n) (CaseN loc' n') | No contra =

465 decSNEq (CaseN loc n) (CaseN loc' n') | No contra =

524 No $ contra . fst . caseNInj

466 No $ contra . fst . caseNInj

525− decSNEq (CaseN loc n) (ElimN n') = No absurd

526 decSNEq (CaseN loc n) (ImplementationCtorN n') = No absurd

467 decSNEq (CaseN loc n) (ImplementationCtorN n') = No absurd

527 decSNEq (CaseN loc n) (MetaN n' x) = No absurd

468 decSNEq (CaseN loc n) (MetaN n' x) = No absurd

528− decSNEq (ElimN n) (WhereN x n' y) = No absurd

529− decSNEq (ElimN n) (WithN x n') = No absurd

530− decSNEq (ElimN n) (ImplementationN n' xs) = No absurd

531− decSNEq (ElimN n) (ParentN n' x) = No absurd

532− decSNEq (ElimN n) (MethodN n') = No absurd

533− decSNEq (ElimN n) (CaseN loc n') = No absurd

534− decSNEq (ElimN n) (ElimN n') with (assert_total $ decTTNameEq n n')

535− decSNEq (ElimN n) (ElimN n) | Yes Refl =

536− Yes Refl

537− decSNEq (ElimN n) (ElimN n') | No contra =

538− No $ contra . elimNInj

539− decSNEq (ElimN n) (ImplementationCtorN n') = No absurd

540− decSNEq (ElimN n) (MetaN n' x) = No absurd

541 decSNEq (ImplementationCtorN n) (WhereN x n' y) = No absurd

469 decSNEq (ImplementationCtorN n) (WhereN x n' y) = No absurd

542 decSNEq (ImplementationCtorN n) (WithN x n') = No absurd

470 decSNEq (ImplementationCtorN n) (WithN x n') = No absurd

543 decSNEq (ImplementationCtorN n) (ImplementationN n' xs) = No absurd

471 decSNEq (ImplementationCtorN n) (ImplementationN n' xs) = No absurd

544 decSNEq (ImplementationCtorN n) (ParentN n' x) = No absurd

472 decSNEq (ImplementationCtorN n) (ParentN n' x) = No absurd

545 decSNEq (ImplementationCtorN n) (MethodN n') = No absurd

473 decSNEq (ImplementationCtorN n) (MethodN n') = No absurd

546 decSNEq (ImplementationCtorN n) (CaseN loc n') = No absurd

474 decSNEq (ImplementationCtorN n) (CaseN loc n') = No absurd

547− decSNEq (ImplementationCtorN n) (ElimN n') = No absurd

548 decSNEq (ImplementationCtorN n) (ImplementationCtorN n') with (assert_total $ decTTNameEq n n')

475 decSNEq (ImplementationCtorN n) (ImplementationCtorN n') with (assert_total $ decTTNameEq n n')

549 decSNEq (ImplementationCtorN n) (ImplementationCtorN n) | Yes Refl =

476 decSNEq (ImplementationCtorN n) (ImplementationCtorN n) | Yes Refl =

550 Yes Refl

477 Yes Refl

@@ -557,7 +484,6 @@ mutual

557 decSNEq (MetaN n n') (ParentN x y) = No absurd

484 decSNEq (MetaN n n') (ParentN x y) = No absurd

558 decSNEq (MetaN n n') (MethodN x) = No absurd

485 decSNEq (MetaN n n') (MethodN x) = No absurd

559 decSNEq (MetaN n n') (CaseN loc x) = No absurd

486 decSNEq (MetaN n n') (CaseN loc x) = No absurd

560− decSNEq (MetaN n n') (ElimN x) = No absurd

561 decSNEq (MetaN n n') (ImplementationCtorN x) = No absurd

487 decSNEq (MetaN n n') (ImplementationCtorN x) = No absurd

562 decSNEq (MetaN n n') (MetaN x y) with (assert_total $ decTTNameEq n x)

488 decSNEq (MetaN n n') (MetaN x y) with (assert_total $ decTTNameEq n x)

563 decSNEq (MetaN n n') (MetaN n y) | Yes Refl with (assert_total $ decTTNameEq n' y)

489 decSNEq (MetaN n n') (MetaN n y) | Yes Refl with (assert_total $ decTTNameEq n' y)

@@ -1006,7 +932,6 @@ mutual

1006 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))

932 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))

1007 quote (MethodN n) = `(MethodN ~(quote n))

933 quote (MethodN n) = `(MethodN ~(quote n))

1008 quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))

934 quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))

1009− quote (ElimN n) = `(ElimN ~(quote n))

1010 quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n))

935 quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n))

1011 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))

936 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))

1012

937

@@ -1026,7 +951,6 @@ mutual

1026 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))

951 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))

1027 quote (MethodN n) = `(MethodN ~(quote n))

952 quote (MethodN n) = `(MethodN ~(quote n))

1028 quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))

953 quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))

1029− quote (ElimN n) = `(ElimN ~(quote n))

1030 quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n))

954 quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n))

1031 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))

955 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))

1032

956

libs/prelude/Language/Reflection/Errors.idr−1

@@ -35,7 +35,6 @@ data Err = Msg String

35 | CantResolveAlts (List TTName)

36 | NoValidAlts (List TTName)

37 | IncompleteTerm TT

38− | NoEliminator String TT

39 | UniverseError

38 | UniverseError

40 | ProgramLineComment

39 | ProgramLineComment

41 | Inaccessible TTName

40 | Inaccessible TTName

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

@@ -7,7 +7,7 @@ import Prelude.Uninhabited

7%access public export

8

9||| Boolean Data Type

10−%case data Bool = False | True

10+data Bool = False | True

11

12||| The underlying implementation of the if ... then ... else ... syntax

13||| @ b the condition on the if

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

@@ -11,7 +11,7 @@ import Prelude.List

11%access public export

12

13||| A sum type

14−%elim data Either : (a, b : Type) -> Type where

14+data Either : (a, b : Type) -> Type where

15 ||| One possibility of the sum, conventionally used to represent errors

16 Left : (l : a) -> Either a b

17 ||| The other possibility, conventionally used to represent success

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

@@ -66,7 +66,7 @@ Eq Bool where

66

67

68-- ---------------------------------------------------------- [ Ordering Interface ]

69−%elim data Ordering = LT | EQ | GT

69+data Ordering = LT | EQ | GT

70

71Eq Ordering where

72 LT == LT = True

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

@@ -19,7 +19,7 @@ infix 5 \\

19infixr 7 ::,++

20

21||| Generic lists

22−%elim data List : (elem : Type) -> Type where

22+data List : (elem : Type) -> Type where

23 ||| Empty list

24 Nil : List elem

25 ||| A non-empty list, consisting of a head element and the rest of

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

@@ -14,7 +14,7 @@ import Prelude.Uninhabited

14

15||| Natural numbers: unbounded, unsigned integers which can be pattern

16||| matched.

17−%elim data Nat =

17+data Nat =

18 ||| Zero

19 Z |

20 ||| Successor

libs/prelude/prelude.ipkg+1−1

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

1package prelude

2

3−opts = "--nobuiltins --total --no-elim-deprecation-warnings --partial-eval"

3+opts = "--nobuiltins --total --partial-eval"

4

5modules = Builtins

6

man/idris.1−2

@@ -101,8 +101,6 @@ should not necessarily be seen as production ready nor for industrial use.

101 --nocolor,--nocolour Disable coloured output

102 --consolewidth WIDTH Select console width: auto, infinite, nat

103 --highlight Emit source code highlighting

104− --no-elim-deprecation-warnings

105− Disable deprecation warnings for %elim

106 --no-tactic-deprecation-warnings

104 --no-tactic-deprecation-warnings

107 Disable deprecation warnings for the old tactic

105 Disable deprecation warnings for the old tactic

108 sublanguage

106 sublanguage

src/IRTS/Compiler.hs−1

@@ -197,7 +197,6 @@ showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)

197 snRank (ParentN n s) = "3" ++ nameRank n ++ show s

198 snRank (MethodN n) = "4" ++ nameRank n

199 snRank (CaseN _ n) = "5" ++ nameRank n

200− snRank (ElimN n) = "6" ++ nameRank n

201 snRank (ImplementationCtorN n) = "7" ++ nameRank n

200 snRank (ImplementationCtorN n) = "7" ++ nameRank n

202 snRank (WithN i n) = "8" ++ nameRank n ++ show i

201 snRank (WithN i n) = "8" ++ nameRank n ++ show i

203

202

src/Idris/AbsSyntaxTree.hs−4

@@ -1092,8 +1092,6 @@ mapPT f t = f (mpt t) where

1092

1093data PTactic' t = Intro [Name] | Intros | Focus Name

1094 | Refine Name [Bool] | Rewrite t | DoUnify

1095− | Induction t

1096− | CaseTac t

1097 | Equiv t

1095 | Equiv t

1098 | Claim Name t

1096 | Claim Name t

1099 | Unfocus

1097 | Unfocus

@@ -1132,7 +1130,6 @@ instance Sized a => Sized (PTactic' a) where

1132 size (Focus nm) = 1 + size nm

1130 size (Focus nm) = 1 + size nm

1133 size (Refine nm bs) = 1 + size nm + length bs

1131 size (Refine nm bs) = 1 + size nm + length bs

1134 size (Rewrite t) = 1 + size t

1132 size (Rewrite t) = 1 + size t

1135− size (Induction t) = 1 + size t

1136 size (LetTac nm t) = 1 + size nm + size t

1133 size (LetTac nm t) = 1 + size nm + size t

1137 size (Exact t) = 1 + size t

1134 size (Exact t) = 1 + size t

1138 size Compute = 1

1135 size Compute = 1

@@ -1153,7 +1150,6 @@ instance Sized a => Sized (PTactic' a) where

1153 size (TFail ts) = 1 + size ts

1150 size (TFail ts) = 1 + size ts

1154 size SourceFC = 1

1151 size SourceFC = 1

1155 size DoUnify = 1

1152 size DoUnify = 1

1156− size (CaseTac x) = 1 + size x

1157 size (Equiv t) = 1 + size t

1153 size (Equiv t) = 1 + size t

1158 size (Claim x y) = 1 + size x + size y

1154 size (Claim x y) = 1 + size x + size y

1159 size Unfocus = 1

1155 size Unfocus = 1

src/Idris/CmdOptions.hs−1

@@ -222,7 +222,6 @@ parseFlags = many $

222

223 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

224

225− <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")

226 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

225 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

227

226

228 where

227 where

src/Idris/Core/Binary.hs−6

@@ -133,9 +133,6 @@ instance Binary a => Binary (Err' a) where

133 put x1

134 put x2

135 put x3

136− put (NoEliminator s t) = do putWord8 37

137− put s

138− put t

139 put (InvalidTCArg n t) = do putWord8 38

136 put (InvalidTCArg n t) = do putWord8 38

140 put n

137 put n

141 put t

138 put t

@@ -211,9 +208,6 @@ instance Binary a => Binary (Err' a) where

211 x2 <- get

208 x2 <- get

212 x3 <- get

209 x3 <- get

213 return (ElabScriptDebug x1 x2 x3)

210 return (ElabScriptDebug x1 x2 x3)

214− 37 -> do x1 <- get

215− x2 <- get

216− return (NoEliminator x1 x2)

217 38 -> do x1 <- get

211 38 -> do x1 <- get

218 x2 <- get

212 x2 <- get

219 return (InvalidTCArg x1 x2)

213 return (InvalidTCArg x1 x2)

src/Idris/Core/Elaborate.hs−6

@@ -446,12 +446,6 @@ expandLet n v = processTactic' (ExpandLet n v)

446rewrite :: Raw -> Elab' aux ()

447rewrite tm = processTactic' (Rewrite tm)

448

449−induction :: Raw -> Elab' aux ()

450−induction tm = processTactic' (Induction tm)

451−

452−casetac :: Raw -> Elab' aux ()

453−casetac tm = processTactic' (CaseTac tm)

454−

455equiv :: Raw -> Elab' aux ()

449equiv :: Raw -> Elab' aux ()

456equiv tm = processTactic' (Equiv tm)

450equiv tm = processTactic' (Equiv tm)

457

451

src/Idris/Core/ProofState.hs−60

@@ -91,8 +91,6 @@ data Tactic = Attack

91 | LetBind Name RigCount Raw Raw

92 | ExpandLet Name Term

93 | Rewrite Raw

94− | Induction Raw

95− | CaseTac Raw

96 | Equiv Raw

94 | Equiv Raw

97 | PatVar Name

95 | PatVar Name

98 | PatBind Name RigCount

96 | PatBind Name RigCount

@@ -728,62 +726,6 @@ mkP lt l r (Bind n b sc)

728 b { binderTy = ty' }

726 b { binderTy = ty' }

729mkP lt l r x = x

727mkP lt l r x = x

730

728

731−casetac :: Raw -> Bool -> RunTactic

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

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

734− let tmt' = normalise ctxt env tmt

735− let (tacn, tacstr, _) = if induction

736− then (ElimN, "eliminator", "Induction")

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

738− case unApply tmt' of

739− (P _ tnm _, tyargs) -> do

740− case lookupTy (SN (tacn tnm)) ctxt of

741− [elimTy] -> do

742− param_pos <- case lookupMetaInformation tnm ctxt of

743− [DataMI param_pos] -> return param_pos

744− m | not (null tyargs) -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)

745− _ -> return []

746− let (params, indicies) = splitTyArgs param_pos tyargs

747− let args = getArgTys elimTy

748− let args' = drop (length params) args

749− let restargs = init $ tail args'

750− let consargs = take (length restargs - length indicies) restargs

751− let indxnames = makeIndexNames indicies

752− currentNames <- query $ allTTNames . getProofTerm . pterm

753− let tmnm = case tm of

754− Var nm -> uniqueNameCtxt ctxt nm currentNames

755− _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames

756− let tmvar = P Bound tmnm tmt'

757− prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam RigW tmt') (mkP tmvar tmv tmvar t)

758− consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)

759− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

760− (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

761− action (\ps -> ps {holes = holes ps \\ [x],

762− recents = x : recents ps })

763− mapM_ addConsHole (reverse consargs')

764− let res' = forget res

765− (scv, sct) <- lift $ check ctxt env res'

766− let (scv', _) = specialise ctxt env [] scv

767− return scv'

768− [] -> lift $ tfail $ NoEliminator tacstr tmt'

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

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

771− tmt'

772− where makeConsArg (nm, ty) = P Bound nm ty

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

774− bindConsArgs [] v = v

775− addConsHole (nm, ty) =

776− action (\ps -> ps { holes = nm : holes ps })

777− splitTyArgs param_pos tyargs =

778− let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs

779− in (map snd params, map snd indicies)

780− makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []

781− replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

782− let var = P Bound idnm idxt

783− return $ Bind idnm (Lam RigW idxt) (mkP var idxv var t)) prop $ zip idnms idxs

784−casetac tm induction ctxt env _ = fail $ "Can't do " ++ (if induction then "induction" else "case analysis") ++ " here"

785−

786−

787equiv :: Raw -> RunTactic

729equiv :: Raw -> RunTactic

788equiv tm ctxt env (Bind x (Hole t) sc) =

730equiv tm ctxt env (Bind x (Hole t) sc) =

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

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

@@ -1111,8 +1053,6 @@ process t h = tactic (Just h) (mktac t)

1111 mktac (LetBind n r t v) = letbind n r t v

1053 mktac (LetBind n r t v) = letbind n r t v

1112 mktac (ExpandLet n b) = expandLet n b

1054 mktac (ExpandLet n b) = expandLet n b

1113 mktac (Rewrite t) = rewrite t

1055 mktac (Rewrite t) = rewrite t

1114− mktac (Induction t) = casetac t True

1115− mktac (CaseTac t) = casetac t False

1116 mktac (Equiv t) = equiv t

1056 mktac (Equiv t) = equiv t

1117 mktac (PatVar n) = patvar n

1057 mktac (PatVar n) = patvar n

1118 mktac (PatBind n rig) = patbind n rig

1058 mktac (PatBind n rig) = patbind n rig

src/Idris/Core/TT.hs−7

@@ -273,7 +273,6 @@ data Err' t

273 | CantResolveAlts [Name]

274 | NoValidAlts [Name]

275 | IncompleteTerm t

276− | NoEliminator String t

277 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

276 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

278 -- ^ Location, bad universe, old domain, new domain, suspects

277 -- ^ Location, bad universe, old domain, new domain, suspects

279 | UniqueError Universe Name

278 | UniqueError Universe Name

@@ -485,7 +484,6 @@ data SpecialName = WhereN !Int !Name !Name

485 | ParentN !Name !T.Text

484 | ParentN !Name !T.Text

486 | MethodN !Name

485 | MethodN !Name

487 | CaseN !FC' !Name

486 | CaseN !FC' !Name

488− | ElimN !Name

489 | ImplementationCtorN !Name

487 | ImplementationCtorN !Name

490 | MetaN !Name !Name

488 | MetaN !Name !Name

491 deriving (Eq, Ord, Data, Generic, Typeable)

489 deriving (Eq, Ord, Data, Generic, Typeable)

@@ -530,7 +528,6 @@ instance Show SpecialName where

530 show (ParentN p c) = show p ++ "#" ++ T.unpack c

528 show (ParentN p c) = show p ++ "#" ++ T.unpack c

531 show (CaseN fc n) = "case block in " ++ show n ++

529 show (CaseN fc n) = "case block in " ++ show n ++

532 if fc == FC' emptyFC then "" else " at " ++ show fc

530 if fc == FC' emptyFC then "" else " at " ++ show fc

533− show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

534 show (ImplementationCtorN n) = "constructor of " ++ show n

531 show (ImplementationCtorN n) = "constructor of " ++ show n

535 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"

532 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"

536

533

@@ -547,7 +544,6 @@ showCG (SN s) = showCG' s

547 showCG' (MethodN m) = '!':showCG m

544 showCG' (MethodN m) = '!':showCG m

548 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

545 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

549 showCG' (CaseN fc c) = showCG c ++ showFC' fc ++ "_case"

546 showCG' (CaseN fc c) = showCG c ++ showFC' fc ++ "_case"

550− showCG' (ElimN sn) = showCG sn ++ "_elim"

551 showCG' (ImplementationCtorN n) = showCG n ++ "_ictor"

547 showCG' (ImplementationCtorN n) = showCG n ++ "_ictor"

552 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta

548 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta

553 showFC' (FC' NoFC) = ""

549 showFC' (FC' NoFC) = ""

@@ -1090,8 +1086,6 @@ data Datatype n = Data { d_typename :: n,

1090

1086

1091-- | Data declaration options

1087-- | Data declaration options

1092data DataOpt = Codata -- ^ Set if the the data-type is coinductive

1088data DataOpt = Codata -- ^ Set if the the data-type is coinductive

1093− | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

1094− | DefaultCaseFun -- ^ Set if a case function should be generated for data type

1095 | DataErrRev

1089 | DataErrRev

1096 deriving (Show, Eq, Generic)

1090 deriving (Show, Eq, Generic)

1097

1091

@@ -1512,7 +1506,6 @@ nextName (SN x) = SN (nextName' x)

1512 nextName' (ImplementationN n ns) = ImplementationN (nextName n) ns

1506 nextName' (ImplementationN n ns) = ImplementationN (nextName n) ns

1513 nextName' (ParentN n ns) = ParentN (nextName n) ns

1507 nextName' (ParentN n ns) = ParentN (nextName n) ns

1514 nextName' (CaseN fc n) = CaseN fc (nextName n)

1508 nextName' (CaseN fc n) = CaseN fc (nextName n)

1515− nextName' (ElimN n) = ElimN (nextName n)

1516 nextName' (MethodN n) = MethodN (nextName n)

1509 nextName' (MethodN n) = MethodN (nextName n)

1517 nextName' (ImplementationCtorN n) = ImplementationCtorN (nextName n)

1510 nextName' (ImplementationCtorN n) = ImplementationCtorN (nextName n)

1518 nextName' (MetaN parent meta) = MetaN parent (nextName meta)

1511 nextName' (MetaN parent meta) = MetaN parent (nextName meta)

src/Idris/Delaborate.hs−6

@@ -460,12 +460,6 @@ pprintErr' i (IncompleteTerm t)

460 getMissing hs env (App _ f a)

461 = getMissing hs env f ++ getMissing hs env a

462 getMissing hs env _ = []

463−pprintErr' i (NoEliminator s t)

464− = text "No " <> text s <> text " for type " <+>

465− annTm t (pprintTerm i (delabSugared i t)) <$>

466− text "Please note that 'induction' is experimental." <$>

467− text "Only types declared with '%elim' can be used." <$>

468− text "Consider writing a pattern matching definition instead."

469pprintErr' i (UniverseError fc uexp old new suspects) =

463pprintErr' i (UniverseError fc uexp old new suspects) =

470 text "Universe inconsistency." <>

464 text "Universe inconsistency." <>

471 (indented . vsep) [ text "Working on:" <+> text (show uexp)

465 (indented . vsep) [ text "Working on:" <+> text (show uexp)

src/Idris/Elab/Data.hs−247

@@ -110,12 +110,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

110 >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)

111 _ -> return ()

112

113− -- create an eliminator

114− when (DefaultEliminator `elem` opts) $

115− evalStateT (elabCaseFun True params n t dcons info) Map.empty

116− -- create a case function

117− when (DefaultCaseFun `elem` opts) $

118− evalStateT (elabCaseFun False params n t dcons info) Map.empty

119 -- create a rewriting lemma

113 -- create a rewriting lemma

120 when (n /= sUN "=") $

114 when (n /= sUN "=") $

121 elabRewriteLemma info n cty

115 elabRewriteLemma info n cty

@@ -312,244 +306,3 @@ addParamConstraints fc ps cty cons

312 addIBC (IBCConstraint fc con)

306 addIBC (IBCConstraint fc con)

313 _ -> return ()

307 _ -> return ()

314 constraintTy t = return ()

308 constraintTy t = return ()

315−

316−type EliminatorState = StateT (Map.Map String Int) Idris

317−

318−-- -- Issue #1616 in the issue tracker.

319−-- https://github.com/idris-lang/Idris-dev/issues/1616

320−--

321−-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

322−-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

323−-- rename to caseFun to match updated intend

324−elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

325− [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])] ->

326− ElabInfo -> EliminatorState ()

327−elabCaseFun ind paramPos n ty cons info = do

328− elimLog "Elaborating case function"

329− put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

330− let (cnstrs, _) = splitPi ty

331− let (pms, idxs) = splitPms cnstrs

332− generalParams <- namePis False pms

333− motiveIdxs <- namePis False idxs

334− let motive = mkMotive n paramPos generalParams motiveIdxs

335− consTerms <- mapM (\(c@(_, _, cnm, _, _, _, _)) -> do

336− let casefunt = if ind then "elim_" else "case_"

337− name <- freshName $ casefunt ++ simpleName cnm

338− consTerm <- extractConsTerm c generalParams

339− return (name, expl, consTerm)) cons

340− scrutineeIdxs <- namePis False idxs

341− let motiveConstr = [(motiveName, expl, motive)]

342− let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

343− let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))

344− let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName elimFC eliminatorTy

345− let clauseConsElimArgs = map getPiName consTerms

346− let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

347− let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'

348− let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

349− elimLog elimSig

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

351− let eliminatorDef = PClauses elimFC [TotalFn] elimDeclName eliminatorClauses

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

353− State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)

354− (ierror . Elaborating "type declaration of " elimDeclName Nothing)

355− -- Do not elaborate clauses if there aren't any

356− case eliminatorClauses of

357− [] -> State.lift $ solveDeferred elimFC elimDeclName -- Remove meta-variable for type

358− _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

359− (ierror . Elaborating "clauses of " elimDeclName Nothing)

360− where elimLog :: String -> EliminatorState ()

361− elimLog s = State.lift (logElab 2 s)

362−

363− elimFC :: FC

364− elimFC = fileFC $ "(casefun " ++ show n ++ ")"

365−

366− elimDeclName :: Name

367− elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

368−

369− splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

370− splitPi = splitPi' []

371− where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

372− splitPi' acc (PPi pl n _ tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr

373− splitPi' acc t = (reverse acc, t)

374−

375− splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])

376− splitPms cnstrs = (map fst pms, map fst idxs)

377− where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])

378−

379− isMachineGenerated :: Name -> Bool

380− isMachineGenerated (MN _ _) = True

381− isMachineGenerated _ = False

382−

383− namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]

384− namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms

385− let oldNames = map fst names

386− let params = map snd names

387− return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params

388−

389− mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))

390− mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))

391− mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg

392− return (oldName, (name, pl, piarg))

393− where keyOf :: PTerm -> String

394− keyOf (PRef _ _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"

395− keyOf (PApp _ tyf _) = keyOf tyf

396− keyOf (PType _) = "ty__"

397− keyOf _ = "carg__"

398− nameStart :: Name -> Char

399− nameStart n = nameStart' (simpleName n)

400− where nameStart' :: String -> Char

401− nameStart' "" = ' '

402− nameStart' ns = head ns

403−

404− simpleName :: Name -> String

405− simpleName (NS n _) = simpleName n

406− simpleName (MN i n) = str n ++ show i

407− simpleName n = show n

408−

409− freshName :: String -> EliminatorState Name

410− freshName key = do

411− nameMap <- get

412− let i = fromMaybe 0 (Map.lookup key nameMap)

413− let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)

414− put $ Map.insert key (i+1) nameMap

415− return name

416−

417− scrutineeName :: Name

418− scrutineeName = sUN "scrutinee"

419−

420− scrutineeArgName :: Name

421− scrutineeArgName = sUN "scrutineeArg"

422−

423− motiveName :: Name

424− motiveName = sUN "prop"

425−

426− mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

427− mkMotive n paramPos params indicies =

428− let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))

429− in piConstr (indicies ++ [scrutineeTy]) (PType elimFC)

430−

431− piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm

432− piConstr [] ty = ty

433− piConstr ((n, pl, tyb):tyr) ty = PPi pl n elimFC tyb (piConstr tyr ty)

434−

435− interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]

436− interlievePos idxs [] l2 i = l2

437− interlievePos idxs l1 [] i = l1

438− interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))

439− interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))

440−

441− replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm

442− replaceParams paramPos params cns =

443− let (_, cnsResTy) = splitPi cns

444− in case cnsResTy of

445− PApp _ _ args ->

446− let oldParams = paramNamesOf 0 paramPos args

447− in removeParamPis oldParams params cns

448− _ -> cns

449−

450− removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm

451− removeParamPis oldParams params (PPi pl n fc tyb tyr) =

452− case findIndex (== n) oldParams of

453− Nothing -> (PPi pl n fc (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))

454− Just i -> (removeParamPis oldParams params tyr)

455− removeParamPis oldParams params (PRef _ _ n) =

456− case findIndex (== n) oldParams of

457− Nothing -> (PRef elimFC [] n)

458− Just i -> let (newname,_,_) = params !! i in (PRef elimFC [] (newname))

459− removeParamPis oldParams params (PApp _ cns args) =

460− PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args

461− where replaceParamArgs :: [PArg] -> [PArg]

462− replaceParamArgs [] = []

463− replaceParamArgs (arg:args) =

464− case extractName (getTm arg) of

465− [] -> arg:replaceParamArgs args

466− [n] ->

467− case findIndex (== n) oldParams of

468− Nothing -> arg:replaceParamArgs args

469− Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC [] newname}:replaceParamArgs args

470− removeParamPis oldParams params t = t

471−

472− paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]

473− paramNamesOf i paramPos [] = []

474− paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args

475−

476− extractName :: PTerm -> [Name]

477− extractName (PRef _ _ n) = [n]

478− extractName _ = []

479−

480− splitArgPms :: PTerm -> ([PTerm], [PTerm])

481− splitArgPms (PApp _ f args) = splitArgPms' args

482− where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])

483− splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)

484− where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])

485− splitArgPms _ = ([],[])

486−

487−

488− implicitIndexes :: (Docstring (Either Err PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

489− implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

490− i <- State.lift getIState

491− implargs' <- case lookupCtxt cnm (idris_implicits i) of

492− [] -> do fail $ "Error while showing implicits for " ++ show cnm

493− [args] -> do return args

494− _ -> do fail $ "Ambigous name for " ++ show cnm

495− let implargs = mapMaybe convertImplPi implargs'

496− let (_, cnsResTy) = splitPi ty

497− case cnsResTy of

498− PApp _ _ args ->

499− let oldParams = paramNamesOf 0 paramPos args

500− in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

501− _ -> return implargs

502−

503− extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

504− extractConsTerm (doc, argDocs, cnm, _, ty, fc, fs) generalParameters = do

505− let cons' = replaceParams paramPos generalParameters ty

506− let (args, resTy) = splitPi cons'

507− implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

508− consArgs <- namePis False args

509− let recArgs = findRecArgs consArgs

510− let recMotives = if ind then map applyRecMotive recArgs else []

511− let (_, consIdxs) = splitArgPms resTy

512− return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

513− where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

514− applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC [] n))

515− where (_, idxs) = splitArgPms ty

516−

517− findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

518− findRecArgs [] = []

519− findRecArgs (ty@(_,_,PRef _ _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

520− findRecArgs (ty@(_,_,PApp _ (PRef _ _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

521− findRecArgs (ty:rs) = findRecArgs rs

522−

523− applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm

524− applyCons tn targs = PApp elimFC (PRef elimFC [] tn) (map convertArg targs)

525−

526− convertArg :: (Name, Plicity, PTerm) -> PArg

527− convertArg (n, _, _) = pexp (PRef elimFC [] n)

528−

529− applyMotive :: [PTerm] -> PTerm -> PTerm

530− applyMotive idxs t = PApp elimFC (PRef elimFC [] motiveName) (map pexp idxs ++ [pexp t])

531−

532− getPiName :: (Name, Plicity, PTerm) -> Name

533− getPiName (name,_,_) = name

534−

535− convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)

536− convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

537− convertImplPi _ = Nothing

538−

539− generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

540− generateEliminatorClauses (doc, _, cnm, _, ty, fc, fs) cnsElim generalArgs generalParameters = do

541− let cons' = replaceParams paramPos generalParameters ty

542− let (args, resTy) = splitPi cons'

543− i <- State.lift getIState

544− implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

545− let (_, generalIdxs') = splitArgPms resTy

546− let generalIdxs = map pexp generalIdxs'

547− consArgs <- namePis False args

548− let lhsPattern = PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

549− let recArgs = findRecArgs consArgs

550− let recElims = if ind then map applyRecElim recArgs else []

551− let rhsExpr = PApp elimFC (PRef elimFC [] cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

552− return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

553− where applyRecElim :: (Name, Plicity, PTerm) -> PArg

554− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC [] recCnm])

555− where (_, idxs) = splitArgPms recTy

src/Idris/Elab/Quasiquote.hs−1

@@ -23,7 +23,6 @@ extract2 n c a b = do (a', ex1) <- extractUnquotes n a

23

24extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])

25extractTUnquotes n (Rewrite t) = extract1 n Rewrite t

26−extractTUnquotes n (Induction t) = extract1 n Induction t

27extractTUnquotes n (LetTac name t) = extract1 n (LetTac name) t

26extractTUnquotes n (LetTac name t) = extract1 n (LetTac name) t

28extractTUnquotes n (LetTacTy name t1 t2) = extract2 n (LetTacTy name) t1 t2

27extractTUnquotes n (LetTacTy name t1 t2) = extract2 n (LetTacTy name) t1 t2

29extractTUnquotes n (Exact tm) = extract1 n Exact tm

28extractTUnquotes n (Exact tm) = extract1 n Exact tm

src/Idris/Elab/Term.hs−22

@@ -1749,24 +1749,6 @@ collectDeferred top casenames ctxt tm = cd [] tm

1749 (cd env a)

1750 cd env t = return t

1751

1752−case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1753−case_ ind autoSolve ist fn tm = do

1754− attack

1755− tyn <- getNameFrom (sMN 0 "ity")

1756− claim tyn RType

1757− valn <- getNameFrom (sMN 0 "ival")

1758− claim valn (Var tyn)

1759− letn <- getNameFrom (sMN 0 "irule")

1760− letbind letn RigW (Var tyn) (Var valn)

1761− focus valn

1762− elab ist toplevel ERHS [] (sMN 0 "tac") tm

1763− env <- get_env

1764− let (Just binding) = lookupBinder letn env

1765− let val = binderVal binding

1766− if ind then induction (forget val)

1767− else casetac (forget val)

1768− when autoSolve solveAll

1769−

1770-- | Compute the appropriate name for a top-level metavariable

1752-- | Compute the appropriate name for a top-level metavariable

1771metavarName :: [String] -> Name -> Name

1753metavarName :: [String] -> Name -> Name

1772metavarName _ n@(NS _ _) = n

1754metavarName _ n@(NS _ _) = n

@@ -2416,10 +2398,6 @@ runTac autoSolve ist perhapsFC fn tac

2416 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2398 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2417 rewrite (Var letn)

2399 rewrite (Var letn)

2418 when autoSolve solveAll

2400 when autoSolve solveAll

2419− runT (Induction tm) -- let bind tm, similar to the others

2420− = case_ True autoSolve ist fn tm

2421− runT (CaseTac tm)

2422− = case_ False autoSolve ist fn tm

2423 runT (LetTac n tm)

2401 runT (LetTac n tm)

2424 = do attack

2402 = do attack

2425 tyn <- getNameFrom (sMN 0 "letty")

2403 tyn <- getNameFrom (sMN 0 "letty")

src/Idris/IdrisDoc.hs−2

@@ -342,8 +342,6 @@ extractPTactic (Intro ns) = ns

342extractPTactic (Focus n) = [n]

343extractPTactic (Refine n _) = [n]

344extractPTactic (Rewrite p) = extract p

345−extractPTactic (Induction p) = extract p

346−extractPTactic (CaseTac p) = extract p

347extractPTactic (Equiv p) = extract p

345extractPTactic (Equiv p) = extract p

348extractPTactic (MatchRefine n) = [n]

346extractPTactic (MatchRefine n) = [n]

349extractPTactic (LetTac n p) = n : extract p

347extractPTactic (LetTac n p) = n : extract p

src/Idris/Options.hs−1

@@ -93,7 +93,6 @@ data Opt = Filename String

93 | UseConsoleWidth ConsoleWidth

94 | DumpHighlights

95 | DesugarNats

96− | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim

97 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

96 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

98 deriving (Show, Eq, Generic)

97 deriving (Show, Eq, Generic)

99

98

src/Idris/Parser/Data.hs+7−25

@@ -134,29 +134,15 @@ recordI :: IdrisParser DataOpts

134recordI = do keyword "record"; return []

135 <|> do keyword "corecord"; return [Codata]

136

137−{- | Parses if a data should not have a default eliminator

138−DefaultEliminator ::= 'noelim'?

139− -}

140dataOpts :: DataOpts -> IdrisParser DataOpts

137dataOpts :: DataOpts -> IdrisParser DataOpts

141−dataOpts opts

138+dataOpts opts =

142− = do let kw = "%elim"

143− fc <- extent $ reserved kw

144− warnElim fc kw

145− dataOpts (DefaultEliminator : DefaultCaseFun : opts)

146− <|> do let kw = "%case"

147− fc <- extent $ reserved kw

148− warnElim fc kw

149− dataOpts (DefaultCaseFun : opts)

150− <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

139+ do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

151 <|> return opts

140 <|> return opts

152 <?> "data options"

141 <?> "data options"

153− where warnElim fc kw =

154− parserWarning fc (Just NoElimDeprecationWarnings)

155− (Msg ("The '" ++ kw ++ "' directive is deprecated."))

156

142

157{- | Parses a data type declaration

143{- | Parses a data type declaration

158−Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

144+Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?

159− | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?

145+ | DocComment? Accessibility? DataI FnName Name* DataRest?

160 ;

146 ;

161Constructor' ::= Constructor KeepTerminator;

147Constructor' ::= Constructor KeepTerminator;

162ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

148ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

@@ -175,10 +161,10 @@ data_ syn = (checkDeclFixity $

175 (doc, argDocs) <- P.option noDocs docComment

161 (doc, argDocs) <- P.option noDocs docComment

176 pushIndent

162 pushIndent

177 acc <- accessibility

163 acc <- accessibility

178− elim <- dataOpts []

164+ errRev <- dataOpts []

179 co <- dataI

165 co <- dataI

180 ist <- get

166 ist <- get

181− let dataOpts = combineDataOpts (elim ++ co)

167+ let dataOpts = errRev ++ co

182 doc' = annotCode (tryFullExpr syn ist) doc

168 doc' = annotCode (tryFullExpr syn ist) doc

183 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

169 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

184 | (n, d) <- argDocs ]

170 | (n, d) <- argDocs ]

@@ -201,7 +187,7 @@ data_ syn = (checkDeclFixity $

201 let tyn = expandNS syn tyn_in

187 let tyn = expandNS syn tyn_in

202 d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do

188 d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do

203 P.try (lchar '=') <|> do keyword "where"

189 P.try (lchar '=') <|> do keyword "where"

204− let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

190+ let kw = (if Codata `elem` dataOpts then "co" else "") ++ "data "

205 let n = show tyn_in ++ " "

191 let n = show tyn_in ++ " "

206 let s = kw ++ n

192 let s = kw ++ n

207 let as = unwords (map show args) ++ " "

193 let as = unwords (map show args) ++ " "

@@ -227,10 +213,6 @@ data_ syn = (checkDeclFixity $

227 mkPApp fc t xs = PApp fc t (map pexp xs)

213 mkPApp fc t xs = PApp fc t (map pexp xs)

228 bindArgs :: [PTerm] -> PTerm -> PTerm

214 bindArgs :: [PTerm] -> PTerm -> PTerm

229 bindArgs xs t = foldr (PPi expl (sMN 0 "_t") NoFC) t xs

215 bindArgs xs t = foldr (PPi expl (sMN 0 "_t") NoFC) t xs

230− combineDataOpts :: DataOpts -> DataOpts

231− combineDataOpts opts = if Codata `elem` opts

232− then delete DefaultEliminator opts

233− else opts

234

216

235

217

236{- | Parses a type constructor declaration

218{- | Parses a type constructor declaration

src/Idris/Parser/Expr.hs−3

@@ -391,7 +391,6 @@ simpleExpr syn =

391 <|> do lchar '%'; fc <- extent $ reserved "instance"

392 parserWarning fc Nothing $ Msg "The use of %instance is deprecated, use %implementation instead."

393 return (PResolveTC fc)

394− <|> do reserved "elim_for"; (t, fc) <- withExtent $ fnName; return (PRef fc [] (SN $ ElimN t))

395 <|> proofExpr syn

394 <|> proofExpr syn

396 <|> tacticsExpr syn

395 <|> tacticsExpr syn

397 <|> P.try (do fc <- extent (reserved "Type*"); return $ PUniverse fc AllTypes)

396 <|> P.try (do fc <- extent (reserved "Type*"); return $ PUniverse fc AllTypes)

@@ -1491,8 +1490,6 @@ tactics =

1491 do n <- spaced fnName

1490 do n <- spaced fnName

1492 return $ MatchRefine n)

1491 return $ MatchRefine n)

1493 , expressionTactic ["rewrite"] Rewrite

1492 , expressionTactic ["rewrite"] Rewrite

1494− , expressionTactic ["case"] CaseTac

1495− , expressionTactic ["induction"] Induction

1496 , expressionTactic ["equiv"] Equiv

1493 , expressionTactic ["equiv"] Equiv

1497 , (["let"], Nothing, \syn -> -- FIXME syntax for let

1494 , (["let"], Nothing, \syn -> -- FIXME syntax for let

1498 do n <- (indentGt *> name)

1495 do n <- (indentGt *> name)

src/Idris/Reflection.hs−10

@@ -115,8 +115,6 @@ reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist

115reifyApp ist t [Constant (Str n), x]

116 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

117reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

118−reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

119−reifyApp ist t [t'] | t == reflm "Case" = liftM (CaseTac . delab ist) (reifyTT t')

120reifyApp ist t [t']

118reifyApp ist t [t']

121 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

119 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

122reifyApp ist t [t']

120reifyApp ist t [t']

@@ -278,9 +276,6 @@ reifyTTNameApp t [sn]

278 reifySN t [fc, n]

276 reifySN t [fc, n]

279 | t == reflm "CaseN" =

277 | t == reflm "CaseN" =

280 CaseN <$> (FC' <$> reifyFC fc) <*> reifyTTName n

278 CaseN <$> (FC' <$> reifyFC fc) <*> reifyTTName n

281− reifySN t [n]

282− | t == reflm "ElimN" =

283− ElimN <$> reifyTTName n

284 reifySN t [n]

279 reifySN t [n]

285 | t == reflm "ImplementationCtorN" =

280 | t == reflm "ImplementationCtorN" =

286 ImplementationCtorN <$> reifyTTName n

281 ImplementationCtorN <$> reifyTTName n

@@ -722,8 +717,6 @@ reflectSpecialName (MethodN n) =

722 reflCall "MethodN" [reflectName n]

717 reflCall "MethodN" [reflectName n]

723reflectSpecialName (CaseN fc n) =

718reflectSpecialName (CaseN fc n) =

724 reflCall "CaseN" [reflectFC (unwrapFC fc), reflectName n]

719 reflCall "CaseN" [reflectFC (unwrapFC fc), reflectName n]

725−reflectSpecialName (ElimN n) =

726− reflCall "ElimN" [reflectName n]

727reflectSpecialName (ImplementationCtorN n) =

720reflectSpecialName (ImplementationCtorN n) =

728 reflCall "ImplementationCtorN" [reflectName n]

721 reflCall "ImplementationCtorN" [reflectName n]

729reflectSpecialName (MetaN parent meta) =

722reflectSpecialName (MetaN parent meta) =

@@ -928,9 +921,6 @@ reflectErr (CantResolveAlts ss) =

928 raw_apply (Var $ reflErrName "CantResolveAlts")

921 raw_apply (Var $ reflErrName "CantResolveAlts")

929 [rawList (Var $ reflm "TTName") (map reflectName ss)]

922 [rawList (Var $ reflm "TTName") (map reflectName ss)]

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

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

931−reflectErr (NoEliminator str t)

932− = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

933− reflect t]

934reflectErr (UniverseError fc ue old new tys) =

924reflectErr (UniverseError fc ue old new tys) =

935 -- NB: loses information, but OK because this is not likely to be rewritten

925 -- NB: loses information, but OK because this is not likely to be rewritten

936 Var $ reflErrName "UniverseError"

926 Var $ reflErrName "UniverseError"

test/pkg010/expected+2−2

23 [--O3] | [--O2] | [--O1] | [--O0] | [--partial-eval] |

24 [--no-partial-eval] | [-O|--level ARG] | [--target TRIPLE] | [--cpu CPU]

26− [--highlight] | [--no-elim-deprecation-warnings] |

27− [--no-tactic-deprecation-warnings]) [FILES] [-v|--version]

26+ [--highlight] | [--no-tactic-deprecation-warnings]) [FILES]

27+ [-v|--version]

28)

test/quasiquote001/expected+2−2

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

1App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))))

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

3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 27))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 29))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar "./QuasiquoteBasics.idr" 30))))

3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 27))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 29))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 30)) (TType (UVar "./Builtins.idr" 32))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 33)) (TType (UVar "./Builtins.idr" 35))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 36))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 37))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar "./QuasiquoteBasics.idr" 30))))

4--------------

5−App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))

5+App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 30)) (TType (UVar "./Builtins.idr" 32))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 33)) (TType (UVar "./Builtins.idr" 35))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 36))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 37))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 30)) (TType (UVar "./Builtins.idr" 32))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 33)) (TType (UVar "./Builtins.idr" 35))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 36))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 37))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 30)) (TType (UVar "./Builtins.idr" 32))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 33)) (TType (UVar "./Builtins.idr" 35))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 36))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 37))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))