Merge pull request #4198 from ahmadsalim/bug/fixtotalitchecking
Fixing issue with totality regarding partially applied functions
commita92f2f87a66c5db5bea6410d6f022aa4a695e0f8
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateWed 15 Nov 2017, 19:56 (9 years ago)
parent8c5758cdcaa109
src/Idris/Termination.hs+1−1
@@ -429,7 +429,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
429429 [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args
430430 _ -> args
431431 where expand i (Bind n (Pi _ _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs
432− expand i (Bind n (Pi _ _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []
432+ expand i (Bind n (Pi _ _ _ _) sc) [] = Nothing : expand (i + 1) sc []
433433 expand i _ xs = xs
434434
435435 mkChange n args pargs = [(n, expandToArity n (sizes args))]
test/totality024/expectednew file+1
@@ -0,0 +1 @@
1+totality023.idr:5:3:Main.ana is possibly not total due to: Main.ana, go
test/totality024/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ totality023.idr --check
3+rm -f *.ibc
test/totality024/totality023.idrnew file+7
@@ -0,0 +1,7 @@
1+%default total
2+
3+mutual
4+ ana : (a -> Maybe a) -> a -> Nat
5+ ana f = go . f
6+ where go Nothing = Z
7+ go (Just x) = S $ ana f x