mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
Merge branch 'feature/betteroperatormessage' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/betteroperatormessage
Conflicts: test/reg050/expected
This commit is contained in:
commit
c70b2a310a
@ -119,7 +119,7 @@ singleLineComment :: MonadicParsing m => m ()
|
||||
singleLineComment = (string "--" *>
|
||||
many (satisfy (not . isEol)) *>
|
||||
eol *> pure ())
|
||||
<?> "single-line comment"
|
||||
<?> ""
|
||||
|
||||
{- | Consumes a multi-line comment
|
||||
|
||||
@ -321,10 +321,17 @@ opChars = ":!#$%&*+./<=>?@\\^|-~"
|
||||
operatorLetter :: MonadicParsing m => m Char
|
||||
operatorLetter = oneOf opChars
|
||||
|
||||
|
||||
commentMarkers :: [String]
|
||||
commentMarkers = [ "--", "|||" ]
|
||||
|
||||
invalidOperators :: [String]
|
||||
invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\"]
|
||||
|
||||
-- | Parses an operator
|
||||
operator :: MonadicParsing m => m String
|
||||
operator = do op <- token . some $ operatorLetter
|
||||
when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $
|
||||
when (op `elem` (invalidOperators ++ commentMarkers)) $
|
||||
fail $ op ++ " is not a valid operator"
|
||||
return op
|
||||
|
||||
|
@ -37,7 +37,8 @@ table fixes
|
||||
toTable (reverse fixes) ++
|
||||
[[backtick],
|
||||
[binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],
|
||||
[binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft]]
|
||||
[binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft],
|
||||
[nofixityoperator]]
|
||||
where
|
||||
flatten :: PTerm -> PTerm -- flatten application
|
||||
flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
|
||||
@ -80,6 +81,13 @@ backtick = Infix (do indentPropHolds gtProp
|
||||
fc <- getFC
|
||||
return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
|
||||
|
||||
-- | Operator without fixity (throws an error)
|
||||
nofixityoperator :: Operator IdrisParser PTerm
|
||||
nofixityoperator = Infix (do indentPropHolds gtProp
|
||||
op <- try operator
|
||||
unexpected $ "Operator without known fixity: " ++ op) AssocNone
|
||||
|
||||
|
||||
{- | Parses an operator in function position i.e. enclosed by `()', with an
|
||||
optional namespace
|
||||
|
||||
|
@ -291,6 +291,10 @@ syntaxRule syn
|
||||
|
||||
mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
|
||||
mkSimple es
|
||||
-- Can't parse a full expression followed by operator like characters due to ambiguity
|
||||
mkSimple' (Expr e : Symbol s : es)
|
||||
| takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es
|
||||
where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
|
||||
mkSimple' (e : es) = e : mkSimple' es
|
||||
mkSimple' [] = []
|
||||
|
||||
|
@ -37,6 +37,6 @@ EQ two False two False = one
|
||||
EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)
|
||||
EQ _ _ _ _ = zero
|
||||
|
||||
example : <| id == id in (two ~> two) |>
|
||||
example : <| (id == id in (two ~> two)) |>
|
||||
example = ?prf
|
||||
|
||||
|
@ -10,20 +10,8 @@ When elaborating an application of function Prelude.Monad.>>=:
|
||||
List
|
||||
with
|
||||
\{uv0} => argTy -> uv
|
||||
./baddoublebang.idr:6:26: error: not
|
||||
a terminator, expected: "$",
|
||||
"&&", "*", "*>", "+", "++", "-",
|
||||
"->", ".", "/", "/=", "::", ";",
|
||||
"<", "<#>", "<$>", "<*", "<*>",
|
||||
"<+>", "<->", "<.>", "<<", "<=",
|
||||
"<|>", "=", "==", ">", ">=",
|
||||
">>", ">>=", "\\\\", "`", "in",
|
||||
"||", "~=~",
|
||||
ambiguous use of a left-associative operator,
|
||||
ambiguous use of a non-associative operator,
|
||||
ambiguous use of a right-associative operator,
|
||||
end of input, function argument,
|
||||
matching application expression,
|
||||
single-line comment
|
||||
./baddoublebang.idr:6:28: error: unexpected
|
||||
Operator without known fixity:
|
||||
!!, expected: space
|
||||
doubleBang mmn = do pure !!mmn
|
||||
^
|
||||
^
|
||||
|
Loading…
Reference in New Issue
Block a user