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

git.iko.soy/Idris-dev

Correct totality check of f=f, and add regression test

commit11dbfc0de201aac53ac7c2e45fa2c81523351ab0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 17 Dec 2012, 12:06 (14 years ago) parentbc3e807

4 files changed+9−3

unifiedsplit

src/Idris/Coverage.hs+2−3

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

559559 x -> error (show x)

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

561561 = Total []

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

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

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

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

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

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

566565 | Just d <- lookup e path

567566 = if desc > 0

test/test017/expected+1

@@ -1 +1,2 @@

11test017a.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 @@

11#!/bin/bash

22idris $@ --check test017.idr

33idris $@ --check test017a.idr

4+idris $@ --check test017b.idr

45rm -f *.ibc

test/test017/test017b.idrnew file+5

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

1+module foo

3+total foo : _|_

4+foo = foo