Merge branch 'master' into repl-definitions
commitae9b938acf0fcbaa218233b6485043a6da7b4d42
authorAlyssa Carter <trillionalyssa@gmail.com>
dateWed 23 Jul 2014, 17:18 (12 years ago)
parent7d081b0abc99c6
.travis.yml+1
@@ -12,6 +12,7 @@ before_install:
1212 - sudo apt-get install -qq expect
1313install:
1414 - cabal install -f FFI -f LLVM --only-dependencies --enable-tests
15+ - ghc-pkg list
1516before_script:
1617 - cabal sdist
1718 - cd ..
libs/base/Data/Vect/Quantifiers.idr+4−1
@@ -5,9 +5,12 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
55 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
66
77anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8−anyNilAbsurd (Here _) impossible
8+anyNilAbsurd (Here _) impossible
99anyNilAbsurd (There _) impossible
1010
11+instance Uninhabited (Any p Nil) where
12+ uninhabited = anyNilAbsurd
13+
1114anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
1215anyElim _ f (Here p) = f p
1316anyElim f _ (There p) = f p
libs/prelude/Prelude/Traversable.idr+6
@@ -9,8 +9,14 @@ traverse_ f = foldr (($>) . f) (pure ())
99sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
1010sequence_ = foldr ($>) (pure ())
1111
12+for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
13+for_ = flip traverse_
14+
1215class (Functor t, Foldable t) => Traversable (t : Type -> Type) where
1316 traverse : Applicative f => (a -> f b) -> t a -> f (t b)
1417
1518sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
1619sequence = 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 {
195195 idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined
196196 }
197197
198+-- Required for parsers library, and therefore trifecta
199+instance Show IState where
200+ show = const "{internal state}"
201+
198202data SizeChange = Smaller | Same | Bigger | Unknown
199203 deriving (Show, Eq)
200204{-!
src/Idris/ParseExpr.hs+1−1
@@ -522,7 +522,7 @@ app syn = do f <- reserved "mkForeign"
522522 return (dslify i ap)
523523
524524 <|> do f <- simpleExpr syn
525− (do try $ symbol "<=="
525+ (do try $ reservedOp "<=="
526526 fc <- getFC
527527 ff <- fnName
528528 return (PLet (sMN 0 "match")
test/totality003/totality003.idr+1−1
@@ -3,5 +3,5 @@ module smaller
33total
44qsort : Ord a => List a -> List a
55qsort [] = []
6−qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
6+qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
77 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
test/totality003/totality003a.idr+1−1
@@ -3,5 +3,5 @@ module smaller
33total
44qsort : Ord a => List a -> List a
55qsort [] = []
6−qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++
6+qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
77 (x :: qsort (filter (>= x) xs))