{-# LANGUAGE GADTs        #-}
{-# LANGUAGE DataKinds    #-}

module Agda.Syntax.Concrete.Operators.Parser where

import Control.Applicative ( Alternative((<|>), many) )
import Control.Monad ((<=<))

import Data.Either
import Data.Function (on)
import Data.Kind ( Type )
import qualified Data.List as List
import Data.Maybe
import qualified Data.Strict.Maybe as Strict
import Data.Set (Set)

import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Notation
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Operators.Parser.Monad hiding (parse)
import qualified Agda.Syntax.Concrete.Operators.Parser.Monad as P

import Agda.Utils.Pretty
import Agda.Utils.List  ( spanEnd )
import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Singleton

import Agda.Utils.Impossible

placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
placeholder :: forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
p =
  forall tok a. Doc -> Parser tok a -> Parser tok a
doc ([Char] -> Doc
text ([Char]
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show PositionInName
p)) forall a b. (a -> b) -> a -> b
$
  forall tok.
(MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok)
sat forall a b. (a -> b) -> a -> b
$ \case
    Placeholder PositionInName
p' | PositionInName
p' forall a. Eq a => a -> a -> Bool
== PositionInName
p -> Bool
True
    MaybePlaceholder e
_                        -> Bool
False

maybePlaceholder ::
  Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
maybePlaceholder :: forall e.
Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
maybePlaceholder Maybe PositionInName
mp Parser e e
p = case Maybe PositionInName
mp of
  Maybe PositionInName
Nothing -> Parser e (MaybePlaceholder e)
p'
  Just PositionInName
h  -> forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
h forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser e (MaybePlaceholder e)
p'
  where
  p' :: Parser e (MaybePlaceholder e)
p' = forall e. e -> MaybePlaceholder e
noPlaceholder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
p

satNoPlaceholder :: (e -> Maybe a) -> Parser e a
satNoPlaceholder :: forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder e -> Maybe a
p = forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
sat' forall a b. (a -> b) -> a -> b
$ \case
    NoPlaceholder Maybe PositionInName
_ e
e -> e -> Maybe a
p e
e
    Placeholder PositionInName
_     -> forall a. Maybe a
Nothing

data ExprView e
    = LocalV QName
    | WildV e
    | OtherV e
    | AppV e (NamedArg e)
    | OpAppV QName (Set A.Name) (OpAppArgs' e)
      -- ^ The 'QName' is possibly ambiguous, but it must correspond
      -- to one of the names in the set.
    | HiddenArgV (Named_ e)
    | InstanceArgV (Named_ e)
    | LamV (List1 LamBinding) e
    | ParenV e
--    deriving (Show)

class HasRange e => IsExpr e where
  exprView    :: e -> ExprView e
  unExprView  :: ExprView e -> e
  patternView :: e -> Maybe Pattern

instance IsExpr e => HasRange (ExprView e) where
  getRange :: ExprView e -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. IsExpr e => ExprView e -> e
unExprView

instance IsExpr Expr where
    exprView :: Expr -> ExprView Expr
exprView = \case
        Ident QName
x         -> forall e. QName -> ExprView e
LocalV QName
x
        App Range
_ Expr
e1 NamedArg Expr
e2     -> forall e. e -> NamedArg e -> ExprView e
AppV Expr
e1 NamedArg Expr
e2
        OpApp Range
r QName
d Set Name
ns OpAppArgs
es -> forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
d Set Name
ns OpAppArgs
es
        HiddenArg Range
_ Named_ Expr
e   -> forall e. Named_ e -> ExprView e
HiddenArgV Named_ Expr
e
        InstanceArg Range
_ Named_ Expr
e -> forall e. Named_ e -> ExprView e
InstanceArgV Named_ Expr
e
        Paren Range
_ Expr
e       -> forall e. e -> ExprView e
ParenV Expr
e
        Lam Range
_ List1 LamBinding
bs    Expr
e   -> forall e. List1 LamBinding -> e -> ExprView e
LamV List1 LamBinding
bs Expr
e
        e :: Expr
e@Underscore{}  -> forall e. e -> ExprView e
WildV Expr
e
        Expr
e               -> forall e. e -> ExprView e
OtherV Expr
e
    unExprView :: ExprView Expr -> Expr
unExprView = \case
        LocalV QName
x       -> QName -> Expr
Ident QName
x
        AppV Expr
e1 NamedArg Expr
e2     -> Range -> Expr -> NamedArg Expr -> Expr
App (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Expr
e1 NamedArg Expr
e2) Expr
e1 NamedArg Expr
e2
        OpAppV QName
d Set Name
ns OpAppArgs
es -> Range -> QName -> Set Name -> OpAppArgs -> Expr
OpApp (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
d OpAppArgs
es) QName
d Set Name
ns OpAppArgs
es
        HiddenArgV Named_ Expr
e   -> Range -> Named_ Expr -> Expr
HiddenArg (forall a. HasRange a => a -> Range
getRange Named_ Expr
e) Named_ Expr
e
        InstanceArgV Named_ Expr
e -> Range -> Named_ Expr -> Expr
InstanceArg (forall a. HasRange a => a -> Range
getRange Named_ Expr
e) Named_ Expr
e
        ParenV Expr
e       -> Range -> Expr -> Expr
Paren (forall a. HasRange a => a -> Range
getRange Expr
e) Expr
e
        LamV List1 LamBinding
bs Expr
e      -> Range -> List1 LamBinding -> Expr -> Expr
Lam (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange List1 LamBinding
bs Expr
e) List1 LamBinding
bs Expr
e
        WildV Expr
e        -> Expr
e
        OtherV Expr
e       -> Expr
e

    patternView :: Expr -> Maybe Pattern
patternView = Expr -> Maybe Pattern
isPattern

instance IsExpr Pattern where
    exprView :: Pattern -> ExprView Pattern
exprView = \case
        IdentP QName
x         -> forall e. QName -> ExprView e
LocalV QName
x
        AppP Pattern
e1 NamedArg Pattern
e2       -> forall e. e -> NamedArg e -> ExprView e
AppV Pattern
e1 NamedArg Pattern
e2
        OpAppP Range
r QName
d Set Name
ns [NamedArg Pattern]
es -> forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
d 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 e. e -> MaybePlaceholder e
noPlaceholder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> OpApp e
Ordinary) [NamedArg Pattern]
es
        HiddenP Range
_ Named_ Pattern
e      -> forall e. Named_ e -> ExprView e
HiddenArgV Named_ Pattern
e
        InstanceP Range
_ Named_ Pattern
e    -> forall e. Named_ e -> ExprView e
InstanceArgV Named_ Pattern
e
        ParenP Range
_ Pattern
e       -> forall e. e -> ExprView e
ParenV Pattern
e
        e :: Pattern
e@WildP{}        -> forall e. e -> ExprView e
WildV Pattern
e
        Pattern
e                -> forall e. e -> ExprView e
OtherV Pattern
e
    unExprView :: ExprView Pattern -> Pattern
unExprView = \case
        LocalV QName
x       -> QName -> Pattern
IdentP QName
x
        AppV Pattern
e1 NamedArg Pattern
e2     -> Pattern -> NamedArg Pattern -> Pattern
AppP Pattern
e1 NamedArg Pattern
e2
        OpAppV QName
d Set Name
ns OpAppArgs' Pattern
es -> let ess :: [NamedArg Pattern]
                              ess :: [NamedArg Pattern]
ess = (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)
                                      (\case
                                          Placeholder{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
                                          NoPlaceholder Maybe PositionInName
_ OpApp Pattern
x -> forall e. e -> OpApp e -> e
fromOrdinary forall a. HasCallStack => a
__IMPOSSIBLE__ OpApp Pattern
x)
                                      OpAppArgs' Pattern
es
                          in Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
OpAppP (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
d [NamedArg Pattern]
ess) QName
d Set Name
ns [NamedArg Pattern]
ess
        HiddenArgV Named_ Pattern
e   -> Range -> Named_ Pattern -> Pattern
HiddenP (forall a. HasRange a => a -> Range
getRange Named_ Pattern
e) Named_ Pattern
e
        InstanceArgV Named_ Pattern
e -> Range -> Named_ Pattern -> Pattern
InstanceP (forall a. HasRange a => a -> Range
getRange Named_ Pattern
e) Named_ Pattern
e
        ParenV Pattern
e       -> Range -> Pattern -> Pattern
ParenP (forall a. HasRange a => a -> Range
getRange Pattern
e) Pattern
e
        LamV List1 LamBinding
_ Pattern
_       -> forall a. HasCallStack => a
__IMPOSSIBLE__
        WildV Pattern
e        -> Pattern
e
        OtherV Pattern
e       -> Pattern
e

    patternView :: Pattern -> Maybe Pattern
patternView = forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Should sections be parsed?
data ParseSections = ParseSections | DoNotParseSections
  deriving (ParseSections -> ParseSections -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ParseSections -> ParseSections -> Bool
$c/= :: ParseSections -> ParseSections -> Bool
== :: ParseSections -> ParseSections -> Bool
$c== :: ParseSections -> ParseSections -> Bool
Eq, Int -> ParseSections -> ShowS
[ParseSections] -> ShowS
ParseSections -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ParseSections] -> ShowS
$cshowList :: [ParseSections] -> ShowS
show :: ParseSections -> [Char]
$cshow :: ParseSections -> [Char]
showsPrec :: Int -> ParseSections -> ShowS
$cshowsPrec :: Int -> ParseSections -> ShowS
Show)

-- | Runs a parser. If sections should be parsed, then identifiers
-- with at least two name parts are split up into multiple tokens,
-- using 'PositionInName' to record the tokens' original positions
-- within their respective identifiers.

parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
parse :: forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
parse (ParseSections
DoNotParseSections, Parser e a
p) [e]
es = forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
P.parse Parser e a
p (forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> MaybePlaceholder e
noPlaceholder [e]
es)
parse (ParseSections
ParseSections,      Parser e a
p) [e]
es = forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
P.parse Parser e a
p (forall a. [List1 a] -> [a]
List1.concat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. IsExpr e => e -> List1 (MaybePlaceholder e)
splitExpr [e]
es)
  where
  splitExpr :: IsExpr e => e -> List1 (MaybePlaceholder e)
  splitExpr :: forall e. IsExpr e => e -> List1 (MaybePlaceholder e)
splitExpr e
e = case forall e. IsExpr e => e -> ExprView e
exprView e
e of
    LocalV QName
n -> QName -> NonEmpty (MaybePlaceholder e)
splitName QName
n
    ExprView e
_        -> NonEmpty (MaybePlaceholder e)
noSplit
    where
    noSplit :: NonEmpty (MaybePlaceholder e)
noSplit = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall e. e -> MaybePlaceholder e
noPlaceholder e
e

    splitName :: QName -> NonEmpty (MaybePlaceholder e)
splitName QName
n = case forall a. NonEmpty a -> a
List1.last List1 Name
ns of
      Name Range
r NameInScope
nis ps :: NameParts
ps@(NamePart
_ :| NamePart
_ : [NamePart]
_) -> forall {e}.
IsExpr e =>
Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
splitParts Range
r NameInScope
nis (forall a. NonEmpty a -> [a]
List1.init List1 Name
ns) PositionInName
Beginning NameParts
ps
      Name
_                          -> NonEmpty (MaybePlaceholder e)
noSplit
      where
      ns :: List1 Name
ns = QName -> List1 Name
qnameParts QName
n

      -- Note that the same range is used for every name part. This is
      -- not entirely correct, but will hopefully not lead to any
      -- problems.

      -- Note also that the module qualifier, if any, is only applied
      -- to the first name part.

      splitParts :: Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
splitParts Range
_ NameInScope
_   [Name]
_ PositionInName
_ (NamePart
Hole :| [])     = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
End
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
_ (Id [Char]
s :| [])     = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall {e} {t :: * -> *}.
(IsExpr e, Foldable t) =>
Range
-> NameInScope
-> t Name
-> PositionInName
-> [Char]
-> MaybePlaceholder e
part Range
r NameInScope
nis [Name]
m PositionInName
End [Char]
s
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
w (NamePart
Hole :| NamePart
p : [NamePart]
ps) = forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
w    forall a. a -> NonEmpty a -> NonEmpty a
<| Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
splitParts Range
r NameInScope
nis [Name]
m  PositionInName
Middle (NamePart
p forall a. a -> [a] -> NonEmpty a
:| [NamePart]
ps)
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
w (Id [Char]
s :| NamePart
p : [NamePart]
ps) = forall {e} {t :: * -> *}.
(IsExpr e, Foldable t) =>
Range
-> NameInScope
-> t Name
-> PositionInName
-> [Char]
-> MaybePlaceholder e
part Range
r NameInScope
nis [Name]
m PositionInName
w [Char]
s forall a. a -> NonEmpty a -> NonEmpty a
<| Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
splitParts Range
r NameInScope
nis [] PositionInName
Middle (NamePart
p forall a. a -> [a] -> NonEmpty a
:| [NamePart]
ps)

      part :: Range
-> NameInScope
-> t Name
-> PositionInName
-> [Char]
-> MaybePlaceholder e
part Range
r NameInScope
nis t Name
m PositionInName
w [Char]
s =
        forall e. Maybe PositionInName -> e -> MaybePlaceholder e
NoPlaceholder (forall a. a -> Maybe a
Strict.Just PositionInName
w)
                      (forall e. IsExpr e => ExprView e -> e
unExprView forall a b. (a -> b) -> a -> b
$ forall e. QName -> ExprView e
LocalV forall a b. (a -> b) -> a -> b
$
                         forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
Qual (Name -> QName
QName forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> NameParts -> Name
Name Range
r NameInScope
nis forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ [Char] -> NamePart
Id [Char]
s) t Name
m)

---------------------------------------------------------------------------
-- * Parser combinators
---------------------------------------------------------------------------

----------------------------
-- Specific combinators

-- | Parse a specific identifier as a NamePart
partP :: IsExpr e => [Name] -> RawName -> Parser e Range
partP :: forall e. IsExpr e => [Name] -> [Char] -> Parser e Range
partP [Name]
ms [Char]
s =
  forall tok a. Doc -> Parser tok a -> Parser tok a
doc ([Char] -> Doc
text (forall a. Show a => a -> [Char]
show [Char]
str)) forall a b. (a -> b) -> a -> b
$
  forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder e -> Maybe Range
isLocal
  where
  str :: [Char]
str = forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
Qual (Name -> QName
QName forall a b. (a -> b) -> a -> b
$ [Char] -> Name
simpleName [Char]
s) [Name]
ms
  isLocal :: e -> Maybe Range
isLocal e
e = case forall e. IsExpr e => e -> ExprView e
exprView e
e of
      LocalV QName
y | [Char]
str forall a. Eq a => a -> a -> Bool
== forall a. Pretty a => a -> [Char]
prettyShow QName
y -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange QName
y
      ExprView e
_ -> forall a. Maybe a
Nothing

-- | Parses a split-up, unqualified name consisting of at least two
-- name parts.
--
-- The parser does not check that underscores and other name parts
-- alternate. The range of the resulting name is the range of the
-- first name part that is not an underscore.

atLeastTwoParts :: IsExpr e => Parser e Name
atLeastTwoParts :: forall e. IsExpr e => Parser e Name
atLeastTwoParts =
  (\(Maybe (Range, NameInScope), NamePart)
p1 [(Maybe (Range, NameInScope), NamePart)]
ps (Maybe (Range, NameInScope), NamePart)
p2 ->
      let all :: NonEmpty (Maybe (Range, NameInScope), NamePart)
all = (Maybe (Range, NameInScope), NamePart)
p1 forall a. a -> [a] -> NonEmpty a
:| [(Maybe (Range, NameInScope), NamePart)]
ps forall a. [a] -> [a] -> [a]
++ [(Maybe (Range, NameInScope), NamePart)
p2] in
      case forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe forall a b. (a, b) -> a
fst NonEmpty (Maybe (Range, NameInScope), NamePart)
all of
        (Range
r,NameInScope
nis) : [(Range, NameInScope)]
_ -> Range -> NameInScope -> NameParts -> Name
Name Range
r NameInScope
nis (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd NonEmpty (Maybe (Range, NameInScope), NamePart)
all)
        []          -> forall a. HasCallStack => a
__IMPOSSIBLE__)
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {e}.
IsExpr e =>
PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
part PositionInName
Beginning
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall {e}.
IsExpr e =>
PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
part PositionInName
Middle)
  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {e}.
IsExpr e =>
PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
part PositionInName
End
  where
  part :: PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
part PositionInName
pos = forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
sat' forall a b. (a -> b) -> a -> b
$ \case
    Placeholder PositionInName
pos'                   | PositionInName
pos forall a. Eq a => a -> a -> Bool
== PositionInName
pos' -> forall a. a -> Maybe a
Just ( forall a. Maybe a
Nothing
                                                             , NamePart
Hole
                                                             )
    NoPlaceholder (Strict.Just PositionInName
pos') e
e | PositionInName
pos forall a. Eq a => a -> a -> Bool
== PositionInName
pos' ->
      case forall e. IsExpr e => e -> ExprView e
exprView e
e of
        LocalV (QName (Name Range
r NameInScope
nis (Id [Char]
s :| []))) -> forall a. a -> Maybe a
Just (forall a. a -> Maybe a
Just (Range
r, NameInScope
nis), [Char] -> NamePart
Id [Char]
s)
        ExprView e
_ -> forall a. Maybe a
Nothing
    MaybePlaceholder e
_ -> forall a. Maybe a
Nothing

-- | Parses a potentially pattern-matching binder

patternBinder :: IsExpr e => Parser e Binder
patternBinder :: forall e. IsExpr e => Parser e Binder
patternBinder = Parser MemoKey e (MaybePlaceholder e) Binder
inOnePart forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Binder
mkBinder_ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e. IsExpr e => Parser e Name
atLeastTwoParts
  where inOnePart :: Parser MemoKey e (MaybePlaceholder e) Binder
inOnePart = forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder forall a b. (a -> b) -> a -> b
$ Pattern -> Maybe Binder
isBinderP forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e. IsExpr e => e -> Maybe Pattern
patternView

-- | Used to define the return type of 'opP'.

type family OperatorType (k :: NotationKind) (e :: Type) :: Type
type instance OperatorType 'InfixNotation   e = MaybePlaceholder e -> MaybePlaceholder e -> e
type instance OperatorType 'PrefixNotation  e = MaybePlaceholder e -> e
type instance OperatorType 'PostfixNotation e = MaybePlaceholder e -> e
type instance OperatorType 'NonfixNotation  e = e

-- | A singleton type for 'NotationKind' (except for the constructor
-- 'NoNotation').

data NK (k :: NotationKind) :: Type where
  In   :: NK 'InfixNotation
  Pre  :: NK 'PrefixNotation
  Post :: NK 'PostfixNotation
  Non  :: NK 'NonfixNotation

-- | Parse the \"operator part\" of the given notation.
--
-- Normal holes (but not binders) at the beginning and end are
-- ignored.
--
-- If the notation does not contain any binders, then a section
-- notation is allowed.
opP :: forall e k. IsExpr e
    => ParseSections
    -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
opP :: forall e (k :: NotationKind).
IsExpr e =>
ParseSections
-> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
opP ParseSections
parseSections Parser e e
p (NewNotation QName
q Set Name
names Fixity
_ Notation
syn Bool
isOp) NK k
kind =
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name]
-> Notation
-> Parser
     e
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
worker (forall a. NonEmpty a -> [a]
List1.init forall a b. (a -> b) -> a -> b
$ QName -> List1 Name
qnameParts QName
q)
                    Notation
withoutExternalHoles) forall a b. (a -> b) -> a -> b
$ \(Range
range, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
hs) ->

  let ([(MaybePlaceholder e, NamedArg (Ranged Int))]
normal, [(LamBinding, Ranged BoundVariablePosition)]
binders) = forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
hs
      lastHole :: Int
lastHole          = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ (-Int
1) forall a. a -> [a] -> [a]
: forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe NotationPart -> Maybe Int
holeTarget Notation
syn

      app :: ([(MaybePlaceholder e, NamedArg (Ranged Int))] ->
              [(MaybePlaceholder e, NamedArg (Ranged Int))]) -> e
      app :: ([(MaybePlaceholder e, NamedArg (Ranged Int))]
 -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
-> e
app [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
f =
        -- If we have an operator and there is exactly one
        -- placeholder for every hole, then we only return
        -- the operator.
        if Bool
isOp Bool -> Bool -> Bool
&& OpAppArgs' e -> Int
noPlaceholders OpAppArgs' e
args forall a. Eq a => a -> a -> Bool
== Int
lastHole forall a. Num a => a -> a -> a
+ Int
1 then
          -- Note that the information in the set "names" is thrown
          -- away here.
          forall e. IsExpr e => ExprView e -> e
unExprView (forall e. QName -> ExprView e
LocalV QName
q')
        else
          forall e. IsExpr e => ExprView e -> e
unExprView (forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
q' Set Name
names OpAppArgs' e
args)
        where
        args :: OpAppArgs' e
args = forall a b. (a -> b) -> [a] -> [b]
map ([(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(LamBinding, Ranged BoundVariablePosition)]
-> Int
-> NamedArg (MaybePlaceholder (OpApp e))
findExprFor ([(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
f [(MaybePlaceholder e, NamedArg (Ranged Int))]
normal) [(LamBinding, Ranged BoundVariablePosition)]
binders) [Int
0..Int
lastHole]
        q' :: QName
q'   = forall a. SetRange a => Range -> a -> a
setRange Range
range QName
q
  in

  case NK k
kind of
    NK k
In   -> \MaybePlaceholder e
x MaybePlaceholder e
y -> ([(MaybePlaceholder e, NamedArg (Ranged Int))]
 -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
-> e
app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
es -> (MaybePlaceholder e
x, NamedArg (Ranged Int)
leadingHole) forall a. a -> [a] -> [a]
: [(MaybePlaceholder e, NamedArg (Ranged Int))]
es forall a. [a] -> [a] -> [a]
++ [(MaybePlaceholder e
y, NamedArg (Ranged Int)
trailingHole)])
    NK k
Pre  -> \  MaybePlaceholder e
y -> ([(MaybePlaceholder e, NamedArg (Ranged Int))]
 -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
-> e
app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
es ->                    [(MaybePlaceholder e, NamedArg (Ranged Int))]
es forall a. [a] -> [a] -> [a]
++ [(MaybePlaceholder e
y, NamedArg (Ranged Int)
trailingHole)])
    NK k
Post -> \MaybePlaceholder e
x   -> ([(MaybePlaceholder e, NamedArg (Ranged Int))]
 -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
-> e
app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
es -> (MaybePlaceholder e
x, NamedArg (Ranged Int)
leadingHole) forall a. a -> [a] -> [a]
: [(MaybePlaceholder e, NamedArg (Ranged Int))]
es)
    NK k
Non  ->         ([(MaybePlaceholder e, NamedArg (Ranged Int))]
 -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
-> e
app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
es ->                    [(MaybePlaceholder e, NamedArg (Ranged Int))]
es)

  where

  (Notation
leadingHoles, Notation
syn1)                  = forall a. (a -> Bool) -> [a] -> ([a], [a])
span    NotationPart -> Bool
isAHole Notation
syn
  (Notation
withoutExternalHoles, Notation
trailingHoles) = forall a. (a -> Bool) -> [a] -> ([a], [a])
spanEnd NotationPart -> Bool
isAHole Notation
syn1

  leadingHole :: NamedArg (Ranged Int)
leadingHole = case Notation
leadingHoles of
    [HolePart Range
_ NamedArg (Ranged Int)
h] -> NamedArg (Ranged Int)
h
    Notation
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__

  trailingHole :: NamedArg (Ranged Int)
trailingHole = case Notation
trailingHoles of
    [HolePart Range
_ NamedArg (Ranged Int)
h] -> NamedArg (Ranged Int)
h
    Notation
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__

  worker ::
    [Name] -> Notation ->
    Parser e (Range, [Either (MaybePlaceholder e, NamedArg (Ranged Int))
                             (LamBinding, Ranged BoundVariablePosition)])
  worker :: [Name]
-> Notation
-> Parser
     e
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
worker [Name]
ms []              = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Range' a
noRange, [])
  worker [Name]
ms (IdPart RString
x : Notation
xs) =
    (\Range
r1 (Range
r2, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es) -> (forall a. Ord a => Range' a -> Range' a -> Range' a
fuseRanges Range
r1 Range
r2, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es))
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e. IsExpr e => [Name] -> [Char] -> Parser e Range
partP [Name]
ms (forall a. Ranged a -> a
rangedThing RString
x)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Name]
-> Notation
-> Parser
     e
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
worker [] Notation
xs
          -- Only the first part is qualified.
  worker [Name]
ms (HolePart Range
_ NamedArg (Ranged Int)
h : Notation
xs) =
    (\MaybePlaceholder e
e (Range
r, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es) -> (Range
r, forall a b. a -> Either a b
Left (MaybePlaceholder e
e, NamedArg (Ranged Int)
h) forall a. a -> [a] -> [a]
: [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es))
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e.
Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
maybePlaceholder
            (if Bool
isOp Bool -> Bool -> Bool
&& ParseSections
parseSections forall a. Eq a => a -> a -> Bool
== ParseSections
ParseSections
             then forall a. a -> Maybe a
Just PositionInName
Middle else forall a. Maybe a
Nothing)
            Parser e e
p
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Name]
-> Notation
-> Parser
     e
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
worker [Name]
ms Notation
xs
  worker [Name]
ms (WildPart Ranged BoundVariablePosition
h : Notation
xs) =
    (\(Range
r, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es) -> let anon :: Binder
anon = Name -> Binder
mkBinder_ Name
simpleHole
                 in (Range
r, forall a b. b -> Either a b
Right (forall {b} {a}. b -> Binder -> (LamBinding' a, b)
mkBinding Ranged BoundVariablePosition
h Binder
anon) forall a. a -> [a] -> [a]
: [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es))
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
-> Notation
-> Parser
     e
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
worker [Name]
ms Notation
xs
  worker [Name]
ms (VarPart Range
_ Ranged BoundVariablePosition
h : Notation
xs) = do
    (\ Binder
b (Range
r, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es) -> (Range
r, forall a b. b -> Either a b
Right (forall {b} {a}. b -> Binder -> (LamBinding' a, b)
mkBinding Ranged BoundVariablePosition
h Binder
b) forall a. a -> [a] -> [a]
: [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged BoundVariablePosition)]
es))
           -- Andreas, 2011-04-07 put just 'Relevant' here, is this
           -- correct?
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e. IsExpr e => Parser e Binder
patternBinder
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Name]
-> Notation
-> Parser
     e
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
worker [Name]
ms Notation
xs

  mkBinding :: b -> Binder -> (LamBinding' a, b)
mkBinding b
h Binder
b = (forall a. NamedArg Binder -> LamBinding' a
DomainFree forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg Binder
b, b
h)

  set :: b -> f (f a) -> f (f b)
set b
x f (f a)
arg = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const b
x)) f (f a)
arg

  findExprFor ::
    [(MaybePlaceholder e, NamedArg (Ranged Int))] ->
    [(LamBinding, Ranged BoundVariablePosition)] -> Int ->
    NamedArg (MaybePlaceholder (OpApp e))
  findExprFor :: [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(LamBinding, Ranged BoundVariablePosition)]
-> Int
-> NamedArg (MaybePlaceholder (OpApp e))
findExprFor [(MaybePlaceholder e, NamedArg (Ranged Int))]
normalHoles [(LamBinding, Ranged BoundVariablePosition)]
binders Int
n =
    case [ (MaybePlaceholder e, NamedArg (Ranged Int))
h | h :: (MaybePlaceholder e, NamedArg (Ranged Int))
h@(MaybePlaceholder e
_, NamedArg (Ranged Int)
m) <- [(MaybePlaceholder e, NamedArg (Ranged Int))]
normalHoles, forall a. Ranged a -> a
rangedThing (forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
m) forall a. Eq a => a -> a -> Bool
== Int
n ] of
      [(Placeholder PositionInName
p,     NamedArg (Ranged Int)
arg)] -> forall {f :: * -> *} {f :: * -> *} {b} {a}.
(Functor f, Functor f) =>
b -> f (f a) -> f (f b)
set (forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
p) NamedArg (Ranged Int)
arg
      [(NoPlaceholder Maybe PositionInName
_ e
e, NamedArg (Ranged Int)
arg)] ->
        forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull
          (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$
           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)
             [ (BoundVariablePosition -> Int
varNumber (forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
m), LamBinding
b)
             | (LamBinding
b, Ranged BoundVariablePosition
m) <- [(LamBinding, Ranged BoundVariablePosition)]
binders
             , BoundVariablePosition -> Int
holeNumber (forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
m) forall a. Eq a => a -> a -> Bool
== Int
n
             ])
        {-then-} (forall {f :: * -> *} {f :: * -> *} {b} {a}.
(Functor f, Functor f) =>
b -> f (f a) -> f (f b)
set (forall e. e -> MaybePlaceholder e
noPlaceholder (forall e. e -> OpApp e
Ordinary e
e)) NamedArg (Ranged Int)
arg) -- no variable to bind
        {-else-} forall a b. (a -> b) -> a -> b
$ \ List1 LamBinding
bs -> forall {f :: * -> *} {f :: * -> *} {b} {a}.
(Functor f, Functor f) =>
b -> f (f a) -> f (f b)
set (forall e. e -> MaybePlaceholder e
noPlaceholder (forall e. Range -> List1 LamBinding -> e -> OpApp e
SyntaxBindingLambda (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange List1 LamBinding
bs e
e) List1 LamBinding
bs e
e)) NamedArg (Ranged Int)
arg
      [(MaybePlaceholder e, NamedArg (Ranged Int))]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

  noPlaceholders :: OpAppArgs' e -> Int
  noPlaceholders :: OpAppArgs' e -> Int
noPlaceholders = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {a} {e}. Num a => MaybePlaceholder e -> a
isPlaceholder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg)
    where
    isPlaceholder :: MaybePlaceholder e -> a
isPlaceholder NoPlaceholder{} = a
0
    isPlaceholder Placeholder{}   = a
1

argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e]
argsP :: forall e. IsExpr e => Parser e e -> Parser e [NamedArg e]
argsP Parser e e
p = forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall {e}. IsExpr e => e -> Arg (Named_ e)
mkArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
p)
  where
  mkArg :: e -> Arg (Named_ e)
mkArg e
e = case forall e. IsExpr e => e -> ExprView e
exprView e
e of
    HiddenArgV   Named_ e
e -> forall a. LensHiding a => a -> a
hide (forall a. a -> Arg a
defaultArg Named_ e
e)
    InstanceArgV Named_ e
e -> forall a. LensHiding a => a -> a
makeInstance (forall a. a -> Arg a
defaultArg Named_ e
e)
    ExprView e
_              -> forall a. a -> Arg a
defaultArg (forall a name. a -> Named name a
unnamed e
e)

appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e
appP :: forall e.
IsExpr e =>
Parser e e -> Parser e [NamedArg e] -> Parser e e
appP Parser e e
p Parser e [NamedArg e]
pa = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {c}. IsExpr c => c -> NamedArg c -> c
app forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser e [NamedArg e]
pa
    where
        app :: c -> NamedArg c -> c
app c
e = forall e. IsExpr e => ExprView e -> e
unExprView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> NamedArg e -> ExprView e
AppV c
e

atomP :: IsExpr e => (QName -> Bool) -> Parser e e
atomP :: forall e. IsExpr e => (QName -> Bool) -> Parser e e
atomP QName -> Bool
p =
  forall tok a. Doc -> Parser tok a -> Parser tok a
doc Doc
"<atom>" forall a b. (a -> b) -> a -> b
$
  forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder forall a b. (a -> b) -> a -> b
$ \e
e ->
  case forall e. IsExpr e => e -> ExprView e
exprView e
e of
    LocalV QName
x | Bool -> Bool
not (QName -> Bool
p QName
x) -> forall a. Maybe a
Nothing
    ExprView e
_                    -> forall a. a -> Maybe a
Just e
e