5aa2a8e · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

452 test/totality007/*.ipkg

453 test/totality007/src/*.idr

454 test/totality007/expected

455+ test/totality008/run

456+ test/totality008/*.idr

457+ test/totality008/expected

455

458

456 test/tutorial001/run

459 test/tutorial001/run

457 test/tutorial001/*.idr

460 test/tutorial001/*.idr

src/Idris/Coverage.hs+11−4

@@ -271,7 +271,7 @@ checkAllCovering _ _ _ _ = return ()

271

272checkPositive :: [Name] -> (Name, Type) -> Idris Totality

273checkPositive mut_ns (cn, ty')

274− = do let ty = delazy ty'

274+ = do let ty = delazy' True ty'

275 let p = cp ty

276 i <- getIState

277 let tot = if p then Total (args ty) else Partial NotPositive

@@ -284,12 +284,19 @@ checkPositive mut_ns (cn, ty')

284 args t = [0..length (getArgTys t)-1]

285

286 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

287+ cp t | (P _ n' _, args) <- unApply t,

288+ n' `elem` mut_ns = all noRec args

287− cp t = True

289+ cp _ = True

288

290

289 posArg (Bind _ (Pi nty) sc)

291 posArg (Bind _ (Pi nty) sc)

290 | (P _ n' _, args) <- unApply nty

292 | (P _ n' _, args) <- unApply nty

291− = n' `notElem` mut_ns && posArg sc

293+ = n' `notElem` mut_ns && all noRec args && posArg sc

292− posArg t = True

294+ posArg t | (P _ n' _, args) <- unApply t,

295+ n' `elem` mut_ns = all noRec args

296+ posArg _ = True

297+

298+ noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

299+

293

300

294calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

301calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

295calcProd i fc topn pats

302calcProd i fc topn pats

test/totality008/expectednew file+1

@@ -0,0 +1 @@

1+totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.c2

test/totality008/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ totality008.idr --check

3+rm -f *.ibc

test/totality008/totality008.idrnew file+8

@@ -0,0 +1,8 @@

1+ data T : Type -> Type where

2+ c1 : T Nat

3+ c2 : T (T Nat)

4+

5+total

6+ElimT : (A : Type) -> T A -> A

7+ElimT _ c1 = 3

8+ElimT _ c2 = c1