8442cef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Deprecate '%assert_total'

8442cefEdwin Brady10 years ago

CHANGELOG.md+8

compare with master

unifiedsplit

@@ -73,6 +73,14 @@

73 them as mutually defined functions with their top level function, meaning

74 that it can spot more total functions.

76+* The totality checker now looks under `if...then...else` blocks when checking

77+ for productivity.

78+

79+* The `%assert_total` directive is now deprecated. Instead, you can

80+ use one of the functions `assert_total`, `assert_smaller` or

81+ `assert_unreachable` to describe more precisely where a totality assertion

82+ is needed.

83+

76## Library updates

84## Library updates

78* `Control.WellFounded` module removed, and added to the Prelude as

86* `Control.WellFounded` module removed, and added to the Prelude as

libs/base/Data/Bits.idr+30−9

@@ -2,7 +2,8 @@ module Data.Bits

3import Data.Fin

5−%default total

5+%default total -- This file is full of totality assertions though. Let's try

6+ -- to improve it! (EB)

6%access export

7%access export

8public export

9public export

@@ -28,7 +29,6 @@ machineTy (S (S (S _))) = Bits64

28bitsUsed : Nat -> Nat

29bitsUsed : Nat -> Nat

29bitsUsed n = 8 * (2 `power` n)

30bitsUsed n = 8 * (2 `power` n)

31−%assert_total

32natToBits' : %static {n : Nat} -> machineTy n -> Nat -> machineTy n

33natToBits' a Z = a

34natToBits' {n=n} a x with (n)

@@ -37,6 +37,7 @@ natToBits' {n=n} a x with (n)

37 natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'

38 natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'

39 natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'

40+ natToBits' a _ | _ = assert_unreachable

41natToBits : %static {n : Nat} -> Nat -> machineTy n

42natToBits : %static {n : Nat} -> Nat -> machineTy n

42natToBits {n=n} x with (n)

43natToBits {n=n} x with (n)

@@ -44,9 +45,10 @@ natToBits {n=n} x with (n)

44 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x

45 | S Z = natToBits' {n=1} (prim__truncInt_B16 0) x

45 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x

46 | S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x

46 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x

47 | S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x

48+ | _ = assert_unreachable

48getPad : %static {n : Nat} -> Nat -> machineTy n

50getPad : %static {n : Nat} -> Nat -> machineTy n

49−getPad n = natToBits (minus (bitsUsed (nextBytes n)) n)

51+getPad n = assert_total $ natToBits (minus (bitsUsed (nextBytes n)) n)

51public export

53public export

52data Bits : Nat -> Type where

54data Bits : Nat -> Type where

@@ -101,6 +103,7 @@ shiftLeft' {n=n} x c with (nextBytes n)

101 | S Z = pad16' n prim__shlB16 x c

103 | S Z = pad16' n prim__shlB16 x c

102 | S (S Z) = pad32' n prim__shlB32 x c

104 | S (S Z) = pad32' n prim__shlB32 x c

103 | S (S (S _)) = pad64' n prim__shlB64 x c

105 | S (S (S _)) = pad64' n prim__shlB64 x c

106+ | _ = assert_unreachable

104

107

105shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n

108shiftLeft : %static {n : Nat} -> Bits n -> Bits n -> Bits n

106shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

109shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)

@@ -111,6 +114,7 @@ shiftRightLogical' {n=n} x c with (n)

111 | S Z = prim__lshrB16 x c

114 | S Z = prim__lshrB16 x c

112 | S (S Z) = prim__lshrB32 x c

115 | S (S Z) = prim__lshrB32 x c

113 | S (S (S _)) = prim__lshrB64 x c

116 | S (S (S _)) = prim__lshrB64 x c

117+ | _ = assert_unreachable

114

118

115shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n

119shiftRightLogical : %static {n : Nat} -> Bits n -> Bits n -> Bits n

116shiftRightLogical {n} (MkBits x) (MkBits y)

120shiftRightLogical {n} (MkBits x) (MkBits y)

@@ -122,6 +126,7 @@ shiftRightArithmetic' {n=n} x c with (nextBytes n)

122 | S Z = pad16' n prim__ashrB16 x c

126 | S Z = pad16' n prim__ashrB16 x c

123 | S (S Z) = pad32' n prim__ashrB32 x c

127 | S (S Z) = pad32' n prim__ashrB32 x c

124 | S (S (S _)) = pad64' n prim__ashrB64 x c

128 | S (S (S _)) = pad64' n prim__ashrB64 x c

129+ | _ = assert_unreachable

125

130

126shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n

131shiftRightArithmetic : %static {n : Nat} -> Bits n -> Bits n -> Bits n

127shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

132shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)

@@ -132,6 +137,7 @@ and' {n=n} x y with (n)

132 | S Z = prim__andB16 x y

137 | S Z = prim__andB16 x y

133 | S (S Z) = prim__andB32 x y

138 | S (S Z) = prim__andB32 x y

134 | S (S (S _)) = prim__andB64 x y

139 | S (S (S _)) = prim__andB64 x y

140+ | _ = assert_unreachable

135

141

136and : %static {n : Nat} -> Bits n -> Bits n -> Bits n

142and : %static {n : Nat} -> Bits n -> Bits n -> Bits n

137and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

143and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)

@@ -142,6 +148,7 @@ or' {n=n} x y with (n)

142 | S Z = prim__orB16 x y

148 | S Z = prim__orB16 x y

143 | S (S Z) = prim__orB32 x y

149 | S (S Z) = prim__orB32 x y

144 | S (S (S _)) = prim__orB64 x y

150 | S (S (S _)) = prim__orB64 x y

151+ | _ = assert_unreachable

145

152

146or : %static {n : Nat} -> Bits n -> Bits n -> Bits n

153or : %static {n : Nat} -> Bits n -> Bits n -> Bits n

147or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

154or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)

@@ -152,6 +159,7 @@ xor' {n=n} x y with (n)

152 | S Z = prim__xorB16 x y

159 | S Z = prim__xorB16 x y

153 | S (S Z) = prim__xorB32 x y

160 | S (S Z) = prim__xorB32 x y

154 | S (S (S _)) = prim__xorB64 x y

161 | S (S (S _)) = prim__xorB64 x y

162+ | _ = assert_unreachable

155

163

156xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n

164xor : %static {n : Nat} -> Bits n -> Bits n -> Bits n

157xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

165xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)

@@ -162,6 +170,7 @@ plus' {n=n} x y with (nextBytes n)

162 | S Z = pad16 n prim__addB16 x y

170 | S Z = pad16 n prim__addB16 x y

163 | S (S Z) = pad32 n prim__addB32 x y

171 | S (S Z) = pad32 n prim__addB32 x y

164 | S (S (S _)) = pad64 n prim__addB64 x y

172 | S (S (S _)) = pad64 n prim__addB64 x y

173+ | _ = assert_unreachable

165

174

166plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

175plus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

167plus (MkBits x) (MkBits y) = MkBits (plus' x y)

176plus (MkBits x) (MkBits y) = MkBits (plus' x y)

@@ -172,6 +181,7 @@ minus' {n=n} x y with (nextBytes n)

172 | S Z = pad16 n prim__subB16 x y

181 | S Z = pad16 n prim__subB16 x y

173 | S (S Z) = pad32 n prim__subB32 x y

182 | S (S Z) = pad32 n prim__subB32 x y

174 | S (S (S _)) = pad64 n prim__subB64 x y

183 | S (S (S _)) = pad64 n prim__subB64 x y

184+ | _ = assert_unreachable

175

185

176minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

186minus : %static {n : Nat} -> Bits n -> Bits n -> Bits n

177minus (MkBits x) (MkBits y) = MkBits (minus' x y)

187minus (MkBits x) (MkBits y) = MkBits (minus' x y)

@@ -182,6 +192,7 @@ times' {n=n} x y with (nextBytes n)

182 | S Z = pad16 n prim__mulB16 x y

192 | S Z = pad16 n prim__mulB16 x y

183 | S (S Z) = pad32 n prim__mulB32 x y

193 | S (S Z) = pad32 n prim__mulB32 x y

184 | S (S (S _)) = pad64 n prim__mulB64 x y

194 | S (S (S _)) = pad64 n prim__mulB64 x y

195+ | _ = assert_unreachable

185

196

186times : %static {n : Nat} -> Bits n -> Bits n -> Bits n

197times : %static {n : Nat} -> Bits n -> Bits n -> Bits n

187times (MkBits x) (MkBits y) = MkBits (times' x y)

198times (MkBits x) (MkBits y) = MkBits (times' x y)

@@ -193,6 +204,7 @@ sdiv' {n=n} x y with (nextBytes n)

193 | S Z = prim__sdivB16 x y

204 | S Z = prim__sdivB16 x y

194 | S (S Z) = prim__sdivB32 x y

205 | S (S Z) = prim__sdivB32 x y

195 | S (S (S _)) = prim__sdivB64 x y

206 | S (S (S _)) = prim__sdivB64 x y

207+ | _ = assert_unreachable

196

208

197partial

209partial

198sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

210sdiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

@@ -205,6 +217,7 @@ udiv' {n=n} x y with (nextBytes n)

205 | S Z = prim__udivB16 x y

217 | S Z = prim__udivB16 x y

206 | S (S Z) = prim__udivB32 x y

218 | S (S Z) = prim__udivB32 x y

207 | S (S (S _)) = prim__udivB64 x y

219 | S (S (S _)) = prim__udivB64 x y

220+ | _ = assert_unreachable

208

221

209partial

222partial

210udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

223udiv : %static {n : Nat} -> Bits n -> Bits n -> Bits n

@@ -217,6 +230,7 @@ srem' {n=n} x y with (nextBytes n)

217 | S Z = prim__sremB16 x y

230 | S Z = prim__sremB16 x y

218 | S (S Z) = prim__sremB32 x y

231 | S (S Z) = prim__sremB32 x y

219 | S (S (S _)) = prim__sremB64 x y

232 | S (S (S _)) = prim__sremB64 x y

233+ | _ = assert_unreachable

220

234

221partial

235partial

222srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

236srem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

@@ -229,6 +243,7 @@ urem' {n=n} x y with (nextBytes n)

229 | S Z = prim__uremB16 x y

243 | S Z = prim__uremB16 x y

230 | S (S Z) = prim__uremB32 x y

244 | S (S Z) = prim__uremB32 x y

231 | S (S (S _)) = prim__uremB64 x y

245 | S (S (S _)) = prim__uremB64 x y

246+ | _ = assert_unreachable

232

247

233partial

248partial

234urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

249urem : %static {n : Nat} -> Bits n -> Bits n -> Bits n

@@ -241,6 +256,7 @@ lt {n=n} x y with (nextBytes n)

241 | S Z = prim__ltB16 x y

256 | S Z = prim__ltB16 x y

242 | S (S Z) = prim__ltB32 x y

257 | S (S Z) = prim__ltB32 x y

243 | S (S (S _)) = prim__ltB64 x y

258 | S (S (S _)) = prim__ltB64 x y

259+ | _ = assert_unreachable

244

260

245lte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

261lte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

246lte {n=n} x y with (nextBytes n)

262lte {n=n} x y with (nextBytes n)

@@ -248,6 +264,7 @@ lte {n=n} x y with (nextBytes n)

248 | S Z = prim__lteB16 x y

264 | S Z = prim__lteB16 x y

249 | S (S Z) = prim__lteB32 x y

265 | S (S Z) = prim__lteB32 x y

250 | S (S (S _)) = prim__lteB64 x y

266 | S (S (S _)) = prim__lteB64 x y

267+ | _ = assert_unreachable

251

268

252eq : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

269eq : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

253eq {n=n} x y with (nextBytes n)

270eq {n=n} x y with (nextBytes n)

@@ -255,6 +272,7 @@ eq {n=n} x y with (nextBytes n)

255 | S Z = prim__eqB16 x y

272 | S Z = prim__eqB16 x y

256 | S (S Z) = prim__eqB32 x y

273 | S (S Z) = prim__eqB32 x y

257 | S (S (S _)) = prim__eqB64 x y

274 | S (S (S _)) = prim__eqB64 x y

275+ | _ = assert_unreachable

258

276

259gte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

277gte : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

260gte {n=n} x y with (nextBytes n)

278gte {n=n} x y with (nextBytes n)

@@ -262,6 +280,7 @@ gte {n=n} x y with (nextBytes n)

262 | S Z = prim__gteB16 x y

280 | S Z = prim__gteB16 x y

263 | S (S Z) = prim__gteB32 x y

281 | S (S Z) = prim__gteB32 x y

264 | S (S (S _)) = prim__gteB64 x y

282 | S (S (S _)) = prim__gteB64 x y

283+ | _ = assert_unreachable

265

284

266gt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

285gt : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int

267gt {n=n} x y with (nextBytes n)

286gt {n=n} x y with (nextBytes n)

@@ -269,6 +288,7 @@ gt {n=n} x y with (nextBytes n)

269 | S Z = prim__gtB16 x y

288 | S Z = prim__gtB16 x y

270 | S (S Z) = prim__gtB32 x y

289 | S (S Z) = prim__gtB32 x y

271 | S (S (S _)) = prim__gtB64 x y

290 | S (S (S _)) = prim__gtB64 x y

291+ | _ = assert_unreachable

272

292

273implementation Eq (Bits n) where

293implementation Eq (Bits n) where

274 (MkBits x) == (MkBits y) = boolOp eq x y

294 (MkBits x) == (MkBits y) = boolOp eq x y

@@ -295,12 +315,12 @@ complement' {n=n} x with (nextBytes n)

295 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad

315 prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad

296 | S (S (S _)) = let pad = getPad {n=3} n in

316 | S (S (S _)) = let pad = getPad {n=3} n in

297 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

317 prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad

318+ | _ = assert_unreachable

298

319

299complement : %static {n : Nat} -> Bits n -> Bits n

320complement : %static {n : Nat} -> Bits n -> Bits n

300complement (MkBits x) = MkBits (complement' x)

321complement (MkBits x) = MkBits (complement' x)

301

322

302-- TODO: Prove

323-- TODO: Prove

303−%assert_total -- can't verify coverage of with block

304zext' : %static {n : Nat} -> %static {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

324zext' : %static {n : Nat} -> %static {m : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

305zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

325zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

306 | (Z, Z) = believe_me x

326 | (Z, Z) = believe_me x

@@ -313,11 +333,11 @@ zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

313 | (S (S Z), S (S Z)) = believe_me x

333 | (S (S Z), S (S Z)) = believe_me x

314 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

334 | (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))

315 | (S (S (S _)), S (S (S _))) = believe_me x

335 | (S (S (S _)), S (S (S _))) = believe_me x

336+ | _ = assert_unreachable

316

337

317zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)

338zeroExtend : %static {n : Nat} -> %static {m : Nat} -> Bits n -> Bits (n+m)

318zeroExtend (MkBits x) = MkBits (zext' x)

339zeroExtend (MkBits x) = MkBits (zext' x)

319

340

320−%assert_total

321intToBits' : %static {n : Nat} -> Integer -> machineTy (nextBytes n)

341intToBits' : %static {n : Nat} -> Integer -> machineTy (nextBytes n)

322intToBits' {n=n} x with (nextBytes n)

342intToBits' {n=n} x with (nextBytes n)

323 | Z = let pad = getPad {n=0} n in

343 | Z = let pad = getPad {n=0} n in

@@ -328,6 +348,7 @@ intToBits' {n=n} x with (nextBytes n)

328 prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad

348 prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad

329 | S (S (S _)) = let pad = getPad {n=3} n in

349 | S (S (S _)) = let pad = getPad {n=3} n in

330 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

350 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

351+ | _ = assert_unreachable

331

352

332intToBits : %static {n : Nat} -> Integer -> Bits n

353intToBits : %static {n : Nat} -> Integer -> Bits n

333intToBits n = MkBits (intToBits' n)

354intToBits n = MkBits (intToBits' n)

@@ -341,6 +362,7 @@ bitsToInt' {n=n} x with (nextBytes n)

341 | S Z = prim__zextB16_BigInt x

362 | S Z = prim__zextB16_BigInt x

342 | S (S Z) = prim__zextB32_BigInt x

363 | S (S Z) = prim__zextB32_BigInt x

343 | S (S (S _)) = prim__zextB64_BigInt x

364 | S (S (S _)) = prim__zextB64_BigInt x

365+ | _ = assert_unreachable

344

366

345bitsToInt : %static {n : Nat} -> Bits n -> Integer

367bitsToInt : %static {n : Nat} -> Bits n -> Integer

346bitsToInt (MkBits x) = bitsToInt' x

368bitsToInt (MkBits x) = bitsToInt' x

@@ -353,7 +375,6 @@ zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

353-- cast x = MkBits (zeroUnused (natToBits n))

375-- cast x = MkBits (zeroUnused (natToBits n))

354

376

355-- TODO: Prove

377-- TODO: Prove

356−%assert_total -- can't verify coverage of with block

357sext' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

378sext' : %static {n : Nat} -> machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

358sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

379sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

359 | (Z, Z) = let pad = getPad {n=0} n in

380 | (Z, Z) = let pad = getPad {n=0} n in

@@ -382,12 +403,12 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

382 (prim__zextB32_B64 pad))

403 (prim__zextB32_B64 pad))

383 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

404 | (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in

384 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

405 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

406+ | _ = assert_unreachable

385

407

386----signExtend : Bits n -> Bits (n+m)

408----signExtend : Bits n -> Bits (n+m)

387--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

409--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

388

410

389-- TODO: Prove

411-- TODO: Prove

390−%assert_total -- can't verify coverage of with block

391trunc' : %static {m : Nat} -> %static {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)

412trunc' : %static {m : Nat} -> %static {n : Nat} -> machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)

392trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

413trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

393 | (Z, Z) = believe_me x

414 | (Z, Z) = believe_me x

@@ -400,6 +421,7 @@ trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))

400 | (S (S Z), S (S Z)) = believe_me x

421 | (S (S Z), S (S Z)) = believe_me x

401 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

422 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))

402 | (S (S (S _)), S (S (S _))) = believe_me x

423 | (S (S (S _)), S (S (S _))) = believe_me x

424+ | _ = assert_unreachable

403

425

404truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n

426truncate : %static {m : Nat} -> %static {n : Nat} -> Bits (m+n) -> Bits n

405truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

427truncate (MkBits x) = MkBits (zeroUnused (trunc' x))

@@ -419,10 +441,9 @@ unsetBit n x = x `and` complement (bitAt n)

419bitsToStr : %static {n : Nat} -> Bits n -> String

441bitsToStr : %static {n : Nat} -> Bits n -> String

420bitsToStr x = pack (helper last x)

442bitsToStr x = pack (helper last x)

421 where

443 where

422− %assert_total

423 helper : %static {n : Nat} -> Fin (S n) -> Bits n -> List Char

444 helper : %static {n : Nat} -> Fin (S n) -> Bits n -> List Char

424 helper FZ _ = []

445 helper FZ _ = []

425− helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

446+ helper (FS x) b = assert_total $ (if getBit x b then '1' else '0') :: helper (weaken x) b

426

447

427implementation Show (Bits n) where

448implementation Show (Bits n) where

428 show = bitsToStr

449 show = bitsToStr

libs/base/Data/Mod2.idr+3−4

@@ -24,7 +24,6 @@ public export partial

24rem : Mod2 n -> Mod2 n -> Mod2 n

25rem = modBin urem

27−%assert_total

28public export

27public export

29intToMod : {n : Nat} -> Integer -> Mod2 n

28intToMod : {n : Nat} -> Integer -> Mod2 n

30intToMod {n=n} x = MkMod2 (intToBits x)

29intToMod {n=n} x = MkMod2 (intToBits x)

@@ -53,10 +52,10 @@ implementation Cast (Bits n) (Mod2 n) where

53modToStr : Mod2 n -> String

52modToStr : Mod2 n -> String

54modToStr x = pack (reverse (helper x))

53modToStr x = pack (reverse (helper x))

55 where

54 where

56− %assert_total

57 helper : Mod2 n -> List Char

55 helper : Mod2 n -> List Char

56+ helper x = assert_total $

58− helper x = strIndex "0123456789" (prim__truncBigInt_Int (bitsToInt (cast (x `rem` 10))))

57+ strIndex "0123456789" (prim__truncBigInt_Int (bitsToInt (cast (x `rem` 10))))

59− :: (if x < 10 then [] else helper (x `div` 10))

58+ :: (if x < 10 then [] else helper (x `div` 10))

62implementation Show (Mod2 n) where

61implementation Show (Mod2 n) where

libs/base/Data/Primitives/Views.idr+12−10

@@ -18,11 +18,12 @@ namespace Integer

18 divides : (val : Integer) -> (d : Integer) -> Divides val d

19 divides val 0 = DivByZero

20 divides val d

21+ = assert_total $

21− = let dividend = if d < 0 then -(val `div` abs d)

22+ let dividend = if d < 0 then -(val `div` abs d)

22− else val `div` d

23+ else val `div` d

23− remainder = abs (val - dividend * d) in

24+ remainder = abs (val - dividend * d) in

24− believe_me (DivBy {d} {div = dividend} {rem = remainder}

25+ believe_me (DivBy {d} {div = dividend} {rem = remainder}

25− (believe_me (Refl {x = True})))

26+ (believe_me (Refl {x = True})))

27 ||| View for recursion over Integers

28 ||| View for recursion over Integers

28 data IntegerRec : Integer -> Type where

29 data IntegerRec : Integer -> Type where

@@ -54,11 +55,12 @@ namespace Int

54 divides : (val : Int) -> (d : Int) -> Divides val d

55 divides : (val : Int) -> (d : Int) -> Divides val d

55 divides val 0 = DivByZero

56 divides val 0 = DivByZero

56 divides val d

57 divides val d

58+ = assert_total $

57− = let dividend = if d < 0 then -(val `div` abs d)

59+ let dividend = if d < 0 then -(val `div` abs d)

58− else val `div` d

60+ else val `div` d

59− remainder = abs (val - dividend * d) in

61+ remainder = abs (val - dividend * d) in

60− believe_me (DivBy {d} {div = dividend} {rem = remainder}

62+ believe_me (DivBy {d} {div = dividend} {rem = remainder}

61− (believe_me (Refl {x = True})))

63+ (believe_me (Refl {x = True})))

63 ||| View for recursion over Ints

65 ||| View for recursion over Ints

64 data IntRec : Int -> Type where

66 data IntRec : Int -> Type where

libs/base/Data/String.idr+1−2

@@ -70,9 +70,8 @@ parseDouble = mkDouble . wfe . trim

70 Just $ (w * ex + f * ex)

71 mkDouble Nothing = Nothing

73− %assert_total

74 intPow : Integer -> Integer -> Double

73 intPow : Integer -> Integer -> Double

75− intPow base exp = if exp > 0 then (num base exp) else 1 / (num base exp)

74+ intPow base exp = assert_total $ if exp > 0 then (num base exp) else 1 / (num base exp)

76 where

75 where

77 num base 0 = 1

76 num base 0 = 1

78 num base e = if e < 0

77 num base e = if e < 0

libs/base/Language/Reflection/Utils.idr+26−23

@@ -235,33 +235,35 @@ implementation (Eq a) => Eq (Binder a) where

235

236implementation Show TT where

237 showPrec = my_show

238− where %assert_total my_show : Prec -> TT -> String

238+ where my_show : Prec -> TT -> String

239− my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t

239+ my_show d (P nt n t) = assert_total $ showCon d "P" $ showArg nt ++ showArg n ++ showArg t

240− my_show d (V i) = showCon d "V" $ showArg i

240+ my_show d (V i) = assert_total $ showCon d "V" $ showArg i

241− my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t

241+ my_show d (Bind n b t) = assert_total $ showCon d "Bind" $ showArg n ++ showArg b ++ showArg t

242− my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2

242+ my_show d (App t1 t2) = assert_total $ showCon d "App" $ showArg t1 ++ showArg t2

243− my_show d (TConst c) = showCon d "TConst" $ showArg c

243+ my_show d (TConst c) = assert_total $ showCon d "TConst" $ showArg c

244 my_show d Erased = "Erased"

245− my_show d (TType u) = showCon d "TType" $ showArg u

245+ my_show d (TType u) = assert_total $ showCon d "TType" $ showArg u

246+ my_show d (UType u) = "UType"

247+

248+implementation Eq Universe where

249+ Reflection.NullType == Reflection.NullType = True

250+ Reflection.UniqueType == Reflection.UniqueType = True

251+ Reflection.AllTypes == Reflection.AllTypes = True

252+ _ == _ = False

246

253

247implementation Eq TT where

254implementation Eq TT where

248 a == b = equalp a b

255 a == b = equalp a b

249− where %assert_total equalp : TT -> TT -> Bool

256+ where equalp : TT -> TT -> Bool

250− equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'

257+ equalp (P nt n t) (P nt' n' t') = assert_total $ nt == nt' && n == n' && t == t'

251− equalp (V i) (V i') = i == i'

258+ equalp (V i) (V i') = assert_total $ i == i'

252− equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'

259+ equalp (Bind n b t) (Bind n' b' t') = assert_total $ n == n' && b == b' && t == t'

253− equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'

260+ equalp (App t1 t2) (App t1' t2') = assert_total $ t1 == t1' && t2 == t2'

254 equalp (TConst c) (TConst c') = c == c'

261 equalp (TConst c) (TConst c') = c == c'

255 equalp Erased Erased = True

262 equalp Erased Erased = True

256 equalp (TType u) (TType u') = u == u'

263 equalp (TType u) (TType u') = u == u'

264+ equalp (UType u) (UType u') = u == u'

257 equalp x y = False

265 equalp x y = False

258

266

259−implementation Eq Universe where

260− Reflection.NullType == Reflection.NullType = True

261− Reflection.UniqueType == Reflection.UniqueType = True

262− Reflection.AllTypes == Reflection.AllTypes = True

263− _ == _ = False

264−

265total

267total

266forget : TT -> Maybe Raw

268forget : TT -> Maybe Raw

267forget tm = fe [] tm

269forget tm = fe [] tm

@@ -288,12 +290,13 @@ forget tm = fe [] tm

288

290

289implementation Show Raw where

291implementation Show Raw where

290 showPrec = my_show

292 showPrec = my_show

291− where %assert_total my_show : Prec -> Raw -> String

293+ where my_show : Prec -> Raw -> String

292− my_show d (Var n) = showCon d "Var" $ showArg n

294+ my_show d (Var n) = assert_total $ showCon d "Var" $ showArg n

293− my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm

295+ my_show d (RBind n b tm) = assert_total $ showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm

294− my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'

296+ my_show d (RApp tm tm') = assert_total $ showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'

295 my_show d RType = "RType"

297 my_show d RType = "RType"

296− my_show d (RConstant c) = showCon d "RConstant" $ showArg c

298+ my_show d (RConstant c) = assert_total $ showCon d "RConstant" $ showArg c

299+ my_show d (RUType u) = "RUType"

297

300

298

301

299implementation Show Err where

302implementation Show Err where

libs/prelude/Builtins.idr+9−4

@@ -172,17 +172,22 @@ assert_smaller x y = y

172assert_total : a -> a

173assert_total x = x

174

175+||| Assert to the totality checker that the case using this expression

176+||| is unreachable

177+assert_unreachable : a

178+-- compiled as primitive

179+

175||| Subvert the type checker. This function is abstract, so it will not reduce in

180||| Subvert the type checker. This function is abstract, so it will not reduce in

176||| the type checker. Use it with care - it can result in segfaults or worse!

181||| the type checker. Use it with care - it can result in segfaults or worse!

177−export %assert_total -- need to pretend

182+export

178believe_me : a -> b

183believe_me : a -> b

179−believe_me x = prim__believe_me _ _ x

184+believe_me x = assert_total (prim__believe_me _ _ x)

180

185

181||| Subvert the type checker. This function *will* reduce in the type checker.

186||| Subvert the type checker. This function *will* reduce in the type checker.

182||| Use it with extreme care - it can result in segfaults or worse!

187||| Use it with extreme care - it can result in segfaults or worse!

183−public export %assert_total

188+public export

184really_believe_me : a -> b

189really_believe_me : a -> b

185−really_believe_me x = prim__believe_me _ _ x

190+really_believe_me x = assert_total (prim__believe_me _ _ x)

186

191

187||| Deprecated alias for `Double`, for the purpose of backwards

192||| Deprecated alias for `Double`, for the purpose of backwards

188||| compatibility. Idris does not support 32 bit floats at present.

193||| compatibility. Idris does not support 32 bit floats at present.

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

@@ -411,11 +411,10 @@ intercalate sep xss = concat $ intersperse sep xss

411||| transpose (transpose [[], [1, 2]]) = [[1, 2]]

412|||

413||| TODO: Solution which satisfies the totality checker?

414−%assert_total

415transpose : List (List a) -> List (List a)

414transpose : List (List a) -> List (List a)

416transpose [] = []

415transpose [] = []

417transpose ([] :: xss) = transpose xss

416transpose ([] :: xss) = transpose xss

418−transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))

417+transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))

419

418

420--------------------------------------------------------------------------------

419--------------------------------------------------------------------------------

421-- Membership tests

420-- Membership tests

src/IRTS/Compiler.hs+78−74

@@ -154,7 +154,7 @@ generate codegen mainmod ir

154

155irMain :: TT Name -> Idris LDecl

156irMain tm = do

157− i <- irTerm M.empty [] tm

157+ i <- irTerm (sMN 0 "runMain") M.empty [] tm

158 return $ LFun [] (sMN 0 "runMain") [] (LForce i)

159

160mkDecls :: [Name] -> Idris [(Name, LDecl)]

@@ -218,10 +218,10 @@ declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x

218declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

219

220mkLDecl n (Function tm _)

221− = declArgs [] True n <$> irTerm M.empty [] tm

221+ = declArgs [] True n <$> irTerm n M.empty [] tm

222

223mkLDecl n (CaseOp ci _ _ _ pats cd)

224− = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc

224+ = declArgs [] (case_inlinable ci || caseName n) n <$> irTree n args sc

225 where

226 (args, sc) = cases_runtime cd

227

@@ -244,8 +244,8 @@ data VarInfo = VI

244

245type Vars = M.Map Name VarInfo

246

247−irTerm :: Vars -> [Name] -> Term -> Idris LExp

247+irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp

248−irTerm vs env tm@(App _ f a) = do

248+irTerm top vs env tm@(App _ f a) = do

249 ist <- getIState

250 case unApply tm of

251 (P _ n _, args)

@@ -257,12 +257,16 @@ irTerm vs env tm@(App _ f a) = do

257

258 (P _ (UN u) _, [_, arg])

259 | u == txt "unsafePerformPrimIO"

260− -> irTerm vs env arg

260+ -> irTerm top vs env arg

261+

262+ (P _ (UN u) _, _)

263+ | u == txt "assert_unreachable"

264+ -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top

261

265

262 -- TMP HACK - until we get inlining.

266 -- TMP HACK - until we get inlining.

263 (P _ (UN r) _, [_, _, _, _, _, arg])

267 (P _ (UN r) _, [_, _, _, _, _, arg])

264 | r == txt "replace"

268 | r == txt "replace"

265− -> irTerm vs env arg

269+ -> irTerm top vs env arg

266

270

267 -- 'void' doesn't have any pattern clauses and only gets called on

271 -- 'void' doesn't have any pattern clauses and only gets called on

268 -- erased things in higher order contexts (also a TMP HACK...)

272 -- erased things in higher order contexts (also a TMP HACK...)

@@ -277,42 +281,42 @@ irTerm vs env tm@(App _ f a) = do

277

281

278 (P _ (UN l) _, [_, arg])

282 (P _ (UN l) _, [_, arg])

279 | l == txt "force"

283 | l == txt "force"

280− -> LForce <$> irTerm vs env arg

284+ -> LForce <$> irTerm top vs env arg

281

285

282 -- Laziness, the new way

286 -- Laziness, the new way

283 (P _ (UN l) _, [_, _, arg])

287 (P _ (UN l) _, [_, _, arg])

284 | l == txt "Delay"

288 | l == txt "Delay"

285− -> LLazyExp <$> irTerm vs env arg

289+ -> LLazyExp <$> irTerm top vs env arg

286

290

287 (P _ (UN l) _, [_, _, arg])

291 (P _ (UN l) _, [_, _, arg])

288 | l == txt "Force"

292 | l == txt "Force"

289− -> LForce <$> irTerm vs env arg

293+ -> LForce <$> irTerm top vs env arg

290

294

291 (P _ (UN a) _, [_, _, _, arg])

295 (P _ (UN a) _, [_, _, _, arg])

292 | a == txt "assert_smaller"

296 | a == txt "assert_smaller"

293− -> irTerm vs env arg

297+ -> irTerm top vs env arg

294

298

295 (P _ (UN a) _, [_, arg])

299 (P _ (UN a) _, [_, arg])

296 | a == txt "assert_total"

300 | a == txt "assert_total"

297− -> irTerm vs env arg

301+ -> irTerm top vs env arg

298

302

299 (P _ (UN p) _, [_, arg])

303 (P _ (UN p) _, [_, arg])

300 | p == txt "par"

304 | p == txt "par"

301− -> do arg' <- irTerm vs env arg

305+ -> do arg' <- irTerm top vs env arg

302 return $ LOp LPar [LLazyExp arg']

306 return $ LOp LPar [LLazyExp arg']

303

307

304 (P _ (UN pf) _, [arg])

308 (P _ (UN pf) _, [arg])

305 | pf == txt "prim_fork"

309 | pf == txt "prim_fork"

306− -> do arg' <- irTerm vs env arg

310+ -> do arg' <- irTerm top vs env arg

307 return $ LOp LFork [LLazyExp arg']

311 return $ LOp LFork [LLazyExp arg']

308

312

309 (P _ (UN m) _, [_,size,t])

313 (P _ (UN m) _, [_,size,t])

310 | m == txt "malloc"

314 | m == txt "malloc"

311− -> irTerm vs env t

315+ -> irTerm top vs env t

312

316

313 (P _ (UN tm) _, [_,t])

317 (P _ (UN tm) _, [_,t])

314 | tm == txt "trace_malloc"

318 | tm == txt "trace_malloc"

315− -> irTerm vs env t -- TODO

319+ -> irTerm top vs env t -- TODO

316

320

317 -- This case is here until we get more general inlining. It's just

321 -- This case is here until we get more general inlining. It's just

318 -- a really common case, and the laziness hurts...

322 -- a really common case, and the laziness hurts...

@@ -324,9 +328,9 @@ irTerm vs env tm@(App _ f a) = do

324 , b == txt "Bool"

328 , b == txt "Bool"

325 , p == txt "Prelude"

329 , p == txt "Prelude"

326 -> do

330 -> do

327− x' <- irTerm vs env x

331+ x' <- irTerm top vs env x

328− t' <- irTerm vs env t

332+ t' <- irTerm top vs env t

329− e' <- irTerm vs env e

333+ e' <- irTerm top vs env e

330 return (LCase Shared x'

334 return (LCase Shared x'

331 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

335 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

332 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

336 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

@@ -375,7 +379,7 @@ irTerm vs env tm@(App _ f a) = do

375

379

376 -- exactly saturated

380 -- exactly saturated

377 EQ | isNewtype

381 EQ | isNewtype

378− -> irTerm vs env (head argsPruned)

382+ -> irTerm top vs env (head argsPruned)

379

383

380 | otherwise -- not newtype, plain data ctor

384 | otherwise -- not newtype, plain data ctor

381 -> buildApp (LV $ Glob n) argsPruned

385 -> buildApp (LV $ Glob n) argsPruned

@@ -384,7 +388,7 @@ irTerm vs env tm@(App _ f a) = do

384 LT | isNewtype -- newtype

388 LT | isNewtype -- newtype

385 , length argsPruned == 1 -- and we already have the value

389 , length argsPruned == 1 -- and we already have the value

386 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args

390 -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args

387− <$> irTerm vs env (head argsPruned)

391+ <$> irTerm top vs env (head argsPruned)

388

392

389 | isNewtype -- newtype but the value is not among args yet

393 | isNewtype -- newtype but the value is not among args yet

390 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]

394 -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]

@@ -398,7 +402,7 @@ irTerm vs env tm@(App _ f a) = do

398

402

399 -- an external name applied to arguments

403 -- an external name applied to arguments

400 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do

404 (P _ n _, args) | S.member (n, length args) (idris_externs ist) -> do

401− LOp (LExternal n) <$> mapM (irTerm vs env) args

405+ LOp (LExternal n) <$> mapM (irTerm top vs env) args

402

406

403 -- a name applied to arguments

407 -- a name applied to arguments

404 (P _ n _, args) -> do

408 (P _ n _, args) -> do

@@ -406,23 +410,23 @@ irTerm vs env tm@(App _ f a) = do

406 -- if it's a primitive that is already saturated,

410 -- if it's a primitive that is already saturated,

407 -- compile to the corresponding op here already to save work

411 -- compile to the corresponding op here already to save work

408 Just (arity, op) | length args == arity

412 Just (arity, op) | length args == arity

409− -> LOp op <$> mapM (irTerm vs env) args

413+ -> LOp op <$> mapM (irTerm top vs env) args

410

414

411 -- otherwise, just apply the name

415 -- otherwise, just apply the name

412 _ -> applyName n ist args

416 _ -> applyName n ist args

413

417

414 -- turn de bruijn vars into regular named references and try again

418 -- turn de bruijn vars into regular named references and try again

415− (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args

419+ (V i, args) -> irTerm top vs env $ mkApp (P Bound (env !! i) Erased) args

416

420

417 (f, args)

421 (f, args)

418 -> LApp False

422 -> LApp False

419− <$> irTerm vs env f

423+ <$> irTerm top vs env f

420− <*> mapM (irTerm vs env) args

424+ <*> mapM (irTerm top vs env) args

421

425

422 where

426 where

423 buildApp :: LExp -> [Term] -> Idris LExp

427 buildApp :: LExp -> [Term] -> Idris LExp

424 buildApp e [] = return e

428 buildApp e [] = return e

425− buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs

429+ buildApp e xs = LApp False e <$> mapM (irTerm top vs env) xs

426

430

427 applyToNames :: LExp -> [Name] -> LExp

431 applyToNames :: LExp -> [Name] -> LExp

428 applyToNames tm [] = tm

432 applyToNames tm [] = tm

@@ -437,7 +441,7 @@ irTerm vs env tm@(App _ f a) = do

437

441

438 applyName :: Name -> IState -> [Term] -> Idris LExp

442 applyName :: Name -> IState -> [Term] -> Idris LExp

439 applyName n ist args =

443 applyName n ist args =

440− LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)

444+ LApp False (LV $ Glob n) <$> mapM (irTerm top vs env . erase) (zip [0..] args)

441 where

445 where

442 erase (i, x)

446 erase (i, x)

443 | i >= arity || i `elem` used = x

447 | i >= arity || i `elem` used = x

@@ -459,31 +463,31 @@ irTerm vs env tm@(App _ f a) = do

459 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

463 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

460 fst4 (x,_,_,_,_) = x

464 fst4 (x,_,_,_,_) = x

461

465

462−irTerm vs env (P _ n _) = return $ LV (Glob n)

466+irTerm top vs env (P _ n _) = return $ LV (Glob n)

463−irTerm vs env (V i)

467+irTerm top vs env (V i)

464 | i >= 0 && i < length env = return $ LV (Glob (env!!i))

468 | i >= 0 && i < length env = return $ LV (Glob (env!!i))

465 | otherwise = ifail $ "bad de bruijn index: " ++ show i

469 | otherwise = ifail $ "bad de bruijn index: " ++ show i

466

470

467−irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc

471+irTerm top vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc

468 where

472 where

469 n' = uniqueName n env

473 n' = uniqueName n env

470

474

471−irTerm vs env (Bind n (Let _ v) sc)

475+irTerm top vs env (Bind n (Let _ v) sc)

472− = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc

476+ = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc

473

477

474−irTerm vs env (Bind _ _ _) = return $ LNothing

478+irTerm top vs env (Bind _ _ _) = return $ LNothing

475

479

476−irTerm vs env (Proj t (-1)) = do

480+irTerm top vs env (Proj t (-1)) = do

477− t' <- irTerm vs env t

481+ t' <- irTerm top vs env t

478 return $ LOp (LMinus (ATInt ITBig))

482 return $ LOp (LMinus (ATInt ITBig))

479 [t', LConst (BI 1)]

483 [t', LConst (BI 1)]

480

484

481−irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i

485+irTerm top vs env (Proj t i) = LProj <$> irTerm top vs env t <*> pure i

482−irTerm vs env (Constant TheWorld) = return $ LNothing

486+irTerm top vs env (Constant TheWorld) = return $ LNothing

483−irTerm vs env (Constant c) = return $ LConst c

487+irTerm top vs env (Constant c) = return $ LConst c

484−irTerm vs env (TType _) = return $ LNothing

488+irTerm top vs env (TType _) = return $ LNothing

485−irTerm vs env Erased = return $ LNothing

489+irTerm top vs env Erased = return $ LNothing

486−irTerm vs env Impossible = return $ LNothing

490+irTerm top vs env Impossible = return $ LNothing

487

491

488doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

492doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

489doForeign vs env (ret : fname : world : args)

493doForeign vs env (ret : fname : world : args)

@@ -494,7 +498,7 @@ doForeign vs env (ret : fname : world : args)

494 where

498 where

495 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits

499 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits

496 = do let l' = toFDesc l

500 = do let l' = toFDesc l

497− r' <- irTerm vs env r

501+ r' <- irTerm (sMN 0 "__foreignCall") vs env r

498 return (l', r')

502 return (l', r')

499 splitArg _ = ifail $ "Badly formed foreign function call"

503 splitArg _ = ifail $ "Badly formed foreign function call"

500

504

@@ -508,24 +512,24 @@ doForeign vs env (ret : fname : world : args)

508 deNS n = n

512 deNS n = n

509doForeign vs env xs = ifail "Badly formed foreign function call"

513doForeign vs env xs = ifail "Badly formed foreign function call"

510

514

511−irTree :: [Name] -> SC -> Idris LExp

515+irTree :: Name -> [Name] -> SC -> Idris LExp

512−irTree args tree = do

516+irTree top args tree = do

513 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

517 logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

514− LLam args <$> irSC M.empty tree

518+ LLam args <$> irSC top M.empty tree

515

519

516−irSC :: Vars -> SC -> Idris LExp

520+irSC :: Name -> Vars -> SC -> Idris LExp

517−irSC vs (STerm t) = irTerm vs [] t

521+irSC top vs (STerm t) = irTerm top vs [] t

518−irSC vs (UnmatchedCase str) = return $ LError str

522+irSC top vs (UnmatchedCase str) = return $ LError str

519

523

520−irSC vs (ProjCase tm alts) = do

524+irSC top vs (ProjCase tm alts) = do

521− tm' <- irTerm vs [] tm

525+ tm' <- irTerm top vs [] tm

522− alts' <- mapM (irAlt vs tm') alts

526+ alts' <- mapM (irAlt top vs tm') alts

523 return $ LCase Shared tm' alts'

527 return $ LCase Shared tm' alts'

524

528

525-- Transform matching on Delay to applications of Force.

529-- Transform matching on Delay to applications of Force.

526−irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

530+irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

527 | delay == txt "Delay"

531 | delay == txt "Delay"

528− = do sc' <- irSC vs $ mkForce n' n sc

532+ = do sc' <- irSC top vs $ mkForce n' n sc

529 return $ LLet n' (LForce (LV (Glob n))) sc'

533 return $ LLet n' (LForce (LV (Glob n))) sc'

530

534

531-- There are two transformations in this case:

535-- There are two transformations in this case:

@@ -550,7 +554,7 @@ irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

550-- Hence, we check whether the variables are used at all

554-- Hence, we check whether the variables are used at all

551-- and erase the casesplit if they are not.

555-- and erase the casesplit if they are not.

552--

556--

553−irSC vs (Case up n [alt]) = do

557+irSC top vs (Case up n [alt]) = do

554 replacement <- case alt of

558 replacement <- case alt of

555 ConCase cn a ns sc -> do

559 ConCase cn a ns sc -> do

556 detag <- fgetState (opt_detaggable . ist_optimisation cn)

560 detag <- fgetState (opt_detaggable . ist_optimisation cn)

@@ -561,9 +565,9 @@ irSC vs (Case up n [alt]) = do

561 _ -> return Nothing

565 _ -> return Nothing

562

566

563 case replacement of

567 case replacement of

564− Just sc -> irSC vs sc

568+ Just sc -> irSC top vs sc

565 _ -> do

569 _ -> do

566− alt' <- irAlt vs (LV (Glob n)) alt

570+ alt' <- irAlt top vs (LV (Glob n)) alt

567 return $ case namesBoundIn alt' `usedIn` subexpr alt' of

571 return $ case namesBoundIn alt' `usedIn` subexpr alt' of

568 [] -> subexpr alt' -- strip the unused top-most case

572 [] -> subexpr alt' -- strip the unused top-most case

569 _ -> LCase up (LV (Glob n)) [alt']

573 _ -> LCase up (LV (Glob n)) [alt']

@@ -594,13 +598,13 @@ irSC vs (Case up n [alt]) = do

594-- This work-around is not entirely optimal; the best approach would be

598-- This work-around is not entirely optimal; the best approach would be

595-- to ensure that such case trees don't arise in the first place.

599-- to ensure that such case trees don't arise in the first place.

596--

600--

597−irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

601+irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

598 detag <- fgetState (opt_detaggable . ist_optimisation cn)

602 detag <- fgetState (opt_detaggable . ist_optimisation cn)

599 if detag

603 if detag

600− then irSC vs (Case up n [ConCase cn a ns sc])

604+ then irSC top vs (Case up n [ConCase cn a ns sc])

601− else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

605+ else LCase up (LV (Glob n)) <$> mapM (irAlt top vs (LV (Glob n))) alts

602

606

603−irSC vs sc@(Case up n alts) = do

607+irSC top vs sc@(Case up n alts) = do

604 -- check that neither alternative needs the newtype optimisation,

608 -- check that neither alternative needs the newtype optimisation,

605 -- see comment above

609 -- see comment above

606 goneWrong <- or <$> mapM isDetaggable alts

610 goneWrong <- or <$> mapM isDetaggable alts

@@ -608,20 +612,20 @@ irSC vs sc@(Case up n alts) = do

608 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

612 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

609

613

610 -- everything okay

614 -- everything okay

611− LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

615+ LCase up (LV (Glob n)) <$> mapM (irAlt top vs (LV (Glob n))) alts

612 where

616 where

613 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn

617 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn

614 isDetaggable _ = return False

618 isDetaggable _ = return False

615

619

616−irSC vs ImpossibleCase = return LNothing

620+irSC top vs ImpossibleCase = return LNothing

617

621

618−irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt

622+irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt

619

623

620-- this leaves out all unused arguments of the constructor

624-- this leaves out all unused arguments of the constructor

621−irAlt vs _ (ConCase n t args sc) = do

625+irAlt top vs _ (ConCase n t args sc) = do

622 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

626 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

623 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

627 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

624− LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc

628+ LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc

625 where

629 where

626 methodVars = case n of

630 methodVars = case n of

627 SN (InstanceCtorN className)

631 SN (InstanceCtorN className)

@@ -631,9 +635,9 @@ irAlt vs _ (ConCase n t args sc) = do

631 _

635 _

632 -> M.empty -- not an instance constructor

636 -> M.empty -- not an instance constructor

633

637

634−irAlt vs _ (ConstCase x rhs)

638+irAlt top vs _ (ConstCase x rhs)

635− | matchable x = LConstCase x <$> irSC vs rhs

639+ | matchable x = LConstCase x <$> irSC top vs rhs

636− | matchableTy x = LDefaultCase <$> irSC vs rhs

640+ | matchableTy x = LDefaultCase <$> irSC top vs rhs

637 where

641 where

638 matchable (I _) = True

642 matchable (I _) = True

639 matchable (BI _) = True

643 matchable (BI _) = True

@@ -657,14 +661,14 @@ irAlt vs _ (ConstCase x rhs)

657

661

658 matchableTy _ = False

662 matchableTy _ = False

659

663

660−irAlt vs tm (SucCase n rhs) = do

664+irAlt top vs tm (SucCase n rhs) = do

661− rhs' <- irSC vs rhs

665+ rhs' <- irSC top vs rhs

662 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

666 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

663 [tm,

667 [tm,

664 LConst (BI 1)]) rhs')

668 LConst (BI 1)]) rhs')

665

669

666−irAlt vs _ (ConstCase c rhs)

670+irAlt top vs _ (ConstCase c rhs)

667 = ifail $ "Can't match on (" ++ show c ++ ")"

671 = ifail $ "Can't match on (" ++ show c ++ ")"

668

672

669−irAlt vs _ (DefaultCase rhs)

673+irAlt top vs _ (DefaultCase rhs)

670− = LDefaultCase <$> irSC vs rhs

674+ = LDefaultCase <$> irSC top vs rhs

src/Idris/AbsSyntaxTree.hs+1

@@ -334,6 +334,7 @@ primDefs = [ sUN "unsafePerformPrimIO"

334 , sUN "mkLazyForeignPrim"

335 , sUN "mkForeignPrim"

336 , sUN "void"

337+ , sUN "assert_unreachable"

337 ]

338 ]

338

339

339-- information that needs writing for the current module's .ibc file

340-- information that needs writing for the current module's .ibc file

src/Idris/Core/CaseTree.hs+10−4

@@ -23,7 +23,7 @@ in order to allow for better optimisation opportunities.

23module Idris.Core.CaseTree (

24 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo

25 , Phase(..), CaseTree, CaseType(..)

26− , simpleCase, small, namesUsed, findCalls, findUsedArgs

26+ , simpleCase, small, namesUsed, findCalls, findCalls', findUsedArgs

27 , substSC, substAlt, mkForce

28 ) where

@@ -150,7 +150,10 @@ namesUsed sc = nub $ nu' [] sc where

150-- in each argument position for the call, in order to help reduce

151-- compilation time, and trace all unused arguments

152findCalls :: SC -> [Name] -> [(Name, [[Name]])]

153+findCalls = findCalls' False

154+

155+findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]

153−findCalls sc topargs = nub $ nu' topargs sc where

156+findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where

154 nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

157 nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

155 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

158 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

156 nu' ps (STerm t) = nub $ nut ps t

159 nu' ps (STerm t) = nub $ nut ps t

@@ -166,8 +169,11 @@ findCalls sc topargs = nub $ nu' topargs sc where

166 | otherwise = [(n, [])] -- tmp

169 | otherwise = [(n, [])] -- tmp

167 nut ps fn@(App _ f a)

170 nut ps fn@(App _ f a)

168 | (P _ n _, args) <- unApply fn

171 | (P _ n _, args) <- unApply fn

172+ = if ignoreasserts && n == sUN "assert_total"

173+ then []

174+ else if n `elem` ps

169− = if n `elem` ps then nut ps f ++ nut ps a

175+ then nut ps f ++ nut ps a

170− else [(n, map argNames args)] ++ concatMap (nut ps) args

176+ else [(n, map argNames args)] ++ concatMap (nut ps) args

171 | (P (TCon _ _) n _, _) <- unApply fn = []

177 | (P (TCon _ _) n _, _) <- unApply fn = []

172 | otherwise = nut ps f ++ nut ps a

178 | otherwise = nut ps f ++ nut ps a

173 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

179 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

src/Idris/Parser.hs+3−1

@@ -702,7 +702,9 @@ fnOpt = do reservedHL "total"; return TotalFn

702 <|> do try (lchar '%' *> reserved "inline");

703 return Inlinable

704 <|> do try (lchar '%' *> reserved "assert_total");

705+ fc <- getFC

706+ parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")

705− return AssertTotal

707+ return AssertTotal

706 <|> do try (lchar '%' *> reserved "error_handler");

708 <|> do try (lchar '%' *> reserved "error_handler");

707 return ErrorHandler

709 return ErrorHandler

708 <|> do try (lchar '%' *> reserved "error_reverse");

710 <|> do try (lchar '%' *> reserved "error_reverse");

test/primitives006/Data/Bytes.idr+3−4

@@ -61,11 +61,11 @@ grow factor (B arr ofs end) = do

61 BA.copy (arr, ofs) (arr', ofs') bytesUsed

62 return $ B arr' ofs' (ofs' + bytesUsed)

64−%assert_total

65export

64export

66snoc : Bytes -> Byte -> Bytes

65snoc : Bytes -> Byte -> Bytes

67snoc bs@(B arr ofs end) byte

66snoc bs@(B arr ofs end) byte

67+ = assert_total $

68− = if end >= BA.size arr

68+ if end >= BA.size arr

69 then unsafePerformIO $ do -- need more space

70 grown <- grow 2 bs

71 return $ snoc grown byte

@@ -114,11 +114,10 @@ namespace ConsView

114 return $ ConsView.Cons first (B arr (ofs+1) end)

115

116infixr 7 ++

117−%assert_total

118export

117export

119(++) : Bytes -> Bytes -> Bytes

118(++) : Bytes -> Bytes -> Bytes

120(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)

119(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)

121− = let countR = endR - ofsR in

120+ = assert_total $ let countR = endR - ofsR in

122 if endL + countR > BA.size arrL

121 if endL + countR > BA.size arrL

123 then unsafePerformIO $ do -- need more space

122 then unsafePerformIO $ do -- need more space

124 grown <- grow 2 bsL

123 grown <- grow 2 bsL

test/reg035/reg035a.lidr+1−2

@@ -15,13 +15,12 @@

15> hasNoDuplicates : (Eq alpha) => List alpha -> Bool

16> hasNoDuplicates as = as == nub as

18−> %assert_total

19> setEq : (Eq alpha) => List alpha -> List alpha -> Bool

18> setEq : (Eq alpha) => List alpha -> List alpha -> Bool

20> setEq Nil Nil = True

19> setEq Nil Nil = True

21> setEq Nil (y :: ys) = False

20> setEq Nil (y :: ys) = False

22> setEq (x :: xs) Nil = False

21> setEq (x :: xs) Nil = False

23> setEq {alpha} (x :: xs) (y :: ys) =

22> setEq {alpha} (x :: xs) (y :: ys) =

24−> (x == y && setEq xs ys)

23+> assert_total $ (x == y && setEq xs ys)

25> ||

24> ||

26> (elem x ys && elem y xs &&

25> (elem x ys && elem y xs &&

27> setEq (filter (/= y) xs) (filter (/= x) ys)

26> setEq (filter (/= y) xs) (filter (/= x) ys)

test/reg041/ott.idr+2−3

@@ -23,18 +23,17 @@ s ~> t = Pi s $ const t

23syntax "<|" [s] "|>" = El s

24syntax [x] "==" [y] "in" [s] = EQ s x s y

26−%assert_total

27EQ : (s : U) -> <| s |> -> (t : U) -> <| t |> -> U

26EQ : (s : U) -> <| s |> -> (t : U) -> <| t |> -> U

28EQ MkU MkU MkU MkU = One

27EQ MkU MkU MkU MkU = One

29EQ MkU Zero MkU Zero = One

28EQ MkU Zero MkU Zero = One

30EQ MkU One MkU One = One

29EQ MkU One MkU One = One

31EQ MkU Two MkU Two = One

30EQ MkU Two MkU Two = One

32−EQ MkU (Pi s t) MkU (Pi s' t') = Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ MkU (t x) MkU (t' y)

31+EQ MkU (Pi s t) MkU (Pi s' t') = assert_total $ Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ MkU (t x) MkU (t' y)

33EQ Zero x Zero y = One

32EQ Zero x Zero y = One

34EQ One x One y = One

33EQ One x One y = One

35EQ Two True Two True = One

34EQ Two True Two True = One

36EQ Two False Two False = One

35EQ Two False Two False = One

37−EQ (Pi s t) f (Pi s' t') g = Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

36+EQ (Pi s t) f (Pi s' t') g = assert_total $ Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

38EQ _ _ _ _ = Zero

37EQ _ _ _ _ = Zero

40example : <| (Basics.id == Basics.id in (OTT.Two ~> OTT.Two)) |>

39example : <| (Basics.id == Basics.id in (OTT.Two ~> OTT.Two)) |>

test/totality015/expectednew file+6

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

1+totality015a.idr:52:3:

2+Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

3+totality015a.idr:42:3:

4+Main.correct is possibly not total due to: Main.quiz

5+totality015a.idr:47:3:

6+Main.wrong is possibly not total due to: Main.quiz

test/totality015/runnew file+4

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality015.idr --check

3+${IDRIS:-idris} $@ totality015a.idr --check

4+rm -f *.ibc

test/totality015/totality015.idrnew file+70

@@ -0,0 +1,70 @@

1+import Data.Primitives.Views

2+import System

4+%default total

6+data Command : Type -> Type where

7+ PutStr : String -> Command ()

8+ GetLine : Command String

10+data ConsoleIO : Type -> Type where

11+ Quit : a -> ConsoleIO a

12+ Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

13+

14+(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

15+(>>=) = Do

16+

17+data Fuel = Dry | More (Lazy Fuel)

18+

19+runCommand : Command a -> IO a

20+runCommand (PutStr x) = putStr x

21+runCommand GetLine = getLine

22+

23+run : Fuel -> ConsoleIO a -> IO (Maybe a)

24+run fuel (Quit val) = do pure (Just val)

25+run (More fuel) (Do c f) = do res <- runCommand c

26+ run fuel (f res)

27+run Dry p = pure Nothing

28+

29+randoms : Int -> Stream Int

30+randoms seed = let seed' = 1664525 * seed + 1013904223 in

31+ (seed' `shiftR` 2) :: randoms seed'

32+

33+arithInputs : Int -> Stream Int

34+arithInputs seed = map bound (randoms seed)

35+ where

36+ bound : Int -> Int

37+ bound x with (divides x 12)

38+ bound ((12 * div) + rem) | (DivBy prf) = abs rem + 1

39+

40+mutual

41+ correct : Stream Int -> (score : Nat) -> ConsoleIO Nat

42+ correct nums score

43+ = do PutStr "Correct!\n"

44+ quiz nums (score + 1)

45+

46+ wrong : Stream Int -> Int -> (score : Nat) -> ConsoleIO Nat

47+ wrong nums ans score

48+ = do PutStr ("Wrong, the answer is " ++ show ans ++ "\n")

49+ quiz nums score

50+

51+ quiz : Stream Int -> (score : Nat) -> ConsoleIO Nat

52+ quiz (num1 :: num2 :: nums) score

53+ = do PutStr ("Score so far: " ++ show score ++ "\n")

54+ PutStr (show num1 ++ " * " ++ show num2 ++ "? ")

55+ answer <- GetLine

56+ if toLower answer == "quit" then Quit score else

57+ if (cast answer == num1 * num2)

58+ then correct nums score

59+ else wrong nums (num1 * num2) score

60+

61+partial

62+forever : Fuel

63+forever = More forever

64+

65+partial

66+main : IO ()

67+main = do seed <- time

68+ Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0)

69+ | Nothing => putStrLn "Ran out of fuel"

70+ putStrLn ("Final score: " ++ show score)

test/totality015/totality015a.idrnew file+63

@@ -0,0 +1,63 @@