78b81b2 · Idris-dev · git.iko.soy

CHANGELOG.md+8

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

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

7474 that it can spot more total functions.

7575

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+

7684## Library updates

7785

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

idris.cabal+3

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

783783 test/totality014/run

784784 test/totality014/*.idr

785785 test/totality014/expected

786+ test/totality015/run

787+ test/totality015/*.idr

788+ test/totality015/expected

786789

787790 test/tutorial001/run

788791 test/tutorial001/*.idr

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

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

22

33import Data.Fin

44

5−%default total

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

6+ -- to improve it! (EB)

67%access export

78

89public export

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

2829bitsUsed : Nat -> Nat

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

3031

31−%assert_total

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

3333natToBits' a Z = a

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

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

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

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

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

40+ natToBits' a _ | _ = assert_unreachable

4041

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

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

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

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

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

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

48+ | _ = assert_unreachable

4749

4850getPad : %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)

5052

5153public export

5254data Bits : Nat -> Type where

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

101103 | S Z = pad16' n prim__shlB16 x c

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

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

106+ | _ = assert_unreachable

104107

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

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

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

111114 | S Z = prim__lshrB16 x c

112115 | S (S Z) = prim__lshrB32 x c

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

117+ | _ = assert_unreachable

114118

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

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

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

122126 | S Z = pad16' n prim__ashrB16 x c

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

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

129+ | _ = assert_unreachable

125130

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

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

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

132137 | S Z = prim__andB16 x y

133138 | S (S Z) = prim__andB32 x y

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

140+ | _ = assert_unreachable

135141

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

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

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

142148 | S Z = prim__orB16 x y

143149 | S (S Z) = prim__orB32 x y

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

151+ | _ = assert_unreachable

145152

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

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

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

152159 | S Z = prim__xorB16 x y

153160 | S (S Z) = prim__xorB32 x y

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

162+ | _ = assert_unreachable

155163

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

157165xor {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)

162170 | S Z = pad16 n prim__addB16 x y

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

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

173+ | _ = assert_unreachable

165174

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

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

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

172181 | S Z = pad16 n prim__subB16 x y

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

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

184+ | _ = assert_unreachable

175185

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

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

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

182192 | S Z = pad16 n prim__mulB16 x y

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

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

195+ | _ = assert_unreachable

185196

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

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

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

193204 | S Z = prim__sdivB16 x y

194205 | S (S Z) = prim__sdivB32 x y

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

207+ | _ = assert_unreachable

196208

197209partial

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

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

205217 | S Z = prim__udivB16 x y

206218 | S (S Z) = prim__udivB32 x y

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

220+ | _ = assert_unreachable

208221

209222partial

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

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

217230 | S Z = prim__sremB16 x y

218231 | S (S Z) = prim__sremB32 x y

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

233+ | _ = assert_unreachable

220234

221235partial

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

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

229243 | S Z = prim__uremB16 x y

230244 | S (S Z) = prim__uremB32 x y

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

246+ | _ = assert_unreachable

232247

233248partial

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

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

241256 | S Z = prim__ltB16 x y

242257 | S (S Z) = prim__ltB32 x y

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

259+ | _ = assert_unreachable

244260

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

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

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

248264 | S Z = prim__lteB16 x y

249265 | S (S Z) = prim__lteB32 x y

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

267+ | _ = assert_unreachable

251268

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

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

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

255272 | S Z = prim__eqB16 x y

256273 | S (S Z) = prim__eqB32 x y

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

275+ | _ = assert_unreachable

258276

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

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

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

262280 | S Z = prim__gteB16 x y

263281 | S (S Z) = prim__gteB32 x y

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

283+ | _ = assert_unreachable

265284

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

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

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

269288 | S Z = prim__gtB16 x y

270289 | S (S Z) = prim__gtB32 x y

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

291+ | _ = assert_unreachable

272292

273293implementation Eq (Bits n) where

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

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

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

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

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

318+ | _ = assert_unreachable

298319

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

300321complement (MkBits x) = MkBits (complement' x)

301322

302323-- TODO: Prove

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

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

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

306326 | (Z, Z) = believe_me x

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

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

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

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

336+ | _ = assert_unreachable

316337

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

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

319340

320−%assert_total

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

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

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

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

328348 prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad

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

330350 prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad

351+ | _ = assert_unreachable

331352

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

333354intToBits n = MkBits (intToBits' n)

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

341362 | S Z = prim__zextB16_BigInt x

342363 | S (S Z) = prim__zextB32_BigInt x

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

365+ | _ = assert_unreachable

344366

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

346368bitsToInt (MkBits x) = bitsToInt' x

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

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

354376

355377-- TODO: Prove

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

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

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

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

382403 (prim__zextB32_B64 pad))

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

384405 believe_me (prim__ashrB64 (prim__shlB64 (believe_me x) pad) pad)

406+ | _ = assert_unreachable

385407

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

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

388410

389411-- TODO: Prove

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

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

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

393414 | (Z, Z) = believe_me x

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

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

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

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

424+ | _ = assert_unreachable

403425

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

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

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

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

420442bitsToStr x = pack (helper last x)

421443 where

422− %assert_total

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

424445 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

426447

427448implementation Show (Bits n) where

428449 show = bitsToStr

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

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

2424rem : Mod2 n -> Mod2 n -> Mod2 n

2525rem = modBin urem

2626

27−%assert_total

2827public export

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

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

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

5352modToStr : Mod2 n -> String

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

5554 where

56− %assert_total

5755 helper : Mod2 n -> List Char

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

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

56+ helper x = assert_total $

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

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

6059

6160

6261implementation Show (Mod2 n) where

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

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

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

1919 divides val 0 = DivByZero

2020 divides val d

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

22− else val `div` d

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

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

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

21+ = assert_total $

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

23+ else val `div` d

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

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

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

2627

2728 ||| View for recursion over Integers

2829 data IntegerRec : Integer -> Type where

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

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

5556 divides val 0 = DivByZero

5657 divides val d

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

58− else val `div` d

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

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

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

58+ = assert_total $

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

60+ else val `div` d

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

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

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

6264

6365 ||| View for recursion over Ints

6466 data IntRec : Int -> Type where

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

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

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

7171 mkDouble Nothing = Nothing

7272

73− %assert_total

7473 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)

7675 where

7776 num base 0 = 1

7877 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

235235

236236implementation Show TT where

237237 showPrec = my_show

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

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

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

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

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

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

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

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) = assert_total $ showCon d "V" $ showArg i

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) = assert_total $ showCon d "App" $ showArg t1 ++ showArg t2

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

244244 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

246253

247254implementation Eq TT where

248255 a == b = equalp a b

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

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

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

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

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

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

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

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

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

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

254261 equalp (TConst c) (TConst c') = c == c'

255262 equalp Erased Erased = True

256263 equalp (TType u) (TType u') = u == u'

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

257265 equalp x y = False

258266

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−

265267total

266268forget : TT -> Maybe Raw

267269forget tm = fe [] tm

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

288290

289291implementation Show Raw where

290292 showPrec = my_show

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

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

293− my_show d (RBind n b tm) = 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'

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

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

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

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

295297 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"

297300

298301

299302implementation Show Err where

libs/contrib/Data/Heap.idr+3−4

@@ -61,11 +61,10 @@ orderBySize left centre right =

6161 largest : Nat

6262 largest = maximum (size left) $ maximum (size centre) (size right)

6363

64−%assert_total -- relies on orderBySize doing the right thing

6564merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a

6665merge Empty right = right

6766merge left Empty = left

68−merge (Node ls ll le lr) (Node rs rl re rr) =

67+merge (Node ls ll le lr) (Node rs rl re rr) = assert_total $ -- relies on orderBySize doing the right thing

6968 if le < re then

7069 let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in

7170 Node mergedSize largest le (merge b c)

@@ -99,9 +98,9 @@ toList : Ord a => MaxiphobicHeap a -> List a

9998toList Empty = []

10099toList (Node s l e r) = toList' (Node s l e r) Refl

101100 where

102− %assert_total -- relies on deleteMinimum making heap smaller

103101 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a

104− toList' heap p = findMinimum heap p :: (Heap.toList (deleteMinimum heap p))

102+ toList' heap p = assert_total $ -- relies on deleteMinimum making heap smaller

103+ findMinimum heap p :: (Heap.toList (deleteMinimum heap p))

105104

106105fromList : Ord a => List a -> MaxiphobicHeap a

107106fromList = foldr insert empty

libs/prelude/Builtins.idr+9−4

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

172172assert_total : a -> a

173173assert_total x = x

174174

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

176+||| is unreachable

177+assert_unreachable : a

178+-- compiled as primitive

179+

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

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

177−export %assert_total -- need to pretend

182+export

178183believe_me : a -> b

179−believe_me x = prim__believe_me _ _ x

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

180185

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

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

183−public export %assert_total

188+public export

184189really_believe_me : a -> b

185−really_believe_me x = prim__believe_me _ _ x

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

186191

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

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

libs/prelude/Prelude/File.idr+35−11

@@ -6,6 +6,7 @@ import Prelude.Maybe

66import Prelude.Monad

77import Prelude.Chars

88import Prelude.Strings

9+import Prelude.Nat

910import Prelude.Cast

1011import Prelude.Bool

1112import Prelude.Basics

@@ -26,11 +27,12 @@ data File : Type where

2627||| An error from a file operation

2728-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure

2829-- the values correspond!

29−data FileError = FileReadError

30+

31+data FileError = GenericFileError Int -- errno

32+ | FileReadError

3033 | FileWriteError

3134 | FileNotFound

3235 | PermissionDenied

33− | GenericFileError Int -- errno

3436

3537private

3638strError : Int -> String

@@ -133,6 +135,22 @@ export

133135closeFile : File -> IO ()

134136closeFile (FHandle h) = do_fclose h

135137

138+private

139+do_getFileSize : Ptr -> IO Int

140+do_getFileSize h = foreign FFI_C "fileSize" (Ptr -> IO Int) h

141+

142+||| Return the size of a File

143+||| Returns an error if the File is not an ordinary file (e.g. a directory)

144+||| Also note that this currently returns an Int, which may overflow if the

145+||| file is very big

146+export

147+fileSize : File -> IO (Either FileError Int)

148+fileSize (FHandle h) = do s <- do_getFileSize h

149+ if (s < 0)

150+ then do err <- getFileError

151+ return (Left err)

152+ else return (Right s)

153+

136154private

137155do_fread : Ptr -> IO' l String

138156do_fread h = prim_fread h

@@ -233,22 +251,28 @@ fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h

233251 return (p > 0)

234252

235253||| Read the contents of a file into a string

236−-- might be reading something infinitely long like /dev/null ...

237−covering export

238−readFile : String -> IO (Either FileError String)

254+||| This checks the size of the file before beginning to read, and only

255+||| reads that many bytes, to ensure that it remains a total function if

256+||| the file is appended to while being read.

257+||| Returns an error if filepath is not a normal file.

258+export

259+readFile : (filepath : String) -> IO (Either FileError String)

239260readFile fn = do Right h <- openFile fn Read

240261 | Left err => return (Left err)

241− c <- readFile' h ""

262+ Right max <- fileSize h

263+ | Left err => return (Left err)

264+ c <- readFile' h max ""

242265 closeFile h

243266 return c

244267 where

245− covering

246− readFile' : File -> String -> IO (Either FileError String)

247− readFile' h contents =

268+ readFile' : File -> Int -> String -> IO (Either FileError String)

269+ readFile' h max contents =

248270 do x <- fEOF h

249− if not x then do Right l <- fGetLine h

271+ if not x && max > 0

272+ then do Right l <- fGetLine h

250273 | Left err => return (Left err)

251− readFile' h (contents ++ l)

274+ assert_total $

275+ readFile' h (max - cast (length l)) (contents ++ l)

252276 else return (Right contents)

253277

254278||| Write a string to a file

libs/prelude/Prelude/Foldable.idr+23−2

@@ -9,9 +9,30 @@ import Prelude.Algebra

99%access public export

1010%default total

1111

12+||| The `Foldable` interface describes how you can iterate over the

13+||| elements in a parameterised type and combine the elements

14+||| together, using a provided function, into a single result.

15+|||

16+||| @t The type of the 'Foldable' parameterised type.

1217interface Foldable (t : Type -> Type) where

13− foldr : (elem -> acc -> acc) -> acc -> t elem -> acc

14− foldl : (acc -> elem -> acc) -> acc -> t elem -> acc

18+

19+ ||| Successivly combine the elements in a parameterised type using

20+ ||| the provided function, starting with the element that is in the

21+ ||| final position i.e. the right-most position.

22+ |||

23+ ||| @func The function used to 'fold' an element into the accumulated result.

24+ ||| @input The parameterised type.

25+ ||| @init The starting value the results are being combined into.

26+ foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc

27+

28+ ||| The same as `foldr` but begins the folding from the element at

29+ ||| the initial position in the data structure i.e. the left-most

30+ ||| position.

31+ |||

32+ ||| @func The function used to 'fold' an element into the accumulated result.

33+ ||| @input The parameterised type.

34+ ||| @init The starting value the results are being combined into.

35+ foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc

1536 foldl f z t = foldr (flip (.) . flip f) id t z

1637

1738||| Combine each element of a structure into a monoid

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

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

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

412412|||

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

414−%assert_total

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

416415transpose [] = []

417416transpose ([] :: 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)))

419418

420419--------------------------------------------------------------------------------

421420-- Membership tests

rts/idris_stdfgn.c+16−3

@@ -5,6 +5,7 @@

55

66#include <fcntl.h>

77#include <errno.h>

8+#include <sys/stat.h>

89#include <stdio.h>

910#include <time.h>

1011

@@ -40,6 +41,18 @@ int fileError(void* h) {

4041 return ferror(f);

4142}

4243

44+int fileSize(void* h) {

45+ FILE* f = (FILE*)h;

46+ int fd = fileno(f);

47+

48+ struct stat buf;

49+ if (fstat(fd, &buf) == 0) {

50+ return (int)(buf.st_size);

51+ } else {

52+ return -1;

53+ }

54+}

55+

4356int idris_writeStr(void* h, char* str) {

4457 FILE* f = (FILE*)h;

4558 if (fputs(str, f)) {

@@ -103,13 +116,13 @@ VAL idris_mkFileError(VM* vm) {

103116 // Make sure this corresponds to the FileError structure in

104117 // Prelude.File

105118 case ENOENT:

106− idris_constructor(result, vm, 2, 0, 0);

119+ idris_constructor(result, vm, 3, 0, 0);

107120 break;

108121 case EACCES:

109− idris_constructor(result, vm, 3, 0, 0);

122+ idris_constructor(result, vm, 4, 0, 0);

110123 break;

111124 default:

112− idris_constructor(result, vm, 4, 1, 0);

125+ idris_constructor(result, vm, 0, 1, 0);

113126 idris_setConArg(result, 0, MKINT((intptr_t)errno));

114127 break;

115128 }

rts/idris_stdfgn.h+4

@@ -12,6 +12,9 @@ void* fileOpen(char* f, char* mode);

1212void fileClose(void* h);

1313int fileEOF(void* h);

1414int fileError(void* h);

15+// Returns a negative number if not a file (e.g. directory or device)

16+int fileSize(void* h);

17+

1518// return 0 on success

1619int idris_writeStr(void*h, char* str);

1720// construct a file error structure (see Prelude.File) from errno

@@ -20,6 +23,7 @@ VAL idris_mkFileError(VM* vm);

2023void* do_popen(const char* cmd, const char* mode);

2124int fpoll(void* h);

2225

26+

2327int idris_eqPtr(void* x, void* y);

2428int isNull(void* ptr);

2529void* idris_stdin();

src/IRTS/Compiler.hs+78−74

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

154154

155155irMain :: TT Name -> Idris LDecl

156156irMain tm = do

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

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

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

159159

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

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

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

219219

220220mkLDecl n (Function tm _)

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

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

222222

223223mkLDecl 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

225225 where

226226 (args, sc) = cases_runtime cd

227227

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

244244

245245type Vars = M.Map Name VarInfo

246246

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

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

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

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

249249 ist <- getIState

250250 case unApply tm of

251251 (P _ n _, args)

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

257257

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

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

261265

262266 -- TMP HACK - until we get inlining.

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

264268 | r == txt "replace"

265− -> irTerm vs env arg

269+ -> irTerm top vs env arg

266270

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

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

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

277281

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

279283 | l == txt "force"

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

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

281285

282286 -- Laziness, the new way

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

284288 | l == txt "Delay"

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

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

286290

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

288292 | l == txt "Force"

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

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

290294

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

292296 | a == txt "assert_smaller"

293− -> irTerm vs env arg

297+ -> irTerm top vs env arg

294298

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

296300 | a == txt "assert_total"

297− -> irTerm vs env arg

301+ -> irTerm top vs env arg

298302

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

300304 | p == txt "par"

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

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

302306 return $ LOp LPar [LLazyExp arg']

303307

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

305309 | pf == txt "prim_fork"

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

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

307311 return $ LOp LFork [LLazyExp arg']

308312

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

310314 | m == txt "malloc"

311− -> irTerm vs env t

315+ -> irTerm top vs env t

312316

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

314318 | tm == txt "trace_malloc"

315− -> irTerm vs env t -- TODO

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

316320

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

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

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

324328 , b == txt "Bool"

325329 , p == txt "Prelude"

326330 -> do

327− x' <- irTerm vs env x

328− t' <- irTerm vs env t

329− e' <- irTerm vs env e

331+ x' <- irTerm top vs env x

332+ t' <- irTerm top vs env t

333+ e' <- irTerm top vs env e

330334 return (LCase Shared x'

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

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

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

375379

376380 -- exactly saturated

377381 EQ | isNewtype

378− -> irTerm vs env (head argsPruned)

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

379383

380384 | otherwise -- not newtype, plain data ctor

381385 -> buildApp (LV $ Glob n) argsPruned

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

384388 LT | isNewtype -- newtype

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

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

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

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

388392

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

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

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

398402

399403 -- an external name applied to arguments

400404 (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

402406

403407 -- a name applied to arguments

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

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

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

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

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

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

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

410414

411415 -- otherwise, just apply the name

412416 _ -> applyName n ist args

413417

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

416420

417421 (f, args)

418422 -> LApp False

419− <$> irTerm vs env f

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

423+ <$> irTerm top vs env f

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

421425

422426 where

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

424428 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

426430

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

428432 applyToNames tm [] = tm

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

437441

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

439443 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)

441445 where

442446 erase (i, x)

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

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

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

460464 fst4 (x,_,_,_,_) = x

461465

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

463−irTerm vs env (V i)

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

467+irTerm top vs env (V i)

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

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

466470

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

468472 where

469473 n' = uniqueName n env

470474

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

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

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

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

473477

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

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

475479

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

477− t' <- irTerm vs env t

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

481+ t' <- irTerm top vs env t

478482 return $ LOp (LMinus (ATInt ITBig))

479483 [t', LConst (BI 1)]

480484

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

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

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

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

485−irTerm vs env Erased = return $ LNothing

486−irTerm vs env Impossible = return $ LNothing

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

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

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

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

489+irTerm top vs env Erased = return $ LNothing

490+irTerm top vs env Impossible = return $ LNothing

487491

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

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

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

494498 where

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

496500 = do let l' = toFDesc l

497− r' <- irTerm vs env r

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

498502 return (l', r')

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

500504

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

508512 deNS n = n

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

510514

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

512−irTree args tree = do

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

516+irTree top args tree = do

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

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

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

515519

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

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

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

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

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

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

519523

520−irSC vs (ProjCase tm alts) = do

521− tm' <- irTerm vs [] tm

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

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

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

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

523527 return $ LCase Shared tm' alts'

524528

525529-- 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])

527531 | delay == txt "Delay"

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

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

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

530534

531535-- There are two transformations in this case:

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

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

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

552556--

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

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

554558 replacement <- case alt of

555559 ConCase cn a ns sc -> do

556560 detag <- fgetState (opt_detaggable . ist_optimisation cn)

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

561565 _ -> return Nothing

562566

563567 case replacement of

564− Just sc -> irSC vs sc

568+ Just sc -> irSC top vs sc

565569 _ -> do

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

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

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

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

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

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

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

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

596600--

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

598602 detag <- fgetState (opt_detaggable . ist_optimisation cn)

599603 if detag

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

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

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

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

602606

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

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

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

605609 -- see comment above

606610 goneWrong <- or <$> mapM isDetaggable alts

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

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

609613

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

612616 where

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

614618 isDetaggable _ = return False

615619

616−irSC vs ImpossibleCase = return LNothing

620+irSC top vs ImpossibleCase = return LNothing

617621

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

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

619623

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

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

623627 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

625629 where

626630 methodVars = case n of

627631 SN (InstanceCtorN className)

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

631635 _

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

633637

634−irAlt vs _ (ConstCase x rhs)

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

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

638+irAlt top vs _ (ConstCase x rhs)

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

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

637641 where

638642 matchable (I _) = True

639643 matchable (BI _) = True

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

657661

658662 matchableTy _ = False

659663

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

661− rhs' <- irSC vs rhs

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

665+ rhs' <- irSC top vs rhs

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

663667 [tm,

664668 LConst (BI 1)]) rhs')

665669

666−irAlt vs _ (ConstCase c rhs)

670+irAlt top vs _ (ConstCase c rhs)

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

668672

669−irAlt vs _ (DefaultCase rhs)

670− = LDefaultCase <$> irSC vs rhs

673+irAlt top vs _ (DefaultCase rhs)

674+ = LDefaultCase <$> irSC top vs rhs

src/Idris/AbsSyntax.hs+9−3

@@ -1939,9 +1939,9 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

19391939 case ns' of

19401940 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

19411941 (insertImpl ns as)

1942− [] -> if f `elem` (map fst (idris_metavars ist))

1943− then Right $ PApp fc (PRef ffc [ffc] f) as

1944− else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

1942+ [] -> case metaVar f (map fst (idris_metavars ist)) of

1943+ Just f' -> Right $ PApp fc (PRef ffc [ffc] f') as

1944+ Nothing -> Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

19451945 alts -> Right $

19461946 PAlternative [] (ExactlyOne True) $

19471947 map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

@@ -1952,6 +1952,12 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

19521952 isImpName f f' | f `elem` imp_meths = f

19531953 | otherwise = f'

19541954

1955+ -- If it's a metavariable name, try to qualify it from the list of

1956+ -- unsolved metavariables

1957+ metaVar f (mvn : ns) | f == nsroot mvn = Just mvn

1958+ metaVar f (_ : ns) = metaVar f ns

1959+ metaVar f [] = Nothing

1960+

19551961 trimAlts [] alts = alts

19561962 trimAlts ns alts

19571963 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

src/Idris/AbsSyntaxTree.hs+1

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

334334 , sUN "mkLazyForeignPrim"

335335 , sUN "mkForeignPrim"

336336 , sUN "void"

337+ , sUN "assert_unreachable"

337338 ]

338339

339340-- 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.

2323module Idris.Core.CaseTree (

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

2525 , Phase(..), CaseTree, CaseType(..)

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

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

2727 , substSC, substAlt, mkForce

2828 ) where

2929

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

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

151151-- compilation time, and trace all unused arguments

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

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

153+findCalls = findCalls' False

154+

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

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

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

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

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

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

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

167170 nut ps fn@(App _ f a)

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

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

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

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

173+ then []

174+ else if n `elem` ps

175+ then nut ps f ++ nut ps a

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

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

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

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

src/Idris/Core/Execute.hs+9

@@ -376,6 +376,15 @@ execForeign env ctxt arity ty fn xs onfail

376376 "The argument to fileClose should be a file handle, but it was " ++

377377 show handle ++

378378 ". Are all cases covered?"

379+ | Just (FFun "fileSize" [(_,handle)] _) <- foreignFromTT arity ty fn xs

380+ = case handle of

381+ EHandle h -> do size <- execIO $ hFileSize h

382+ let res = ioWrap (EConstant (I (fromInteger size)))

383+ execApp env ctxt res (drop arity xs)

384+ _ -> execFail . Msg $

385+ "The argument to fileSize should be a file handle, but it was " ++

386+ show handle ++

387+ ". Are all cases covered?"

379388

380389 | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs

381390 = case ptr of

src/Idris/Coverage.hs+42−16

@@ -470,16 +470,43 @@ checkTotality path fc n

470470checkDeclTotality :: (FC, Name) -> Idris Totality

471471checkDeclTotality (fc, n)

472472 = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"

473−-- buildSCG (fc, n)

474−-- logCoverage 2 $ "Built SCG"

475473 i <- getIState

476− let opts = case lookupCtxt n (idris_flags i) of

477− [fs] -> fs

474+ let opts = case lookupCtxtExact n (idris_flags i) of

475+ Just fs -> fs

478476 _ -> []

479477 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

480478 t <- checkTotality [] fc n

481479 return t

482480

481+-- If the name calls something which is partial, set it as partial

482+verifyTotality :: (FC, Name) -> Idris ()

483+verifyTotality (fc, n)

484+ = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"

485+ ist <- getIState

486+ case lookupTotalExact n (tt_ctxt ist) of

487+ Just (Total _) -> do

488+ let ns = getNames (tt_ctxt ist)

489+

490+ case getPartial ist [] ns of

491+ Nothing -> return ()

492+ Just bad -> do let t' = Partial (Other bad)

493+ logCoverage 2 $ "Set to " ++ show t'

494+ setTotality n t'

495+ addIBC (IBCTotal n t')

496+ _ -> return ()

497+ where

498+ getNames ctxt = case lookupDefExact n ctxt of

499+ Just (CaseOp _ _ _ _ _ defs)

500+ -> let (top, def) = cases_compiletime defs in

501+ map fst (findCalls' True def top)

502+ _ -> []

503+

504+ getPartial ist [] [] = Nothing

505+ getPartial ist bad [] = Just bad

506+ getPartial ist bad (n : ns)

507+ = case lookupTotalExact n (tt_ctxt ist) of

508+ Just (Partial _) -> getPartial ist (n : bad) ns

509+ _ -> getPartial ist bad ns

483510

484511-- | Calculate the size change graph for this definition

485512--

@@ -547,17 +574,19 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

547574 Guarded <- guarded,

548575 del == txt "Delay"

549576 = findCalls cases Delayed arg pvs pargs

550− | (P _ n _, args) <- unApply ap,

551− Delayed <- guarded,

552− n == topfn -- Under a delayed recursive call to the top level function,

553− -- just check the arguments

554− = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args

555577 | (P _ n _, args) <- unApply ap,

556578 Delayed <- guarded,

557579 isConName n (tt_ctxt ist)

558580 = -- Still under a 'Delay' and constructor guarded, so check

559581 -- just the arguments to the constructor, remaining Delayed

560582 concatMap (\x -> findCalls cases guarded x pvs pargs) args

583+ | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,

584+ ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]

585+ -- Continue look inside if...then...else blocks

586+ -- TODO: Consider whether we should do this for user defined ifThenElse

587+ -- rather than just the one in the Prelude as a special case

588+ = findCalls cases guarded t pvs pargs ++

589+ findCalls cases guarded e pvs pargs

561590 | (P _ n _, args) <- unApply ap,

562591 caseName n && n /= topfn,

563592 notPartial (lookupTotalExact n (tt_ctxt ist))

@@ -569,13 +598,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

569598 if n `notElem` cases

570599 then findCallsCase (n : cases) guarded n args pvs pargs

571600 else []

572− | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,

573− ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]

574− -- Continue look inside if...then...else blocks

575− -- TODO: Consider whether we should do this for user defined ifThenElse

576− -- rather than just the one in the Prelude as a special case

577− = findCalls cases guarded t pvs pargs ++

578− findCalls cases guarded e pvs pargs

601+ | (P _ n _, args) <- unApply ap,

602+ Delayed <- guarded

603+ -- Under a delayed recursive call just check the arguments

604+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args

579605 | (P _ n _, args) <- unApply ap

580606 -- Ordinary call, not under a delay.

581607 -- If n is a constructor, set 'args' as Guarded

src/Idris/ElabDecls.hs+4

@@ -219,6 +219,10 @@ elabDecl' what info (PMutual f ps)

219219 (map snd (idris_totcheck i))

220220 mapM_ buildSCG (idris_totcheck i)

221221 mapM_ checkDeclTotality (idris_totcheck i)

222+ -- We've only checked that things are total independently. Given

223+ -- the ordering, something we think is total might have called

224+ -- something we hadn't checked yet

225+ mapM_ verifyTotality (idris_totcheck i)

222226 clear_totcheck

223227 where isDataDecl (PData _ _ _ _ _ _) = True

224228 isDataDecl _ = False

src/Idris/Interactive.hs+8−4

@@ -20,6 +20,7 @@ import Idris.CaseSplit

2020import Idris.AbsSyntax

2121import Idris.ElabDecls

2222import Idris.Error

23+import Idris.ErrReverse

2324import Idris.Delaborate

2425import Idris.Output

2526import Idris.IdeMode hiding (IdeModeCommand(..))

@@ -333,11 +334,14 @@ makeLemma fn updatefile l n

333334 let isProv = checkProv tyline (show n)

334335

335336 ctxt <- getContext

336− (fname, mty) <- case lookupTyName n ctxt of

337− [t] -> return t

338− [] -> ierror (NoSuchVariable n)

339− ns -> ierror (CantResolveAlts (map fst ns))

337+ (fname, mty_full) <- case lookupTyName n ctxt of

338+ [t] -> return t

339+ [] -> ierror (NoSuchVariable n)

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

341+

340342 i <- getIState

343+ let mty = errReverse i mty_full

344+

341345 margs <- case lookup fname (idris_metavars i) of

342346 Just (_, arity, _, _, _) -> return arity

343347 _ -> return (-1)

src/Idris/Parser.hs+4−1

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

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

703703 return Inlinable

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

705− return AssertTotal

705+ fc <- getFC

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

707+ return AssertTotal

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

707709 return ErrorHandler

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

@@ -1819,6 +1821,7 @@ loadSource lidr f toline

18191821 i <- getIState

18201822 mapM_ buildSCG (idris_totcheck i)

18211823 mapM_ checkDeclTotality (idris_totcheck i)

1824+ mapM_ verifyTotality (idris_totcheck i)

18221825

18231826 -- Redo totality check for deferred names

18241827 let deftots = idris_defertotcheck i

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

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

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

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

6363

64−%assert_total

6564export

6665snoc : Bytes -> Byte -> Bytes

6766snoc bs@(B arr ofs end) byte

68− = if end >= BA.size arr

67+ = assert_total $

68+ if end >= BA.size arr

6969 then unsafePerformIO $ do -- need more space

7070 grown <- grow 2 bs

7171 return $ snoc grown byte

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

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

115115

116116infixr 7 ++

117−%assert_total

118117export

119118(++) : Bytes -> Bytes -> Bytes

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

121− = let countR = endR - ofsR in

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

122121 if endL + countR > BA.size arrL

123122 then unsafePerformIO $ do -- need more space

124123 grown <- grow 2 bsL

test/reg035/reg035a.lidr+1−2

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

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

1616> hasNoDuplicates as = as == nub as

1717

18−> %assert_total

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

2019> setEq Nil Nil = True

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

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

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

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

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

2524> ||

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

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

test/reg041/ott.idr+2−3

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

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

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

2525

26−%assert_total

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

2827EQ MkU MkU MkU MkU = One

2928EQ MkU Zero MkU Zero = One

3029EQ MkU One MkU One = One

3130EQ 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)

3332EQ Zero x Zero y = One

3433EQ One x One y = One

3534EQ Two True Two True = One

3635EQ 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)

3837EQ _ _ _ _ = Zero

3938

4039example : <| (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

3+

4+%default total

5+

6+data Command : Type -> Type where

7+ PutStr : String -> Command ()

8+ GetLine : Command String

9+

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