Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.Helpers

Contents

- Relevance
- Attributes

Description

Utility functions used in the Happy parser.

Synopsis

- takeOptionsPragmas :: [Declaration] -> Module
- figureOutTopLevelModule :: [Declaration] -> [Declaration]
- mkName' :: Bool -> (Interval, String) -> Parser Name
- mkValidName :: Bool -> Range -> String -> Either String Name
- mkName :: (Interval, String) -> Parser Name
- mkQName :: [(Interval, String)] -> Parser QName
- mkDomainFree_ :: (NamedArg Binder -> NamedArg Binder) -> Maybe Pattern -> Name -> NamedArg Binder
- mkRString :: (Interval, String) -> RString
- mkRText :: (Interval, String) -> Ranged Text
- pragmaQName :: (Interval, String) -> Parser QName
- mkNamedArg :: Maybe QName -> Either QName Range -> Parser (NamedArg BoundName)
- parsePolarity :: (Interval, String) -> Parser (Ranged 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 :: Catchall -> [Expr] -> RHS -> Parser LamClause
- mkAbsurdLamClause :: Catchall -> 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
- makeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b
- makeShapeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b
- defaultIrrelevantArg :: HasRange a => a -> b -> Arg b
- defaultShapeIrrelevantArg :: HasRange a => a -> b -> Arg b
- makeIrrelevantM :: (HasRange a, LensRelevance b) => a -> b -> Parser b
- makeShapeIrrelevantM :: (HasRange a, LensRelevance b) => a -> b -> Parser b
- assertPristineRelevance :: (HasRange a, LensRelevance b) => a -> b -> Parser ()
- toAttribute :: Range -> Expr -> Parser (Maybe Attr)
- applyAttr :: LensAttribute a => Attr -> a -> Parser a
- applyAttrs :: LensAttribute a => [Attr] -> a -> Parser a
- applyAttrs1 :: LensAttribute a => List1 Attr -> a -> Parser a
- setTacticAttr :: [Attr] -> NamedArg Binder -> NamedArg Binder
- getTacticAttr :: [Attr] -> TacticAttribute
- checkForUniqueAttribute :: (Attribute -> Bool) -> [Attr] -> Parser ()
- errorConflictingAttribute :: Attr -> Parser a
- errorConflictingAttributes :: [Attr] -> Parser a
- prettyAttr :: Attr -> String
- applyAttributes :: Functor f => [Attr] -> ArgInfo -> f (NamedArg Binder) -> Parser (f (NamedArg Binder))

# 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' :: 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`.

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

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 #

mkRText :: (Interval, String) -> Ranged Text 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 #

parsePolarity :: (Interval, String) -> Parser (Ranged 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 Source # (<$) :: a -> LamBinds' b -> LamBinds' a Source #

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

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

mkAbsurdLamClause :: Catchall -> 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 Source # show :: RHSOrTypeSigs -> String Source # showList :: [RHSOrTypeSigs] -> ShowS Source #

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 #

# Relevance

makeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b Source #

makeShapeIrrelevant :: (HasRange a, LensRelevance b) => a -> b -> b Source #

defaultIrrelevantArg :: HasRange a => a -> b -> Arg b Source #

defaultShapeIrrelevantArg :: HasRange a => a -> b -> Arg b Source #

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

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

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

# Attributes

toAttribute :: Range -> Expr -> Parser (Maybe 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 :: [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.

prettyAttr :: Attr -> String Source #

applyAttributes Source #

Arguments

:: Functor f |
=> [Attr] | Can contain `tactic` attribute.
-> ArgInfo | If the attributes to be set are not at default value here, crash.
-> f (NamedArg Binder) | Binders to apply attributes to.
-> Parser (f (NamedArg Binder)) | Binders with attributes applied.

Apply some attributes to some binders.