449e292 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak totality checker

commit449e2927a0cb9c22fc12f60366384abf357b67c5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 16 Dec 2012, 20:24 (14 years ago) parent906862a

4 files changed+8−6

compare with master

unifiedsplit

lib/Prelude/List.idr+2 src/Core/CaseTree.hs+1−1 src/Idris/Coverage.hs+4−5 test/reg006/run+1

lib/Prelude/List.idr+2

@@ -448,6 +448,8 @@ sorted (x::xs) =

448448 Nil => True

449449 (y::ys) => x <= y && sorted (y::ys)

450450

451+%assert_total -- can't work this out, because in the case which is lifted out

452+ -- y::ys and x::xs are bigger than the inputs...

451453mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a

452454mergeBy order [] right = right

453455mergeBy order left [] = left

src/Core/CaseTree.hs+1−1

@@ -79,7 +79,7 @@ instance TermSize CaseAlt where

7979small :: Name -> [Name] -> SC -> Bool

8080small n args t = let as = findAllUsedArgs t args in

8181 length as == length (nub as) &&

82− termsize n t < 6

82+ termsize n t < 20

8383

8484namesUsed :: SC -> [Name]

8585namesUsed sc = nub $ nu' [] sc where

src/Idris/Coverage.hs+4−5

@@ -564,7 +564,7 @@ checkMP ist i mp = if i > 0

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

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

566566 | Just d <- lookup e path

567− = if (desc - d) > 0

567+ = if desc > 0

568568 then -- trace ("Descent " ++ show (desc - d) ++ " "

569569 -- ++ show (path, e)) $

570570 Total []

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

585585 Just (nextarg, sc) ->

586586 if nextarg == arg then

587587 case sc of

588− Same -> return $ tryPath desc ((e, desc):path)

589− es

590− pos

588+ Same -> return $ tryPath desc ((e, desc) : path)

589+ es pos

591590 Smaller -> return $ tryPath (desc+1)

592591 ((e, desc):path)

593592 es

@@ -607,6 +606,6 @@ collapse xs = collapse' Unchecked xs

607606collapse' def (Total r : xs) = Total r

608607collapse' def (Unchecked : xs) = collapse' def xs

609608collapse' def (d : xs) = collapse' d xs

610−collapse' Unchecked [] = Total []

609+-- collapse' Unchecked [] = Total []

611610collapse' def [] = def

612611

test/reg006/run+1

@@ -1,2 +1,3 @@

11#!/bin/bash

22idris $@ reg006.idr -o reg006

3+rm -f *.ibc