Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Parser.Helpers

Contents

Description

Utility functions used in the Happy parser.

Synopsis

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

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!

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

Polarity parser.

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

data LamBinds' a Source #

Result of parsing LamBinds.

Constructors

LamBinds 

Fields

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 #

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

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

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

Build a do-statement

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

mkLamClause Source #

Arguments

:: Bool

Catch-all?

-> [Expr]

Possibly empty list of patterns.

-> RHS 
-> Parser LamClause 

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

Attributes

data Attr Source #

Parsed attribute.

Constructors

Attr 

Fields

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.

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.