{
{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}

{-| The parser is generated by Happy (<http://www.haskell.org/happy>).
 -
 - Ideally, ranges should be as precise as possible, to get messages that
 - emphasize precisely the faulting term(s) upon error.
 -
 - However, interactive highlighting is only applied at the end of each
 - mutual block, keywords are only highlighted once (see
 - `TypeChecking.Rules.Decl'). So if the ranges of two declarations
 - interleave, one must ensure that keyword ranges are not included in
 - the intersection. (Otherwise they are uncolored by the interactive
 - highlighting.)
 -
 -}
module Agda.Syntax.Parser.Parser (
      moduleParser
    , moduleNameParser
    , exprParser
    , exprWhereParser
    , tokensParser
    , holeContentParser
    , splitOnDots  -- only used by the internal test-suite
    ) where

import Control.Monad

import Data.Char
import Data.Functor
import Data.List
import Data.Maybe
import Data.Monoid
import qualified Data.Traversable as T

import Debug.Trace

import Agda.Syntax.Position hiding (tests)
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
import Agda.Syntax.Concrete.Pattern
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Literal

import Agda.TypeChecking.Positivity.Occurrence hiding (tests)

import Agda.Utils.Either hiding (tests)
import Agda.Utils.Functor
import Agda.Utils.Hash
import Agda.Utils.List ( spanJust, chopWhen )
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Tuple
import qualified Agda.Utils.Maybe.Strict as Strict

import Agda.Utils.Impossible
#include "undefined.h"

}

%name tokensParser Tokens
%name exprParser Expr
%name exprWhereParser ExprWhere
%name moduleParser File
%name moduleNameParser ModuleName
%name funclauseParser FunClause
%name holeContentParser HoleContent

%tokentype { Token }
%monad { Parser }
%lexer { lexer } { TokEOF{} }

%expect 9
-- * shift/reduce for \ x y z -> foo = bar
--   shifting means it'll parse as \ x y z -> (foo = bar) rather than
--   (\ x y z -> foo) = bar
--
-- * Telescope let and do-notation let.
--      Expr2 -> 'let' Declarations . LetBody
--      TypedBinding -> '(' 'let' Declarations . ')'
--        ')'   shift, and enter state 486
--              (reduce using rule 189)
--   A do-block cannot end in a 'let' so committing to TypedBinding with a
--   shift is the right thing to do here.
--
-- * Named implicits in TypedBinding {x = y}. When encountering the '=' shift
--   treats this as a named implicit and reducing would fail later.

-- This is a trick to get rid of shift/reduce conflicts arising because we want
-- to parse things like "m >>= \x -> k x". See the Expr rule for more
-- information.
%nonassoc LOWEST
%nonassoc '->'

%token
    'abstract'                { TokKeyword KwAbstract $$ }
    'codata'                  { TokKeyword KwCoData $$ }
    'coinductive'             { TokKeyword KwCoInductive $$ }
    'constructor'             { TokKeyword KwConstructor $$ }
    'data'                    { TokKeyword KwData $$ }
    'eta-equality'            { TokKeyword KwEta $$ }
    'field'                   { TokKeyword KwField $$ }
    'forall'                  { TokKeyword KwForall $$ }
    'variable'                { TokKeyword KwVariable $$ }
    'hiding'                  { TokKeyword KwHiding $$ }
    'import'                  { TokKeyword KwImport $$ }
    'in'                      { TokKeyword KwIn $$ }
    'inductive'               { TokKeyword KwInductive $$ }
    'infix'                   { TokKeyword KwInfix $$ }
    'infixl'                  { TokKeyword KwInfixL $$ }
    'infixr'                  { TokKeyword KwInfixR $$ }
    'instance'                { TokKeyword KwInstance $$ }
    'overlap'                 { TokKeyword KwOverlap $$ }
    'let'                     { TokKeyword KwLet $$ }
    'macro'                   { TokKeyword KwMacro $$ }
    'module'                  { TokKeyword KwModule $$ }
    'mutual'                  { TokKeyword KwMutual $$ }
    'no-eta-equality'         { TokKeyword KwNoEta $$ }
    'open'                    { TokKeyword KwOpen $$ }
    'pattern'                 { TokKeyword KwPatternSyn $$ }
    'postulate'               { TokKeyword KwPostulate $$ }
    'primitive'               { TokKeyword KwPrimitive $$ }
    'private'                 { TokKeyword KwPrivate $$ }
    'Prop'                    { TokKeyword KwProp $$ }
    'public'                  { TokKeyword KwPublic $$ }
    'quote'                   { TokKeyword KwQuote $$ }
    'quoteContext'            { TokKeyword KwQuoteContext $$ }
    'quoteGoal'               { TokKeyword KwQuoteGoal $$ }
    'quoteTerm'               { TokKeyword KwQuoteTerm $$ }
    'record'                  { TokKeyword KwRecord $$ }
    'renaming'                { TokKeyword KwRenaming $$ }
    'rewrite'                 { TokKeyword KwRewrite $$ }
    'Set'                     { TokKeyword KwSet $$ }
    'syntax'                  { TokKeyword KwSyntax $$ }
    'tactic'                  { TokKeyword KwTactic $$ }
    'to'                      { TokKeyword KwTo $$ }
    'unquote'                 { TokKeyword KwUnquote $$ }
    'unquoteDecl'             { TokKeyword KwUnquoteDecl $$ }
    'unquoteDef'              { TokKeyword KwUnquoteDef $$ }
    'using'                   { TokKeyword KwUsing $$ }
    'where'                   { TokKeyword KwWhere $$ }
    'do'                      { TokKeyword KwDo $$ }
    'with'                    { TokKeyword KwWith $$ }

    'BUILTIN'                 { TokKeyword KwBUILTIN $$ }
    'CATCHALL'                { TokKeyword KwCATCHALL $$ }
    'DISPLAY'                 { TokKeyword KwDISPLAY $$ }
    'ETA'                     { TokKeyword KwETA $$ }
    'FOREIGN'                 { TokKeyword KwFOREIGN $$ }
    'COMPILE'                 { TokKeyword KwCOMPILE $$ }
    'IMPOSSIBLE'              { TokKeyword KwIMPOSSIBLE $$ }
    'INJECTIVE'               { TokKeyword KwINJECTIVE $$ }
    'INLINE'                  { TokKeyword KwINLINE $$ }
    'NOINLINE'                { TokKeyword KwNOINLINE $$ }
    'MEASURE'                 { TokKeyword KwMEASURE $$ }
    'NO_TERMINATION_CHECK'    { TokKeyword KwNO_TERMINATION_CHECK $$ }
    'NO_POSITIVITY_CHECK'     { TokKeyword KwNO_POSITIVITY_CHECK $$ }
    'NO_UNIVERSE_CHECK'       { TokKeyword KwNO_UNIVERSE_CHECK $$ }
    'NON_TERMINATING'         { TokKeyword KwNON_TERMINATING $$ }
    'OPTIONS'                 { TokKeyword KwOPTIONS $$ }
    'POLARITY'                { TokKeyword KwPOLARITY $$ }
    'WARNING_ON_USAGE'        { TokKeyword KwWARNING_ON_USAGE $$ }
    'REWRITE'                 { TokKeyword KwREWRITE $$ }
    'STATIC'                  { TokKeyword KwSTATIC $$ }
    'TERMINATING'             { TokKeyword KwTERMINATING $$ }

    setN                      { TokSetN $$ }
    propN                     { TokPropN $$ }
    tex                       { TokTeX $$ }
    comment                   { TokComment $$ }

    '...'                     { TokSymbol SymEllipsis $$ }
    '..'                      { TokSymbol SymDotDot $$ }
    '.'                       { TokSymbol SymDot $$ }
    ';'                       { TokSymbol SymSemi $$ }
    ':'                       { TokSymbol SymColon $$ }
    '='                       { TokSymbol SymEqual $$ }
    '_'                       { TokSymbol SymUnderscore $$ }
    '?'                       { TokSymbol SymQuestionMark $$ }
    '->'                      { TokSymbol SymArrow $$ }
    '\\'                      { TokSymbol SymLambda $$ }
    '@'                       { TokSymbol SymAs $$ }
    '|'                       { TokSymbol SymBar $$ }
    '('                       { TokSymbol SymOpenParen $$ }
    ')'                       { TokSymbol SymCloseParen $$ }
    '(|'                      { TokSymbol SymOpenIdiomBracket $$ }
    '|)'                      { TokSymbol SymCloseIdiomBracket $$ }
    '{{'                      { TokSymbol SymDoubleOpenBrace $$ }
    '}}'                      { TokSymbol SymDoubleCloseBrace $$ }
    '{'                       { TokSymbol SymOpenBrace $$ }
    '}'                       { TokSymbol SymCloseBrace $$ }
--    ':{'                      { TokSymbol SymColonBrace $$ }
    vopen                     { TokSymbol SymOpenVirtualBrace $$ }
    vclose                    { TokSymbol SymCloseVirtualBrace $$ }
    vsemi                     { TokSymbol SymVirtualSemi $$ }
    '{-#'                     { TokSymbol SymOpenPragma $$ }
    '#-}'                     { TokSymbol SymClosePragma $$ }

    id                        { TokId $$ }
    q_id                      { TokQId $$ }

    string                    { TokString $$ }
    literal                   { TokLiteral $$ }

%%

{--------------------------------------------------------------------------
    Parsing the token stream. Used by the TeX compiler.
 --------------------------------------------------------------------------}

-- Parse a list of tokens.
Tokens :: { [Token] }
Tokens : TokensR        { reverse $1 }

-- Happy is much better at parsing left recursive grammars (constant
-- stack size vs. linear stack size for right recursive).
TokensR :: { [Token] }
TokensR : TokensR Token { $2 : $1 }
        |               { [] }

-- Parse single token.
Token :: { Token }
Token
    : 'abstract'                { TokKeyword KwAbstract $1 }
    | 'codata'                  { TokKeyword KwCoData $1 }
    | 'coinductive'             { TokKeyword KwCoInductive $1 }
    | 'constructor'             { TokKeyword KwConstructor $1 }
    | 'data'                    { TokKeyword KwData $1 }
    | 'eta-equality'            { TokKeyword KwEta $1 }
    | 'field'                   { TokKeyword KwField $1 }
    | 'forall'                  { TokKeyword KwForall $1 }
    | 'variable'                { TokKeyword KwVariable $1 }
    | 'hiding'                  { TokKeyword KwHiding $1 }
    | 'import'                  { TokKeyword KwImport $1 }
    | 'in'                      { TokKeyword KwIn $1 }
    | 'inductive'               { TokKeyword KwInductive $1 }
    | 'infix'                   { TokKeyword KwInfix $1 }
    | 'infixl'                  { TokKeyword KwInfixL $1 }
    | 'infixr'                  { TokKeyword KwInfixR $1 }
    | 'instance'                { TokKeyword KwInstance $1 }
    | 'overlap'                 { TokKeyword KwOverlap $1 }
    | 'let'                     { TokKeyword KwLet $1 }
    | 'macro'                   { TokKeyword KwMacro $1 }
    | 'module'                  { TokKeyword KwModule $1 }
    | 'mutual'                  { TokKeyword KwMutual $1 }
    | 'no-eta-equality'         { TokKeyword KwNoEta $1 }
    | 'open'                    { TokKeyword KwOpen $1 }
    | 'pattern'                 { TokKeyword KwPatternSyn $1 }
    | 'postulate'               { TokKeyword KwPostulate $1 }
    | 'primitive'               { TokKeyword KwPrimitive $1 }
    | 'private'                 { TokKeyword KwPrivate $1 }
    | 'Prop'                    { TokKeyword KwProp $1 }
    | 'public'                  { TokKeyword KwPublic $1 }
    | 'quote'                   { TokKeyword KwQuote $1 }
    | 'quoteContext'            { TokKeyword KwQuoteContext $1 }
    | 'quoteGoal'               { TokKeyword KwQuoteGoal $1 }
    | 'quoteTerm'               { TokKeyword KwQuoteTerm $1 }
    | 'record'                  { TokKeyword KwRecord $1 }
    | 'renaming'                { TokKeyword KwRenaming $1 }
    | 'rewrite'                 { TokKeyword KwRewrite $1 }
    | 'Set'                     { TokKeyword KwSet $1 }
    | 'syntax'                  { TokKeyword KwSyntax $1 }
    | 'tactic'                  { TokKeyword KwTactic $1 }
    | 'to'                      { TokKeyword KwTo $1 }
    | 'unquote'                 { TokKeyword KwUnquote $1 }
    | 'unquoteDecl'             { TokKeyword KwUnquoteDecl $1 }
    | 'unquoteDef'              { TokKeyword KwUnquoteDef $1 }
    | 'using'                   { TokKeyword KwUsing $1 }
    | 'where'                   { TokKeyword KwWhere $1 }
    | 'do'                      { TokKeyword KwDo $1 }
    | 'with'                    { TokKeyword KwWith $1 }

    | 'BUILTIN'                 { TokKeyword KwBUILTIN $1 }
    | 'CATCHALL'                { TokKeyword KwCATCHALL $1 }
    | 'DISPLAY'                 { TokKeyword KwDISPLAY $1 }
    | 'ETA'                     { TokKeyword KwETA $1 }
    | 'FOREIGN'                 { TokKeyword KwFOREIGN $1 }
    | 'COMPILE'                 { TokKeyword KwCOMPILE $1 }
    | 'IMPOSSIBLE'              { TokKeyword KwIMPOSSIBLE $1 }
    | 'INJECTIVE'               { TokKeyword KwINJECTIVE $1 }
    | 'INLINE'                  { TokKeyword KwINLINE $1 }
    | 'NOINLINE'                { TokKeyword KwNOINLINE $1 }
    | 'MEASURE'                 { TokKeyword KwMEASURE $1 }
    | 'NO_TERMINATION_CHECK'    { TokKeyword KwNO_TERMINATION_CHECK $1 }
    | 'NO_POSITIVITY_CHECK'     { TokKeyword KwNO_POSITIVITY_CHECK $1 }
    | 'NO_UNIVERSE_CHECK'       { TokKeyword KwNO_UNIVERSE_CHECK $1 }
    | 'NON_TERMINATING'         { TokKeyword KwNON_TERMINATING $1 }
    | 'OPTIONS'                 { TokKeyword KwOPTIONS $1 }
    | 'POLARITY'                { TokKeyword KwPOLARITY $1 }
    | 'REWRITE'                 { TokKeyword KwREWRITE $1 }
    | 'STATIC'                  { TokKeyword KwSTATIC $1 }
    | 'TERMINATING'             { TokKeyword KwTERMINATING $1 }
    | 'WARNING_ON_USAGE'        { TokKeyword KwWARNING_ON_USAGE $1 }

    | setN                      { TokSetN $1 }
    | propN                     { TokPropN $1 }
    | tex                       { TokTeX $1 }
    | comment                   { TokComment $1 }

    | '...'                     { TokSymbol SymEllipsis $1 }
    | '..'                      { TokSymbol SymDotDot $1 }
    | '.'                       { TokSymbol SymDot $1 }
    | ';'                       { TokSymbol SymSemi $1 }
    | ':'                       { TokSymbol SymColon $1 }
    | '='                       { TokSymbol SymEqual $1 }
    | '_'                       { TokSymbol SymUnderscore $1 }
    | '?'                       { TokSymbol SymQuestionMark $1 }
    | '->'                      { TokSymbol SymArrow $1 }
    | '\\'                      { TokSymbol SymLambda $1 }
    | '@'                       { TokSymbol SymAs $1 }
    | '|'                       { TokSymbol SymBar $1 }
    | '('                       { TokSymbol SymOpenParen $1 }
    | ')'                       { TokSymbol SymCloseParen $1 }
    | '(|'                      { TokSymbol SymOpenIdiomBracket $1 }
    | '|)'                      { TokSymbol SymCloseIdiomBracket $1 }
    | '{{'                      { TokSymbol SymDoubleOpenBrace $1 }
    | '}}'                      { TokSymbol SymDoubleCloseBrace $1 }
    | '{'                       { TokSymbol SymOpenBrace $1 }
    | '}'                       { TokSymbol SymCloseBrace $1 }
    | vopen                     { TokSymbol SymOpenVirtualBrace $1 }
    | vclose                    { TokSymbol SymCloseVirtualBrace $1 }
    | vsemi                     { TokSymbol SymVirtualSemi $1 }
    | '{-#'                     { TokSymbol SymOpenPragma $1 }
    | '#-}'                     { TokSymbol SymClosePragma $1 }

    | id                        { TokId $1 }
    | q_id                      { TokQId $1 }
    | string                    { TokString $1 }

    | literal                   { TokLiteral $1 }

{--------------------------------------------------------------------------
    Top level
 --------------------------------------------------------------------------}

File :: { ([Pragma], [Declaration]) }
File : vopen TopLevel maybe_vclose { takeOptionsPragmas $2 }

maybe_vclose :: { () }
maybe_vclose : {- empty -} { () }
             | vclose      { () }

{--------------------------------------------------------------------------
    Meta rules
 --------------------------------------------------------------------------}

-- The first token in a file decides the indentation of the top-level layout
-- block. Or not. It will if we allow the top-level module to be omitted.
-- topen :      {- empty -}     {% pushCurrentContext }


{-  A layout block might have to be closed by a parse error. Example:
        let x = e in e'
    Here the 'let' starts a layout block which should end before the 'in'.  The
    problem is that the lexer doesn't know this, so there is no virtual close
    brace. However when the parser sees the 'in' there will be a parse error.
    This is our cue to close the layout block.
-}
close :: { () }
close : vclose  { () }
      | error   {% popContext }


-- You can use concrete semi colons in a layout block started with a virtual
-- brace, so we don't have to distinguish between the two semi colons. You can't
-- use a virtual semi colon in a block started by a concrete brace, but this is
-- simply because the lexer will not generate virtual semis in this case.
semi :: { Interval }
semi : ';'    { $1 }
     | vsemi  { $1 }


-- Enter the 'imp_dir' lex state, where we can parse the keyword 'to'.
beginImpDir :: { () }
beginImpDir : {- empty -}   {% pushLexState imp_dir }

{--------------------------------------------------------------------------
    Helper rules
 --------------------------------------------------------------------------}

-- An integer. Used in fixity declarations.
Int :: { Integer }
Int : literal   {% case $1 of {
                     LitNat _ i -> return i;
                     _          -> parseError $ "Expected integer"
                   }
                }


{--------------------------------------------------------------------------
    Names
 --------------------------------------------------------------------------}

-- A name is really a sequence of parts, but the lexer just sees it as a
-- string, so we have to do the translation here.
Id :: { Name }
Id : id     {% mkName $1 }

-- Space separated list of one or more identifiers.
SpaceIds :: { [Name] }
SpaceIds
    : Id SpaceIds { $1 : $2 }
    | Id          { [$1] }

-- When looking for a double closed brace, we accept either a single token '}}'
-- (which is what the unicode character "RIGHT WHITE CURLY BRACKET" is
-- postprocessed into in LexActions.hs), but also two consecutive tokens '}'
-- (which a string '}}' is lexed to).  This small hack allows us to keep
-- "record { a = record { }}" working. In the second case, we check that the two
-- tokens '}' are immediately consecutive.
DoubleCloseBrace :: { Range }
DoubleCloseBrace
  : '}}' { getRange $1 }
  | '}' '}' {%
      if posPos (fromJust (rEnd' (getRange $2))) -
         posPos (fromJust (rStart' (getRange $1))) > 2
      then parseErrorRange $2 "Expecting '}}', found separated '}'s."
      else return $ getRange ($1, $2)
    }

-- A possibly dotted identifier.
MaybeDottedId :: { Arg Name }
MaybeDottedId
  : '..' Id { setRelevance NonStrict $ defaultArg $2 }
  | '.'  Id { setRelevance Irrelevant $ defaultArg $2 }
  | Id      { defaultArg $1 }

-- Space separated list of one or more possibly dotted identifiers.
MaybeDottedIds :: { [Arg Name] }
MaybeDottedIds
    : MaybeDottedId MaybeDottedIds { $1 : $2 }
    | MaybeDottedId                { [$1] }

-- Space separated list of one or more identifiers, some of which may
-- be surrounded by braces or dotted.
ArgIds :: { [Arg Name] }
ArgIds
    : MaybeDottedId ArgIds            { $1 : $2 }
    | MaybeDottedId                   { [$1] }
    | '{{' MaybeDottedIds DoubleCloseBrace ArgIds { map makeInstance $2 ++ $4 }
    | '{{' MaybeDottedIds DoubleCloseBrace        { map makeInstance $2 }
    | '{' MaybeDottedIds '}' ArgIds   { map hide $2 ++ $4 }
    | '{' MaybeDottedIds '}'          { map hide $2 }
    | '.' '{' SpaceIds '}' ArgIds     { map (hide . setRelevance Irrelevant . defaultArg) $3 ++ $5 }
    | '.' '{' SpaceIds '}'            { map (hide . setRelevance Irrelevant . defaultArg) $3 }
    | '.' '{{' SpaceIds DoubleCloseBrace ArgIds   { map (makeInstance . setRelevance Irrelevant . defaultArg) $3 ++ $5 }
    | '.' '{{' SpaceIds DoubleCloseBrace          { map (makeInstance . setRelevance Irrelevant . defaultArg) $3 }
    | '..' '{' SpaceIds '}' ArgIds    { map (hide . setRelevance NonStrict . defaultArg) $3 ++ $5 }
    | '..' '{' SpaceIds '}'           { map (hide . setRelevance NonStrict . defaultArg) $3 }
    | '..' '{{' SpaceIds DoubleCloseBrace ArgIds  { map (makeInstance . setRelevance NonStrict . defaultArg) $3 ++ $5 }
    | '..' '{{' SpaceIds DoubleCloseBrace         { map (makeInstance . setRelevance NonStrict . defaultArg) $3 }

-- Modalities preceeding identifiers

ModalArgIds :: { [Arg Name] }
ModalArgIds : Attributes ArgIds  {% mapM (applyAttrs $1) $2 }

-- Attributes are parsed as '@' followed by an atomic expression.

Attribute :: { Attr }
Attribute : '@' ExprOrAttr  {% setRange (getRange ($1,$2)) `fmap` toAttribute $2 }

-- Parse a reverse list of modalities

Attributes :: { [Attr] }
Attributes : {- empty -}  { [] }
  | Attributes Attribute { $2 : $1 }

Attributes1 :: { [Attr] }
Attributes1 : Attribute  { [$1] }
  | Attributes1 Attribute { $2 : $1 }

QId :: { QName }
QId : q_id  {% mkQName $1 }
    | Id    { QName $1 }


-- A module name is just a qualified name
ModuleName :: { QName }
ModuleName : QId { $1 }


-- A binding variable. Can be '_'
BId :: { Name }
BId : Id    { $1 }
    | '_'   { Name (getRange $1) InScope [Hole] }

{- UNUSED
-- A binding variable. Can be '_'
MaybeDottedBId :: { (Relevance, Name) }
MaybeDottedBId
    : BId        { (Relevant  , $1) }
    | '.' BId    { (Irrelevant, $2) }
    | '..' BId   { (NonStrict, $2) }
-}


-- Space separated list of binding identifiers. Used in fixity
-- declarations infixl 100 + -
SpaceBIds :: { [Name] }
SpaceBIds
    : BId SpaceBIds { $1 : $2 }
    | BId           { [$1] }

{- DOES PRODUCE REDUCE/REDUCE CONFLICTS!
-- Space-separated list of binding identifiers. Used in dependent
-- function spaces: (x y z : Nat) -> ...
-- (Used to be comma-separated; hence the name)
-- QUESTION: Should this be replaced by SpaceBIds above?
--CommaBIds :: { [(Relevance,Name)] }
CommaBIds :: { [Name] }
CommaBIds
    : CommaBIds BId { $1 ++ [$2] }  -- SWITCHING DOES NOT HELP
    | BId           { [$1] }
-}

-- Space-separated list of binding identifiers. Used in dependent
-- function spaces: (x y z : Nat) -> ...
-- (Used to be comma-separated; hence the name)
-- QUESTION: Should this be replaced by SpaceBIds above?
-- Andreas, 2011-04-07 the trick avoids reduce/reduce conflicts
-- when parsing  (x y z : A) -> B
-- at point (x y  it is not clear whether x y is an application or
-- a variable list. We could be parsing (x y z) -> B
-- with ((x y) z) being a type.
CommaBIds :: { [NamedArg BoundName] }
CommaBIds : CommaBIdAndAbsurds {%
    case $1 of
      Left ns -> return ns
      Right _ -> parseError $ "expected sequence of bound identifiers, not absurd pattern"
    }

CommaBIdAndAbsurds :: { Either [NamedArg BoundName] [Expr] }
CommaBIdAndAbsurds
  : Application {% boundNamesOrAbsurd $1 }
  | QId '=' QId {% fmap (Left . (:[])) $ mkNamedArg (Just $1) (Left $3) }
  | '_' '=' QId {% fmap (Left . (:[])) $ mkNamedArg Nothing   (Left $3) }
  | QId '=' '_' {% fmap (Left . (:[])) $ mkNamedArg (Just $1) (Right $ getRange $3) }
  | '_' '=' '_' {% fmap (Left . (:[])) $ mkNamedArg Nothing   (Right $ getRange $3) }

-- Parse a sequence of identifiers, including hiding info.
-- Does not include instance arguments.
-- E.g. x {y z} _ {v}
-- To be used in typed bindings, like (x {y z} _ {v} : Nat).
BIdsWithHiding :: { [NamedArg BoundName] }
BIdsWithHiding : Application {%
    let -- interpret an expression as name
        getName :: Expr -> Maybe Name
        getName (Ident (QName x)) = Just x
        getName (Underscore r _)  = Just (Name r InScope [Hole])
        getName _                 = Nothing

        getNames :: Expr -> Maybe [Name]
        getNames (RawApp _ es) = mapM getName es
        getNames e             = singleton `fmap` getName e

        -- interpret an expression as name or list of hidden names
        getName1 :: Expr -> Maybe [Arg Name]
        getName1 (Ident (QName x)) = Just [defaultArg x]
        getName1 (Underscore r _)  = Just [defaultArg $ Name r InScope [Hole]]
        getName1 (HiddenArg _ (Named Nothing e))
                                   = map (setHiding Hidden . defaultArg) `fmap` getNames e
        getName1 _                 = Nothing

    in
    case mapM getName1 $1 of
        Just good -> return $ (map . fmap) (unnamed . mkBoundName_) $ concat good
        Nothing   -> parseError $ "expected sequence of possibly hidden bound identifiers"
    }


-- Space separated list of strings in a pragma.
PragmaStrings :: { [String] }
PragmaStrings
    : {- empty -}           { [] }
    | string PragmaStrings  { snd $1 : $2 }

PragmaString :: { String }
PragmaString
    : string { snd $1 }

Strings :: { [(Interval, String)] }
Strings : {- empty -}    { [] }
        | string Strings { $1 : $2 }

ForeignCode :: { [(Interval, String)] }
ForeignCode
  : {- empty -} { [] }
  | string ForeignCode { $1 : $2 }
  | '{-#' ForeignCode '#-}' ForeignCode { [($1, "{-#")] ++ $2 ++ [($3, "#-}")] ++ $4 }

PragmaName :: { Name }
PragmaName : string {% mkName $1 }

PragmaQName :: { QName }
PragmaQName : string {% pragmaQName $1 }  -- Issue 2125. WAS: string {% fmap QName (mkName $1) }

PragmaQNames :: { [QName] }
PragmaQNames : Strings {% mapM pragmaQName $1 }

{--------------------------------------------------------------------------
    Expressions (terms and types)
 --------------------------------------------------------------------------}

{-  Expressions. You might expect lambdas and lets to appear in the first
    expression category (lowest precedence). The reason they don't is that we
    want to parse things like

        m >>= \x -> k x

    This will leads to a conflict in the following case

        m >>= \x -> k x >>= \y -> k' y

    At the second '>>=' we can either shift or reduce. We solve this problem
    using Happy's precedence directives. The rule 'Expr -> Expr1' (which is the
    rule you shouldn't use to reduce when seeing '>>=') is given LOWEST
    precedence.  The terminals '->' and op (which is what you should shift)
    is given higher precedence.
-}

-- Top level: Function types.
Expr :: { Expr }
Expr
  : TeleArrow Expr                      { Pi $1 $2 }
  | Application3 '->' Expr              { Fun (getRange ($1,$2,$3))
                                              (defaultArg $ RawApp (getRange $1) $1)
                                              $3 }
  | Attributes1 Application3 '->' Expr  {% applyAttrs $1 (defaultArg $ RawApp (getRange ($1,$2)) $2) <&> \ dom ->
                                             Fun (getRange ($1,$2,$3,$4)) dom $4 }
  | Expr1 '=' Expr                      { Equal (getRange ($1, $2, $3)) $1 $3 }
  | Expr1 %prec LOWEST                  { $1 }

-- Level 1: Application
Expr1 :: { Expr }
Expr1  : WithExprs {% case $1 of
                      { [e]    -> return e
                      ; e : es -> return $ WithApp (fuseRange e es) e es
                      ; []     -> parseError "impossible: empty with expressions"
                      }
                   }

WithExprs :: { [Expr] }
WithExprs
  : Application3 '|' WithExprs { RawApp (getRange $1) $1 :  $3 }
  | Application                { [RawApp (getRange $1) $1] }

Application :: { [Expr] }
Application
    : Expr2             { [$1] }
    | Expr3 Application { $1 : $2 }

-- Level 2: Lambdas and lets
Expr2 :: { Expr }
Expr2
    : '\\' LamBindings Expr        { Lam (getRange ($1,$2,$3)) $2 $3 }
    | ExtendedOrAbsurdLam          { $1 }
    | 'forall' ForallBindings Expr        { forallPi $2 $3 }
    | 'let' Declarations LetBody   { Let (getRange ($1,$2,$3)) $2 $3 }
    | 'do' vopen DoStmts close     { DoBlock (getRange ($1, $3)) $3 }
    | Expr3                        { $1 }
    | 'quoteGoal' Id 'in' Expr     { QuoteGoal (getRange ($1,$2,$3,$4)) $2 $4 }
    | 'tactic' Application3               { Tactic (getRange ($1, $2)) (RawApp (getRange $2) $2) [] }
    | 'tactic' Application3 '|' WithExprs { Tactic (getRange ($1, $2, $3, $4)) (RawApp (getRange $2) $2) $4 }

LetBody :: { Maybe Expr }
LetBody : 'in' Expr   { Just $2 }
        | {- empty -} { Nothing }

ExtendedOrAbsurdLam :: { Expr }
ExtendedOrAbsurdLam
    : '\\'  '{' LamClauses '}'     { ExtendedLam (getRange ($1,$2,$3,$4)) (reverse $3) }
    | '\\' 'where' vopen LamWhereClauses close { ExtendedLam (getRange ($1, $2, $4)) (reverse $4) }
    | '\\' AbsurdLamBindings       {% case $2 of
                                       Left (bs, h) -> if null bs then return $ AbsurdLam r h else
                                                       return $ Lam r bs (AbsurdLam r h)
                                                         where r = fuseRange $1 bs
                                       Right es -> do -- it is of the form @\ { p1 ... () }@
                                                     p <- exprToLHS (RawApp (getRange es) es);
                                                     return $ ExtendedLam (fuseRange $1 es)
                                                                     [LamClause (p [] []) AbsurdRHS NoWhere False]
                                   }

Application3 :: { [Expr] }
Application3
    : Expr3              { [$1] }
    | Expr3 Application3 { $1 : $2 }

-- Christian Sattler, 2017-08-04, issue #2671
-- We allow empty lists of expressions for the LHS of extended lambda clauses.
-- I am not sure what Application3 is otherwise used for, so I keep the
-- original type and create this copy solely for extended lambda clauses.
Application3PossiblyEmpty :: { [Expr] }
Application3PossiblyEmpty
    :                                 { [] }
    | Expr3 Application3PossiblyEmpty { $1 : $2 }

-- Level 3: Atoms
Expr3Curly :: { Expr }
Expr3Curly
    : '{' Expr '}'                      { HiddenArg (getRange ($1,$2,$3)) (maybeNamed $2) }
    | '{' '}'                           { let r = fuseRange $1 $2 in HiddenArg r $ unnamed $ Absurd r }

Expr3NoCurly :: { Expr }
Expr3NoCurly
    : '?'                               { QuestionMark (getRange $1) Nothing }
    | '_'                               { Underscore (getRange $1) Nothing }
    | 'Prop'                            { Prop (getRange $1) }
    | 'Set'                             { Set (getRange $1) }
    | 'quote'                           { Quote (getRange $1) }
    | 'quoteTerm'                       { QuoteTerm (getRange $1) }
    | 'quoteContext'                    { QuoteContext (getRange $1) }
    | 'unquote'                         { Unquote (getRange $1) }
    | setN                              { SetN (getRange (fst $1)) (snd $1) }
    | propN                             { PropN (getRange (fst $1)) (snd $1) }
    | '{{' Expr DoubleCloseBrace        { InstanceArg (getRange ($1,$2,$3)) (maybeNamed $2) }
    | '(|' Expr '|)'                    { IdiomBrackets (getRange ($1,$2,$3)) $2 }
    | '(' ')'                           { Absurd (fuseRange $1 $2) }
    | '{{' DoubleCloseBrace             { let r = fuseRange $1 $2 in InstanceArg r $ unnamed $ Absurd r }
    | Id '@' Expr3                      { As (getRange ($1,$2,$3)) $1 $3 }
    | '.' Expr3                         { Dot (fuseRange $1 $2) $2 }
    | 'record' '{' RecordAssignments '}' { Rec (getRange ($1,$2,$3,$4)) $3 }
    | 'record' Expr3NoCurly '{' FieldAssignments '}' { RecUpdate (getRange ($1,$2,$3,$4,$5)) $2 $4 }
    | '...'                             { Ellipsis (getRange $1) }
    | ExprOrAttr                       { $1 }

ExprOrAttr :: { Expr }
ExprOrAttr
    : QId                               { Ident $1 }
    | literal                           { Lit $1 }
    | '(' Expr ')'                      { Paren (getRange ($1,$2,$3)) $2 }

Expr3 :: { Expr }
Expr3
    : Expr3Curly                        { $1 }
    | Expr3NoCurly                      { $1 }

RecordAssignments :: { RecordAssignments }
RecordAssignments
  : {- empty -}        { [] }
  | RecordAssignments1 { $1 }

RecordAssignments1 :: { RecordAssignments }
RecordAssignments1
  : RecordAssignment                        { [$1] }
  | RecordAssignment ';' RecordAssignments1 { $1 : $3 }

RecordAssignment :: { RecordAssignment }
RecordAssignment
  : FieldAssignment  { Left  $1 }
  | ModuleAssignment { Right $1 }

ModuleAssignment :: { ModuleAssignment }
ModuleAssignment
  : ModuleName OpenArgs ImportDirective  { ModuleAssignment $1 $2 $3 }

FieldAssignments :: { [FieldAssignment] }
FieldAssignments
  : {- empty -}       { [] }
  | FieldAssignments1 { $1 }

FieldAssignments1 :: { [FieldAssignment] }
FieldAssignments1
  : FieldAssignment                       { [$1] }
  | FieldAssignment ';' FieldAssignments1 { $1 : $3 }

FieldAssignment :: { FieldAssignment }
FieldAssignment
  : Id '=' Expr   { FieldAssignment $1 $3 }

{--------------------------------------------------------------------------
    Bindings
 --------------------------------------------------------------------------}

-- "Delta ->" to avoid conflict between Delta -> Gamma and Delta -> A.
TeleArrow :: { Telescope }
TeleArrow : Telescope1 '->' { $1 }

Telescope1 :: { Telescope }
Telescope1 : TypedBindings { $1 }

TypedBindings :: { [TypedBinding] }
TypedBindings
    : TypedBinding TypedBindings { $1 : $2 }
    | TypedBinding               { [$1] }


-- A typed binding is either (x1 .. xn : A) or   {y1 .. ym : B}
-- Andreas, 2011-04-07: or  .(x1 .. xn : A) or  .{y1 .. ym : B}
-- Andreas, 2011-04-27: or ..(x1 .. xn : A) or ..{y1 .. ym : B}
TypedBinding :: { TypedBinding }
TypedBinding
    : '.' '(' TBindWithHiding ')'    { setRange (getRange ($2,$3,$4)) $
                             setRelevance Irrelevant $3 }
    | '.' '{' TBind '}'    { setRange (getRange ($2,$3,$4)) $
                             setHiding Hidden $
                             setRelevance Irrelevant $3 }
    | '.' '{{' TBind DoubleCloseBrace
                           { setRange (getRange ($2,$3,$4)) $
                             makeInstance $
                             setRelevance Irrelevant $3 }
    | '..' '(' TBindWithHiding ')'   { setRange (getRange ($2,$3,$4)) $
                             setRelevance NonStrict $3 }
    | '..' '{' TBind '}'   { setRange (getRange ($2,$3,$4)) $
                             setHiding Hidden $
                             setRelevance NonStrict $3 }
    | '..' '{{' TBind DoubleCloseBrace
                           { setRange (getRange ($2,$3,$4)) $
                             makeInstance $
                             setRelevance NonStrict $3 }
    | '(' TBindWithHiding ')'        { setRange (getRange ($1,$2,$3)) $2 }
    | '(' ModalTBindWithHiding ')'        { setRange (getRange ($1,$2,$3)) $2 }
    | '{{' TBind DoubleCloseBrace
                           { setRange (getRange ($1,$2,$3)) $
                             makeInstance $2 }
    | '{{' ModalTBind DoubleCloseBrace
                           { setRange (getRange ($1,$2,$3)) $
                             makeInstance $2 }
    | '{' TBind '}'        { setRange (getRange ($1,$2,$3)) $
                             setHiding Hidden $2 }
    | '{' ModalTBind '}'   { setRange (getRange ($1,$2,$3)) $
                             setHiding Hidden $2 }
    | '(' Open ')'               { TLet (getRange ($1,$3)) $2 }
    | '(' 'let' Declarations ')' { TLet (getRange ($1,$4)) $3 }


-- x1 .. xn : A
-- x1 .. xn :{i1 i2 ..} A
TBind :: { TypedBinding }
TBind : CommaBIds ':' Expr  {
    let r = getRange ($1,$2,$3) -- the range is approximate only for TypedBindings
    in TBind r $1 $3
  }

ModalTBind :: { TypedBinding }
ModalTBind : Attributes1 CommaBIds ':' Expr  {% do
    let r = getRange ($1,$2,$3,$4) -- the range is approximate only for TypedBindings
    xs <- mapM (applyAttrs $1) $2
    return $ TBind r xs $4
  }

-- x {y z} _ {v} : A
TBindWithHiding :: { TypedBinding }
TBindWithHiding : BIdsWithHiding ':' Expr  {
    let r = getRange ($1,$2,$3) -- the range is approximate only for TypedBindings
    in TBind r $1 $3
  }

ModalTBindWithHiding :: { TypedBinding }
ModalTBindWithHiding : Attributes1 BIdsWithHiding ':' Expr  {% do
    let r = getRange ($1,$2,$3,$4) -- the range is approximate only for TypedBindings
    xs <- mapM (applyAttrs $1) $2
    return $ TBind r xs $4
  }

-- A non-empty sequence of lambda bindings.
LamBindings :: { [LamBinding] }
LamBindings
  : LamBinds '->' {%
      case reverse $1 of
        Left _ : _ -> parseError "Absurd lambda cannot have a body."
        _ : _      -> return [ b | Right b <- $1 ]
        []         -> parsePanic "Empty LamBinds"
      }

AbsurdLamBindings :: { Either ([LamBinding], Hiding) [Expr] }
AbsurdLamBindings
  : LamBindsAbsurd {%
    case $1 of
      Left lb -> case reverse lb of
                   Right _ : _ -> parseError "Missing body for lambda"
                   Left h  : _ -> return $ Left ([ b | Right b <- init lb], h)
                   _           -> parseError "Unsupported variant of lambda"
      Right es -> return $ Right es
    }

-- absurd lambda is represented by @Left hiding@
LamBinds :: { [Either Hiding LamBinding] }
LamBinds
  : DomainFreeBinding LamBinds  { map Right $1 ++ $2 }
  | TypedBinding LamBinds       { Right (DomainFull $1) : $2 }
  | DomainFreeBinding           { map Right $1 }
  | TypedBinding                { [Right $ DomainFull $1] }
  | '(' ')'                     { [Left NotHidden] }
  | '{' '}'                     { [Left Hidden] }
  | '{{' DoubleCloseBrace       { [Left (Instance NoOverlap)] }

-- Like LamBinds, but could also parse an absurd LHS of an extended lambda @{ p1 ... () }@
LamBindsAbsurd :: { Either [Either Hiding LamBinding] [Expr] }
LamBindsAbsurd
  : DomainFreeBinding LamBinds  { Left $ map Right $1 ++ $2 }
  | TypedBinding LamBinds       { Left $ Right (DomainFull $1) : $2 }
  | DomainFreeBindingAbsurd     { case $1 of
                                    Left lb -> Left $ map Right lb
                                    Right es -> Right es }
  | TypedBinding                { Left [Right $ DomainFull $1] }
  | '(' ')'                     { Left [Left NotHidden] }
  | '{' '}'                     { Left [Left Hidden] }
  | '{{' DoubleCloseBrace       { Left [Left (Instance NoOverlap)] }

-- FNF, 2011-05-05: No where clauses in extended lambdas for now
NonAbsurdLamClause :: { LamClause }
NonAbsurdLamClause
  : Application3PossiblyEmpty '->' Expr {% do
      p <- exprToLHS (RawApp (getRange $1) $1) ;
      return LamClause{ lamLHS      = p [] []
                      , lamRHS      = RHS $3
                      , lamWhere    = NoWhere
                      , lamCatchAll = False }
        }
  | CatchallPragma Application3PossiblyEmpty '->' Expr {% do
      p <- exprToLHS (RawApp (getRange $2) $2) ;
      return LamClause{ lamLHS      = p [] []
                      , lamRHS      = RHS $4
                      , lamWhere    = NoWhere
                      , lamCatchAll = True }
        }

AbsurdLamClause :: { LamClause }
AbsurdLamClause
-- FNF, 2011-05-09: By being more liberal here, we avoid shift/reduce and reduce/reduce errors.
-- Later stages such as scope checking will complain if we let something through which we should not
  : Application {% do
      p <- exprToLHS (RawApp (getRange $1) $1);
      return LamClause{ lamLHS      = p [] []
                      , lamRHS      = AbsurdRHS
                      , lamWhere    = NoWhere
                      , lamCatchAll = False }
        }
  | CatchallPragma Application {% do
      p <- exprToLHS (RawApp (getRange $2) $2);
      return LamClause{ lamLHS      = p [] []
                      , lamRHS      = AbsurdRHS
                      , lamWhere    = NoWhere
                      , lamCatchAll = True }
        }

LamClause :: { LamClause }
LamClause
  : NonAbsurdLamClause { $1 }
  | AbsurdLamClause { $1 }

-- Parses all extended lambda clauses except for a single absurd clause, which is taken care of
-- in AbsurdLambda
LamClauses :: { [LamClause] }
LamClauses
   : LamClauses semi LamClause { $3 : $1 }
   | AbsurdLamClause semi LamClause { [$3, $1] }
   | NonAbsurdLamClause { [$1] }
--   | {- empty -} { [] }

-- Parses all extended lambda clauses including a single absurd clause. For λ
-- where this is not taken care of in AbsurdLambda
LamWhereClauses :: { [LamClause] }
LamWhereClauses
   : LamWhereClauses semi LamClause { $3 : $1 }
   | LamClause { [$1] }

ForallBindings :: { [LamBinding] }
ForallBindings
  : TypedUntypedBindings1 '->' { $1 }

-- A non-empty sequence of possibly untyped bindings.
TypedUntypedBindings1 :: { [LamBinding] }
TypedUntypedBindings1
  : DomainFreeBinding TypedUntypedBindings1 { $1 ++ $2 }
  | TypedBinding TypedUntypedBindings1      { DomainFull $1 : $2 }
  | DomainFreeBinding                       { $1 }
  | TypedBinding                            { [DomainFull $1] }

-- A possibly empty sequence of possibly untyped bindings.
-- This is used as telescope in data and record decls.
TypedUntypedBindings :: { [LamBinding] }
TypedUntypedBindings
  : DomainFreeBinding TypedUntypedBindings { $1 ++ $2 }
  | TypedBinding TypedUntypedBindings      { DomainFull $1 : $2 }
  |                                        { [] }

-- A domain free binding is either x or {x1 .. xn}
DomainFreeBinding :: { [LamBinding] }
DomainFreeBinding
  : DomainFreeBindingAbsurd {% case $1 of
                             Left lbs -> return lbs
                             Right _ -> parseError "expected sequence of bound identifiers, not absurd pattern"
                          }

-- A domain free binding is either x or {x1 .. xn}
DomainFreeBindingAbsurd :: { Either [LamBinding] [Expr]}
DomainFreeBindingAbsurd
    : BId               { Left [DomainFree $ defaultNamedArg $ mkBoundName_ $1]  }
    | '.' BId           { Left [DomainFree $ setRelevance Irrelevant $ defaultNamedArg $ mkBoundName_ $2]  }
    | '..' BId          { Left [DomainFree $ setRelevance NonStrict $ defaultNamedArg $ mkBoundName_ $2]  }
    | '(' CommaBIdAndAbsurds ')'
         { mapLeft (map DomainFree) $2 }
    | '(' Attributes1 CommaBIdAndAbsurds ')'
         {% applyAttrs $2 defaultArgInfo <&> \ ai ->
              mapLeft (map (DomainFree . setArgInfo ai)) $3 }
    | '{' CommaBIdAndAbsurds '}'
         { mapLeft (map (DomainFree . setHiding Hidden)) $2 }
    | '{' Attributes1 CommaBIdAndAbsurds '}'
         {% applyAttrs $2 defaultArgInfo <&> \ ai ->
              mapLeft (map (DomainFree . setHiding Hidden . setArgInfo ai)) $3 }
    | '{{' CommaBIds DoubleCloseBrace { Left $ map (DomainFree . makeInstance) $2 }
    | '{{' Attributes1 CommaBIds DoubleCloseBrace
         {% applyAttrs $2 defaultArgInfo <&> \ ai ->
              Left $ map (DomainFree . makeInstance . setArgInfo ai) $3 }
    | '.' '{' CommaBIds '}' { Left $ map (DomainFree . setHiding Hidden . setRelevance Irrelevant) $3 }
    | '.' '{{' CommaBIds DoubleCloseBrace { Left $ map (DomainFree . makeInstance . setRelevance Irrelevant) $3 }
    | '..' '{' CommaBIds '}' { Left $ map (DomainFree . setHiding Hidden . setRelevance NonStrict) $3 }
    | '..' '{{' CommaBIds DoubleCloseBrace { Left $ map (DomainFree . makeInstance . setRelevance NonStrict) $3 }


{--------------------------------------------------------------------------
    Do-notation
 --------------------------------------------------------------------------}

DoStmts :: { [DoStmt] }
DoStmts : DoStmt              { [$1] }
        | DoStmt vsemi        { [$1] }    -- #3046
        | DoStmt semi DoStmts { $1 : $3 }

DoStmt :: { DoStmt }
DoStmt : Expr DoWhere {% buildDoStmt $1 $2 }

DoWhere :: { [LamClause] }
DoWhere
  : {- empty -} { [] }
  | 'where' vopen LamWhereClauses close { reverse $3 }

{--------------------------------------------------------------------------
    Modules and imports
 --------------------------------------------------------------------------}

-- Import directives
ImportDirective :: { ImportDirective }
ImportDirective : ImportDirectives {% mergeImportDirectives $1 }

ImportDirectives :: { [ImportDirective] }
ImportDirectives
  : ImportDirective1 ImportDirectives { $1 : $2 }
  | {- empty -}                       { [] }

ImportDirective1 :: { ImportDirective }
  : 'public'      { defaultImportDir { importDirRange = getRange $1, publicOpen = True } }
  | Using         { defaultImportDir { importDirRange = snd $1, using    = fst $1 } }
  | Hiding        { defaultImportDir { importDirRange = snd $1, hiding   = fst $1 } }
  | RenamingDir   { defaultImportDir { importDirRange = snd $1, impRenaming = fst $1 } }

Using :: { (Using, Range) }
Using
    : 'using' '(' CommaImportNames ')'   { (Using $3 , getRange ($1,$2,$3,$4)) }
        -- using can have an empty list

Hiding :: { ([ImportedName], Range) }
Hiding
    : 'hiding' '(' CommaImportNames ')'  { ($3 , getRange ($1,$2,$3,$4)) }
        -- if you want to hide nothing that's fine, isn't it?

RenamingDir :: { ([Renaming] , Range) }
RenamingDir
    : 'renaming' '(' Renamings ')'      { ($3 , getRange ($1,$2,$3,$4)) }
    | 'renaming' '(' ')'                { ([] , getRange ($1,$2,$3)) }

-- Renamings of the form 'x to y'
Renamings :: { [Renaming] }
Renamings
    : Renaming ';' Renamings    { $1 : $3 }
    | Renaming                  { [$1] }

Renaming :: { Renaming }
Renaming
    : ImportName_ 'to' Id { Renaming $1 (setImportedName $1 $3) (getRange $2) }

-- We need a special imported name here, since we have to trigger
-- the imp_dir state exactly one token before the 'to'
ImportName_ :: { ImportedName }
ImportName_
    : beginImpDir Id          { ImportedName $2 }
    | 'module' beginImpDir Id { ImportedModule $3 }

ImportName :: { ImportedName }
ImportName : Id          { ImportedName $1 }
           | 'module' Id { ImportedModule $2 }

-- Actually semi-colon separated
CommaImportNames :: { [ImportedName] }
CommaImportNames
    : {- empty -}       { [] }
    | CommaImportNames1 { $1 }

CommaImportNames1 :: { [ImportedName] }
CommaImportNames1
    : ImportName                        { [$1] }
    | ImportName ';' CommaImportNames1  { $1 : $3 }

{--------------------------------------------------------------------------
    Function clauses
 --------------------------------------------------------------------------}

-- A left hand side of a function clause. We parse it as an expression, and
-- then check that it is a valid left hand side.
LHS :: { LHS }
LHS : Expr1 RewriteEquations WithExpressions
        {% exprToLHS $1 >>= \p -> return (p $2 $3) }

WithExpressions :: { [Expr] }
WithExpressions
  : {- empty -} { [] }
  | 'with' Expr
      { case $2 of { WithApp _ e es -> e : es; e -> [e] } }

RewriteEquations :: { [Expr] }
RewriteEquations
  : {- empty -} { [] }
  | 'rewrite' Expr1
      { case $2 of { WithApp _ e es -> e : es; e -> [e] } }

-- Parsing either an expression @e@ or a @rewrite e1 | ... | en@.
HoleContent :: { HoleContent }
HoleContent
  : Expr             { HoleContentExpr    $1 }
  | RewriteEquations { HoleContentRewrite $1 }

-- Where clauses are optional.
WhereClause :: { WhereClause }
WhereClause
    : {- empty -}                      { NoWhere         }
    | 'where' Declarations0            { AnyWhere $2     }
    | 'module' Id 'where' Declarations0 { SomeWhere $2 PublicAccess $4 }
    | 'module' Underscore 'where' Declarations0 { SomeWhere $2 PublicAccess $4 }

ExprWhere :: { ExprWhere }
ExprWhere : Expr WhereClause { ExprWhere $1 $2 }

{--------------------------------------------------------------------------
    Different kinds of declarations
 --------------------------------------------------------------------------}

-- Top-level definitions.
Declaration :: { [Declaration] }
Declaration
    : Fields        {  $1  }
    | FunClause     {  $1  }  -- includes type signatures
    | Data          { [$1] }
    | DataSig       { [$1] }  -- lone data type signature in mutual block
    | Record        { [$1] }
    | RecordSig     { [$1] }  -- lone record signature in mutual block
    | Infix         { [$1] }
    | Generalize    {  $1  }
    | Mutual        { [$1] }
    | Abstract      { [$1] }
    | Private       { [$1] }
    | Instance      { [$1] }
    | Macro         { [$1] }
    | Postulate     { [$1] }
    | Primitive     { [$1] }
    | Open          {  $1  }
--    | Import      { [$1] }
    | ModuleMacro   { [$1] }
    | Module        { [$1] }
    | Pragma        { [$1] }
    | Syntax        { [$1] }
    | PatternSyn    { [$1] }
    | UnquoteDecl   { [$1] }


{--------------------------------------------------------------------------
    Individual declarations
 --------------------------------------------------------------------------}

-- Type signatures of the form "n1 n2 n3 ... : Type", with at least
-- one bound name.
TypeSigs :: { [Declaration] }
TypeSigs : SpaceIds ':' Expr { map (\ x -> typeSig defaultArgInfo x $3) $1 }

-- A variant of TypeSigs where any sub-sequence of names can be marked
-- as hidden or irrelevant using braces and dots:
-- {n1 .n2} n3 .n4 {n5} .{n6 n7} ... : Type.
ArgTypeSigs :: { [Arg Declaration] }
ArgTypeSigs
  : ModalArgIds ':' Expr { map (fmap (\ x -> typeSig defaultArgInfo x $3)) $1 }
  | 'overlap' ModalArgIds ':' Expr {%
      let setOverlap x =
            case getHiding x of
              Instance _ -> return $ makeInstance' YesOverlap x
              _          -> parseErrorRange $1
                             "The 'overlap' keyword only applies to instance fields (fields marked with {{ }})"
      in T.traverse (setOverlap . fmap (\ x -> typeSig defaultArgInfo x $4)) $2 }
  | 'instance' ArgTypeSignatures {
    let
      setInstance (TypeSig info x t) = TypeSig (makeInstance info) x t
      setInstance _ = __IMPOSSIBLE__ in
    map (fmap setInstance) $2 }

-- Function declarations. The left hand side is parsed as an expression to allow
-- declarations like 'x::xs ++ ys = e', when '::' has higher precedence than '++'.
-- FunClause also handle possibly dotted type signatures.
FunClause :: { [Declaration] }
FunClause : LHS RHS WhereClause {% funClauseOrTypeSigs [] $1 $2 $3 }
  | Attributes1 LHS RHS WhereClause {% funClauseOrTypeSigs $1 $2 $3 $4 }

RHS :: { RHSOrTypeSigs }
RHS : '=' Expr      { JustRHS (RHS $2) }
    | ':' Expr      { TypeSigsRHS $2 }
    | {- empty -}   { JustRHS AbsurdRHS }

-- Data declaration. Can be local.
Data :: { Declaration }
Data : 'data' Id TypedUntypedBindings ':' Expr 'where'
            Declarations0       { Data (getRange ($1,$2,$3,$4,$5,$6,$7)) Inductive $2 $3 $5 $7 }
     | 'codata' Id TypedUntypedBindings ':' Expr 'where'
            Declarations0       { Data (getRange ($1,$2,$3,$4,$5,$6,$7)) CoInductive $2 $3 $5 $7 }

  -- New cases when we already had a DataSig.  Then one can omit the sort.
     | 'data' Id TypedUntypedBindings 'where'
            Declarations0       { DataDef (getRange ($1,$2,$3,$4,$5)) Inductive $2 $3 $5 }
     | 'codata' Id TypedUntypedBindings 'where'
            Declarations0       { DataDef (getRange ($1,$2,$3,$4,$5)) CoInductive $2 $3 $5 }

-- Data type signature. Found in mutual blocks.
DataSig :: { Declaration }
DataSig : 'data' Id TypedUntypedBindings ':' Expr
  { DataSig (getRange ($1,$2,$3,$4,$5)) Inductive $2 $3 $5 }

-- Andreas, 2012-03-16:  The Expr3NoCurly instead of Id in everything
-- following 'record' is to remove the (harmless) shift/reduce conflict
-- introduced by record update expressions.

-- Record declarations.
Record :: { Declaration }
Record : 'record' Expr3NoCurly TypedUntypedBindings ':' Expr 'where'
            RecordDeclarations
         {% exprToName $2 >>= \ n -> let ((x,y,z),ds) = $7 in return $ Record (getRange ($1,$2,$3,$4,$5,$6,$7)) n x y z $3 $5 ds }
       | 'record' Expr3NoCurly TypedUntypedBindings 'where'
            RecordDeclarations
         {% exprToName $2 >>= \ n -> let ((x,y,z),ds) = $5 in return $ RecordDef (getRange ($1,$2,$3,$4,$5)) n x y z $3 ds }

-- Record type signature. In mutual blocks.
RecordSig :: { Declaration }
RecordSig : 'record' Expr3NoCurly TypedUntypedBindings ':' Expr
  {% exprToName $2 >>= \ n -> return $ RecordSig (getRange ($1,$2,$3,$4,$5)) n $3 $5 }

-- Declaration of record constructor name.
RecordConstructorName :: { (Name, IsInstance) }
RecordConstructorName :                  'constructor' Id        { ($2, NotInstanceDef) }
                      | 'instance' vopen 'constructor' Id vclose { ($4, InstanceDef) }

-- Fixity declarations.
Infix :: { Declaration }
Infix : 'infix'  Int SpaceBIds  { Infix (Fixity (getRange ($1,$3)) (Related $2) NonAssoc)   $3 }
      | 'infixl' Int SpaceBIds  { Infix (Fixity (getRange ($1,$3)) (Related $2) LeftAssoc)  $3 }
      | 'infixr' Int SpaceBIds  { Infix (Fixity (getRange ($1,$3)) (Related $2) RightAssoc) $3 }

-- Field declarations.
Fields :: { [Declaration] }
Fields : 'field' ArgTypeSignatures
            { let
                inst i = case getHiding i of
                           Instance _ -> InstanceDef
                           _          -> NotInstanceDef
                toField (Arg info (TypeSig info' x t)) = Field (inst info') x (Arg info t)
              in map toField $2 }
  -- | 'field' ModalArgTypeSignatures
  --           { let
  --               inst i = case getHiding i of
  --                          Instance _ -> InstanceDef
  --                          _          -> NotInstanceDef
  --               toField (Arg info (TypeSig info' x t)) = Field (inst info') x (Arg info t)
  --             in map toField $2 }

-- Variable declarations for automatic generalization
Generalize :: { [Declaration] }
Generalize : 'variable' ArgTypeSignaturesOrEmpty
            { let
                toGeneralize (Arg info (TypeSig _ x t)) = TypeSig info x t
              in [ Generalize (fuseRange $1 $2) (map toGeneralize $2) ] }

-- Mutually recursive declarations.
Mutual :: { Declaration }
Mutual : 'mutual' Declarations0  { Mutual (fuseRange $1 $2) $2 }


-- Abstract declarations.
Abstract :: { Declaration }
Abstract : 'abstract' Declarations0  { Abstract (fuseRange $1 $2) $2 }


-- Private can only appear on the top-level (or rather the module level).
Private :: { Declaration }
Private : 'private' Declarations0        { Private (fuseRange $1 $2) UserWritten $2 }


-- Instance declarations.
Instance :: { Declaration }
Instance : 'instance' Declarations0  { InstanceB (fuseRange $1 $2) $2 }


-- Macro declarations.
Macro :: { Declaration }
Macro : 'macro' Declarations0 { Macro (fuseRange $1 $2) $2 }


-- Postulates.
Postulate :: { Declaration }
Postulate : 'postulate' Declarations0 { Postulate (fuseRange $1 $2) $2 }

-- Primitives. Can only contain type signatures.
Primitive :: { Declaration }
Primitive : 'primitive' TypeSignatures0  { Primitive (fuseRange $1 $2) $2 }

-- Unquoting declarations.
UnquoteDecl :: { Declaration }
UnquoteDecl
  : 'unquoteDecl' '=' Expr { UnquoteDecl (fuseRange $1 $3) [] $3 }
  | 'unquoteDecl' SpaceIds '=' Expr { UnquoteDecl (fuseRange $1 $4) $2 $4 }
  | 'unquoteDef'  SpaceIds '=' Expr { UnquoteDef (fuseRange $1 $4) $2 $4 }

-- Syntax declaration (To declare eg. mixfix binders)
Syntax :: { Declaration }
Syntax : 'syntax' Id HoleNames '=' SimpleIds  {%
  case $2 of
    Name _ _ [_] -> case mkNotation $3 $5 of
      Left err -> parseError $ "Malformed syntax declaration: " ++ err
      Right n -> return $ Syntax $2 n
    _ -> parseError "Syntax declarations are allowed only for simple names (without holes)"
}

-- Pattern synonyms.
PatternSyn :: { Declaration }
PatternSyn : 'pattern' Id PatternSynArgs '=' Expr {% do
  p <- exprToPattern $5
  return (PatternSyn (getRange ($1,$2,$3,$4,$5)) $2 $3 p)
  }

PatternSynArgs :: { [Arg Name] }
PatternSynArgs
  : {- empty -} { [] }
  | LamBinds    {% patternSynArgs $1 }

SimpleIds :: { [RString] }
SimpleIds : SimpleId { [$1] }
          | SimpleIds SimpleId {$1 ++ [$2]}

HoleNames :: { [NamedArg HoleName] }
HoleNames : HoleName { [$1] }
          | HoleNames HoleName {$1 ++ [$2]}

HoleName :: { NamedArg HoleName }
HoleName
  : SimpleTopHole { defaultNamedArg $1 }
  | '{'  SimpleHole '}'  { hide         $ defaultNamedArg $2 }
  | '{{' SimpleHole '}}' { makeInstance $ defaultNamedArg $2 }
  | '{'  SimpleId '=' SimpleHole '}'  { hide         $ defaultArg $ named $2 $4 }
  | '{{' SimpleId '=' SimpleHole '}}' { makeInstance $ defaultArg $ named $2 $4 }

SimpleTopHole :: { HoleName }
SimpleTopHole
  : SimpleId { ExprHole $1 }
  | '(' '\\' SimpleId '->' SimpleId ')' { LambdaHole $3 $5 }
  | '(' '\\' '_'      '->' SimpleId ')' { LambdaHole (Ranged (getRange $3) "_") $5 }

SimpleHole :: { HoleName }
SimpleHole
  : SimpleId { ExprHole $1 }
  | '\\' SimpleId '->' SimpleId { LambdaHole $2 $4 }
  | '\\' '_'      '->' SimpleId { LambdaHole (Ranged (getRange $3) "_") $4 }
-- Variable name hole to be implemented later.

-- Discard the interval.
SimpleId :: { RString }
SimpleId : id  { Ranged (getRange $ fst $1) (stringToRawName $ snd $1) }

MaybeOpen :: { Maybe Range }
MaybeOpen : 'open'      { Just (getRange $1) }
          | {- empty -} { Nothing }

-- Open
Open :: { [Declaration] }
Open : MaybeOpen 'import' ModuleName OpenArgs ImportDirective {%
    let
    { doOpen = maybe DontOpen (const DoOpen) $1
    ; m   = $3
    ; es  = $4
    ; dir = $5
    ; r   = getRange ($1, $2, m, es, dir)
    ; mr  = getRange m
    ; unique = hashString $ prettyShow $ (Strict.Nothing :: Strict.Maybe ()) <$ r
         -- turn range into unique id, but delete file path
         -- which is absolute and messes up suite of failing tests
         -- (different hashs on different installations)
         -- TODO: Don't use (insecure) hashes in this way.
    ; fresh  = Name mr NotInScope [ Id $ stringToRawName $ ".#" ++ prettyShow m ++ "-" ++ show unique ]
    ; fresh' = Name mr NotInScope [ Id $ stringToRawName $ ".#" ++ prettyShow m ++ "-" ++ show (unique + 1) ]
    ; impStm asR = Import r m (Just (AsName (Right fresh) asR)) DontOpen defaultImportDir
    ; appStm m' es =
        Private r Inserted
          [ ModuleMacro r m'
             (SectionApp (getRange es) []
               (RawApp (getRange es) (Ident (QName fresh) : es)))
             doOpen dir
          ]
    ; (initArgs, last2Args) = splitAt (length es - 2) es
    ; parseAsClause = case last2Args of
      { [ Ident (QName (Name asR InScope [Id x]))
        , e
          -- Andreas, 2018-11-03, issue #3364, accept anything after 'as'
          -- but require it to be a 'Name' in the scope checker.
        ] | rawNameToString x == "as" -> Just . (asR,) $
          if | Ident (QName m') <- e -> Right m'
             | otherwise             -> Left e
      ; _ -> Nothing
      }
    } in
    case es of
      { [] -> return [Import r m Nothing doOpen dir]
      ; _ | Just (asR, m') <- parseAsClause ->
              if null initArgs then return
                 [ Import (getRange (m, asR, m', dir)) m
                     (Just (AsName m' asR)) doOpen dir
                 ]
              else return [ impStm asR, appStm (fromRight (const fresh') m') initArgs ]
          -- Andreas, 2017-05-13, issue #2579
          -- Nisse reports that importing with instantation but without open
          -- could be usefule for bringing instances into scope.
          -- Ulf, 2018-12-6: Not since fixes of #1913 and #2489 which require
          -- instances to be in scope.
          | DontOpen <- doOpen -> parseErrorRange $2 "An import statement with module instantiation is useless without either an `open' keyword or an `as` binding giving a name to the instantiated module."
          | otherwise -> return
              [ impStm noRange
              , appStm (noName $ beginningOf $ getRange m) es
              ]
      }
  }
  |'open' ModuleName OpenArgs ImportDirective {
    let
    { m   = $2
    ; es  = $3
    ; dir = $4
    ; r   = getRange ($1, m, es, dir)
    } in
    [ case es of
      { []  -> Open r m dir
      ; _   -> Private r Inserted
                 [ ModuleMacro r (noName $ beginningOf $ getRange m)
                             (SectionApp (getRange (m , es)) [] (RawApp (fuseRange m es) (Ident m : es)))
                             DoOpen dir
                 ]
      }
    ]
  }
  | 'open' ModuleName '{{' '...' DoubleCloseBrace ImportDirective {
    let r = getRange $2 in
    [ Private r Inserted
      [ ModuleMacro r (noName $ beginningOf $ getRange $2) (RecordModuleInstance r $2) DoOpen $6
      ]
    ]
  }

OpenArgs :: { [Expr] }
OpenArgs : {- empty -}    { [] }
         | Expr3 OpenArgs { $1 : $2 }

ModuleApplication :: { Telescope -> Parser ModuleApplication }
ModuleApplication : ModuleName '{{' '...' DoubleCloseBrace { (\ts ->
                    if null ts then return $ RecordModuleInstance (getRange ($1,$2,$3,$4)) $1
                    else parseError "No bindings allowed for record module with non-canonical implicits" )
                    }
                  | ModuleName OpenArgs {
                    (\ts -> return $ SectionApp (getRange ($1, $2)) ts (RawApp (fuseRange $1 $2) (Ident $1 : $2)) ) }


-- Module instantiation
ModuleMacro :: { Declaration }
ModuleMacro : 'module' ModuleName TypedUntypedBindings '=' ModuleApplication ImportDirective
                    {% do { ma <- $5 (map addType $3)
                          ; name <- ensureUnqual $2
                          ; return $ ModuleMacro (getRange ($1, $2, ma, $6)) name ma DontOpen $6 } }
            | 'open' 'module' Id TypedUntypedBindings '=' ModuleApplication ImportDirective
                    {% do {ma <- $6 (map addType $4); return $ ModuleMacro (getRange ($1, $2, $3, ma, $7)) $3 ma DoOpen $7 } }

-- Module
Module :: { Declaration }
Module : 'module' ModuleName TypedUntypedBindings 'where' Declarations0
                    { Module (getRange ($1,$2,$3,$4,$5)) $2 (map addType $3) $5 }
       | 'module' Underscore TypedUntypedBindings 'where' Declarations0
                    { Module (getRange ($1,$2,$3,$4,$5)) (QName $2) (map addType $3) $5 }

Underscore :: { Name }
Underscore : '_' { noName (getRange $1) }

TopLevel :: { [Declaration] }
TopLevel : TopDeclarations { figureOutTopLevelModule $1 }

Pragma :: { Declaration }
Pragma : DeclarationPragma  { Pragma $1 }

DeclarationPragma :: { Pragma }
DeclarationPragma
  : BuiltinPragma            { $1 }
  | RewritePragma            { $1 }
  | CompilePragma            { $1 }
  | ForeignPragma            { $1 }
  | StaticPragma             { $1 }
  | InjectivePragma          { $1 }
  | InlinePragma             { $1 }
  | NoInlinePragma           { $1 }
  | ImpossiblePragma         { $1 }
  | TerminatingPragma        { $1 }
  | NonTerminatingPragma     { $1 }
  | NoTerminationCheckPragma { $1 }
  | WarningOnUsagePragma     { $1 }
  | MeasurePragma            { $1 }
  | CatchallPragma           { $1 }
  | DisplayPragma            { $1 }
  | EtaPragma                { $1 }
  | NoPositivityCheckPragma  { $1 }
  | NoUniverseCheckPragma    { $1 }
  | PolarityPragma           { $1 }
  | OptionsPragma            { $1 }
    -- Andreas, 2014-03-06
    -- OPTIONS pragma not allowed everywhere, but don't give parse error.
    -- Give better error during type checking instead.

OptionsPragma :: { Pragma }
OptionsPragma : '{-#' 'OPTIONS' PragmaStrings '#-}' { OptionsPragma (getRange ($1,$2,$4)) $3 }

BuiltinPragma :: { Pragma }
BuiltinPragma
    : '{-#' 'BUILTIN' string PragmaQName '#-}'
      { BuiltinPragma (getRange ($1,$2,fst $3,$4,$5)) (snd $3) $4 }
    -- Extra rule to accept keyword REWRITE also as built-in:
    | '{-#' 'BUILTIN' 'REWRITE' PragmaQName '#-}'
      { BuiltinPragma (getRange ($1,$2,$3,$4,$5)) "REWRITE" $4 }

RewritePragma :: { Pragma }
RewritePragma
    : '{-#' 'REWRITE' PragmaQNames '#-}'
      { RewritePragma (getRange ($1,$2,$3,$4)) $3 }

ForeignPragma :: { Pragma }
ForeignPragma
  : '{-#' 'FOREIGN' string ForeignCode '#-}' { ForeignPragma (getRange ($1, $2, fst $3, $5)) (snd $3) (recoverLayout $4) }

CompilePragma :: { Pragma }
CompilePragma
  : '{-#' 'COMPILE' string PragmaQName PragmaStrings '#-}'
    { CompilePragma (getRange ($1,$2,fst $3,$4,$6)) (snd $3) $4 (unwords $5) }

StaticPragma :: { Pragma }
StaticPragma
  : '{-#' 'STATIC' PragmaQName '#-}'
    { StaticPragma (getRange ($1,$2,$3,$4)) $3 }

InlinePragma :: { Pragma }
InlinePragma
  : '{-#' 'INLINE' PragmaQName '#-}'
    { InlinePragma (getRange ($1,$2,$3,$4)) True $3 }

NoInlinePragma :: { Pragma }
NoInlinePragma
  : '{-#' 'NOINLINE' PragmaQName '#-}'
    { InlinePragma (getRange ($1,$2,$3,$4)) False $3 }

InjectivePragma :: { Pragma }
InjectivePragma
  : '{-#' 'INJECTIVE' PragmaQName '#-}'
    { InjectivePragma (getRange ($1,$2,$3,$4)) $3 }

DisplayPragma :: { Pragma }
DisplayPragma
  : '{-#' 'DISPLAY' string PragmaStrings '#-}' {%
      let (r, s) = $3 in
      parseDisplayPragma (fuseRange $1 $5) (iStart r) (unwords (s : $4)) }

EtaPragma :: { Pragma }
EtaPragma
  : '{-#' 'ETA' PragmaQName '#-}'
    { EtaPragma (getRange ($1,$2,$3,$4)) $3 }

NoTerminationCheckPragma :: { Pragma }
NoTerminationCheckPragma
  : '{-#' 'NO_TERMINATION_CHECK' '#-}'
    { TerminationCheckPragma (getRange ($1,$2,$3)) NoTerminationCheck }

NonTerminatingPragma :: { Pragma }
NonTerminatingPragma
  : '{-#' 'NON_TERMINATING' '#-}'
    { TerminationCheckPragma (getRange ($1,$2,$3)) NonTerminating }

TerminatingPragma :: { Pragma }
TerminatingPragma
  : '{-#' 'TERMINATING' '#-}'
    { TerminationCheckPragma (getRange ($1,$2,$3)) Terminating }

MeasurePragma :: { Pragma }
MeasurePragma
  : '{-#' 'MEASURE' PragmaName '#-}'
    { let r = getRange ($1, $2, $3, $4) in
      TerminationCheckPragma r (TerminationMeasure r $3) }

CatchallPragma :: { Pragma }
CatchallPragma
  : '{-#' 'CATCHALL' '#-}'
    { CatchallPragma (getRange ($1,$2,$3)) }


ImpossiblePragma :: { Pragma }
  : '{-#' 'IMPOSSIBLE' '#-}'  { ImpossiblePragma (getRange ($1,$2,$3)) }

NoPositivityCheckPragma :: { Pragma }
NoPositivityCheckPragma
  : '{-#' 'NO_POSITIVITY_CHECK' '#-}'
    { NoPositivityCheckPragma (getRange ($1,$2,$3)) }

NoUniverseCheckPragma :: { Pragma }
NoUniverseCheckPragma
  : '{-#' 'NO_UNIVERSE_CHECK' '#-}'
    { NoUniverseCheckPragma (getRange ($1,$2,$3)) }

PolarityPragma :: { Pragma }
PolarityPragma
  : '{-#' 'POLARITY' PragmaName Polarities '#-}'
    { let (rs, occs) = unzip (reverse $4) in
      PolarityPragma (getRange ($1,$2,$3,rs,$5)) $3 occs }

WarningOnUsagePragma :: { Pragma }
WarningOnUsagePragma
  : '{-#' 'WARNING_ON_USAGE' PragmaQName literal '#-}'
  {%  case $4 of
        { LitString r str -> return $ WarningOnUsage (getRange ($1,$2,$3,r,$5)) $3 str
        ; _ -> parseError "Expected string literal"
        }
  }

-- Possibly empty list of polarities. Reversed.
Polarities :: { [(Range, Occurrence)] }
Polarities : {- empty -}          { [] }
           | Polarities Polarity  { $2 : $1 }

Polarity :: { (Range, Occurrence) }
Polarity : string {% polarity $1 }

{--------------------------------------------------------------------------
    Sequences of declarations
 --------------------------------------------------------------------------}

-- Possibly empty list of type signatures, with several identifiers allowed
-- for every signature.
TypeSignatures0 :: { [TypeSignature] }
TypeSignatures
    : vopen close    { [] }
    | TypeSignatures { $1 }

-- Non-empty list of type signatures, with several identifiers allowed
-- for every signature.
TypeSignatures :: { [TypeSignature] }
TypeSignatures
    : vopen TypeSignatures1 close   { reverse $2 }

-- Inside the layout block.
TypeSignatures1 :: { [TypeSignature] }
TypeSignatures1
    : TypeSignatures1 semi TypeSigs { reverse $3 ++ $1 }
    | TypeSigs                      { reverse $1 }

-- A variant of TypeSignatures which uses ArgTypeSigs instead of
-- TypeSigs.
ArgTypeSignatures :: { [Arg TypeSignature] }
ArgTypeSignatures
    : vopen ArgTypeSignatures1 close   { reverse $2 }

-- Inside the layout block.
ArgTypeSignatures1 :: { [Arg TypeSignature] }
ArgTypeSignatures1
    : ArgTypeSignatures1 semi ArgTypeSigs { reverse $3 ++ $1 }
    | ArgTypeSigs                         { reverse $1 }

-- A variant of TypeSignatures which uses ArgTypeSigs instead of
-- TypeSigs.
ArgTypeSignaturesOrEmpty :: { [Arg TypeSignature] }
ArgTypeSignaturesOrEmpty
    : vopen ArgTypeSignatures0 close   { reverse $2 }

-- Inside the layout block.
ArgTypeSignatures0 :: { [Arg TypeSignature] }
ArgTypeSignatures0
    : ArgTypeSignatures0 semi ArgTypeSigs { reverse $3 ++ $1 }
    | ArgTypeSigs                         { reverse $1 }
    | {- empty -}                         { [] }

-- -- A variant of TypeSignatures which uses ModalArgTypeSigs instead of
-- -- TypeSigs.
-- ModalArgTypeSignatures :: { [Arg TypeSignature] }
-- ModalArgTypeSignatures
--     : vopen ModalArgTypeSignatures1 close   { reverse $2 }

-- -- Inside the layout block.
-- ModalArgTypeSignatures1 :: { [Arg TypeSignature] }
-- ModalArgTypeSignatures1
--     : ModalArgTypeSignatures1 semi ModalArgTypeSigs { reverse $3 ++ $1 }
--     | ModalArgTypeSigs                              { reverse $1 }

-- Record declarations, including an optional record constructor name.
RecordDeclarations :: { ((Maybe (Ranged Induction), Maybe HasEta, Maybe (Name, IsInstance)), [Declaration]) }
RecordDeclarations
                                  : vopen RecordDirectives close {% ((,) `fmap` verifyRecordDirectives $2 <*> pure []) }
                                  | vopen RecordDirectives semi Declarations1 close {% ((,) `fmap` verifyRecordDirectives $2 <*> pure $4) }
                                  | vopen Declarations1 close {% ((,) `fmap` verifyRecordDirectives [] <*> pure $2)  }


RecordDirectives :: { [RecordDirective] }
RecordDirectives
                                  : { [] }
                                  | RecordDirectives semi RecordDirective { $3 : $1 }
                                  | RecordDirective { [$1] }

RecordDirective :: { RecordDirective }
RecordDirective
                                  : RecordConstructorName { Constructor $1 }
                                  | RecordInduction       { Induction $1 }
                                  | RecordEta             { Eta $1 }

RecordEta :: { Ranged HasEta }
RecordEta
                                  : 'eta-equality' { Ranged (getRange $1) YesEta }
                                  | 'no-eta-equality' { Ranged (getRange $1) NoEta }

-- Declaration of record as 'inductive' or 'coinductive'.
RecordInduction :: { Ranged Induction }
RecordInduction
   : 'inductive'   { Ranged (getRange $1) Inductive   }
   | 'coinductive' { Ranged (getRange $1) CoInductive }

-- Arbitrary declarations
Declarations :: { [Declaration] }
Declarations
    : vopen Declarations1 close { $2 }

-- Arbitrary declarations (possibly empty)
Declarations0 :: { [Declaration] }
Declarations0
    : vopen close  { [] }
    | Declarations { $1 }

Declarations1 :: { [Declaration] }
Declarations1
    : Declaration semi Declarations1 { $1 ++ $3 }
    | Declaration vsemi              { $1 } -- #3046
    | Declaration                    { $1 }

TopDeclarations :: { [Declaration] }
TopDeclarations
  : {- empty -}   { [] }
  | Declarations1 { $1 }

{

{--------------------------------------------------------------------------
    Parsers
 --------------------------------------------------------------------------}

-- | Parse the token stream. Used by the TeX compiler.
tokensParser :: Parser [Token]

-- | Parse an expression. Could be used in interactions.
exprParser :: Parser Expr

-- | Parse an expression followed by a where clause. Could be used in interactions.
exprWhereParser :: Parser ExprWhere

-- | Parse a module.
moduleParser :: Parser Module


{--------------------------------------------------------------------------
    Happy stuff
 --------------------------------------------------------------------------}

-- | Required by Happy.
happyError :: Parser a
happyError = parseError "Parse error"


{--------------------------------------------------------------------------
    Utility functions
 --------------------------------------------------------------------------}

-- | Grab leading OPTIONS pragmas.
takeOptionsPragmas :: [Declaration] -> ([Pragma], [Declaration])
takeOptionsPragmas = spanJust $ \ d -> case d of
  Pragma p@OptionsPragma{} -> Just p
  _                        -> 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 ds =
  case spanAllowedBeforeModule 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.
    (ds0, [ Module{} ]) -> ds

    -- Case 2: The declarations in the module are not indented.
    -- This is allowed for the top level module, and thus rectified here.
    (ds0, Module r m tel [] : ds2) -> ds0 ++ [Module r m tel 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.
    (ds0, Module r m tel ds1 : ds2) -> 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.
    _ -> ds0 ++ [Module r (QName $ noName r) [] ds1]
      where
      (ds0, ds1) = (`span` ds) $ \case
        Pragma OptionsPragma{} -> True
        _ -> 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 = beginningOfFile $ getRange ds1

-- | Create a name from a string.

mkName :: (Interval, String) -> Parser Name
mkName (i, s) = do
    let xs = C.stringNameParts s
    mapM_ isValidId xs
    unless (alternating xs) $ parseError $ "a name cannot contain two consecutive underscores"
    return $ Name (getRange i) InScope xs
    where
        isValidId Hole   = return ()
        isValidId (Id y) = do
          let x = rawNameToString y
              err = "in the name " ++ s ++ ", the part " ++ x ++ " is not valid"
          case parse defaultParseFlags [0] (lexer return) x of
            ParseOk _ TokId{}  -> return ()
            ParseFailed{}      -> parseError err
            ParseOk _ TokEOF{} -> parseError err
            ParseOk _ t   -> parseError . ((err ++ " because it is ") ++) $ case t of
              TokId{}       -> __IMPOSSIBLE__
              TokQId{}      -> __IMPOSSIBLE__ -- "qualified"
              TokKeyword{}  -> "a keyword"
              TokLiteral{}  -> "a literal"
              TokSymbol s _ -> case s of
                SymDot               -> __IMPOSSIBLE__ -- "reserved"
                SymSemi              -> "used to separate declarations"
                SymVirtualSemi       -> __IMPOSSIBLE__
                SymBar               -> "used for with-arguments"
                SymColon             -> "part of declaration syntax"
                SymArrow             -> "the function arrow"
                SymEqual             -> "part of declaration syntax"
                SymLambda            -> "used for lambda-abstraction"
                SymUnderscore        -> "used for anonymous identifiers"
                SymQuestionMark      -> "a meta variable"
                SymAs                -> "used for as-patterns"
                SymOpenParen         -> "used to parenthesize expressions"
                SymCloseParen        -> "used to parenthesize expressions"
                SymOpenIdiomBracket  -> "an idiom bracket"
                SymCloseIdiomBracket -> "an idiom bracket"
                SymDoubleOpenBrace   -> "used for instance arguments"
                SymDoubleCloseBrace  -> "used for instance arguments"
                SymOpenBrace         -> "used for hidden arguments"
                SymCloseBrace        -> "used for hidden arguments"
                SymOpenVirtualBrace  -> __IMPOSSIBLE__
                SymCloseVirtualBrace -> __IMPOSSIBLE__
                SymOpenPragma        -> __IMPOSSIBLE__ -- "used for pragmas"
                SymClosePragma       -> __IMPOSSIBLE__ -- "used for pragmas"
                SymEllipsis          -> "used for function clauses"
                SymDotDot            -> __IMPOSSIBLE__ -- "a modality"
                SymEndComment        -> "the end-of-comment brace"
              TokString{}   -> __IMPOSSIBLE__
              TokSetN{}     -> "a type universe"
              TokPropN{}    -> "a prop universe"
              TokTeX{}      -> __IMPOSSIBLE__  -- used by the LaTeX backend only
              TokMarkup{}   -> __IMPOSSIBLE__  -- ditto
              TokComment{}  -> __IMPOSSIBLE__
              TokDummy{}    -> __IMPOSSIBLE__
              TokEOF{}      -> __IMPOSSIBLE__

        -- we know that there are no two Ids in a row
        alternating (Hole : Hole : _) = False
        alternating (_ : xs)          = alternating xs
        alternating []                = True

-- | Create a qualified name from a list of strings
mkQName :: [(Interval, String)] -> Parser QName
mkQName ss = do
    xs <- mapM mkName ss
    return $ foldr Qual (QName $ last xs) (init xs)

-- | 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 (r, s) = do
  let ss = chopWhen (== '.') s
  mkQName $ map (r,) ss

mkNamedArg :: Maybe QName -> Either QName Range -> Parser (NamedArg BoundName)
mkNamedArg x y = do
  lbl <- case x of
           Nothing        -> return $ Just $ unranged "_"
           Just (QName x) -> return $ Just $ Ranged (getRange x) (prettyShow x)
           _              -> parseError "expected unqualified variable name"
  var <- case y of
           Left (QName y) -> return $ BName y noFixity'
           Right r        -> return $ BName (noName r) noFixity'
           _              -> parseError "expected unqualified variable name"
  return $ defaultArg $ Named lbl var

-- | Polarity parser.

polarity :: (Interval, String) -> Parser (Range, Occurrence)
polarity (i, s) =
  case s of
    "_"  -> ret Unused
    "++" -> ret StrictPos
    "+"  -> ret JustPos
    "-"  -> ret JustNeg
    "*"  -> ret Mixed
    _    -> parseError $ "Not a valid polarity: " ++ s
  where
  ret x = return (getRange i, x)

recoverLayout :: [(Interval, String)] -> String
recoverLayout [] = ""
recoverLayout xs@((i, _) : _) = go (iStart i) xs
  where
    c0 = posCol (iStart i)

    go cur [] = ""
    go cur ((i, s) : xs) = padding cur (iStart i) ++ s ++ go (iEnd i) xs

    padding Pn{ posLine = l1, posCol = c1 } Pn{ posLine = l2, posCol = c2 }
      | l1 < l2  = genericReplicate (l2 - l1) '\n' ++ genericReplicate (max 0 (c2 - c0)) ' '
      | l1 == l2 = genericReplicate (c2 - c1) ' '

ensureUnqual :: QName -> Parser Name
ensureUnqual (QName x) = return x
ensureUnqual q@Qual{}  = parseError' (rStart' $ getRange q) "Qualified name not allowed here"

-- | Match a particular name.
isName :: String -> (Interval, String) -> Parser ()
isName s (_,s')
    | s == s'   = return ()
    | otherwise = parseError $ "expected " ++ s ++ ", found " ++ s'

-- | Build a forall pi (forall x y z -> ...)
forallPi :: [LamBinding] -> Expr -> Expr
forallPi bs e = Pi (map addType bs) e

-- | Converts lambda bindings to typed bindings.
addType :: LamBinding -> TypedBinding
addType (DomainFull b) = b
addType (DomainFree x) = TBind r [x] $ Underscore r Nothing
  where r = getRange x

boundNamesOrAbsurd :: [Expr] -> Parser (Either [NamedArg BoundName] [Expr])
boundNamesOrAbsurd es
  | any isAbsurd es = return $ Right es
  | otherwise       =
    case mapM getBName es of
        Just good -> return $ Left $ map defaultNamedArg good
        Nothing   -> parseError $ "expected sequence of bound identifiers"
  where
    getName :: Expr -> Maybe Name
    getName (Ident (QName x)) = Just x
    getName (Underscore r _)  = Just $ Name r NotInScope [Hole]
    getName _                 = Nothing

    getBName :: Expr -> Maybe BoundName
    getBName e = fmap mkBoundName_ $ getName e

    isAbsurd :: Expr -> Bool
    isAbsurd (Absurd _)                  = True
    isAbsurd (HiddenArg _ (Named _ e))   = isAbsurd e
    isAbsurd (InstanceArg _ (Named _ e)) = isAbsurd e
    isAbsurd (Paren _ expr)              = isAbsurd expr
    isAbsurd (RawApp _ exprs)            = any isAbsurd exprs
    isAbsurd _                           = False

-- | Build a do-statement
buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
buildDoStmt (RawApp r [e]) cs = buildDoStmt e cs
buildDoStmt (Let r ds Nothing) [] = return $ DoLet r ds
buildDoStmt (RawApp r es) cs
  | (es1, arr : es2) <- break isLeftArrow es =
    case filter isLeftArrow es2 of
      arr : _ -> parseError' (rStart' $ getRange arr) $ "Unexpected " ++ prettyShow arr
      [] -> DoBind (getRange arr)
              <$> exprToPattern (RawApp (getRange es1) es1)
              <*> pure (RawApp (getRange es2) es2)
              <*> pure cs
  where
    isLeftArrow (Ident (QName (Name _ _ [Id arr]))) = elem arr ["<-", "←"]
    isLeftArrow _ = False
buildDoStmt e (_ : _) = parseError' (rStart' $ getRange e) "Only pattern matching do-statements can have where clauses."
buildDoStmt e [] = return $ DoThen e

mergeImportDirectives :: [ImportDirective] -> Parser ImportDirective
mergeImportDirectives is = do
  i <- foldl merge (return defaultImportDir) is
  verifyImportDirective i
  where
    merge mi i2 = do
      i1 <- mi
      let err = parseError' (rStart' $ getRange i2) "Cannot mix using and hiding module directives"
      return $ ImportDirective
        { importDirRange = fuseRange i1 i2
        , using          = mappend (using i1) (using i2)
        , hiding         = hiding i1 ++ hiding i2
        , impRenaming    = impRenaming i1 ++ impRenaming i2
        , publicOpen     = publicOpen i1 || publicOpen i2 }

-- | Check that an import directive doesn't contain repeated names
verifyImportDirective :: ImportDirective -> Parser ImportDirective
verifyImportDirective i =
    case filter ((>1) . length)
         $ group
         $ sort xs
    of
        []  -> return i
        yss -> parseErrorRange (head $ concat yss) $
                "Repeated name" ++ s ++ " in import directive: " ++
                concat (intersperse ", " $ map (prettyShow . head) yss)
            where
                s = case yss of
                        [_] -> ""
                        _   -> "s"
    where
        xs = names (using i) ++ hiding i ++ map renFrom (impRenaming i)
        names (Using xs)    = xs
        names UseEverything = []

data RecordDirective
   = Induction (Ranged Induction)
   | Constructor (Name, IsInstance)
   | Eta         (Ranged HasEta)
   deriving (Eq,Show)

verifyRecordDirectives :: [RecordDirective] -> Parser (Maybe (Ranged Induction), Maybe HasEta, Maybe (Name, IsInstance))
verifyRecordDirectives xs
  | null rs = return (ltm is, ltm es, ltm cs)
  | otherwise = parseErrorRange (head rs) $ "Repeated record directives at: \n" ++ intercalate "\n" (map prettyShow rs)
 where
  ltm :: [a] -> Maybe a
  ltm [] = Nothing
  ltm (x:xs) = Just x
  errorFromList [] = []
  errorFromList [x] = []
  errorFromList xs = map getRange xs
  rs = sort (concat ([errorFromList is, errorFromList es', errorFromList cs]))
  is = [ i | Induction i <- xs ]
  es' = [ i | Eta i <- xs ]
  es = map rangedThing es'
  cs = [ i | Constructor i <- xs ]


-- | Breaks up a string into substrings. Returns every maximal
-- subsequence of zero or more characters distinct from @'.'@.
--
-- > splitOnDots ""         == [""]
-- > splitOnDots "foo.bar"  == ["foo", "bar"]
-- > splitOnDots ".foo.bar" == ["", "foo", "bar"]
-- > splitOnDots "foo.bar." == ["foo", "bar", ""]
-- > splitOnDots "foo..bar" == ["foo", "", "bar"]
splitOnDots :: String -> [String]
splitOnDots ""        = [""]
splitOnDots ('.' : s) = [] : splitOnDots s
splitOnDots (c   : s) = case splitOnDots s of
  p : ps -> (c : p) : ps


-- | Returns 'True' iff the name is a valid Haskell (hierarchical)
-- module name.
validHaskellModuleName :: String -> Bool
validHaskellModuleName = all ok . splitOnDots
  where
  -- Checks if a dot-less module name is well-formed.
  ok :: String -> Bool
  ok []      = False
  ok (c : s) =
    isUpper c &&
    all (\c -> isLower c || c == '_' ||
               isUpper c ||
               generalCategory c == DecimalNumber ||
               c == '\'')
        s

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

-- | Turn an expression into a left hand side.
exprToLHS :: Expr -> Parser ([Expr] -> [Expr] -> LHS)
exprToLHS e = LHS <$> exprToPattern e

-- | Turn an expression into a pattern. Fails if the expression is not a
--   valid pattern.
exprToPattern :: Expr -> Parser Pattern
exprToPattern e = do
    let failure = parseErrorRange e $ "Not a valid pattern: " ++ prettyShow e
    case e of
        Ident x                 -> return $ IdentP x
        App _ e1 e2             -> AppP <$> exprToPattern e1
                                        <*> T.mapM (T.mapM exprToPattern) e2
        Paren r e               -> ParenP r
                                        <$> exprToPattern e
        Underscore r _          -> return $ WildP r
        Absurd r                -> return $ AbsurdP r
        As r x e                -> AsP r x <$> exprToPattern e
        Dot r (HiddenArg _ e)   -> return $ HiddenP r $ fmap (DotP r) e
        Dot r e                 -> return $ DotP r e
        Lit l                   -> return $ LitP l
        HiddenArg r e           -> HiddenP r <$> T.mapM exprToPattern e
        InstanceArg r e         -> InstanceP r <$> T.mapM exprToPattern e
        RawApp r es             -> RawAppP r <$> mapM exprToPattern es
        Quote r                 -> return $ QuoteP r
        Rec r es | Just fs <- mapM maybeLeft es -> do
          RecP r <$> T.mapM (T.mapM exprToPattern) fs
        Equal r e1 e2           -> return $ EqualP r [(e1, e2)]
        Ellipsis r              -> return $ EllipsisP r
        -- WithApp has already lost the range information of the bars '|'
        WithApp r e es          -> do
          p  <- exprToPattern e
          ps <- forM es $ \ e -> defaultNamedArg . WithP (getRange e) <$> exprToPattern e  -- TODO #2822: Range!
          return $ foldl AppP p ps
        _ -> failure

opAppExprToPattern :: OpApp Expr -> Parser Pattern
opAppExprToPattern (SyntaxBindingLambda _ _ _) = parseError "Syntax binding lambda cannot appear in a pattern"
opAppExprToPattern (Ordinary e) = exprToPattern e

-- | Turn an expression into a name. Fails if the expression is not a
--   valid identifier.
exprToName :: Expr -> Parser Name
exprToName (Ident (QName x)) = return x
exprToName e = parseErrorRange e $ "Not a valid identifier: " ++ prettyShow e

stripSingletonRawApp :: Expr -> Expr
stripSingletonRawApp (RawApp _ [e]) = stripSingletonRawApp e
stripSingletonRawApp e = e

isEqual :: Expr -> Maybe (Expr, Expr)
isEqual e =
  case stripSingletonRawApp e of
    Equal _ a b -> Just (stripSingletonRawApp a, stripSingletonRawApp b)
    _           -> Nothing

maybeNamed :: Expr -> Named_ Expr
maybeNamed e =
  case isEqual e of
    Just (Ident (QName x), b) -> named (Ranged (getRange x) (nameToRawName x)) b
    _                         -> unnamed e

patternSynArgs :: [Either Hiding LamBinding] -> Parser [Arg Name]
patternSynArgs = mapM pSynArg
  where
    pSynArg Left{}                   = parseError "Absurd patterns are not allowed in pattern synonyms"
    pSynArg (Right DomainFull{})     = parseError "Unexpected type signature in pattern synonym argument"
    pSynArg (Right (DomainFree x))
      | let h = getHiding x, h `notElem` [Hidden, NotHidden] = parseError $ prettyShow h ++ " arguments not allowed to pattern synonyms"
      | getRelevance x /= Relevant                = parseError "Arguments to pattern synonyms must be relevant"
      | otherwise                                 = return $ fmap (boundName . namedThing) x

parsePanic s = parseError $ "Internal parser error: " ++ s ++ ". Please report this as a bug."

{- RHS or type signature -}

data RHSOrTypeSigs
 = JustRHS RHS
 | TypeSigsRHS Expr
 deriving Show

patternToNames :: Pattern -> Parser [(ArgInfo, Name)]
patternToNames p =
  case p of
    IdentP (QName i)         -> return [(defaultArgInfo, i)]
    WildP r                  -> return [(defaultArgInfo, C.noName r)]
    DotP _ (Ident (QName i)) -> return [(setRelevance Irrelevant defaultArgInfo, i)]
    RawAppP _ ps             -> concat <$> mapM patternToNames ps
    _                        -> parseError $
      "Illegal name in type signature: " ++ prettyShow p

funClauseOrTypeSigs :: [Attr] -> LHS -> RHSOrTypeSigs -> WhereClause -> Parser [Declaration]
funClauseOrTypeSigs attrs lhs mrhs wh = do
  -- traceShowM lhs
  case mrhs of
    JustRHS rhs   -> do
      unless (null attrs) $ parseErrorRange attrs $ "A function clause cannot have attributes"
      return [FunClause lhs rhs wh False]
    TypeSigsRHS e -> case wh of
      NoWhere -> case lhs of
        LHS p _ _ | hasEllipsis p -> parseError "The ellipsis ... cannot have a type signature"
        LHS _ _ (_:_) -> parseError "Illegal: with in type signature"
        LHS _ (_:_) _ -> parseError "Illegal: rewrite in type signature"
        LHS p _ _ | hasWithPatterns p -> parseError "Illegal: with patterns in type signature"
        LHS p [] []  -> forMM (patternToNames p) $ \ (info, x) -> do
          info <- applyAttrs attrs info
          return $ typeSig info x e
      _ -> parseError "A type signature cannot have a where clause"

parseDisplayPragma :: Range -> Position -> String -> Parser Pragma
parseDisplayPragma r pos s =
  case parsePosString pos defaultParseFlags [normal] funclauseParser s of
    ParseOk s [FunClause (LHS lhs [] []) (RHS rhs) NoWhere ca] | null (parseInp s) ->
      return $ DisplayPragma r lhs rhs
    _ -> parseError "Invalid DISPLAY pragma. Should have form {-# DISPLAY LHS = RHS #-}."

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

-- * Attributes

-- | Parsed attribute.

data Attr = Attr
  { attrRange :: Range       -- ^ Range includes the @.
  , attrName  :: String      -- ^ Concrete, user written attribute for error reporting.
  , theAttr   :: Attribute   -- ^ Parsed attribute.
  }

instance HasRange Attr where
  getRange = attrRange

instance SetRange Attr where
  setRange r (Attr _ x a) = Attr r x a

-- | Parse an attribute.
toAttribute :: (HasRange e, Pretty e) => e -> Parser Attr
toAttribute x = maybe failure (return . Attr (getRange x) y) $ stringToAttribute y
  where
  y = prettyShow x
  failure = parseErrorRange x $ "Unknown attribute: " ++ y

-- | 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 attr@(Attr r x a) = maybe failure return . setPristineAttribute a
  where
  failure = errorConflictingAttribute 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 rattrs arg = do
  let attrs = reverse rattrs
  checkForUniqueAttribute (isJust . isQuantityAttribute ) attrs
  checkForUniqueAttribute (isJust . isRelevanceAttribute) attrs
  foldM (flip applyAttr) arg attrs

-- | 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 p attrs = do
  let pAttrs = filter (p . theAttr) attrs
  when (length pAttrs >= 2) $
    errorConflictingAttributes pAttrs

-- | Report an attribute as conflicting (e.g., with an already set value).
errorConflictingAttribute :: Attr -> Parser a
errorConflictingAttribute a = parseErrorRange a $ "Conflicting attribute: " ++ attrName a

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