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

lib/Prelude/List.idr+2

compare with master

unifiedsplit

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

448 Nil => True

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

450

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...

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

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

452mergeBy order [] right = right

454mergeBy order [] right = right

453mergeBy order left [] = left

455mergeBy order left [] = left

src/Core/CaseTree.hs+1−1

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

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

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

81 length as == length (nub as) &&

82− termsize n t < 6

82+ termsize n t < 20

83

84namesUsed :: SC -> [Name]

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

src/Idris/Coverage.hs+4−5

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

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

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

566 | Just d <- lookup e path

567− = if (desc - d) > 0

567+ = if desc > 0

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

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

570 Total []

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

585 Just (nextarg, sc) ->

586 if nextarg == arg then

587 case sc of

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

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

589− es

590− pos

589+ es pos

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

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

592 ((e, desc):path)

591 ((e, desc):path)

593 es

592 es

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

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

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

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

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

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

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

610−collapse' Unchecked [] = Total []

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

611collapse' def [] = def

610collapse' def [] = def

612

611

test/reg006/run+1

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

1#!/bin/bash

2idris $@ reg006.idr -o reg006

3+rm -f *.ibc