11dbfc0 · Idris-dev · git.iko.soy

src/Idris/Coverage.hs+2−3

@@ -559,9 +559,8 @@ checkMP ist i mp = if i > 0

559 x -> error (show x)

560 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

561 = Total []

562−-- tryPath desc path (e@(f, []) : es) arg

562+ tryPath desc path (e@(f, []) : es) arg

563−-- | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

563+ | e `elem` es = Partial (Mutual [f])

564−-- tryPath (-10000) ((e, desc) : path) es 0

565 tryPath desc path (e@(f, nextargs) : es) arg

564 tryPath desc path (e@(f, nextargs) : es) arg

566 | Just d <- lookup e path

565 | Just d <- lookup e path

567 = if desc > 0

566 = if desc > 0

test/test017/expected+1

@@ -1 +1,2 @@

1test017a.idr:5:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

2+test017b.idr:4:foo.foo is possibly not total due to recursive path foo.foo

test/test017/run+1

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

1#!/bin/bash

2idris $@ --check test017.idr

3idris $@ --check test017a.idr

4+idris $@ --check test017b.idr

4rm -f *.ibc

5rm -f *.ibc

test/test017/test017b.idrnew file+5

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

1+module foo

2+

3+total foo : _|_

4+foo = foo

5+