{-# LANGUAGE GADTs #-}

{-| 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.Arrow (second)
import Control.Monad

import Data.Either (partitionEithers)
import qualified Data.Foldable as Fold
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse)
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 qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
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.Either
import Agda.Utils.Pretty
import Agda.Utils.List
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 :: ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
k = Account Phase -> ScopeM a -> ScopeM a
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo
  [ Phase
Bench.Parsing
  , case ExprKind
k of
      ExprKind
IsExpr    -> Phase
Bench.OperatorsExpr
      ExprKind
IsPattern -> Phase
Bench.OperatorsPattern
  ]

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

type FlatScope = Map QName [AbstractName]

-- | Compute all defined names in scope and their fixities/notations.
-- Note that overloaded names (constructors) can have several
-- fixities/notations. Then we 'mergeNotations'. (See issue 1194.)
getDefinedNames :: KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames :: KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames KindsOfNames
kinds FlatScope
names =
  [ [NewNotation] -> [NewNotation]
mergeNotations ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> a -> b
$ (AbstractName -> NewNotation) -> [AbstractName] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> Name -> NewNotation
namesToNotation QName
x (Name -> NewNotation)
-> (AbstractName -> Name) -> AbstractName -> NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) [AbstractName]
ds
  | (QName
x, [AbstractName]
ds) <- FlatScope -> [(QName, [AbstractName])]
forall k a. Map k a -> [(k, a)]
Map.toList FlatScope
names
  , (AbstractName -> Bool) -> [AbstractName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((KindOfName -> KindsOfNames -> Bool
`elemKindsOfNames` KindsOfNames
kinds) (KindOfName -> Bool)
-> (AbstractName -> KindOfName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind) [AbstractName]
ds
  , Bool -> Bool
not ([AbstractName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AbstractName]
ds)
  ]
  -- Andreas, 2013-03-21 see Issue 822
  -- Names can have different kinds, i.e., 'defined' and 'constructor'.
  -- We need to consider all names that have *any* matching kind,
  -- not only those whose first appearing kind is matching.

-- | Compute all names (first component) and operators/notations
-- (second component) in scope.
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames FlatScope
flat = do
  let defs :: [[NewNotation]]
defs = KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames KindsOfNames
allKindsOfNames FlatScope
flat
  [(Name, Name)]
locals <- ((Name, Name) -> Name) -> [(Name, Name)] -> [(Name, Name)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)] -> [(Name, Name)])
-> (LocalVars -> [(Name, Name)]) -> LocalVars -> [(Name, Name)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVars -> [(Name, Name)]
notShadowedLocals (LocalVars -> [(Name, Name)])
-> TCMT IO LocalVars -> TCMT IO [(Name, Name)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
  -- Note: Debug printout aligned with the one in buildParsers.
  VerboseKey -> VerboseLevel -> [VerboseKey] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"scope.operators" VerboseLevel
50
    [ VerboseKey
"flat  = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ FlatScope -> VerboseKey
forall a. Show a => a -> VerboseKey
show FlatScope
flat
    , VerboseKey
"defs  = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [[NewNotation]] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [[NewNotation]]
defs
    , VerboseKey
"locals= " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [(Name, Name)] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [(Name, Name)]
locals
    ]
  let localNots :: [NewNotation]
localNots  = ((Name, Name) -> NewNotation) -> [(Name, Name)] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> NewNotation
localOp [(Name, Name)]
locals
      localNames :: Set QName
localNames = [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 a b. (a -> b) -> [a] -> [b]
map NewNotation -> QName
notaName [NewNotation]
localNots
      otherNots :: [NewNotation]
otherNots  = (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter (\NewNotation
n -> Bool -> Bool
not (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (NewNotation -> QName
notaName NewNotation
n) Set QName
localNames))
                          ([[NewNotation]] -> [NewNotation]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[NewNotation]]
defs)
  ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
forall (m :: * -> *) a. Monad m => a -> m a
return (([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation]))
-> ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ ([NewNotation] -> [NewNotation])
-> ([QName], [NewNotation]) -> ([QName], [NewNotation])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> NewNotation
useDefaultFixity) (([QName], [NewNotation]) -> ([QName], [NewNotation]))
-> ([QName], [NewNotation]) -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ [NewNotation] -> ([QName], [NewNotation])
forall (t :: * -> *).
Foldable t =>
t NewNotation -> ([QName], [NewNotation])
split ([NewNotation] -> ([QName], [NewNotation]))
-> [NewNotation] -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ [NewNotation]
localNots [NewNotation] -> [NewNotation] -> [NewNotation]
forall a. [a] -> [a] -> [a]
++ [NewNotation]
otherNots
  where
    localOp :: (Name, Name) -> NewNotation
localOp (Name
x, Name
y) = QName -> Name -> NewNotation
namesToNotation (Name -> QName
QName Name
x) Name
y
    split :: t NewNotation -> ([QName], [NewNotation])
split t NewNotation
ops      = [Either QName NewNotation] -> ([QName], [NewNotation])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either QName NewNotation] -> ([QName], [NewNotation]))
-> [Either QName NewNotation] -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ (NewNotation -> [Either QName NewNotation])
-> t NewNotation -> [Either QName NewNotation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NewNotation -> [Either QName NewNotation]
opOrNot t NewNotation
ops
    opOrNot :: NewNotation -> [Either QName NewNotation]
opOrNot NewNotation
n      = QName -> Either QName NewNotation
forall a b. a -> Either a b
Left (NewNotation -> QName
notaName NewNotation
n) Either QName NewNotation
-> [Either QName NewNotation] -> [Either QName NewNotation]
forall a. a -> [a] -> [a]
:
                     if [GenPart] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (NewNotation -> [GenPart]
notation NewNotation
n) then [] else [NewNotation -> Either QName NewNotation
forall a b. b -> Either a b
Right NewNotation
n]

-- | A data structure used internally by 'buildParsers'.
data InternalParsers e = InternalParsers
  { InternalParsers e -> Parser e e
pTop    :: Parser e e
  , InternalParsers e -> Parser e e
pApp    :: Parser e e
  , InternalParsers e -> Parser e [NamedArg e]
pArgs   :: Parser e [NamedArg e]
  , InternalParsers e -> Parser e e
pNonfix :: Parser e 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
/= :: ExprKind -> ExprKind -> Bool
$c/= :: ExprKind -> ExprKind -> Bool
== :: ExprKind -> ExprKind -> Bool
$c== :: ExprKind -> ExprKind -> Bool
Eq, VerboseLevel -> ExprKind -> VerboseKey -> VerboseKey
[ExprKind] -> VerboseKey -> VerboseKey
ExprKind -> VerboseKey
(VerboseLevel -> ExprKind -> VerboseKey -> VerboseKey)
-> (ExprKind -> VerboseKey)
-> ([ExprKind] -> VerboseKey -> VerboseKey)
-> Show ExprKind
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [ExprKind] -> VerboseKey -> VerboseKey
$cshowList :: [ExprKind] -> VerboseKey -> VerboseKey
show :: ExprKind -> VerboseKey
$cshow :: ExprKind -> VerboseKey
showsPrec :: VerboseLevel -> ExprKind -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> ExprKind -> VerboseKey -> VerboseKey
Show)

-- | The data returned by 'buildParsers'.

data Parsers e = Parsers
  { Parsers e -> [e] -> [e]
parser :: [e] -> [e]
    -- ^ A parser for expressions or patterns (depending on the
    -- 'ExprKind' argument given to 'buildParsers').
  , Parsers e -> [e] -> [[NamedArg e]]
argsParser :: [e] -> [[NamedArg e]]
    -- ^ A parser for sequences of arguments.
  , Parsers e -> [NotationSection]
operators :: [NotationSection]
    -- ^ All operators/notations/sections that were used to generate
    -- the grammar.
  , 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 'buildParser'.
  }

-- | 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 :: 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]
ops) <- FlatScope -> ScopeM ([QName], [NewNotation])
localNames FlatScope
flat

    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 (Name -> [NamePart]
nameParts (Name -> [NamePart]) -> (QName -> Name) -> QName -> [NamePart]
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 (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 VerboseKey
partsInExpr =
          [VerboseKey] -> Set VerboseKey
forall a. Ord a => [a] -> Set a
Set.fromList [ VerboseKey
s | Id VerboseKey
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 =
          [ VerboseKey -> Set VerboseKey -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member VerboseKey
p Set VerboseKey
partsInExpr
          | VerboseKey
p <- [GenPart] -> [VerboseKey]
stringParts (NewNotation -> [GenPart]
notation NewNotation
n)
          ]

        addHole :: Bool -> VerboseKey -> [NamePart]
addHole Bool
True  VerboseKey
p = [NamePart
Hole, VerboseKey -> NamePart
Id VerboseKey
p]
        addHole Bool
False VerboseKey
p = [VerboseKey -> NamePart
Id VerboseKey
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 -> [GenPart] -> Bool
firstPartPresent Bool
withHole [GenPart]
n =
          [NamePart] -> Trie NamePart () -> Bool
forall k v. Ord k => [k] -> Trie k v -> Bool
Trie.member (Bool -> VerboseKey -> [NamePart]
addHole Bool
withHole VerboseKey
p) Trie NamePart ()
partListsInExpr
          where
          p :: VerboseKey
p = case [GenPart]
n of
            NormalHole{} : IdPart RString
p : [GenPart]
_ -> RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
p
            IdPart RString
p : [GenPart]
_                -> RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
p
            [GenPart]
_                           -> VerboseKey
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 -> [GenPart] -> Bool
lastPartPresent Bool
withHole [GenPart]
n =
          [NamePart] -> Trie NamePart () -> Bool
forall k v. Ord k => [k] -> Trie k v -> Bool
Trie.member (Bool -> VerboseKey -> [NamePart]
addHole Bool
withHole VerboseKey
p) Trie NamePart ()
reversedPartListsInExpr
          where
          p :: VerboseKey
p = case [GenPart] -> [GenPart]
forall a. [a] -> [a]
reverse [GenPart]
n of
            NormalHole{} : IdPart RString
p : [GenPart]
_ -> RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
p
            IdPart RString
p : [GenPart]
_                -> RString -> VerboseKey
forall a. Ranged a -> a
rangedThing RString
p
            [GenPart]
_                           -> VerboseKey
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 -> [GenPart] -> Bool
correctUnderscores Bool
withInitialHole Bool
withFinalHole [GenPart]
n =
          Bool -> [GenPart] -> Bool
firstPartPresent Bool
withInitialHole [GenPart]
n
            Bool -> Bool -> Bool
&&
          Bool -> [GenPart] -> Bool
lastPartPresent  Bool
withFinalHole   [GenPart]
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 -> [GenPart] -> Bool
correctUnderscores Bool
False Bool
False (NewNotation -> [GenPart]
notation NewNotation
n)
            else (VerboseKey -> Bool) -> [VerboseKey] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\VerboseKey
s -> [NamePart] -> Trie NamePart () -> Bool
forall k v. Ord k => [k] -> Trie k v -> Bool
Trie.member [VerboseKey -> NamePart
Id VerboseKey
s] Trie NamePart ()
partListsInExpr)
                     ([GenPart] -> [VerboseKey]
stringParts ([GenPart] -> [VerboseKey]) -> [GenPart] -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ NewNotation -> [GenPart]
notation NewNotation
n)
          ]

        -- Should be used with sections.
        correctUnderscoresSect :: NotationKind -> Notation -> Bool
        correctUnderscoresSect :: NotationKind -> [GenPart] -> Bool
correctUnderscoresSect NotationKind
k [GenPart]
n = case (NotationKind
k, [GenPart] -> NotationKind
notationKind [GenPart]
n) of
          (NotationKind
PrefixNotation,  NotationKind
InfixNotation)   -> Bool -> Bool -> [GenPart] -> Bool
correctUnderscores Bool
True Bool
False [GenPart]
n
          (NotationKind
PostfixNotation, NotationKind
InfixNotation)   -> Bool -> Bool -> [GenPart] -> Bool
correctUnderscores Bool
False Bool
True [GenPart]
n
          (NotationKind
NonfixNotation,  NotationKind
InfixNotation)   -> Bool -> Bool -> [GenPart] -> Bool
correctUnderscores Bool
True Bool
True [GenPart]
n
          (NotationKind
NonfixNotation,  NotationKind
PrefixNotation)  -> Bool -> Bool -> [GenPart] -> Bool
correctUnderscores Bool
False Bool
True [GenPart]
n
          (NotationKind
NonfixNotation,  NotationKind
PostfixNotation) -> Bool -> Bool -> [GenPart] -> Bool
correctUnderscores Bool
True Bool
False [GenPart]
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 :: [[NewNotation]]
cons       = KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames
                       ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
ConName, 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
$
                       ([NewNotation] -> QName) -> [[NewNotation]] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> QName
notaName (NewNotation -> QName)
-> ([NewNotation] -> NewNotation) -> [NewNotation] -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NewNotation] -> NewNotation
forall a. [a] -> a
head) [[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
$
                       [[NewNotation]] -> [NewNotation]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[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 -> [GenPart] -> Bool
correctUnderscoresSect NotationKind
k (NewNotation -> [GenPart]
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 :: Maybe FixityLevel
sectLevel = Maybe FixityLevel
forall a. Maybe a
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 -> [GenPart] -> Bool
correctUnderscoresSect NotationKind
NonfixNotation (NewNotation -> [GenPart]
notation NewNotation
n)
              ]

        -- The triples have the form (level, operators). The lowest
        -- level comes first.
        relatedOperators :: [(PrecedenceLevel, [NotationSection])]
        relatedOperators :: [(PrecedenceLevel, [NotationSection])]
relatedOperators =
          ([(PrecedenceLevel, [NotationSection])]
 -> (PrecedenceLevel, [NotationSection]))
-> [[(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]
++ [[NotationSection]] -> [NotationSection]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (((PrecedenceLevel, [NotationSection]) -> [NotationSection])
-> [(PrecedenceLevel, [NotationSection])] -> [[NotationSection]]
forall a b. (a -> b) -> [a] -> [b]
map (PrecedenceLevel, [NotationSection]) -> [NotationSection]
forall a b. (a, b) -> b
snd [(PrecedenceLevel, [NotationSection])]
rest))) ([[(PrecedenceLevel, [NotationSection])]]
 -> [(PrecedenceLevel, [NotationSection])])
-> ([NewNotation] -> [[(PrecedenceLevel, [NotationSection])]])
-> [NewNotation]
-> [(PrecedenceLevel, [NotationSection])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          ((PrecedenceLevel, [NotationSection])
 -> (PrecedenceLevel, [NotationSection]) -> Bool)
-> [(PrecedenceLevel, [NotationSection])]
-> [[(PrecedenceLevel, [NotationSection])]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (PrecedenceLevel -> PrecedenceLevel -> Bool
forall a. Eq a => a -> a -> Bool
(==) (PrecedenceLevel -> PrecedenceLevel -> Bool)
-> ((PrecedenceLevel, [NotationSection]) -> PrecedenceLevel)
-> (PrecedenceLevel, [NotationSection])
-> (PrecedenceLevel, [NotationSection])
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (PrecedenceLevel, [NotationSection]) -> PrecedenceLevel
forall a b. (a, b) -> a
fst) ([(PrecedenceLevel, [NotationSection])]
 -> [[(PrecedenceLevel, [NotationSection])]])
-> ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
-> [NewNotation]
-> [[(PrecedenceLevel, [NotationSection])]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          ((PrecedenceLevel, [NotationSection])
 -> (PrecedenceLevel, [NotationSection]) -> Ordering)
-> [(PrecedenceLevel, [NotationSection])]
-> [(PrecedenceLevel, [NotationSection])]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (PrecedenceLevel -> PrecedenceLevel -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (PrecedenceLevel -> PrecedenceLevel -> Ordering)
-> ((PrecedenceLevel, [NotationSection]) -> PrecedenceLevel)
-> (PrecedenceLevel, [NotationSection])
-> (PrecedenceLevel, [NotationSection])
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (PrecedenceLevel, [NotationSection]) -> PrecedenceLevel
forall a b. (a, b) -> a
fst) ([(PrecedenceLevel, [NotationSection])]
 -> [(PrecedenceLevel, [NotationSection])])
-> ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
-> [NewNotation]
-> [(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

    VerboseKey -> VerboseLevel -> [VerboseKey] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"scope.operators" VerboseLevel
50
      [ VerboseKey
"unrelatedOperators = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [NotationSection] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [NotationSection]
unrelatedOperators
      , VerboseKey
"nonWithSections    = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [NotationSection] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [NotationSection]
nonWithSections
      , VerboseKey
"relatedOperators   = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [(PrecedenceLevel, [NotationSection])] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [(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 :: forall e.
Parser e e
-> Parser e e
-> Parser e [NamedArg e]
-> Parser e e
-> Parser e e
-> InternalParsers e
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
$
                            ((Parser e e -> Parser e e) -> Parser e e -> Parser e e)
-> Parser e e -> [Parser e e -> Parser e e] -> Parser e e
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (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
pApp InternalParsers e
p)
                              (((PrecedenceLevel, [NotationSection]) -> Parser e e -> Parser e e)
-> [(PrecedenceLevel, [NotationSection])]
-> [Parser e e -> Parser e e]
forall a b. (a -> b) -> [a] -> [b]
map (\(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)
                                   [(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. (a -> b) -> [a] -> [b]
map (\(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]
-> [NotationSection] -> [(PrecedenceLevel, NotationSection)]
forall a b. [a] -> [b] -> [(a, b)]
zip [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])
-> [NotationSection]
-> (NotationSection -> Parser e e)
-> [Parser e e]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (NotationSection -> Parser e e)
-> [NotationSection] -> [Parser e e]
forall a b. (a -> b) -> [a] -> [b]
map [NotationSection]
nonWithSections (\NotationSection
sect ->
                              let n :: NewNotation
n = NotationSection -> NewNotation
sectNotation NotationSection
sect

                                  inner :: forall k. NK k ->
                                           Parser e (OperatorType k e)
                                  inner :: NK k -> Parser e (OperatorType k e)
inner = ParseSections
-> Parser e e -> NewNotation -> NK k -> Parser 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 [GenPart] -> NotationKind
notationKind (NewNotation -> [GenPart]
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 (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 (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 (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 (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__)
              , pAtom :: Parser e e
pAtom   = (QName -> Bool) -> Parser e e
forall e. IsExpr e => (QName -> Bool) -> Parser e e
atomP QName -> Bool
isAtom
              }

    VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"scope.grammar" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
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
$$ VerboseLevel -> Doc -> Doc
nest VerboseLevel
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 (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 :: forall e.
([e] -> [e])
-> ([e] -> [[NamedArg e]])
-> [NotationSection]
-> FlatScope
-> Parsers e
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
. [GenPart] -> NotationKind
notationKind ([GenPart] -> NotationKind)
-> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [GenPart]
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
. [GenPart] -> NotationKind
notationKind ([GenPart] -> NotationKind)
-> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [GenPart]
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
. [GenPart] -> NotationKind
notationKind ([GenPart] -> NotationKind)
-> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [GenPart]
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
. [GenPart] -> NotationKind
notationKind ([GenPart] -> NotationKind)
-> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [GenPart]
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
$
                (if Bool
includeHigher then (Parser e e
higher Parser e e -> [Parser e e] -> [Parser e e]
forall a. a -> [a] -> [a]
:) else [Parser e e] -> [Parser e e]
forall a. a -> a
id) ([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 :: NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK k
k =
              [Parser e (OperatorType k e)] -> Parser e (OperatorType k e)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum ([Parser e (OperatorType k e)] -> Parser e (OperatorType k e))
-> ([NotationSection] -> [Parser e (OperatorType k e)])
-> [NotationSection]
-> Parser e (OperatorType k e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
              (NotationSection -> Parser e (OperatorType k e))
-> [NotationSection] -> [Parser 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 :: NK k -> Parser e (OperatorType k e)
inner = ParseSections
-> Parser e e -> NewNotation -> NK k -> Parser 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 -> 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 (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 -> 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 -> 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 -> MaybePlaceholder e -> e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
-> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
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 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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]) -> Pattern -> [Pattern]
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 (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)
traverse (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs) Named_ Pattern
q))
    RawAppP Range
_ [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 [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)
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)
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)
traverse) (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs) [Arg (Named_ Pattern)]
ps
    HiddenP Range
_ Named_ Pattern
_      -> VerboseKey -> [Pattern]
forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
fail VerboseKey
"bad hidden argument"
    InstanceP Range
_ Named_ Pattern
_    -> VerboseKey -> [Pattern]
forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
fail VerboseKey
"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 (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 (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@AbsurdP{}      -> Pattern -> [Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@LitP{}         -> Pattern -> [Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@QuoteP{}       -> Pattern -> [Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    p :: Pattern
p@IdentP{}       -> Pattern -> [Pattern]
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)
mapM ((Pattern -> [Pattern])
-> FieldAssignment' Pattern -> [FieldAssignment' Pattern]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
parsePat [Pattern] -> [Pattern]
prs)) [FieldAssignment' Pattern]
fs
    p :: Pattern
p@EqualP{}       -> Pattern -> [Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p -- Andrea: cargo culted from DotP
    EllipsisP Range
_      -> VerboseKey -> [Pattern]
forall (m :: * -> *) a. MonadFail m => VerboseKey -> m a
fail VerboseKey
"bad ellipsis"
    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' is either a pattern ('Left') or a lhs ('Right').
type ParseLHS = Either Pattern (QName, LHSCore)

-- | 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) (RawAppP Range
_ [WildP{}]) =
    (ParseLHS, [NotationSection])
-> ScopeM (ParseLHS, [NotationSection])
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName, LHSCore) -> ParseLHS
forall a b. b -> Either a b
Right (QName
qn, 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 (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Pattern -> () -> ()
seq () [Pattern]
result () -> [Pattern] -> [Pattern]
`seq` [Pattern]
result

    -- Classify parse results.
    let cons :: [QName]
cons = KindsOfNames -> FlatScope -> [QName]
getNames ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
ConName, 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] -> [QName] -> PatternCheckConfig
PatternCheckConfig Maybe QName
top [QName]
cons [QName]
flds
    case (Pattern -> Maybe (Pattern, ParseLHS))
-> [Pattern] -> [(Pattern, ParseLHS)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (PatternCheckConfig -> Pattern -> Maybe (Pattern, ParseLHS)
validPattern PatternCheckConfig
conf) [Pattern]
ps of
        -- Unique result.
        [(Pattern
_,ParseLHS
lhs)] -> do VerboseKey -> VerboseLevel -> Doc -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"scope.operators" VerboseLevel
50 (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc
"Parsed lhs:" Doc -> Doc -> Doc
<+> ParseLHS -> Doc
forall a. Pretty a => a -> Doc
pretty ParseLHS
lhs
                        (ParseLHS, [NotationSection])
-> ScopeM (ParseLHS, [NotationSection])
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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 -> TypeError
NoParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p
        -- Ambiguous result.
        [(Pattern, ParseLHS)]
rs        -> TypeError -> ScopeM (ParseLHS, [NotationSection])
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 =
          ([NewNotation] -> QName) -> [[NewNotation]] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> QName
notaName (NewNotation -> QName)
-> ([NewNotation] -> NewNotation) -> [NewNotation] -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NewNotation] -> NewNotation
forall a. [a] -> a
head) ([[NewNotation]] -> [QName]) -> [[NewNotation]] -> [QName]
forall a b. (a -> b) -> a -> b
$ KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames KindsOfNames
kinds FlatScope
flat

        -- The pattern is retained for error reporting in case of ambiguous parses.
        validPattern :: PatternCheckConfig -> Pattern -> Maybe (Pattern, ParseLHS)
        validPattern :: PatternCheckConfig -> Pattern -> Maybe (Pattern, ParseLHS)
validPattern PatternCheckConfig
conf Pattern
p =
          case (PatternCheckConfig -> Pattern -> Maybe ParseLHS
classifyPattern PatternCheckConfig
conf Pattern
p, Maybe QName
top) of
            (Just res :: ParseLHS
res@Left{}, Maybe QName
Nothing) -> (Pattern, ParseLHS) -> Maybe (Pattern, ParseLHS)
forall a. a -> Maybe a
Just (Pattern
p, ParseLHS
res)  -- expect pattern
            (Just res :: ParseLHS
res@Right{}, Just{}) -> (Pattern, ParseLHS) -> Maybe (Pattern, ParseLHS)
forall a. a -> Maybe a
Just (Pattern
p, ParseLHS
res)  -- expect lhs
            (Maybe ParseLHS, Maybe QName)
_ -> Maybe (Pattern, ParseLHS)
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]
conNames :: [QName]     -- ^ Valid constructor names.
  , PatternCheckConfig -> [QName]
fldNames :: [QName]     -- ^ Valid field names.
  }

-- | Returns zero or one classified patterns.
classifyPattern :: PatternCheckConfig -> Pattern -> Maybe ParseLHS
classifyPattern :: PatternCheckConfig -> Pattern -> Maybe ParseLHS
classifyPattern PatternCheckConfig
conf Pattern
p =
  case Pattern -> [Arg (Named_ Pattern)]
patternAppView Pattern
p of

    -- case @f ps@
    Arg ArgInfo
_ (Named Maybe NamedName
_ (IdentP 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
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Pattern) -> Bool) -> [Arg (Named_ Pattern)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Arg (Named_ Pattern) -> Bool
validPat [Arg (Named_ Pattern)]
ps
      ParseLHS -> Maybe ParseLHS
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS -> Maybe ParseLHS) -> ParseLHS -> Maybe ParseLHS
forall a b. (a -> b) -> a -> b
$ (QName, LHSCore) -> ParseLHS
forall a b. b -> Either a b
Right (QName
x, 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 QName
x)) : [Arg (Named_ Pattern)]
ps | QName
x QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PatternCheckConfig -> [QName]
fldNames PatternCheckConfig
conf -> do
      -- ps0 :: [NamedArg ParseLHS]
      [NamedArg ParseLHS]
ps0 <- (Arg (Named_ Pattern) -> Maybe (NamedArg ParseLHS))
-> [Arg (Named_ Pattern)] -> Maybe [NamedArg ParseLHS]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg (Named_ Pattern) -> Maybe (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
forall a b. Either a b -> Bool
isLeft (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) <- [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
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (NamedArg ParseLHS -> Bool) -> [NamedArg ParseLHS] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ParseLHS -> Bool
forall a b. Either a b -> Bool
isLeft (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
      let (QName
f, NamedArg LHSCore
lhs)      = NamedArg ParseLHS -> (QName, NamedArg LHSCore)
forall a b c. NamedArg (Either a (b, c)) -> (b, NamedArg c)
fromR NamedArg ParseLHS
p2
          ([Arg (Named_ Pattern)]
ps', Arg (Named_ Pattern)
_:[Arg (Named_ Pattern)]
ps'') = VerboseLevel
-> [Arg (Named_ Pattern)]
-> ([Arg (Named_ Pattern)], [Arg (Named_ Pattern)])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt ([NamedArg ParseLHS] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg ParseLHS]
ps1) [Arg (Named_ Pattern)]
ps
      ParseLHS -> Maybe ParseLHS
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS -> Maybe ParseLHS) -> ParseLHS -> Maybe ParseLHS
forall a b. (a -> b) -> a -> b
$ (QName, LHSCore) -> ParseLHS
forall a b. b -> Either a b
Right (QName
f, 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: ordinary pattern
    [Arg (Named_ Pattern)]
_ -> do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [QName] -> Pattern -> Bool
validConPattern (PatternCheckConfig -> [QName]
conNames PatternCheckConfig
conf) Pattern
p
      ParseLHS -> Maybe ParseLHS
forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS -> Maybe ParseLHS) -> ParseLHS -> Maybe ParseLHS
forall a b. (a -> b) -> a -> b
$ Pattern -> ParseLHS
forall a b. a -> Either a b
Left Pattern
p

  where -- allNames = conNames conf ++ fldNames conf
        validPat :: Arg (Named_ Pattern) -> Bool
validPat = [QName] -> Pattern -> Bool
validConPattern (PatternCheckConfig -> [QName]
conNames PatternCheckConfig
conf) (Pattern -> Bool)
-> (Arg (Named_ Pattern) -> Pattern)
-> Arg (Named_ Pattern)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg
        classPat :: NamedArg Pattern -> Maybe (NamedArg ParseLHS)
        classPat :: Arg (Named_ Pattern) -> Maybe (NamedArg ParseLHS)
classPat = (Named_ Pattern -> Maybe (Named NamedName ParseLHS))
-> Arg (Named_ Pattern) -> Maybe (NamedArg ParseLHS)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM ((Pattern -> Maybe ParseLHS)
-> Named_ Pattern -> Maybe (Named NamedName ParseLHS)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM (PatternCheckConfig -> Pattern -> Maybe ParseLHS
classifyPattern PatternCheckConfig
conf))
        fromR :: NamedArg (Either a (b, c)) -> (b, NamedArg c)
        fromR :: NamedArg (Either a (b, c)) -> (b, NamedArg c)
fromR (Arg ArgInfo
info (Named Maybe NamedName
n (Right (b
b, c
c)))) = (b
b, ArgInfo -> Named NamedName c -> NamedArg c
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Maybe NamedName -> c -> Named NamedName c
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
n c
c))
        fromR (Arg ArgInfo
info (Named Maybe NamedName
n (Left  a
a     ))) = (b, NamedArg c)
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
    Right (QName
f, LHSCore
lhs) -> LHSCore -> ScopeM LHSCore
forall (m :: * -> *) a. Monad m => a -> m a
return LHSCore
lhs
    ParseLHS
_ -> TypeError -> ScopeM LHSCore
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 -> 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
    Left Pattern
p -> Pattern -> ScopeM Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
    ParseLHS
_      -> TypeError -> ScopeM Pattern
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 -> TypeError
NoParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p

-- | Helper function for 'parseLHS' and 'parsePattern'.
validConPattern :: [QName] -> Pattern -> Bool
validConPattern :: [QName] -> Pattern -> Bool
validConPattern [QName]
cons Pattern
p = case Pattern -> [Pattern]
appView Pattern
p of
    [WithP Range
_ Pattern
p]   -> [QName] -> Pattern -> Bool
validConPattern [QName]
cons Pattern
p
    [Pattern
_]           -> Bool
True
    IdentP QName
x : [Pattern]
ps -> QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem QName
x [QName]
cons Bool -> Bool -> Bool
&& (Pattern -> Bool) -> [Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([QName] -> Pattern -> Bool
validConPattern [QName]
cons) [Pattern]
ps
    [QuoteP Range
_, Pattern
_] -> Bool
True
    DotP Range
_ Expr
e : [Pattern]
ps -> (Pattern -> Bool) -> [Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([QName] -> Pattern -> Bool
validConPattern [QName]
cons) [Pattern]
ps
    [Pattern]
_             -> Bool
False
-- Andreas, 2012-06-04: I do not know why the following line was
-- the catch-all case.  It seems that the new catch-all works also
-- and is more logical.
--    ps            -> all (validConPattern cons) ps

-- | Helper function for 'parseLHS' and 'parsePattern'.
appView :: Pattern -> [Pattern]
appView :: Pattern -> [Pattern]
appView Pattern
p = case Pattern
p of
    AppP Pattern
p Arg (Named_ Pattern)
a         -> Pattern -> [Pattern]
appView Pattern
p [Pattern] -> [Pattern] -> [Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
a]
    OpAppP Range
_ QName
op Set Name
_ [Arg (Named_ Pattern)]
ps -> QName -> Pattern
IdentP QName
op Pattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
: (Arg (Named_ Pattern) -> Pattern)
-> [Arg (Named_ Pattern)] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map Arg (Named_ Pattern) -> Pattern
forall a. NamedArg a -> a
namedArg [Arg (Named_ Pattern)]
ps
    ParenP Range
_ Pattern
p       -> Pattern -> [Pattern]
appView Pattern
p
    RawAppP Range
_ [Pattern]
_      -> [Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
    HiddenP Range
_ Named_ Pattern
_      -> [Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
    InstanceP Range
_ Named_ Pattern
_    -> [Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
    Pattern
_                -> [Pattern
p]

-- | 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 (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 ([Name] -> [Name]
forall a. [a] -> [a]
init ([Name] -> [Name]) -> (QName -> [Name]) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Name]
qnameParts) [QName]
qs

-- | Parse a list of expressions into an application.
parseApplication :: [Expr] -> ScopeM Expr
parseApplication :: [Expr] -> ScopeM Expr
parseApplication [Expr
e] = Expr -> ScopeM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
parseApplication [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
    -- 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 <- [Expr]
es ]

    -- Parse
    let result :: [Expr]
result = Parsers Expr -> [Expr] -> [Expr]
forall e. Parsers e -> [e] -> [e]
parser Parsers Expr
p [Expr]
es
    case (Expr -> () -> ()) -> () -> [Expr] -> ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Expr -> () -> ()
seq () [Expr]
result () -> [Expr] -> [Expr]
`seq` [Expr]
result of
        [Expr
e] -> do
          VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"scope.operators" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
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
<+> Expr -> Doc
forall a. Pretty a => a -> Doc
pretty Expr
e
          Expr -> ScopeM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
        []  -> TypeError -> ScopeM Expr
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
$ [Expr] -> TypeError
NoParseForApplication [Expr]
es
        [Expr]
es' -> TypeError -> ScopeM Expr
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
$ [Expr] -> [Expr] -> TypeError
AmbiguousParseForApplication [Expr]
es
                         ([Expr] -> TypeError) -> [Expr] -> TypeError
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
forall e. IsExpr e => e -> e
fullParen [Expr]
es'

parseModuleIdentifier :: Expr -> ScopeM QName
parseModuleIdentifier :: Expr -> ScopeM QName
parseModuleIdentifier (Ident QName
m) = QName -> ScopeM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
parseModuleIdentifier Expr
e = TypeError -> ScopeM QName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> ScopeM QName) -> TypeError -> ScopeM QName
forall a b. (a -> b) -> a -> b
$ Expr -> TypeError
NotAModuleExpr Expr
e

parseRawModuleApplication :: [Expr] -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication :: [Expr] -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication [Expr]
es = 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 Expr
e : [Expr]
es_args = [Expr]
es
    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 (m :: * -> *) a. Monad m => a -> m a
return (QName
m, [NamedArg Expr]
as)
        []   -> TypeError -> ScopeM (QName, [NamedArg Expr])
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
$ [Expr] -> TypeError
NoParseForApplication [Expr]
es
        [[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 (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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
$ [Expr] -> [Expr] -> TypeError
AmbiguousParseForApplication [Expr]
es
                    ([Expr] -> TypeError) -> [Expr] -> TypeError
forall a b. (a -> b) -> a -> b
$ ([NamedArg Expr] -> Expr) -> [[NamedArg Expr]] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map [NamedArg Expr] -> Expr
f [[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
_ [Expr]
es) = [Expr] -> ScopeM (QName, [NamedArg Expr])
parseRawModuleApplication [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 (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 (m :: * -> *) a. Monad m => a -> m a
return (QName
m, [])

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

fullParen :: IsExpr e => e -> e
fullParen :: 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' :: 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 [NamedArg (MaybePlaceholder (OpApp 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
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> ExprView e
forall e.
QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> ExprView e
OpAppV QName
x Set Name
ns ([NamedArg (MaybePlaceholder (OpApp e))] -> ExprView e)
-> [NamedArg (MaybePlaceholder (OpApp e))] -> ExprView e
forall a b. (a -> b) -> a -> b
$ ((NamedArg (MaybePlaceholder (OpApp e))
 -> NamedArg (MaybePlaceholder (OpApp e)))
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> [NamedArg (MaybePlaceholder (OpApp e))]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg (MaybePlaceholder (OpApp e))
  -> NamedArg (MaybePlaceholder (OpApp e)))
 -> [NamedArg (MaybePlaceholder (OpApp e))]
 -> [NamedArg (MaybePlaceholder (OpApp e))])
-> ((e -> e)
    -> NamedArg (MaybePlaceholder (OpApp e))
    -> NamedArg (MaybePlaceholder (OpApp e)))
-> (e -> e)
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> [NamedArg (MaybePlaceholder (OpApp e))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (MaybePlaceholder (OpApp e))
 -> Named NamedName (MaybePlaceholder (OpApp e)))
-> NamedArg (MaybePlaceholder (OpApp e))
-> NamedArg (MaybePlaceholder (OpApp e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (MaybePlaceholder (OpApp e))
  -> Named NamedName (MaybePlaceholder (OpApp e)))
 -> NamedArg (MaybePlaceholder (OpApp e))
 -> NamedArg (MaybePlaceholder (OpApp e)))
-> ((e -> e)
    -> Named NamedName (MaybePlaceholder (OpApp e))
    -> Named NamedName (MaybePlaceholder (OpApp e)))
-> (e -> e)
-> NamedArg (MaybePlaceholder (OpApp e))
-> NamedArg (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 (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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) e -> e
forall e. IsExpr e => e -> e
fullParen' [NamedArg (MaybePlaceholder (OpApp e))]
es
    LamV [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
$ [LamBinding] -> e -> ExprView e
forall e. [LamBinding] -> e -> ExprView e
LamV [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