89ca106 · Idris-dev · git.iko.soy

src/Idris/Termination.hs+2−1

@@ -351,7 +351,8 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

351 Delayed <- guarded

352 -- Under a delayed recursive call just check the arguments

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

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

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

355+ not (n `elem` pvs)

355 -- Ordinary call, not under a delay.

356 -- Ordinary call, not under a delay.

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

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

357 = let nguarded = case guarded of

358 = let nguarded = case guarded of

test/regression001/reg005.idrnew file+8

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

1+total

2+map' : (a -> b) -> List a -> List b

3+map' _ [] = []

4+map' f (x :: xs) = f x :: map' f xs

5+

6+f : a

7+f = f

8+

test/regression001/run+2−2

@@ -1,7 +1,7 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ --check \

3− reg001.idr reg002.idr reg003.idr reg004.lidr reg036.idr reg037.idr \

3+ reg001.idr reg002.idr reg003.idr reg004.lidr reg005.idr \

4− reg038.idr reg046.idr \

4+ reg036.idr reg037.idr reg038.idr reg046.idr \

5 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \

6 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \

7 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \