git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4121 from eraserhd/prefix-sections

Exclude custom prefix operators from sections

commitd6be6210f0e376b8824bff45ef2ee0fa93f02bfa authorAhmad Salim Al-Sibahi <asal@itu.dk> dateFri 13 Oct 2017, 09:02 (9 years ago) parent19624c7e10b6f6
3 files changed+20−5
compare with master
unifiedsplit
src/Idris/Parser/Expr.hs+14−2 test/basic023/expected+1 test/basic023/sections.idr+5−3
src/Idris/Parser/Expr.hs+14−2
@@ -470,8 +470,8 @@ bracketed' open syn =
470470 <|> try (dependentPair TypeOrTerm [] open syn)
471471 <|> try (do fc <- getFC
472472 opName <- operatorName
473− -- No prefix operators! (bit of a hack here...)
474− guard $ opName /= sUN "-" && opName /= sUN "!"
473+ guardNotPrefix opName
474+
475475 e <- expr syn
476476 lchar ')'
477477 return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
@@ -492,6 +492,18 @@ bracketed' open syn =
492492 operatorName = sUN <$> operator
493493 <|> fst <$> between (lchar '`') (lchar '`') fnName
494494
495+ justPrefix :: FixDecl -> Maybe Name
496+ justPrefix (Fix (PrefixN _) opName) = Just (sUN opName)
497+ justPrefix _ = Nothing
498+
499+ guardNotPrefix :: Name -> IdrisParser ()
500+ guardNotPrefix opName = do
501+ guard $ opName /= sUN "-"
502+ guard $ opName /= sUN "!"
503+
504+ ops <- idris_infixes <$> get
505+ guard . not . (opName `elem`) . mapMaybe justPrefix $ ops
506+
495507{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
496508dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
497509dependentPair pun prev openFC syn =
test/basic023/expected+1
@@ -4,3 +4,4 @@ True
44True
55True
66True
7+True
test/basic023/sections.idr+5−3
@@ -1,12 +1,13 @@
1−preInc : Nat -> Nat
2−preInc = (1 `plus`)
3−
41postInc : Nat -> Nat
52postInc = (`plus` 1)
63
74cons : Int -> List Int -> List Int
85cons = (::)
96
7+prefix 1 :/
8+(:/) : Nat -> Nat
9+(:/) = (1 `plus`)
10+
1011main : IO ()
1112main = do
1213 printLn $ (1 `cons`) [2] == [1,2]
@@ -17,3 +18,4 @@ main = do
1718 printLn $ (- x) == -4 -- prefix, not section
1819 let io : IO Integer = pure 9
1920 printLn $ (! io) == 9 -- prefix, not section
21+ printLn $ (:/ 3) == 4 -- custom prefix operator (#2571)