Support backticked operators in sections

CHANGELOG.md

@@ -8,6 +8,8 @@
 + The `LinearTypes` language extension has been revised. It implements the
   rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative
   Type Theory" and now works with holes and case expressions.
++ Backticked operators can appear in sections, e.g. `(\`LTE\` 42)` or
+  `(1 \`plus\`)`.
 
 ## Library Updates
 

CONTRIBUTORS

@@ -107,6 +107,7 @@ Jan de Muijnck-Hughes
 Jan Doms
 Jan Stolarek
 Jason Dagit
+Jason Felice
 Jason Gross
 Jean-Remi Desjardins
 Jeff Hemphill

src/Idris/Parser/Expr.hs

@@ -468,27 +468,29 @@ bracketed' open syn =
                lchar ')'
                return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
         <|> try (dependentPair TypeOrTerm [] open syn)
-        <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
+        <|> try (do fc <- getFC
+                    opName <- operatorName
                     -- No prefix operators! (bit of a hack here...)
-                    if (o == "-" || o == "!")
-                      then fail "minus not allowed in section"
-                      else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
-                         (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),
-                                                        pexp e]))
-        <|> try (do l <- simpleExpr syn
-                    op <- option Nothing (do o <- operator
-                                             lchar ')'
-                                             return (Just o))
-                    fc0 <- getFC
-                    case op of
-                         Nothing -> bracketedExpr syn open l
-                         Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder
-                             (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,
-                                                              pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
+                    guard $ opName /= sUN "-" && opName /= sUN "!"
+                    e <- expr syn
+                    lchar ')'
+                    return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
+                      (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),
+                                                    pexp e]))
+        <|> try (simpleExpr syn >>= \l ->
+                     try (do opName <- operatorName
+                             lchar ')'
+                             fc <- getFC
+                             return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
+                               (PApp fc (PRef fc [] opName) [pexp l,
+                                                             pexp (PRef fc [] (sMN 1000 "ARG"))]))
+                 <|> bracketedExpr syn open l)
         <|> do l <- expr (allowConstr syn)
                bracketedExpr (allowConstr syn) open l
-
-
+  where
+    operatorName :: IdrisParser Name
+    operatorName =     sUN <$> operator
+                   <|> fst <$> between (lchar '`') (lchar '`') fnName
 
 {-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
 dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

test/TestData.hs

@@ -52,28 +52,29 @@ testFamiliesData = [
   ("base",            "Base",
     [ (  1, C_CG )]),
   ("basic",           "Basic",
-    [ (  1, ANY  ),
-      (  2, ANY  ),
-      (  3, ANY  ),
-      (  4, ANY  ),
-      (  5, ANY  ),
-      (  6, ANY  ),
-      (  7, C_CG ),
-      (  8, ANY  ),
-      (  9, ANY  ),
-      ( 10, ANY  ),
-      ( 11, C_CG ),
-      ( 12, ANY  ),
-      ( 13, ANY  ),
-      ( 14, ANY  ),
-      ( 15, ANY  ),
-      ( 16, ANY  ),
-      ( 17, ANY  ),
-      ( 18, ANY  ),
-      ( 19, ANY  ),
-      ( 20, ANY  ),
-      ( 21, C_CG  ),
-      ( 22, NODE_CG  )]),
+    [ (  1, ANY     ),
+      (  2, ANY     ),
+      (  3, ANY     ),
+      (  4, ANY     ),
+      (  5, ANY     ),
+      (  6, ANY     ),
+      (  7, C_CG    ),
+      (  8, ANY     ),
+      (  9, ANY     ),
+      ( 10, ANY     ),
+      ( 11, C_CG    ),
+      ( 12, ANY     ),
+      ( 13, ANY     ),
+      ( 14, ANY     ),
+      ( 15, ANY     ),
+      ( 16, ANY     ),
+      ( 17, ANY     ),
+      ( 18, ANY     ),
+      ( 19, ANY     ),
+      ( 20, ANY     ),
+      ( 21, C_CG    ),
+      ( 22, NODE_CG ),
+      ( 23, ANY     )]),
   ("bignum",          "Bignum",
     [ (  1, ANY  ),
       (  2, ANY  )]),

test/basic023/expected

@@ -0,0 +1,6 @@
+True
+True
+True
+True
+True
+True

test/basic023/run

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ sections.idr -o sections
+./sections
+rm -f sections *.ibc

test/basic023/sections.idr

@@ -0,0 +1,19 @@
+preInc : Nat -> Nat
+preInc = (1 `plus`)
+
+postInc : Nat -> Nat
+postInc = (`plus` 1)
+
+cons : Int -> List Int -> List Int
+cons = (::)
+
+main : IO ()
+main = do
+  printLn $ (1 `cons`) [2] == [1,2]
+  printLn $ (1 ::) [2]     == [1,2]
+  printLn $ (`cons` [2]) 1 == [1,2]
+  printLn $ (:: [2]) 1     == [1,2]
+  let x : Integer = 4
+  printLn $ (- x) == -4         -- prefix, not section
+  let io : IO Integer = pure 9
+  printLn $ (! io) == 9         -- prefix, not section