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

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

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

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

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

import Data.Either (partitionEithers)
import qualified Data.Foldable as Fold
import 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 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.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Flat
import Agda.Syntax.Scope.Monad

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

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

import Agda.Utils.Impossible

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

-- | Bills the operator parser.

billToParser :: ExprKind -> ScopeM a -> ScopeM a
billToParser :: forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
k = forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> 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
---------------------------------------------------------------------------

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

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

-- | The data returned by 'buildParsers'.

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

-- | Builds parsers for operator applications from all the operators
-- and function symbols in scope.
--
-- When parsing a pattern we do not use bound names. The effect is
-- that unqualified operator parts (that are not constructor parts)
-- can be used as atomic names in the pattern (so they can be
-- rebound). See @test/succeed/OpBind.agda@ for an example.
--
-- When parsing a pattern we also disallow the use of sections, mainly
-- because there is little need for sections in patterns. Note that
-- sections are parsed by splitting up names into multiple tokens
-- (@_+_@ is replaced by @_@, @+@ and @_@), and if we were to support
-- sections in patterns, then we would have to accept certain such
-- sequences of tokens as single pattern variables.

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

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

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

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

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

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

        -- Every regular name part (not holes etc.).
        partsInExpr :: Set RawName
        partsInExpr :: Set String
partsInExpr =
          forall a. Ord a => [a] -> Set a
Set.fromList [ String
s | Id String
s <- 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 =
          [ forall a. Ord a => a -> Set a -> Bool
Set.member String
p Set String
partsInExpr
          | String
p <- Notation -> [String]
stringParts (NewNotation -> Notation
notation NewNotation
n)
          ]

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

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

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

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

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

        -- Should be used with sections.
        correctUnderscoresSect :: NotationKind -> Notation -> Bool
        correctUnderscoresSect :: NotationKind -> Notation -> Bool
correctUnderscoresSect NotationKind
k Notation
n = case (NotationKind
k, Notation -> NotationKind
notationKind Notation
n) of
          (NotationKind
PrefixNotation,  NotationKind
InfixNotation)   -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
True Bool
False Notation
n
          (NotationKind
PostfixNotation, NotationKind
InfixNotation)   -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
False Bool
True Notation
n
          (NotationKind
NonfixNotation,  NotationKind
InfixNotation)   -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
True Bool
True Notation
n
          (NotationKind
NonfixNotation,  NotationKind
PrefixNotation)  -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
False Bool
True Notation
n
          (NotationKind
NonfixNotation,  NotationKind
PostfixNotation) -> Bool -> Bool -> Notation -> Bool
correctUnderscores Bool
True Bool
False Notation
n
          (NotationKind, NotationKind)
_                                  -> 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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition NewNotation -> Bool
nonfix (forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *). Foldable t => t Bool -> Bool
and 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
CoConName, KindOfName
FldName, KindOfName
PatternSynName]) FlatScope
flat
        conNames :: Set QName
conNames   = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$
                       forall a. (a -> Bool) -> [a] -> [a]
filter (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> Set a -> Bool
Set.member Set QName
namesInExpr) forall a b. (a -> b) -> a -> b
$
                       forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> QName
notaName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head) [[NewNotation]]
cons
        conParts :: Set QName
conParts   = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$
                       forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NewNotation -> [QName]
notationNames forall a b. (a -> b) -> a -> b
$
                       forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> [Bool]
partsPresent) forall a b. (a -> b) -> a -> b
$
                       forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[NewNotation]]
cons

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

        isAtom :: QName -> Bool
isAtom QName
x
          | ExprKind
kind forall a. Eq a => a -> a -> Bool
== ExprKind
IsPattern Bool -> Bool -> Bool
&& Bool -> Bool
not (QName -> Bool
isQualified QName
x) =
            Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
conParts) Bool -> Bool -> Bool
|| forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
conNames
          | Bool
otherwise =
            Bool -> Bool
not (forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
allParts) Bool -> Bool -> 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 (forall a. a -> Maybe a
Just FixityLevel
l) Bool
True
              | NewNotation
n <- [NewNotation]
ns
              , NewNotation -> Bool
isinfix NewNotation
n Bool -> Bool -> Bool
&& NewNotation -> Bool
notaIsOperator NewNotation
n
              , NotationKind
k <- [NotationKind
PrefixNotation, NotationKind
PostfixNotation]
              , NotationKind -> Notation -> Bool
correctUnderscoresSect NotationKind
k (NewNotation -> Notation
notation NewNotation
n)
              ]

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

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

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

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

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

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

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

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

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Parsers
      { parser :: [e] -> [e]
parser         = forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
parse (ParseSections
parseSections, forall e. InternalParsers e -> Parser e e
pTop  InternalParsers e
g)
      , argsParser :: [e] -> [[NamedArg e]]
argsParser     = forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
parse (ParseSections
parseSections, 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity

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

        isPrefix, isPostfix :: NotationSection -> Bool
        isPrefix :: NotationSection -> Bool
isPrefix  = (forall a. Eq a => a -> a -> Bool
== NotationKind
PrefixNotation)  forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> NotationKind
sectKind
        isPostfix :: NotationSection -> Bool
isPostfix = (forall a. Eq a => a -> a -> Bool
== NotationKind
PostfixNotation) 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 forall a. Eq a => a -> a -> Bool
== NotationKind
InfixNotation
             Bool -> Bool -> Bool
&&
          Fixity -> Associativity
fixityAssoc (NewNotation -> Fixity
notaFixity (NotationSection -> NewNotation
sectNotation NotationSection
s)) 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 =
            forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise (PrecedenceKey -> MemoKey
NodeK PrecedenceKey
key) forall a b. (a -> b) -> a -> b
$
              forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum forall a b. (a -> b) -> a -> b
$
                (if Bool
includeHigher then (Parser e e
higher forall a. a -> [a] -> [a]
:) else forall a. a -> a
id) forall a b. (a -> b) -> a -> b
$
                forall a. [Maybe a] -> [a]
catMaybes [Maybe (Parser e e)
nonAssoc, Maybe (Parser e e)
preRights, Maybe (Parser e e)
postLefts]
            where
            choice :: forall k.
                      NK k -> [NotationSection] ->
                      Parser e (OperatorType k e)
            choice :: forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK k
k =
              forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Fold.asum forall b c a. (b -> c) -> (a -> b) -> a -> c
.
              forall a b. (a -> b) -> [a] -> [b]
map (\NotationSection
sect ->
                let n :: NewNotation
n = NotationSection -> NewNotation
sectNotation NotationSection
sect

                    inner :: forall k.
                             NK k -> Parser e (OperatorType k e)
                    inner :: forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner = 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   -> 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 forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
Beginning
                                        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'InfixNotation
In
                          else 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 forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'InfixNotation
In
                                    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
End
                          else forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
inner NK 'PostfixNotation
Post

                  NK k
Non  -> forall a. HasCallStack => a
__IMPOSSIBLE__)

            nonAssoc :: Maybe (Parser e e)
            nonAssoc :: Maybe (Parser e e)
nonAssoc = case forall a. (a -> Bool) -> [a] -> [a]
filter (Associativity -> NotationSection -> Bool
isInfix Associativity
NonAssoc) [NotationSection]
ops of
              []  -> forall a. Maybe a
Nothing
              [NotationSection]
ops -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
                (\e
x MaybePlaceholder e -> MaybePlaceholder e -> e
f e
y -> MaybePlaceholder e -> MaybePlaceholder e -> e
f (forall e. e -> MaybePlaceholder e
noPlaceholder e
x) (forall e. e -> MaybePlaceholder e
noPlaceholder e
y))
                  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
higher
                  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'InfixNotation
In [NotationSection]
ops
                  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 []   = forall a. Maybe a
Nothing
            or [a] -> f a
p1 []   [a] -> f a
p2 [a]
ops2 = forall a. a -> Maybe a
Just ([a] -> f a
p2 [a]
ops2)
            or [a] -> f a
p1 [a]
ops1 [a] -> f a
p2 []   = 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 = forall a. a -> Maybe a
Just ([a] -> f a
p1 [a]
ops1 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 =
              forall {f :: * -> *} {a} {a} {a}.
Alternative f =>
([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
or (forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'PrefixNotation
Pre)
                 (forall a. (a -> Bool) -> [a] -> [a]
filter NotationSection -> Bool
isPrefix [NotationSection]
ops)
                 (\[NotationSection]
ops -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall e. e -> MaybePlaceholder e
noPlaceholder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
higher)
                                   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'InfixNotation
In [NotationSection]
ops)
                 (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
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> a
Data.Function.fix forall a b. (a -> b) -> a -> b
$ \Parser e e
preRights ->
                forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoiseIfPrinting (PrecedenceKey -> MemoKey
PreRightsK PrecedenceKey
key) forall a b. (a -> b) -> a -> b
$
                  Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
preRight forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall e. e -> MaybePlaceholder e
noPlaceholder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser e e
preRights 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 =
              forall {f :: * -> *} {a} {a} {a}.
Alternative f =>
([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
or (forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'PostfixNotation
Post)
                 (forall a. (a -> Bool) -> [a] -> [a]
filter NotationSection -> Bool
isPostfix [NotationSection]
ops)
                 (\[NotationSection]
ops -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (k :: NotationKind).
NK k -> [NotationSection] -> Parser e (OperatorType k e)
choice NK 'InfixNotation
In [NotationSection]
ops
                               forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall e. e -> MaybePlaceholder e
noPlaceholder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
higher))
                 (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
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> a
Data.Function.fix forall a b. (a -> b) -> a -> b
$ \Parser e e
postLefts ->
                forall tok. MemoKey -> Parser tok tok -> Parser tok tok
memoise (PrecedenceKey -> MemoKey
PostLeftsK PrecedenceKey
key) forall a b. (a -> b) -> a -> b
$
                  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall e. e -> MaybePlaceholder e
noPlaceholder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser e e
postLefts forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser e e
higher))
                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
postLeft


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

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


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

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

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

  Delivers an infinite tree

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

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

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

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

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

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

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

parseLHS' LHSOrPatSyn
lhsOrPatSyn Maybe QName
top Pattern
p = do

    -- Build parser.
    Parsers Pattern
patP <- forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
buildParsers ExprKind
IsPattern (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 (forall e. Parsers e -> [e] -> [e]
parser Parsers Pattern
patP) Pattern
p
               in  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr seq :: forall a b. a -> b -> b
seq () [Pattern]
result seq :: forall a b. a -> b -> b
`seq` [Pattern]
result

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

    let ([Maybe Pattern]
errs, [(Pattern, ParseLHS)]
results) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (PatternCheckConfig -> Pattern -> PM (Pattern, ParseLHS)
validPattern PatternCheckConfig
conf) [Pattern]
ps
    forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS String
"scope.operators" Int
60 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ Doc
"Possible parses for lhs:" ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Pattern, ParseLHS)]
results
    case [(Pattern, ParseLHS)]
results of
        -- Unique result.
        [(Pattern
_,ParseLHS
lhs)] -> do forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS String
"scope.operators" Int
50 forall a b. (a -> b) -> a -> b
$ Doc
"Parsed lhs:" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty ParseLHS
lhs
                        forall (m :: * -> *) a. Monad m => a -> m a
return (ParseLHS
lhs, forall e. Parsers e -> [NotationSection]
operators Parsers Pattern
patP)
        -- No result.
        []        -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (forall e. Parsers e -> [NotationSection]
operators Parsers Pattern
patP)
                               forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
NoParseForLHS LHSOrPatSyn
lhsOrPatSyn (forall a. [Maybe a] -> [a]
catMaybes [Maybe Pattern]
errs) Pattern
p
        -- Ambiguous result.
        [(Pattern, ParseLHS)]
rs        -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (forall e. Parsers e -> [NotationSection]
operators Parsers Pattern
patP)
                               forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> Pattern -> [Pattern] -> TypeError
AmbiguousParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p forall a b. (a -> b) -> a -> b
$
                       forall a b. (a -> b) -> [a] -> [b]
map (forall e. IsExpr e => e -> e
fullParen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Pattern, ParseLHS)]
rs
    where
        getNames :: KindsOfNames -> FlatScope -> [QName]
getNames KindsOfNames
kinds FlatScope
flat =
          forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> QName
notaName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head) 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 -> PM (Pattern, ParseLHS)
        validPattern :: PatternCheckConfig -> Pattern -> PM (Pattern, ParseLHS)
validPattern PatternCheckConfig
conf Pattern
p = do
          ParseLHS
res <- PatternCheckConfig -> Pattern -> PM ParseLHS
classifyPattern PatternCheckConfig
conf Pattern
p
          case (ParseLHS
res, Maybe QName
top) of
            (ParsePattern{}, Maybe QName
Nothing) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, ParseLHS
res)  -- expect pattern
            (ParseLHS{}    , Just{} ) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, ParseLHS
res)  -- expect lhs
            (ParseLHS, Maybe QName)
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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

  fromParseLHS :: ParseLHS -> (QName, LHSCore)
  fromParseLHS :: ParseLHS -> (QName, LHSCore)
fromParseLHS = \case
    ParseLHS QName
f LHSCore
lhs -> (QName
f, LHSCore
lhs)
    ParsePattern{} -> 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 = forall a. ExprKind -> ScopeM a -> ScopeM a
billToParser ExprKind
IsPattern forall a b. (a -> b) -> a -> b
$ do
  (ParseLHS
res, [NotationSection]
ops) <- LHSOrPatSyn
-> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
parseLHS' LHSOrPatSyn
IsLHS (forall a. a -> Maybe a
Just QName
top) Pattern
p
  case ParseLHS
res of
    ParseLHS QName
f LHSCore
lhs -> forall (m :: * -> *) a. Monad m => a -> m a
return LHSCore
lhs
    ParseLHS
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation [NotationSection]
ops
                   forall a b. (a -> b) -> a -> b
$ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
NoParseForLHS LHSOrPatSyn
IsLHS [] Pattern
p

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

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

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

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


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

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

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

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

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

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

    -- Build the arguments parser
    Parsers Expr
p <- 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 $-} forall e. Parsers e -> [e] -> [[NamedArg e]]
argsParser Parsers Expr
p [Expr]
es_args of
        [[NamedArg Expr]
as] -> forall (m :: * -> *) a. Monad m => a -> m a
return (QName
m, [NamedArg Expr]
as)
        []   -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (forall e. Parsers e -> [NotationSection]
operators Parsers Expr
p)
                          forall a b. (a -> b) -> a -> b
$ List2 Expr -> TypeError
NoParseForApplication List2 Expr
es
        [NamedArg Expr]
as : [[NamedArg Expr]]
ass -> do
          let f :: [NamedArg Expr] -> Expr
f = forall e. IsExpr e => e -> e
fullParen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Range -> Expr -> NamedArg Expr -> Expr
App forall a. Range' a
noRange) (QName -> Expr
Ident QName
m)
          forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [NotationSection] -> TypeError -> TypeError
OperatorInformation (forall e. Parsers e -> [NotationSection]
operators Parsers Expr
p)
                    forall a b. (a -> b) -> a -> b
$ List2 Expr -> List1 Expr -> TypeError
AmbiguousParseForApplication List2 Expr
es
                    forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [NamedArg Expr] -> Expr
f ([NamedArg Expr]
as forall a. a -> [a] -> NonEmpty a
:| [[NamedArg Expr]]
ass)

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

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

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

fullParen' :: IsExpr e => e -> e
fullParen' :: forall e. IsExpr e => e -> e
fullParen' e
e = case 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 forall a b. (a -> b) -> a -> b
$ forall e. IsExpr e => ExprView e -> e
unExprView forall a b. (a -> b) -> a -> b
$ forall e. e -> NamedArg e -> ExprView e
AppV (forall e. IsExpr e => e -> e
fullParen' e
e1) (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  -> forall e. IsExpr e => e -> e
fullParen' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Named_ e
e2
    OpAppV QName
x Set Name
ns OpAppArgs' e
es -> e -> e
par forall a b. (a -> b) -> a -> b
$ forall e. IsExpr e => ExprView e -> e
unExprView forall a b. (a -> b) -> a -> b
$ forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
x Set Name
ns forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall e. IsExpr e => e -> e
fullParen' OpAppArgs' e
es
    LamV List1 LamBinding
bs e
e -> e -> e
par forall a b. (a -> b) -> a -> b
$ forall e. IsExpr e => ExprView e -> e
unExprView forall a b. (a -> b) -> a -> b
$ forall e. List1 LamBinding -> e -> ExprView e
LamV List1 LamBinding
bs (forall e. IsExpr e => e -> e
fullParen e
e)
    where
        par :: e -> e
par = forall e. IsExpr e => ExprView e -> e
unExprView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> ExprView e
ParenV