ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Parser.Helpers

Utility functions used in the Happy parser.

Contents

Relevance
Attributes

Synopsis

value takeOptionsPragmas
value figureOutTopLevelModule
value mkName'
value mkValidName
value mkName
value mkQName
value mkDomainFree_
value mkRString
value mkRText
value pragmaQName
value mkNamedArg
value parsePolarity
value recoverLayout
value ensureUnqual
data LamBinds'
type LamBinds
value mkAbsurdBinding
value mkLamBinds
value forallPi
value addType
value onlyErased
value extLam
value extOrAbsLam
value exprAsNamesAndPatterns
value exprAsNameAndPattern
value exprAsNameOrHiddenNames
value boundNamesOrAbsurd
value exprToAssignment
value buildWithBlock
value buildWithStmt
value buildUsingStmt
value buildSingleWithStmt
value defaultBuildDoStmt
value buildDoStmt
value exprToLHS
value exprToPattern
value exprToName
value maybeNamed
value patternSynArgs
value mkLamClause
value mkAbsurdLamClause
data RHSOrTypeSigs
value patternToNames
value funClauseOrTypeSigs
value typeSig
value makeIrrelevant
value makeShapeIrrelevant
value defaultIrrelevantArg
value defaultShapeIrrelevantArg
value makeIrrelevantM
value makeShapeIrrelevantM
value assertPristineRelevance
value toAttribute
value applyAttr
value applyAttrs
value applyAttrs1
value setTacticAttr
value getTacticAttr
value checkForUniqueAttribute
value errorConflictingAttribute
value errorConflictingAttributes
value prettyAttr
value applyAttributes

PackageAgda-2.8.0.2
Exports63
LanguageHaskell2010
LicenceMIT
SourceHelpers.hs

valuetakeOptionsPragmas :: [Declaration] -> Module

Source#

Grab leading OPTIONS pragmas.

valuefigureOutTopLevelModule :: [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).

valuemkName' :: Bool -> (Interval, String) -> Parser Name

Source#

Create a name from a string. The boolean indicates whether a part of the name can be token constructor.

valuemkValidName :: Bool -> Range -> String -> Either String Name

Source#

Create a name from a string. The boolean indicates whether a part of the name can be token constructor.

valuemkName :: (Interval, String) -> Parser Name

Source#

Create a name from a string

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

Source#

Create a qualified name from a list of strings

valuemkDomainFree_

valuemkRString :: (Interval, String) -> RString

valuemkRText :: (Interval, String) -> Ranged Text

valuepragmaQName :: (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!

valuemkNamedArg

valueparsePolarity :: (Interval, String) -> Parser (Ranged Occurrence)

Source#

Polarity parser.

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

valueensureUnqual :: QName -> Parser Name

datadata LamBinds' a

Source#

Result of parsing LamBinds.

Constructors

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

Instances1Functor

Functor LamBinds'Defined in Agda-2.8.0.2 · Agda.Syntax.Parser.Helpers

typetype LamBinds = LamBinds' [LamBinding]

valuemkAbsurdBinding :: Hiding -> LamBinds

valuemkLamBinds :: a -> LamBinds' a

valueforallPi :: List1 LamBinding -> Expr -> Expr

Source#

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

valueaddType :: LamBinding -> TypedBinding

Source#

Converts lambda bindings to typed bindings.

valueonlyErased

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

Source#

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.

valueextLam

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

Source#

Constructs extended lambdas.

valueextOrAbsLam

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

Source#

Constructs extended or absurd lambdas.

valueexprAsNamesAndPatterns :: Expr -> Maybe (List1 (Name, Maybe Expr))

Source#

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

valueexprAsNameAndPattern :: Expr -> Maybe (Name, Maybe Expr)

valueexprAsNameOrHiddenNames

:: Expr
-> Maybe (List1 (NamedArg (Name, Maybe Expr)))

valueboundNamesOrAbsurd

:: List1 Expr
-> Parser (Either (List1 (NamedArg Binder)) (List1 Expr))

valueexprToAssignment :: Expr -> Parser (Maybe (Pattern, Range, Expr))

Source#

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

valuebuildWithBlock

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

Source#

Build a with-block

valuebuildWithStmt

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

Source#

Build a with-statement

valuebuildUsingStmt :: List1 Expr -> Parser RewriteEqn

valuebuildSingleWithStmt

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

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

Source#

Build a do-statement

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

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

Source#

Turn an expression into a left hand side.

valueexprToPattern :: Expr -> Parser Pattern

Source#

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

valueexprToName :: Expr -> Parser Name

Source#

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

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

valuepatternSynArgs :: [NamedArg Binder] -> Parser [WithHiding Name]

valuemkLamClause

:: Catchall
-> [Expr]
Possibly empty list of patterns.
-> RHS
-> Parser LamClause

valuemkAbsurdLamClause :: Catchall -> List1 Expr -> Parser LamClause

datadata RHSOrTypeSigs

Constructors

JustRHS RHS
TypeSigsRHS Expr

Instances1Show

Show RHSOrTypeSigsDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Helpers

valuepatternToNames :: Pattern -> Parser (List1 (ArgInfo, Name))

valuefunClauseOrTypeSigs

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

valuetypeSig :: ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration

Relevance

valuemakeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b

valuemakeShapeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b

valuedefaultIrrelevantArg :: HasRange a => a -> b -> Arg b

valuedefaultShapeIrrelevantArg :: HasRange a => a -> b -> Arg b

valuemakeIrrelevantM :: (HasRange a, LensRelevance b) => a -> b -> Parser b

valuemakeShapeIrrelevantM :: (HasRange a, LensRelevance b) => a -> b -> Parser b

valueassertPristineRelevance

:: (HasRange a, LensRelevance b)
=> a
-> b
-> Parser ()

Attributes

valuetoAttribute :: Range -> Expr -> Parser (Maybe Attr)

Source#

Parse an attribute.

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

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