git.iko.soy/Idris-dev
on master help sign in
Support backticked operators in sections (#4119)

* Postfix sections for ticked ops, e.g. (1 `plus`) and prefix sections for ticked ops, e.g. (`plus` 1)

commit19624c7e1966615312328e0e05f5888b85bbfca8 authorJason Felice <jason.m.felice@gmail.com> dateThu 12 Oct 2017, 13:51 (9 years ago) parentecc97b5
7 files changed+75−40
compare with master
unifiedsplit
CHANGELOG.md+2 CONTRIBUTORS+1 src/Idris/Parser/Expr.hs+20−18 test/TestData.hs+23−22 test/basic023/expected+6 test/basic023/run+4 test/basic023/sections.idr+19
CHANGELOG.md+2
@@ -8,6 +8,8 @@
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\`)`.
1113
1214## Library Updates
1315
CONTRIBUTORS+1
@@ -107,6 +107,7 @@ Jan de Muijnck-Hughes
107107Jan Doms
108108Jan Stolarek
109109Jason Dagit
110+Jason Felice
110111Jason Gross
111112Jean-Remi Desjardins
112113Jeff Hemphill
src/Idris/Parser/Expr.hs+20−18
@@ -468,27 +468,29 @@ 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; o <- operator; e <- expr syn; lchar ')'
471+ <|> try (do fc <- getFC
472+ opName <- operatorName
472473 -- No prefix operators! (bit of a hack here...)
473− if (o == "-" || o == "!")
474− then fail "minus not allowed in section"
475− else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
476− (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),
477− pexp e]))
478− <|> try (do l <- simpleExpr syn
479− op <- option Nothing (do o <- operator
480− lchar ')'
481− return (Just o))
482− fc0 <- getFC
483− case op of
484− Nothing -> bracketedExpr syn open l
485− Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder
486− (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,
487− pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
474+ guard $ opName /= sUN "-" && opName /= sUN "!"
475+ e <- expr syn
476+ lchar ')'
477+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
478+ (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),
479+ pexp e]))
480+ <|> try (simpleExpr syn >>= \l ->
481+ try (do opName <- operatorName
482+ lchar ')'
483+ fc <- getFC
484+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
485+ (PApp fc (PRef fc [] opName) [pexp l,
486+ pexp (PRef fc [] (sMN 1000 "ARG"))]))
487+ <|> bracketedExpr syn open l)
488488 <|> do l <- expr (allowConstr syn)
489489 bracketedExpr (allowConstr syn) open l
490−
491−
490+ where
491+ operatorName :: IdrisParser Name
492+ operatorName = sUN <$> operator
493+ <|> fst <$> between (lchar '`') (lchar '`') fnName
492494
493495{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
494496dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
test/TestData.hs+23−22
@@ -52,28 +52,29 @@ testFamiliesData = [
5252 ("base", "Base",
5353 [ ( 1, C_CG )]),
5454 ("basic", "Basic",
55− [ ( 1, ANY ),
56− ( 2, ANY ),
57− ( 3, ANY ),
58− ( 4, ANY ),
59− ( 5, ANY ),
60− ( 6, ANY ),
61− ( 7, C_CG ),
62− ( 8, ANY ),
63− ( 9, ANY ),
64− ( 10, ANY ),
65− ( 11, C_CG ),
66− ( 12, ANY ),
67− ( 13, ANY ),
68− ( 14, ANY ),
69− ( 15, ANY ),
70− ( 16, ANY ),
71− ( 17, ANY ),
72− ( 18, ANY ),
73− ( 19, ANY ),
74− ( 20, ANY ),
75− ( 21, C_CG ),
76− ( 22, NODE_CG )]),
55+ [ ( 1, ANY ),
56+ ( 2, ANY ),
57+ ( 3, ANY ),
58+ ( 4, ANY ),
59+ ( 5, ANY ),
60+ ( 6, ANY ),
61+ ( 7, C_CG ),
62+ ( 8, ANY ),
63+ ( 9, ANY ),
64+ ( 10, ANY ),
65+ ( 11, C_CG ),
66+ ( 12, ANY ),
67+ ( 13, ANY ),
68+ ( 14, ANY ),
69+ ( 15, ANY ),
70+ ( 16, ANY ),
71+ ( 17, ANY ),
72+ ( 18, ANY ),
73+ ( 19, ANY ),
74+ ( 20, ANY ),
75+ ( 21, C_CG ),
76+ ( 22, NODE_CG ),
77+ ( 23, ANY )]),
7778 ("bignum", "Bignum",
7879 [ ( 1, ANY ),
7980 ( 2, ANY )]),
test/basic023/expectednew file+6
@@ -0,0 +1,6 @@
1+True
2+True
3+True
4+True
5+True
6+True
test/basic023/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ sections.idr -o sections
3+./sections
4+rm -f sections *.ibc
test/basic023/sections.idrnew file+19
@@ -0,0 +1,19 @@
1+preInc : Nat -> Nat
2+preInc = (1 `plus`)
3+
4+postInc : Nat -> Nat
5+postInc = (`plus` 1)
6+
7+cons : Int -> List Int -> List Int
8+cons = (::)
9+
10+main : IO ()
11+main = do
12+ printLn $ (1 `cons`) [2] == [1,2]
13+ printLn $ (1 ::) [2] == [1,2]
14+ printLn $ (`cons` [2]) 1 == [1,2]
15+ printLn $ (:: [2]) 1 == [1,2]
16+ let x : Integer = 4
17+ printLn $ (- x) == -4 -- prefix, not section
18+ let io : IO Integer = pure 9
19+ printLn $ (! io) == 9 -- prefix, not section