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

module Agda.Syntax.Concrete.Operators.Parser where

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

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.Fixity
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.Impossible

placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
placeholder :: 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 (String -> Doc
text (String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PositionInName -> String
forall a. Show a => a -> String
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
$ \MaybePlaceholder e
t ->
  case MaybePlaceholder e
t of
    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 :: 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 :: (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
$ \MaybePlaceholder e
tok ->
  case MaybePlaceholder e
tok of
    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) [NamedArg (MaybePlaceholder (OpApp 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 [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 t. HasRange t => t -> 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 Expr
e = case Expr
e of
        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 [NamedArg (MaybePlaceholder (OpApp Expr))]
es -> QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp Expr))]
-> ExprView Expr
forall e.
QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> ExprView e
OpAppV QName
d Set Name
ns [NamedArg (MaybePlaceholder (OpApp Expr))]
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
_ [LamBinding]
bs    Expr
e   -> [LamBinding] -> Expr -> ExprView Expr
forall e. [LamBinding] -> e -> ExprView e
LamV [LamBinding]
bs Expr
e
        Underscore{}    -> Expr -> ExprView Expr
forall e. e -> ExprView e
WildV Expr
e
        Expr
_               -> Expr -> ExprView Expr
forall e. e -> ExprView e
OtherV Expr
e
    unExprView :: ExprView Expr -> Expr
unExprView ExprView Expr
e = case ExprView Expr
e of
        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 [NamedArg (MaybePlaceholder (OpApp Expr))]
es -> Range
-> QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp Expr))]
-> Expr
OpApp (QName -> [NamedArg (MaybePlaceholder (OpApp Expr))] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
d [NamedArg (MaybePlaceholder (OpApp Expr))]
es) QName
d Set Name
ns [NamedArg (MaybePlaceholder (OpApp Expr))]
es
        HiddenArgV Named_ Expr
e   -> Range -> Named_ Expr -> Expr
HiddenArg (Named_ Expr -> Range
forall t. HasRange t => t -> Range
getRange Named_ Expr
e) Named_ Expr
e
        InstanceArgV Named_ Expr
e -> Range -> Named_ Expr -> Expr
InstanceArg (Named_ Expr -> Range
forall t. HasRange t => t -> Range
getRange Named_ Expr
e) Named_ Expr
e
        ParenV Expr
e       -> Range -> Expr -> Expr
Paren (Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e) Expr
e
        LamV [LamBinding]
bs Expr
e      -> Range -> [LamBinding] -> Expr -> Expr
Lam ([LamBinding] -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange [LamBinding]
bs Expr
e) [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 Pattern
e = case Pattern
e of
        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
-> [NamedArg (MaybePlaceholder (OpApp Pattern))]
-> ExprView Pattern
forall e.
QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> ExprView e
OpAppV QName
d Set Name
ns (((NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
-> [NamedArg Pattern]
-> [NamedArg (MaybePlaceholder (OpApp Pattern))]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
 -> [NamedArg Pattern]
 -> [NamedArg (MaybePlaceholder (OpApp Pattern))])
-> ((Pattern -> MaybePlaceholder (OpApp Pattern))
    -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
-> (Pattern -> MaybePlaceholder (OpApp Pattern))
-> [NamedArg Pattern]
-> [NamedArg (MaybePlaceholder (OpApp Pattern))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName Pattern
 -> Named NamedName (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 NamedName (MaybePlaceholder (OpApp Pattern)))
 -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
-> ((Pattern -> MaybePlaceholder (OpApp Pattern))
    -> Named NamedName Pattern
    -> Named NamedName (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 NamedName (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
        WildP{}          -> Pattern -> ExprView Pattern
forall e. e -> ExprView e
WildV Pattern
e
        Pattern
_                -> Pattern -> ExprView Pattern
forall e. e -> ExprView e
OtherV Pattern
e
    unExprView :: ExprView Pattern -> Pattern
unExprView ExprView Pattern
e = case ExprView Pattern
e of
        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 [NamedArg (MaybePlaceholder (OpApp Pattern))]
es -> let ess :: [NamedArg Pattern]
                              ess :: [NamedArg Pattern]
ess = ((NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
-> [NamedArg (MaybePlaceholder (OpApp Pattern))]
-> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
 -> [NamedArg (MaybePlaceholder (OpApp Pattern))]
 -> [NamedArg Pattern])
-> ((MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
-> (MaybePlaceholder (OpApp Pattern) -> Pattern)
-> [NamedArg (MaybePlaceholder (OpApp Pattern))]
-> [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (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 NamedName (MaybePlaceholder (OpApp Pattern))
  -> Named NamedName Pattern)
 -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
-> ((MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> Named NamedName (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 NamedName (MaybePlaceholder (OpApp Pattern))
-> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)
                                      (\MaybePlaceholder (OpApp Pattern)
x -> case MaybePlaceholder (OpApp Pattern)
x of
                                          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)
                                      [NamedArg (MaybePlaceholder (OpApp 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 t. HasRange t => t -> 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 t. HasRange t => t -> Range
getRange Named NamedName Pattern
e) Named NamedName Pattern
e
        ParenV Pattern
e       -> Range -> Pattern -> Pattern
ParenP (Pattern -> Range
forall t. HasRange t => t -> Range
getRange Pattern
e) Pattern
e
        LamV [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 -> String -> String
[ParseSections] -> String -> String
ParseSections -> String
(Int -> ParseSections -> String -> String)
-> (ParseSections -> String)
-> ([ParseSections] -> String -> String)
-> Show ParseSections
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [ParseSections] -> String -> String
$cshowList :: [ParseSections] -> String -> String
show :: ParseSections -> String
$cshow :: ParseSections -> String
showsPrec :: Int -> ParseSections -> String -> String
$cshowsPrec :: Int -> ParseSections -> String -> String
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 :: (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 ([[MaybePlaceholder e]] -> [MaybePlaceholder e]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[MaybePlaceholder e]] -> [MaybePlaceholder e])
-> [[MaybePlaceholder e]] -> [MaybePlaceholder e]
forall a b. (a -> b) -> a -> b
$ (e -> [MaybePlaceholder e]) -> [e] -> [[MaybePlaceholder e]]
forall a b. (a -> b) -> [a] -> [b]
map e -> [MaybePlaceholder e]
forall e. IsExpr e => e -> [MaybePlaceholder e]
splitExpr [e]
es)
  where
  splitExpr :: IsExpr e => e -> [MaybePlaceholder e]
  splitExpr :: e -> [MaybePlaceholder e]
splitExpr e
e = case e -> ExprView e
forall e. IsExpr e => e -> ExprView e
exprView e
e of
    LocalV QName
n -> QName -> [MaybePlaceholder e]
splitName QName
n
    ExprView e
_        -> [MaybePlaceholder e]
noSplit
    where
    noSplit :: [MaybePlaceholder e]
noSplit = [e -> MaybePlaceholder e
forall e. e -> MaybePlaceholder e
noPlaceholder e
e]

    splitName :: QName -> [MaybePlaceholder e]
splitName QName
n = case [Name] -> Name
forall a. [a] -> a
last [Name]
ns of
      Name Range
r NameInScope
nis ps :: [NamePart]
ps@(NamePart
_ : NamePart
_ : [NamePart]
_) -> Range
-> NameInScope
-> [Name]
-> PositionInName
-> [NamePart]
-> [MaybePlaceholder e]
forall e.
IsExpr e =>
Range
-> NameInScope
-> [Name]
-> PositionInName
-> [NamePart]
-> [MaybePlaceholder e]
splitParts Range
r NameInScope
nis ([Name] -> [Name]
forall a. [a] -> [a]
init [Name]
ns) PositionInName
Beginning [NamePart]
ps
      Name
_                         -> [MaybePlaceholder e]
noSplit
      where
      ns :: [Name]
ns = QName -> [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
-> [NamePart]
-> [MaybePlaceholder e]
splitParts Range
_ NameInScope
_   [Name]
_ PositionInName
_ []          = [MaybePlaceholder e]
forall a. HasCallStack => a
__IMPOSSIBLE__
      splitParts Range
_ NameInScope
_   [Name]
_ PositionInName
_ (NamePart
Hole : []) = [PositionInName -> MaybePlaceholder e
forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
End]
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
_ (Id String
s : []) = [Range
-> NameInScope
-> [Name]
-> PositionInName
-> String
-> MaybePlaceholder e
forall e (t :: * -> *).
(IsExpr e, Foldable t) =>
Range
-> NameInScope
-> t Name
-> PositionInName
-> String
-> MaybePlaceholder e
part Range
r NameInScope
nis [Name]
m PositionInName
End String
s]
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
w (NamePart
Hole : [NamePart]
ps) = PositionInName -> MaybePlaceholder e
forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
w MaybePlaceholder e -> [MaybePlaceholder e] -> [MaybePlaceholder e]
forall a. a -> [a] -> [a]
: Range
-> NameInScope
-> [Name]
-> PositionInName
-> [NamePart]
-> [MaybePlaceholder e]
splitParts Range
r NameInScope
nis [Name]
m  PositionInName
Middle [NamePart]
ps
      splitParts Range
r NameInScope
nis [Name]
m PositionInName
w (Id String
s : [NamePart]
ps) = Range
-> NameInScope
-> [Name]
-> PositionInName
-> String
-> MaybePlaceholder e
forall e (t :: * -> *).
(IsExpr e, Foldable t) =>
Range
-> NameInScope
-> t Name
-> PositionInName
-> String
-> MaybePlaceholder e
part Range
r NameInScope
nis [Name]
m PositionInName
w String
s MaybePlaceholder e -> [MaybePlaceholder e] -> [MaybePlaceholder e]
forall a. a -> [a] -> [a]
: Range
-> NameInScope
-> [Name]
-> PositionInName
-> [NamePart]
-> [MaybePlaceholder e]
splitParts Range
r NameInScope
nis [] PositionInName
Middle [NamePart]
ps

      part :: Range
-> NameInScope
-> t Name
-> PositionInName
-> String
-> MaybePlaceholder e
part Range
r NameInScope
nis t Name
m PositionInName
w String
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 (Range -> NameInScope -> [NamePart] -> Name
Name Range
r NameInScope
nis [String -> NamePart
Id String
s])) t Name
m)

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

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

-- | Parse a specific identifier as a NamePart
partP :: IsExpr e => [Name] -> RawName -> Parser e Range
partP :: [Name] -> String -> Parser e Range
partP [Name]
ms String
s =
  Doc -> Parser e Range -> Parser e Range
forall tok a. Doc -> Parser tok a -> Parser tok a
doc (String -> Doc
text (String -> String
forall a. Show a => a -> String
show String
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 :: String
str = QName -> String
forall a. Pretty a => a -> String
prettyShow (QName -> String) -> QName -> String
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
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [String -> NamePart
Id String
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 | String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== QName -> String
forall a. Pretty a => a -> String
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 t. HasRange t => t -> 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 :: Parser e Name
atLeastTwoParts =
  (\(Maybe (Range, NameInScope), NamePart)
p1 [(Maybe (Range, NameInScope), NamePart)]
ps (Maybe (Range, NameInScope), NamePart)
p2 ->
      let all :: [(Maybe (Range, NameInScope), NamePart)]
all = (Maybe (Range, NameInScope), NamePart)
p1 (Maybe (Range, NameInScope), NamePart)
-> [(Maybe (Range, NameInScope), NamePart)]
-> [(Maybe (Range, NameInScope), NamePart)]
forall a. a -> [a] -> [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))
-> [(Maybe (Range, NameInScope), NamePart)]
-> [(Range, NameInScope)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Range, NameInScope), NamePart)
-> Maybe (Range, NameInScope)
forall a b. (a, b) -> a
fst [(Maybe (Range, NameInScope), NamePart)]
all of
        (Range
r,NameInScope
nis) : [(Range, NameInScope)]
_ -> Range -> NameInScope -> [NamePart] -> Name
Name Range
r NameInScope
nis (((Maybe (Range, NameInScope), NamePart) -> NamePart)
-> [(Maybe (Range, NameInScope), NamePart)] -> [NamePart]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Range, NameInScope), NamePart) -> NamePart
forall a b. (a, b) -> b
snd [(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 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
$ \MaybePlaceholder e
tok -> case MaybePlaceholder e
tok of
    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 String
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), String -> NamePart
Id String
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 :: 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
$ \ e
e -> Pattern -> Maybe Binder
isBinderP (Pattern -> Maybe Binder) -> Maybe Pattern -> Maybe Binder
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< e -> Maybe Pattern
forall e. IsExpr e => e -> Maybe Pattern
patternView e
e

-- | 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 :: 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 ([Name] -> [Name]
forall a. [a] -> [a]
init ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ QName -> [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
$ (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
&& [NamedArg (MaybePlaceholder (OpApp e))] -> Int
noPlaceholders [NamedArg (MaybePlaceholder (OpApp 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
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> ExprView e
forall e.
QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> ExprView e
OpAppV QName
q' Set Name
names [NamedArg (MaybePlaceholder (OpApp e))]
args)
        where
        args :: [NamedArg (MaybePlaceholder (OpApp e))]
args = (Int -> NamedArg (MaybePlaceholder (OpApp e)))
-> [Int] -> [NamedArg (MaybePlaceholder (OpApp 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 t. SetRange t => Range -> t -> t
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] -> String -> Parser MemoKey e (MaybePlaceholder e) Range
forall e. IsExpr e => [Name] -> String -> Parser e Range
partP [Name]
ms (RString -> String
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_ (Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [NamePart
Hole])
                 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 b) -> f (f b)
set b
x f (f b)
arg = (f b -> f b) -> f (f b) -> f (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> f b -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> b -> b
forall a b. a -> b -> a
const b
x)) f (f b)
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 b.
(Functor f, Functor f) =>
b -> f (f b) -> 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)] -> case [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] of
        [] -> MaybePlaceholder (OpApp e)
-> NamedArg (Ranged Int) -> NamedArg (MaybePlaceholder (OpApp e))
forall (f :: * -> *) (f :: * -> *) b b.
(Functor f, Functor f) =>
b -> f (f b) -> 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
        [LamBinding]
bs -> MaybePlaceholder (OpApp e)
-> NamedArg (Ranged Int) -> NamedArg (MaybePlaceholder (OpApp e))
forall (f :: * -> *) (f :: * -> *) b b.
(Functor f, Functor f) =>
b -> f (f b) -> f (f b)
set (OpApp e -> MaybePlaceholder (OpApp e)
forall e. e -> MaybePlaceholder e
noPlaceholder (Range -> [LamBinding] -> e -> OpApp e
forall e. Range -> [LamBinding] -> e -> OpApp e
SyntaxBindingLambda ([LamBinding] -> e -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange [LamBinding]
bs e
e) [LamBinding]
bs e
e)) NamedArg (Ranged Int)
arg
      [(MaybePlaceholder e, NamedArg (Ranged Int))]
_ -> NamedArg (MaybePlaceholder (OpApp e))
forall a. HasCallStack => a
__IMPOSSIBLE__

  noPlaceholders :: [NamedArg (MaybePlaceholder (OpApp e))] -> Int
  noPlaceholders :: [NamedArg (MaybePlaceholder (OpApp e))] -> Int
noPlaceholders = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int)
-> ([NamedArg (MaybePlaceholder (OpApp e))] -> [Int])
-> [NamedArg (MaybePlaceholder (OpApp e))]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg (MaybePlaceholder (OpApp e)) -> Int)
-> [NamedArg (MaybePlaceholder (OpApp e))] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (MaybePlaceholder (OpApp e) -> Int
forall p e. Num p => MaybePlaceholder e -> p
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 -> p
isPlaceholder NoPlaceholder{} = p
0
    isPlaceholder Placeholder{}   = p
1

argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e]
argsP :: Parser e e -> Parser e [NamedArg e]
argsP Parser e e
p = Parser MemoKey e (MaybePlaceholder e) (NamedArg e)
-> Parser e [NamedArg e]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (e -> NamedArg e
forall a. IsExpr a => a -> Arg (Named_ a)
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 :: a -> Arg (Named_ a)
mkArg a
e = case a -> ExprView a
forall e. IsExpr e => e -> ExprView e
exprView a
e of
    HiddenArgV   Named_ a
e -> Arg (Named_ a) -> Arg (Named_ a)
forall a. LensHiding a => a -> a
hide (Named_ a -> Arg (Named_ a)
forall a. a -> Arg a
defaultArg Named_ a
e)
    InstanceArgV Named_ a
e -> Arg (Named_ a) -> Arg (Named_ a)
forall a. LensHiding a => a -> a
makeInstance (Named_ a -> Arg (Named_ a)
forall a. a -> Arg a
defaultArg Named_ a
e)
    ExprView a
_              -> Named_ a -> Arg (Named_ a)
forall a. a -> Arg a
defaultArg (a -> Named_ a
forall a name. a -> Named name a
unnamed a
e)

appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e
appP :: 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 :: (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