Agda.Syntax.Parser.Helpers

Utility functions used in the Happy parser.

Documentation

takeOptionsPragmas :: [Declaration] -> Module

Grab leading OPTIONS pragmas.

figureOutTopLevelModule :: [Declaration] -> [Declaration]

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

Create a name from a string.

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

Create a qualified name from a list of strings

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

mkRString :: (Interval, String) -> RString

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

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)

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

Polarity parser.

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

ensureUnqual :: QName -> Parser Name

data LamBinds' a

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

Functor LamBinds'

Defined in Agda.Syntax.Parser.Helpers

Methods

fmap :: (a -> b) -> LamBinds' a -> LamBinds' b

(<$) :: a -> LamBinds' b -> LamBinds' a

type LamBinds = LamBinds' [LamBinding]

mkAbsurdBinding :: Hiding -> LamBinds

mkLamBinds :: a -> LamBinds' a

forallPi :: List1 LamBinding -> Expr -> Expr

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

addType :: LamBinding -> TypedBinding

Converts lambda bindings to typed bindings.

onlyErased

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

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

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

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

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

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

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

Build a with-block

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

Build a with-statement

buildUsingStmt :: List1 Expr -> Parser RewriteEqn

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

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

Build a do-statement

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

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

Turn an expression into a left hand side.

exprToPattern :: Expr -> Parser Pattern

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

exprToName :: Expr -> Parser Name

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

maybeNamed :: Expr -> Parser (Named_ Expr)

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]

mkLamClause

Arguments

:: Bool

Catch-all?

-> [Expr]

Possibly empty list of patterns.

-> RHS

-> Parser LamClause

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

data RHSOrTypeSigs

Constructors

JustRHS RHS

TypeSigsRHS Expr

Instances

Show RHSOrTypeSigs

Defined in Agda.Syntax.Parser.Helpers

Methods

showsPrec :: Int -> RHSOrTypeSigs -> ShowS

show :: RHSOrTypeSigs -> String

showList :: [RHSOrTypeSigs] -> ShowS

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

Attributes

data Attr

Parsed attribute.

Constructors

Attr

Fields

• attrRange :: Range

  Range includes the @.

• attrName :: String

  Concrete, user written attribute for error reporting.

• theAttr :: Attribute

  Parsed attribute.

Instances

HasRange Attr

Defined in Agda.Syntax.Parser.Helpers

Methods

getRange :: Attr -> Range

SetRange Attr

Defined in Agda.Syntax.Parser.Helpers

Methods

setRange :: Range -> Attr -> Attr

toAttribute :: Range -> Expr -> Parser Attr

Parse an attribute.

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

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

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

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

Set the tactic attribute of a binder

getTacticAttr :: [Attr] -> TacticAttribute

Get the tactic attribute if present.

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

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

errorConflictingAttribute :: Attr -> Parser a

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

errorConflictingAttributes :: [Attr] -> Parser a

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