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

module Agda.Syntax.Concrete.Operators.Parser where

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

import Data.Either
import Data.Kind ( Type )
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 =
  Doc
-> Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e)
forall tok a. Doc -> Parser tok a -> Parser tok a
doc ([Char] -> Doc
text ([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PositionInName -> [Char]
forall a. Show a => a -> [Char]
show PositionInName
p)) (Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e))
-> Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e)
forall a b. (a -> b) -> a -> b
$
  (MaybePlaceholder e -> Bool) -> Parser e (MaybePlaceholder e)
forall tok.
(MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok)
sat ((MaybePlaceholder e -> Bool) -> Parser e (MaybePlaceholder e))
-> (MaybePlaceholder e -> Bool) -> Parser e (MaybePlaceholder e)
forall a b. (a -> b) -> a -> b
$ \case
    Placeholder PositionInName
p' | PositionInName
p' PositionInName -> PositionInName -> Bool
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  -> PositionInName -> Parser e (MaybePlaceholder e)
forall e. PositionInName -> Parser e (MaybePlaceholder e)
placeholder PositionInName
h Parser e (MaybePlaceholder e)
-> Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser e (MaybePlaceholder e)
p'
  where
  p' :: Parser e (MaybePlaceholder e)
p' = e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder (e -> MaybePlaceholder e)
-> Parser e e -> Parser e (MaybePlaceholder e)
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 = (MaybePlaceholder e -> Maybe a) -> Parser e a
forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
sat' ((MaybePlaceholder e -> Maybe a) -> Parser e a)
-> (MaybePlaceholder e -> Maybe a) -> Parser e a
forall a b. (a -> b) -> a -> b
$ \case
    NoPlaceholder Maybe PositionInName
_ e
e -> e -> Maybe a
p e
e
    Placeholder PositionInName
_     -> Maybe a
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 = e -> Range
forall a. HasRange a => a -> Range
getRange (e -> Range) -> (ExprView e -> e) -> ExprView e -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView

instance IsExpr Expr where
    exprView :: Expr -> ExprView Expr
exprView = \case
        Ident QName
x         -> QName -> ExprView Expr
forall e. QName -> ExprView e
LocalV QName
x
        App Range
_ Expr
e1 NamedArg Expr
e2     -> Expr -> NamedArg Expr -> ExprView Expr
forall e. e -> NamedArg e -> ExprView e
AppV Expr
e1 NamedArg Expr
e2
        OpApp Range
r QName
d Set Name
ns OpAppArgs
es -> QName -> Set Name -> OpAppArgs -> ExprView Expr
forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
d Set Name
ns OpAppArgs
es
        HiddenArg Range
_ Named_ Expr
e   -> Named_ Expr -> ExprView Expr
forall e. Named_ e -> ExprView e
HiddenArgV Named_ Expr
e
        InstanceArg Range
_ Named_ Expr
e -> Named_ Expr -> ExprView Expr
forall e. Named_ e -> ExprView e
InstanceArgV Named_ Expr
e
        Paren Range
_ Expr
e       -> Expr -> ExprView Expr
forall e. e -> ExprView e
ParenV Expr
e
        Lam Range
_ List1 LamBinding
bs    Expr
e   -> List1 LamBinding -> Expr -> ExprView Expr
forall e. List1 LamBinding -> e -> ExprView e
LamV List1 LamBinding
bs Expr
e
        e :: Expr
e@Underscore{}  -> Expr -> ExprView Expr
forall e. e -> ExprView e
WildV Expr
e
        Expr
e               -> Expr -> ExprView Expr
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 (Expr -> NamedArg Expr -> Range
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 (QName -> OpAppArgs -> Range
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 (Named_ Expr -> Range
forall a. HasRange a => a -> Range
getRange Named_ Expr
e) Named_ Expr
e
        InstanceArgV Named_ Expr
e -> Range -> Named_ Expr -> Expr
InstanceArg (Named_ Expr -> Range
forall a. HasRange a => a -> Range
getRange Named_ Expr
e) Named_ Expr
e
        ParenV Expr
e       -> Range -> Expr -> Expr
Paren (Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e) Expr
e
        LamV List1 LamBinding
bs Expr
e      -> Range -> List1 LamBinding -> Expr -> Expr
Lam (List1 LamBinding -> Expr -> Range
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         -> QName -> ExprView Pattern
forall e. QName -> ExprView e
LocalV QName
x
        AppP Pattern
e1 NamedArg Pattern
e2       -> Pattern -> NamedArg Pattern -> ExprView Pattern
forall e. e -> NamedArg e -> ExprView e
AppV Pattern
e1 NamedArg Pattern
e2
        OpAppP Range
r QName
d Set Name
ns [NamedArg Pattern]
es -> QName -> Set Name -> OpAppArgs' Pattern -> ExprView Pattern
forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
d Set Name
ns (OpAppArgs' Pattern -> ExprView Pattern)
-> OpAppArgs' Pattern -> ExprView Pattern
forall a b. (a -> b) -> a -> b
$ ((NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
-> [NamedArg Pattern] -> OpAppArgs' Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
 -> [NamedArg Pattern] -> OpAppArgs' Pattern)
-> ((Pattern -> MaybePlaceholder (OpApp Pattern))
    -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
-> (Pattern -> MaybePlaceholder (OpApp Pattern))
-> [NamedArg Pattern]
-> OpAppArgs' Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName Pattern
 -> Named_ (MaybePlaceholder (OpApp Pattern)))
-> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName Pattern
  -> Named_ (MaybePlaceholder (OpApp Pattern)))
 -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
-> ((Pattern -> MaybePlaceholder (OpApp Pattern))
    -> Named NamedName Pattern
    -> Named_ (MaybePlaceholder (OpApp Pattern)))
-> (Pattern -> MaybePlaceholder (OpApp Pattern))
-> NamedArg Pattern
-> NamedArg (MaybePlaceholder (OpApp Pattern))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> MaybePlaceholder (OpApp Pattern))
-> Named NamedName Pattern
-> Named_ (MaybePlaceholder (OpApp Pattern))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (OpApp Pattern -> MaybePlaceholder (OpApp Pattern)
forall e. e -> MaybePlaceholder e
noPlaceholder (OpApp Pattern -> MaybePlaceholder (OpApp Pattern))
-> (Pattern -> OpApp Pattern)
-> Pattern
-> MaybePlaceholder (OpApp Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> OpApp Pattern
forall e. e -> OpApp e
Ordinary) [NamedArg Pattern]
es
        HiddenP Range
_ Named NamedName Pattern
e      -> Named NamedName Pattern -> ExprView Pattern
forall e. Named_ e -> ExprView e
HiddenArgV Named NamedName Pattern
e
        InstanceP Range
_ Named NamedName Pattern
e    -> Named NamedName Pattern -> ExprView Pattern
forall e. Named_ e -> ExprView e
InstanceArgV Named NamedName Pattern
e
        ParenP Range
_ Pattern
e       -> Pattern -> ExprView Pattern
forall e. e -> ExprView e
ParenV Pattern
e
        e :: Pattern
e@WildP{}        -> Pattern -> ExprView Pattern
forall e. e -> ExprView e
WildV Pattern
e
        Pattern
e                -> Pattern -> ExprView Pattern
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 = ((NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
-> OpAppArgs' Pattern -> [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
 -> OpAppArgs' Pattern -> [NamedArg Pattern])
-> ((MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
-> (MaybePlaceholder (OpApp Pattern) -> Pattern)
-> OpAppArgs' Pattern
-> [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ (MaybePlaceholder (OpApp Pattern))
 -> Named NamedName Pattern)
-> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ (MaybePlaceholder (OpApp Pattern))
  -> Named NamedName Pattern)
 -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
-> ((MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> Named_ (MaybePlaceholder (OpApp Pattern))
    -> Named NamedName Pattern)
-> (MaybePlaceholder (OpApp Pattern) -> Pattern)
-> NamedArg (MaybePlaceholder (OpApp Pattern))
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MaybePlaceholder (OpApp Pattern) -> Pattern)
-> Named_ (MaybePlaceholder (OpApp Pattern))
-> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)
                                      (\case
                                          Placeholder{}     -> Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
                                          NoPlaceholder Maybe PositionInName
_ OpApp Pattern
x -> Pattern -> OpApp Pattern -> Pattern
forall e. e -> OpApp e -> e
fromOrdinary Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__ OpApp Pattern
x)
                                      OpAppArgs' Pattern
es
                          in Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
OpAppP (QName -> [NamedArg Pattern] -> Range
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 NamedName Pattern
e   -> Range -> Named NamedName Pattern -> Pattern
HiddenP (Named NamedName Pattern -> Range
forall a. HasRange a => a -> Range
getRange Named NamedName Pattern
e) Named NamedName Pattern
e
        InstanceArgV Named NamedName Pattern
e -> Range -> Named NamedName Pattern -> Pattern
InstanceP (Named NamedName Pattern -> Range
forall a. HasRange a => a -> Range
getRange Named NamedName Pattern
e) Named NamedName Pattern
e
        ParenV Pattern
e       -> Range -> Pattern -> Pattern
ParenP (Pattern -> Range
forall a. HasRange a => a -> Range
getRange Pattern
e) Pattern
e
        LamV List1 LamBinding
_ Pattern
_       -> Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
        WildV Pattern
e        -> Pattern
e
        OtherV Pattern
e       -> Pattern
e

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

-- | Should sections be parsed?
data ParseSections = ParseSections | DoNotParseSections
  deriving (ParseSections -> ParseSections -> Bool
(ParseSections -> ParseSections -> Bool)
-> (ParseSections -> ParseSections -> Bool) -> Eq ParseSections
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 -> [Char] -> [Char]
[ParseSections] -> [Char] -> [Char]
ParseSections -> [Char]
(Int -> ParseSections -> [Char] -> [Char])
-> (ParseSections -> [Char])
-> ([ParseSections] -> [Char] -> [Char])
-> Show ParseSections
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [ParseSections] -> [Char] -> [Char]
$cshowList :: [ParseSections] -> [Char] -> [Char]
show :: ParseSections -> [Char]
$cshow :: ParseSections -> [Char]
showsPrec :: Int -> ParseSections -> [Char] -> [Char]
$cshowsPrec :: Int -> ParseSections -> [Char] -> [Char]
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 = Parser e a -> [MaybePlaceholder e] -> [a]
forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
P.parse Parser e a
p ((e -> MaybePlaceholder e) -> [e] -> [MaybePlaceholder e]
forall a b. (a -> b) -> [a] -> [b]
map e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder [e]
es)
parse (ParseSections
ParseSections,      Parser e a
p) [e]
es = Parser e a -> [MaybePlaceholder e] -> [a]
forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
P.parse Parser e a
p ([List1 (MaybePlaceholder e)] -> [MaybePlaceholder e]
forall a. [List1 a] -> [a]
List1.concat ([List1 (MaybePlaceholder e)] -> [MaybePlaceholder e])
-> [List1 (MaybePlaceholder e)] -> [MaybePlaceholder e]
forall a b. (a -> b) -> a -> b
$ (e -> List1 (MaybePlaceholder e))
-> [e] -> [List1 (MaybePlaceholder e)]
forall a b. (a -> b) -> [a] -> [b]
map e -> List1 (MaybePlaceholder e)
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 e -> ExprView e
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 = MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
forall el coll. Singleton el coll => el -> coll
singleton (MaybePlaceholder e -> NonEmpty (MaybePlaceholder e))
-> MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
forall a b. (a -> b) -> a -> b
$ e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder e
e

    splitName :: QName -> NonEmpty (MaybePlaceholder e)
splitName QName
n = case NonEmpty Name -> Name
forall a. NonEmpty a -> a
List1.last NonEmpty Name
ns of
      Name Range
r NameInScope
nis ps :: NameParts
ps@(NamePart
_ :| NamePart
_ : [NamePart]
_) -> Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
forall {e}.
IsExpr e =>
Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
splitParts Range
r NameInScope
nis (NonEmpty Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init NonEmpty Name
ns) PositionInName
Beginning NameParts
ps
      Name
_                          -> NonEmpty (MaybePlaceholder e)
noSplit
      where
      ns :: NonEmpty Name
ns = QName -> NonEmpty 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 :| [])     = MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
forall el coll. Singleton el coll => el -> coll
singleton (MaybePlaceholder e -> NonEmpty (MaybePlaceholder e))
-> MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
forall a b. (a -> b) -> a -> b
$ PositionInName -> MaybePlaceholder e
forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
End
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
_ (Id [Char]
s :| [])     = MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
forall el coll. Singleton el coll => el -> coll
singleton (MaybePlaceholder e -> NonEmpty (MaybePlaceholder e))
-> MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
forall a b. (a -> b) -> a -> b
$ Range
-> NameInScope
-> [Name]
-> PositionInName
-> [Char]
-> MaybePlaceholder e
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) = PositionInName -> MaybePlaceholder e
forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
w    MaybePlaceholder e
-> NonEmpty (MaybePlaceholder e) -> NonEmpty (MaybePlaceholder e)
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 NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| [NamePart]
ps)
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
w (Id [Char]
s :| NamePart
p : [NamePart]
ps) = Range
-> NameInScope
-> [Name]
-> PositionInName
-> [Char]
-> MaybePlaceholder e
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 MaybePlaceholder e
-> NonEmpty (MaybePlaceholder e) -> NonEmpty (MaybePlaceholder e)
forall a. a -> NonEmpty a -> NonEmpty a
<| Range
-> NameInScope
-> [Name]
-> PositionInName
-> NameParts
-> NonEmpty (MaybePlaceholder e)
splitParts Range
r NameInScope
nis [] PositionInName
Middle (NamePart
p NamePart -> [NamePart] -> NameParts
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 =
        Maybe PositionInName -> e -> MaybePlaceholder e
forall e. Maybe PositionInName -> e -> MaybePlaceholder e
NoPlaceholder (PositionInName -> Maybe PositionInName
forall a. a -> Maybe a
Strict.Just PositionInName
w)
                      (ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (ExprView e -> e) -> ExprView e -> e
forall a b. (a -> b) -> a -> b
$ QName -> ExprView e
forall e. QName -> ExprView e
LocalV (QName -> ExprView e) -> QName -> ExprView e
forall a b. (a -> b) -> a -> b
$
                         (Name -> QName -> QName) -> QName -> t Name -> QName
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
Qual (Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> NameParts -> Name
Name Range
r NameInScope
nis (NameParts -> Name) -> NameParts -> Name
forall a b. (a -> b) -> a -> b
$ NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
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 =
  Doc -> Parser e Range -> Parser e Range
forall tok a. Doc -> Parser tok a -> Parser tok a
doc ([Char] -> Doc
text ([Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
str)) (Parser e Range -> Parser e Range)
-> Parser e Range -> Parser e Range
forall a b. (a -> b) -> a -> b
$
  (e -> Maybe Range) -> Parser e Range
forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder e -> Maybe Range
isLocal
  where
  str :: [Char]
str = QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> [Char]) -> QName -> [Char]
forall a b. (a -> b) -> a -> b
$ (Name -> QName -> QName) -> QName -> [Name] -> QName
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
Qual (Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ [Char] -> Name
simpleName [Char]
s) [Name]
ms
  isLocal :: e -> Maybe Range
isLocal e
e = case e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView e
e of
      LocalV QName
y | [Char]
str [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
y -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasRange a => a -> Range
getRange QName
y
      ExprView e
_ -> Maybe Range
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 (Maybe (Range, NameInScope), NamePart)
-> [(Maybe (Range, NameInScope), NamePart)]
-> NonEmpty (Maybe (Range, NameInScope), NamePart)
forall a. a -> [a] -> NonEmpty a
:| [(Maybe (Range, NameInScope), NamePart)]
ps [(Maybe (Range, NameInScope), NamePart)]
-> [(Maybe (Range, NameInScope), NamePart)]
-> [(Maybe (Range, NameInScope), NamePart)]
forall a. [a] -> [a] -> [a]
++ [(Maybe (Range, NameInScope), NamePart)
p2] in
      case ((Maybe (Range, NameInScope), NamePart)
 -> Maybe (Range, NameInScope))
-> NonEmpty (Maybe (Range, NameInScope), NamePart)
-> [(Range, NameInScope)]
forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (Maybe (Range, NameInScope), NamePart)
-> Maybe (Range, NameInScope)
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 (((Maybe (Range, NameInScope), NamePart) -> NamePart)
-> NonEmpty (Maybe (Range, NameInScope), NamePart) -> NameParts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe (Range, NameInScope), NamePart) -> NamePart
forall a b. (a, b) -> b
snd NonEmpty (Maybe (Range, NameInScope), NamePart)
all)
        []          -> Name
forall a. HasCallStack => a
__IMPOSSIBLE__)
  ((Maybe (Range, NameInScope), NamePart)
 -> [(Maybe (Range, NameInScope), NamePart)]
 -> (Maybe (Range, NameInScope), NamePart)
 -> Name)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Maybe (Range, NameInScope), NamePart)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     ([(Maybe (Range, NameInScope), NamePart)]
      -> (Maybe (Range, NameInScope), NamePart) -> Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PositionInName
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Maybe (Range, NameInScope), NamePart)
forall {e}.
IsExpr e =>
PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
part PositionInName
Beginning
  Parser
  MemoKey
  e
  (MaybePlaceholder e)
  ([(Maybe (Range, NameInScope), NamePart)]
   -> (Maybe (Range, NameInScope), NamePart) -> Name)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     [(Maybe (Range, NameInScope), NamePart)]
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     ((Maybe (Range, NameInScope), NamePart) -> Name)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser
  MemoKey
  e
  (MaybePlaceholder e)
  (Maybe (Range, NameInScope), NamePart)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     [(Maybe (Range, NameInScope), NamePart)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (PositionInName
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Maybe (Range, NameInScope), NamePart)
forall {e}.
IsExpr e =>
PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
part PositionInName
Middle)
  Parser
  MemoKey
  e
  (MaybePlaceholder e)
  ((Maybe (Range, NameInScope), NamePart) -> Name)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Maybe (Range, NameInScope), NamePart)
-> Parser MemoKey e (MaybePlaceholder e) Name
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PositionInName
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Maybe (Range, NameInScope), NamePart)
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 = (MaybePlaceholder e
 -> Maybe (Maybe (Range, NameInScope), NamePart))
-> Parser e (Maybe (Range, NameInScope), NamePart)
forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
sat' ((MaybePlaceholder e
  -> Maybe (Maybe (Range, NameInScope), NamePart))
 -> Parser e (Maybe (Range, NameInScope), NamePart))
-> (MaybePlaceholder e
    -> Maybe (Maybe (Range, NameInScope), NamePart))
-> Parser e (Maybe (Range, NameInScope), NamePart)
forall a b. (a -> b) -> a -> b
$ \case
    Placeholder PositionInName
pos'                   | PositionInName
pos PositionInName -> PositionInName -> Bool
forall a. Eq a => a -> a -> Bool
== PositionInName
pos' -> (Maybe (Range, NameInScope), NamePart)
-> Maybe (Maybe (Range, NameInScope), NamePart)
forall a. a -> Maybe a
Just ( Maybe (Range, NameInScope)
forall a. Maybe a
Nothing
                                                             , NamePart
Hole
                                                             )
    NoPlaceholder (Strict.Just PositionInName
pos') e
e | PositionInName
pos PositionInName -> PositionInName -> Bool
forall a. Eq a => a -> a -> Bool
== PositionInName
pos' ->
      case e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView e
e of
        LocalV (QName (Name Range
r NameInScope
nis (Id [Char]
s :| []))) -> (Maybe (Range, NameInScope), NamePart)
-> Maybe (Maybe (Range, NameInScope), NamePart)
forall a. a -> Maybe a
Just ((Range, NameInScope) -> Maybe (Range, NameInScope)
forall a. a -> Maybe a
Just (Range
r, NameInScope
nis), [Char] -> NamePart
Id [Char]
s)
        ExprView e
_ -> Maybe (Maybe (Range, NameInScope), NamePart)
forall a. Maybe a
Nothing
    MaybePlaceholder e
_ -> Maybe (Maybe (Range, NameInScope), NamePart)
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 e Binder
inOnePart Parser e Binder -> Parser e Binder -> Parser e Binder
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Binder
mkBinder_ (Name -> Binder)
-> Parser MemoKey e (MaybePlaceholder e) Name -> Parser e Binder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser MemoKey e (MaybePlaceholder e) Name
forall e. IsExpr e => Parser e Name
atLeastTwoParts
  where inOnePart :: Parser e Binder
inOnePart = (e -> Maybe Binder) -> Parser e Binder
forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder ((e -> Maybe Binder) -> Parser e Binder)
-> (e -> Maybe Binder) -> Parser e Binder
forall a b. (a -> b) -> a -> b
$ Pattern -> Maybe Binder
isBinderP (Pattern -> Maybe Binder)
-> (e -> Maybe Pattern) -> e -> Maybe Binder
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< e -> Maybe Pattern
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 =
  (((Range,
   [Either
      (MaybePlaceholder e, NamedArg (Ranged Int))
      (LamBinding, Ranged Int)])
  -> OperatorType k e)
 -> Parser
      MemoKey
      e
      (MaybePlaceholder e)
      (Range,
       [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged Int)])
 -> Parser e (OperatorType k e))
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged Int)])
-> ((Range,
     [Either
        (MaybePlaceholder e, NamedArg (Ranged Int))
        (LamBinding, Ranged Int)])
    -> OperatorType k e)
-> Parser e (OperatorType k e)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Range,
  [Either
     (MaybePlaceholder e, NamedArg (Ranged Int))
     (LamBinding, Ranged Int)])
 -> OperatorType k e)
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged Int)])
-> Parser e (OperatorType k e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name]
-> Notation
-> Parser
     MemoKey
     e
     (MaybePlaceholder e)
     (Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged Int)])
worker (NonEmpty Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init (NonEmpty Name -> [Name]) -> NonEmpty Name -> [Name]
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty Name
qnameParts QName
q)
                    Notation
withoutExternalHoles) (((Range,
   [Either
      (MaybePlaceholder e, NamedArg (Ranged Int))
      (LamBinding, Ranged Int)])
  -> OperatorType k e)
 -> Parser e (OperatorType k e))
-> ((Range,
     [Either
        (MaybePlaceholder e, NamedArg (Ranged Int))
        (LamBinding, Ranged Int)])
    -> OperatorType k e)
-> Parser e (OperatorType k e)
forall a b. (a -> b) -> a -> b
$ \(Range
range, [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged Int)]
hs) ->

  let ([(MaybePlaceholder e, NamedArg (Ranged Int))]
normal, [(LamBinding, Ranged Int)]
binders) = [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged Int)]
-> ([(MaybePlaceholder e, NamedArg (Ranged Int))],
    [(LamBinding, Ranged Int)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either
   (MaybePlaceholder e, NamedArg (Ranged Int))
   (LamBinding, Ranged Int)]
hs
      lastHole :: Int
lastHole          = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (-Int
1) Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (GenPart -> Maybe Int) -> Notation -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe GenPart -> 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lastHole Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 then
          -- Note that the information in the set "names" is thrown
          -- away here.
          ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (QName -> ExprView e
forall e. QName -> ExprView e
LocalV QName
q')
        else
          ExprView e -> e
forall e. IsExpr e => ExprView e -> e
unExprView (QName -> Set Name -> OpAppArgs' e -> ExprView e
forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
OpAppV QName
q' Set Name
names OpAppArgs' e
args)
        where
        args :: OpAppArgs' e
args = (Int -> NamedArg (MaybePlaceholder (OpApp e)))
-> [Int] -> OpAppArgs' e
forall a b. (a -> b) -> [a] -> [b]
map ([(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(LamBinding, Ranged Int)]
-> 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 Int)]
binders) [Int
0..Int
lastHole]
        q' :: QName
q'   = Range -> QName -> QName
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) (MaybePlaceholder e, NamedArg (Ranged Int))
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
forall a. a -> [a] -> [a]
: [(MaybePlaceholder e, NamedArg (Ranged Int))]
es [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
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 [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
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) (MaybePlaceholder e, NamedArg (Ranged Int))
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
-> [(MaybePlaceholder e, NamedArg (Ranged Int))]
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)                  = (GenPart -> Bool) -> Notation -> (Notation, Notation)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span    GenPart -> Bool
isNormalHole Notation
syn
  (Notation
withoutExternalHoles, Notation
trailingHoles) = (GenPart -> Bool) -> Notation -> (Notation, Notation)
forall a. (a -> Bool) -> [a] -> ([a], [a])
spanEnd GenPart -> Bool
isNormalHole Notation
syn1

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

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

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

  mkBinding :: b -> Binder -> (LamBinding' a, b)
mkBinding b
h Binder
b = (NamedArg Binder -> LamBinding' a
forall a. NamedArg Binder -> LamBinding' a
DomainFree (NamedArg Binder -> LamBinding' a)
-> NamedArg Binder -> LamBinding' a
forall a b. (a -> b) -> a -> b
$ Binder -> NamedArg Binder
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 = (f a -> f b) -> f (f a) -> f (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> a -> b
forall a b. a -> b -> a
const b
x)) f (f a)
arg

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

  noPlaceholders :: OpAppArgs' e -> Int
  noPlaceholders :: OpAppArgs' e -> Int
noPlaceholders = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> (OpAppArgs' e -> [Int]) -> OpAppArgs' e -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (MaybePlaceholder (OpApp e)) -> Int)
-> OpAppArgs' e -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MaybePlaceholder (OpApp e) -> Int
forall {a} {e}. Num a => MaybePlaceholder e -> a
isPlaceholder (MaybePlaceholder (OpApp e) -> Int)
-> (NamedArg (MaybePlaceholder (OpApp e))
    -> MaybePlaceholder (OpApp e))
-> NamedArg (MaybePlaceholder (OpApp e))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (MaybePlaceholder (OpApp e)) -> MaybePlaceholder (OpApp e)
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 = Parser MemoKey e (MaybePlaceholder e) (NamedArg e)
-> Parser MemoKey e (MaybePlaceholder e) [NamedArg e]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (e -> NamedArg e
forall {e}. IsExpr e => e -> Arg (Named_ e)
mkArg (e -> NamedArg e)
-> Parser e e -> Parser MemoKey e (MaybePlaceholder e) (NamedArg e)
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 e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView e
e of
    HiddenArgV   Named_ e
e -> Arg (Named_ e) -> Arg (Named_ e)
forall a. LensHiding a => a -> a
hide (Named_ e -> Arg (Named_ e)
forall a. a -> Arg a
defaultArg Named_ e
e)
    InstanceArgV Named_ e
e -> Arg (Named_ e) -> Arg (Named_ e)
forall a. LensHiding a => a -> a
makeInstance (Named_ e -> Arg (Named_ e)
forall a. a -> Arg a
defaultArg Named_ e
e)
    ExprView e
_              -> Named_ e -> Arg (Named_ e)
forall a. a -> Arg a
defaultArg (e -> Named_ e
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 = (e -> NamedArg e -> e) -> e -> [NamedArg e] -> e
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl e -> NamedArg e -> e
forall {c}. IsExpr c => c -> NamedArg c -> c
app (e -> [NamedArg e] -> e)
-> Parser e e
-> Parser MemoKey e (MaybePlaceholder e) ([NamedArg e] -> e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser e e
p Parser MemoKey e (MaybePlaceholder e) ([NamedArg e] -> e)
-> Parser e [NamedArg e] -> Parser e e
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 = ExprView c -> c
forall e. IsExpr e => ExprView e -> e
unExprView (ExprView c -> c) -> (NamedArg c -> ExprView c) -> NamedArg c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> NamedArg c -> ExprView 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 =
  Doc -> Parser e e -> Parser e e
forall tok a. Doc -> Parser tok a -> Parser tok a
doc Doc
"<atom>" (Parser e e -> Parser e e) -> Parser e e -> Parser e e
forall a b. (a -> b) -> a -> b
$
  (e -> Maybe e) -> Parser e e
forall e a. (e -> Maybe a) -> Parser e a
satNoPlaceholder ((e -> Maybe e) -> Parser e e) -> (e -> Maybe e) -> Parser e e
forall a b. (a -> b) -> a -> b
$ \e
e ->
  case e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView e
e of
    LocalV QName
x | Bool -> Bool
not (QName -> Bool
p QName
x) -> Maybe e
forall a. Maybe a
Nothing
    ExprView e
_                    -> e -> Maybe e
forall a. a -> Maybe a
Just e
e