Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Parser.Helpers

Contents

Attributes

Description

Utility functions used in the Happy parser.

Synopsis

takeOptionsPragmas :: [Declaration] -> Module
figureOutTopLevelModule :: [Declaration] -> [Declaration]
mkName :: (Interval, String) -> Parser Name
mkQName :: [(Interval, String)] -> Parser QName
mkDomainFree_ :: (NamedArg Binder -> NamedArg Binder) -> Maybe Pattern -> Name -> NamedArg Binder
mkRString :: (Interval, String) -> RString
pragmaQName :: (Interval, String) -> Parser QName
mkNamedArg :: Maybe QName -> Either QName Range -> Parser (NamedArg BoundName)
polarity :: (Interval, String) -> Parser (Range, Occurrence)
recoverLayout :: [(Interval, String)] -> String
ensureUnqual :: QName -> Parser Name
data LamBinds' a = LamBinds {
- lamBindings :: a
- absurdBinding :: Maybe Hiding
}
type LamBinds = LamBinds' [LamBinding]
mkAbsurdBinding :: Hiding -> LamBinds
mkLamBinds :: a -> LamBinds' a
forallPi :: List1 LamBinding -> Expr -> Expr
addType :: LamBinding -> TypedBinding
onlyErased :: [Attr] -> Parser Erased
extLam :: Range -> [Attr] -> List1 LamClause -> Parser Expr
extOrAbsLam :: Range -> [Attr] -> Either ([LamBinding], Hiding) (List1 Expr) -> Parser Expr
exprAsNamesAndPatterns :: Expr -> Maybe (List1 (Name, Maybe Expr))
exprAsNameAndPattern :: Expr -> Maybe (Name, Maybe Expr)
exprAsNameOrHiddenNames :: Expr -> Maybe (List1 (NamedArg (Name, Maybe Expr)))
boundNamesOrAbsurd :: List1 Expr -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))
exprToAssignment :: Expr -> Parser (Maybe (Pattern, Range, Expr))
buildWithBlock :: [Either RewriteEqn (List1 (Named Name Expr))] -> Parser ([RewriteEqn], [Named Name Expr])
buildWithStmt :: List1 (Named Name Expr) -> Parser [Either RewriteEqn (List1 (Named Name Expr))]
buildUsingStmt :: List1 Expr -> Parser RewriteEqn
buildSingleWithStmt :: Named Name Expr -> Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr))
defaultBuildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt
exprToLHS :: Expr -> Parser ([RewriteEqn] -> [WithExpr] -> LHS)
exprToPattern :: Expr -> Parser Pattern
exprToName :: Expr -> Parser Name
maybeNamed :: Expr -> Parser (Named_ Expr)
patternSynArgs :: [NamedArg Binder] -> Parser [WithHiding Name]
mkLamClause :: Bool -> [Expr] -> RHS -> Parser LamClause
mkAbsurdLamClause :: Bool -> List1 Expr -> Parser LamClause
data RHSOrTypeSigs
- = JustRHS RHS
- | TypeSigsRHS Expr
patternToNames :: Pattern -> Parser (List1 (ArgInfo, Name))
funClauseOrTypeSigs :: [Attr] -> ([RewriteEqn] -> [WithExpr] -> LHS) -> [Either RewriteEqn (List1 (Named Name Expr))] -> RHSOrTypeSigs -> WhereClause -> Parser (List1 Declaration)
typeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
data Attr = Attr {
- attrRange :: Range
- attrName :: String
- theAttr :: Attribute
}
toAttribute :: Range -> Expr -> Parser Attr
applyAttr :: LensAttribute a => Attr -> a -> Parser a
applyAttrs :: LensAttribute a => [Attr] -> a -> Parser a
applyAttrs1 :: LensAttribute a => List1 Attr -> a -> Parser a
setTacticAttr :: List1 Attr -> NamedArg Binder -> NamedArg Binder
getTacticAttr :: [Attr] -> TacticAttribute
checkForUniqueAttribute :: (Attribute -> Bool) -> [Attr] -> Parser ()
errorConflictingAttribute :: Attr -> Parser a
errorConflictingAttributes :: [Attr] -> Parser a

Documentation

takeOptionsPragmas :: [Declaration] -> Module Source #

Grab leading OPTIONS pragmas.

figureOutTopLevelModule :: [Declaration] -> [Declaration] Source #

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).

mkName :: (Interval, String) -> Parser Name Source #

Create a name from a string.

mkQName :: [(Interval, String)] -> Parser QName Source #

Create a qualified name from a list of strings

mkDomainFree_ :: (NamedArg Binder -> NamedArg Binder) -> Maybe Pattern -> Name -> NamedArg Binder Source #

mkRString :: (Interval, String) -> RString Source #

pragmaQName :: (Interval, String) -> Parser QName Source #

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

mkNamedArg :: Maybe QName -> Either QName Range -> Parser (NamedArg BoundName) Source #

polarity :: (Interval, String) -> Parser (Range, Occurrence) Source #

Polarity parser.

recoverLayout :: [(Interval, String)] -> String Source #

ensureUnqual :: QName -> Parser Name Source #

data LamBinds' a Source #

Result of parsing LamBinds.

Constructors

LamBinds
Fields lamBindings :: a A number of domain-free or typed bindings or record patterns. absurdBinding :: Maybe Hiding Followed by possibly a final absurd pattern.

Instances

Instances details

Functor LamBinds' Source #
Instance details Defined in Agda.Syntax.Parser.Helpers Methods fmap :: (a -> b) -> LamBinds' a -> LamBinds' b (<$) :: a -> LamBinds' b -> LamBinds' a #

type LamBinds = LamBinds' [LamBinding] Source #

mkAbsurdBinding :: Hiding -> LamBinds Source #

mkLamBinds :: a -> LamBinds' a Source #

forallPi :: List1 LamBinding -> Expr -> Expr Source #

Build a forall pi (forall x y z -> ...)

addType :: LamBinding -> TypedBinding Source #

Converts lambda bindings to typed bindings.

onlyErased Source #

Arguments

:: [Attr]	The attributes, in reverse order.
-> Parser Erased

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.

extLam Source #

Arguments

:: 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

Constructs extended lambdas.

extOrAbsLam Source #

Arguments

:: Range	The range of the lambda symbol.
-> [Attr]	The attributes, in reverse order.
-> Either ([LamBinding], Hiding) (List1 Expr)
-> Parser Expr

Constructs extended or absurd lambdas.

exprAsNamesAndPatterns :: Expr -> Maybe (List1 (Name, Maybe Expr)) Source #

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

exprAsNameAndPattern :: Expr -> Maybe (Name, Maybe Expr) Source #

exprAsNameOrHiddenNames :: Expr -> Maybe (List1 (NamedArg (Name, Maybe Expr))) Source #

boundNamesOrAbsurd :: List1 Expr -> Parser (Either (List1 (NamedArg Binder)) (List1 Expr)) Source #

exprToAssignment :: Expr -> Parser (Maybe (Pattern, Range, Expr)) Source #

Match a pattern-matching "assignment" statement p <- e

buildWithBlock :: [Either RewriteEqn (List1 (Named Name Expr))] -> Parser ([RewriteEqn], [Named Name Expr]) Source #

Build a with-block

buildWithStmt :: List1 (Named Name Expr) -> Parser [Either RewriteEqn (List1 (Named Name Expr))] Source #

Build a with-statement

buildUsingStmt :: List1 Expr -> Parser RewriteEqn Source #

buildSingleWithStmt :: Named Name Expr -> Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr)) Source #

defaultBuildDoStmt :: Expr -> [LamClause] -> Parser DoStmt Source #

Build a do-statement

buildDoStmt :: Expr -> [LamClause] -> Parser DoStmt Source #

exprToLHS :: Expr -> Parser ([RewriteEqn] -> [WithExpr] -> LHS) Source #

Turn an expression into a left hand side.

exprToPattern :: Expr -> Parser Pattern Source #

Turn an expression into a pattern. Fails if the expression is not a valid pattern.

exprToName :: Expr -> Parser Name Source #

Turn an expression into a name. Fails if the expression is not a valid identifier.

maybeNamed :: Expr -> Parser (Named_ Expr) Source #

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).

patternSynArgs :: [NamedArg Binder] -> Parser [WithHiding Name] Source #

mkLamClause Source #

Arguments

:: Bool	Catch-all?
-> [Expr]	Possibly empty list of patterns.
-> RHS
-> Parser LamClause

mkAbsurdLamClause :: Bool -> List1 Expr -> Parser LamClause Source #

data RHSOrTypeSigs Source #

Constructors

JustRHS RHS
TypeSigsRHS Expr

Instances

Instances details

Show RHSOrTypeSigs Source #
Instance details Defined in Agda.Syntax.Parser.Helpers Methods showsPrec :: Int -> RHSOrTypeSigs -> ShowS show :: RHSOrTypeSigs -> String showList :: [RHSOrTypeSigs] -> ShowS

patternToNames :: Pattern -> Parser (List1 (ArgInfo, Name)) Source #

funClauseOrTypeSigs :: [Attr] -> ([RewriteEqn] -> [WithExpr] -> LHS) -> [Either RewriteEqn (List1 (Named Name Expr))] -> RHSOrTypeSigs -> WhereClause -> Parser (List1 Declaration) Source #

typeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration Source #

Attributes

data Attr Source #

Parsed attribute.

Constructors

Attr
Fields attrRange :: Range Range includes the @. attrName :: String Concrete, user written attribute for error reporting. theAttr :: Attribute Parsed attribute.

Instances

Instances details

HasRange Attr Source #
Instance details Defined in Agda.Syntax.Parser.Helpers Methods getRange :: Attr -> Range Source #
SetRange Attr Source #
Instance details Defined in Agda.Syntax.Parser.Helpers Methods setRange :: Range -> Attr -> Attr Source #

toAttribute :: Range -> Expr -> Parser Attr Source #

Parse an attribute.

applyAttr :: LensAttribute a => Attr -> a -> Parser a Source #

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.

applyAttrs :: LensAttribute a => [Attr] -> a -> Parser a Source #

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.

applyAttrs1 :: LensAttribute a => List1 Attr -> a -> Parser a Source #

setTacticAttr :: List1 Attr -> NamedArg Binder -> NamedArg Binder Source #

Set the tactic attribute of a binder

getTacticAttr :: [Attr] -> TacticAttribute Source #

Get the tactic attribute if present.

checkForUniqueAttribute :: (Attribute -> Bool) -> [Attr] -> Parser () Source #

Report a parse error if two attributes in the list are of the same kind, thus, present conflicting information.

errorConflictingAttribute :: Attr -> Parser a Source #

Report an attribute as conflicting (e.g., with an already set value).

errorConflictingAttributes :: [Attr] -> Parser a Source #

Report attributes as conflicting (e.g., with each other). Precondition: List not emtpy.