    -- | Utility functions used in the Happy parser.

    module Agda.Syntax.Parser.Helpers where

    import Prelude hiding (null)

    import Control.Applicative ( (<|>) )
    import Control.Monad.State ( modify' )

    import Data.Bifunctor (first, second)
    import Data.Char
    import qualified Data.List as List
    import Data.Maybe
    import Data.Semigroup ((<>), sconcat)
    import Data.Text (Text)
    import qualified Data.Text as T

    import Agda.Syntax.Position
    import Agda.Syntax.Parser.Monad
    import Agda.Syntax.Parser.Lexer
    import Agda.Syntax.Parser.Tokens
    import Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Attribute as CA
    import Agda.Syntax.Concrete.Pattern
    import Agda.Syntax.Common
    import Agda.Syntax.Notation
    import Agda.Syntax.Literal

    import Agda.TypeChecking.Positivity.Occurrence

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.Hash
    import Agda.Utils.List ( spanJust, chopWhen, initLast )
    import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty hiding ((<>))
    import Agda.Utils.Singleton
    import qualified Agda.Utils.Maybe.Strict as Strict
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.List2 as List2

    import Agda.Utils.Impossible

    -- | Grab leading OPTIONS pragmas.
    takeOptionsPragmas :: [Declaration] -> Module
    takeOptionsPragmas :: [Declaration] -> Module
    takeOptionsPragmas = ([Pragma] -> [Declaration] -> Module)
    -> ([Pragma], [Declaration]) -> Module
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry [Pragma] -> [Declaration] -> Module
    Mod (([Pragma], [Declaration]) -> Module)
    -> ([Declaration] -> ([Pragma], [Declaration]))
    -> [Declaration]
    -> Module
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Declaration -> Maybe Pragma)
    -> [Declaration] -> ([Pragma], [Declaration])
    forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
    spanJust (\ Declaration
    d -> case Declaration
    d of
      Pragma p :: Pragma
    p@OptionsPragma{} -> Pragma -> Maybe Pragma
    forall a. a -> Maybe a
    Just Pragma
    p
      Declaration
    _                        -> Maybe Pragma
    forall a. Maybe a
    Nothing)

    -- | Insert a top-level module if there is none.
    --   Also fix-up for the case the declarations in the top-level module
    --   are not indented (this is allowed as a special case).
    figureOutTopLevelModule :: [Declaration] -> [Declaration]
    figureOutTopLevelModule :: [Declaration] -> [Declaration]
    figureOutTopLevelModule [Declaration]
    ds =
      case [Declaration] -> ([Declaration], [Declaration])
    spanAllowedBeforeModule [Declaration]
    ds of
        -- Andreas 2016-02-01, issue #1388.
        -- We need to distinguish two additional cases.

        -- Case 1: Regular file layout: imports followed by one module. Nothing to do.
        ([Declaration]
    ds0, [ Module{} ]) -> [Declaration]
    ds

        -- Case 2: The declarations in the module are not indented.
        -- This is allowed for the top level module, and thus rectified here.
        ([Declaration]
    ds0, Module Range
    r Erased
    erased QName
    m Telescope
    tel [] : [Declaration]
    ds2) ->
          [Declaration]
    ds0 [Declaration] -> [Declaration] -> [Declaration]
    forall a. [a] -> [a] -> [a]
    ++ [Range
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    r Erased
    erased QName
    m Telescope
    tel [Declaration]
    ds2]

        -- Case 3: There is a module with indented declarations,
        -- followed by non-indented declarations.  This should be a
        -- parse error and be reported later (see @toAbstract TopLevel{}@),
        -- thus, we do not do anything here.
        ([Declaration]
    ds0, Module Range
    r Erased
    _ QName
    m Telescope
    tel [Declaration]
    ds1 : [Declaration]
    ds2) -> [Declaration]
    ds  -- Gives parse error in scope checker.
        -- OLD code causing issue 1388:
        -- (ds0, Module r m tel ds1 : ds2) -> ds0 ++ [Module r m tel $ ds1 ++ ds2]

        -- Case 4: a top-level module declaration is missing.
        -- Andreas, 2017-01-01, issue #2229:
        -- Put everything (except OPTIONS pragmas) into an anonymous module.
        ([Declaration], [Declaration])
    _ -> [Declaration]
    ds0 [Declaration] -> [Declaration] -> [Declaration]
    forall a. [a] -> [a] -> [a]
    ++ [Range
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    r Erased
    defaultErased (Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ Range -> Name
    noName Range
    r) [] [Declaration]
    ds1]
          where
          ([Declaration]
    ds0, [Declaration]
    ds1) = ((Declaration -> Bool)
    -> [Declaration] -> ([Declaration], [Declaration])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    `span` [Declaration]
    ds) ((Declaration -> Bool) -> ([Declaration], [Declaration]))
    -> (Declaration -> Bool) -> ([Declaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ \case
            Pragma OptionsPragma{} -> Bool
    True
            Declaration
    _ -> Bool
    False
          -- Andreas, 2017-05-17, issue #2574.
          -- Since the module noName will act as jump target, it needs a range.
          -- We use the beginning of the file as beginning of the top level module.
          r :: Range
    r = Range -> Range
    forall a. BeginningOfFile a => a -> Range
    beginningOfFile (Range -> Range) -> Range -> Range
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Range
    forall a. HasRange a => a -> Range
    getRange [Declaration]
    ds1

    -- | Create a name from a string. The boolean indicates whether a part
    -- of the name can be token 'constructor'.
    mkName' :: Bool -> (Interval, String) -> Parser Name
    mkName' :: Bool -> (Interval, [Char]) -> Parser Name
    mkName' Bool
    constructor (Interval
    i, [Char]
    s) =
      ([Char] -> Parser Name)
    -> (Name -> Parser Name) -> Either [Char] Name -> Parser Name
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either [Char] -> Parser Name
    forall a. [Char] -> Parser a
    parseError Name -> Parser Name
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either [Char] Name -> Parser Name)
    -> Either [Char] Name -> Parser Name
    forall a b. (a -> b) -> a -> b
    $ Bool -> Range -> [Char] -> Either [Char] Name
    mkValidName Bool
    constructor (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i) [Char]
    s

    -- | Create a name from a string. The boolean indicates whether a part
    -- of the name can be token 'constructor'.
    mkValidName :: Bool -> Range -> String -> Either String Name
    mkValidName :: Bool -> Range -> [Char] -> Either [Char] Name
    mkValidName Bool
    constructor' Range
    r [Char]
    s = do
        let
          xs :: NameParts
    xs = [Char] -> NameParts
    C.stringNameParts [Char]
    s

          -- The keyword constructor can appear as the only NamePart in the
          -- last segment of a qualified name --- Foo.constructor refers to
          -- the constructor of the record Foo.
          constructor :: Bool
    constructor = case NameParts
    xs of
            NamePart
    _ :| [] -> Bool
    constructor'
            NameParts
    _       -> Bool
    False
          --  The constructor' argument to mkName' determines whether this
          --  is the last segment of a QName, the local variable constructor
          --  additionally takes whether it's the only NamePart into
          --  consideration.

        (NamePart -> Either [Char] ()) -> NameParts -> Either [Char] ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Bool -> NamePart -> Either [Char] ()
    isValidId Bool
    constructor) NameParts
    xs
        Bool -> Either [Char] () -> Either [Char] ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (NameParts -> Bool
    alternating NameParts
    xs) (Either [Char] () -> Either [Char] ())
    -> Either [Char] () -> Either [Char] ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Either [Char] ()
    forall {a} {b}. a -> Either a b
    parseError ([Char] -> Either [Char] ()) -> [Char] -> Either [Char] ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "a name cannot contain two consecutive underscores"
        Name -> Either [Char] Name
    forall a. a -> Either [Char] a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> Either [Char] Name) -> Name -> Either [Char] Name
    forall a b. (a -> b) -> a -> b
    $ Range -> NameInScope -> NameParts -> Name
    Name Range
    r NameInScope
    InScope NameParts
    xs
        where
            parseError :: a -> Either a b
    parseError = a -> Either a b
    forall {a} {b}. a -> Either a b
    Left
            isValidId :: Bool -> NamePart -> Either [Char] ()
    isValidId Bool
    _ NamePart
    Hole   = () -> Either [Char] ()
    forall a. a -> Either [Char] a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            isValidId Bool
    con (Id [Char]
    y) = do
              let x :: [Char]
    x = [Char] -> [Char]
    rawNameToString [Char]
    y
                  err :: [Char]
    err = [Char]
    "in the name " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", the part " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is not valid"
              case ParseFlags -> [Int] -> Parser Token -> [Char] -> ParseResult Token
    forall a.
    ParseFlags -> [Int] -> Parser a -> [Char] -> ParseResult a
    parse ParseFlags
    defaultParseFlags [Int
    0] ((Token -> Parser Token) -> Parser Token
    forall a. (Token -> Parser a) -> Parser a
    lexer Token -> Parser Token
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return) [Char]
    x of
                ParseOk ParseState
    _ TokId{}  -> () -> Either [Char] ()
    forall a. a -> Either [Char] a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                ParseFailed{}      -> [Char] -> Either [Char] ()
    forall {a} {b}. a -> Either a b
    parseError [Char]
    err
                ParseOk ParseState
    _ TokEOF{} -> [Char] -> Either [Char] ()
    forall {a} {b}. a -> Either a b
    parseError [Char]
    err
                ParseOk ParseState
    _ (TokKeyword Keyword
    KwConstructor Interval
    _) | Bool
    con -> () -> Either [Char] ()
    forall a. a -> Either [Char] a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                ParseOk ParseState
    _ Token
    t   -> [Char] -> Either [Char] ()
    forall {a} {b}. a -> Either a b
    parseError ([Char] -> Either [Char] ())
    -> ([Char] -> [Char]) -> [Char] -> Either [Char] ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char]
    err [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " because it is ") [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) ([Char] -> Either [Char] ()) -> [Char] -> Either [Char] ()
    forall a b. (a -> b) -> a -> b
    $ case Token
    t of
                  TokQId{}      -> [Char]
    "qualified"
                  TokKeyword{}  -> [Char]
    "a keyword"
                  TokLiteral{}  -> [Char]
    "a literal"
                  TokSymbol Symbol
    s Interval
    _ -> case Symbol
    s of
                    Symbol
    SymDot               -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- "reserved"
                    Symbol
    SymSemi              -> [Char]
    "used to separate declarations"
                    Symbol
    SymVirtualSemi       -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Symbol
    SymBar               -> [Char]
    "used for with-arguments"
                    Symbol
    SymColon             -> [Char]
    "part of declaration syntax"
                    Symbol
    SymArrow             -> [Char]
    "the function arrow"
                    Symbol
    SymEqual             -> [Char]
    "part of declaration syntax"
                    Symbol
    SymLambda            -> [Char]
    "used for lambda-abstraction"
                    Symbol
    SymUnderscore        -> [Char]
    "used for anonymous identifiers"
                    Symbol
    SymQuestionMark      -> [Char]
    "a meta variable"
                    Symbol
    SymAs                -> [Char]
    "used for as-patterns"
                    Symbol
    SymOpenParen         -> [Char]
    "used to parenthesize expressions"
                    Symbol
    SymCloseParen        -> [Char]
    "used to parenthesize expressions"
                    Symbol
    SymOpenIdiomBracket  -> [Char]
    "an idiom bracket"
                    Symbol
    SymCloseIdiomBracket -> [Char]
    "an idiom bracket"
                    Symbol
    SymEmptyIdiomBracket -> [Char]
    "an empty idiom bracket"
                    Symbol
    SymDoubleOpenBrace   -> [Char]
    "used for instance arguments"
                    Symbol
    SymDoubleCloseBrace  -> [Char]
    "used for instance arguments"
                    Symbol
    SymOpenBrace         -> [Char]
    "used for hidden arguments"
                    Symbol
    SymCloseBrace        -> [Char]
    "used for hidden arguments"
                    Symbol
    SymOpenVirtualBrace  -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Symbol
    SymCloseVirtualBrace -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    Symbol
    SymOpenPragma        -> [Char]
    "used for pragmas"
                    Symbol
    SymClosePragma       -> [Char]
    "used for pragmas"
                    Symbol
    SymEllipsis          -> [Char]
    "used for function clauses"
                    Symbol
    SymDotDot            -> [Char]
    "a modality"
                    Symbol
    SymEndComment        -> [Char]
    "the end-of-comment brace"
                  TokString{}   -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  TokTeX{}      -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- used by the LaTeX backend only
                  TokMarkup{}   -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- ditto
                  TokComment{}  -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  TokDummy{}    -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- we know that there are no two Ids in a row
            alternating :: NameParts -> Bool
    alternating (NamePart
    Hole :| NamePart
    Hole : [NamePart]
    _) = Bool
    False
            alternating (NamePart
    _    :| NamePart
    x   : [NamePart]
    xs) = NameParts -> Bool
    alternating (NameParts -> Bool) -> NameParts -> Bool
    forall a b. (a -> b) -> a -> b
    $ NamePart
    x NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| [NamePart]
    xs
            alternating (NamePart
    _    :|       []) = Bool
    True

    -- | Create a name from a string
    mkName :: (Interval, String) -> Parser Name
    mkName :: (Interval, [Char]) -> Parser Name
    mkName = Bool -> (Interval, [Char]) -> Parser Name
    mkName' Bool
    False

    -- | Create a qualified name from a list of strings
    mkQName :: [(Interval, String)] -> Parser QName
    mkQName :: [(Interval, [Char])] -> Parser QName
    mkQName [(Interval, [Char])]
    ss | Just ([(Interval, [Char])]
    ss0, (Interval, [Char])
    ss1) <- [(Interval, [Char])]
    -> Maybe ([(Interval, [Char])], (Interval, [Char]))
    forall a. [a] -> Maybe ([a], a)
    initLast [(Interval, [Char])]
    ss = do
      xs0 <- ((Interval, [Char]) -> Parser Name)
    -> [(Interval, [Char])] -> Parser [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Interval, [Char]) -> Parser Name
    mkName [(Interval, [Char])]
    ss0
      xs1 <- mkName' True ss1
      return $ foldr Qual (QName xs1) xs0
    mkQName [(Interval, [Char])]
    _ = Parser QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- The lexer never gives us an empty list of parts

    mkDomainFree_ :: (NamedArg Binder -> NamedArg Binder) -> Maybe Pattern -> Name -> NamedArg Binder
    mkDomainFree_ :: (NamedArg Binder -> NamedArg Binder)
    -> Maybe Pattern -> Name -> NamedArg Binder
    mkDomainFree_ NamedArg Binder -> NamedArg Binder
    f Maybe Pattern
    p Name
    n = NamedArg Binder -> NamedArg Binder
    f (NamedArg Binder -> NamedArg Binder)
    -> NamedArg Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ Binder -> NamedArg Binder
    forall a. a -> NamedArg a
    defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ Maybe Pattern -> BinderNameOrigin -> BoundName -> Binder
    forall a. Maybe Pattern -> BinderNameOrigin -> a -> Binder' a
    Binder Maybe Pattern
    p BinderNameOrigin
    UserBinderName (BoundName -> Binder) -> BoundName -> Binder
    forall a b. (a -> b) -> a -> b
    $ Name -> BoundName
    mkBoundName_ Name
    n

    mkRString :: (Interval, String) -> RString
    mkRString :: (Interval, [Char]) -> RString
    mkRString (Interval
    i, [Char]
    s) = Range -> [Char] -> RString
    forall a. Range -> a -> Ranged a
    Ranged (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i) [Char]
    s

    mkRText :: (Interval, String) -> Ranged Text
    mkRText :: (Interval, [Char]) -> Ranged Text
    mkRText (Interval
    i, [Char]
    s) = Range -> Text -> Ranged Text
    forall a. Range -> a -> Ranged a
    Ranged (Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i) (Text -> Ranged Text) -> Text -> Ranged Text
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Text
    T.pack [Char]
    s

    -- | Create a qualified name from a string (used in pragmas).
    --   Range of each name component is range of whole string.
    --   TODO: precise ranges!

    pragmaQName :: (Interval, String) -> Parser QName
    pragmaQName :: (Interval, [Char]) -> Parser QName
    pragmaQName (Interval
    r, [Char]
    s) = do
      let ss :: [[Char]]
    ss = (Char -> Bool) -> [Char] -> [[Char]]
    forall a. (a -> Bool) -> [a] -> [[a]]
    chopWhen (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '.') [Char]
    s
      [(Interval, [Char])] -> Parser QName
    mkQName ([(Interval, [Char])] -> Parser QName)
    -> [(Interval, [Char])] -> Parser QName
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> (Interval, [Char])) -> [[Char]] -> [(Interval, [Char])]
    forall a b. (a -> b) -> [a] -> [b]
    map (Interval
    r,) [[Char]]
    ss

    mkNamedArg :: Maybe QName -> Either QName Range -> Parser (NamedArg BoundName)
    mkNamedArg :: Maybe QName -> Either QName Range -> Parser (NamedArg BoundName)
    mkNamedArg Maybe QName
    x Either QName Range
    y = do
      lbl <- case Maybe QName
    x of
               Maybe QName
    Nothing        -> Maybe NamedName -> Parser (Maybe NamedName)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe NamedName -> Parser (Maybe NamedName))
    -> Maybe NamedName -> Parser (Maybe NamedName)
    forall a b. (a -> b) -> a -> b
    $ NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> RString -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    UserWritten (RString -> NamedName) -> RString -> NamedName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> RString
    forall a. a -> Ranged a
    unranged [Char]
    "_"
               Just (QName Name
    x) -> Maybe NamedName -> Parser (Maybe NamedName)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe NamedName -> Parser (Maybe NamedName))
    -> Maybe NamedName -> Parser (Maybe NamedName)
    forall a b. (a -> b) -> a -> b
    $ NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> RString -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    UserWritten (RString -> NamedName) -> RString -> NamedName
    forall a b. (a -> b) -> a -> b
    $ Range -> [Char] -> RString
    forall a. Range -> a -> Ranged a
    Ranged (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) ([Char] -> RString) -> [Char] -> RString
    forall a b. (a -> b) -> a -> b
    $ Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x
               Maybe QName
    _              -> [Char] -> Parser (Maybe NamedName)
    forall a. [Char] -> Parser a
    parseError [Char]
    "expected unqualified variable name"
      var <- case y of
               Left (QName Name
    y) -> BoundName -> Parser BoundName
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (BoundName -> Parser BoundName) -> BoundName -> Parser BoundName
    forall a b. (a -> b) -> a -> b
    $ Name -> Fixity' -> BoundName
    mkBoundName Name
    y Fixity'
    noFixity'
               Right Range
    r        -> BoundName -> Parser BoundName
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (BoundName -> Parser BoundName) -> BoundName -> Parser BoundName
    forall a b. (a -> b) -> a -> b
    $ Name -> Fixity' -> BoundName
    mkBoundName (Range -> Name
    noName Range
    r) Fixity'
    noFixity'
               Either QName Range
    _              -> [Char] -> Parser BoundName
    forall a. [Char] -> Parser a
    parseError [Char]
    "expected unqualified variable name"
      return $ defaultArg $ Named lbl var

    -- | Polarity parser.
    --
    --- Unknown polarities are replaced with the default polarity.

    parsePolarity :: (Interval, String) -> Parser (Ranged Occurrence)
    parsePolarity :: (Interval, [Char]) -> Parser (Ranged Occurrence)
    parsePolarity (Interval
    i, [Char]
    s) =
      case [Char]
    s of
        [Char]
    "_"  -> Occurrence -> Parser (Ranged Occurrence)
    ret Occurrence
    Unused
        [Char]
    "++" -> Occurrence -> Parser (Ranged Occurrence)
    ret Occurrence
    StrictPos
        [Char]
    "+"  -> Occurrence -> Parser (Ranged Occurrence)
    ret Occurrence
    JustPos
        [Char]
    "-"  -> Occurrence -> Parser (Ranged Occurrence)
    ret Occurrence
    JustNeg
        [Char]
    "*"  -> Occurrence -> Parser (Ranged Occurrence)
    ret Occurrence
    Mixed
        [Char]
    _    -> do
          ParseWarning -> Parser ()
    parseWarning (Range -> [Char] -> ParseWarning
    UnknownPolarity Range
    r [Char]
    s)
          Occurrence -> Parser (Ranged Occurrence)
    ret Occurrence
    Mixed
      where
        r :: Range
    r = Interval -> Range
    forall a. HasRange a => a -> Range
    getRange Interval
    i
        ret :: Occurrence -> Parser (Ranged Occurrence)
    ret = Ranged Occurrence -> Parser (Ranged Occurrence)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ranged Occurrence -> Parser (Ranged Occurrence))
    -> (Occurrence -> Ranged Occurrence)
    -> Occurrence
    -> Parser (Ranged Occurrence)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Occurrence -> Ranged Occurrence
    forall a. Range -> a -> Ranged a
    Ranged Range
    r

    recoverLayout :: [(Interval, String)] -> String
    recoverLayout :: [(Interval, [Char])] -> [Char]
    recoverLayout [] = [Char]
    ""
    recoverLayout xs :: [(Interval, [Char])]
    xs@((Interval
    i, [Char]
    _) : [(Interval, [Char])]
    _) = Position' SrcFile -> [(Interval, [Char])] -> [Char]
    go (Interval -> Position' SrcFile
    forall a. Interval' a -> Position' a
    iStart Interval
    i) [(Interval, [Char])]
    xs
      where
        c0 :: Word32
    c0 = Position' SrcFile -> Word32
    forall a. Position' a -> Word32
    posCol (Interval -> Position' SrcFile
    forall a. Interval' a -> Position' a
    iStart Interval
    i)

        go :: Position' SrcFile -> [(Interval, [Char])] -> [Char]
    go Position' SrcFile
    cur [] = [Char]
    ""
        go Position' SrcFile
    cur ((Interval
    i, [Char]
    s) : [(Interval, [Char])]
    xs) = Position' SrcFile -> Position' SrcFile -> [Char]
    padding Position' SrcFile
    cur (Interval -> Position' SrcFile
    forall a. Interval' a -> Position' a
    iStart Interval
    i) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Position' SrcFile -> [(Interval, [Char])] -> [Char]
    go (Interval -> Position' SrcFile
    forall a. Interval' a -> Position' a
    iEnd Interval
    i) [(Interval, [Char])]
    xs

        padding :: Position' SrcFile -> Position' SrcFile -> [Char]
    padding Pn{ posLine :: forall a. Position' a -> Word32
    posLine = Word32
    l1, posCol :: forall a. Position' a -> Word32
    posCol = Word32
    c1 } Pn{ posLine :: forall a. Position' a -> Word32
    posLine = Word32
    l2, posCol :: forall a. Position' a -> Word32
    posCol = Word32
    c2 }
          | Word32
    l1 Word32 -> Word32 -> Bool
    forall a. Ord a => a -> a -> Bool
    < Word32
    l2   = Word32 -> Char -> [Char]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate (Word32
    l2 Word32 -> Word32 -> Word32
    forall a. Num a => a -> a -> a
    - Word32
    l1) Char
    '\n' [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Word32 -> Char -> [Char]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate (Word32 -> Word32 -> Word32
    forall a. Ord a => a -> a -> a
    max Word32
    0 (Word32
    c2 Word32 -> Word32 -> Word32
    forall a. Num a => a -> a -> a
    - Word32
    c0)) Char
    ' '
          | Word32
    l1 Word32 -> Word32 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Word32
    l2  = Word32 -> Char -> [Char]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate (Word32
    c2 Word32 -> Word32 -> Word32
    forall a. Num a => a -> a -> a
    - Word32
    c1) Char
    ' '
          | Bool
    otherwise = [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    ensureUnqual :: QName -> Parser Name
    ensureUnqual :: QName -> Parser Name
    ensureUnqual (QName Name
    x) = Name -> Parser Name
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    x
    ensureUnqual q :: QName
    q@Qual{}  = Maybe PositionWithoutFile -> [Char] -> Parser Name
    forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
    parseError' (Range -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range -> Maybe PositionWithoutFile)
    -> Range -> Maybe PositionWithoutFile
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    q) [Char]
    "Qualified name not allowed here"

    ------------------------------------------------------------------------
    -- Lambinds

    -- | Result of parsing @LamBinds@.
    data LamBinds' a = LamBinds
      { forall a. LamBinds' a -> a
    lamBindings   :: a             -- ^ A number of domain-free or typed bindings or record patterns.
      , forall a. LamBinds' a -> Maybe Hiding
    absurdBinding :: Maybe Hiding  -- ^ Followed by possibly a final absurd pattern.
      } deriving ((forall a b. (a -> b) -> LamBinds' a -> LamBinds' b)
    -> (forall a b. a -> LamBinds' b -> LamBinds' a)
    -> Functor LamBinds'
    forall a b. a -> LamBinds' b -> LamBinds' a
    forall a b. (a -> b) -> LamBinds' a -> LamBinds' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> LamBinds' a -> LamBinds' b
    fmap :: forall a b. (a -> b) -> LamBinds' a -> LamBinds' b
    $c<$ :: forall a b. a -> LamBinds' b -> LamBinds' a
    <$ :: forall a b. a -> LamBinds' b -> LamBinds' a
    Functor)

    type LamBinds = LamBinds' [LamBinding]

    mkAbsurdBinding :: Hiding -> LamBinds
    mkAbsurdBinding :: Hiding -> LamBinds
    mkAbsurdBinding = [LamBinding] -> Maybe Hiding -> LamBinds
    forall a. a -> Maybe Hiding -> LamBinds' a
    LamBinds [] (Maybe Hiding -> LamBinds)
    -> (Hiding -> Maybe Hiding) -> Hiding -> LamBinds
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Hiding -> Maybe Hiding
    forall a. a -> Maybe a
    Just

    mkLamBinds :: a -> LamBinds' a
    mkLamBinds :: forall a. a -> LamBinds' a
    mkLamBinds a
    bs = a -> Maybe Hiding -> LamBinds' a
    forall a. a -> Maybe Hiding -> LamBinds' a
    LamBinds a
    bs Maybe Hiding
    forall a. Maybe a
    Nothing

    -- | Build a forall pi (forall x y z -> ...)
    forallPi :: List1 LamBinding -> Expr -> Expr
    forallPi :: List1 LamBinding -> Expr -> Expr
    forallPi List1 LamBinding
    bs Expr
    e = Telescope1 -> Expr -> Expr
    Pi ((LamBinding -> TypedBinding) -> List1 LamBinding -> Telescope1
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LamBinding -> TypedBinding
    addType List1 LamBinding
    bs) Expr
    e

    -- | Converts lambda bindings to typed bindings.
    addType :: LamBinding -> TypedBinding
    addType :: LamBinding -> TypedBinding
    addType (DomainFull TypedBinding
    b) = TypedBinding
    b
    addType (DomainFree NamedArg Binder
    x) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
    forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
    TBind Range
    r (NamedArg Binder -> List1 (NamedArg Binder)
    forall el coll. Singleton el coll => el -> coll
    singleton NamedArg Binder
    x) (Expr -> TypedBinding) -> Expr -> TypedBinding
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe [Char] -> Expr
    Underscore Range
    r Maybe [Char]
    forall a. Maybe a
    Nothing
      where r :: Range
    r = NamedArg Binder -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg Binder
    x

    -- | Returns the value of the first erasure attribute, if any, or else
    -- the default value of type 'Erased'.
    --
    -- Raises warnings for all attributes except for erasure attributes,
    -- and for multiple erasure attributes.

    onlyErased
      :: [Attr]  -- ^ The attributes, in reverse order.
      -> Parser Erased
    onlyErased :: [Attr] -> Parser Erased
    onlyErased [Attr]
    as = do
      es <- [Maybe Erased] -> [Erased]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe Erased] -> [Erased])
    -> Parser [Maybe Erased] -> Parser [Erased]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Attr -> Parser (Maybe Erased)) -> [Attr] -> Parser [Maybe Erased]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Attr -> Parser (Maybe Erased)
    onlyErased' ([Attr] -> [Attr]
    forall a. [a] -> [a]
    reverse [Attr]
    as)
      case es of
        []     -> Erased -> Parser Erased
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Erased
    defaultErased
        [Erased
    e]    -> Erased -> Parser Erased
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Erased
    e
        Erased
    e : [Erased]
    es -> do
          ParseWarning -> Parser ()
    parseWarning (ParseWarning -> Parser ()) -> ParseWarning -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe [Char] -> ParseWarning
    MultipleAttributes ([Erased] -> Range
    forall a. HasRange a => a -> Range
    getRange [Erased]
    es) ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "erasure")
          Erased -> Parser Erased
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Erased
    e
      where
      onlyErased' :: Attr -> Parser (Maybe Erased)
    onlyErased' Attr
    a = case Attr -> Attribute
    theAttr Attr
    a of
        RelevanceAttribute{} -> [Char] -> Parser (Maybe Erased)
    unsup [Char]
    "Relevance"
        CohesionAttribute{}  -> [Char] -> Parser (Maybe Erased)
    unsup [Char]
    "Cohesion"
        LockAttribute{}      -> [Char] -> Parser (Maybe Erased)
    unsup [Char]
    "Lock"
        CA.TacticAttribute{} -> [Char] -> Parser (Maybe Erased)
    unsup [Char]
    "Tactic"
        PolarityAttribute{}  -> [Char] -> Parser (Maybe Erased)
    unsup [Char]
    "Polarity"
        QuantityAttribute Quantity
    q  -> Parser (Maybe Erased)
    -> (Erased -> Parser (Maybe Erased))
    -> Maybe Erased
    -> Parser (Maybe Erased)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ([Char] -> Parser (Maybe Erased)
    unsup [Char]
    "Linearity") (Maybe Erased -> Parser (Maybe Erased)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Erased -> Parser (Maybe Erased))
    -> (Erased -> Maybe Erased) -> Erased -> Parser (Maybe Erased)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Erased -> Maybe Erased
    forall a. a -> Maybe a
    Just) (Maybe Erased -> Parser (Maybe Erased))
    -> Maybe Erased -> Parser (Maybe Erased)
    forall a b. (a -> b) -> a -> b
    $ Quantity -> Maybe Erased
    erasedFromQuantity Quantity
    q
        where
        unsup :: [Char] -> Parser (Maybe Erased)
    unsup [Char]
    s = do
          ParseWarning -> Parser ()
    parseWarning (ParseWarning -> Parser ()) -> ParseWarning -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe [Char] -> ParseWarning
    UnsupportedAttribute (Attr -> Range
    attrRange Attr
    a) ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    s)
          Maybe Erased -> Parser (Maybe Erased)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Erased
    forall a. Maybe a
    Nothing

    -- | Constructs extended lambdas.

    extLam
      :: Range            -- ^ The range of the lambda symbol and @where@ or
                          --   the braces.
      -> [Attr]           -- ^ The attributes in reverse order.
      -> List1 LamClause  -- ^ The clauses in reverse order.
      -> Parser Expr
    extLam :: Range -> [Attr] -> NonEmpty LamClause -> Parser Expr
    extLam Range
    symbolRange [Attr]
    attrs NonEmpty LamClause
    cs = do
      e <- [Attr] -> Parser Erased
    onlyErased [Attr]
    attrs
      let cs' = NonEmpty LamClause -> NonEmpty LamClause
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse NonEmpty LamClause
    cs
      return $ ExtendedLam (getRange (symbolRange, e, cs')) e cs'

    -- | Constructs extended or absurd lambdas.

    extOrAbsLam
      :: Range   -- ^ The range of the lambda symbol.
      -> [Attr]  -- ^ The attributes, in reverse order.
      -> Either ([LamBinding], Hiding) (List1 Expr)
      -> Parser Expr
    extOrAbsLam :: Range
    -> [Attr]
    -> Either ([LamBinding], Hiding) (List1 Expr)
    -> Parser Expr
    extOrAbsLam Range
    lambdaRange [Attr]
    attrs Either ([LamBinding], Hiding) (List1 Expr)
    cs = case Either ([LamBinding], Hiding) (List1 Expr)
    cs of
      Right List1 Expr
    es -> do
        -- It is of the form @\ { p1 ... () }@.
        e  <- [Attr] -> Parser Erased
    onlyErased [Attr]
    attrs
        cl <- mkAbsurdLamClause empty es
        return $ ExtendedLam (getRange (lambdaRange, e, es)) e $ singleton cl
      Left ([LamBinding]
    bs, Hiding
    h) -> do
        (Attr -> Parser ()) -> [Attr] -> Parser ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\Attr
    a -> ParseWarning -> Parser ()
    parseWarning (ParseWarning -> Parser ()) -> ParseWarning -> Parser ()
    forall a b. (a -> b) -> a -> b
    $
                       Range -> Maybe [Char] -> ParseWarning
    UnsupportedAttribute (Attr -> Range
    attrRange Attr
    a) Maybe [Char]
    forall a. Maybe a
    Nothing)
              ([Attr] -> [Attr]
    forall a. [a] -> [a]
    reverse [Attr]
    attrs)
        [LamBinding]
    -> Parser Expr -> (List1 LamBinding -> Parser Expr) -> Parser Expr
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull [LamBinding]
    bs
          {-then-} (Expr -> Parser Expr
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Parser Expr) -> Expr -> Parser Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Hiding -> Expr
    AbsurdLam Range
    r Hiding
    h)
          {-else-} ((List1 LamBinding -> Parser Expr) -> Parser Expr)
    -> (List1 LamBinding -> Parser Expr) -> Parser Expr
    forall a b. (a -> b) -> a -> b
    $ \ List1 LamBinding
    bs -> Expr -> Parser Expr
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Parser Expr) -> Expr -> Parser Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 LamBinding -> Expr -> Expr
    Lam Range
    r List1 LamBinding
    bs (Range -> Hiding -> Expr
    AbsurdLam Range
    r Hiding
    h)
        where
        r :: Range
    r = Range -> [LamBinding] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Range
    lambdaRange [LamBinding]
    bs

    -- | Interpret an expression as a list of names and (not parsed yet) as-patterns

    exprAsNamesAndPatterns :: Expr -> Maybe (List1 (Name, Maybe Expr))
    exprAsNamesAndPatterns :: Expr -> Maybe (List1 (Name, Maybe Expr))
    exprAsNamesAndPatterns = (Expr -> Maybe (Name, Maybe Expr))
    -> List1 Expr -> Maybe (List1 (Name, Maybe Expr))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM Expr -> Maybe (Name, Maybe Expr)
    exprAsNameAndPattern (List1 Expr -> Maybe (List1 (Name, Maybe Expr)))
    -> (Expr -> List1 Expr) -> Expr -> Maybe (List1 (Name, Maybe Expr))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> List1 Expr
    exprAsTele
      where
        exprAsTele :: Expr -> List1 Expr
        exprAsTele :: Expr -> List1 Expr
    exprAsTele (RawApp Range
    _ List2 Expr
    es) = List2 Expr -> List1 Expr
    forall a. List2 a -> List1 a
    List2.toList1 List2 Expr
    es
        exprAsTele Expr
    e             = Expr -> List1 Expr
    forall el coll. Singleton el coll => el -> coll
    singleton Expr
    e

    exprAsNameAndPattern :: Expr -> Maybe (Name, Maybe Expr)
    exprAsNameAndPattern :: Expr -> Maybe (Name, Maybe Expr)
    exprAsNameAndPattern (Ident (QName Name
    x)) = (Name, Maybe Expr) -> Maybe (Name, Maybe Expr)
    forall a. a -> Maybe a
    Just (Name
    x, Maybe Expr
    forall a. Maybe a
    Nothing)
    exprAsNameAndPattern (Underscore Range
    r Maybe [Char]
    _)  = (Name, Maybe Expr) -> Maybe (Name, Maybe Expr)
    forall a. a -> Maybe a
    Just (Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    simpleHole, Maybe Expr
    forall a. Maybe a
    Nothing)
    exprAsNameAndPattern (As Range
    _ Name
    n Expr
    e)        = (Name, Maybe Expr) -> Maybe (Name, Maybe Expr)
    forall a. a -> Maybe a
    Just (Name
    n, Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    e)
    exprAsNameAndPattern (Paren Range
    r Expr
    e)       = (Name, Maybe Expr) -> Maybe (Name, Maybe Expr)
    forall a. a -> Maybe a
    Just (Range -> Name -> Name
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Name
    simpleHole, Expr -> Maybe Expr
    forall a. a -> Maybe a
    Just Expr
    e)
    exprAsNameAndPattern Expr
    _                 = Maybe (Name, Maybe Expr)
    forall a. Maybe a
    Nothing

    -- interpret an expression as name or list of hidden / instance names
    exprAsNameOrHiddenNames :: Expr -> Maybe (List1 (NamedArg (Name, Maybe Expr)))
    exprAsNameOrHiddenNames :: Expr -> Maybe (List1 (NamedArg (Name, Maybe Expr)))
    exprAsNameOrHiddenNames = \case
      HiddenArg Range
    _ (Named Maybe NamedName
    Nothing Expr
    e) ->
        ((Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> List1 (Name, Maybe Expr) -> List1 (NamedArg (Name, Maybe Expr))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NamedArg (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr)
    forall a. LensHiding a => a -> a
    hide (NamedArg (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> ((Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> (Name, Maybe Expr)
    -> NamedArg (Name, Maybe Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr)
    forall a. a -> NamedArg a
    defaultNamedArg) (List1 (Name, Maybe Expr) -> List1 (NamedArg (Name, Maybe Expr)))
    -> Maybe (List1 (Name, Maybe Expr))
    -> Maybe (List1 (NamedArg (Name, Maybe Expr)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Maybe (List1 (Name, Maybe Expr))
    exprAsNamesAndPatterns Expr
    e
      InstanceArg Range
    _ (Named Maybe NamedName
    Nothing Expr
    e) ->
        ((Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> List1 (Name, Maybe Expr) -> List1 (NamedArg (Name, Maybe Expr))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NamedArg (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr)
    forall a. LensHiding a => a -> a
    makeInstance (NamedArg (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> ((Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> (Name, Maybe Expr)
    -> NamedArg (Name, Maybe Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr)
    forall a. a -> NamedArg a
    defaultNamedArg) (List1 (Name, Maybe Expr) -> List1 (NamedArg (Name, Maybe Expr)))
    -> Maybe (List1 (Name, Maybe Expr))
    -> Maybe (List1 (NamedArg (Name, Maybe Expr)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Maybe (List1 (Name, Maybe Expr))
    exprAsNamesAndPatterns Expr
    e
      Expr
    e ->
        NamedArg (Name, Maybe Expr) -> List1 (NamedArg (Name, Maybe Expr))
    forall el coll. Singleton el coll => el -> coll
    singleton (NamedArg (Name, Maybe Expr)
     -> List1 (NamedArg (Name, Maybe Expr)))
    -> ((Name, Maybe Expr) -> NamedArg (Name, Maybe Expr))
    -> (Name, Maybe Expr)
    -> List1 (NamedArg (Name, Maybe Expr))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Maybe Expr) -> NamedArg (Name, Maybe Expr)
    forall a. a -> NamedArg a
    defaultNamedArg ((Name, Maybe Expr) -> List1 (NamedArg (Name, Maybe Expr)))
    -> Maybe (Name, Maybe Expr)
    -> Maybe (List1 (NamedArg (Name, Maybe Expr)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Maybe (Name, Maybe Expr)
    exprAsNameAndPattern Expr
    e

    boundNamesOrAbsurd :: List1 Expr -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    boundNamesOrAbsurd :: List1 Expr
    -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    boundNamesOrAbsurd List1 Expr
    es
      | (Expr -> Bool) -> List1 Expr -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Expr -> Bool
    isAbsurd List1 Expr
    es = Either (List1 (NamedArg Binder)) (List1 Expr)
    -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (List1 (NamedArg Binder)) (List1 Expr)
     -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr)))
    -> Either (List1 (NamedArg Binder)) (List1 Expr)
    -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    forall a b. (a -> b) -> a -> b
    $ List1 Expr -> Either (List1 (NamedArg Binder)) (List1 Expr)
    forall a b. b -> Either a b
    Right List1 Expr
    es
      | Bool
    otherwise       =
        case (Expr -> Maybe (Name, Maybe Expr))
    -> List1 Expr -> Maybe (List1 (Name, Maybe Expr))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM Expr -> Maybe (Name, Maybe Expr)
    exprAsNameAndPattern List1 Expr
    es of
            Maybe (List1 (Name, Maybe Expr))
    Nothing   -> [Char] -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    forall a. [Char] -> Parser a
    parseError ([Char] -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr)))
    -> [Char] -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "expected sequence of bound identifiers"
            Just List1 (Name, Maybe Expr)
    good -> (List1 (NamedArg Binder)
     -> Either (List1 (NamedArg Binder)) (List1 Expr))
    -> Parser (List1 (NamedArg Binder))
    -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    forall a b. (a -> b) -> Parser a -> Parser b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap List1 (NamedArg Binder)
    -> Either (List1 (NamedArg Binder)) (List1 Expr)
    forall {a} {b}. a -> Either a b
    Left (Parser (List1 (NamedArg Binder))
     -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr)))
    -> Parser (List1 (NamedArg Binder))
    -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
    forall a b. (a -> b) -> a -> b
    $ List1 (Name, Maybe Expr)
    -> ((Name, Maybe Expr) -> Parser (NamedArg Binder))
    -> Parser (List1 (NamedArg Binder))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM List1 (Name, Maybe Expr)
    good (((Name, Maybe Expr) -> Parser (NamedArg Binder))
     -> Parser (List1 (NamedArg Binder)))
    -> ((Name, Maybe Expr) -> Parser (NamedArg Binder))
    -> Parser (List1 (NamedArg Binder))
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    n, Maybe Expr
    me) -> do
                           p <- (Expr -> Parser Pattern) -> Maybe Expr -> Parser (Maybe Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse Expr -> Parser Pattern
    exprToPattern Maybe Expr
    me
                           return (defaultNamedArg (Binder p UserBinderName (mkBoundName_ n)))

      where

        isAbsurd :: Expr -> Bool
        isAbsurd :: Expr -> Bool
    isAbsurd (Absurd Range
    _)                  = Bool
    True
        isAbsurd (HiddenArg Range
    _ (Named Maybe NamedName
    _ Expr
    e))   = Expr -> Bool
    isAbsurd Expr
    e
        isAbsurd (InstanceArg Range
    _ (Named Maybe NamedName
    _ Expr
    e)) = Expr -> Bool
    isAbsurd Expr
    e
        isAbsurd (Paren Range
    _ Expr
    e)                 = Expr -> Bool
    isAbsurd Expr
    e
        isAbsurd (As Range
    _ Name
    _ Expr
    e)                  = Expr -> Bool
    isAbsurd Expr
    e
        isAbsurd (RawApp Range
    _ List2 Expr
    es)               = (Expr -> Bool) -> List2 Expr -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Expr -> Bool
    isAbsurd List2 Expr
    es
        isAbsurd Expr
    _                           = Bool
    False

    -- | Match a pattern-matching "assignment" statement @p <- e@
    exprToAssignment :: Expr -> Parser (Maybe (Pattern, Range, Expr))
    exprToAssignment :: Expr -> Parser (Maybe (Pattern, Range, Expr))
    exprToAssignment e :: Expr
    e@(RawApp Range
    r List2 Expr
    es)
      | ([Expr]
    es1, Expr
    arr : [Expr]
    es2) <- (Expr -> Bool) -> List2 Expr -> ([Expr], [Expr])
    forall a. (a -> Bool) -> List2 a -> ([a], [a])
    List2.break Expr -> Bool
    isLeftArrow List2 Expr
    es =
        case (Expr -> Bool) -> [Expr] -> [Expr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Expr -> Bool
    isLeftArrow [Expr]
    es2 of
          Expr
    arr : [Expr]
    _ -> Maybe PositionWithoutFile
    -> [Char] -> Parser (Maybe (Pattern, Range, Expr))
    forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
    parseError' (Range -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range -> Maybe PositionWithoutFile)
    -> Range -> Maybe PositionWithoutFile
    forall a b. (a -> b) -> a -> b
    $ Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    arr) ([Char] -> Parser (Maybe (Pattern, Range, Expr)))
    -> [Char] -> Parser (Maybe (Pattern, Range, Expr))
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    arr
          [] ->
            -- Andreas, 2021-05-06, issue #5365
            -- Handle pathological cases like @do <-@ and @do x <-@.
            case ([Expr]
    es1, [Expr]
    es2) of
              (Expr
    e1:[Expr]
    rest1, Expr
    e2:[Expr]
    rest2) -> do
                p <- Expr -> Parser Pattern
    exprToPattern (Expr -> Parser Pattern) -> Expr -> Parser Pattern
    forall a b. (a -> b) -> a -> b
    $ List1 Expr -> Expr
    rawApp (List1 Expr -> Expr) -> List1 Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e1 Expr -> [Expr] -> List1 Expr
    forall a. a -> [a] -> NonEmpty a
    :| [Expr]
    rest1
                pure $ Just (p, getRange arr, rawApp (e2 :| rest2))
              ([Expr], [Expr])
    _ -> Maybe PositionWithoutFile
    -> [Char] -> Parser (Maybe (Pattern, Range, Expr))
    forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
    parseError' (Range -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range -> Maybe PositionWithoutFile)
    -> Range -> Maybe PositionWithoutFile
    forall a b. (a -> b) -> a -> b
    $ Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e) ([Char] -> Parser (Maybe (Pattern, Range, Expr)))
    -> [Char] -> Parser (Maybe (Pattern, Range, Expr))
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Incomplete binding " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    e
      where
        isLeftArrow :: Expr -> Bool
    isLeftArrow (Ident (QName (Name Range
    _ NameInScope
    _ (Id [Char]
    arr :| [])))) =
          [Char]
    arr [Char] -> [[Char]] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [[Char]
    "<-", [Char]
    "\x2190"]  -- \leftarrow [issue #5465, unicode might crash happy]
        isLeftArrow Expr
    _ = Bool
    False
    exprToAssignment Expr
    _ = Maybe (Pattern, Range, Expr)
    -> Parser (Maybe (Pattern, Range, Expr))
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (Pattern, Range, Expr)
    forall a. Maybe a
    Nothing

    -- | Build a with-block
    buildWithBlock ::
      [Either RewriteEqn (List1 (Named Name Expr))] ->
      Parser ([RewriteEqn], [Named Name Expr])
    buildWithBlock :: [Either RewriteEqn (List1 (Named Name Expr))]
    -> Parser ([RewriteEqn], [Named Name Expr])
    buildWithBlock [Either RewriteEqn (List1 (Named Name Expr))]
    rees = case [Either RewriteEqn (List1 (Named Name Expr))]
    -> [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    forall a b. [Either a b] -> [Either (List1 a) (List1 b)]
    groupByEither [Either RewriteEqn (List1 (Named Name Expr))]
    rees of
      (Left List1 RewriteEqn
    rs : [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    rest) -> (List1 RewriteEqn -> [Item (List1 RewriteEqn)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 RewriteEqn
    rs,) ([Named Name Expr] -> ([RewriteEqn], [Named Name Expr]))
    -> Parser [Named Name Expr]
    -> Parser ([RewriteEqn], [Named Name Expr])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    -> Parser [Named Name Expr]
    forall a b.
    (HasRange a, HasRange b) =>
    [Either (List1 a) (List1 (List1 b))] -> Parser [b]
    finalWith [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    rest
      [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    rest             -> ([],) ([Named Name Expr] -> ([RewriteEqn], [Named Name Expr]))
    -> Parser [Named Name Expr]
    -> Parser ([RewriteEqn], [Named Name Expr])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    -> Parser [Named Name Expr]
    forall a b.
    (HasRange a, HasRange b) =>
    [Either (List1 a) (List1 (List1 b))] -> Parser [b]
    finalWith [Either (List1 RewriteEqn) (List1 (List1 (Named Name Expr)))]
    rest

      where

        finalWith :: (HasRange a, HasRange b) =>
                     [Either (List1 a) (List1 (List1 b))] -> Parser [b]
        finalWith :: forall a b.
    (HasRange a, HasRange b) =>
    [Either (List1 a) (List1 (List1 b))] -> Parser [b]
    finalWith []             = [b] -> Parser [b]
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([b] -> Parser [b]) -> [b] -> Parser [b]
    forall a b. (a -> b) -> a -> b
    $ []
        finalWith [Right List1 (List1 b)
    ees]    = [b] -> Parser [b]
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([b] -> Parser [b]) -> [b] -> Parser [b]
    forall a b. (a -> b) -> a -> b
    $ List1 b -> [Item (List1 b)]
    forall l. IsList l => l -> [Item l]
    List1.toList (List1 b -> [Item (List1 b)]) -> List1 b -> [Item (List1 b)]
    forall a b. (a -> b) -> a -> b
    $ List1 (List1 b) -> List1 b
    forall a. Semigroup a => NonEmpty a -> a
    sconcat List1 (List1 b)
    ees
        finalWith (Right{} : [Either (List1 a) (List1 (List1 b))]
    tl) = Maybe PositionWithoutFile -> [Char] -> Parser [b]
    forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
    parseError' (Range -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range -> Maybe PositionWithoutFile)
    -> Range -> Maybe PositionWithoutFile
    forall a b. (a -> b) -> a -> b
    $ [Either (List1 a) (List1 (List1 b))] -> Range
    forall a. HasRange a => a -> Range
    getRange [Either (List1 a) (List1 (List1 b))]
    tl)
          [Char]
    "Cannot use rewrite / pattern-matching with after a with-abstraction."
        finalWith (Left{} : [Either (List1 a) (List1 (List1 b))]
    _)   = Parser [b]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Build a with-statement
    buildWithStmt :: List1 (Named Name Expr) ->
                     Parser [Either RewriteEqn (List1 (Named Name Expr))]
    buildWithStmt :: List1 (Named Name Expr)
    -> Parser [Either RewriteEqn (List1 (Named Name Expr))]
    buildWithStmt List1 (Named Name Expr)
    nes = do
      ws <- (Named Name Expr
     -> Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr)))
    -> [Named Name Expr]
    -> Parser [Either (Named Name (Pattern, Expr)) (Named Name Expr)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Named Name Expr
    -> Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr))
    buildSingleWithStmt (List1 (Named Name Expr) -> [Item (List1 (Named Name Expr))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (Named Name Expr)
    nes)
      let rws = [Either (Named Name (Pattern, Expr)) (Named Name Expr)]
    -> [Either
          (List1 (Named Name (Pattern, Expr))) (List1 (Named Name Expr))]
    forall a b. [Either a b] -> [Either (List1 a) (List1 b)]
    groupByEither [Either (Named Name (Pattern, Expr)) (Named Name Expr)]
    ws
      pure $ map (first (Invert ())) rws

    buildUsingStmt :: List1 Expr -> Parser RewriteEqn
    buildUsingStmt :: List1 Expr -> Parser RewriteEqn
    buildUsingStmt List1 Expr
    es = do
      mpatexprs <- (Expr -> Parser (Maybe (Pattern, Range, Expr)))
    -> List1 Expr -> Parser (NonEmpty (Maybe (Pattern, Range, Expr)))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM Expr -> Parser (Maybe (Pattern, Range, Expr))
    exprToAssignment List1 Expr
    es
      case mapM (fmap $ \(Pattern
    pat, Range
    _, Expr
    expr) -> (Pattern
    pat, Expr
    expr)) mpatexprs of
        Maybe (NonEmpty (Pattern, Expr))
    Nothing -> Maybe PositionWithoutFile -> [Char] -> Parser RewriteEqn
    forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
    parseError' (Range -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range -> Maybe PositionWithoutFile)
    -> Range -> Maybe PositionWithoutFile
    forall a b. (a -> b) -> a -> b
    $ List1 Expr -> Range
    forall a. HasRange a => a -> Range
    getRange List1 Expr
    es) [Char]
    "Expected assignments"
        Just NonEmpty (Pattern, Expr)
    assignments -> RewriteEqn -> Parser RewriteEqn
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (RewriteEqn -> Parser RewriteEqn)
    -> RewriteEqn -> Parser RewriteEqn
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (Pattern, Expr) -> RewriteEqn
    forall qn nm p e. List1 (p, e) -> RewriteEqn' qn nm p e
    LeftLet NonEmpty (Pattern, Expr)
    assignments

    buildSingleWithStmt ::
      Named Name Expr ->
      Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr))
    buildSingleWithStmt :: Named Name Expr
    -> Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr))
    buildSingleWithStmt Named Name Expr
    e = do
      mpatexpr <- Expr -> Parser (Maybe (Pattern, Range, Expr))
    exprToAssignment (Named Name Expr -> Expr
    forall name a. Named name a -> a
    namedThing Named Name Expr
    e)
      pure $ case mpatexpr of
        Just (Pattern
    pat, Range
    _, Expr
    expr) -> Named Name (Pattern, Expr)
    -> Either (Named Name (Pattern, Expr)) (Named Name Expr)
    forall {a} {b}. a -> Either a b
    Left ((Pattern
    pat, Expr
    expr) (Pattern, Expr) -> Named Name Expr -> Named Name (Pattern, Expr)
    forall a b. a -> Named Name b -> Named Name a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Named Name Expr
    e)
        Maybe (Pattern, Range, Expr)
    Nothing             -> Named Name Expr
    -> Either (Named Name (Pattern, Expr)) (Named Name Expr)
    forall a b. b -> Either a b
    Right Named Name Expr
    e

    -- | Build a do-statement
    defaultBuildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
    defaultBuildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
    defaultBuildDoStmt Expr
    e (LamClause
    _ : [LamClause]
    _) = Maybe PositionWithoutFile -> [Char] -> Parser DoStmt
    forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
    parseError' (Range -> Maybe PositionWithoutFile
    forall a. Range' a -> Maybe PositionWithoutFile
    rStart' (Range -> Maybe PositionWithoutFile)
    -> Range -> Maybe PositionWithoutFile
    forall a b. (a -> b) -> a -> b
    $ Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e) [Char]
    "Only pattern matching do-statements can have where clauses."
    defaultBuildDoStmt Expr
    e []      = DoStmt -> Parser DoStmt
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DoStmt -> Parser DoStmt) -> DoStmt -> Parser DoStmt
    forall a b. (a -> b) -> a -> b
    $ Expr -> DoStmt
    DoThen Expr
    e

    buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
    buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
    buildDoStmt (Let Range
    r List1 Declaration
    ds Maybe Expr
    Nothing) [] = DoStmt -> Parser DoStmt
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DoStmt -> Parser DoStmt) -> DoStmt -> Parser DoStmt
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 Declaration -> DoStmt
    DoLet Range
    r List1 Declaration
    ds
    buildDoStmt e :: Expr
    e@(RawApp Range
    r List2 Expr
    _)    [LamClause]
    cs = do
      mpatexpr <- Expr -> Parser (Maybe (Pattern, Range, Expr))
    exprToAssignment Expr
    e
      case mpatexpr of
        Just (Pattern
    pat, Range
    r, Expr
    expr) -> DoStmt -> Parser DoStmt
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DoStmt -> Parser DoStmt) -> DoStmt -> Parser DoStmt
    forall a b. (a -> b) -> a -> b
    $ Range -> Pattern -> Expr -> [LamClause] -> DoStmt
    DoBind Range
    r Pattern
    pat Expr
    expr [LamClause]
    cs
        Maybe (Pattern, Range, Expr)
    Nothing -> Expr -> [LamClause] -> Parser DoStmt
    defaultBuildDoStmt Expr
    e [LamClause]
    cs
    buildDoStmt Expr
    e [LamClause]
    cs = Expr -> [LamClause] -> Parser DoStmt
    defaultBuildDoStmt Expr
    e [LamClause]
    cs

    {--------------------------------------------------------------------------
        Patterns
     --------------------------------------------------------------------------}

    -- | Turn an expression into a left hand side.
    exprToLHS :: Expr -> Parser ([RewriteEqn] -> [WithExpr] -> LHS)
    exprToLHS :: Expr -> Parser ([RewriteEqn] -> [WithExpr] -> LHS)
    exprToLHS Expr
    e = Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
    LHS (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS)
    -> Parser Pattern -> Parser ([RewriteEqn] -> [WithExpr] -> LHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Parser Pattern
    exprToPattern Expr
    e

    -- | Turn an expression into a pattern. Fails if the expression is not a
    --   valid pattern.
    exprToPattern :: Expr -> Parser Pattern
    exprToPattern :: Expr -> Parser Pattern
    exprToPattern Expr
    e = case Expr -> Maybe Pattern
    C.isPattern Expr
    e of
      Maybe Pattern
    Nothing -> Expr -> [Char] -> Parser Pattern
    forall r a. HasRange r => r -> [Char] -> Parser a
    parseErrorRange Expr
    e ([Char] -> Parser Pattern) -> [Char] -> Parser Pattern
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Not a valid pattern: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    e
      Just Pattern
    p  -> Pattern -> Parser Pattern
    forall a. a -> Parser a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pattern
    p

    -- | Turn an expression into a name. Fails if the expression is not a
    --   valid identifier.
    exprToName :: Expr -> Parser Name
    exprToName :: Expr -> Parser Name
    exprToName (Ident (QName Name
    x)) = Name -> Parser Name
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    x
    exprToName Expr
    e = Expr -> [Char] -> Parser Name
    forall r a. HasRange r => r -> [Char] -> Parser a
    parseErrorRange Expr
    e ([Char] -> Parser Name) -> [Char] -> Parser Name
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Not a valid identifier: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    e

    -- | When given expression is @e1 = e2@, turn it into a named expression.
    --   Call this inside an implicit argument @{e}@ or @{{e}}@, where
    --   an equality must be a named argument (rather than a cubical partial match).
    maybeNamed :: Expr -> Parser (Named_ Expr)
    maybeNamed :: Expr -> Parser (Named NamedName Expr)
    maybeNamed Expr
    e =
      case Expr
    e of
        Equal Range
    _ Expr
    e1 Expr
    e2 -> do
          let succeed :: [Char] -> Parser (Named NamedName Expr)
    succeed [Char]
    x = Named NamedName Expr -> Parser (Named NamedName Expr)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Named NamedName Expr -> Parser (Named NamedName Expr))
    -> Named NamedName Expr -> Parser (Named NamedName Expr)
    forall a b. (a -> b) -> a -> b
    $ NamedName -> Expr -> Named NamedName Expr
    forall name a. name -> a -> Named name a
    named (Origin -> RString -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    UserWritten (RString -> NamedName) -> RString -> NamedName
    forall a b. (a -> b) -> a -> b
    $ Range -> [Char] -> RString
    forall a. Range -> a -> Ranged a
    Ranged (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e1) [Char]
    x) Expr
    e2
          case Expr
    e1 of
            Ident (QName Name
    x) -> [Char] -> Parser (Named NamedName Expr)
    succeed ([Char] -> Parser (Named NamedName Expr))
    -> [Char] -> Parser (Named NamedName Expr)
    forall a b. (a -> b) -> a -> b
    $ Name -> [Char]
    nameToRawName Name
    x
            -- We could have the following, but names of arguments cannot be _.
            -- Underscore{}    -> succeed $ "_"
            Expr
    _ -> Expr -> [Char] -> Parser (Named NamedName Expr)
    forall r a. HasRange r => r -> [Char] -> Parser a
    parseErrorRange Expr
    e ([Char] -> Parser (Named NamedName Expr))
    -> [Char] -> Parser (Named NamedName Expr)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Not a valid named argument: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    e
        Expr
    _ -> Named NamedName Expr -> Parser (Named NamedName Expr)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Named NamedName Expr -> Parser (Named NamedName Expr))
    -> Named NamedName Expr -> Parser (Named NamedName Expr)
    forall a b. (a -> b) -> a -> b
    $ Expr -> Named NamedName Expr
    forall a name. a -> Named name a
    unnamed Expr
    e

    -- Andreas, 2024-02-20, issue #7136:
    -- The following function has been rewritten to a defensive pattern matching style
    -- to be robust against future parser changes.
    patternSynArgs :: [NamedArg Binder] -> Parser [WithHiding Name]
    patternSynArgs :: [NamedArg Binder] -> Parser [WithHiding Name]
    patternSynArgs = (NamedArg Binder -> Parser (WithHiding Name))
    -> [NamedArg Binder] -> Parser [WithHiding Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM \ NamedArg Binder
    x -> do
      let
        abort :: [Char] -> Parser (WithHiding Name)
    abort [Char]
    s = [Char] -> Parser (WithHiding Name)
    forall a. [Char] -> Parser a
    parseError ([Char] -> Parser (WithHiding Name))
    -> [Char] -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Illegal pattern synonym argument  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ NamedArg Binder -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow NamedArg Binder
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char]
    "(" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ".)"
        noAnn :: [Char] -> [Char]
    noAnn [Char]
    s = [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " annotations not allowed in pattern synonym arguments"

      case NamedArg Binder
    x of

        -- Invariant: fixity is not used here, and neither finiteness
        Arg ArgInfo
    ai (Named Maybe NamedName
    mn (Binder Maybe Pattern
    mp BinderNameOrigin
    _ (BName Name
    n Fixity'
    fix TacticAttribute
    mtac Bool
    fin)))
          | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Fixity' -> Bool
    forall a. Null a => a -> Bool
    null Fixity'
    fix -> Parser (WithHiding Name)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          | Bool
    fin            -> Parser (WithHiding Name)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Error cases:
        Arg ArgInfo
    _ (Named Maybe NamedName
    _ (Binder (Just Pattern
    _) BinderNameOrigin
    _ BoundName
    _)) ->
          [Char] -> Parser (WithHiding Name)
    abort [Char]
    "Arguments to pattern synonyms cannot be patterns themselves"
        Arg ArgInfo
    _ (Named Maybe NamedName
    _ (Binder Maybe Pattern
    _ BinderNameOrigin
    _ (BName Name
    _ Fixity'
    _ TacticAttribute
    tac Bool
    _))) | Bool -> Bool
    not (TacticAttribute -> Bool
    forall a. Null a => a -> Bool
    null TacticAttribute
    tac) ->
          [Char] -> Parser (WithHiding Name)
    abort ([Char] -> Parser (WithHiding Name))
    -> [Char] -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    noAnn [Char]
    "Tactic"

        -- Benign case:
        Arg ArgInfo
    ai (Named Maybe NamedName
    mn (Binder Maybe Pattern
    Nothing BinderNameOrigin
    _ (BName Name
    n Fixity'
    _ TacticAttribute
    _ Bool
    _)))
          -- allow {n = n} for backwards compat with Agda 2.6
          | Bool -> (NamedName -> Bool) -> Maybe NamedName -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True ((Name -> [Char]
    C.nameToRawName Name
    n [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) ([Char] -> Bool) -> (NamedName -> [Char]) -> NamedName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RString -> [Char]
    forall a. Ranged a -> a
    rangedThing (RString -> [Char])
    -> (NamedName -> RString) -> NamedName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedName -> RString
    forall a. WithOrigin a -> a
    woThing) Maybe NamedName
    mn ->
            case ArgInfo
    ai of

              -- Benign case:
              ArgInfo Hiding
    h (Modality Relevant{} (Quantityω QωOrigin
    _) Cohesion
    Continuous (PolarityModality { modPolarityAnn :: PolarityModality -> ModalPolarity
    modPolarityAnn = ModalPolarity
    MixedPolarity })) Origin
    UserWritten FreeVariables
    UnknownFVs (Annotation Lock
    IsNotLock) ->
                WithHiding Name -> Parser (WithHiding Name)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (WithHiding Name -> Parser (WithHiding Name))
    -> WithHiding Name -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $ Hiding -> Name -> WithHiding Name
    forall a. Hiding -> a -> WithHiding a
    WithHiding Hiding
    h Name
    n

              -- Error cases:
              ArgInfo Hiding
    _ Modality
    _ Origin
    _ FreeVariables
    _ (Annotation (IsLock LockOrigin
    _)) ->
                [Char] -> Parser (WithHiding Name)
    abort ([Char] -> Parser (WithHiding Name))
    -> [Char] -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    noAnn [Char]
    "Lock"

              ArgInfo Hiding
    h (Modality Relevance
    r Quantity
    q Cohesion
    c PolarityModality
    p) Origin
    _ FreeVariables
    _ Annotation
    _
                | Bool -> Bool
    not (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isRelevant Relevance
    r) ->
                    [Char] -> Parser (WithHiding Name)
    abort [Char]
    "Arguments to pattern synonyms must be relevant"
                | Bool -> Bool
    not (Quantity -> Bool
    forall a. LensQuantity a => a -> Bool
    isQuantityω Quantity
    q) ->
                    [Char] -> Parser (WithHiding Name)
    abort ([Char] -> Parser (WithHiding Name))
    -> [Char] -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    noAnn [Char]
    "Quantity"
                | PolarityModality -> ModalPolarity
    modPolarityAnn PolarityModality
    p ModalPolarity -> ModalPolarity -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ModalPolarity
    MixedPolarity ->
                    [Char] -> Parser (WithHiding Name)
    abort ([Char] -> Parser (WithHiding Name))
    -> [Char] -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    noAnn [Char]
    "Polarity"
                | Cohesion
    c Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Cohesion
    Continuous ->
                    [Char] -> Parser (WithHiding Name)
    abort ([Char] -> Parser (WithHiding Name))
    -> [Char] -> Parser (WithHiding Name)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    noAnn [Char]
    "Cohesion"

              -- Invariant: origin and fvs not used.
              ArgInfo Hiding
    _ Modality
    _ Origin
    _ (KnownFVs IntSet
    _) Annotation
    _ -> Parser (WithHiding Name)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              ArgInfo Hiding
    _ Modality
    _ Origin
    o FreeVariables
    _ Annotation
    _ | Origin
    o Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Origin
    UserWritten -> Parser (WithHiding Name)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              ArgInfo Hiding
    _ Modality
    _ Origin
    _ FreeVariables
    _ Annotation
    _ -> Parser (WithHiding Name)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          -- Error case: other named args are unsupported (issue #7136)
          | Bool
    otherwise ->
              [Char] -> Parser (WithHiding Name)
    abort [Char]
    "Arguments to pattern synonyms cannot be named"

    mkLamClause
      :: Catchall
      -> [Expr] -- ^ Possibly empty list of patterns.
      -> RHS
      -> Parser LamClause
    mkLamClause :: Catchall -> [Expr] -> RHS -> Parser LamClause
    mkLamClause Catchall
    catchall [Expr]
    es RHS
    rhs = (Expr -> Parser Pattern) -> [Expr] -> Parser [Pattern]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Expr -> Parser Pattern
    exprToPattern [Expr]
    es Parser [Pattern] -> ([Pattern] -> LamClause) -> Parser LamClause
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ [Pattern]
    ps ->
      LamClause{ lamLHS :: [Pattern]
    lamLHS = [Pattern]
    ps, lamRHS :: RHS
    lamRHS = RHS
    rhs, lamCatchall :: Catchall
    lamCatchall = Catchall
    catchall }

    mkAbsurdLamClause :: Catchall -> List1 Expr -> Parser LamClause
    mkAbsurdLamClause :: Catchall -> List1 Expr -> Parser LamClause
    mkAbsurdLamClause Catchall
    catchall List1 Expr
    es = Catchall -> [Expr] -> RHS -> Parser LamClause
    mkLamClause Catchall
    catchall (List1 Expr -> [Item (List1 Expr)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 Expr
    es) RHS
    forall e. RHS' e
    AbsurdRHS

    {- RHS or type signature -}

    data RHSOrTypeSigs
     = JustRHS RHS
     | TypeSigsRHS Expr
     deriving Int -> RHSOrTypeSigs -> [Char] -> [Char]
    [RHSOrTypeSigs] -> [Char] -> [Char]
    RHSOrTypeSigs -> [Char]
    (Int -> RHSOrTypeSigs -> [Char] -> [Char])
    -> (RHSOrTypeSigs -> [Char])
    -> ([RHSOrTypeSigs] -> [Char] -> [Char])
    -> Show RHSOrTypeSigs
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> RHSOrTypeSigs -> [Char] -> [Char]
    showsPrec :: Int -> RHSOrTypeSigs -> [Char] -> [Char]
    $cshow :: RHSOrTypeSigs -> [Char]
    show :: RHSOrTypeSigs -> [Char]
    $cshowList :: [RHSOrTypeSigs] -> [Char] -> [Char]
    showList :: [RHSOrTypeSigs] -> [Char] -> [Char]
    Show

    patternToNames :: Pattern -> Parser (List1 (ArgInfo, Name))
    patternToNames :: Pattern -> Parser (List1 (ArgInfo, Name))
    patternToNames = \case
        IdentP Bool
    _ (QName Name
    i)           -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name)))
    -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo, Name) -> List1 (ArgInfo, Name)
    forall el coll. Singleton el coll => el -> coll
    singleton (ArgInfo
    defaultArgInfo, Name
    i)
        WildP Range
    r                      -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name)))
    -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo, Name) -> List1 (ArgInfo, Name)
    forall el coll. Singleton el coll => el -> coll
    singleton (ArgInfo
    defaultArgInfo, Range -> Name
    C.noName Range
    r)
        DotP KwRange
    kwr Range
    _ (Ident (QName Name
    i)) -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name)))
    -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo, Name) -> List1 (ArgInfo, Name)
    forall el coll. Singleton el coll => el -> coll
    singleton (KwRange -> ArgInfo -> ArgInfo
    forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeIrrelevant KwRange
    kwr ArgInfo
    defaultArgInfo, Name
    i)
        RawAppP Range
    _ List2 Pattern
    ps                 -> NonEmpty (List1 (ArgInfo, Name)) -> List1 (ArgInfo, Name)
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (NonEmpty (List1 (ArgInfo, Name)) -> List1 (ArgInfo, Name))
    -> (List2 (List1 (ArgInfo, Name))
        -> NonEmpty (List1 (ArgInfo, Name)))
    -> List2 (List1 (ArgInfo, Name))
    -> List1 (ArgInfo, Name)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List2 (List1 (ArgInfo, Name)) -> NonEmpty (List1 (ArgInfo, Name))
    forall a. List2 a -> List1 a
    List2.toList1 (List2 (List1 (ArgInfo, Name)) -> List1 (ArgInfo, Name))
    -> Parser (List2 (List1 (ArgInfo, Name)))
    -> Parser (List1 (ArgInfo, Name))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> Parser (List1 (ArgInfo, Name)))
    -> List2 Pattern -> Parser (List2 (List1 (ArgInfo, Name)))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> List2 a -> m (List2 b)
    mapM Pattern -> Parser (List1 (ArgInfo, Name))
    patternToNames List2 Pattern
    ps
        Pattern
    p -> [Char] -> Parser (List1 (ArgInfo, Name))
    forall a. [Char] -> Parser a
    parseError ([Char] -> Parser (List1 (ArgInfo, Name)))
    -> [Char] -> Parser (List1 (ArgInfo, Name))
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Illegal name in type signature: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Pattern -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Pattern
    p

    funClauseOrTypeSigs :: [Attr] -> ([RewriteEqn] -> [WithExpr] -> LHS)
                        -> [Either RewriteEqn (List1 (Named Name Expr))]
                        -> RHSOrTypeSigs
                        -> WhereClause -> Parser (List1 Declaration)
    funClauseOrTypeSigs :: [Attr]
    -> ([RewriteEqn] -> [WithExpr] -> LHS)
    -> [Either RewriteEqn (List1 (Named Name Expr))]
    -> RHSOrTypeSigs
    -> WhereClause
    -> Parser (List1 Declaration)
    funClauseOrTypeSigs [Attr]
    attrs [RewriteEqn] -> [WithExpr] -> LHS
    lhs' [Either RewriteEqn (List1 (Named Name Expr))]
    with RHSOrTypeSigs
    mrhs WhereClause
    wh = do
      (rs , es) <- [Either RewriteEqn (List1 (Named Name Expr))]
    -> Parser ([RewriteEqn], [Named Name Expr])
    buildWithBlock [Either RewriteEqn (List1 (Named Name Expr))]
    with
      let lhs = [RewriteEqn] -> [WithExpr] -> LHS
    lhs' [RewriteEqn]
    rs ((Named Name Expr -> WithExpr) -> [Named Name Expr] -> [WithExpr]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Expr -> Arg Expr) -> Named Name Expr -> WithExpr
    forall a b. (a -> b) -> Named Name a -> Named Name b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> Arg Expr
    observeModifiers) [Named Name Expr]
    es)
      -- traceShowM lhs
      case mrhs of
        JustRHS RHS
    rhs   -> do
          Bool -> Parser () -> Parser ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Attr] -> Bool
    forall a. Null a => a -> Bool
    null [Attr]
    attrs) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ ParseWarning -> Parser ()
    parseWarning (ParseWarning -> Parser ()) -> ParseWarning -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ Range -> [Char] -> ParseWarning
    MisplacedAttributes ([Attr] -> Range
    forall a. HasRange a => a -> Range
    getRange [Attr]
    attrs) [Char]
    "A function clause cannot have attributes"
          List1 Declaration -> Parser (List1 Declaration)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (List1 Declaration -> Parser (List1 Declaration))
    -> List1 Declaration -> Parser (List1 Declaration)
    forall a b. (a -> b) -> a -> b
    $ Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ LHS -> RHS -> WhereClause -> Catchall -> Declaration
    FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    forall a. Null a => a
    empty
        TypeSigsRHS Expr
    e -> case WhereClause
    wh of
          WhereClause
    NoWhere -> case LHS
    lhs of
            LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    _ | Pattern -> Bool
    forall a. HasEllipsis a => a -> Bool
    hasEllipsis Pattern
    p -> [Char] -> Parser (List1 Declaration)
    forall a. [Char] -> Parser a
    parseError [Char]
    "The ellipsis ... cannot have a type signature"
            LHS Pattern
    _ [RewriteEqn]
    _ (WithExpr
    _:[WithExpr]
    _) -> [Char] -> Parser (List1 Declaration)
    forall a. [Char] -> Parser a
    parseError [Char]
    "Illegal: with in type signature"
            LHS Pattern
    _ (RewriteEqn
    _:[RewriteEqn]
    _) [WithExpr]
    _ -> [Char] -> Parser (List1 Declaration)
    forall a. [Char] -> Parser a
    parseError [Char]
    "Illegal: rewrite in type signature"
            LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    _ | Pattern -> Bool
    forall p. CPatternLike p => p -> Bool
    hasWithPatterns Pattern
    p -> [Char] -> Parser (List1 Declaration)
    forall a. [Char] -> Parser a
    parseError [Char]
    "Illegal: with patterns in type signature"
            LHS Pattern
    p [] [] -> Parser (List1 (ArgInfo, Name))
    -> ((ArgInfo, Name) -> Parser Declaration)
    -> Parser (List1 Declaration)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    m (t a) -> (a -> m b) -> m (t b)
    forMM (Pattern -> Parser (List1 (ArgInfo, Name))
    patternToNames Pattern
    p) (((ArgInfo, Name) -> Parser Declaration)
     -> Parser (List1 Declaration))
    -> ((ArgInfo, Name) -> Parser Declaration)
    -> Parser (List1 Declaration)
    forall a b. (a -> b) -> a -> b
    $ \ (ArgInfo
    info, Name
    x) -> do
              info <- [Attr] -> ArgInfo -> Parser ArgInfo
    forall a. LensAttribute a => [Attr] -> a -> Parser a
    applyAttrs [Attr]
    attrs ArgInfo
    info
              return $ typeSig info (getTacticAttr attrs) x e
          WhereClause
    _ -> [Char] -> Parser (List1 Declaration)
    forall a. [Char] -> Parser a
    parseError [Char]
    "A type signature cannot have a where clause"

    typeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    typeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    typeSig ArgInfo
    i TacticAttribute
    tac Name
    n Expr
    e = ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    i TacticAttribute
    tac Name
    n (Expr -> Expr
    Generalized Expr
    e)

    ------------------------------------------------------------------------
    -- * Relevance

    makeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b
    makeIrrelevant :: forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeIrrelevant = Relevance -> b -> b
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance (Relevance -> b -> b) -> (a -> Relevance) -> a -> b -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OriginIrrelevant -> Relevance
    Irrelevant (OriginIrrelevant -> Relevance)
    -> (a -> OriginIrrelevant) -> a -> Relevance
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> OriginIrrelevant
    OIrrDot (Range -> OriginIrrelevant)
    -> (a -> Range) -> a -> OriginIrrelevant
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Range
    forall a. HasRange a => a -> Range
    getRange

    makeShapeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b
    makeShapeIrrelevant :: forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeShapeIrrelevant = Relevance -> b -> b
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance (Relevance -> b -> b) -> (a -> Relevance) -> a -> b -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OriginShapeIrrelevant -> Relevance
    ShapeIrrelevant (OriginShapeIrrelevant -> Relevance)
    -> (a -> OriginShapeIrrelevant) -> a -> Relevance
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> OriginShapeIrrelevant
    OShIrrDotDot (Range -> OriginShapeIrrelevant)
    -> (a -> Range) -> a -> OriginShapeIrrelevant
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Range
    forall a. HasRange a => a -> Range
    getRange

    defaultIrrelevantArg :: HasRange a => a -> b -> Arg b
    defaultIrrelevantArg :: forall a b. HasRange a => a -> b -> Arg b
    defaultIrrelevantArg a
    a = a -> Arg b -> Arg b
    forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeIrrelevant a
    a (Arg b -> Arg b) -> (b -> Arg b) -> b -> Arg b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> Arg b
    forall a. a -> Arg a
    defaultArg

    defaultShapeIrrelevantArg :: HasRange a => a -> b -> Arg b
    defaultShapeIrrelevantArg :: forall a b. HasRange a => a -> b -> Arg b
    defaultShapeIrrelevantArg a
    a = a -> Arg b -> Arg b
    forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeShapeIrrelevant a
    a (Arg b -> Arg b) -> (b -> Arg b) -> b -> Arg b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> Arg b
    forall a. a -> Arg a
    defaultArg

    makeIrrelevantM :: (HasRange a, LensRelevance b) => a -> b -> Parser b
    makeIrrelevantM :: forall a b. (HasRange a, LensRelevance b) => a -> b -> Parser b
    makeIrrelevantM a
    r b
    x = do
      a -> b -> Parser ()
    forall a b. (HasRange a, LensRelevance b) => a -> b -> Parser ()
    assertPristineRelevance a
    r b
    x
      b -> Parser b
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b -> Parser b) -> b -> Parser b
    forall a b. (a -> b) -> a -> b
    $ a -> b -> b
    forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeIrrelevant a
    r b
    x

    makeShapeIrrelevantM :: (HasRange a, LensRelevance b) => a -> b -> Parser b
    makeShapeIrrelevantM :: forall a b. (HasRange a, LensRelevance b) => a -> b -> Parser b
    makeShapeIrrelevantM a
    r b
    x = do
      a -> b -> Parser ()
    forall a b. (HasRange a, LensRelevance b) => a -> b -> Parser ()
    assertPristineRelevance a
    r b
    x
      b -> Parser b
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (b -> Parser b) -> b -> Parser b
    forall a b. (a -> b) -> a -> b
    $ a -> b -> b
    forall a b. (HasRange a, LensRelevance b) => a -> b -> b
    makeShapeIrrelevant a
    r b
    x

    assertPristineRelevance :: (HasRange a, LensRelevance b) => a -> b -> Parser ()
    assertPristineRelevance :: forall a b. (HasRange a, LensRelevance b) => a -> b -> Parser ()
    assertPristineRelevance a
    r b
    x = Bool -> Parser () -> Parser ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Relevance -> Bool
    forall a. Null a => a -> Bool
    null (Relevance -> Bool) -> Relevance -> Bool
    forall a b. (a -> b) -> a -> b
    $ b -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance b
    x) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $
      a -> [Char] -> Parser ()
    forall r a. HasRange r => r -> [Char] -> Parser a
    parseErrorRange a
    r ([Char] -> Parser ()) -> [Char] -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Conflicting relevance information"

    ------------------------------------------------------------------------
    -- * Attributes

    -- | Parse an attribute.
    toAttribute :: Range -> Expr -> Parser (Maybe Attr)
    toAttribute :: Range -> Expr -> Parser (Maybe Attr)
    toAttribute Range
    r Expr
    e = do
      case Range -> Expr -> Maybe Attribute
    exprToAttribute Range
    r Expr
    e of
        Maybe Attribute
    Nothing -> Maybe Attr
    forall a. Maybe a
    Nothing Maybe Attr -> Parser () -> Parser (Maybe Attr)
    forall a b. a -> Parser b -> Parser a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ ParseWarning -> Parser ()
    parseWarning (Range -> [Char] -> ParseWarning
    UnknownAttribute Range
    r [Char]
    s)
        Just Attribute
    a -> do
          let attr :: Attr
    attr = Range -> [Char] -> Attribute -> Attr
    Attr Range
    r [Char]
    s Attribute
    a
          (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify' \ ParseState
    st -> ParseState
    st{ parseAttributes = attr : parseAttributes st }
          Maybe Attr -> Parser (Maybe Attr)
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Attr -> Parser (Maybe Attr))
    -> Maybe Attr -> Parser (Maybe Attr)
    forall a b. (a -> b) -> a -> b
    $ Attr -> Maybe Attr
    forall a. a -> Maybe a
    Just Attr
    attr
      where
        s :: [Char]
    s = Expr -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Expr
    e

    -- | Apply an attribute to thing (usually `Arg`).
    --   This will fail if one of the attributes is already set
    --   in the thing to something else than the default value.
    applyAttr :: (LensAttribute a) => Attr -> a -> Parser a
    applyAttr :: forall a. LensAttribute a => Attr -> a -> Parser a
    applyAttr attr :: Attr
    attr@(Attr Range
    _ [Char]
    _ Attribute
    a) = Parser a -> (a -> Parser a) -> Maybe a -> Parser a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Parser a
    failure a -> Parser a
    forall a. a -> Parser a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> Parser a) -> (a -> Maybe a) -> a -> Parser a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> a -> Maybe a
    forall a. LensAttribute a => Attribute -> a -> Maybe a
    setPristineAttribute Attribute
    a
      where
      failure :: Parser a
    failure = Attr -> Parser a
    forall a. Attr -> Parser a
    errorConflictingAttribute Attr
    attr

    -- | Apply attributes to thing (usually `Arg`).
    --   Expects a reversed list of attributes.
    --   This will fail if one of the attributes is already set
    --   in the thing to something else than the default value.
    applyAttrs :: LensAttribute a => [Attr] -> a -> Parser a
    applyAttrs :: forall a. LensAttribute a => [Attr] -> a -> Parser a
    applyAttrs [Attr]
    rattrs a
    arg = do
      let attrs :: [Attr]
    attrs = [Attr] -> [Attr]
    forall a. [a] -> [a]
    reverse [Attr]
    rattrs
      (Attribute -> Bool) -> [Attr] -> Parser ()
    checkForUniqueAttribute (Maybe Quantity -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Quantity -> Bool)
    -> (Attribute -> Maybe Quantity) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> Maybe Quantity
    isQuantityAttribute ) [Attr]
    attrs
      (Attribute -> Bool) -> [Attr] -> Parser ()
    checkForUniqueAttribute (Maybe Relevance -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Relevance -> Bool)
    -> (Attribute -> Maybe Relevance) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> Maybe Relevance
    isRelevanceAttribute) [Attr]
    attrs
      (Attribute -> Bool) -> [Attr] -> Parser ()
    checkForUniqueAttribute (Bool -> Bool
    not (Bool -> Bool) -> (Attribute -> Bool) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TacticAttribute -> Bool
    forall a. Null a => a -> Bool
    null (TacticAttribute -> Bool)
    -> (Attribute -> TacticAttribute) -> Attribute -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attribute -> TacticAttribute
    isTacticAttribute) [Attr]
    attrs
      (a -> Attr -> Parser a) -> a -> [Attr] -> Parser a
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ((Attr -> a -> Parser a) -> a -> Attr -> Parser a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Attr -> a -> Parser a
    forall a. LensAttribute a => Attr -> a -> Parser a
    applyAttr) a
    arg [Attr]
    attrs

    applyAttrs1 :: LensAttribute a => List1 Attr -> a -> Parser a
    applyAttrs1 :: forall a. LensAttribute a => List1 Attr -> a -> Parser a
    applyAttrs1 = [Attr] -> a -> Parser a
    forall a. LensAttribute a => [Attr] -> a -> Parser a
    applyAttrs ([Attr] -> a -> Parser a)
    -> (List1 Attr -> [Attr]) -> List1 Attr -> a -> Parser a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Attr -> [Item (List1 Attr)]
    List1 Attr -> [Attr]
    forall l. IsList l => l -> [Item l]
    List1.toList

    -- | Set the tactic attribute of a binder
    setTacticAttr :: [Attr] -> NamedArg Binder -> NamedArg Binder
    setTacticAttr :: [Attr] -> NamedArg Binder -> NamedArg Binder
    setTacticAttr [] = NamedArg Binder -> NamedArg Binder
    forall a. a -> a
    id
    setTacticAttr [Attr]
    as = (Binder -> Binder) -> NamedArg Binder -> NamedArg Binder
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg ((Binder -> Binder) -> NamedArg Binder -> NamedArg Binder)
    -> (Binder -> Binder) -> NamedArg Binder -> NamedArg Binder
    forall a b. (a -> b) -> a -> b
    $ (BoundName -> BoundName) -> Binder -> Binder
    forall a b. (a -> b) -> Binder' a -> Binder' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((BoundName -> BoundName) -> Binder -> Binder)
    -> (BoundName -> BoundName) -> Binder -> Binder
    forall a b. (a -> b) -> a -> b
    $ \ BoundName
    b ->
      case [Attr] -> TacticAttribute
    getTacticAttr [Attr]
    as of
        TacticAttribute
    t | TacticAttribute -> Bool
    forall a. Null a => a -> Bool
    null TacticAttribute
    t    -> BoundName
    b
          | Bool
    otherwise -> BoundName
    b { bnameTactic = t }

    -- | Get the tactic attribute if present.
    getTacticAttr :: [Attr] -> TacticAttribute
    getTacticAttr :: [Attr] -> TacticAttribute
    getTacticAttr [Attr]
    as = Maybe (Ranged Expr) -> TacticAttribute
    forall a. Maybe (Ranged a) -> TacticAttribute' a
    C.TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute)
    -> Maybe (Ranged Expr) -> TacticAttribute
    forall a b. (a -> b) -> a -> b
    $
      case [Attribute] -> [Attribute]
    tacticAttributes [ Attribute
    a | Attr Range
    _ [Char]
    _ Attribute
    a <- [Attr]
    as ] of
        [CA.TacticAttribute Ranged Expr
    e] -> Ranged Expr -> Maybe (Ranged Expr)
    forall a. a -> Maybe a
    Just Ranged Expr
    e
        [] -> Maybe (Ranged Expr)
    forall a. Maybe a
    Nothing
        [Attribute]
    _  -> Maybe (Ranged Expr)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Report a parse error if two attributes in the list are of the same kind,
    --   thus, present conflicting information.
    checkForUniqueAttribute :: (Attribute -> Bool) -> [Attr] -> Parser ()
    checkForUniqueAttribute :: (Attribute -> Bool) -> [Attr] -> Parser ()
    checkForUniqueAttribute Attribute -> Bool
    p [Attr]
    attrs = do
      let pAttrs :: [Attr]
    pAttrs = (Attr -> Bool) -> [Attr] -> [Attr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Attribute -> Bool
    p (Attribute -> Bool) -> (Attr -> Attribute) -> Attr -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attr -> Attribute
    theAttr) [Attr]
    attrs
      Bool -> Parser () -> Parser ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([Attr] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Attr]
    pAttrs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    2) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $
        [Attr] -> Parser ()
    forall a. [Attr] -> Parser a
    errorConflictingAttributes [Attr]
    pAttrs

    -- | Report an attribute as conflicting (e.g., with an already set value).
    errorConflictingAttribute :: Attr -> Parser a
    errorConflictingAttribute :: forall a. Attr -> Parser a
    errorConflictingAttribute Attr
    a = Attr -> [Char] -> Parser a
    forall r a. HasRange r => r -> [Char] -> Parser a
    parseErrorRange Attr
    a ([Char] -> Parser a) -> [Char] -> Parser a
    forall a b. (a -> b) -> a -> b
    $
      [Char]
    "Conflicting attribute: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Attr -> [Char]
    prettyAttr Attr
    a

    -- | Report attributes as conflicting (e.g., with each other).
    --   Precondition: List not emtpy.
    errorConflictingAttributes :: [Attr] -> Parser a
    errorConflictingAttributes :: forall a. [Attr] -> Parser a
    errorConflictingAttributes [Attr
    a] = Attr -> Parser a
    forall a. Attr -> Parser a
    errorConflictingAttribute Attr
    a
    errorConflictingAttributes [Attr]
    as  = [Attr] -> [Char] -> Parser a
    forall r a. HasRange r => r -> [Char] -> Parser a
    parseErrorRange [Attr]
    as ([Char] -> Parser a) -> [Char] -> Parser a
    forall a b. (a -> b) -> a -> b
    $
      [Char]
    "Conflicting attributes: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    unwords ((Attr -> [Char]) -> [Attr] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Attr -> [Char]
    prettyAttr [Attr]
    as)

    prettyAttr :: Attr -> String
    prettyAttr :: Attr -> [Char]
    prettyAttr = ([Char]
    "@" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) ([Char] -> [Char]) -> (Attr -> [Char]) -> Attr -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Attr -> [Char]
    attrName

    -- | Apply some attributes to some binders.
    applyAttributes :: Functor f
      => [Attr]
           -- ^ Can contain @tactic@ attribute.
      -> ArgInfo
           -- ^ If the attributes to be set are not at default value here, crash.
      -> f (NamedArg Binder)
           -- ^ Binders to apply attributes to.
      -> Parser (f (NamedArg Binder))
           -- ^ Binders with attributes applied.
    applyAttributes :: forall (f :: * -> *).
    Functor f =>
    [Attr]
    -> ArgInfo -> f (NamedArg Binder) -> Parser (f (NamedArg Binder))
    applyAttributes [Attr]
    attrs ArgInfo
    ai f (NamedArg Binder)
    bs = do
      [Attr] -> ArgInfo -> Parser ArgInfo
    forall a. LensAttribute a => [Attr] -> a -> Parser a
    applyAttrs [Attr]
    attrs ArgInfo
    ai Parser ArgInfo
    -> (ArgInfo -> f (NamedArg Binder)) -> Parser (f (NamedArg Binder))
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ ArgInfo
    ai' ->
        (NamedArg Binder -> NamedArg Binder)
    -> f (NamedArg Binder) -> f (NamedArg Binder)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Attr] -> NamedArg Binder -> NamedArg Binder
    setTacticAttr [Attr]
    attrs (NamedArg Binder -> NamedArg Binder)
    -> (NamedArg Binder -> NamedArg Binder)
    -> NamedArg Binder
    -> NamedArg Binder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> NamedArg Binder -> NamedArg Binder
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    ai') f (NamedArg Binder)
    bs