c70b2a3 · Idris-dev · git.iko.soy

src/Idris/ParseHelpers.hs+9−2

compare with master

unifiedsplit

@@ -119,7 +119,7 @@ singleLineComment :: MonadicParsing m => m ()

119singleLineComment = (string "--" *>

120 many (satisfy (not . isEol)) *>

121 eol *> pure ())

122− <?> "single-line comment"

122+ <?> ""

123

124{- | Consumes a multi-line comment

125

@@ -321,10 +321,17 @@ opChars = ":!#$%&*+./<=>?@\\^|-~"

321operatorLetter :: MonadicParsing m => m Char

322operatorLetter = oneOf opChars

323

324+

325+commentMarkers :: [String]

326+commentMarkers = [ "--", "|||" ]

327+

328+invalidOperators :: [String]

329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\"]

330+

324-- | Parses an operator

331-- | Parses an operator

325operator :: MonadicParsing m => m String

332operator :: MonadicParsing m => m String

326operator = do op <- token . some $ operatorLetter

333operator = do op <- token . some $ operatorLetter

327− when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $

334+ when (op `elem` (invalidOperators ++ commentMarkers)) $

328 fail $ op ++ " is not a valid operator"

335 fail $ op ++ " is not a valid operator"

329 return op

336 return op

330

337

src/Idris/ParseOps.hs+9−1

@@ -37,7 +37,8 @@ table fixes

37 toTable (reverse fixes) ++

38 [[backtick],

39 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

40− [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft]]

40+ [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft],

41+ [nofixityoperator]]

41 where

42 where

42 flatten :: PTerm -> PTerm -- flatten application

43 flatten :: PTerm -> PTerm -- flatten application

43 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

@@ -80,6 +81,13 @@ backtick = Infix (do indentPropHolds gtProp

80 fc <- getFC

81 fc <- getFC

81 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82

83

84+-- | Operator without fixity (throws an error)

85+nofixityoperator :: Operator IdrisParser PTerm

86+nofixityoperator = Infix (do indentPropHolds gtProp

87+ op <- try operator

88+ unexpected $ "Operator without known fixity: " ++ op) AssocNone

89+

90+

83{- | Parses an operator in function position i.e. enclosed by `()', with an

91{- | Parses an operator in function position i.e. enclosed by `()', with an

84 optional namespace

92 optional namespace

85

93

src/Idris/Parser.hs+4

@@ -291,6 +291,10 @@ syntaxRule syn

291

292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

293 mkSimple es

294+ -- Can't parse a full expression followed by operator like characters due to ambiguity

295+ mkSimple' (Expr e : Symbol s : es)

296+ | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

297+ where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

294 mkSimple' (e : es) = e : mkSimple' es

298 mkSimple' (e : es) = e : mkSimple' es

295 mkSimple' [] = []

299 mkSimple' [] = []

296

300

test/reg041/ott.idr+1−1

@@ -37,6 +37,6 @@ EQ two False two False = one

37EQ (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)

38EQ _ _ _ _ = zero

39

40−example : <| id == id in (two ~> two) |>

40+example : <| (id == id in (two ~> two)) |>

41example = ?prf

42

test/reg050/expected+4−16

@@ -10,20 +10,8 @@ When elaborating an application of function Prelude.Monad.>>=:

10 List

11 with

12 \{uv0} => argTy -> uv

13−./baddoublebang.idr:6:26: error: not

13+./baddoublebang.idr:6:28: error: unexpected

14+ Operator without known fixity:

14− a terminator, expected: "$",

15+ !!, expected: space

15− "&&", "*", "*>", "+", "++", "-",

16− "->", ".", "/", "/=", "::", ";",

17− "<", "<#>", "<$>", "<*", "<*>",

18− "<+>", "<->", "<.>", "<<", "<=",

19− "<|>", "=", "==", ">", ">=",

20− ">>", ">>=", "\\\\", "`", "in",

21− "||", "~=~",

22− ambiguous use of a left-associative operator,

23− ambiguous use of a non-associative operator,

24− ambiguous use of a right-associative operator,

25− end of input, function argument,

26− matching application expression,

27− single-line comment

28doubleBang mmn = do pure !!mmn

16doubleBang mmn = do pure !!mmn

29− ^

17+ ^