| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Parser.Helpers
Contents
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
- patternToNames :: Pattern -> Parser (List1 (Arg Name))
- patternToArgPattern :: Pattern -> Arg Pattern
- 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
- applyAttrsDropTactic :: 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
- haveTacticAttr :: [Attr] -> Maybe (Ranged Expr)
- 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.
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 #
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!
parsePolarity :: (Interval, String) -> Parser (Ranged Occurrence) Source #
Polarity parser.
Result of parsing LamBinds.
Constructors
| LamBinds | |
Fields
| |
type LamBinds = LamBinds' [LamBinding] Source #
mkAbsurdBinding :: Hiding -> LamBinds Source #
mkLamBinds :: a -> LamBinds' a Source #
addType :: LamBinding -> TypedBinding Source #
Converts lambda bindings to typed bindings.
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.
Arguments
| :: Range | The range of the lambda symbol and |
| -> [Attr] | The attributes in reverse order. |
| -> List1 LamClause | The clauses in reverse order. |
| -> Parser Expr |
Constructs extended lambdas.
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
buildUsingStmt :: List1 Expr -> Parser RewriteEqn Source #
buildSingleWithStmt :: Named Name Expr -> Parser (Either (Named Name (Pattern, Expr)) (Named Name Expr)) 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 #
data RHSOrTypeSigs Source #
Constructors
| JustRHS RHS | |
| TypeSigsRHS Expr |
Instances
| Show RHSOrTypeSigs Source # | |
Defined in Agda.Syntax.Parser.Helpers Methods showsPrec :: Int -> RHSOrTypeSigs -> ShowS # show :: RHSOrTypeSigs -> String # showList :: [RHSOrTypeSigs] -> ShowS # | |
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
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.
applyAttrsDropTactic :: 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.
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 #