module Agda.Syntax.Parser.Helpers where
import Prelude hiding (null)
import Control.Applicative ( (<|>) )
import Control.Monad
import Control.Monad.State
import Data.Bifunctor (first, second)
import Data.Char
import qualified Data.List as List
import Data.Maybe
import Data.Semigroup ((<>), sconcat)
import qualified Data.Traversable 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 )
import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty hiding ((<>))
import Agda.Utils.Singleton
import qualified Agda.Utils.Maybe.Strict as Strict
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Impossible
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)
figureOutTopLevelModule :: [Declaration] -> [Declaration]
figureOutTopLevelModule :: [Declaration] -> [Declaration]
figureOutTopLevelModule [Declaration]
ds =
case [Declaration] -> ([Declaration], [Declaration])
spanAllowedBeforeModule [Declaration]
ds of
([Declaration]
ds0, [ Module{} ]) -> [Declaration]
ds
([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]
([Declaration]
ds0, Module Range
r Erased
_ QName
m Telescope
tel [Declaration]
ds1 : [Declaration]
ds2) -> [Declaration]
ds
([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
r :: Range
r = Range -> Range
beginningOfFile (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Range
forall a. HasRange a => a -> Range
getRange [Declaration]
ds1
mkName :: (Interval, String) -> Parser Name
mkName :: (Interval, [Char]) -> Parser Name
mkName (Interval
i, [Char]
s) = do
let xs :: NameParts
xs = [Char] -> NameParts
C.stringNameParts [Char]
s
(NamePart -> Parser ()) -> NameParts -> Parser ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ NamePart -> Parser ()
isValidId NameParts
xs
Bool -> Parser () -> Parser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (NameParts -> Bool
alternating NameParts
xs) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Parser ()
forall a. [Char] -> Parser a
parseError ([Char] -> Parser ()) -> [Char] -> Parser ()
forall a b. (a -> b) -> a -> b
$ [Char]
"a name cannot contain two consecutive underscores"
Name -> Parser Name
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Parser Name) -> Name -> Parser Name
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> NameParts -> Name
Name (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i) NameInScope
InScope NameParts
xs
where
isValidId :: NamePart -> Parser ()
isValidId NamePart
Hole = () -> Parser ()
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
isValidId (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{} -> () -> Parser ()
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ParseFailed{} -> [Char] -> Parser ()
forall a. [Char] -> Parser a
parseError [Char]
err
ParseOk ParseState
_ TokEOF{} -> [Char] -> Parser ()
forall a. [Char] -> Parser a
parseError [Char]
err
ParseOk ParseState
_ Token
t -> [Char] -> Parser ()
forall a. [Char] -> Parser a
parseError ([Char] -> Parser ()) -> ([Char] -> [Char]) -> [Char] -> Parser ()
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] -> Parser ()) -> [Char] -> Parser ()
forall a b. (a -> b) -> a -> b
$ case Token
t of
TokQId{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
TokKeyword{} -> [Char]
"a keyword"
TokLiteral{} -> [Char]
"a literal"
TokSymbol Symbol
s Interval
_ -> case Symbol
s of
Symbol
SymDot -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
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]
forall a. HasCallStack => a
__IMPOSSIBLE__
Symbol
SymClosePragma -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
Symbol
SymEllipsis -> [Char]
"used for function clauses"
Symbol
SymDotDot -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
Symbol
SymEndComment -> [Char]
"the end-of-comment brace"
TokString{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
TokTeX{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
TokMarkup{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
TokComment{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
TokDummy{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
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
mkQName :: [(Interval, String)] -> Parser QName
mkQName :: [(Interval, [Char])] -> Parser QName
mkQName [(Interval, [Char])]
ss = do
xs <- ((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])]
ss
return $ foldr Qual (QName $ last xs) (init xs)
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 -> BoundName -> Binder
forall a. Maybe Pattern -> a -> Binder' a
Binder Maybe Pattern
p (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
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 :: (Interval, String) -> Parser (Range, Occurrence)
polarity :: (Interval, [Char]) -> Parser (Range, Occurrence)
polarity (Interval
i, [Char]
s) =
case [Char]
s of
[Char]
"_" -> Occurrence -> Parser (Range, Occurrence)
ret Occurrence
Unused
[Char]
"++" -> Occurrence -> Parser (Range, Occurrence)
ret Occurrence
StrictPos
[Char]
"+" -> Occurrence -> Parser (Range, Occurrence)
ret Occurrence
JustPos
[Char]
"-" -> Occurrence -> Parser (Range, Occurrence)
ret Occurrence
JustNeg
[Char]
"*" -> Occurrence -> Parser (Range, Occurrence)
ret Occurrence
Mixed
[Char]
_ -> [Char] -> Parser (Range, Occurrence)
forall a. [Char] -> Parser a
parseError ([Char] -> Parser (Range, Occurrence))
-> [Char] -> Parser (Range, Occurrence)
forall a b. (a -> b) -> a -> b
$ [Char]
"Not a valid polarity: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
where
ret :: Occurrence -> Parser (Range, Occurrence)
ret Occurrence
x = (Range, Occurrence) -> Parser (Range, Occurrence)
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Interval -> Range
forall a. HasRange a => a -> Range
getRange Interval
i, Occurrence
x)
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 :: Int32
c0 = Position' SrcFile -> Int32
forall a. Position' a -> Int32
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 -> Int32
posLine = Int32
l1, posCol :: forall a. Position' a -> Int32
posCol = Int32
c1 } Pn{ posLine :: forall a. Position' a -> Int32
posLine = Int32
l2, posCol :: forall a. Position' a -> Int32
posCol = Int32
c2 }
| Int32
l1 Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
< Int32
l2 = Int32 -> Char -> [Char]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate (Int32
l2 Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
- Int32
l1) Char
'\n' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int32 -> Char -> [Char]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate (Int32 -> Int32 -> Int32
forall a. Ord a => a -> a -> a
max Int32
0 (Int32
c2 Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
- Int32
c0)) Char
' '
| Int32
l1 Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
== Int32
l2 = Int32 -> Char -> [Char]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate (Int32
c2 Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
- Int32
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"
data LamBinds' a = LamBinds
{ forall a. LamBinds' a -> a
lamBindings :: a
, forall a. LamBinds' a -> Maybe Hiding
absurdBinding :: Maybe Hiding
} 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
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
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
onlyErased
:: [Attr]
-> 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"
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
extLam
:: Range
-> [Attr]
-> List1 LamClause
-> 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'
extOrAbsLam
:: Range
-> [Attr]
-> 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
e <- [Attr] -> Parser Erased
onlyErased [Attr]
attrs
cl <- mkAbsurdLamClause False 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
(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)
((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
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
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 (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
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
[] ->
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"]
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
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__
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
defaultBuildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
defaultBuildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
defaultBuildDoStmt Expr
e (LamClause
_ : [LamClause]
_) = Maybe PositionWithoutFile -> [Char] -> Parser DoStmt
forall a. Maybe PositionWithoutFile -> [Char] -> Parser a
parseError' (Range -> Maybe PositionWithoutFile
forall a. Range' a -> Maybe PositionWithoutFile
rStart' (Range -> Maybe PositionWithoutFile)
-> Range -> Maybe PositionWithoutFile
forall a b. (a -> b) -> a -> b
$ Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e) [Char]
"Only pattern matching do-statements can have where clauses."
defaultBuildDoStmt Expr
e [] = DoStmt -> Parser DoStmt
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DoStmt -> Parser DoStmt) -> DoStmt -> Parser DoStmt
forall a b. (a -> b) -> a -> b
$ Expr -> DoStmt
DoThen Expr
e
buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
buildDoStmt (Let Range
r List1 Declaration
ds Maybe Expr
Nothing) [] = DoStmt -> Parser DoStmt
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (DoStmt -> Parser DoStmt) -> DoStmt -> Parser DoStmt
forall a b. (a -> b) -> a -> b
$ Range -> List1 Declaration -> DoStmt
DoLet Range
r List1 Declaration
ds
buildDoStmt e :: Expr
e@(RawApp Range
r List2 Expr
_) [LamClause]
cs = do
mpatexpr <- Expr -> Parser (Maybe (Pattern, Range, Expr))
exprToAssignment Expr
e
case mpatexpr of
Just (Pattern
pat, Range
r, Expr
expr) -> DoStmt -> Parser DoStmt
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DoStmt -> Parser DoStmt) -> DoStmt -> Parser DoStmt
forall a b. (a -> b) -> a -> b
$ Range -> Pattern -> Expr -> [LamClause] -> DoStmt
DoBind Range
r Pattern
pat Expr
expr [LamClause]
cs
Maybe (Pattern, Range, Expr)
Nothing -> Expr -> [LamClause] -> Parser DoStmt
defaultBuildDoStmt Expr
e [LamClause]
cs
buildDoStmt Expr
e [LamClause]
cs = Expr -> [LamClause] -> Parser DoStmt
defaultBuildDoStmt Expr
e [LamClause]
cs
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
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
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
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
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
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
Arg ArgInfo
ai (Named Maybe NamedName
mn (Binder Maybe Pattern
mp (BName Name
n Fixity'
fix TacticAttribute
mtac Bool
fin)))
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Fixity' -> Bool
forall a. Null a => a -> Bool
null Fixity'
fix -> Parser (WithHiding Name)
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
fin -> Parser (WithHiding Name)
forall a. HasCallStack => a
__IMPOSSIBLE__
Arg ArgInfo
_ (Named Maybe NamedName
_ (Binder (Just Pattern
_) BoundName
_)) ->
[Char] -> Parser (WithHiding Name)
abort [Char]
"Arguments to pattern synonyms cannot be patterns themselves"
Arg ArgInfo
_ (Named Maybe NamedName
_ (Binder Maybe Pattern
_ (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"
Arg ArgInfo
ai (Named Maybe NamedName
mn (Binder Maybe Pattern
Nothing (BName Name
n Fixity'
_ TacticAttribute
_ Bool
_)))
| 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
ArgInfo Hiding
h (Modality Relevance
Relevant (Quantityω QωOrigin
_) Cohesion
Continuous) 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
ArgInfo Hiding
_ Modality
_ Origin
_ FreeVariables
_ (Annotation (IsLock LockOrigin
_)) ->
[Char] -> Parser (WithHiding Name)
abort ([Char] -> Parser (WithHiding Name))
-> [Char] -> Parser (WithHiding Name)
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
noAnn [Char]
"Lock"
ArgInfo Hiding
h (Modality Relevance
r Quantity
q Cohesion
c) 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"
| 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"
ArgInfo Hiding
_ Modality
_ Origin
_ (KnownFVs IntSet
_) Annotation
_ -> Parser (WithHiding Name)
forall a. HasCallStack => a
__IMPOSSIBLE__
ArgInfo Hiding
_ Modality
_ Origin
o FreeVariables
_ Annotation
_ | Origin
o Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
/= Origin
UserWritten -> Parser (WithHiding Name)
forall a. HasCallStack => a
__IMPOSSIBLE__
ArgInfo Hiding
_ Modality
_ Origin
_ FreeVariables
_ Annotation
_ -> Parser (WithHiding Name)
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise ->
[Char] -> Parser (WithHiding Name)
abort [Char]
"Arguments to pattern synonyms cannot be named"
mkLamClause
:: Bool
-> [Expr]
-> RHS
-> Parser LamClause
mkLamClause :: Bool -> [Expr] -> RHS -> Parser LamClause
mkLamClause Bool
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 :: Bool
lamCatchAll = Bool
catchAll }
mkAbsurdLamClause :: Bool -> List1 Expr -> Parser LamClause
mkAbsurdLamClause :: Bool -> List1 Expr -> Parser LamClause
mkAbsurdLamClause Bool
catchAll List1 Expr
es = Bool -> [Expr] -> RHS -> Parser LamClause
mkLamClause Bool
catchAll (List1 Expr -> [Item (List1 Expr)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Expr
es) RHS
forall e. RHS' e
AbsurdRHS
data RHSOrTypeSigs
= JustRHS RHS
| TypeSigsRHS Expr
deriving Int -> RHSOrTypeSigs -> [Char] -> [Char]
[RHSOrTypeSigs] -> [Char] -> [Char]
RHSOrTypeSigs -> [Char]
(Int -> RHSOrTypeSigs -> [Char] -> [Char])
-> (RHSOrTypeSigs -> [Char])
-> ([RHSOrTypeSigs] -> [Char] -> [Char])
-> Show RHSOrTypeSigs
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> RHSOrTypeSigs -> [Char] -> [Char]
showsPrec :: Int -> RHSOrTypeSigs -> [Char] -> [Char]
$cshow :: RHSOrTypeSigs -> [Char]
show :: RHSOrTypeSigs -> [Char]
$cshowList :: [RHSOrTypeSigs] -> [Char] -> [Char]
showList :: [RHSOrTypeSigs] -> [Char] -> [Char]
Show
patternToNames :: Pattern -> Parser (List1 (ArgInfo, Name))
patternToNames :: Pattern -> Parser (List1 (ArgInfo, Name))
patternToNames = \case
IdentP Bool
_ (QName Name
i) -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name)))
-> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
forall a b. (a -> b) -> a -> b
$ (ArgInfo, Name) -> List1 (ArgInfo, Name)
forall el coll. Singleton el coll => el -> coll
singleton ((ArgInfo, Name) -> List1 (ArgInfo, Name))
-> (ArgInfo, Name) -> List1 (ArgInfo, Name)
forall a b. (a -> b) -> a -> b
$ (ArgInfo
defaultArgInfo, Name
i)
WildP Range
r -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name)))
-> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
forall a b. (a -> b) -> a -> b
$ (ArgInfo, Name) -> List1 (ArgInfo, Name)
forall el coll. Singleton el coll => el -> coll
singleton ((ArgInfo, Name) -> List1 (ArgInfo, Name))
-> (ArgInfo, Name) -> List1 (ArgInfo, Name)
forall a b. (a -> b) -> a -> b
$ (ArgInfo
defaultArgInfo, Range -> Name
C.noName Range
r)
DotP Range
_ (Ident (QName Name
i)) -> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name)))
-> List1 (ArgInfo, Name) -> Parser (List1 (ArgInfo, Name))
forall a b. (a -> b) -> a -> b
$ (ArgInfo, Name) -> List1 (ArgInfo, Name)
forall el coll. Singleton el coll => el -> coll
singleton ((ArgInfo, Name) -> List1 (ArgInfo, Name))
-> (ArgInfo, Name) -> List1 (ArgInfo, Name)
forall a b. (a -> b) -> a -> b
$ (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo, Name
i)
RawAppP Range
_ List2 Pattern
ps -> NonEmpty (List1 (ArgInfo, Name)) -> List1 (ArgInfo, Name)
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty (List1 (ArgInfo, Name)) -> List1 (ArgInfo, Name))
-> (List2 (List1 (ArgInfo, Name))
-> NonEmpty (List1 (ArgInfo, Name)))
-> List2 (List1 (ArgInfo, Name))
-> List1 (ArgInfo, Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List2 (List1 (ArgInfo, Name)) -> NonEmpty (List1 (ArgInfo, Name))
forall a. List2 a -> List1 a
List2.toList1 (List2 (List1 (ArgInfo, Name)) -> List1 (ArgInfo, Name))
-> Parser (List2 (List1 (ArgInfo, Name)))
-> Parser (List1 (ArgInfo, Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern -> Parser (List1 (ArgInfo, Name)))
-> List2 Pattern -> Parser (List2 (List1 (ArgInfo, Name)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> List2 a -> m (List2 b)
mapM Pattern -> Parser (List1 (ArgInfo, Name))
patternToNames List2 Pattern
ps
Pattern
p -> [Char] -> Parser (List1 (ArgInfo, Name))
forall a. [Char] -> Parser a
parseError ([Char] -> Parser (List1 (ArgInfo, Name)))
-> [Char] -> Parser (List1 (ArgInfo, Name))
forall a b. (a -> b) -> a -> b
$
[Char]
"Illegal name in type signature: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pattern -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Pattern
p
funClauseOrTypeSigs :: [Attr] -> ([RewriteEqn] -> [WithExpr] -> LHS)
-> [Either RewriteEqn (List1 (Named Name Expr))]
-> RHSOrTypeSigs
-> WhereClause -> Parser (List1 Declaration)
funClauseOrTypeSigs :: [Attr]
-> ([RewriteEqn] -> [WithExpr] -> LHS)
-> [Either RewriteEqn (List1 (Named Name Expr))]
-> RHSOrTypeSigs
-> WhereClause
-> Parser (List1 Declaration)
funClauseOrTypeSigs [Attr]
attrs [RewriteEqn] -> [WithExpr] -> LHS
lhs' [Either RewriteEqn (List1 (Named Name Expr))]
with RHSOrTypeSigs
mrhs WhereClause
wh = do
(rs , es) <- [Either RewriteEqn (List1 (Named Name Expr))]
-> Parser ([RewriteEqn], [Named Name Expr])
buildWithBlock [Either RewriteEqn (List1 (Named Name Expr))]
with
let lhs = [RewriteEqn] -> [WithExpr] -> LHS
lhs' [RewriteEqn]
rs ((Named Name Expr -> WithExpr) -> [Named Name Expr] -> [WithExpr]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Arg Expr) -> Named Name Expr -> WithExpr
forall a b. (a -> b) -> Named Name a -> Named Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Arg Expr
observeModifiers) [Named Name Expr]
es)
case mrhs of
JustRHS RHS
rhs -> do
Bool -> Parser () -> Parser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Attr] -> Bool
forall a. Null a => a -> Bool
null [Attr]
attrs) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ [Attr] -> [Char] -> Parser ()
forall r a. HasRange r => r -> [Char] -> Parser a
parseErrorRange [Attr]
attrs ([Char] -> Parser ()) -> [Char] -> Parser ()
forall a b. (a -> b) -> a -> b
$ [Char]
"A function clause cannot have attributes"
List1 Declaration -> Parser (List1 Declaration)
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (List1 Declaration -> Parser (List1 Declaration))
-> List1 Declaration -> Parser (List1 Declaration)
forall a b. (a -> b) -> a -> b
$ Declaration -> List1 Declaration
forall el coll. Singleton el coll => el -> coll
singleton (Declaration -> List1 Declaration)
-> Declaration -> List1 Declaration
forall a b. (a -> b) -> a -> b
$ LHS -> RHS -> WhereClause -> Bool -> Declaration
FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
False
TypeSigsRHS Expr
e -> case WhereClause
wh of
WhereClause
NoWhere -> case LHS
lhs of
LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_ | Pattern -> Bool
forall a. HasEllipsis a => a -> Bool
hasEllipsis Pattern
p -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"The ellipsis ... cannot have a type signature"
LHS Pattern
_ [RewriteEqn]
_ (WithExpr
_:[WithExpr]
_) -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"Illegal: with in type signature"
LHS Pattern
_ (RewriteEqn
_:[RewriteEqn]
_) [WithExpr]
_ -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"Illegal: rewrite in type signature"
LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_ | Pattern -> Bool
forall p. CPatternLike p => p -> Bool
hasWithPatterns Pattern
p -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"Illegal: with patterns in type signature"
LHS Pattern
p [] [] -> Parser (List1 (ArgInfo, Name))
-> ((ArgInfo, Name) -> Parser Declaration)
-> Parser (List1 Declaration)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM (Pattern -> Parser (List1 (ArgInfo, Name))
patternToNames Pattern
p) (((ArgInfo, Name) -> Parser Declaration)
-> Parser (List1 Declaration))
-> ((ArgInfo, Name) -> Parser Declaration)
-> Parser (List1 Declaration)
forall a b. (a -> b) -> a -> b
$ \ (ArgInfo
info, Name
x) -> do
info <- [Attr] -> ArgInfo -> Parser ArgInfo
forall a. LensAttribute a => [Attr] -> a -> Parser a
applyAttrs [Attr]
attrs ArgInfo
info
return $ typeSig info (getTacticAttr attrs) x e
WhereClause
_ -> [Char] -> Parser (List1 Declaration)
forall a. [Char] -> Parser a
parseError [Char]
"A type signature cannot have a where clause"
typeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
typeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
typeSig ArgInfo
i TacticAttribute
tac Name
n Expr
e = ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
i TacticAttribute
tac Name
n (Expr -> Expr
Generalized Expr
e)
data Attr = Attr
{ Attr -> Range
attrRange :: Range
, Attr -> [Char]
attrName :: String
, Attr -> Attribute
theAttr :: Attribute
}
instance HasRange Attr where
getRange :: Attr -> Range
getRange = Attr -> Range
attrRange
instance SetRange Attr where
setRange :: Range -> Attr -> Attr
setRange Range
r (Attr Range
_ [Char]
x Attribute
a) = Range -> [Char] -> Attribute -> Attr
Attr Range
r [Char]
x Attribute
a
toAttribute :: Range -> Expr -> Parser Attr
toAttribute :: Range -> Expr -> Parser Attr
toAttribute Range
r Expr
e = do
attr <- Parser Attr
-> (Attribute -> Parser Attr) -> Maybe Attribute -> Parser Attr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Parser Attr
failure (Attr -> Parser Attr
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (Attr -> Parser Attr)
-> (Attribute -> Attr) -> Attribute -> Parser Attr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> [Char] -> Attribute -> Attr
Attr Range
r [Char]
s) (Maybe Attribute -> Parser Attr) -> Maybe Attribute -> Parser Attr
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Attribute
exprToAttribute Expr
e
modify' (\ ParseState
st -> ParseState
st{ parseAttributes = (theAttr attr, r, s) : parseAttributes st })
return attr
where
s :: [Char]
s = Expr -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Expr
e
failure :: Parser Attr
failure = Expr -> [Char] -> Parser Attr
forall r a. HasRange r => r -> [Char] -> Parser a
parseErrorRange Expr
e ([Char] -> Parser Attr) -> [Char] -> Parser Attr
forall a b. (a -> b) -> a -> b
$ [Char]
"Unknown attribute: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
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
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
setTacticAttr :: List1 Attr -> NamedArg Binder -> NamedArg Binder
setTacticAttr :: List1 Attr -> NamedArg Binder -> NamedArg Binder
setTacticAttr List1 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] -> TacticAttribute) -> [Attr] -> TacticAttribute
forall a b. (a -> b) -> a -> b
$ List1 Attr -> [Item (List1 Attr)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Attr
as of
TacticAttribute
t | TacticAttribute -> Bool
forall a. Null a => a -> Bool
null TacticAttribute
t -> BoundName
b
| Bool
otherwise -> BoundName
b { bnameTactic = t }
getTacticAttr :: [Attr] -> TacticAttribute
getTacticAttr :: [Attr] -> TacticAttribute
getTacticAttr [Attr]
as = Maybe (Ranged Expr) -> TacticAttribute
forall a. Maybe (Ranged a) -> TacticAttribute' a
C.TacticAttribute (Maybe (Ranged Expr) -> TacticAttribute)
-> Maybe (Ranged Expr) -> TacticAttribute
forall a b. (a -> b) -> a -> b
$
case [Attribute] -> [Attribute]
tacticAttributes [ Attribute
a | Attr Range
_ [Char]
_ Attribute
a <- [Attr]
as ] of
[CA.TacticAttribute Ranged Expr
e] -> Ranged Expr -> Maybe (Ranged Expr)
forall a. a -> Maybe a
Just Ranged Expr
e
[] -> Maybe (Ranged Expr)
forall a. Maybe a
Nothing
[Attribute]
_ -> Maybe (Ranged Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
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
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]
attrName Attr
a
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]
attrName [Attr]
as)