git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1980 from david-christiansen/dsl-dollars

Fix minor bugs that result from other changes

commitec13063750602b748a36f2fbdb782681855cbf30 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 6 Mar 2015, 10:53 (12 years ago) parent16c3c3cc9b1759
4 files changed+8−15
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Errors.idr+1−1 src/Idris/ElabTerm.hs+1−1 src/Idris/ParseHelpers.hs+1−1 test/reg050/expected+5−12
libs/prelude/Language/Reflection/Errors.idr+1−1
@@ -29,7 +29,7 @@ data Err = Msg String
2929 | NoTypeDecl TTName
3030 | NotInjective TT TT TT
3131 | CantResolve TT
32− | CantResolveAlts (List String)
32+ | CantResolveAlts (List TTName)
3333 | IncompleteTerm TT
3434 | UniverseError
3535 | ProgramLineComment
src/Idris/ElabTerm.hs+1−1
@@ -2600,7 +2600,7 @@ reflectErr (NotInjective t1 t2 t3) =
26002600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
26012601reflectErr (CantResolveAlts ss) =
26022602 raw_apply (Var $ reflErrName "CantResolveAlts")
2603− [rawList (Var $ (sUN "String")) (map Var ss)]
2603+ [rawList (Var $ reflm "TTName") (map reflectName ss)]
26042604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
26052605reflectErr UniverseError = Var $ reflErrName "UniverseError"
26062606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
src/Idris/ParseHelpers.hs+1−1
@@ -326,7 +326,7 @@ commentMarkers :: [String]
326326commentMarkers = [ "--", "|||" ]
327327
328328invalidOperators :: [String]
329−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%"]
329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
330330
331331-- | Parses an operator
332332operator :: MonadicParsing m => m String
test/reg050/expected+5−12
@@ -1,15 +1,8 @@
1−badbangop.idr:16:1:When elaborating right hand side of opUse:
2−When elaborating an application of function Prelude.Monad.>>=:
3− Can't unify
4− List Integer
5− with
6− argTy -> retTy
7−
8− Specifically:
9− Can't unify
10− List
11− with
12− \{uv0} => argTy -> uv
1+./badbangop.idr:7:1: error: ! is
2+ not a valid
3+ operator, expected: space
4+(!) : List a -> Nat -> Maybe a
5+^
136./baddoublebang.idr:6:28: error: unexpected
147 Operator without known fixity:
158 !!, expected: space