13308b1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow declaring fixity of ticked operators (#4140)

commit13308b1e854432b6d4ec7ac60de7833411fa3074 authorJason Felice <jason.m.felice@gmail.com> dateMon 23 Oct 2017, 07:09 (9 years ago) parent3d514ac

8 files changed+137−115

compare with master

unifiedsplit

CHANGELOG.md+6−2 src/Idris/Parser.hs+3−3 src/Idris/Parser/Expr.hs+12−17 src/Idris/Parser/Helpers.hs+12−37 src/Idris/Parser/Ops.hs+87−55 src/Idris/REPL/Parser.hs+1−1 test/basic023/expected+3 test/basic023/sections.idr+13

CHANGELOG.md+6−2

@@ -8,8 +8,12 @@

88+ The `LinearTypes` language extension has been revised. It implements the

99 rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative

1010 Type Theory" and now works with holes and case expressions.

11−+ Backticked operators can appear in sections, e.g. `(\`LTE\` 42)` or

12− `(1 \`plus\`)`.

11++ Backticked operators can appear in sections, e.g. ``(`LTE` 42)`` or

12+ ``(1 `plus`)``.

13++ Backticked operators can have their precendence and associativity set like

14+ other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with

15+ undeclared fixity are treated as non-associative with precedence lower

16+ than all declared operators.

1317

1418## Library Updates

1519

src/Idris/Parser.hs+3−3

@@ -1086,7 +1086,7 @@ RHSName ::= '{' FnName '}';

10861086-}

10871087rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

10881088rhs syn n = do lchar '='

1089− indentPropHolds gtProp

1089+ indentGt

10901090 expr syn

10911091 <|> do symbol "?=";

10921092 fc <- getFC

@@ -1181,7 +1181,7 @@ clause syn

11811181 <|> do (l, op, nfc) <- try (do

11821182 pushIndent

11831183 l <- argExpr syn

1184− (op, nfc) <- operatorFC

1184+ (op, nfc) <- symbolicOperatorFC

11851185 when (op == "=" || op == "?=" ) $

11861186 fail "infix clause definition with \"=\" and \"?=\" not supported "

11871187 return (l, op, nfc))

@@ -1533,7 +1533,7 @@ parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left

15331533 t <- spaced (expr defaultSyntax)

15341534 i <- get

15351535 return $ tactic (desugar defaultSyntax i t)

1536− spaced parser = indentPropHolds gtProp *> parser

1536+ spaced parser = indentGt *> parser

15371537

15381538-- | Parse module header and imports

15391539parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

src/Idris/Parser/Expr.hs+12−17

@@ -468,8 +468,7 @@ bracketed' open syn =

468468 lchar ')'

469469 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

470470 <|> try (dependentPair TypeOrTerm [] open syn)

471− <|> try (do fc <- getFC

472− opName <- operatorName

471+ <|> try (do (opName, fc) <- operatorName

473472 guardNotPrefix opName

474473

475474 e <- expr syn

@@ -478,7 +477,7 @@ bracketed' open syn =

478477 (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),

479478 pexp e]))

480479 <|> try (simpleExpr syn >>= \l ->

481− try (do opName <- operatorName

480+ try (do (opName, _) <- operatorName

482481 lchar ')'

483482 fc <- getFC

484483 return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

@@ -488,10 +487,6 @@ bracketed' open syn =

488487 <|> do l <- expr (allowConstr syn)

489488 bracketedExpr (allowConstr syn) open l

490489 where

491− operatorName :: IdrisParser Name

492− operatorName = sUN <$> operator

493− <|> fst <$> between (lchar '`') (lchar '`') fnName

494−

495490 justPrefix :: FixDecl -> Maybe Name

496491 justPrefix (Fix (PrefixN _) opName) = Just (sUN opName)

497492 justPrefix _ = Nothing

@@ -1558,8 +1553,8 @@ tactics =

15581553 imps <- many imp

15591554 return $ Refine n imps)

15601555 , (["claim"], Nothing, \syn ->

1561− do n <- indentPropHolds gtProp *> (fst <$> name)

1562− goal <- indentPropHolds gtProp *> expr syn

1556+ do n <- indentGt *> (fst <$> name)

1557+ goal <- indentGt *> expr syn

15631558 return $ Claim n goal)

15641559 , (["mrefine"], Just ExprTArg, const $

15651560 do n <- spaced (fst <$> fnName)

@@ -1569,15 +1564,15 @@ tactics =

15691564 , expressionTactic ["induction"] Induction

15701565 , expressionTactic ["equiv"] Equiv

15711566 , (["let"], Nothing, \syn -> -- FIXME syntax for let

1572− do n <- (indentPropHolds gtProp *> (fst <$> name))

1573− (do indentPropHolds gtProp *> lchar ':'

1574− ty <- indentPropHolds gtProp *> expr' syn

1575− indentPropHolds gtProp *> lchar '='

1576− t <- indentPropHolds gtProp *> expr syn

1567+ do n <- (indentGt *> (fst <$> name))

1568+ (do indentGt *> lchar ':'

1569+ ty <- indentGt *> expr' syn

1570+ indentGt *> lchar '='

1571+ t <- indentGt *> expr syn

15771572 i <- get

15781573 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))

1579− <|> (do indentPropHolds gtProp *> lchar '='

1580− t <- indentPropHolds gtProp *> expr syn

1574+ <|> (do indentGt *> lchar '='

1575+ t <- indentGt *> expr syn

15811576 i <- get

15821577 return $ LetTac n (desugar syn i t)))

15831578

@@ -1628,7 +1623,7 @@ tactics =

16281623 i <- get

16291624 return $ tactic (desugar syn i t))

16301625 noArgs names tactic = (names, Nothing, const (return tactic))

1631− spaced parser = indentPropHolds gtProp *> parser

1626+ spaced parser = indentGt *> parser

16321627 imp :: IdrisParser Bool

16331628 imp = do lchar '?'; return False

16341629 <|> do lchar '_'; return True

src/Idris/Parser/Helpers.hs+12−37

@@ -408,17 +408,17 @@ invalidOperators :: [String]

408408invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]

409409

410410-- | Parses an operator

411−operator :: MonadicParsing m => m String

412−operator = do op <- token . some $ operatorLetter

413− when (op `elem` (invalidOperators ++ commentMarkers)) $

414− fail $ op ++ " is not a valid operator"

415− return op

411+symbolicOperator :: MonadicParsing m => m String

412+symbolicOperator = do op <- token . some $ operatorLetter

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

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

415+ return op

416416

417417-- | Parses an operator

418−operatorFC :: MonadicParsing m => m (String, FC)

419−operatorFC = do (FC f (l, c) _) <- getFC

420− op <- operator

421− return (op, FC f (l, c) (l, c + length op))

418+symbolicOperatorFC :: MonadicParsing m => m (String, FC)

419+symbolicOperatorFC = do (FC f (l, c) _) <- getFC

420+ op <- symbolicOperator

421+ return (op, FC f (l, c) (l, c + length op))

422422

423423{- * Position helpers -}

424424{- | Get filename from position (returns "(interactive)" when no source file is given) -}

@@ -590,36 +590,11 @@ notEndBlock = do ist <- get

590590 when (i < lvl || isParen) (fail "end of block")

591591 _ -> return ()

592592

593−-- | Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails

594−data IndentProperty = IndentProperty (Int -> Int -> Bool) String

595−

596−-- | Allows comparison of indent, and fails if property doesn't hold

597−indentPropHolds :: IndentProperty -> IdrisParser ()

598−indentPropHolds (IndentProperty op msg) = do

593+indentGt :: IdrisParser ()

594+indentGt = do

599595 li <- lastIndent

600596 i <- indent

601− when (not $ op i li) $ fail ("Wrong indention: " ++ msg)

602−

603−-- | Greater-than indent property

604−gtProp :: IndentProperty

605−gtProp = IndentProperty (>) "should be greater than context indentation"

606−

607−-- | Greater-than or equal to indent property

608−gteProp :: IndentProperty

609−gteProp = IndentProperty (>=) "should be greater than or equal context indentation"

610−

611−-- | Equal indent property

612−eqProp :: IndentProperty

613−eqProp = IndentProperty (==) "should be equal to context indentation"

614−

615−-- | Less-than indent property

616−ltProp :: IndentProperty

617−ltProp = IndentProperty (<) "should be less than context indentation"

618−

619−-- | Less-than or equal to indent property

620−lteProp :: IndentProperty

621−lteProp = IndentProperty (<=) "should be less than or equal to context indentation"

622−

597+ when (i <= li) $ fail "Wrong indention: should be greater than context indentation"

623598

624599-- | Checks that there are no braces that are not closed

625600notOpenBraces :: IdrisParser ()

src/Idris/Parser/Ops.hs+87−55

@@ -16,8 +16,10 @@ import Idris.Parser.Helpers

1616import Prelude hiding (pi)

1717

1818import Control.Applicative

19+import Control.Arrow (first)

1920import Control.Monad

2021import Control.Monad.State.Strict

22+import Data.Char (isAlpha)

2123import Data.List

2224import Text.Parser.Expression

2325import Text.Trifecta hiding (char, charLiteral, natural, span, string,

@@ -29,56 +31,85 @@ table :: [FixDecl] -> OperatorTable IdrisParser PTerm

2931table fixes

3032 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++

3133 toTable (reverse fixes) ++

32− [[backtick],

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

34− [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],

35− [nofixityoperator]]

34+ [[noFixityBacktickOperator],

35+ [binary "$" AssocRight $ \fc _ x y -> flatten $ PApp fc x [pexp y]],

36+ [binary "=" AssocLeft $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],

37+ [noFixityOperator]]

3638 where

37− flatten :: PTerm -> PTerm -- flatten application

39+ flatten :: PTerm -> PTerm -- flatten application

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

39− flatten t = t

40−

41−

42−-- | Calculates table for fixity declarations

43−toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

44−toTable fs = map (map toBin)

45− (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

46− where toBin (Fix (PrefixN _) op) = prefix op

47− (\fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x])

48− toBin (Fix f op)

49− = binary op (\fc x y -> PApp fc (PRef fc [] (sUN op)) [pexp x,pexp y]) (assoc f)

50− assoc (Infixl _) = AssocLeft

51− assoc (Infixr _) = AssocRight

52− assoc (InfixN _) = AssocNone

53−

54−-- | Binary operator

55−binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm

56−binary name f = Infix (do indentPropHolds gtProp

57− fc <- reservedOpFC name

58− indentPropHolds gtProp

59− return (f fc))

60−

61−-- | Prefix operator

62−prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm

63−prefix name f = Prefix (do reservedOp name

64− fc <- getFC

65− indentPropHolds gtProp

66− return (f fc))

67−

68−-- | Backtick operator

69−backtick :: Operator IdrisParser PTerm

70−backtick = Infix (do indentPropHolds gtProp

71− lchar '`'; (n, fc) <- fnName

72− lchar '`'

73− indentPropHolds gtProp

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

75−

76−-- | Operator without fixity (throws an error)

77−nofixityoperator :: Operator IdrisParser PTerm

78−nofixityoperator = Infix (do indentPropHolds gtProp

79− op <- try operator

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

41+ flatten t = t

42+

43+ noFixityBacktickOperator :: Operator IdrisParser PTerm

44+ noFixityBacktickOperator = flip Infix AssocNone $ do

45+ (n, fc) <- backtickOperator

46+ return $ \x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y]

47+

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

49+ noFixityOperator :: Operator IdrisParser PTerm

50+ noFixityOperator = flip Infix AssocNone $ do

51+ indentGt

52+ op <- try symbolicOperator

53+ unexpected $ "Operator without known fixity: " ++ op

54+

55+ -- | Calculates table for fixity declarations

56+ toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

57+ toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

58+

59+ toBin (Fix (PrefixN _) op) = prefix op $ \fc x ->

60+ PApp fc (PRef fc [] (sUN op)) [pexp x]

61+ toBin (Fix f op) = binary op (assoc f) $ \fc n x y ->

62+ PApp fc (PRef fc [] n) [pexp x,pexp y]

63+

64+ assoc (Infixl _) = AssocLeft

65+ assoc (Infixr _) = AssocRight

66+ assoc (InfixN _) = AssocNone

67+

68+ isBacktick :: String -> Bool

69+ isBacktick (c : _) = c == '_' || isAlpha c

70+ isBacktick _ = False

71+

72+ binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm

73+ binary name assoc f

74+ | isBacktick name = flip Infix assoc $ try $ do

75+ (n, fc) <- backtickOperator

76+ guard $ show (nsroot n) == name

77+ return $ f fc n

78+ | otherwise = flip Infix assoc $ do

79+ indentGt

80+ fc <- reservedOpFC name

81+ indentGt

82+ return $ f fc (sUN name)

83+

84+ prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm

85+ prefix name f = Prefix (do reservedOp name

86+ fc <- getFC

87+ indentGt

88+ return (f fc))

89+

90+{- | Parses a function used as an operator -- enclosed in backticks

8191

92+@

93+ BacktickOperator ::=

94+ '`' Name '`'

95+ ;

96+@

97+-}

98+backtickOperator :: IdrisParser (Name, FC)

99+backtickOperator = between (indentGt *> lchar '`') (indentGt *> lchar '`') name

100+

101+{- | Parses an operator name (either a symbolic name or a backtick-quoted name)

102+

103+@

104+ OperatorName ::=

105+ SymbolicOperator

106+ | BacktickOperator

107+ ;

108+@

109+-}

110+operatorName :: IdrisParser (Name, FC)

111+operatorName = first sUN <$> symbolicOperatorFC

112+ <|> backtickOperator

82113

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

84115 optional namespace

@@ -96,7 +127,7 @@ operatorFront = try (do (FC f (l, c) _) <- getFC

96127 op <- lchar '(' *> reservedOp "=" <* lchar ')'

97128 return (eqTy, FC f (l, c) (l, c+3)))

98129 <|> maybeWithNS (do (FC f (l, c) _) <- getFC

99− op <- lchar '(' *> operator

130+ op <- lchar '(' *> symbolicOperator

100131 (FC _ _ (l', c')) <- getFC

101132 lchar ')'

102133 return (op, (FC f (l, c) (l', c' + 1)))) False []

@@ -120,7 +151,7 @@ Fixity ::=

120151fixity :: IdrisParser PDecl

121152fixity = do pushIndent

122153 f <- fixityType; i <- fst <$> natural;

123− ops <- sepBy1 operator (lchar ',')

154+ ops <- sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

124155 terminator

125156 let prec = fromInteger i

126157 istate <- get

@@ -137,14 +168,15 @@ fixity = do pushIndent

137168 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""

138169 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill

139170 <?> "fixity declaration"

140− where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

141− alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

171+ where

172+ alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

173+ alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

142174

143− checkValidity :: (FixDecl, [FixDecl]) -> Bool

144− checkValidity (f, fs) = all (== f) fs

175+ checkValidity :: (FixDecl, [FixDecl]) -> Bool

176+ checkValidity (f, fs) = all (== f) fs

145177

146− extractName :: FixDecl -> String

147− extractName (Fix _ n) = n

178+ extractName :: FixDecl -> String

179+ extractName (Fix _ n) = n

148180

149181-- | Check that a declaration of an operator also has fixity declared

150182checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl

src/Idris/REPL/Parser.hs+1−1

@@ -234,7 +234,7 @@ exprArg cmd name = do

234234 return $ Left ("Usage is :" ++ name ++ " <expression>")

235235

236236 let justOperator = do

237− (op, fc) <- P.operatorFC

237+ (op, fc) <- P.symbolicOperatorFC

238238 eof

239239 return $ Right $ cmd (PRef fc [] (sUN op))

240240

test/basic023/expected+3

@@ -5,3 +5,6 @@ True

55True

66True

77True

8+True

9+True

10+True

test/basic023/sections.idr+13

@@ -1,9 +1,19 @@

11postInc : Nat -> Nat

22postInc = (`plus` 1)

4+infixr 8 `cons`

45cons : Int -> List Int -> List Int

56cons = (::)

8+namespace A

9+ infixr 8 `nmul`

10+ nmul : Nat -> Nat -> Nat

11+ nmul = (*)

12+

13+namespace B

14+ nmul : Nat -> Nat -> Nat

15+ nmul _ y = y

16+

717prefix 1 :/

818(:/) : Nat -> Nat

919(:/) = (1 `plus`)

@@ -19,3 +29,6 @@ main = do

1929 let io : IO Integer = pure 9

2030 printLn $ (! io) == 9 -- prefix, not section

2131 printLn $ (:/ 3) == 4 -- custom prefix operator (#2571)

32+ printLn $ 1 `cons` 2 `cons` [3] == [1,2,3]

33+ printLn $ 2 `A.nmul` 3 `B.nmul` 5 == 10

34+ printLn $ 2 `B.nmul` 3 `A.nmul` 5 == 15