{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}

{-| The parser doesn't know about operators and parses everything as normal
    function application. This module contains the functions that parses the
    operators properly. For a stand-alone implementation of this see
    @src\/prototyping\/mixfix\/old@.

    It also contains the function that puts parenthesis back given the
    precedence of the context.
-}

module Agda.Syntax.Concrete.Operators
    ( parseApplication
    , parseModuleApplication
    , parseLHS
    , parsePattern
    , parsePatternSyn
    ) where

import Control.Applicative ( Alternative((<|>)))
import Control.Monad.Except (throwError)

import Data.Either (partitionEithers)
import qualified Data.Foldable as Fold
import qualified Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Traversable as Trav

import Agda.Syntax.Common
import Agda.Syntax.Concrete hiding (appView)
import Agda.Syntax.Concrete.Operators.Parser
import Agda.Syntax.Concrete.Operators.Parser.Monad hiding (parse)
import Agda.Syntax.Concrete.Pattern
import Agda.Syntax.Position
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Flat
import Agda.Syntax.Scope.Monad

import Agda.TypeChecking.Monad.Base (typeError, TypeError(..), LHSOrPatSyn(..))
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State (getScope)

import Agda.Utils.Function (applyWhen)
import Agda.Utils.Either
import Agda.Syntax.Common.Pretty
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.List2 (List2, pattern List2)
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Maybe
import Agda.Utils.Monad (guardWithError)
import Agda.Utils.Trie (Trie)
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Billing
---------------------------------------------------------------------------

-- | Bills the operator parser.

billToParser :: ExprKind -> ScopeM a -> ScopeM a
billToParser :: forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
k = Account (BenchPhase (TCMT IO)) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo
  [ BenchPhase (TCMT IO)
Phase
Bench.Parsing
  , case ExprKind
k of
      ExprKind
IsExpr    -> BenchPhase (TCMT IO)
Phase
Bench.OperatorsExpr
      ExprKind
IsPattern -> BenchPhase (TCMT IO)
Phase
Bench.OperatorsPattern
  ]

---------------------------------------------------------------------------
-- * Building the parser
---------------------------------------------------------------------------

-- | A data structure used internally by 'buildParsers'.
data InternalParsers e = InternalParsers
  { forall e. InternalParsers e -> Parser e e
pTop    :: Parser e e
  , forall e. InternalParsers e -> Parser e e
pApp    :: Parser e e
  , forall e. InternalParsers e -> Parser e [NamedArg e]
pArgs   :: Parser e [NamedArg e]
  , forall e. InternalParsers e -> Parser e e
pNonfix :: Parser e e
  , forall e. InternalParsers e -> Parser e e
pAtom   :: Parser e e
  }

-- | Expression kinds: Expressions or patterns.
data ExprKind = IsExpr | IsPattern
  deriving (ExprKind -> ExprKind -> Bool
(ExprKind -> ExprKind -> Bool)
-> (ExprKind -> ExprKind -> Bool) -> Eq ExprKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExprKind -> ExprKind -> Bool
== :: ExprKind -> ExprKind -> Bool
$c/= :: ExprKind -> ExprKind -> Bool
/= :: ExprKind -> ExprKind -> Bool
Eq, Int -> ExprKind -> ShowS
[ExprKind] -> ShowS
ExprKind -> String
(Int -> ExprKind -> ShowS)
-> (ExprKind -> String) -> ([ExprKind] -> ShowS) -> Show ExprKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExprKind -> ShowS
showsPrec :: Int -> ExprKind -> ShowS
$cshow :: ExprKind -> String
show :: ExprKind -> String
$cshowList :: [ExprKind] -> ShowS
showList :: [ExprKind] -> ShowS
Show)

-- | The data returned by 'buildParsers'.

data Parsers e = Parsers
  { forall e. Parsers e -> [e] -> [e]
parser :: [e] -> [e]
    -- ^ A parser for expressions or patterns (depending on the
    -- 'ExprKind' argument given to 'buildParsers').
  , forall e. Parsers e -> [e] -> [[NamedArg e]]
argsParser :: [e] -> [[NamedArg e]]
    -- ^ A parser for sequences of arguments.
  , forall e. Parsers e -> [NotationSection]
operators :: [NotationSection]
    -- ^ All operators/notations/sections that were used to generate
    -- the grammar.
  , forall e. Parsers e -> FlatScope
flattenedScope :: FlatScope
    -- ^ A flattened scope that only contains those names that are
    -- unqualified or qualified by qualifiers that occur in the list
    -- of names given to 'buildParsers'.
  }

-- | Builds parsers for operator applications from all the operators
-- and function symbols in scope.
--
-- When parsing a pattern we do not use bound names. The effect is
-- that unqualified 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.
--
-- When parsing a pattern we also disallow the use of sections, mainly
-- because there is little need for sections in patterns. Note that
-- sections are parsed by splitting up names into multiple tokens
-- (@_+_@ is replaced by @_@, @+@ and @_@), and if we were to support
-- sections in patterns, then we would have to accept certain such
-- sequences of tokens as single pattern variables.

buildParsers
  :: forall e. IsExpr e
  => ExprKind
     -- ^ Should expressions or patterns be parsed?
  -> [QName]
     -- ^ This list must include every name part in the
     -- expression/pattern to be parsed (excluding name parts inside
     -- things like parenthesised subexpressions that are treated as
     -- atoms). The list is used to optimise the parser. For
     -- instance, a given notation is only included in the generated
     -- grammar if all of the notation's name parts are present in
     -- the list of names.
  -> ScopeM (Parsers e)
buildParsers :: forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
buildParsers ExprKind
kind [QName]
exprNames = do
    FlatScope
flat         <- [[Name]] -> ScopeInfo -> FlatScope
flattenScope ([QName] -> [[Name]]
qualifierModules [QName]
exprNames) (ScopeInfo -> FlatScope) -> TCMT IO ScopeInfo -> TCMT IO FlatScope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                      TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
    ([QName]
names, [NewNotation]
ops0) <- FlatScope -> ScopeM ([QName], [NewNotation])
localNames FlatScope
flat
    let ops :: [NewNotation]
ops | ExprKind
kind ExprKind -> ExprKind -> Bool
forall a. Eq a => a -> a -> Bool
== ExprKind
IsPattern = (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (NewNotation -> Bool) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Bool
isLambdaNotation) [NewNotation]
ops0
            | Bool
otherwise         = [NewNotation]
ops0

    let -- All names.
        namesInExpr :: Set QName
        namesInExpr :: Set QName
namesInExpr = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList [QName]
exprNames

        partListsInExpr' :: [[NamePart]]
partListsInExpr' = (QName -> [NamePart]) -> [QName] -> [[NamePart]]
forall a b. (a -> b) -> [a] -> [b]
map (NameParts -> [Item NameParts]
NameParts -> [NamePart]
forall l. IsList l => l -> [Item l]
List1.toList (NameParts -> [NamePart])
-> (QName -> NameParts) -> QName -> [NamePart]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> NameParts
nameParts (Name -> NameParts) -> (QName -> Name) -> QName -> NameParts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
unqualify) ([QName] -> [[NamePart]]) -> [QName] -> [[NamePart]]
forall a b. (a -> b) -> a -> b
$
                           Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
namesInExpr

        partListTrie :: ([[NamePart]] -> t [k]) -> Trie k ()
partListTrie [[NamePart]] -> t [k]
f =
          ([k] -> Trie k () -> Trie k ()) -> Trie k () -> t [k] -> Trie k ()
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\[k]
ps -> Trie k () -> Trie k () -> Trie k ()
forall k v. Ord k => Trie k v -> Trie k v -> Trie k v
Trie.union ([k] -> () -> Trie k ()
forall k v. [k] -> v -> Trie k v
Trie.everyPrefix [k]
ps ()))
                Trie k ()
forall a. Null a => a
Trie.empty
                ([[NamePart]] -> t [k]
f [[NamePart]]
partListsInExpr')

        -- All names.
        partListsInExpr :: Trie NamePart ()
        partListsInExpr :: Trie NamePart ()
partListsInExpr = ([[NamePart]] -> [[NamePart]]) -> Trie NamePart ()
forall {t :: * -> *} {k}.
(Foldable t, Ord k) =>
([[NamePart]] -> t [k]) -> Trie k ()
partListTrie [[NamePart]] -> [[NamePart]]
forall a. a -> a
id

        -- All names, with the name parts in reverse order.
        reversedPartListsInExpr :: Trie NamePart ()
        reversedPartListsInExpr :: Trie NamePart ()
reversedPartListsInExpr = ([[NamePart]] -> [[NamePart]]) -> Trie NamePart ()
forall {t :: * -> *} {k}.
(Foldable t, Ord k) =>
([[NamePart]] -> t [k]) -> Trie k ()
partListTrie (([NamePart] -> [NamePart]) -> [[NamePart]] -> [[NamePart]]
forall a b. (a -> b) -> [a] -> [b]
map [NamePart] -> [NamePart]
forall a. [a] -> [a]
reverse)

        -- Every regular name part (not holes etc.).
        partsInExpr :: Set RawName
        partsInExpr :: Set String
partsInExpr =
          [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList [ String
s | Id String
s <- [[NamePart]] -> [NamePart]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[NamePart]]
partListsInExpr' ]

        -- Are all name parts present in the expression?
        partsPresent :: NewNotation -> [Bool]
partsPresent NewNotation
n =
          [ String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
p Set String
partsInExpr
          | String
p <- Notation -> [String]
stringParts (NewNotation -> Notation
notation NewNotation
n)
          ]

        addHole :: Bool -> String -> [NamePart]
addHole Bool
True  String
p = [NamePart
Hole, String -> NamePart
Id String
p]
        addHole Bool
False String
p = [String -> NamePart
Id String
p]

        -- Is the first identifier part present in n present in the
        -- expression, without any preceding name parts, except for a
        -- leading underscore iff withHole is True?
        firstPartPresent :: Bool -> Notation -> Bool
firstPartPresent Bool
withHole Notation
n =
          [NamePart] -> Trie NamePart () -> Bool
forall k v. Ord k => [k] -> Trie k v -> Bool
Trie.member (Bool -> String -> [NamePart]
addHole Bool
withHole String
p) Trie NamePart ()
partListsInExpr
          where
          p :: String
p = case Notation
n of
            HolePart{} : IdPart RString
p : Notation
_ -> RString -> String
forall a. Ranged a -> a
rangedThing RString
p
            IdPart RString
p : Notation
_              -> RString -> String
forall a. Ranged a -> a
rangedThing RString
p
            Notation
_                         -> String
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- Is the last identifier part present in n present in the
        -- expression, without any succeeding name parts, except for a
        -- trailing underscore iff withHole is True?
        lastPartPresent :: Bool -> Notation -> Bool
lastPartPresent Bool
withHole Notation
n =
          [NamePart] -> Trie NamePart () -> Bool
forall k v. Ord k => [k] -> Trie k v -> Bool
Trie.member (Bool -> String -> [NamePart]
addHole Bool
withHole String
p) Trie NamePart ()
reversedPartListsInExpr
          where
          p :: String
p = case Notation -> Notation
forall a. [a] -> [a]
reverse Notation
n of
            HolePart{} : IdPart RString
p : Notation
_ -> RString -> String
forall a. Ranged a -> a
rangedThing RString
p
            IdPart RString
p : Notation
_              -> RString -> String
forall a. Ranged a -> a
rangedThing RString
p
            Notation
_                         -> String
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- Are the initial and final identifier parts present with
        -- the right mix of leading and trailing underscores?
        correctUnderscores :: Bool -> Bool -> Notation -> Bool
        correctUnderscores :: Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
withInitialHole Bool
withFinalHole Notation
n =
          Bool -> Notation -> Bool
firstPartPresent Bool
withInitialHole Notation
n
            Bool -> Bool -> Bool
&&
          Bool -> Notation -> Bool
lastPartPresent  Bool
withFinalHole   Notation
n

        -- Should be used with operators (not sections) and notations
        -- coming from syntax declarations.
        filterCorrectUnderscoresOp :: [NewNotation] -> [NotationSection]
        filterCorrectUnderscoresOp :: [NewNotation] -> [NotationSection]
filterCorrectUnderscoresOp [NewNotation]
ns =
          [ NewNotation -> NotationSection
noSection NewNotation
n
          | NewNotation
n <- [NewNotation]
ns
          , if NewNotation -> Bool
notaIsOperator NewNotation
n
            then Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
False Bool
False (NewNotation -> Notation
notation NewNotation
n)
            else (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\String
s -> [NamePart] -> Trie NamePart () -> Bool
forall k v. Ord k => [k] -> Trie k v -> Bool
Trie.member [String -> NamePart
Id String
s] Trie NamePart ()
partListsInExpr)
                     (Notation -> [String]
stringParts (Notation -> [String]) -> Notation -> [String]
forall a b. (a -> b) -> a -> b
$ NewNotation -> Notation
notation NewNotation
n)
          ]

        -- Should be used with sections.
        correctUnderscoresSect :: NotationKind -> Notation -> Bool
        correctUnderscoresSect :: NotationKind -> Notation -> Bool
correctUnderscoresSect NotationKind
k Notation
n = case (NotationKind
k, Notation -> NotationKind
notationKind Notation
n) of
          (NotationKind
PrefixNotation,  NotationKind
InfixNotation)   -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
True Bool
False Notation
n
          (NotationKind
PostfixNotation, NotationKind
InfixNotation)   -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
False Bool
True Notation
n
          (NotationKind
NonfixNotation,  NotationKind
InfixNotation)   -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
True Bool
True Notation
n
          (NotationKind
NonfixNotation,  NotationKind
PrefixNotation)  -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
False Bool
True Notation
n
          (NotationKind
NonfixNotation,  NotationKind
PostfixNotation) -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
True Bool
False Notation
n
          (NotationKind, NotationKind)
_                                  -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

        -- If "or" is replaced by "and" in conParts/allParts below,
        -- then the misspelled operator application "if x thenn x else
        -- x" can be parsed as "if" applied to five arguments,
        -- resulting in a confusing error message claiming that "if"
        -- is not in scope.

        ([NewNotation]
non, [NewNotation]
fix) = (NewNotation -> Bool)
-> [NewNotation] -> ([NewNotation], [NewNotation])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition NewNotation -> Bool
nonfix ((NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> (NewNotation -> [Bool]) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [Bool]
partsPresent) [NewNotation]
ops)

        cons :: [List1 NewNotation]
cons       = KindsOfNames -> FlatScope -> [List1 NewNotation]
getDefinedNames
                       ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
ConName, KindOfName
CoConName, KindOfName
FldName, KindOfName
PatternSynName]) FlatScope
flat
        conNames :: Set QName
conNames   = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$
                       (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((QName -> Set QName -> Bool) -> Set QName -> QName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set QName
namesInExpr) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$
                       (List1 NewNotation -> QName) -> [List1 NewNotation] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> QName
notaName (NewNotation -> QName)
-> (List1 NewNotation -> NewNotation) -> List1 NewNotation -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 NewNotation -> NewNotation
forall a. NonEmpty a -> a
List1.head) [List1 NewNotation]
cons
        conParts :: Set QName
conParts   = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$
                       (NewNotation -> [QName]) -> [NewNotation] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NewNotation -> [QName]
notationNames ([NewNotation] -> [QName]) -> [NewNotation] -> [QName]
forall a b. (a -> b) -> a -> b
$
                       (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> (NewNotation -> [Bool]) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [Bool]
partsPresent) ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> a -> b
$
                       [List1 NewNotation] -> [NewNotation]
forall a. [List1 a] -> [a]
List1.concat [List1 NewNotation]
cons

        allNames :: Set QName
allNames   = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$
                       (QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((QName -> Set QName -> Bool) -> Set QName -> QName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set QName
namesInExpr) [QName]
names
        allParts :: Set QName
allParts   = Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
conParts
                       ([QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$
                        (NewNotation -> [QName]) -> [NewNotation] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NewNotation -> [QName]
notationNames ([NewNotation] -> [QName]) -> [NewNotation] -> [QName]
forall a b. (a -> b) -> a -> b
$
                        (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> (NewNotation -> [Bool]) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [Bool]
partsPresent) [NewNotation]
ops)

        isAtom :: QName -> Bool
isAtom QName
x
          | ExprKind
kind ExprKind -> ExprKind -> Bool
forall a. Eq a => a -> a -> Bool
== ExprKind
IsPattern Bool -> Bool -> Bool
&& Bool -> Bool
not (QName -> Bool
isQualified QName
x) =
            Bool -> Bool
not (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
conParts) Bool -> Bool -> Bool
|| QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
conNames
          | Bool
otherwise =
            Bool -> Bool
not (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
allParts) Bool -> Bool -> Bool
|| QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
allNames
        -- If string is a part of notation, it cannot be used as an identifier,
        -- unless it is also used as an identifier. See issue 307.

        parseSections :: ParseSections
parseSections = case ExprKind
kind of
          ExprKind
IsPattern -> ParseSections
DoNotParseSections
          ExprKind
IsExpr    -> ParseSections
ParseSections

    let nonClosedSections :: FixityLevel -> [NewNotation] -> [NotationSection]
nonClosedSections FixityLevel
l [NewNotation]
ns =
          case ParseSections
parseSections of
            ParseSections
DoNotParseSections -> []
            ParseSections
ParseSections      ->
              [ NewNotation
-> NotationKind -> Maybe FixityLevel -> Bool -> NotationSection
NotationSection NewNotation
n NotationKind
k (FixityLevel -> Maybe FixityLevel
forall a. a -> Maybe a
Just FixityLevel
l) Bool
True
              | NewNotation
n <- [NewNotation]
ns
              , NewNotation -> Bool
isinfix NewNotation
n Bool -> Bool -> Bool
&& NewNotation -> Bool
notaIsOperator NewNotation
n
              , NotationKind
k <- [NotationKind
PrefixNotation, NotationKind
PostfixNotation]
              , NotationKind -> Notation -> Bool
correctUnderscoresSect NotationKind
k (NewNotation -> Notation
notation NewNotation
n)
              ]

        unrelatedOperators :: [NotationSection]
        unrelatedOperators :: [NotationSection]
unrelatedOperators =
          [NewNotation] -> [NotationSection]
filterCorrectUnderscoresOp [NewNotation]
unrelated
            [NotationSection] -> [NotationSection] -> [NotationSection]
forall a. [a] -> [a] -> [a]
++
          FixityLevel -> [NewNotation] -> [NotationSection]
nonClosedSections FixityLevel
Unrelated [NewNotation]
unrelated
          where
          unrelated :: [NewNotation]
unrelated = (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter ((FixityLevel -> FixityLevel -> Bool
forall a. Eq a => a -> a -> Bool
== FixityLevel
Unrelated) (FixityLevel -> Bool)
-> (NewNotation -> FixityLevel) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> FixityLevel
level) [NewNotation]
fix

        nonWithSections :: [NotationSection]
        nonWithSections :: [NotationSection]
nonWithSections =
          (NotationSection -> NotationSection)
-> [NotationSection] -> [NotationSection]
forall a b. (a -> b) -> [a] -> [b]
map (\NotationSection
s -> NotationSection
s { sectLevel = Nothing })
              ([NewNotation] -> [NotationSection]
filterCorrectUnderscoresOp [NewNotation]
non)
            [NotationSection] -> [NotationSection] -> [NotationSection]
forall a. [a] -> [a] -> [a]
++
          case ParseSections
parseSections of
            ParseSections
DoNotParseSections -> []
            ParseSections
ParseSections      ->
              [ NewNotation
-> NotationKind -> Maybe FixityLevel -> Bool -> NotationSection
NotationSection NewNotation
n NotationKind
NonfixNotation Maybe FixityLevel
forall a. Maybe a
Nothing Bool
True
              | NewNotation
n <- [NewNotation]
fix
              , NewNotation -> Bool
notaIsOperator NewNotation
n
              , NotationKind -> Notation -> Bool
correctUnderscoresSect NotationKind
NonfixNotation (NewNotation -> Notation
notation NewNotation
n)
              ]

        -- The triples have the form (level, operators). The lowest
        -- level comes first.
        relatedOperators :: [(PrecedenceLevel, [NotationSection])]
        relatedOperators :: [(PrecedenceLevel, [NotationSection])]
relatedOperators =
          (NonEmpty (PrecedenceLevel, [NotationSection])
 -> (PrecedenceLevel, [NotationSection]))
-> [NonEmpty (PrecedenceLevel, [NotationSection])]
-> [(PrecedenceLevel, [NotationSection])]
forall a b. (a -> b) -> [a] -> [b]
map (\((PrecedenceLevel
l, [NotationSection]
ns) :| [(PrecedenceLevel, [NotationSection])]
rest) -> (PrecedenceLevel
l, [NotationSection]
ns [NotationSection] -> [NotationSection] -> [NotationSection]
forall a. [a] -> [a] -> [a]
++ ((PrecedenceLevel, [NotationSection]) -> [NotationSection])
-> [(PrecedenceLevel, [NotationSection])] -> [NotationSection]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PrecedenceLevel, [NotationSection]) -> [NotationSection]
forall a b. (a, b) -> b
snd [(PrecedenceLevel, [NotationSection])]
rest)) ([NonEmpty (PrecedenceLevel, [NotationSection])]
 -> [(PrecedenceLevel, [NotationSection])])
-> ([NewNotation]
    -> [NonEmpty (PrecedenceLevel, [NotationSection])])
-> [NewNotation]
-> [(PrecedenceLevel, [NotationSection])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          ((PrecedenceLevel, [NotationSection]) -> PrecedenceLevel)
-> [(PrecedenceLevel, [NotationSection])]
-> [NonEmpty (PrecedenceLevel, [NotationSection])]
forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn (PrecedenceLevel, [NotationSection]) -> PrecedenceLevel
forall a b. (a, b) -> a
fst ([(PrecedenceLevel, [NotationSection])]
 -> [NonEmpty (PrecedenceLevel, [NotationSection])])
-> ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
-> [NewNotation]
-> [NonEmpty (PrecedenceLevel, [NotationSection])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          (NewNotation -> Maybe (PrecedenceLevel, [NotationSection]))
-> [NewNotation] -> [(PrecedenceLevel, [NotationSection])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\NewNotation
n -> case NewNotation -> FixityLevel
level NewNotation
n of
                            FixityLevel
Unrelated     -> Maybe (PrecedenceLevel, [NotationSection])
forall a. Maybe a
Nothing
                            r :: FixityLevel
r@(Related PrecedenceLevel
l) ->
                              (PrecedenceLevel, [NotationSection])
-> Maybe (PrecedenceLevel, [NotationSection])
forall a. a -> Maybe a
Just (PrecedenceLevel
l, [NewNotation] -> [NotationSection]
filterCorrectUnderscoresOp [NewNotation
n] [NotationSection] -> [NotationSection] -> [NotationSection]
forall a. [a] -> [a] -> [a]
++
                                       FixityLevel -> [NewNotation] -> [NotationSection]
nonClosedSections FixityLevel
r [NewNotation
n])) ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
-> [NewNotation] -> [(PrecedenceLevel, [NotationSection])]
forall a b. (a -> b) -> a -> b
$
          [NewNotation]
fix

        everything :: [NotationSection]
        everything :: [NotationSection]
everything =
          ((PrecedenceLevel, [NotationSection]) -> [NotationSection])
-> [(PrecedenceLevel, [NotationSection])] -> [NotationSection]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PrecedenceLevel, [NotationSection]) -> [NotationSection]
forall a b. (a, b) -> b
snd [(PrecedenceLevel, [NotationSection])]
relatedOperators [NotationSection] -> [NotationSection] -> [NotationSection]
forall a. [a] -> [a] -> [a]
++
          [NotationSection]
unrelatedOperators [NotationSection] -> [NotationSection] -> [NotationSection]
forall a. [a] -> [a] -> [a]
++
          [NotationSection]
nonWithSections

    String -> Int -> [String] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> [String] -> m ()
reportS String
"scope.operators" Int
50
      [ String
"unrelatedOperators = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [NotationSection] -> String
forall a. Pretty a => a -> String
prettyShow [NotationSection]
unrelatedOperators
      , String
"nonWithSections    = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [NotationSection] -> String
forall a. Pretty a => a -> String
prettyShow [NotationSection]
nonWithSections
      , String
"relatedOperators   = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(PrecedenceLevel, [NotationSection])] -> String
forall a. Pretty a => a -> String
prettyShow [(PrecedenceLevel, [NotationSection])]
relatedOperators
      ]

    let g :: InternalParsers e
g = (InternalParsers e -> InternalParsers e) -> InternalParsers e
forall a. (a -> a) -> a
Data.Function.fix ((InternalParsers e -> InternalParsers e) -> InternalParsers e)
-> (InternalParsers e -> InternalParsers e) -> InternalParsers e
forall a b. (a -> b) -> a -> b
$ \InternalParsers e
p -> InternalParsers
              { pTop :: Parser e e
pTop    = MemoKey -> Parser e e -> Parser e e
forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise MemoKey
TopK (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$
                          [Parser e e] -> Parser e e
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
forall a b. (a -> b) -> a -> b
$
                            ((PrecedenceLevel, [NotationSection]) -> Parser e e -> Parser e e)
-> Parser e e
-> [(PrecedenceLevel, [NotationSection])]
-> Parser e e
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(PrecedenceLevel
l, [NotationSection]
ns) Parser e e
higher ->
                                       PrecedenceKey
-> ParseSections
-> Parser e e
-> [NotationSection]
-> Parser e e
-> Bool
-> Parser e e
mkP (PrecedenceLevel -> PrecedenceKey
forall a b. b -> Either a b
Right PrecedenceLevel
l) ParseSections
parseSections
                                           (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pTop InternalParsers e
p) [NotationSection]
ns Parser e e
higher Bool
True) (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pApp InternalParsers e
p)
                                   [(PrecedenceLevel, [NotationSection])]
relatedOperators Parser e e -> [Parser e e] -> [Parser e e]
forall a. a -> [a] -> [a]
:
                            (PrecedenceLevel -> NotationSection -> Parser e e)
-> [PrecedenceLevel] -> [NotationSection] -> [Parser e e]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ PrecedenceLevel
k NotationSection
n ->
                                    PrecedenceKey
-> ParseSections
-> Parser e e
-> [NotationSection]
-> Parser e e
-> Bool
-> Parser e e
mkP (PrecedenceLevel -> PrecedenceKey
forall a b. a -> Either a b
Left PrecedenceLevel
k) ParseSections
parseSections
                                        (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pTop InternalParsers e
p) [NotationSection
n] (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pApp InternalParsers e
p) Bool
False) [PrecedenceLevel
0..] [NotationSection]
unrelatedOperators
              , pApp :: Parser e e
pApp    = MemoKey -> Parser e e -> Parser e e
forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise MemoKey
AppK (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$ Parser e e -> Parser e [NamedArg e] -> Parser e e
forall e.
IsExpr e =>
Parser e e -> Parser e [NamedArg e] -> Parser e e
appP (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pNonfix InternalParsers e
p) (InternalParsers e -> Parser e [NamedArg e]
forall e. InternalParsers e -> Parser e [NamedArg e]
pArgs InternalParsers e
p)
              , pArgs :: Parser e [NamedArg e]
pArgs   = Parser e e -> Parser e [NamedArg e]
forall e. IsExpr e => Parser e e -> Parser e [NamedArg e]
argsP (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pNonfix InternalParsers e
p)
              , pNonfix :: Parser e e
pNonfix = MemoKey -> Parser e e -> Parser e e
forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise MemoKey
NonfixK (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$
                          [Parser e e] -> Parser e e
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
forall a b. (a -> b) -> a -> b
$
                            InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pAtom InternalParsers e
p Parser e e -> [Parser e e] -> [Parser e e]
forall a. a -> [a] -> [a]
:
                            (NotationSection -> Parser e e)
-> [NotationSection] -> [Parser e e]
forall a b. (a -> b) -> [a] -> [b]
map (\NotationSection
sect ->
                              let n :: NewNotation
n = NotationSection -> NewNotation
sectNotation NotationSection
sect

                                  inner :: forall k. NK k ->
                                           Parser e (OperatorType k e)
                                  inner :: forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner = ParseSections
-> Parser e e
-> NewNotation
-> NK k
-> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall e (k :: NotationKind).
IsExpr e =>
ParseSections
-> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
opP ParseSections
parseSections (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pTop InternalParsers e
p) NewNotation
n
                              in
                              case Notation -> NotationKind
notationKind (NewNotation -> Notation
notation NewNotation
n) of
                                NotationKind
InfixNotation ->
                                  ((MaybePlaceholder e -> MaybePlaceholder e -> e)
 -> MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e
-> (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e
-> e
forall a b c. (a -> b -> c) -> b -> a -> c
flip (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> MaybePlaceholder e -> e
forall a b. (a -> b) -> a -> b
($) (MaybePlaceholder e
 -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
 -> MaybePlaceholder e
 -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     ((MaybePlaceholder e -> MaybePlaceholder e -> e)
      -> MaybePlaceholder e -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PositionInName
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
Beginning
                                           Parser
  MemoKey
  e
  (MaybePlaceholder e)
  ((MaybePlaceholder e -> MaybePlaceholder e -> e)
   -> MaybePlaceholder e -> e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'InfixNotation
In
                                           Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser e e
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PositionInName
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
End
                                NotationKind
PrefixNotation ->
                                  NK 'PrefixNotation -> Parser e (OperatorType 'PrefixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'PrefixNotation
Pre Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser e e
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PositionInName
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
End
                                NotationKind
PostfixNotation ->
                                  ((MaybePlaceholder e -> e) -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e
forall a b c. (a -> b -> c) -> b -> a -> c
flip (MaybePlaceholder e -> e) -> MaybePlaceholder e -> e
forall a b. (a -> b) -> a -> b
($) (MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser
     MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PositionInName
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
Beginning
                                           Parser
  MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
-> Parser e e
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NK 'PostfixNotation -> Parser e (OperatorType 'PostfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'PostfixNotation
Post
                                NotationKind
NonfixNotation -> NK 'NonfixNotation -> Parser e (OperatorType 'NonfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'NonfixNotation
Non
                                NotationKind
NoNotation     -> Parser e e
forall a. HasCallStack => a
__IMPOSSIBLE__) [NotationSection]
nonWithSections
              , pAtom :: Parser e e
pAtom   = (QName -> Bool) -> Parser e e
forall e. IsExpr e => (QName -> Bool) -> Parser e e
atomP QName -> Bool
isAtom
              }

    -- Andreas, 2020-06-03 #4712
    -- Note: needs Agda to be compiled with DEBUG to print the grammar.
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"scope.grammar" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
      Doc
"Operator grammar:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Parser e e -> Doc
forall tok a. Parser tok a -> Doc
grammar (InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pTop InternalParsers e
g))

    Parsers e -> ScopeM (Parsers e)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Parsers e -> ScopeM (Parsers e))
-> Parsers e -> ScopeM (Parsers e)
forall a b. (a -> b) -> a -> b
$ Parsers
      { parser :: [e] -> [e]
parser         = (ParseSections, Parser e e) -> [e] -> [e]
forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
parse (ParseSections
parseSections, InternalParsers e -> Parser e e
forall e. InternalParsers e -> Parser e e
pTop  InternalParsers e
g)
      , argsParser :: [e] -> [[NamedArg e]]
argsParser     = (ParseSections, Parser e [NamedArg e]) -> [e] -> [[NamedArg e]]
forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
parse (ParseSections
parseSections, InternalParsers e -> Parser e [NamedArg e]
forall e. InternalParsers e -> Parser e [NamedArg e]
pArgs InternalParsers e
g)
      , operators :: [NotationSection]
operators      = [NotationSection]
everything
      , flattenedScope :: FlatScope
flattenedScope = FlatScope
flat
      }
    where
        level :: NewNotation -> FixityLevel
        level :: NewNotation -> FixityLevel
level = Fixity -> FixityLevel
fixityLevel (Fixity -> FixityLevel)
-> (NewNotation -> Fixity) -> NewNotation -> FixityLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity

        nonfix, isinfix, isprefix, ispostfix :: NewNotation -> Bool
        nonfix :: NewNotation -> Bool
nonfix    = (NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
NonfixNotation)  (NotationKind -> Bool)
-> (NewNotation -> NotationKind) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notation -> NotationKind
notationKind (Notation -> NotationKind)
-> (NewNotation -> Notation) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Notation
notation
        isinfix :: NewNotation -> Bool
isinfix   = (NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
InfixNotation)   (NotationKind -> Bool)
-> (NewNotation -> NotationKind) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notation -> NotationKind
notationKind (Notation -> NotationKind)
-> (NewNotation -> Notation) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Notation
notation
        isprefix :: NewNotation -> Bool
isprefix  = (NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
PrefixNotation)  (NotationKind -> Bool)
-> (NewNotation -> NotationKind) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notation -> NotationKind
notationKind (Notation -> NotationKind)
-> (NewNotation -> Notation) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Notation
notation
        ispostfix :: NewNotation -> Bool
ispostfix = (NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
PostfixNotation) (NotationKind -> Bool)
-> (NewNotation -> NotationKind) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notation -> NotationKind
notationKind (Notation -> NotationKind)
-> (NewNotation -> Notation) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Notation
notation

        isPrefix, isPostfix :: NotationSection -> Bool
        isPrefix :: NotationSection -> Bool
isPrefix  = (NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
PrefixNotation)  (NotationKind -> Bool)
-> (NotationSection -> NotationKind) -> NotationSection -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> NotationKind
sectKind
        isPostfix :: NotationSection -> Bool
isPostfix = (NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
PostfixNotation) (NotationKind -> Bool)
-> (NotationSection -> NotationKind) -> NotationSection -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> NotationKind
sectKind

        isInfix :: Associativity -> NotationSection -> Bool
        isInfix :: Associativity -> NotationSection -> Bool
isInfix Associativity
ass NotationSection
s =
          NotationSection -> NotationKind
sectKind NotationSection
s NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
InfixNotation
             Bool -> Bool -> Bool
&&
          Fixity -> Associativity
fixityAssoc (NewNotation -> Fixity
notaFixity (NotationSection -> NewNotation
sectNotation NotationSection
s)) Associativity -> Associativity -> Bool
forall a. Eq a => a -> a -> Bool
== Associativity
ass

        mkP :: PrecedenceKey  -- Memoisation key.
            -> ParseSections
            -> Parser e e
            -> [NotationSection]
            -> Parser e e  -- A parser for an expression of higher precedence.
            -> Bool  -- Include the \"expression of higher precedence\"
                     -- parser as one of the choices?
            -> Parser e e
        mkP :: PrecedenceKey
-> ParseSections
-> Parser e e
-> [NotationSection]
-> Parser e e
-> Bool
-> Parser e e
mkP PrecedenceKey
key ParseSections
parseSections Parser e e
p0 [NotationSection]
ops Parser e e
higher Bool
includeHigher =
            MemoKey -> Parser e e -> Parser e e
forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise (PrecedenceKey -> MemoKey
NodeK PrecedenceKey
key) (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$
              [Parser e e] -> Parser e e
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
forall a b. (a -> b) -> a -> b
$
                Bool
-> ([Parser e e] -> [Parser e e]) -> [Parser e e] -> [Parser e e]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
includeHigher (Parser e e
higher Parser e e -> [Parser e e] -> [Parser e e]
forall a. a -> [a] -> [a]
:) ([Parser e e] -> [Parser e e]) -> [Parser e e] -> [Parser e e]
forall a b. (a -> b) -> a -> b
$
                [Maybe (Parser e e)] -> [Parser e e]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Parser e e)
nonAssoc, Maybe (Parser e e)
preRights, Maybe (Parser e e)
postLefts]
            where
            choice :: forall k.
                      NK k -> [NotationSection] ->
                      Parser e (OperatorType k e)
            choice :: forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK k
k =
              [Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)]
-> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum ([Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)]
 -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e))
-> ([NotationSection]
    -> [Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)])
-> [NotationSection]
-> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
              (NotationSection
 -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e))
-> [NotationSection]
-> [Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)]
forall a b. (a -> b) -> [a] -> [b]
map (\NotationSection
sect ->
                let n :: NewNotation
n = NotationSection -> NewNotation
sectNotation NotationSection
sect

                    inner :: forall k.
                             NK k -> Parser e (OperatorType k e)
                    inner :: forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner = ParseSections
-> Parser e e
-> NewNotation
-> NK k
-> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall e (k :: NotationKind).
IsExpr e =>
ParseSections
-> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
opP ParseSections
parseSections Parser e e
p0 NewNotation
n
                in
                case NK k
k of
                  NK k
In   -> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'InfixNotation
In

                  NK k
Pre  -> if NewNotation -> Bool
isinfix NewNotation
n Bool -> Bool -> Bool
|| NewNotation -> Bool
ispostfix NewNotation
n
                          then ((MaybePlaceholder e -> OperatorType k e)
 -> MaybePlaceholder e -> OperatorType k e)
-> MaybePlaceholder e
-> (MaybePlaceholder e -> OperatorType k e)
-> OperatorType k e
forall a b c. (a -> b -> c) -> b -> a -> c
flip (MaybePlaceholder e -> OperatorType k e)
-> MaybePlaceholder e -> OperatorType k e
forall a b. (a -> b) -> a -> b
($) (MaybePlaceholder e
 -> (MaybePlaceholder e -> OperatorType k e) -> OperatorType k e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     ((MaybePlaceholder e -> OperatorType k e) -> OperatorType k e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PositionInName
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
Beginning
                                        Parser
  MemoKey
  e
  (MaybePlaceholder e)
  ((MaybePlaceholder e -> OperatorType k e) -> OperatorType k e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> OperatorType k e)
-> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'InfixNotation
In
                          else NK 'PrefixNotation -> Parser e (OperatorType 'PrefixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'PrefixNotation
Pre

                  NK k
Post -> if NewNotation -> Bool
isinfix NewNotation
n Bool -> Bool -> Bool
|| NewNotation -> Bool
isprefix NewNotation
n
                          then (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> OperatorType k e
(MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> MaybePlaceholder e -> e
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((MaybePlaceholder e -> MaybePlaceholder e -> e)
 -> MaybePlaceholder e -> OperatorType k e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> OperatorType k e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'InfixNotation
In
                                    Parser
  MemoKey
  e
  (MaybePlaceholder e)
  (MaybePlaceholder e -> OperatorType k e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PositionInName
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
End
                          else NK 'PostfixNotation -> Parser e (OperatorType 'PostfixNotation e)
forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'PostfixNotation
Post

                  NK k
Non  -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
forall a. HasCallStack => a
__IMPOSSIBLE__)

            nonAssoc :: Maybe (Parser e e)
            nonAssoc :: Maybe (Parser e e)
nonAssoc = case (NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
forall a. (a -> Bool) -> [a] -> [a]
filter (Associativity -> NotationSection -> Bool
isInfix Associativity
NonAssoc) [NotationSection]
ops of
              []  -> Maybe (Parser e e)
forall a. Maybe a
Nothing
              [NotationSection]
ops -> Parser e e -> Maybe (Parser e e)
forall a. a -> Maybe a
Just (Parser e e -> Maybe (Parser e e))
-> Parser e e -> Maybe (Parser e e)
forall a b. (a -> b) -> a -> b
$
                (\e
x MaybePlaceholder e -> MaybePlaceholder e -> e
f e
y -> MaybePlaceholder e -> MaybePlaceholder e -> e
f (e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder e
x) (e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder e
y))
                  (e -> (MaybePlaceholder e -> MaybePlaceholder e -> e) -> e -> e)
-> Parser e e
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     ((MaybePlaceholder e -> MaybePlaceholder e -> e) -> e -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
higher
                  Parser
  MemoKey
  e
  (MaybePlaceholder e)
  ((MaybePlaceholder e -> MaybePlaceholder e -> e) -> e -> e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (e -> e)
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NK 'InfixNotation
-> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'InfixNotation
In [NotationSection]
ops
                  Parser MemoKey e (MaybePlaceholder e) (e -> e)
-> Parser e e -> Parser e e
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser e e
higher

            or :: ([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
or [a] -> f a
p1 []   [a] -> f a
p2 []   = Maybe (f a)
forall a. Maybe a
Nothing
            or [a] -> f a
p1 []   [a] -> f a
p2 [a]
ops2 = f a -> Maybe (f a)
forall a. a -> Maybe a
Just ([a] -> f a
p2 [a]
ops2)
            or [a] -> f a
p1 [a]
ops1 [a] -> f a
p2 []   = f a -> Maybe (f a)
forall a. a -> Maybe a
Just ([a] -> f a
p1 [a]
ops1)
            or [a] -> f a
p1 [a]
ops1 [a] -> f a
p2 [a]
ops2 = f a -> Maybe (f a)
forall a. a -> Maybe a
Just ([a] -> f a
p1 [a]
ops1 f a -> f a -> f a
forall a. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [a] -> f a
p2 [a]
ops2)

            preRight :: Maybe (Parser e (MaybePlaceholder e -> e))
            preRight :: Maybe
  (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
preRight =
              ([NotationSection]
 -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
-> [NotationSection]
-> ([NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
-> [NotationSection]
-> Maybe
     (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
forall {f :: * -> *} {a} {a} {a}.
Alternative f =>
([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
or (NK 'PrefixNotation
-> [NotationSection] -> Parser e (OperatorType 'PrefixNotation e)
forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'PrefixNotation
Pre)
                 ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
forall a. (a -> Bool) -> [a] -> [a]
filter NotationSection -> Bool
isPrefix [NotationSection]
ops)
                 (\[NotationSection]
ops -> ((MaybePlaceholder e -> MaybePlaceholder e -> e)
 -> MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e
-> (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e
-> e
forall a b c. (a -> b -> c) -> b -> a -> c
flip (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> MaybePlaceholder e -> e
forall a b. (a -> b) -> a -> b
($) (MaybePlaceholder e
 -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
 -> MaybePlaceholder e
 -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     ((MaybePlaceholder e -> MaybePlaceholder e -> e)
      -> MaybePlaceholder e -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder (e -> MaybePlaceholder e)
-> Parser e e
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
higher)
                                   Parser
  MemoKey
  e
  (MaybePlaceholder e)
  ((MaybePlaceholder e -> MaybePlaceholder e -> e)
   -> MaybePlaceholder e -> e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NK 'InfixNotation
-> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'InfixNotation
In [NotationSection]
ops)
                 ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
forall a. (a -> Bool) -> [a] -> [a]
filter (Associativity -> NotationSection -> Bool
isInfix Associativity
RightAssoc) [NotationSection]
ops)

            preRights :: Maybe (Parser e e)
            preRights :: Maybe (Parser e e)
preRights = do
              Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
preRight <- Maybe
  (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
preRight
              Parser e e -> Maybe (Parser e e)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Parser e e -> Maybe (Parser e e))
-> Parser e e -> Maybe (Parser e e)
forall a b. (a -> b) -> a -> b
$ (Parser e e -> Parser e e) -> Parser e e
forall a. (a -> a) -> a
Data.Function.fix ((Parser e e -> Parser e e) -> Parser e e)
-> (Parser e e -> Parser e e) -> Parser e e
forall a b. (a -> b) -> a -> b
$ \Parser e e
preRights ->
                MemoKey -> Parser e e -> Parser e e
forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoiseIfPrinting (PrecedenceKey -> MemoKey
PreRightsK PrecedenceKey
key) (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$
                  Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
preRight Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser e e
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder (e -> MaybePlaceholder e)
-> Parser e e
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser e e
preRights Parser e e -> Parser e e -> Parser e e
forall a.
Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser e e
higher))

            postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))
            postLeft :: Maybe
  (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
postLeft =
              ([NotationSection]
 -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
-> [NotationSection]
-> ([NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
-> [NotationSection]
-> Maybe
     (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
forall {f :: * -> *} {a} {a} {a}.
Alternative f =>
([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
or (NK 'PostfixNotation
-> [NotationSection] -> Parser e (OperatorType 'PostfixNotation e)
forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'PostfixNotation
Post)
                 ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
forall a. (a -> Bool) -> [a] -> [a]
filter NotationSection -> Bool
isPostfix [NotationSection]
ops)
                 (\[NotationSection]
ops -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> MaybePlaceholder e -> e
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((MaybePlaceholder e -> MaybePlaceholder e -> e)
 -> MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (MaybePlaceholder e -> MaybePlaceholder e -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NK 'InfixNotation
-> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'InfixNotation
In [NotationSection]
ops
                               Parser
  MemoKey
  e
  (MaybePlaceholder e)
  (MaybePlaceholder e -> MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder (e -> MaybePlaceholder e)
-> Parser e e
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
higher))
                 ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
forall a. (a -> Bool) -> [a] -> [a]
filter (Associativity -> NotationSection -> Bool
isInfix Associativity
LeftAssoc) [NotationSection]
ops)

            postLefts :: Maybe (Parser e e)
            postLefts :: Maybe (Parser e e)
postLefts = do
              Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
postLeft <- Maybe
  (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
postLeft
              Parser e e -> Maybe (Parser e e)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Parser e e -> Maybe (Parser e e))
-> Parser e e -> Maybe (Parser e e)
forall a b. (a -> b) -> a -> b
$ (Parser e e -> Parser e e) -> Parser e e
forall a. (a -> a) -> a
Data.Function.fix ((Parser e e -> Parser e e) -> Parser e e)
-> (Parser e e -> Parser e e) -> Parser e e
forall a b. (a -> b) -> a -> b
$ \Parser e e
postLefts ->
                MemoKey -> Parser e e -> Parser e e
forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise (PrecedenceKey -> MemoKey
PostLeftsK PrecedenceKey
key) (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$
                  ((MaybePlaceholder e -> e) -> MaybePlaceholder e -> e)
-> MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e
forall a b c. (a -> b -> c) -> b -> a -> c
flip (MaybePlaceholder e -> e) -> MaybePlaceholder e -> e
forall a b. (a -> b) -> a -> b
($) (MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser
     MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder (e -> MaybePlaceholder e)
-> Parser e e
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser e e
postLefts Parser e e -> Parser e e -> Parser e e
forall a.
Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser e e
higher))
                           Parser
  MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
-> Parser e e
forall a b.
Parser MemoKey e (MaybePlaceholder e) (a -> b)
-> Parser MemoKey e (MaybePlaceholder e) a
-> Parser MemoKey e (MaybePlaceholder e) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
postLeft


---------------------------------------------------------------------------
-- * Parse functions
---------------------------------------------------------------------------

-- | Returns the list of possible parses.
parsePat
  :: ([Pattern] -> [Pattern]) -- ^ Turns a 'RawAppP' into possible parses.
  -> Pattern                  -- ^ Pattern possibly containing 'RawAppP's.
  -> [Pattern]                -- ^ Possible parses, not containing 'RawAppP's.
parsePat :: ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs = \case
    AppP Pattern
p (Arg ArgInfo
info Named_ Pattern
q) ->
        Pattern -> Pattern
forall e. IsExpr e => e -> e
fullParen' (Pattern -> Pattern) -> [Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern -> Arg (Named_ Pattern) -> Pattern
AppP (Pattern -> Arg (Named_ Pattern) -> Pattern)
-> [Pattern] -> [Arg (Named_ Pattern) -> Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs Pattern
p [Arg (Named_ Pattern) -> Pattern]
-> [Arg (Named_ Pattern)] -> [Pattern]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ArgInfo -> Named_ Pattern -> Arg (Named_ Pattern)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Named_ Pattern -> Arg (Named_ Pattern))
-> [Named_ Pattern] -> [Arg (Named_ Pattern)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern -> [Pattern]) -> Named_ Pattern -> [Named_ Pattern]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named NamedName a -> f (Named NamedName b)
traverse (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs) Named_ Pattern
q))
    RawAppP Range
_ List2 Pattern
ps     -> Pattern -> Pattern
forall e. IsExpr e => e -> e
fullParen' (Pattern -> Pattern) -> [Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs (Pattern -> [Pattern]) -> [Pattern] -> [Pattern]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Pattern] -> [Pattern]
prs (List2 Pattern -> [Item (List2 Pattern)]
forall l. IsList l => l -> [Item l]
List2.toList List2 Pattern
ps))
    OpAppP Range
r QName
d Set Name
ns [Arg (Named_ Pattern)]
ps -> Pattern -> Pattern
forall e. IsExpr e => e -> e
fullParen' (Pattern -> Pattern)
-> ([Arg (Named_ Pattern)] -> Pattern)
-> [Arg (Named_ Pattern)]
-> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> QName -> Set Name -> [Arg (Named_ Pattern)] -> Pattern
OpAppP Range
r QName
d Set Name
ns ([Arg (Named_ Pattern)] -> Pattern)
-> [[Arg (Named_ Pattern)]] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
-> [Arg (Named_ Pattern)] -> [[Arg (Named_ Pattern)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
 -> [Arg (Named_ Pattern)] -> [[Arg (Named_ Pattern)]])
-> ((Pattern -> [Pattern])
    -> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
-> (Pattern -> [Pattern])
-> [Arg (Named_ Pattern)]
-> [[Arg (Named_ Pattern)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ Pattern -> [Named_ Pattern])
-> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse ((Named_ Pattern -> [Named_ Pattern])
 -> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
-> ((Pattern -> [Pattern]) -> Named_ Pattern -> [Named_ Pattern])
-> (Pattern -> [Pattern])
-> Arg (Named_ Pattern)
-> [Arg (Named_ Pattern)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> [Pattern]) -> Named_ Pattern -> [Named_ Pattern]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Named NamedName a -> f (Named NamedName b)
traverse) (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs) [Arg (Named_ Pattern)]
ps
    HiddenP Range
_ Named_ Pattern
_      -> String -> [Pattern]
forall a. String -> [a]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"bad hidden argument"
    InstanceP Range
_ Named_ Pattern
_    -> String -> [Pattern]
forall a. String -> [a]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"bad instance argument"
    AsP Range
r Name
x Pattern
p        -> Range -> Name -> Pattern -> Pattern
AsP Range
r Name
x (Pattern -> Pattern) -> [Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs Pattern
p
    p :: Pattern
p@DotP{}         -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    ParenP Range
r Pattern
p       -> Pattern -> Pattern
forall e. IsExpr e => e -> e
fullParen' (Pattern -> Pattern) -> [Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs Pattern
p
    p :: Pattern
p@WildP{}        -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@AbsurdP{}      -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@LitP{}         -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@QuoteP{}       -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@IdentP{}       -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    RecP Range
r [FieldAssignment' Pattern]
fs        -> Range -> [FieldAssignment' Pattern] -> Pattern
RecP Range
r ([FieldAssignment' Pattern] -> Pattern)
-> [[FieldAssignment' Pattern]] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FieldAssignment' Pattern -> [FieldAssignment' Pattern])
-> [FieldAssignment' Pattern] -> [[FieldAssignment' Pattern]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Pattern -> [Pattern])
-> FieldAssignment' Pattern -> [FieldAssignment' Pattern]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
traverse (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs)) [FieldAssignment' Pattern]
fs
    p :: Pattern
p@EqualP{}       -> Pattern -> [Pattern]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p -- Andrea: cargo culted from DotP
    EllipsisP Range
r Maybe Pattern
mp   -> Maybe Pattern -> [Pattern] -> (Pattern -> [Pattern]) -> [Pattern]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Pattern
mp (String -> [Pattern]
forall a. String -> [a]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"bad ellipsis") ((Pattern -> [Pattern]) -> [Pattern])
-> (Pattern -> [Pattern]) -> [Pattern]
forall a b. (a -> b) -> a -> b
$ \Pattern
p ->
                          Range -> Maybe Pattern -> Pattern
EllipsisP Range
r (Maybe Pattern -> Pattern)
-> (Pattern -> Maybe Pattern) -> Pattern -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Pattern) -> [Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs Pattern
p
    WithP Range
r Pattern
p        -> Range -> Pattern -> Pattern
WithP Range
r (Pattern -> Pattern) -> [Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs Pattern
p


{- Implement parsing of copattern left hand sides, e.g.

  record Tree (A : Set) : Set where
    field
      label : A
      child : Bool -> Tree A

  -- corecursive function defined by copattern matching
  alternate : {A : Set}(a b : A) -> Tree A
  -- shallow copatterns
         label (alternate a b)              = a
         child (alternate a b) True         = alternate b a
  -- deep copatterns:
  label (child (alternate a b) False)       = b
  child (child (alternate a b) False) True  = alternate a b
  child (child (alternate a b) False) False = alternate a b

  Delivers an infinite tree

                   a
              b        b
            a   a    a   a
           b b b b  b b b b
                 ...

  Each lhs is a pattern tree with a distinct path of destructors
  ("child", "label") from the root to the defined symbol ("alternate").
  All branches besides this distinct path are patterns.

  Syntax.Concrete.LHSCore represents a lhs
   - the destructor path
   - the side patterns
   - the defined function symbol
   - the applied patterns
-}

-- | The result of 'parseLHS'.
data ParseLHS
  = ParsePattern Pattern    -- ^ We parsed a pattern.
  | ParseLHS QName LHSCore  -- ^ We parsed a lhs.

instance Pretty ParseLHS where
  pretty :: ParseLHS -> Doc
pretty = \case
    ParsePattern Pattern
p  -> Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p
    ParseLHS QName
_f LHSCore
lhs -> LHSCore -> Doc
forall a. Pretty a => a -> Doc
pretty LHSCore
lhs

-- | Parses a left-hand side, workhorse for 'parseLHS'.
--
parseLHS'
  :: LHSOrPatSyn
       -- ^ Are we trying to parse a lhs or a pattern synonym?
       --   For error reporting only!
  -> Maybe QName
       -- ^ Name of the function/patSyn definition if we parse a lhs.
       --   'Nothing' if we parse a pattern.
  -> Pattern
       -- ^ Thing to parse.
  -> ScopeM (ParseLHS, [NotationSection])
       -- ^ The returned list contains all operators/notations/sections that
       -- were used to generate the grammar.

parseLHS' :: LHSOrPatSyn
-> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
parseLHS' LHSOrPatSyn
IsLHS (Just QName
qn) WildP{} =
    (ParseLHS, [NotationSection])
-> ScopeM (ParseLHS, [NotationSection])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> LHSCore -> ParseLHS
ParseLHS QName
qn (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
forall a b. (a -> b) -> a -> b
$ QName -> [Arg (Named_ Pattern)] -> LHSCore
LHSHead QName
qn [], [])

parseLHS' LHSOrPatSyn
lhsOrPatSyn Maybe QName
top Pattern
p = do

    -- Build parser.
    Parsers Pattern
patP <- ExprKind -> [QName] -> ScopeM (Parsers Pattern)
forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
buildParsers ExprKind
IsPattern (Pattern -> [QName]
forall p. CPatternLike p => p -> [QName]
patternQNames Pattern
p)

    -- Run parser, forcing result.
    let ps :: [Pattern]
ps   = let result :: [Pattern]
result = ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat (Parsers Pattern -> [Pattern] -> [Pattern]
forall e. Parsers e -> [e] -> [e]
parser Parsers Pattern
patP) Pattern
p
               in  (Pattern -> () -> ()) -> () -> [Pattern] -> ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Pattern -> () -> ()
forall a b. a -> b -> b
seq () [Pattern]
result () -> [Pattern] -> [Pattern]
forall a b. a -> b -> b
`seq` [Pattern]
result

    -- Classify parse results.
    let cons :: [QName]
cons = KindsOfNames -> FlatScope -> [QName]
getNames ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
ConName, KindOfName
CoConName, KindOfName
PatternSynName])
                        (Parsers Pattern -> FlatScope
forall e. Parsers e -> FlatScope
flattenedScope Parsers Pattern
patP)
    let flds :: [QName]
flds = KindsOfNames -> FlatScope -> [QName]
getNames ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
FldName])
                        (Parsers Pattern -> FlatScope
forall e. Parsers e -> FlatScope
flattenedScope Parsers Pattern
patP)
    let conf :: PatternCheckConfig
conf = Maybe QName
-> (QName -> Bool) -> (QName -> Bool) -> PatternCheckConfig
PatternCheckConfig Maybe QName
top ([QName] -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [QName]
cons) ([QName] -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [QName]
flds)

    let ([Maybe Pattern]
errs, [(Pattern, ParseLHS)]
results) = [Either (Maybe Pattern) (Pattern, ParseLHS)]
-> ([Maybe Pattern], [(Pattern, ParseLHS)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (Maybe Pattern) (Pattern, ParseLHS)]
 -> ([Maybe Pattern], [(Pattern, ParseLHS)]))
-> [Either (Maybe Pattern) (Pattern, ParseLHS)]
-> ([Maybe Pattern], [(Pattern, ParseLHS)])
forall a b. (a -> b) -> a -> b
$ (Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS))
-> [Pattern] -> [Either (Maybe Pattern) (Pattern, ParseLHS)]
forall a b. (a -> b) -> [a] -> [b]
map (PatternCheckConfig
-> Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS)
validPattern PatternCheckConfig
conf) [Pattern]
ps
    String -> Int -> Doc -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
forall (m :: * -> *). MonadDebug m => String -> Int -> Doc -> m ()
reportS String
"scope.operators" Int
60 (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ Doc
"Possible parses for lhs:" ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Pattern, ParseLHS) -> Doc) -> [(Pattern, ParseLHS)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc)
-> ((Pattern, ParseLHS) -> Doc) -> (Pattern, ParseLHS) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseLHS -> Doc
forall a. Pretty a => a -> Doc
pretty (ParseLHS -> Doc)
-> ((Pattern, ParseLHS) -> ParseLHS) -> (Pattern, ParseLHS) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern, ParseLHS) -> ParseLHS
forall a b. (a, b) -> b
snd) [(Pattern, ParseLHS)]
results
    case [(Pattern, ParseLHS)]
results of
        -- Unique result.
        [(Pattern
_,ParseLHS
lhs)] -> do String -> Int -> Doc -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
forall (m :: * -> *). MonadDebug m => String -> Int -> Doc -> m ()
reportS String
"scope.operators" Int
50 (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc
"Parsed lhs:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ParseLHS -> Doc
forall a. Pretty a => a -> Doc
pretty ParseLHS
lhs
                        (ParseLHS, [NotationSection])
-> ScopeM (ParseLHS, [NotationSection])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS
lhs, Parsers Pattern -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Pattern
patP)
        -- No result.
        []        -> TypeError -> ScopeM (ParseLHS, [NotationSection])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM (ParseLHS, [NotationSection]))
-> TypeError -> ScopeM (ParseLHS, [NotationSection])
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (Parsers Pattern -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Pattern
patP)
                               (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
NoParseForLHS LHSOrPatSyn
lhsOrPatSyn ([Maybe Pattern] -> [Pattern]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Pattern]
errs) Pattern
p
        -- Ambiguous result.
        [(Pattern, ParseLHS)]
rs        -> TypeError -> ScopeM (ParseLHS, [NotationSection])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM (ParseLHS, [NotationSection]))
-> TypeError -> ScopeM (ParseLHS, [NotationSection])
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (Parsers Pattern -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Pattern
patP)
                               (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> Pattern -> [Pattern] -> TypeError
AmbiguousParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p ([Pattern] -> TypeError) -> [Pattern] -> TypeError
forall a b. (a -> b) -> a -> b
$
                       ((Pattern, ParseLHS) -> Pattern)
-> [(Pattern, ParseLHS)] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Pattern
forall e. IsExpr e => e -> e
fullParen (Pattern -> Pattern)
-> ((Pattern, ParseLHS) -> Pattern)
-> (Pattern, ParseLHS)
-> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern, ParseLHS) -> Pattern
forall a b. (a, b) -> a
fst) [(Pattern, ParseLHS)]
rs
    where
        getNames :: KindsOfNames -> FlatScope -> [QName]
getNames KindsOfNames
kinds FlatScope
flat =
          (List1 NewNotation -> QName) -> [List1 NewNotation] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> QName
notaName (NewNotation -> QName)
-> (List1 NewNotation -> NewNotation) -> List1 NewNotation -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 NewNotation -> NewNotation
forall a. NonEmpty a -> a
List1.head) ([List1 NewNotation] -> [QName]) -> [List1 NewNotation] -> [QName]
forall a b. (a -> b) -> a -> b
$ KindsOfNames -> FlatScope -> [List1 NewNotation]
getDefinedNames KindsOfNames
kinds FlatScope
flat

        -- The pattern is retained for error reporting in case of ambiguous parses.
        validPattern :: PatternCheckConfig -> Pattern -> PM (Pattern, ParseLHS)
        validPattern :: PatternCheckConfig
-> Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS)
validPattern PatternCheckConfig
conf Pattern
p = do
          ParseLHS
res <- PatternCheckConfig -> Pattern -> PM ParseLHS
classifyPattern PatternCheckConfig
conf Pattern
p
          case (ParseLHS
res, Maybe QName
top) of
            (ParsePattern{}, Maybe QName
Nothing) -> (Pattern, ParseLHS) -> Either (Maybe Pattern) (Pattern, ParseLHS)
forall a. a -> Either (Maybe Pattern) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, ParseLHS
res)  -- expect pattern
            (ParseLHS{}    , Just{} ) -> (Pattern, ParseLHS) -> Either (Maybe Pattern) (Pattern, ParseLHS)
forall a. a -> Either (Maybe Pattern) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, ParseLHS
res)  -- expect lhs
            (ParseLHS, Maybe QName)
_ -> Maybe Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS)
forall a. Maybe Pattern -> Either (Maybe Pattern) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Maybe Pattern
forall a. Maybe a
Nothing

-- | Name sets for classifying a pattern.
data PatternCheckConfig = PatternCheckConfig
  { PatternCheckConfig -> Maybe QName
topName :: Maybe QName    -- ^ Name of defined symbol.
  , PatternCheckConfig -> QName -> Bool
conName :: QName -> Bool  -- ^ Valid constructor name?
  , PatternCheckConfig -> QName -> Bool
fldName :: QName -> Bool  -- ^ Valid field name?
  }

-- | The monad for pattern checking and classification.
--
--   The error message is either empty or a subpattern that was found to be invalid.
type PM = Either (Maybe Pattern)

-- | Returns zero or one classified patterns.
--   In case of zero, return the offending subpattern.
classifyPattern :: PatternCheckConfig -> Pattern -> PM ParseLHS
classifyPattern :: PatternCheckConfig -> Pattern -> PM ParseLHS
classifyPattern PatternCheckConfig
conf Pattern
p =
  case Pattern -> List1 (Arg (Named_ Pattern))
patternAppView Pattern
p of

    -- case @f ps@
    Arg ArgInfo
_ (Named Maybe NamedName
_ (IdentP Bool
_ QName
x)) :| [Arg (Named_ Pattern)]
ps | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== PatternCheckConfig -> Maybe QName
topName PatternCheckConfig
conf -> do
      (Arg (Named_ Pattern) -> Either (Maybe Pattern) ())
-> [Arg (Named_ Pattern)] -> Either (Maybe Pattern) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Pattern -> Either (Maybe Pattern) ()
valid (Pattern -> Either (Maybe Pattern) ())
-> (Arg (Named_ Pattern) -> Pattern)
-> Arg (Named_ Pattern)
-> Either (Maybe Pattern) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg) [Arg (Named_ Pattern)]
ps
      ParseLHS -> PM ParseLHS
forall a. a -> Either (Maybe Pattern) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS -> PM ParseLHS) -> ParseLHS -> PM ParseLHS
forall a b. (a -> b) -> a -> b
$ QName -> LHSCore -> ParseLHS
ParseLHS QName
x (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
forall a b. (a -> b) -> a -> b
$ LHSCore -> [Arg (Named_ Pattern)] -> LHSCore
lhsCoreAddSpine (QName -> [Arg (Named_ Pattern)] -> LHSCore
LHSHead QName
x []) [Arg (Named_ Pattern)]
ps

    -- case @d ps@
    Arg ArgInfo
_ (Named Maybe NamedName
_ (IdentP Bool
_ QName
x)) :| [Arg (Named_ Pattern)]
ps | PatternCheckConfig -> QName -> Bool
fldName PatternCheckConfig
conf QName
x -> do

      -- Step 1: check for valid copattern lhs.
      [NamedArg ParseLHS]
ps0 :: [NamedArg ParseLHS] <- (Arg (Named_ Pattern)
 -> Either (Maybe Pattern) (NamedArg ParseLHS))
-> [Arg (Named_ Pattern)]
-> Either (Maybe Pattern) [NamedArg ParseLHS]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Arg (Named_ Pattern) -> Either (Maybe Pattern) (NamedArg ParseLHS)
classPat [Arg (Named_ Pattern)]
ps
      let ([NamedArg ParseLHS]
ps1, [NamedArg ParseLHS]
rest) = (NamedArg ParseLHS -> Bool)
-> [NamedArg ParseLHS]
-> ([NamedArg ParseLHS], [NamedArg ParseLHS])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (ParseLHS -> Bool
isParsePattern (ParseLHS -> Bool)
-> (NamedArg ParseLHS -> ParseLHS) -> NamedArg ParseLHS -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg ParseLHS -> ParseLHS
forall a. NamedArg a -> a
namedArg) [NamedArg ParseLHS]
ps0
      (NamedArg ParseLHS
p2, [NamedArg ParseLHS]
ps3) <- Maybe Pattern
-> Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
-> Either (Maybe Pattern) (NamedArg ParseLHS, [NamedArg ParseLHS])
forall e a. e -> Maybe a -> Either e a
maybeToEither Maybe Pattern
forall a. Maybe a
Nothing (Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
 -> Either (Maybe Pattern) (NamedArg ParseLHS, [NamedArg ParseLHS]))
-> Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
-> Either (Maybe Pattern) (NamedArg ParseLHS, [NamedArg ParseLHS])
forall a b. (a -> b) -> a -> b
$ [NamedArg ParseLHS]
-> Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
forall a. [a] -> Maybe (a, [a])
uncons [NamedArg ParseLHS]
rest
          -- when (null rest): no field pattern or def pattern found

      -- Ensure that the @ps3@ are patterns rather than lhss.
      (NamedArg ParseLHS -> Either (Maybe Pattern) ())
-> [NamedArg ParseLHS] -> Either (Maybe Pattern) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Pattern -> Bool -> Either (Maybe Pattern) ()
forall e (m :: * -> *). MonadError e m => e -> Bool -> m ()
guardWithError Maybe Pattern
forall a. Maybe a
Nothing (Bool -> Either (Maybe Pattern) ())
-> (NamedArg ParseLHS -> Bool)
-> NamedArg ParseLHS
-> Either (Maybe Pattern) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseLHS -> Bool
isParsePattern (ParseLHS -> Bool)
-> (NamedArg ParseLHS -> ParseLHS) -> NamedArg ParseLHS -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg ParseLHS -> ParseLHS
forall a. NamedArg a -> a
namedArg) [NamedArg ParseLHS]
ps3

      -- Step 2: construct the lhs.
      let (QName
f, LHSCore
lhs0)     = ParseLHS -> (QName, LHSCore)
fromParseLHS (ParseLHS -> (QName, LHSCore)) -> ParseLHS -> (QName, LHSCore)
forall a b. (a -> b) -> a -> b
$ NamedArg ParseLHS -> ParseLHS
forall a. NamedArg a -> a
namedArg NamedArg ParseLHS
p2
          lhs :: NamedArg LHSCore
lhs           = NamedArg ParseLHS -> LHSCore -> NamedArg LHSCore
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg ParseLHS
p2 LHSCore
lhs0
          ([Arg (Named_ Pattern)]
ps', Arg (Named_ Pattern)
_:[Arg (Named_ Pattern)]
ps'') = Int
-> [Arg (Named_ Pattern)]
-> ([Arg (Named_ Pattern)], [Arg (Named_ Pattern)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([NamedArg ParseLHS] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg ParseLHS]
ps1) [Arg (Named_ Pattern)]
ps
      ParseLHS -> PM ParseLHS
forall a. a -> Either (Maybe Pattern) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS -> PM ParseLHS) -> ParseLHS -> PM ParseLHS
forall a b. (a -> b) -> a -> b
$ QName -> LHSCore -> ParseLHS
ParseLHS QName
f (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
forall a b. (a -> b) -> a -> b
$ LHSCore -> [Arg (Named_ Pattern)] -> LHSCore
lhsCoreAddSpine (QName
-> [Arg (Named_ Pattern)]
-> NamedArg LHSCore
-> [Arg (Named_ Pattern)]
-> LHSCore
LHSProj QName
x [Arg (Named_ Pattern)]
ps' NamedArg LHSCore
lhs []) [Arg (Named_ Pattern)]
ps''

    -- case @...@
    Arg ArgInfo
_ (Named Maybe NamedName
_ (EllipsisP Range
r (Just Pattern
p))) :| [Arg (Named_ Pattern)]
ps -> do
      PatternCheckConfig -> Pattern -> PM ParseLHS
classifyPattern PatternCheckConfig
conf Pattern
p PM ParseLHS -> (ParseLHS -> PM ParseLHS) -> PM ParseLHS
forall a b.
Either (Maybe Pattern) a
-> (a -> Either (Maybe Pattern) b) -> Either (Maybe Pattern) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case  -- TODO: avoid re-parsing
        ParsePattern{}    -> Maybe Pattern -> PM ParseLHS
forall a. Maybe Pattern -> Either (Maybe Pattern) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Maybe Pattern
forall a. Maybe a
Nothing
        (ParseLHS QName
f LHSCore
core) -> do
          (Arg (Named_ Pattern) -> Either (Maybe Pattern) ())
-> [Arg (Named_ Pattern)] -> Either (Maybe Pattern) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Pattern -> Either (Maybe Pattern) ()
valid (Pattern -> Either (Maybe Pattern) ())
-> (Arg (Named_ Pattern) -> Pattern)
-> Arg (Named_ Pattern)
-> Either (Maybe Pattern) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg) [Arg (Named_ Pattern)]
ps
          let ellcore :: LHSCore
ellcore = Range -> LHSCore -> LHSCore
LHSEllipsis Range
r LHSCore
core
          ParseLHS -> PM ParseLHS
forall a. a -> Either (Maybe Pattern) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS -> PM ParseLHS) -> ParseLHS -> PM ParseLHS
forall a b. (a -> b) -> a -> b
$ QName -> LHSCore -> ParseLHS
ParseLHS QName
f (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
forall a b. (a -> b) -> a -> b
$ LHSCore -> [Arg (Named_ Pattern)] -> LHSCore
lhsCoreAddSpine LHSCore
ellcore [Arg (Named_ Pattern)]
ps

    -- case: ordinary pattern
    List1 (Arg (Named_ Pattern))
_ -> Pattern -> ParseLHS
ParsePattern Pattern
p ParseLHS -> Either (Maybe Pattern) () -> PM ParseLHS
forall a b.
a -> Either (Maybe Pattern) b -> Either (Maybe Pattern) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Pattern -> Either (Maybe Pattern) ()
valid Pattern
p

  where
  valid :: Pattern -> Either (Maybe Pattern) ()
valid = (QName -> Bool) -> Pattern -> Either (Maybe Pattern) ()
validConPattern ((QName -> Bool) -> Pattern -> Either (Maybe Pattern) ())
-> (QName -> Bool) -> Pattern -> Either (Maybe Pattern) ()
forall a b. (a -> b) -> a -> b
$ PatternCheckConfig -> QName -> Bool
conName PatternCheckConfig
conf

  classPat :: NamedArg Pattern -> PM (NamedArg ParseLHS)
  classPat :: Arg (Named_ Pattern) -> Either (Maybe Pattern) (NamedArg ParseLHS)
classPat = (Named_ Pattern -> Either (Maybe Pattern) (Named_ ParseLHS))
-> Arg (Named_ Pattern)
-> Either (Maybe Pattern) (NamedArg ParseLHS)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Arg a -> m (Arg b)
Trav.mapM ((Pattern -> PM ParseLHS)
-> Named_ Pattern -> Either (Maybe Pattern) (Named_ ParseLHS)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Named NamedName a -> m (Named NamedName b)
Trav.mapM (PatternCheckConfig -> Pattern -> PM ParseLHS
classifyPattern PatternCheckConfig
conf))

  isParsePattern :: ParseLHS -> Bool
isParsePattern = \case
    ParsePattern{} -> Bool
True
    ParseLHS{}     -> Bool
False

  fromParseLHS :: ParseLHS -> (QName, LHSCore)
  fromParseLHS :: ParseLHS -> (QName, LHSCore)
fromParseLHS = \case
    ParseLHS QName
f LHSCore
lhs -> (QName
f, LHSCore
lhs)
    ParsePattern{} -> (QName, LHSCore)
forall a. HasCallStack => a
__IMPOSSIBLE__


-- | Parses a left-hand side, and makes sure that it defined the expected name.
parseLHS :: QName -> Pattern -> ScopeM LHSCore
parseLHS :: QName -> Pattern -> ScopeM LHSCore
parseLHS QName
top Pattern
p = ExprKind -> ScopeM LHSCore -> ScopeM LHSCore
forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
IsPattern (ScopeM LHSCore -> ScopeM LHSCore)
-> ScopeM LHSCore -> ScopeM LHSCore
forall a b. (a -> b) -> a -> b
$ do
  (ParseLHS
res, [NotationSection]
ops) <- LHSOrPatSyn
-> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
parseLHS' LHSOrPatSyn
IsLHS (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
top) Pattern
p
  case ParseLHS
res of
    ParseLHS QName
f LHSCore
lhs -> LHSCore -> ScopeM LHSCore
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return LHSCore
lhs
    ParseLHS
_ -> TypeError -> ScopeM LHSCore
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM LHSCore) -> TypeError -> ScopeM LHSCore
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation [NotationSection]
ops
                   (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
NoParseForLHS LHSOrPatSyn
IsLHS [] Pattern
p

-- | Parses a pattern.
parsePattern :: Pattern -> ScopeM Pattern
parsePattern :: Pattern -> ScopeM Pattern
parsePattern = LHSOrPatSyn -> Pattern -> ScopeM Pattern
parsePatternOrSyn LHSOrPatSyn
IsLHS

parsePatternSyn :: Pattern -> ScopeM Pattern
parsePatternSyn :: Pattern -> ScopeM Pattern
parsePatternSyn = LHSOrPatSyn -> Pattern -> ScopeM Pattern
parsePatternOrSyn LHSOrPatSyn
IsPatSyn

parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
parsePatternOrSyn LHSOrPatSyn
lhsOrPatSyn Pattern
p = ExprKind -> ScopeM Pattern -> ScopeM Pattern
forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
IsPattern (ScopeM Pattern -> ScopeM Pattern)
-> ScopeM Pattern -> ScopeM Pattern
forall a b. (a -> b) -> a -> b
$ do
  (ParseLHS
res, [NotationSection]
ops) <- LHSOrPatSyn
-> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
parseLHS' LHSOrPatSyn
lhsOrPatSyn Maybe QName
forall a. Maybe a
Nothing Pattern
p
  case ParseLHS
res of
    ParsePattern Pattern
p -> Pattern -> ScopeM Pattern
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    ParseLHS
_ -> TypeError -> ScopeM Pattern
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM Pattern) -> TypeError -> ScopeM Pattern
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation [NotationSection]
ops
                   (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
NoParseForLHS LHSOrPatSyn
lhsOrPatSyn [] Pattern
p

-- | Helper function for 'parseLHS' and 'parsePattern'.
--
--   Returns a subpattern that is not a valid constructor pattern
--   or nothing if the whole pattern is a valid constructor pattern.
validConPattern
  :: (QName -> Bool)     -- ^ Test for constructor name.
  -> Pattern             -- ^ Supposedly a constructor pattern.
  -> PM ()   -- ^ Offending subpattern or nothing.
validConPattern :: (QName -> Bool) -> Pattern -> Either (Maybe Pattern) ()
validConPattern QName -> Bool
cons = Pattern -> Either (Maybe Pattern) ()
loop
  where
  loop :: Pattern -> Either (Maybe Pattern) ()
loop Pattern
p = case Pattern -> List1 Pattern
appView Pattern
p of
      WithP Range
_ Pattern
p :| [] -> Pattern -> Either (Maybe Pattern) ()
loop Pattern
p
      Pattern
_ :| []         -> Either (Maybe Pattern) ()
ok
      IdentP Bool
_ QName
x :| [Pattern]
ps
        | QName -> Bool
cons QName
x      -> (Pattern -> Either (Maybe Pattern) ())
-> [Pattern] -> Either (Maybe Pattern) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Pattern -> Either (Maybe Pattern) ()
loop [Pattern]
ps
        | Bool
otherwise   -> Either (Maybe Pattern) ()
failure
      QuoteP Range
_ :| [Pattern
_] -> Either (Maybe Pattern) ()
ok
      DotP Range
_ Expr
e :| [Pattern]
ps  -> (Pattern -> Either (Maybe Pattern) ())
-> [Pattern] -> Either (Maybe Pattern) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Pattern -> Either (Maybe Pattern) ()
loop [Pattern]
ps
      List1 Pattern
_               -> Either (Maybe Pattern) ()
failure
    where
    ok :: Either (Maybe Pattern) ()
ok      = () -> Either (Maybe Pattern) ()
forall a. a -> Either (Maybe Pattern) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    failure :: Either (Maybe Pattern) ()
failure = Maybe Pattern -> Either (Maybe Pattern) ()
forall a. Maybe Pattern -> Either (Maybe Pattern) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Pattern -> Either (Maybe Pattern) ())
-> Maybe Pattern -> Either (Maybe Pattern) ()
forall a b. (a -> b) -> a -> b
$ Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
p


-- | Helper function for 'parseLHS' and 'parsePattern'.
appView :: Pattern -> List1 Pattern
appView :: Pattern -> List1 Pattern
appView = [Pattern] -> Pattern -> List1 Pattern
loop []
  where
  loop :: [Pattern] -> Pattern -> List1 Pattern
loop [Pattern]
acc = \case
    AppP Pattern
p Arg (Named_ Pattern)
a         -> [Pattern] -> Pattern -> List1 Pattern
loop (Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
a Pattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
: [Pattern]
acc) Pattern
p
    OpAppP Range
_ QName
op Set Name
_ [Arg (Named_ Pattern)]
ps -> (Bool -> QName -> Pattern
IdentP Bool
True QName
op Pattern -> [Pattern] -> List1 Pattern
forall a. a -> [a] -> NonEmpty a
:| (Arg (Named_ Pattern) -> Pattern)
-> [Arg (Named_ Pattern)] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg [Arg (Named_ Pattern)]
ps)
                          List1 Pattern -> [Pattern] -> List1 Pattern
forall a. NonEmpty a -> [a] -> NonEmpty a
`List1.appendList`
                        [Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
acc
    ParenP Range
_ Pattern
p       -> [Pattern] -> Pattern -> List1 Pattern
loop [Pattern]
acc Pattern
p
    RawAppP Range
_ List2 Pattern
_      -> List1 Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
    HiddenP Range
_ Named_ Pattern
_      -> List1 Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
    InstanceP Range
_ Named_ Pattern
_    -> List1 Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
    p :: Pattern
p@IdentP{}       -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@WildP{}        -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@AsP{}          -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@AbsurdP{}      -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@LitP{}         -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@QuoteP{}       -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@DotP{}         -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@RecP{}         -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@EqualP{}       -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@EllipsisP{}    -> Pattern -> List1 Pattern
ret Pattern
p
    p :: Pattern
p@WithP{}        -> Pattern -> List1 Pattern
ret Pattern
p
   where
   ret :: Pattern -> List1 Pattern
ret Pattern
p = Pattern
p Pattern -> [Pattern] -> List1 Pattern
forall a. a -> [a] -> NonEmpty a
:| [Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
acc

-- | Return all qualifiers occuring in a list of 'QName's.
--   Each qualifier is returned as a list of names, e.g.
--   for @Data.Nat._+_@ we return the list @[Data,Nat]@.
qualifierModules :: [QName] -> [[Name]]
qualifierModules :: [QName] -> [[Name]]
qualifierModules [QName]
qs =
  ([Name] -> [Name]) -> [[Name]] -> [[Name]]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn [Name] -> [Name]
forall a. a -> a
id ([[Name]] -> [[Name]]) -> [[Name]] -> [[Name]]
forall a b. (a -> b) -> a -> b
$ ([Name] -> Bool) -> [[Name]] -> [[Name]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Name] -> Bool) -> [Name] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([[Name]] -> [[Name]]) -> [[Name]] -> [[Name]]
forall a b. (a -> b) -> a -> b
$ (QName -> [Name]) -> [QName] -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map (NonEmpty Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init (NonEmpty Name -> [Name])
-> (QName -> NonEmpty Name) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> NonEmpty Name
qnameParts) [QName]
qs

-- | Parse a list of expressions (typically from a 'RawApp') into an application.
parseApplication :: List2 Expr -> ScopeM Expr
parseApplication :: List2 Expr -> ScopeM Expr
parseApplication List2 Expr
es  = ExprKind -> ScopeM Expr -> ScopeM Expr
forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
IsExpr (ScopeM Expr -> ScopeM Expr) -> ScopeM Expr -> ScopeM Expr
forall a b. (a -> b) -> a -> b
$ do
    let es0 :: [Item (List2 Expr)]
es0 = List2 Expr -> [Item (List2 Expr)]
forall l. IsList l => l -> [Item l]
List2.toList List2 Expr
es
    -- Build the parser
    Parsers Expr
p <- ExprKind -> [QName] -> ScopeM (Parsers Expr)
forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
buildParsers ExprKind
IsExpr [ QName
q | Ident QName
q <- [Item (List2 Expr)]
[Expr]
es0 ]

    -- Parse
    let result :: [Expr]
result = Parsers Expr -> [Expr] -> [Expr]
forall e. Parsers e -> [e] -> [e]
parser Parsers Expr
p [Item (List2 Expr)]
[Expr]
es0
    case (Expr -> () -> ()) -> () -> [Expr] -> ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Expr -> () -> ()
forall a b. a -> b -> b
seq () [Expr]
result () -> [Expr] -> [Expr]
forall a b. a -> b -> b
`seq` [Expr]
result of
      [Expr
e]   -> do
          String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"scope.operators" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
            Doc
"Parsed an operator application:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
          Expr -> ScopeM Expr
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
      []    -> TypeError -> ScopeM Expr
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM Expr) -> TypeError -> ScopeM Expr
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (Parsers Expr -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Expr
p)
                         (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ List2 Expr -> TypeError
NoParseForApplication List2 Expr
es
      Expr
e:[Expr]
es' -> TypeError -> ScopeM Expr
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM Expr) -> TypeError -> ScopeM Expr
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (Parsers Expr -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Expr
p)
                         (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ List2 Expr -> List1 Expr -> TypeError
AmbiguousParseForApplication List2 Expr
es
                         (List1 Expr -> TypeError) -> List1 Expr -> TypeError
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr) -> List1 Expr -> List1 Expr
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Expr
forall e. IsExpr e => e -> e
fullParen (Expr
e Expr -> [Expr] -> List1 Expr
forall a. a -> [a] -> NonEmpty a
:| [Expr]
es')

parseModuleIdentifier :: Expr -> ScopeM QName
parseModuleIdentifier :: Expr -> ScopeM QName
parseModuleIdentifier (Ident QName
m) = QName -> ScopeM QName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
parseModuleIdentifier Expr
e = TypeError -> ScopeM QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM QName) -> TypeError -> ScopeM QName
forall a b. (a -> b) -> a -> b
$ Expr -> TypeError
NotAModuleExpr Expr
e

parseRawModuleApplication :: List2 Expr -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication :: List2 Expr -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication es :: List2 Expr
es@(List2 Expr
e Expr
e2 [Expr]
rest) = ExprKind
-> ScopeM (QName, [NamedArg Expr])
-> ScopeM (QName, [NamedArg Expr])
forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
IsExpr (ScopeM (QName, [NamedArg Expr])
 -> ScopeM (QName, [NamedArg Expr]))
-> ScopeM (QName, [NamedArg Expr])
-> ScopeM (QName, [NamedArg Expr])
forall a b. (a -> b) -> a -> b
$ do
    let es_args :: [Expr]
es_args = Expr
e2Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
rest
    QName
m <- Expr -> ScopeM QName
parseModuleIdentifier Expr
e

    -- Build the arguments parser
    Parsers Expr
p <- ExprKind -> [QName] -> ScopeM (Parsers Expr)
forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
buildParsers ExprKind
IsExpr [ QName
q | Ident QName
q <- [Expr]
es_args ]

    -- Parse
    -- TODO: not sure about forcing
    case {-force $-} Parsers Expr -> [Expr] -> [[NamedArg Expr]]
forall e. Parsers e -> [e] -> [[NamedArg e]]
argsParser Parsers Expr
p [Expr]
es_args of
        [[NamedArg Expr]
as] -> (QName, [NamedArg Expr]) -> ScopeM (QName, [NamedArg Expr])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
m, [NamedArg Expr]
as)
        []   -> TypeError -> ScopeM (QName, [NamedArg Expr])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM (QName, [NamedArg Expr]))
-> TypeError -> ScopeM (QName, [NamedArg Expr])
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (Parsers Expr -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Expr
p)
                          (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ List2 Expr -> TypeError
NoParseForApplication List2 Expr
es
        [NamedArg Expr]
as : [[NamedArg Expr]]
ass -> do
          let f :: [NamedArg Expr] -> Expr
f = Expr -> Expr
forall e. IsExpr e => e -> e
fullParen (Expr -> Expr)
-> ([NamedArg Expr] -> Expr) -> [NamedArg Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Range -> Expr -> NamedArg Expr -> Expr
App Range
forall a. Range' a
noRange) (QName -> Expr
Ident QName
m)
          TypeError -> ScopeM (QName, [NamedArg Expr])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> ScopeM (QName, [NamedArg Expr]))
-> TypeError -> ScopeM (QName, [NamedArg Expr])
forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (Parsers Expr -> [NotationSection]
forall e. Parsers e -> [NotationSection]
operators Parsers Expr
p)
                    (TypeError -> TypeError) -> TypeError -> TypeError
forall a b. (a -> b) -> a -> b
$ List2 Expr -> List1 Expr -> TypeError
AmbiguousParseForApplication List2 Expr
es
                    (List1 Expr -> TypeError) -> List1 Expr -> TypeError
forall a b. (a -> b) -> a -> b
$ ([NamedArg Expr] -> Expr) -> NonEmpty [NamedArg Expr] -> List1 Expr
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [NamedArg Expr] -> Expr
f ([NamedArg Expr]
as [NamedArg Expr] -> [[NamedArg Expr]] -> NonEmpty [NamedArg Expr]
forall a. a -> [a] -> NonEmpty a
:| [[NamedArg Expr]]
ass)

-- | Parse an expression into a module application
--   (an identifier plus a list of arguments).
parseModuleApplication :: Expr -> ScopeM (QName, [NamedArg Expr])
parseModuleApplication :: Expr -> ScopeM (QName, [NamedArg Expr])
parseModuleApplication (RawApp Range
_ List2 Expr
es) = List2 Expr -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication List2 Expr
es
parseModuleApplication (App Range
r Expr
e1 NamedArg Expr
e2) = do -- TODO: do we need this case?
    (QName
m, [NamedArg Expr]
args) <- Expr -> ScopeM (QName, [NamedArg Expr])
parseModuleApplication Expr
e1
    (QName, [NamedArg Expr]) -> ScopeM (QName, [NamedArg Expr])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
m, [NamedArg Expr]
args [NamedArg Expr] -> [NamedArg Expr] -> [NamedArg Expr]
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr
e2])
parseModuleApplication Expr
e = do
    QName
m <- Expr -> ScopeM QName
parseModuleIdentifier Expr
e
    (QName, [NamedArg Expr]) -> ScopeM (QName, [NamedArg Expr])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
m, [])

---------------------------------------------------------------------------
-- * Inserting parenthesis
---------------------------------------------------------------------------

fullParen :: IsExpr e => e -> e
fullParen :: forall e. IsExpr e => e -> e
fullParen e
e = case e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView (e -> ExprView e) -> e -> ExprView e
forall a b. (a -> b) -> a -> b
$ e -> e
forall e. IsExpr e => e -> e
fullParen' e
e of
    ParenV e
e    -> e
e
    ExprView e
e'          -> ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView ExprView e
e'

fullParen' :: IsExpr e => e -> e
fullParen' :: forall e. IsExpr e => e -> e
fullParen' e
e = case e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView e
e of
    LocalV QName
_     -> e
e
    WildV e
_      -> e
e
    OtherV e
_     -> e
e
    HiddenArgV Named_ e
_ -> e
e
    InstanceArgV Named_ e
_ -> e
e
    ParenV e
_     -> e
e
    AppV e
e1 (Arg ArgInfo
info Named_ e
e2) -> e -> e
par (e -> e) -> e -> e
forall a b. (a -> b) -> a -> b
$ ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (ExprView e -> e) -> ExprView e -> e
forall a b. (a -> b) -> a -> b
$ e -> Arg (Named_ e) -> ExprView e
forall e. e -> NamedArg e -> ExprView e
AppV (e -> e
forall e. IsExpr e => e -> e
fullParen' e
e1) (ArgInfo -> Named_ e -> Arg (Named_ e)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Named_ e
e2')
        where
            e2' :: Named_ e
e2' = case ArgInfo -> Hiding
argInfoHiding ArgInfo
info of
                Hiding
Hidden     -> Named_ e
e2
                Instance{} -> Named_ e
e2
                Hiding
NotHidden  -> e -> e
forall e. IsExpr e => e -> e
fullParen' (e -> e) -> Named_ e -> Named_ e
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Named_ e
e2
    OpAppV QName
x Set Name
ns OpAppArgs' e
es -> e -> e
par (e -> e) -> e -> e
forall a b. (a -> b) -> a -> b
$ ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (ExprView e -> e) -> ExprView e -> e
forall a b. (a -> b) -> a -> b
$ QName -> Set Name -> OpAppArgs' e -> ExprView e
forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
x Set Name
ns (OpAppArgs' e -> ExprView e) -> OpAppArgs' e -> ExprView e
forall a b. (a -> b) -> a -> b
$ ((Arg (Named NamedName (MaybePlaceholder (OpApp e)))
 -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
-> OpAppArgs' e -> OpAppArgs' e
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg (Named NamedName (MaybePlaceholder (OpApp e)))
  -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
 -> OpAppArgs' e -> OpAppArgs' e)
-> ((e -> e)
    -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
    -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
-> (e -> e)
-> OpAppArgs' e
-> OpAppArgs' e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (MaybePlaceholder (OpApp e))
 -> Named NamedName (MaybePlaceholder (OpApp e)))
-> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
-> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (MaybePlaceholder (OpApp e))
  -> Named NamedName (MaybePlaceholder (OpApp e)))
 -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
 -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
-> ((e -> e)
    -> Named NamedName (MaybePlaceholder (OpApp e))
    -> Named NamedName (MaybePlaceholder (OpApp e)))
-> (e -> e)
-> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
-> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
-> Named NamedName (MaybePlaceholder (OpApp e))
-> Named NamedName (MaybePlaceholder (OpApp e))
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
 -> Named NamedName (MaybePlaceholder (OpApp e))
 -> Named NamedName (MaybePlaceholder (OpApp e)))
-> ((e -> e)
    -> MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
-> (e -> e)
-> Named NamedName (MaybePlaceholder (OpApp e))
-> Named NamedName (MaybePlaceholder (OpApp e))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpApp e -> OpApp e)
-> MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e)
forall a b. (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((OpApp e -> OpApp e)
 -> MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
-> ((e -> e) -> OpApp e -> OpApp e)
-> (e -> e)
-> MaybePlaceholder (OpApp e)
-> MaybePlaceholder (OpApp e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> e) -> OpApp e -> OpApp e
forall a b. (a -> b) -> OpApp a -> OpApp b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) e -> e
forall e. IsExpr e => e -> e
fullParen' OpAppArgs' e
es
    LamV List1 LamBinding
bs e
e -> e -> e
par (e -> e) -> e -> e
forall a b. (a -> b) -> a -> b
$ ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (ExprView e -> e) -> ExprView e -> e
forall a b. (a -> b) -> a -> b
$ List1 LamBinding -> e -> ExprView e
forall e. List1 LamBinding -> e -> ExprView e
LamV List1 LamBinding
bs (e -> e
forall e. IsExpr e => e -> e
fullParen e
e)
    where
        par :: e -> e
par = ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (ExprView e -> e) -> (e -> ExprView e) -> e -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> ExprView e
forall e. e -> ExprView e
ParenV