ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Parser.Helpers

Utility functions used in the Happy parser.

4 types
48 values

PackageAgda-2.7.0.1
Exports52
LanguageHaskell2010
LicenceMIT
SourceHelpers.hs

valuetakeOptionsPragmas :: [Declaration] -> Module

Grab leading OPTIONS pragmas.

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

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

Create a name from a string.

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

Create a qualified name from a list of strings

valuemkDomainFree_

valuemkRString :: (Interval, String) -> RString

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

valuemkNamedArg

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

Polarity parser.

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

valueensureUnqual :: QName -> Parser Name

datadata LamBinds' a

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.7.0.1 · Agda.Syntax.Parser.Helpers

typetype LamBinds = LamBinds' [LamBinding]

valuemkAbsurdBinding :: Hiding -> LamBinds

valuemkLamBinds :: a -> LamBinds' a

valueforallPi :: List1 LamBinding -> Expr -> Expr

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

valueaddType :: LamBinding -> TypedBinding

Converts lambda bindings to typed bindings.

valueonlyErased

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

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

Constructs extended lambdas.

valueextOrAbsLam

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

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

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

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

valuebuildWithBlock

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

Build a with-block

valuebuildWithStmt

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

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

Build a do-statement

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

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

Turn an expression into a left hand side.

valueexprToPattern :: Expr -> Parser Pattern

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

valueexprToName :: Expr -> Parser Name

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

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

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

valuemkLamClause

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

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

datadata RHSOrTypeSigs

Constructors

JustRHS RHS
TypeSigsRHS Expr

Instances1Show

Show RHSOrTypeSigsDefined in Agda-2.7.0.1 · 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

Attributes

10 declarations

datadata Attr

Parsed attribute.

Constructors

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

Instances2HasRange, SetRange

HasRange AttrDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Helpers
SetRange AttrDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Helpers

valuetoAttribute :: Range -> Expr -> Parser Attr

Parse an attribute.

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

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

valueapplyAttrs1 :: LensAttribute a => List1 Attr -> a -> Parser a

valuesetTacticAttr :: List1 Attr -> NamedArg Binder -> NamedArg Binder

Set the tactic attribute of a binder

valuegetTacticAttr :: [Attr] -> TacticAttribute

Get the tactic attribute if present.

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

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

valueerrorConflictingAttribute :: Attr -> Parser a

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

valueerrorConflictingAttributes :: [Attr] -> Parser a

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