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

git.iko.soy/Idris-dev

Remove pattern variables from size change graphs

This should have been happening already, but it turns out not when the variable is applied to arguments. Fixes #3491

commit89ca1069feca5f36b0a6d7df27f354635f412ece authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Mar 2017, 10:37 (10 years ago) parentb8b447f

3 files changed+12−3

unifiedsplit

src/Idris/Termination.hs+2−1

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

351351 Delayed <- guarded

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

353353 = 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)

355356 -- Ordinary call, not under a delay.

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

357358 = 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

6+f : a

7+f = f

test/regression001/run+2−2

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

11#!/usr/bin/env bash

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

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

4− reg038.idr reg046.idr \

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

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

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

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

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