Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Abstract

Contents

Patterns

Description

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

Synopsis

Documentation

newtype BindName Source #

Constructors

BindName
Fields unBind :: Name

Instances

Eq BindName Source #
Methods (==) :: BindName -> BindName -> Bool # (/=) :: BindName -> BindName -> Bool #
Data BindName Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindName -> c BindName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindName # toConstr :: BindName -> Constr # dataTypeOf :: BindName -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BindName) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindName) # gmapT :: (forall b. Data b => b -> b) -> BindName -> BindName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r # gmapQ :: (forall d. Data d => d -> u) -> BindName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BindName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindName -> m BindName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName #
Ord BindName Source #
Methods compare :: BindName -> BindName -> Ordering # (<) :: BindName -> BindName -> Bool # (<=) :: BindName -> BindName -> Bool # (>) :: BindName -> BindName -> Bool # (>=) :: BindName -> BindName -> Bool # max :: BindName -> BindName -> BindName # min :: BindName -> BindName -> BindName #
Show BindName Source #
Methods showsPrec :: Int -> BindName -> ShowS # show :: BindName -> String # showList :: [BindName] -> ShowS #
KillRange BindName Source #
Methods killRange :: KillRangeT BindName Source #
SetRange BindName Source #
Methods setRange :: Range -> BindName -> BindName Source #
HasRange BindName Source #
Methods getRange :: BindName -> Range Source #
ToConcrete BindName Name Source #
Methods toConcrete :: BindName -> AbsToCon Name Source # bindToConcrete :: BindName -> (Name -> AbsToCon b) -> AbsToCon b Source #

type Args = [NamedArg Expr] Source #

data Expr Source #

Expressions after scope checking (operators parsed, names resolved).

Constructors

Var Name	Bound variable.
Def QName	Constant: axiom, function, data or record type.
Proj ProjOrigin AmbiguousQName	Projection (overloaded).
Con AmbiguousQName	Constructor (overloaded).
PatternSyn AmbiguousQName	Pattern synonym.
Macro QName	Macro.
Lit Literal	Literal.
QuestionMark MetaInfo InteractionId	Meta variable for interaction. The `InteractionId` is usually identical with the `metaNumber` of `MetaInfo`. However, if you want to print an interaction meta as just `?` instead of `?n`, you should set the `metaNumber` to `Nothing` while keeping the `InteractionId`.
Underscore MetaInfo	Meta variable for hidden argument (must be inferred locally).
Dot ExprInfo Expr	`.e`, for postfix projection.
App AppInfo Expr (NamedArg Expr)	Ordinary (binary) application.
WithApp ExprInfo Expr [Expr]	With application.
Lam ExprInfo LamBinding Expr	`λ bs → e`.
AbsurdLam ExprInfo Hiding	`λ()` or `λ{}`.
ExtendedLam ExprInfo DefInfo QName [Clause]
Pi ExprInfo Telescope Expr	Dependent function space `Γ → A`.
Fun ExprInfo (Arg Expr) Expr	Non-dependent function space.
Set ExprInfo Integer	`Set`, `Set1`, `Set2`, ...
Prop ExprInfo	`Prop` (no longer supported, used as dummy type).
Let ExprInfo [LetBinding] Expr	`let bs in e`.
ETel Telescope	Only used when printing telescopes.
Rec ExprInfo RecordAssigns	Record construction.
RecUpdate ExprInfo Expr Assigns	Record update.
ScopedExpr ScopeInfo Expr	Scope annotation.
QuoteGoal ExprInfo Name Expr	Binds `Name` to current type in `Expr`.
QuoteContext ExprInfo	Returns the current context.
Quote ExprInfo	Quote an identifier `QName`.
QuoteTerm ExprInfo	Quote a term.
Unquote ExprInfo	The splicing construct: unquote ...
Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]	tactic e x1 .. xn \| y1 \| .. \| yn
DontCare Expr	For printing `DontCare` from `Syntax.Internal`.

Instances

Eq Expr Source #	Does not compare `ScopeInfo` fields. Does not distinguish between prefix and postfix projections.
Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Data Expr Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr # toConstr :: Expr -> Constr # dataTypeOf :: Expr -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Expr) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) # gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #
Show Expr Source #
Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
KillRange Expr Source #
Methods killRange :: KillRangeT Expr Source #
HasRange Expr Source #
Methods getRange :: Expr -> Range Source #
Underscore Expr Source #
Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #
IsProjP Expr Source #
Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
SubstExpr Assign Source #
Methods substExpr :: [(Name, Expr)] -> Assign -> Assign Source #
SubstExpr Expr Source #
Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
AllNames Expr Source #
Methods allNames :: Expr -> Seq QName Source #
ExprLike Expr Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr Source # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Expr -> m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
MapNamedArgPattern NAP Source #
Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
PrettyTCM Expr Source #
Methods prettyTCM :: Expr -> TCM Doc Source #
IsFlexiblePattern Pattern Source #
Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern -> TCM Bool Source #
UniverseBi Declaration Pattern Source #
Methods universeBi :: Declaration -> [Pattern]
UniverseBi Declaration Expr Source #
Methods universeBi :: Declaration -> [Expr]
ToConcrete Pattern Pattern Source #
Methods toConcrete :: Pattern -> AbsToCon Pattern Source # bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LHSCore Pattern Source #
Methods toConcrete :: LHSCore -> AbsToCon Pattern Source # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
ToConcrete Expr Expr Source #
Methods toConcrete :: Expr -> AbsToCon Expr Source # bindToConcrete :: Expr -> (Expr -> AbsToCon b) -> AbsToCon b Source #
Reify MetaId Expr Source #
Methods reify :: MetaId -> TCM Expr Source # reifyWhen :: Bool -> MetaId -> TCM Expr Source #
Reify Literal Expr Source #
Methods reify :: Literal -> TCM Expr Source # reifyWhen :: Bool -> Literal -> TCM Expr Source #
Reify Level Expr Source #
Methods reify :: Level -> TCM Expr Source # reifyWhen :: Bool -> Level -> TCM Expr Source #
Reify Sort Expr Source #
Methods reify :: Sort -> TCM Expr Source # reifyWhen :: Bool -> Sort -> TCM Expr Source #
Reify Type Expr Source #
Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Reify Term Expr Source #
Methods reify :: Term -> TCM Expr Source # reifyWhen :: Bool -> Term -> TCM Expr Source #
Reify Expr Expr Source #
Methods reify :: Expr -> TCM Expr Source # reifyWhen :: Bool -> Expr -> TCM Expr Source #
Reify DisplayTerm Expr Source #
Methods reify :: DisplayTerm -> TCM Expr Source # reifyWhen :: Bool -> DisplayTerm -> TCM Expr Source #
ToAbstract Literal Expr Source #
Methods toAbstract :: Literal -> WithNames Expr Source #
ToAbstract Sort Expr Source #
Methods toAbstract :: Sort -> WithNames Expr Source #
ToAbstract Term Expr Source #
Methods toAbstract :: Term -> WithNames Expr Source #
ToAbstract HoleContent HoleContent Source #	Content of interaction hole.
Methods toAbstract :: HoleContent -> ScopeM HoleContent Source #
ToAbstract Expr Expr Source #
Methods toAbstract :: Expr -> ScopeM Expr Source #
ToAbstract OldQName Expr Source #
Methods toAbstract :: OldQName -> ScopeM Expr Source #
ToAbstract Pattern (Names, Pattern) Source #
Methods toAbstract :: Pattern -> WithNames (Names, Pattern) Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract (Pattern' Expr) (Pattern' Expr) Source #
Methods toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr) Source #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source #
Methods toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr) Source #
ToAbstract (Expr, Elims) Expr Source #
Methods toAbstract :: (Expr, Elims) -> WithNames Expr Source #
ToAbstract (Expr, Elim) Expr Source #
Methods toAbstract :: (Expr, Elim) -> WithNames Expr Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

type Assigns = [Assign] Source #

type RecordAssign = Either Assign ModuleName Source #

type RecordAssigns = [RecordAssign] Source #

data Axiom Source #

Is a type signature a postulate or a function signature?

Constructors

FunSig	A function signature.
NoFunSig	Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally).

Instances

Eq Axiom Source #
Methods (==) :: Axiom -> Axiom -> Bool # (/=) :: Axiom -> Axiom -> Bool #
Data Axiom Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Axiom -> c Axiom # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Axiom # toConstr :: Axiom -> Constr # dataTypeOf :: Axiom -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Axiom) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Axiom) # gmapT :: (forall b. Data b => b -> b) -> Axiom -> Axiom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r # gmapQ :: (forall d. Data d => d -> u) -> Axiom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Axiom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom #
Ord Axiom Source #
Methods compare :: Axiom -> Axiom -> Ordering # (<) :: Axiom -> Axiom -> Bool # (<=) :: Axiom -> Axiom -> Bool # (>) :: Axiom -> Axiom -> Bool # (>=) :: Axiom -> Axiom -> Bool # max :: Axiom -> Axiom -> Axiom # min :: Axiom -> Axiom -> Axiom #
Show Axiom Source #
Methods showsPrec :: Int -> Axiom -> ShowS # show :: Axiom -> String # showList :: [Axiom] -> ShowS #

type Ren a = [(a, a)] Source #

Renaming (generic).

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo
Fields renModules :: Ren ModuleName renNames :: Ren QName

Instances

Eq ScopeCopyInfo Source #
Methods (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool # (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool #
Data ScopeCopyInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopeCopyInfo -> c ScopeCopyInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeCopyInfo # toConstr :: ScopeCopyInfo -> Constr # dataTypeOf :: ScopeCopyInfo -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ScopeCopyInfo) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ScopeCopyInfo) # gmapT :: (forall b. Data b => b -> b) -> ScopeCopyInfo -> ScopeCopyInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ScopeCopyInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeCopyInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo #
Show ScopeCopyInfo Source #
Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS # show :: ScopeCopyInfo -> String # showList :: [ScopeCopyInfo] -> ShowS #
Pretty ScopeCopyInfo Source #
Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
KillRange ScopeCopyInfo Source #
Methods killRange :: KillRangeT ScopeCopyInfo Source #

initCopyInfo :: ScopeCopyInfo Source #

data Declaration Source #

Constructors

Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr	Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments.
Field DefInfo QName (Arg Expr)	record field
Primitive DefInfo QName Expr	primitive function
Mutual MutualInfo [Declaration]	a bunch of mutually recursive definitions
Section ModuleInfo ModuleName [TypedBindings] [Declaration]
Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective	The `ImportDirective` is for highlighting purposes.
Import ModuleInfo ModuleName ImportDirective	The `ImportDirective` is for highlighting purposes.
Pragma Range Pragma
Open ModuleInfo ModuleName ImportDirective	only retained for highlighting purposes
FunDef DefInfo QName Delayed [Clause]	sequence of function clauses
DataSig DefInfo QName Telescope Expr	lone data signature
DataDef DefInfo QName [LamBinding] [Constructor]	the `LamBinding`s are `DomainFree` and bind the parameters of the datatype.
RecSig DefInfo QName Telescope Expr	lone record signature
RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) [LamBinding] Expr [Declaration]	The `LamBinding`s are `DomainFree` and bind the parameters of the datatype. The `Expr` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Prop`, and the optional name is the constructor's name.
PatternSynDef QName [Arg Name] (Pattern' Void)	Only for highlighting purposes
UnquoteDecl MutualInfo [DefInfo] [QName] Expr
UnquoteDef [DefInfo] [QName] Expr
ScopedDecl ScopeInfo [Declaration]	scope annotation

Instances

Eq Declaration Source #	Does not compare `ScopeInfo` fields.
Methods (==) :: Declaration -> Declaration -> Bool # (/=) :: Declaration -> Declaration -> Bool #
Data Declaration Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration # toConstr :: Declaration -> Constr # dataTypeOf :: Declaration -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) # gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration #
Show Declaration Source #
Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS #
KillRange Declaration Source #
Methods killRange :: KillRangeT Declaration Source #
HasRange Declaration Source #
Methods getRange :: Declaration -> Range Source #
GetDefInfo Declaration Source #
Methods getDefInfo :: Declaration -> Maybe DefInfo Source #
AnyAbstract Declaration Source #
Methods anyAbstract :: Declaration -> Bool Source #
AllNames Declaration Source #
Methods allNames :: Declaration -> Seq QName Source #
ExprLike Declaration Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Declaration -> m Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Declaration -> m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
ShowHead Declaration Source #
Methods showHead :: Declaration -> String Source #
UniverseBi Declaration RString Source #
Methods universeBi :: Declaration -> [RString]
UniverseBi Declaration AmbiguousQName Source #
Methods universeBi :: Declaration -> [AmbiguousQName]
UniverseBi Declaration ModuleName Source #
Methods universeBi :: Declaration -> [ModuleName]
UniverseBi Declaration QName Source #
Methods universeBi :: Declaration -> [QName]
UniverseBi Declaration ModuleInfo Source #
Methods universeBi :: Declaration -> [ModuleInfo]
UniverseBi Declaration Pattern Source #
Methods universeBi :: Declaration -> [Pattern]
UniverseBi Declaration TypedBinding Source #
Methods universeBi :: Declaration -> [TypedBinding]
UniverseBi Declaration LamBinding Source #
Methods universeBi :: Declaration -> [LamBinding]
UniverseBi Declaration LetBinding Source #
Methods universeBi :: Declaration -> [LetBinding]
UniverseBi Declaration Declaration Source #
Methods universeBi :: Declaration -> [Declaration]
UniverseBi Declaration Expr Source #
Methods universeBi :: Declaration -> [Expr]
ToAbstract NiceDeclaration Declaration Source #
Methods toAbstract :: NiceDeclaration -> ScopeM Declaration Source #
UniverseBi Declaration (Pattern' Void) Source #
Methods universeBi :: Declaration -> [Pattern' Void]
ToConcrete Declaration [Declaration] Source #
Methods toConcrete :: Declaration -> AbsToCon [Declaration] Source # bindToConcrete :: Declaration -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
ToConcrete (Constr Constructor) Declaration Source #
Methods toConcrete :: Constr Constructor -> AbsToCon Declaration Source # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b Source #
ToAbstract [Declaration] [Declaration] Source #
Methods toAbstract :: [Declaration] -> ScopeM [Declaration] Source #

class GetDefInfo a where Source #

Minimal complete definition

getDefInfo

Methods

getDefInfo :: a -> Maybe DefInfo Source #

Instances

GetDefInfo Declaration Source #
Methods getDefInfo :: Declaration -> Maybe DefInfo Source #

type ImportDirective = ImportDirective' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type ImportedName = ImportedName' QName ModuleName Source #

data ModuleApplication Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]	`tel. M args`: applies `M` to `args` and abstracts `tel`.
RecordModuleIFS ModuleName	M {{...}}

Instances

Eq ModuleApplication Source #
Methods (==) :: ModuleApplication -> ModuleApplication -> Bool # (/=) :: ModuleApplication -> ModuleApplication -> Bool #
Data ModuleApplication Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleApplication -> c ModuleApplication # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication # toConstr :: ModuleApplication -> Constr # dataTypeOf :: ModuleApplication -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication) # gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication #
Show ModuleApplication Source #
Methods showsPrec :: Int -> ModuleApplication -> ShowS # show :: ModuleApplication -> String # showList :: [ModuleApplication] -> ShowS #
KillRange ModuleApplication Source #
Methods killRange :: KillRangeT ModuleApplication Source #
AllNames ModuleApplication Source #
Methods allNames :: ModuleApplication -> Seq QName Source #
ExprLike ModuleApplication Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleApplication -> m ModuleApplication Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication Source # mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source #
ToConcrete ModuleApplication ModuleApplication Source #
Methods toConcrete :: ModuleApplication -> AbsToCon ModuleApplication Source # bindToConcrete :: ModuleApplication -> (ModuleApplication -> AbsToCon b) -> AbsToCon b Source #

data Pragma Source #

Constructors

OptionsPragma [String]
BuiltinPragma String ResolvedName	`ResolvedName` is not `UnknownName`. Name can be ambiguous e.g. for built-in constructors.
BuiltinNoDefPragma String QName	Builtins that do not come with a definition, but declare a name for an Agda concept.
RewritePragma QName
CompilePragma String QName String
CompiledPragma QName String
CompiledExportPragma QName String
CompiledTypePragma QName String
CompiledDataPragma QName String [String]
CompiledJSPragma QName String
CompiledUHCPragma QName String
CompiledDataUHCPragma QName String [String]
StaticPragma QName
EtaPragma QName	For coinductive records, use pragma instead of regular `eta-equality` definition (as it is might make Agda loop).
InjectivePragma QName
InlinePragma Bool QName
DisplayPragma QName [NamedArg Pattern] Expr

Instances

Eq Pragma Source #
Methods (==) :: Pragma -> Pragma -> Bool # (/=) :: Pragma -> Pragma -> Bool #
Data Pragma Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma # toConstr :: Pragma -> Constr # dataTypeOf :: Pragma -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) # gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma #
Show Pragma Source #
Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
ExprLike Pragma Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma Source # foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pragma -> m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
ToAbstract Pragma [Pragma] Source #
Methods toAbstract :: Pragma -> ScopeM [Pragma] Source #

data LetBinding Source #

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo BindName Expr Expr	LetBind info rel name type defn
LetPatBind LetInfo Pattern Expr	Irrefutable pattern binding.
LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective	`LetApply mi newM (oldM args) renamings dir`. The `ImportDirective` is for highlighting purposes.
LetOpen ModuleInfo ModuleName ImportDirective	only for highlighting and abstractToConcrete
LetDeclaredVariable BindName	Only used for highlighting. Refers to the first occurrence of `x` in `let x : A; x = e`.

Instances

Eq LetBinding Source #
Methods (==) :: LetBinding -> LetBinding -> Bool # (/=) :: LetBinding -> LetBinding -> Bool #
Data LetBinding Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetBinding -> c LetBinding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBinding # toConstr :: LetBinding -> Constr # dataTypeOf :: LetBinding -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c LetBinding) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetBinding) # gmapT :: (forall b. Data b => b -> b) -> LetBinding -> LetBinding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r # gmapQ :: (forall d. Data d => d -> u) -> LetBinding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBinding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding #
Show LetBinding Source #
Methods showsPrec :: Int -> LetBinding -> ShowS # show :: LetBinding -> String # showList :: [LetBinding] -> ShowS #
KillRange LetBinding Source #
Methods killRange :: KillRangeT LetBinding Source #
HasRange LetBinding Source #
Methods getRange :: LetBinding -> Range Source #
SubstExpr LetBinding Source #
Methods substExpr :: [(Name, Expr)] -> LetBinding -> LetBinding Source #
AllNames LetBinding Source #
Methods allNames :: LetBinding -> Seq QName Source #
ExprLike LetBinding Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LetBinding -> m LetBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LetBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LetBinding -> m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
UniverseBi Declaration LetBinding Source #
Methods universeBi :: Declaration -> [LetBinding]
ToConcrete LetBinding [Declaration] Source #
Methods toConcrete :: LetBinding -> AbsToCon [Declaration] Source # bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
ToAbstract LetDef [LetBinding] Source #
Methods toAbstract :: LetDef -> ScopeM [LetBinding] Source #
ToAbstract LetDefs [LetBinding] Source #
Methods toAbstract :: LetDefs -> ScopeM [LetBinding] Source #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source #
Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) Source #

type TypeSignature = Declaration Source #

Only Axioms.

type Constructor = TypeSignature Source #

type Field = TypeSignature Source #

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree ArgInfo BindName	. `x` or `{x}` or `.x` or `.{x}`
DomainFull TypedBindings	. `(xs:e)` or `{xs:e}` or `(let Ds)`

Instances

Eq LamBinding Source #
Methods (==) :: LamBinding -> LamBinding -> Bool # (/=) :: LamBinding -> LamBinding -> Bool #
Data LamBinding Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding -> c LamBinding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamBinding # toConstr :: LamBinding -> Constr # dataTypeOf :: LamBinding -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c LamBinding) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamBinding) # gmapT :: (forall b. Data b => b -> b) -> LamBinding -> LamBinding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r # gmapQ :: (forall d. Data d => d -> u) -> LamBinding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding #
Show LamBinding Source #
Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
KillRange LamBinding Source #
Methods killRange :: KillRangeT LamBinding Source #
HasRange LamBinding Source #
Methods getRange :: LamBinding -> Range Source #
LensHiding LamBinding Source #
Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
AllNames LamBinding Source #
Methods allNames :: LamBinding -> Seq QName Source #
ExprLike LamBinding Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LamBinding -> m LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
UniverseBi Declaration LamBinding Source #
Methods universeBi :: Declaration -> [LamBinding]
ToAbstract LamBinding LamBinding Source #
Methods toAbstract :: LamBinding -> ScopeM LamBinding Source #
ToConcrete LamBinding [LamBinding] Source #
Methods toConcrete :: LamBinding -> AbsToCon [LamBinding] Source # bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b Source #

data TypedBindings Source #

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

. (xs : e) or {xs : e}

Instances

Eq TypedBindings Source #
Methods (==) :: TypedBindings -> TypedBindings -> Bool # (/=) :: TypedBindings -> TypedBindings -> Bool #
Data TypedBindings Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBindings -> c TypedBindings # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypedBindings # toConstr :: TypedBindings -> Constr # dataTypeOf :: TypedBindings -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TypedBindings) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypedBindings) # gmapT :: (forall b. Data b => b -> b) -> TypedBindings -> TypedBindings # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBindings -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBindings -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedBindings -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBindings -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBindings -> m TypedBindings # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBindings -> m TypedBindings # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBindings -> m TypedBindings #
Show TypedBindings Source #
Methods showsPrec :: Int -> TypedBindings -> ShowS # show :: TypedBindings -> String # showList :: [TypedBindings] -> ShowS #
KillRange TypedBindings Source #
Methods killRange :: KillRangeT TypedBindings Source #
HasRange TypedBindings Source #
Methods getRange :: TypedBindings -> Range Source #
LensHiding TypedBindings Source #
Methods getHiding :: TypedBindings -> Hiding Source # setHiding :: Hiding -> TypedBindings -> TypedBindings Source # mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings Source #
SubstExpr TypedBindings Source #
Methods substExpr :: [(Name, Expr)] -> TypedBindings -> TypedBindings Source #
AllNames TypedBindings Source #
Methods allNames :: TypedBindings -> Seq QName Source #
ExprLike TypedBindings Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBindings -> m TypedBindings Source # foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> TypedBindings -> m TypedBindings Source # mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings Source #
Reify Telescope Telescope Source #
Methods reify :: Telescope -> TCM Telescope Source # reifyWhen :: Bool -> Telescope -> TCM Telescope Source #
ToAbstract TypedBindings TypedBindings Source #
Methods toAbstract :: TypedBindings -> ScopeM TypedBindings Source #
ToConcrete TypedBindings [TypedBindings] Source #
Methods toConcrete :: TypedBindings -> AbsToCon [TypedBindings] Source # bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings Source #
Methods toAbstract :: (Dom r, Name) -> WithNames TypedBindings Source #

data TypedBinding Source #

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

We would have to typecheck the type A several times.
If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

TBind Range [WithHiding BindName] Expr	As in telescope `(x y z : A)` or type `(x y z : A) -> B`.
TLet Range [LetBinding]	E.g. `(let x = e)` or `(let open M)`.

Instances

Eq TypedBinding Source #
Methods (==) :: TypedBinding -> TypedBinding -> Bool # (/=) :: TypedBinding -> TypedBinding -> Bool #
Data TypedBinding Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding -> c TypedBinding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypedBinding # toConstr :: TypedBinding -> Constr # dataTypeOf :: TypedBinding -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TypedBinding) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypedBinding) # gmapT :: (forall b. Data b => b -> b) -> TypedBinding -> TypedBinding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedBinding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding #
Show TypedBinding Source #
Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
KillRange TypedBinding Source #
Methods killRange :: KillRangeT TypedBinding Source #
HasRange TypedBinding Source #
Methods getRange :: TypedBinding -> Range Source #
SubstExpr TypedBinding Source #
Methods substExpr :: [(Name, Expr)] -> TypedBinding -> TypedBinding Source #
AllNames TypedBinding Source #
Methods allNames :: TypedBinding -> Seq QName Source #
ExprLike TypedBinding Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBinding -> m TypedBinding Source # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> TypedBinding -> m TypedBinding Source # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding Source #
PrettyTCM TypedBinding Source #
Methods prettyTCM :: TypedBinding -> TCM Doc Source #
UniverseBi Declaration TypedBinding Source #
Methods universeBi :: Declaration -> [TypedBinding]
ToConcrete TypedBinding TypedBinding Source #
Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding Source # bindToConcrete :: TypedBinding -> (TypedBinding -> AbsToCon b) -> AbsToCon b Source #
ToAbstract TypedBinding TypedBinding Source #
Methods toAbstract :: TypedBinding -> ScopeM TypedBinding Source #

type Telescope = [TypedBindings] Source #

data ProblemEq Source #

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete.

Constructors

ProblemEq
Fields problemInPat :: Pattern problemInst :: Term problemType :: Dom Type

Instances

Eq ProblemEq Source #
Methods (==) :: ProblemEq -> ProblemEq -> Bool # (/=) :: ProblemEq -> ProblemEq -> Bool #
Data ProblemEq Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq # toConstr :: ProblemEq -> Constr # dataTypeOf :: ProblemEq -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) # gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq #
Show ProblemEq Source #
Methods showsPrec :: Int -> ProblemEq -> ShowS # show :: ProblemEq -> String # showList :: [ProblemEq] -> ShowS #
KillRange ProblemEq Source #
Methods killRange :: KillRangeT ProblemEq Source #

data Clause' lhs Source #

We could throw away where clauses at this point and translate them to let. It's not obvious how to remember that the let was really a where clause though, so for the time being we keep it here.

Constructors

Clause
Fields clauseLHS :: lhs clauseStrippedPats :: [ProblemEq] Only in with-clauses where we inherit some already checked patterns from the parent. These live in the context of the parent clause left-hand side. clauseRHS :: RHS clauseWhereDecls :: WhereDeclarations clauseCatchall :: Bool

Instances

Functor Clause' Source #
Methods fmap :: (a -> b) -> Clause' a -> Clause' b # (<$) :: a -> Clause' b -> Clause' a #
Foldable Clause' Source #
Methods fold :: Monoid m => Clause' m -> m # foldMap :: Monoid m => (a -> m) -> Clause' a -> m # foldr :: (a -> b -> b) -> b -> Clause' a -> b # foldr' :: (a -> b -> b) -> b -> Clause' a -> b # foldl :: (b -> a -> b) -> b -> Clause' a -> b # foldl' :: (b -> a -> b) -> b -> Clause' a -> b # foldr1 :: (a -> a -> a) -> Clause' a -> a # foldl1 :: (a -> a -> a) -> Clause' a -> a # toList :: Clause' a -> [a] # null :: Clause' a -> Bool # length :: Clause' a -> Int # elem :: Eq a => a -> Clause' a -> Bool # maximum :: Ord a => Clause' a -> a # minimum :: Ord a => Clause' a -> a # sum :: Num a => Clause' a -> a # product :: Num a => Clause' a -> a #
Traversable Clause' Source #
Methods traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) # sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) # mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) # sequence :: Monad m => Clause' (m a) -> m (Clause' a) #
AllNames Clause Source #
Methods allNames :: Clause -> Seq QName Source #
LHSToSpine Clause SpineClause Source #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
Reify NamedClause Clause Source #
Methods reify :: NamedClause -> TCM Clause Source # reifyWhen :: Bool -> NamedClause -> TCM Clause Source #
ToAbstract Clause Clause Source #
Methods toAbstract :: Clause -> ScopeM Clause Source #
Eq lhs => Eq (Clause' lhs) Source #
Methods (==) :: Clause' lhs -> Clause' lhs -> Bool # (/=) :: Clause' lhs -> Clause' lhs -> Bool #
Data lhs => Data (Clause' lhs) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause' lhs -> c (Clause' lhs) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Clause' lhs) # toConstr :: Clause' lhs -> Constr # dataTypeOf :: Clause' lhs -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Clause' lhs)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Clause' lhs)) # gmapT :: (forall b. Data b => b -> b) -> Clause' lhs -> Clause' lhs # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r # gmapQ :: (forall d. Data d => d -> u) -> Clause' lhs -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause' lhs -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) #
Show lhs => Show (Clause' lhs) Source #
Methods showsPrec :: Int -> Clause' lhs -> ShowS # show :: Clause' lhs -> String # showList :: [Clause' lhs] -> ShowS #
KillRange a => KillRange (Clause' a) Source #
Methods killRange :: KillRangeT (Clause' a) Source #
HasRange a => HasRange (Clause' a) Source #
Methods getRange :: Clause' a -> Range Source #
ExprLike a => ExprLike (Clause' a) Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a) Source # foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Clause' a -> m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source #
Reify (QNamed Clause) Clause Source #
Methods reify :: QNamed Clause -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause -> TCM Clause Source #
ToAbstract (QNamed Clause) Clause Source #
Methods toAbstract :: QNamed Clause -> WithNames Clause Source #
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source #
Methods toConcrete :: Clause' a -> AbsToCon [Declaration] Source # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
ToAbstract [QNamed Clause] [Clause] Source #
Methods toAbstract :: [QNamed Clause] -> WithNames [Clause] Source #

data WhereDeclarations Source #

Constructors

WhereDecls
Fields whereModule :: Maybe ModuleName whereDecls :: [Declaration]

Instances

Eq WhereDeclarations Source #
Methods (==) :: WhereDeclarations -> WhereDeclarations -> Bool # (/=) :: WhereDeclarations -> WhereDeclarations -> Bool #
Data WhereDeclarations Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereDeclarations -> c WhereDeclarations # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WhereDeclarations # toConstr :: WhereDeclarations -> Constr # dataTypeOf :: WhereDeclarations -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c WhereDeclarations) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c WhereDeclarations) # gmapT :: (forall b. Data b => b -> b) -> WhereDeclarations -> WhereDeclarations # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r # gmapQ :: (forall d. Data d => d -> u) -> WhereDeclarations -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereDeclarations -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations #
Show WhereDeclarations Source #
Methods showsPrec :: Int -> WhereDeclarations -> ShowS # show :: WhereDeclarations -> String # showList :: [WhereDeclarations] -> ShowS #
KillRange WhereDeclarations Source #
Methods killRange :: KillRangeT WhereDeclarations Source #
HasRange WhereDeclarations Source #
Methods getRange :: WhereDeclarations -> Range Source #
AllNames WhereDeclarations Source #
Methods allNames :: WhereDeclarations -> Seq QName Source #
ExprLike WhereDeclarations Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> WhereDeclarations -> m WhereDeclarations Source # foldExpr :: Monoid m => (Expr -> m) -> WhereDeclarations -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> WhereDeclarations -> m WhereDeclarations Source # mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations Source #
ToConcrete WhereDeclarations WhereClause Source #
Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause Source # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b Source #

noWhereDecls :: WhereDeclarations Source #

type Clause = Clause' LHS Source #

type SpineClause = Clause' SpineLHS Source #

data RHS Source #

Constructors

RHS
Fields rhsExpr :: Expr rhsConcrete :: Maybe Expr We store the original concrete expression in case we have to reproduce it during interactive case splitting. `Nothing` for internally generated rhss.
AbsurdRHS
WithRHS QName [Expr] [Clause]	The `QName` is the name of the with function.
RewriteRHS
Fields rewriteExprs :: [(QName, Expr)] The `QName`s are the names of the generated with functions, one for each `Expr`. rewriteStrippedPats :: [ProblemEq] The patterns stripped by with-desugaring. These are only present if this rewrite follows a with. rewriteRHS :: RHS The RHS should not be another `RewriteRHS`. rewriteWhereDecls :: WhereDeclarations The where clauses are attached to the `RewriteRHS` by

Instances

Eq RHS Source #	Ignore `rhsConcrete` when comparing `RHS`s.
Methods (==) :: RHS -> RHS -> Bool # (/=) :: RHS -> RHS -> Bool #
Data RHS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS -> c RHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RHS # toConstr :: RHS -> Constr # dataTypeOf :: RHS -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c RHS) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RHS) # gmapT :: (forall b. Data b => b -> b) -> RHS -> RHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r # gmapQ :: (forall d. Data d => d -> u) -> RHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS -> m RHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS #
Show RHS Source #
Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
KillRange RHS Source #
Methods killRange :: KillRangeT RHS Source #
HasRange RHS Source #
Methods getRange :: RHS -> Range Source #
AllNames RHS Source #
Methods allNames :: RHS -> Seq QName Source #
ExprLike RHS Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS Source # foldExpr :: Monoid m => (Expr -> m) -> RHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> RHS -> m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
ToAbstract AbstractRHS RHS Source #
Methods toAbstract :: AbstractRHS -> ScopeM RHS Source #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source #
Methods toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source #

data SpineLHS Source #

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as ProjP d.

Constructors

SpineLHS
Fields spLhsInfo :: LHSInfo Range. spLhsDefName :: QName Name of function we are defining. spLhsPats :: [NamedArg Pattern] Elimination by pattern, projections, with-patterns.

Instances

Eq SpineLHS Source #
Methods (==) :: SpineLHS -> SpineLHS -> Bool # (/=) :: SpineLHS -> SpineLHS -> Bool #
Data SpineLHS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpineLHS -> c SpineLHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpineLHS # toConstr :: SpineLHS -> Constr # dataTypeOf :: SpineLHS -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SpineLHS) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpineLHS) # gmapT :: (forall b. Data b => b -> b) -> SpineLHS -> SpineLHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r # gmapQ :: (forall d. Data d => d -> u) -> SpineLHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SpineLHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS #
Show SpineLHS Source #
Methods showsPrec :: Int -> SpineLHS -> ShowS # show :: SpineLHS -> String # showList :: [SpineLHS] -> ShowS #
KillRange SpineLHS Source #
Methods killRange :: KillRangeT SpineLHS Source #
HasRange SpineLHS Source #
Methods getRange :: SpineLHS -> Range Source #
ExprLike SpineLHS Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS Source # foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> SpineLHS -> m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
LHSToSpine Clause SpineClause Source #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ToConcrete SpineLHS LHS Source #
Methods toConcrete :: SpineLHS -> AbsToCon LHS Source # bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b Source #

data LHS Source #

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

LHS
Fields lhsInfo :: LHSInfo Range. lhsCore :: LHSCore Copatterns.

Instances

Eq LHS Source #	Ignore `Range` when comparing `LHS`s.
Methods (==) :: LHS -> LHS -> Bool # (/=) :: LHS -> LHS -> Bool #
Data LHS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS # toConstr :: LHS -> Constr # dataTypeOf :: LHS -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c LHS) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) # gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS #
Show LHS Source #
Methods showsPrec :: Int -> LHS -> ShowS # show :: LHS -> String # showList :: [LHS] -> ShowS #
KillRange LHS Source #
Methods killRange :: KillRangeT LHS Source #
HasRange LHS Source #
Methods getRange :: LHS -> Range Source #
AllNames Clause Source #
Methods allNames :: Clause -> Seq QName Source #
ExprLike LHS Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS Source # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHS -> m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
LHSToSpine Clause SpineClause Source #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ToConcrete LHS LHS Source #
Methods toConcrete :: LHS -> AbsToCon LHS Source # bindToConcrete :: LHS -> (LHS -> AbsToCon b) -> AbsToCon b Source #
Reify NamedClause Clause Source #
Methods reify :: NamedClause -> TCM Clause Source # reifyWhen :: Bool -> NamedClause -> TCM Clause Source #
ToAbstract Clause Clause Source #
Methods toAbstract :: Clause -> ScopeM Clause Source #
ToAbstract LeftHandSide LHS Source #
Methods toAbstract :: LeftHandSide -> ScopeM LHS Source #
Reify (QNamed Clause) Clause Source #
Methods reify :: QNamed Clause -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause -> TCM Clause Source #
ToAbstract (QNamed Clause) Clause Source #
Methods toAbstract :: QNamed Clause -> WithNames Clause Source #
ToAbstract [QNamed Clause] [Clause] Source #
Methods toAbstract :: [QNamed Clause] -> WithNames [Clause] Source #

data LHSCore' e Source #

The lhs in projection-application and with-pattern view. Parameterised over the type e of dot patterns.

Constructors

LHSHead	The head applied to ordinary patterns.
Fields lhsDefName :: QName Head `f`. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSProj	Projection.
Fields lhsDestructor :: AmbiguousQName Record projection identifier. lhsFocus :: NamedArg (LHSCore' e) Main argument of projection. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSWith	With patterns.
Fields lhsHead :: LHSCore' e E.g. the `LHSHead`. lhsWithPatterns :: [Pattern' e] Applied to with patterns `\| p1 \| ... \| pn`. These patterns are not prefixed with `WithP`! lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.

Instances

Functor LHSCore' Source #
Methods fmap :: (a -> b) -> LHSCore' a -> LHSCore' b # (<$) :: a -> LHSCore' b -> LHSCore' a #
Foldable LHSCore' Source #
Methods fold :: Monoid m => LHSCore' m -> m # foldMap :: Monoid m => (a -> m) -> LHSCore' a -> m # foldr :: (a -> b -> b) -> b -> LHSCore' a -> b # foldr' :: (a -> b -> b) -> b -> LHSCore' a -> b # foldl :: (b -> a -> b) -> b -> LHSCore' a -> b # foldl' :: (b -> a -> b) -> b -> LHSCore' a -> b # foldr1 :: (a -> a -> a) -> LHSCore' a -> a # foldl1 :: (a -> a -> a) -> LHSCore' a -> a # toList :: LHSCore' a -> [a] # null :: LHSCore' a -> Bool # length :: LHSCore' a -> Int # elem :: Eq a => a -> LHSCore' a -> Bool # maximum :: Ord a => LHSCore' a -> a # minimum :: Ord a => LHSCore' a -> a # sum :: Num a => LHSCore' a -> a # product :: Num a => LHSCore' a -> a #
Traversable LHSCore' Source #
Methods traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) # sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) # mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) # sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a) #
ToConcrete LHSCore Pattern Source #
Methods toConcrete :: LHSCore -> AbsToCon Pattern Source # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
ToAbstract LHSCore (LHSCore' Expr) Source #
Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) Source #
Eq e => Eq (LHSCore' e) Source #
Methods (==) :: LHSCore' e -> LHSCore' e -> Bool # (/=) :: LHSCore' e -> LHSCore' e -> Bool #
Data e => Data (LHSCore' e) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore' e -> c (LHSCore' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LHSCore' e) # toConstr :: LHSCore' e -> Constr # dataTypeOf :: LHSCore' e -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (LHSCore' e)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d a. (Data d, Data a) => c (t d a)) -> Maybe (c (LHSCore' e)) # gmapT :: (forall b. Data b => b -> b) -> LHSCore' e -> LHSCore' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r # gmapQ :: (forall d. Data d => d -> u) -> LHSCore' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) #
Show e => Show (LHSCore' e) Source #
Methods showsPrec :: Int -> LHSCore' e -> ShowS # show :: LHSCore' e -> String # showList :: [LHSCore' e] -> ShowS #
KillRange e => KillRange (LHSCore' e) Source #
Methods killRange :: KillRangeT (LHSCore' e) Source #
HasRange (LHSCore' e) Source #
Methods getRange :: LHSCore' e -> Range Source #
ExprLike a => ExprLike (LHSCore' a) Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source # foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source #
Methods toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr) Source #

type LHSCore = LHSCore' Expr Source #

Patterns

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName
ConP ConPatInfo AmbiguousQName (NAPs e)
ProjP PatInfo ProjOrigin AmbiguousQName	Destructor pattern `d`.
DefP PatInfo AmbiguousQName (NAPs e)	Defined pattern: function definition `f ps`. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.
WildP PatInfo	Underscore pattern entered by user. Or generated at type checking for implicit arguments.
AsP PatInfo BindName (Pattern' e)
DotP PatInfo e	Dot pattern `.e`
AbsurdP PatInfo
LitP Literal
PatternSynP PatInfo AmbiguousQName (NAPs e)
RecP PatInfo [FieldAssignment' (Pattern' e)]
WithP PatInfo (Pattern' e)	`\| p`, for with-patterns.

Instances

Functor Pattern' Source #
Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b # (<$) :: a -> Pattern' b -> Pattern' a #
Foldable Pattern' Source #
Methods fold :: Monoid m => Pattern' m -> m # foldMap :: Monoid m => (a -> m) -> Pattern' a -> m # foldr :: (a -> b -> b) -> b -> Pattern' a -> b # foldr' :: (a -> b -> b) -> b -> Pattern' a -> b # foldl :: (b -> a -> b) -> b -> Pattern' a -> b # foldl' :: (b -> a -> b) -> b -> Pattern' a -> b # foldr1 :: (a -> a -> a) -> Pattern' a -> a # foldl1 :: (a -> a -> a) -> Pattern' a -> a # toList :: Pattern' a -> [a] # null :: Pattern' a -> Bool # length :: Pattern' a -> Int # elem :: Eq a => a -> Pattern' a -> Bool # maximum :: Ord a => Pattern' a -> a # minimum :: Ord a => Pattern' a -> a # sum :: Num a => Pattern' a -> a # product :: Num a => Pattern' a -> a #
Traversable Pattern' Source #
Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) #
MapNamedArgPattern NAP Source #
Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
IsFlexiblePattern Pattern Source #
Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern -> TCM Bool Source #
UniverseBi Declaration Pattern Source #
Methods universeBi :: Declaration -> [Pattern]
ToConcrete Pattern Pattern Source #
Methods toConcrete :: Pattern -> AbsToCon Pattern Source # bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
UniverseBi Declaration (Pattern' Void) Source #
Methods universeBi :: Declaration -> [Pattern' Void]
APatternLike a (Pattern' a) Source #
Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m Source # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #
ToAbstract Pattern (Pattern' Expr) Source #
Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) Source #
ToAbstract Pattern (Names, Pattern) Source #
Methods toAbstract :: Pattern -> WithNames (Names, Pattern) Source #
Eq e => Eq (Pattern' e) Source #
Methods (==) :: Pattern' e -> Pattern' e -> Bool # (/=) :: Pattern' e -> Pattern' e -> Bool #
Data e => Data (Pattern' e) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' e -> c (Pattern' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' e) # toConstr :: Pattern' e -> Constr # dataTypeOf :: Pattern' e -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' e)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d a. (Data d, Data a) => c (t d a)) -> Maybe (c (Pattern' e)) # gmapT :: (forall b. Data b => b -> b) -> Pattern' e -> Pattern' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r # gmapQ :: (forall d. Data d => d -> u) -> Pattern' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) #
Show e => Show (Pattern' e) Source #
Methods showsPrec :: Int -> Pattern' e -> ShowS # show :: Pattern' e -> String # showList :: [Pattern' e] -> ShowS #
KillRange e => KillRange (Pattern' e) Source #
Methods killRange :: KillRangeT (Pattern' e) Source #
SetRange (Pattern' a) Source #
Methods setRange :: Range -> Pattern' a -> Pattern' a Source #
HasRange (Pattern' e) Source #
Methods getRange :: Pattern' e -> Range Source #
IsProjP (Pattern' e) Source #
Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP e => MaybePostfixProjP (Pattern' e) Source #
Methods maybePostfixProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
ExprLike a => ExprLike (Pattern' a) Source #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source # foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m Source # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source #
NamesIn (Pattern' a) Source #
Methods namesIn :: Pattern' a -> Set QName Source #
ExpandPatternSynonyms (Pattern' e) Source #
Methods expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #
ToAbstract (Pattern' Expr) (Pattern' Expr) Source #
Methods toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr) Source #

type NAPs e = [NamedArg (Pattern' e)] Source #

type Pattern = Pattern' Expr Source #

type Patterns = [NamedArg Pattern] Source #

class MaybePostfixProjP a where Source #

Minimal complete definition

maybePostfixProjP

Methods

maybePostfixProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) Source #

Instances

MaybePostfixProjP a => MaybePostfixProjP (Arg a) Source #
Methods maybePostfixProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) Source #
IsProjP e => MaybePostfixProjP (Pattern' e) Source #
Methods maybePostfixProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
MaybePostfixProjP a => MaybePostfixProjP (Named n a) Source #
Methods maybePostfixProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source #

type HoleContent = HoleContent' Expr Source #

class AllNames a where Source #

Extracts all the names which are declared in a Declaration. This does not include open public or let expressions, but it does include local modules, where clauses and the names of extended lambdas.

Minimal complete definition

allNames

Methods

allNames :: a -> Seq QName Source #

Instances

AllNames QName Source #
Methods allNames :: QName -> Seq QName Source #
AllNames RHS Source #
Methods allNames :: RHS -> Seq QName Source #
AllNames Clause Source #
Methods allNames :: Clause -> Seq QName Source #
AllNames WhereDeclarations Source #
Methods allNames :: WhereDeclarations -> Seq QName Source #
AllNames TypedBinding Source #
Methods allNames :: TypedBinding -> Seq QName Source #
AllNames TypedBindings Source #
Methods allNames :: TypedBindings -> Seq QName Source #
AllNames LamBinding Source #
Methods allNames :: LamBinding -> Seq QName Source #
AllNames LetBinding Source #
Methods allNames :: LetBinding -> Seq QName Source #
AllNames ModuleApplication Source #
Methods allNames :: ModuleApplication -> Seq QName Source #
AllNames Declaration Source #
Methods allNames :: Declaration -> Seq QName Source #
AllNames Expr Source #
Methods allNames :: Expr -> Seq QName Source #
AllNames CallInfo Source #
Methods allNames :: CallInfo -> Seq QName Source #
AllNames CallPath Source #
Methods allNames :: CallPath -> Seq QName Source #
AllNames a => AllNames [a] Source #
Methods allNames :: [a] -> Seq QName Source #
AllNames a => AllNames (Maybe a) Source #
Methods allNames :: Maybe a -> Seq QName Source #
AllNames a => AllNames (Arg a) Source #
Methods allNames :: Arg a -> Seq QName Source #
(AllNames a, AllNames b) => AllNames (a, b) Source #
Methods allNames :: (a, b) -> Seq QName Source #
AllNames a => AllNames (Named name a) Source #
Methods allNames :: Named name a -> Seq QName Source #

axiomName :: Declaration -> QName Source #

The name defined by the given axiom.

Precondition: The declaration has to be a (scoped) Axiom.

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Minimal complete definition

anyAbstract

Methods

anyAbstract :: a -> Bool Source #

Instances

AnyAbstract Declaration Source #
Methods anyAbstract :: Declaration -> Bool Source #
AnyAbstract a => AnyAbstract [a] Source #
Methods anyAbstract :: [a] -> Bool Source #

class NameToExpr a where Source #

Minimal complete definition

nameExpr

Methods

nameExpr :: a -> Expr Source #

Instances

NameToExpr ResolvedName Source #	Assumes name is not `UnknownName`.
Methods nameExpr :: ResolvedName -> Expr Source #
NameToExpr AbstractName Source #	Turn an `AbstractName` to an expression.
Methods nameExpr :: AbstractName -> Expr Source #

app :: Expr -> [NamedArg Expr] -> Expr Source #

mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr Source #

patternToExpr :: Pattern -> Expr Source #

type PatternSynDefn = ([Arg Name], Pattern' Void) Source #

type PatternSynDefns = Map QName PatternSynDefn Source #

lambdaLiftExpr :: [Name] -> Expr -> Expr Source #

class SubstExpr a where Source #

Minimal complete definition

substExpr

Methods

substExpr :: [(Name, Expr)] -> a -> a Source #

Instances

SubstExpr Name Source #
Methods substExpr :: [(Name, Expr)] -> Name -> Name Source #
SubstExpr ModuleName Source #
Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
SubstExpr TypedBinding Source #
Methods substExpr :: [(Name, Expr)] -> TypedBinding -> TypedBinding Source #
SubstExpr TypedBindings Source #
Methods substExpr :: [(Name, Expr)] -> TypedBindings -> TypedBindings Source #
SubstExpr LetBinding Source #
Methods substExpr :: [(Name, Expr)] -> LetBinding -> LetBinding Source #
SubstExpr Assign Source #
Methods substExpr :: [(Name, Expr)] -> Assign -> Assign Source #
SubstExpr Expr Source #
Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
SubstExpr a => SubstExpr [a] Source #
Methods substExpr :: [(Name, Expr)] -> [a] -> [a] Source #
SubstExpr a => SubstExpr (Arg a) Source #
Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source #
Methods substExpr :: [(Name, Expr)] -> Either a b -> Either a b Source #
(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source #
Methods substExpr :: [(Name, Expr)] -> (a, b) -> (a, b) Source #
SubstExpr a => SubstExpr (Named name a) Source #
Methods substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #

insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) Source #

module Agda.Syntax.Abstract.Name