-- | Utility functions used in the Happy parser.

{-# OPTIONS_GHC -Wunused-matches #-}

module Agda.Syntax.Parser.Helpers where

import Prelude hiding (null)

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

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

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

import Agda.TypeChecking.Positivity.Occurrence

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

import Agda.Utils.Impossible
import Data.List (partition)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type LamBinds = LamBinds' [LamBinding]

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

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

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

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

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

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

-- | Constructs extended lambdas.

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

-- | Constructs extended or absurd lambdas.

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

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

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

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

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

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

  where

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

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

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

  where

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

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

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

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

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

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


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

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

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

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

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

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

  case NamedArg Binder
x of

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

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

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

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

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

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

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

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

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

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

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

{- RHS or type signature -}

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

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

-- | Interpret leading dot as irrelevance

patternToArgPattern :: Pattern -> Arg Pattern
patternToArgPattern :: Pattern -> Arg Pattern
patternToArgPattern = \case
   DotP KwRange
kwr Range
_ (Ident QName
x)        -> KwRange -> Arg Pattern -> Arg Pattern
forall a b. (HasRange a, LensRelevance b) => a -> b -> b
makeIrrelevant KwRange
kwr (Arg Pattern -> Arg Pattern) -> Arg Pattern -> Arg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Arg Pattern
forall a. a -> Arg a
defaultArg (Pattern -> Arg Pattern) -> Pattern -> Arg Pattern
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Pattern
IdentP Bool
True QName
x
   DotP KwRange
kwr Range
_ (Underscore Range
r Maybe [Char]
_) -> KwRange -> Arg Pattern -> Arg Pattern
forall a b. (HasRange a, LensRelevance b) => a -> b -> b
makeIrrelevant KwRange
kwr (Arg Pattern -> Arg Pattern) -> Arg Pattern -> Arg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Arg Pattern
forall a. a -> Arg a
defaultArg (Pattern -> Arg Pattern) -> Pattern -> Arg Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Pattern
WildP Range
r
   Pattern
p -> Pattern -> Arg Pattern
forall a. a -> Arg a
defaultArg Pattern
p


funClauseOrTypeSigs :: [Attr] -> ([RewriteEqn] -> [WithExpr] -> LHS)
                    -> [Either RewriteEqn (List1 (Named Name Expr))]
                    -> RHSOrTypeSigs
                    -> WhereClause -> Parser (List1 Declaration)
funClauseOrTypeSigs :: [Attr]
-> ([RewriteEqn] -> [WithExpr] -> LHS)
-> [Either RewriteEqn (List1 (Named Name Expr))]
-> RHSOrTypeSigs
-> WhereClause
-> Parser (List1 Declaration)
funClauseOrTypeSigs [Attr]
attrs [RewriteEqn] -> [WithExpr] -> LHS
lhs' [Either RewriteEqn (List1 (Named Name Expr))]
with RHSOrTypeSigs
mrhs WhereClause
wh = do
  (rs , es) <- [Either RewriteEqn (List1 (Named Name Expr))]
-> Parser ([RewriteEqn], [Named Name Expr])
buildWithBlock [Either RewriteEqn (List1 (Named Name Expr))]
with
  let lhs = [RewriteEqn] -> [WithExpr] -> LHS
lhs' [RewriteEqn]
rs ((Named Name Expr -> WithExpr) -> [Named Name Expr] -> [WithExpr]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Arg Expr) -> Named Name Expr -> WithExpr
forall a b. (a -> b) -> Named Name a -> Named Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Arg Expr
observeModifiers) [Named Name Expr]
es)
  -- traceShowM lhs
  case mrhs of
    JustRHS RHS
rhs   -> do
      Maybe (Ranged Expr) -> (Ranged Expr -> Parser ()) -> Parser ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust ([Attr] -> Maybe (Ranged Expr)
haveTacticAttr [Attr]
attrs) \ Ranged Expr
re ->
        ParseWarning -> Parser ()
parseWarning (ParseWarning -> Parser ()) -> ParseWarning -> Parser ()
forall a b. (a -> b) -> a -> b
$ Range -> [Char] -> ParseWarning
MisplacedAttributes (Ranged Expr -> Range
forall a. HasRange a => a -> Range
getRange Ranged Expr
re) ([Char] -> ParseWarning) -> [Char] -> ParseWarning
forall a b. (a -> b) -> a -> b
$
          [Char]
"Ignoring tactic attribute, illegal in function clauses"
      -- Andreas, 2025-07-09, issue #7989: extract irrelevance info from lhs pattern
      let (Arg ArgInfo
info Pattern
p) = Pattern -> Arg Pattern
patternToArgPattern (Pattern -> Arg Pattern) -> Pattern -> Arg Pattern
forall a b. (a -> b) -> a -> b
$ LHS -> Pattern
lhsOriginalPattern LHS
lhs
      -- Andreas, 2025-07-10, issue #7988: allow attributes in function clause
      info <- [Attr] -> ArgInfo -> Parser ArgInfo
forall a. LensAttribute a => [Attr] -> a -> Parser a
applyAttrs [Attr]
attrs ArgInfo
info
      return $ singleton $ FunClause info lhs{ lhsOriginalPattern = p } rhs wh empty
    TypeSigsRHS Expr
e -> case WhereClause
wh of
      WhereClause
NoWhere -> case LHS
lhs of
        LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_ | Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"The ellipsis ... cannot have a type signature"
        LHS Pattern
_ [RewriteEqn]
_ (WithExpr
_:[WithExpr]
_) -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"Illegal: with in type signature"
        LHS Pattern
_ (RewriteEqn
_:[RewriteEqn]
_) [WithExpr]
_ -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"Illegal: rewrite in type signature"
        LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_ | Pattern -> Bool
forall p. CPatternLike p => p -> Bool
hasWithPatterns Pattern
p -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"Illegal: with patterns in type signature"
        LHS Pattern
p [] [] -> Parser (List1 (Arg Name))
-> (Arg Name -> Parser Declaration) -> Parser (List1 Declaration)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM (Pattern -> Parser (List1 (Arg Name))
patternToNames Pattern
p) ((Arg Name -> Parser Declaration) -> Parser (List1 Declaration))
-> (Arg Name -> Parser Declaration) -> Parser (List1 Declaration)
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
info Name
x) -> do
          info <- [Attr] -> ArgInfo -> Parser ArgInfo
forall a. LensAttribute a => [Attr] -> a -> Parser a
applyAttrs [Attr]
attrs ArgInfo
info
          return $ typeSig info (getTacticAttr attrs) x e
      WhereClause
_ -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"A type signature cannot have a where clause"

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

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

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

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

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

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

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

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

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

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

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

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

-- | Apply attributes to thing (usually `Arg`).
--   Expects a reversed list of attributes.
--   This will fail if one of the attributes is already set
--   in the thing to something else than the default value.
applyAttrsDropTactic :: LensAttribute a => [Attr] -> a -> Parser a
applyAttrsDropTactic :: forall a. LensAttribute a => [Attr] -> a -> Parser a
applyAttrsDropTactic [Attr]
rattrs a
arg = do
  let ([Attr]
tactics, [Attr]
attrs) = (Attr -> Bool) -> [Attr] -> ([Attr], [Attr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Attr -> Bool
isTactic [Attr]
rattrs
  [Attr] -> ([Attr] -> Parser ()) -> Parser ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull [Attr]
tactics \ [Attr]
ts ->
    ParseWarning -> Parser ()
parseWarning (ParseWarning -> Parser ()) -> ParseWarning -> Parser ()
forall a b. (a -> b) -> a -> b
$ Range -> [Char] -> ParseWarning
MisplacedAttributes ([Attr] -> Range
forall a. HasRange a => a -> Range
getRange [Attr]
ts) ([Char] -> ParseWarning) -> [Char] -> ParseWarning
forall a b. (a -> b) -> a -> b
$
      [Char]
"Ignoring misplaced @(tactic ...) attribute"
  [Attr] -> a -> Parser a
forall a. LensAttribute a => [Attr] -> a -> Parser a
applyAttrs [Attr]
attrs a
arg
  where
    isTactic :: Attr -> Bool
    isTactic :: Attr -> Bool
isTactic = Maybe (Ranged Expr) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Ranged Expr) -> Bool)
-> (Attr -> Maybe (Ranged Expr)) -> Attr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticAttribute -> Maybe (Ranged Expr)
forall a. TacticAttribute' a -> Maybe (Ranged a)
C.theTacticAttribute (TacticAttribute -> Maybe (Ranged Expr))
-> (Attr -> TacticAttribute) -> Attr -> Maybe (Ranged Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attribute -> TacticAttribute
isTacticAttribute (Attribute -> TacticAttribute)
-> (Attr -> Attribute) -> Attr -> TacticAttribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attr -> Attribute
theAttr

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

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

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

-- | Get the tactic attribute if present.
getTacticAttr :: [Attr] -> TacticAttribute
getTacticAttr :: [Attr] -> TacticAttribute
getTacticAttr = Maybe (Ranged Expr) -> TacticAttribute
forall a. Maybe (Ranged a) -> TacticAttribute' a
C.TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute)
-> ([Attr] -> Maybe (Ranged Expr)) -> [Attr] -> TacticAttribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Attr] -> Maybe (Ranged Expr)
haveTacticAttr

-- | Check if tactic attribute is present.
haveTacticAttr :: [Attr] -> Maybe (Ranged Expr)
haveTacticAttr :: [Attr] -> Maybe (Ranged Expr)
haveTacticAttr [Attr]
as =
  case [Attribute] -> [Attribute]
tacticAttributes [ Attribute
a | Attr Range
_ [Char]
_ Attribute
a <- [Attr]
as ] of
    [CA.TacticAttribute Ranged Expr
e] -> Ranged Expr -> Maybe (Ranged Expr)
forall a. a -> Maybe a
Just Ranged Expr
e
    [] -> Maybe (Ranged Expr)
forall a. Maybe a
Nothing
    [Attribute]
_  -> Maybe (Ranged Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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