ae9b938 · Idris-dev · git.iko.soy

.travis.yml+1

compare with master

unifiedsplit

@@ -12,6 +12,7 @@ before_install:

12 - sudo apt-get install -qq expect

13install:

14 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests

15+ - ghc-pkg list

15before_script:

16before_script:

16 - cabal sdist

17 - cabal sdist

17 - cd ..

18 - cd ..

libs/base/Data/Vect/Quantifiers.idr+4−1

@@ -5,9 +5,12 @@ data Any : (P : a -> Type) -> Vect n a -> Type where

5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)

6

7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_

8−anyNilAbsurd (Here _) impossible

8+anyNilAbsurd (Here _) impossible

9anyNilAbsurd (There _) impossible

10

11+instance Uninhabited (Any p Nil) where

12+ uninhabited = anyNilAbsurd

13+

11anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

14anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

12anyElim _ f (Here p) = f p

15anyElim _ f (Here p) = f p

13anyElim f _ (There p) = f p

16anyElim f _ (There p) = f p

libs/prelude/Prelude/Traversable.idr+6

@@ -9,8 +9,14 @@ traverse_ f = foldr (($>) . f) (pure ())

9sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()

10sequence_ = foldr ($>) (pure ())

11

12+for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()

13+for_ = flip traverse_

14+

12class (Functor t, Foldable t) => Traversable (t : Type -> Type) where

15class (Functor t, Foldable t) => Traversable (t : Type -> Type) where

13 traverse : Applicative f => (a -> f b) -> t a -> f (t b)

16 traverse : Applicative f => (a -> f b) -> t a -> f (t b)

14

17

15sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)

18sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)

16sequence = traverse id

19sequence = traverse id

20+

21+for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)

22+for = flip traverse

src/Idris/AbsSyntaxTree.hs+4

@@ -195,6 +195,10 @@ data IState = IState {

195 idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined

196 }

197

198+-- Required for parsers library, and therefore trifecta

199+instance Show IState where

200+ show = const "{internal state}"

201+

198data SizeChange = Smaller | Same | Bigger | Unknown

202data SizeChange = Smaller | Same | Bigger | Unknown

199 deriving (Show, Eq)

203 deriving (Show, Eq)

200{-!

204{-!

src/Idris/ParseExpr.hs+1−1

@@ -522,7 +522,7 @@ app syn = do f <- reserved "mkForeign"

522 return (dslify i ap)

523

524 <|> do f <- simpleExpr syn

525− (do try $ symbol "<=="

525+ (do try $ reservedOp "<=="

526 fc <- getFC

527 ff <- fnName

528 return (PLet (sMN 0 "match")

test/totality003/totality003.idr+1−1

@@ -3,5 +3,5 @@ module smaller

3total

4qsort : Ord a => List a -> List a

5qsort [] = []

6−qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++

6+qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++

7 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))

test/totality003/totality003a.idr+1−1