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

git.iko.soy/Idris-dev

on master help sign in

Allow declaring fixity of ticked operators (#4140)

13308b1Jason Felice9 years ago

CHANGELOG.md+6−2

compare with master

unifiedsplit

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

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

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

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

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

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

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

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.

14## Library Updates

18## Library Updates

src/Idris/Parser.hs+3−3

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

1086-}

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

1088rhs syn n = do lchar '='

1089− indentPropHolds gtProp

1089+ indentGt

1090 expr syn

1091 <|> do symbol "?=";

1092 fc <- getFC

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

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

1182 pushIndent

1183 l <- argExpr syn

1184− (op, nfc) <- operatorFC

1184+ (op, nfc) <- symbolicOperatorFC

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

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

1187 return (l, op, nfc))

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

1533 t <- spaced (expr defaultSyntax)

1534 i <- get

1535 return $ tactic (desugar defaultSyntax i t)

1536− spaced parser = indentPropHolds gtProp *> parser

1536+ spaced parser = indentGt *> parser

1537

1538-- | Parse module header and imports

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

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

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

468 lchar ')'

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

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

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

472− opName <- operatorName

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

473 guardNotPrefix opName

472 guardNotPrefix opName

474

473

475 e <- expr syn

474 e <- expr syn

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

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

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

479 pexp e]))

478 pexp e]))

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

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

481− try (do opName <- operatorName

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

482 lchar ')'

481 lchar ')'

483 fc <- getFC

482 fc <- getFC

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

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

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

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

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

489 bracketedExpr (allowConstr syn) open l

488 bracketedExpr (allowConstr syn) open l

490 where

489 where

491− operatorName :: IdrisParser Name

492− operatorName = sUN <$> operator

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

494−

495 justPrefix :: FixDecl -> Maybe Name

490 justPrefix :: FixDecl -> Maybe Name

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

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

497 justPrefix _ = Nothing

492 justPrefix _ = Nothing

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

1558 imps <- many imp

1553 imps <- many imp

1559 return $ Refine n imps)

1554 return $ Refine n imps)

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

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

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

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

1562− goal <- indentPropHolds gtProp *> expr syn

1557+ goal <- indentGt *> expr syn

1563 return $ Claim n goal)

1558 return $ Claim n goal)

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

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

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

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

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

1569 , expressionTactic ["induction"] Induction

1564 , expressionTactic ["induction"] Induction

1570 , expressionTactic ["equiv"] Equiv

1565 , expressionTactic ["equiv"] Equiv

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

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

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

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

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

1568+ (do indentGt *> lchar ':'

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

1569+ ty <- indentGt *> expr' syn

1575− indentPropHolds gtProp *> lchar '='

1570+ indentGt *> lchar '='

1576− t <- indentPropHolds gtProp *> expr syn

1571+ t <- indentGt *> expr syn

1577 i <- get

1572 i <- get

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

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

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

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

1580− t <- indentPropHolds gtProp *> expr syn

1575+ t <- indentGt *> expr syn

1581 i <- get

1576 i <- get

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

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

1583

1578

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

1628 i <- get

1623 i <- get

1629 return $ tactic (desugar syn i t))

1624 return $ tactic (desugar syn i t))

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

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

1631− spaced parser = indentPropHolds gtProp *> parser

1626+ spaced parser = indentGt *> parser

1632 imp :: IdrisParser Bool

1627 imp :: IdrisParser Bool

1633 imp = do lchar '?'; return False

1628 imp = do lchar '?'; return False

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

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

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

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

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

409

410-- | Parses an operator

411−operator :: MonadicParsing m => m String

411+symbolicOperator :: MonadicParsing m => m String

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

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

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

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

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

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

415− return op

415+ return op

416

417-- | Parses an operator

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

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

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

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

420− op <- operator

420+ op <- symbolicOperator

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

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

422

423{- * Position helpers -}

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

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

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

591 _ -> return ()

592

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

593+indentGt :: IdrisParser ()

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

594+indentGt = do

595−

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

597−indentPropHolds :: IndentProperty -> IdrisParser ()

598−indentPropHolds (IndentProperty op msg) = do

599 li <- lastIndent

595 li <- lastIndent

600 i <- indent

596 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"

597+ when (i <= li) $ fail "Wrong indention: 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−

623

598

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

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

625notOpenBraces :: IdrisParser ()

600notOpenBraces :: IdrisParser ()

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

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

16import Prelude hiding (pi)

18import Control.Applicative

19+import Control.Arrow (first)

19import Control.Monad

20import Control.Monad

20import Control.Monad.State.Strict

21import Control.Monad.State.Strict

22+import Data.Char (isAlpha)

21import Data.List

23import Data.List

22import Text.Parser.Expression

24import Text.Parser.Expression

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

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

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

29table fixes

31table fixes

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

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

31 toTable (reverse fixes) ++

33 toTable (reverse fixes) ++

32− [[backtick],

34+ [[noFixityBacktickOperator],

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

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

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

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

35− [nofixityoperator]]

37+ [noFixityOperator]]

36 where

38 where

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

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

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

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

39− flatten t = t

41+ flatten t = t

40−

42+

41−

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+

42−-- | Calculates table for fixity declarations

55+ -- | Calculates table for fixity declarations

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

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

44−toTable fs = map (map toBin)

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

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

58+

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

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

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

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

48− toBin (Fix f op)

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

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

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

63+

50− assoc (Infixl _) = AssocLeft

64+ assoc (Infixl _) = AssocLeft

51− assoc (Infixr _) = AssocRight

65+ assoc (Infixr _) = AssocRight

52− assoc (InfixN _) = AssocNone

66+ assoc (InfixN _) = AssocNone

53−

67+

54−-- | Binary operator

68+ isBacktick :: String -> Bool

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

70+ isBacktick _ = False

71+

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

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

56−binary name f = Infix (do indentPropHolds gtProp

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

57− fc <- reservedOpFC name

80+ fc <- reservedOpFC name

58− indentPropHolds gtProp

81+ indentGt

59− return (f fc))

82+ return $ f fc (sUN name)

60−

83+

61−-- | Prefix operator

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

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

63−prefix name f = Prefix (do reservedOp name

85+ prefix name f = Prefix (do reservedOp name

64− fc <- getFC

86+ fc <- getFC

65− indentPropHolds gtProp

87+ indentGt

66− return (f fc))

88+ return (f fc))

67−

89+

68−-- | Backtick operator

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

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

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

113

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

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

84 optional namespace

115 optional namespace

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

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

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

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

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

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

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

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

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

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

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

101 lchar ')'

132 lchar ')'

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

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

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

120fixity :: IdrisParser PDecl

151fixity :: IdrisParser PDecl

121fixity = do pushIndent

152fixity = do pushIndent

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

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

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

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

124 terminator

155 terminator

125 let prec = fromInteger i

156 let prec = fromInteger i

126 istate <- get

157 istate <- get

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

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

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

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

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

139 <?> "fixity declaration"

170 <?> "fixity declaration"

171+ where

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

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

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

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

142

174

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

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

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

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

145

177

146− extractName :: FixDecl -> String

178+ extractName :: FixDecl -> String

147− extractName (Fix _ n) = n

179+ extractName (Fix _ n) = n

148

180

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

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

150checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl

182checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl

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

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

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

235

236 let justOperator = do

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

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

238 eof

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

240

test/basic023/expected+3

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

5True

6True

7True

8+True

9+True

10+True

test/basic023/sections.idr+13

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

1postInc : Nat -> Nat

2postInc = (`plus` 1)

4+infixr 8 `cons`

4cons : Int -> List Int -> List Int

5cons : Int -> List Int -> List Int

5cons = (::)

6cons = (::)

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+

7prefix 1 :/

17prefix 1 :/

8(:/) : Nat -> Nat

18(:/) : Nat -> Nat

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

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

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

19 let io : IO Integer = pure 9

29 let io : IO Integer = pure 9

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

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

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

31 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