[ Operator parser ] Fixed a long-standing operator fixity bug.

With this fix in place operator parsing takes perhaps 25% more time
for the standard library (the difference is roughly two seconds with
my current setup).

doc/release-notes/2-4-4.txt

@@ -46,6 +46,51 @@ Pragmas and options
 Language
 ========
 
+* A long-standing operator fixity bug has been fixed. As a consequence
+  some programs that used to parse no longer do.
+
+  Previously each precedence level was (incorrectly) split up into
+  five separate ones, ordered as follows, with the earlier ones
+  binding less tightly than the later ones:
+
+    - Non-associative operators.
+
+    - Left associative operators.
+
+    - Right associative operators.
+
+    - Prefix operators.
+
+    - Postfix operators.
+
+  Now this problem has been addressed. It is no longer possible to mix
+  operators of a given precedence level but different associativity.
+  However, prefix and right associative operators are seen as having
+  the same associativity, and similarly for postfix and left
+  associative operators.
+
+  Examples
+  --------
+
+  The following code is no longer accepted:
+
+    infixl 6 _+_
+    infix  6 _∸_
+
+    rejected : ℕ
+    rejected = 1 + 0 ∸ 1
+
+  However, the following previously rejected code is accepted:
+
+    infixr 4 _,_
+    infix  4 ,_
+
+    ,_ : {A : Set} {B : A → Set} {x : A} → B x → Σ A B
+    , y = _ , y
+
+    accepted : Σ ℕ λ i → Σ ℕ λ j → Σ (i ≡ j) λ _ → Σ ℕ λ k → j ≡ k
+    accepted = 5 , , refl , , refl
+
 * Building records from modules.
 
   The "record { <fields> }" syntax is now extended to accept module names as

examples/ParenDepTac.agda

@@ -47,9 +47,9 @@ data Parens : Set where
 infixr 5 _·_
 
 _·_ : Parens -> Parens -> Parens
-ε    · ys = ys
-≪ xs · ys = ≪ (xs · ys)
-≫ xs · ys = ≫ (xs · ys)
+ε      · ys = ys
+(≪ xs) · ys = ≪ (xs · ys)
+(≫ xs) · ys = ≫ (xs · ys)
 
 ·ass : (xs : Parens){ys zs : Parens} -> xs · (ys · zs) ≡ (xs · ys) · zs
 ·ass ε      = refl
@@ -232,4 +232,3 @@ complete xs0 p0 = parse init εS xs0 p0
 
   parse init       _ (≫ zs) ()
   parse init       s ε      tt = subst _∈S ·unitR s
-

examples/Termination/StreamEating.agda

@@ -36,7 +36,7 @@ data SP (A B : Set) : Set where
 -- and an inner recursion on SP A B
 eat : ∀ {A B} → SP A B → Stream A → Stream B
 eat (get f)    (a ∷ as) = eat (f a) (♭ as)
-eat (put b sp) as       = b ∷ ♯ eat (♭ sp) as
+eat (put b sp) as       = b ∷ (♯ eat (♭ sp) as)
 
 _∘_ : ∀ {A B C} → SP B C → SP A B → SP A C
 get f₁    ∘ put x sp₂ = f₁ x ∘ ♭ sp₂

examples/lib/Logic/ChainReasoning.agda

@@ -10,7 +10,7 @@ module Mono where
     (trans : (x y z : A) -> x == y -> y == z -> x == z)
     where
 
-    infix 2 chain>_
+    infix 3 chain>_
     infixl 2 _===_
     infix 3 _by_
 
@@ -31,7 +31,7 @@ module Poly where
     (trans : {A : Set}(x y z : A) -> x == y -> y == z -> x == z)
     where
 
-    infix 2 chain>_
+    infix 3 chain>_
     infixl 2 _===_
     infix 3 _by_
 
@@ -50,7 +50,7 @@ module Poly where
     (trans : {A B C : Set}(x : A)(y : B)(z : C) -> x == y -> y == z -> x == z)
     where
 
-    infix 2 chain>_
+    infix 3 chain>_
     infixl 2 _===_
     infix 3 _by_
 
@@ -69,7 +69,7 @@ module Poly where
     (trans : {A B C : Set1}(x : A)(y : B)(z : C) -> x == y -> y == z -> x == z)
     where
 
-    infix 2 chain>_
+    infix 3 chain>_
     infixl 2 _===_
     infix 3 _by_
 
@@ -81,4 +81,3 @@ module Poly where
 
     _by_ : {A B : Set1}{x : A}(y : B) -> x == y -> x == y
     y by eq = eq
-

examples/tactics/ac/EqProof.agda

@@ -6,7 +6,7 @@ module EqProof
   (trans : {x y z : A} -> x == y -> y == z -> x == z)
   where
 
-  infix 2 eqProof>_
+  infix 3 eqProof>_
   infixl 2 _===_
   infix 3 _by_
 
@@ -18,4 +18,3 @@ module EqProof
 
   _by_ : {x : A}(y : A) -> x == y -> x == y
   y by eq = eq
-

src/full/Agda/Syntax/Concrete/Operators.hs

@@ -143,26 +143,6 @@ data UseBoundNames = UseBoundNames | DontUseBoundNames
     The effect is that operator parts (that are not constructor parts)
     can be used as atomic names in the pattern (so they can be
     rebound). See test/succeed/OpBind.agda for an example.
-
-    To avoid problems with operators of the same precedence but different
-    associativity we decide (completely arbitrary) to fix the precedences of
-    operators with the same given precedence in the following order (from
-    loosest to hardest):
-
-    - non-associative
-
-    - left associative
-
-    - right associative
-
-    - prefix
-
-    - postfix
-
-    This has the effect that if you mix operators with the same precedence but
-    different associativity the parser won't complain. One could argue that
-    this is a Bad Thing, but since it's not trivial to implement the check it
-    will stay this way until people start complaining about it.
 -}
 buildParsers :: forall e. IsExpr e => Range -> FlatScope -> UseBoundNames -> ScopeM (Parsers e)
 buildParsers r flat use = do
@@ -187,7 +167,7 @@ buildParsers r flat use = do
     let chain = foldr ( $ )
 
     return $ Data.Function.fix $ \p -> Parsers
-        { pTop    = chain (pApp p) (concatMap (mkP (pTop p)) (order fix))
+        { pTop    = chain (pApp p) (map (mkP (pTop p)) (order fix))
         , pApp    = appP (pNonfix p) (pArgs p)
         , pArgs   = argsP (pNonfix p)
         , pNonfix = chain (pAtom p) (map (nonfixP . opP (pTop p)) non)
@@ -219,27 +199,42 @@ buildParsers r flat use = do
         order :: [NewNotation] -> [[NewNotation]]
         order = groupBy ((==) `on` level) . sortBy (compare `on` level)
 
-        -- | Each element of the returned list takes the parser for an
-        -- expression of higher precedence as parameter.
-        mkP :: Parser e e -> [NewNotation] -> [Parser e e -> Parser e e]
-        mkP p0 ops = case concat [infx, inlfx, inrfx, prefx, postfx] of
-            []      -> [id]
-            fs      -> fs
+        mkP :: Parser e e
+            -> [NewNotation]
+            -> Parser e e
+               -- ^ A parser for an expression of higher precedence.
+            -> Parser e e
+        mkP p0 []           higher = __IMPOSSIBLE__
+        mkP p0 ops@(op : _) higher =
+            memoise (Node (level op)) $
+              Fold.asum [higher, nonAssoc, preRights, postLefts]
             where
-                inlfx   = fixP infixlP  isinfixl
-                inrfx   = fixP infixrP  isinfixr
-                infx    = fixP infixP   isinfix
-                prefx   = fixP prefixP  isprefix
-                postfx  = fixP postfixP ispostfix
-
-                fixP :: (Parser e (NewNotation,Range,[e]) ->
-                           Parser e e -> Parser e e) ->
-                        (NewNotation -> Bool) ->
-                        [Parser e e -> Parser e e]
-                fixP f g =
-                    case filter g ops of
-                        []  -> []
-                        ops -> [ f $ Fold.asum $ map (opP p0) ops ]
+            choice f = Fold.asum . map (f . opP p0)
+
+            nonAssoc = do
+              x <- higher
+              f <- choice binop (filter isinfix ops)
+              y <- higher
+              return (f x y)
+
+            preRight =
+              choice preop (filter isprefix ops)
+              <|>
+              flip ($) <$> higher
+                       <*> choice binop (filter isinfixr ops)
+
+            preRights =
+              preRight <*> (preRights <|> higher)
+
+            postLeft =
+              choice postop (filter ispostfix ops)
+              <|>
+              flip <$> choice binop (filter isinfixl ops)
+                   <*> higher
+
+            postLefts =
+              memoise (PostLefts (level op)) $
+                flip ($) <$> (postLefts <|> higher) <*> postLeft
 
 
 ---------------------------------------------------------------------------

src/full/Agda/Syntax/Concrete/Operators/Parser.hs

@@ -1,13 +1,17 @@
 {-# LANGUAGE CPP                 #-}
+{-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module Agda.Syntax.Concrete.Operators.Parser where
 
 import Control.Applicative
 import Control.Exception (throw)
 
+import Data.Hashable
 import Data.Maybe
 
+import GHC.Generics (Generic)
+
 import Agda.Syntax.Position
 import Agda.Syntax.Common hiding (Arg, Dom, NamedArg)
 import Agda.Syntax.Fixity
@@ -21,7 +25,12 @@ import Agda.Utils.Monad
 #include "undefined.h"
 import Agda.Utils.Impossible
 
-type Parser tok a = MemoisedCPS.Parser () tok tok a
+data MemoKey = Node Integer | PostLefts Integer
+  deriving (Eq, Generic)
+
+instance Hashable MemoKey
+
+type Parser tok a = MemoisedCPS.Parser MemoKey tok tok a
 
 data ExprView e
     = LocalV QName
@@ -129,32 +138,12 @@ rebuildBinding (WildV e) =
   DomainFree defaultArgInfo $ mkBoundName_ $ Name noRange [Hole]
 rebuildBinding e = throw $ Exception (getRange e) "Expected variable name in binding position"
 
--- | Parse using the appropriate fixity, given a parser parsing the
--- operator part, the name of the operator, and a parser of
+-- | Parse a \"nonfix\" operator application, given a parser parsing
+-- the operator part, the name of the operator, and a parser of
 -- subexpressions.
-infixP, infixrP, infixlP, postfixP, prefixP,nonfixP ::
+nonfixP ::
   IsExpr e =>
   Parser e (NewNotation,Range,[e]) -> Parser e e -> Parser e e
-prefixP op p = do
-    fs <- many (preop op)
-    e  <- p
-    return $ foldr ( $ ) e fs
-
-postfixP op p = do
-    e <- p
-    fs <- many (postop op)
-    return $ foldl (flip ( $ )) e fs
-
-infixlP op p = chainl1 p (binop op)
-infixrP op p = chainr1 p (binop op)
-infixP  op p = do
-    e <- p
-    restP e
-    where
-        restP x = return x <|> do
-            f <- binop op
-            f x <$> p
-
 nonfixP op p = do
   (nsyn,r,es) <- op
   return $ rebuild nsyn r es

test/fail/Issue147a.err

@@ -1,5 +1,5 @@
 Issue147a.agda:10,9-12
 Don't know how to parse f x. Could mean any one of:
-  f_ x
   f x
+  f_ x
 when scope checking f x

test/fail/Issue147b.err

@@ -1,6 +1,6 @@
 Issue147b.agda:10,1-10
 Don't know how to parse bad (f x). Could mean any one of:
-  bad (f_ x)
   bad (f x)
+  bad (f_ x)
 when scope checking the left-hand side bad (f x) in the definition
 of bad

test/fail/Same-Precedence-Different-Associativity.agda

@@ -0,0 +1,20 @@
+data ℕ : Set where
+  zero : ℕ
+  suc  : ℕ → ℕ
+
+{-# BUILTIN NATURAL ℕ #-}
+
+infixl 6 _+_
+infix  6 _∸_
+
+_+_ : ℕ → ℕ → ℕ
+zero  + n = n
+suc m + n = suc (m + n)
+
+_∸_ : ℕ → ℕ → ℕ
+m     ∸ zero  = m
+zero  ∸ suc n = zero
+suc m ∸ suc n = m ∸ n
+
+should-be-rejected : ℕ
+should-be-rejected = 1 + 0 ∸ 1

test/fail/Same-Precedence-Different-Associativity.err

@@ -0,0 +1,3 @@
+Same-Precedence-Different-Associativity.agda:20,22-31
+Could not parse the application 1 + 0 ∸ 1
+when scope checking 1 + 0 ∸ 1

test/interaction/Issue1060.agda

@@ -26,7 +26,7 @@ sym refl = refl
 trans : ∀ {a}{A : Set a}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans refl refl = refl
 
-infix  2 _∎
+infix  3 _∎
 infixr 2 _≡⟨_⟩_
 infix  1 begin_
 

test/lib-succeed/Issue784/Values.agda

@@ -132,7 +132,7 @@ NonRepetitiveTypes ℓ = Σ[ t ∈ Types ℓ ] NonRepetitiveNames t
 
 ∪-assoc : ∀ {l} {A : Set l} (x y z : List A) → (x ∪ y) ∪ z ≡ x ∪ (y ∪ z)
 ∪-assoc [] y z = refl
-∪-assoc (x ∷ xs) y z = ≡-elim′ (λ e → x ∷ e ≡ x ∷ xs ∪ (y ∪ z)) (≡-sym $ ∪-assoc xs y z) refl
+∪-assoc (x ∷ xs) y z = ≡-elim′ (λ e → x ∷ e ≡ (x ∷ xs) ∪ (y ∪ z)) (≡-sym $ ∪-assoc xs y z) refl
 
 ≡⇒≋ : ∀ {ℓ} {A : Set ℓ} {x y : List A} → x ≡ y → x ≋ y
 ≡⇒≋ refl = refl
@@ -373,7 +373,7 @@ x∪y⊆x̀∪ỳ : ∀ {ℓ} {A : Set ℓ} {x x̀ y ỳ : List A} → x ⊆ x̀
 x∪y⊆x̀∪ỳ {x = []} {x̀ = []} _ y⊆ỳ = y⊆ỳ
 x∪y⊆x̀∪ỳ {x = []} {x̀ = _ ∷ t̀} _ y⊆ỳ = there ∘ x∪y⊆x̀∪ỳ ([]⊆x t̀) y⊆ỳ
 x∪y⊆x̀∪ỳ {x = h ∷ t} {x̀ = x̀} {y = y} {ỳ = ỳ} x⊆x̀ y⊆ỳ = f where
-    f : h ∷ t ∪ y ⊆ x̀ ∪ ỳ
+    f : (h ∷ t) ∪ y ⊆ x̀ ∪ ỳ
     f {e} (here {x = .h} e≡h) = e∈x⇒e∈x∪y ỳ (x⊆x̀ $ here e≡h)
     f {e} (there {xs = .(t ∪ y)} p) = x∪y⊆x̀∪ỳ (x∪y⊆z⇒y⊆z [ h ] t x⊆x̀) y⊆ỳ p
 
@@ -388,9 +388,9 @@ t≋t∖n∪t∩n [] _ = refl
 t≋t∖n∪t∩n (h ∷ t) n with n ∋! proj₁ h
 ... | false = e∷x≋e∷y h $ t≋t∖n∪t∩n t n
 ... | true = ≋-trans p₁ p₂ where
-           p₁ : h ∷ t ≋ h ∷ (t ∖∖ n) ∪ filter-∈ t n
+           p₁ : h ∷ t ≋ (h ∷ (t ∖∖ n)) ∪ filter-∈ t n
            p₁ = e∷x≋e∷y h $ t≋t∖n∪t∩n t n
-           p₂ : h ∷ (t ∖∖ n) ∪ filter-∈ t n ≋ (t ∖∖ n) ∪ h ∷ filter-∈ t n
+           p₂ : (h ∷ (t ∖∖ n)) ∪ filter-∈ t n ≋ (t ∖∖ n) ∪ (h ∷ filter-∈ t n)
            p₂ = ≋-del-ins-r [] h (t ∖∖ n) (filter-∈ t n)
 
 e₁∈x⇒e₂∉x⇒e≢e₂ : ∀ {ℓ} {A : Set ℓ} {e₁ e₂ : A} {x : List A} → e₁ ∈ x → e₂ ∉ x → e₁ ≢ e₂
@@ -484,7 +484,7 @@ a∈x⇒x≋y⇒a∈y a∈x x≋y = x⊆y≋z (e∈l⇒[e]⊆l a∈x) x≋y (her
 x⊆z⇒y⊆z⇒x∪y⊆z : ∀ {ℓ} {A : Set ℓ} {x y z : List A} → x ⊆ z → y ⊆ z → x ∪ y ⊆ z
 x⊆z⇒y⊆z⇒x∪y⊆z {x = []} _ y⊆z = y⊆z
 x⊆z⇒y⊆z⇒x∪y⊆z {x = h ∷ t} {y = y} {z = z} x⊆z y⊆z = f where
-    f : h ∷ t ∪ y ⊆ z
+    f : (h ∷ t) ∪ y ⊆ z
     f {e} (here e≡h) = x⊆z $ here e≡h
     f {e} (there e∈t∪y) = x⊆z⇒y⊆z⇒x∪y⊆z (x∪y⊆z⇒y⊆z [ h ] t x⊆z) y⊆z e∈t∪y
 
@@ -690,7 +690,7 @@ x⊆y⇒∃x̀,y≋x∪x̀ {x = h ∷ t} {y = y} (h∉t ∷ nr-t) nr-y h∷t⊆y
         p₁ = x⊆e∷y⇒e∉x⇒x⊆y (x⊆y≋z (x∪y⊆z⇒y⊆z [ h ] t h∷t⊆y) y≋h∷ỳ) h∉t
         nr-ỳ = nr-x∪y⇒nr-y [ h ] ỳ $ nr-x≋y y≋h∷ỳ nr-y
         t̀ , ỳ≋t∪t̀ = x⊆y⇒∃x̀,y≋x∪x̀ nr-t nr-ỳ p₁
-        p₂ : h ∷ ỳ ≋ h ∷ t ∪ t̀
+        p₂ : h ∷ ỳ ≋ (h ∷ t) ∪ t̀
         p₂ = y≋ỳ⇒x∪y≋x∪ỳ [ h ] ỳ≋t∪t̀
      in t̀ , ≋-trans y≋h∷ỳ p₂