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

type Args = [NamedArg Expr] #

data Expr #

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 QName	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 ExprInfo Expr (NamedArg Expr)	Ordinary (binary) application.
WithApp ExprInfo Expr [Expr]	With application.
Lam LamInfo LamBinding Expr	`λ bs → e`.
AbsurdLam LamInfo Hiding	`λ()` or `λ{}`.
ExtendedLam LamInfo 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 #	Does not compare `ScopeInfo` fields. Does not distinguish between prefix and postfix projections.
Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Data Expr #
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 #
Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
KillRange Expr #
Methods killRange :: KillRangeT Expr #
HasRange Expr #
Methods getRange :: Expr -> Range #
Underscore Expr #
Methods underscore :: Expr # isUnderscore :: Expr -> Bool #
IsProjP Expr #
Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) #
SubstExpr Assign #
Methods substExpr :: [(Name, Expr)] -> Assign -> Assign #
SubstExpr Expr #
Methods substExpr :: [(Name, Expr)] -> Expr -> Expr #
AllNames Expr #
Methods allNames :: Expr -> Seq QName #
ExprLike Expr #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Expr -> m Expr # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr # mapExpr :: (Expr -> Expr) -> Expr -> Expr #
MapNamedArgPattern NAP #
Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP #
PrettyTCM Expr #
Methods prettyTCM :: Expr -> TCM Doc #
ExpandPatternSynonyms Pattern #
Methods expandPatternSynonyms :: Pattern -> TCM Pattern #
IsFlexiblePattern Pattern #
Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Pattern -> TCM Bool #
UniverseBi Declaration Pattern #
Methods universeBi :: Declaration -> [Pattern] #
UniverseBi Declaration Expr #
Methods universeBi :: Declaration -> [Expr] #
ToConcrete Pattern Pattern #
Methods toConcrete :: Pattern -> AbsToCon Pattern # bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b #
ToConcrete LHSCore Pattern #
Methods toConcrete :: LHSCore -> AbsToCon Pattern # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b #
ToConcrete Expr Expr #
Methods toConcrete :: Expr -> AbsToCon Expr # bindToConcrete :: Expr -> (Expr -> AbsToCon b) -> AbsToCon b #
Reify MetaId Expr #
Methods reify :: MetaId -> TCM Expr # reifyWhen :: Bool -> MetaId -> TCM Expr #
Reify Literal Expr #
Methods reify :: Literal -> TCM Expr # reifyWhen :: Bool -> Literal -> TCM Expr #
Reify Level Expr #
Methods reify :: Level -> TCM Expr # reifyWhen :: Bool -> Level -> TCM Expr #
Reify Sort Expr #
Methods reify :: Sort -> TCM Expr # reifyWhen :: Bool -> Sort -> TCM Expr #
Reify Type Expr #
Methods reify :: Type -> TCM Expr # reifyWhen :: Bool -> Type -> TCM Expr #
Reify Term Expr #
Methods reify :: Term -> TCM Expr # reifyWhen :: Bool -> Term -> TCM Expr #
Reify Expr Expr #
Methods reify :: Expr -> TCM Expr # reifyWhen :: Bool -> Expr -> TCM Expr #
Reify DisplayTerm Expr #
Methods reify :: DisplayTerm -> TCM Expr # reifyWhen :: Bool -> DisplayTerm -> TCM Expr #
ToAbstract Literal Expr #
Methods toAbstract :: Literal -> WithNames Expr #
ToAbstract Sort Expr #
Methods toAbstract :: Sort -> WithNames Expr #
ToAbstract Term Expr #
Methods toAbstract :: Term -> WithNames Expr #
ToAbstract Expr Expr #
Methods toAbstract :: Expr -> ScopeM Expr #
ToAbstract OldQName Expr #
Methods toAbstract :: OldQName -> ScopeM Expr #
ToAbstract Pattern (Names, Pattern) #
Methods toAbstract :: Pattern -> WithNames (Names, Pattern) #
ToAbstract [Arg Term] [NamedArg Expr] #
Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] #
ToAbstract (Pattern' Expr) (Pattern' Expr) #
Methods toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr) #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) #
Methods toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr) #
ToAbstract (Expr, Elims) Expr #
Methods toAbstract :: (Expr, Elims) -> WithNames Expr #
ToAbstract (Expr, Elim) Expr #
Methods toAbstract :: (Expr, Elim) -> WithNames Expr #

type Assign = FieldAssignment' Expr #

Record field assignment f = e.

type Assigns = [Assign] #

type RecordAssign = Either Assign ModuleName #

type RecordAssigns = [RecordAssign] #

data Axiom #

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 #
Methods (==) :: Axiom -> Axiom -> Bool # (/=) :: Axiom -> Axiom -> Bool #
Data Axiom #
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 #
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 #
Methods showsPrec :: Int -> Axiom -> ShowS # show :: Axiom -> String # showList :: [Axiom] -> ShowS #

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

Renaming (generic).

data ScopeCopyInfo #

Constructors

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

Instances

Eq ScopeCopyInfo #
Methods (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool # (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool #
Data ScopeCopyInfo #
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 #
Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS # show :: ScopeCopyInfo -> String # showList :: [ScopeCopyInfo] -> ShowS #
Pretty ScopeCopyInfo #
Methods pretty :: ScopeCopyInfo -> Doc # prettyPrec :: Int -> ScopeCopyInfo -> Doc # prettyList :: [ScopeCopyInfo] -> Doc #
KillRange ScopeCopyInfo #
Methods killRange :: KillRangeT ScopeCopyInfo #

initCopyInfo :: ScopeCopyInfo #

data Declaration #

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 Bool) (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 #	Does not compare `ScopeInfo` fields.
Methods (==) :: Declaration -> Declaration -> Bool # (/=) :: Declaration -> Declaration -> Bool #
Data Declaration #
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 #
Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS #
KillRange Declaration #
Methods killRange :: KillRangeT Declaration #
HasRange Declaration #
Methods getRange :: Declaration -> Range #
GetDefInfo Declaration #
Methods getDefInfo :: Declaration -> Maybe DefInfo #
AnyAbstract Declaration #
Methods anyAbstract :: Declaration -> Bool #
AllNames Declaration #
Methods allNames :: Declaration -> Seq QName #
ExprLike Declaration #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Declaration -> m Declaration # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration #
ShowHead Declaration #
Methods showHead :: Declaration -> String #
UniverseBi Declaration RString #
Methods universeBi :: Declaration -> [RString] #
UniverseBi Declaration AmbiguousQName #
Methods universeBi :: Declaration -> [AmbiguousQName] #
UniverseBi Declaration ModuleName #
Methods universeBi :: Declaration -> [ModuleName] #
UniverseBi Declaration QName #
Methods universeBi :: Declaration -> [QName] #
UniverseBi Declaration ModuleInfo #
Methods universeBi :: Declaration -> [ModuleInfo] #
UniverseBi Declaration Pattern #
Methods universeBi :: Declaration -> [Pattern] #
UniverseBi Declaration TypedBinding #
Methods universeBi :: Declaration -> [TypedBinding] #
UniverseBi Declaration LamBinding #
Methods universeBi :: Declaration -> [LamBinding] #
UniverseBi Declaration LetBinding #
Methods universeBi :: Declaration -> [LetBinding] #
UniverseBi Declaration Declaration #
Methods universeBi :: Declaration -> [Declaration] #
UniverseBi Declaration Expr #
Methods universeBi :: Declaration -> [Expr] #
ToAbstract NiceDeclaration Declaration #
Methods toAbstract :: NiceDeclaration -> ScopeM Declaration #
UniverseBi Declaration (Pattern' Void) #
Methods universeBi :: Declaration -> [Pattern' Void] #
ToConcrete Declaration [Declaration] #
Methods toConcrete :: Declaration -> AbsToCon [Declaration] # bindToConcrete :: Declaration -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
ToConcrete (Constr Constructor) Declaration #
Methods toConcrete :: Constr Constructor -> AbsToCon Declaration # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b #
ToAbstract [Declaration] [Declaration] #
Methods toAbstract :: [Declaration] -> ScopeM [Declaration] #

class GetDefInfo a where #

Minimal complete definition

getDefInfo

Methods

getDefInfo :: a -> Maybe DefInfo #

Instances

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

type ImportDirective = ImportDirective' QName ModuleName #

type Renaming = Renaming' QName ModuleName #

type ImportedName = ImportedName' QName ModuleName #

data ModuleApplication #

Constructors

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

Instances

Eq ModuleApplication #
Methods (==) :: ModuleApplication -> ModuleApplication -> Bool # (/=) :: ModuleApplication -> ModuleApplication -> Bool #
Data ModuleApplication #
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 #
Methods showsPrec :: Int -> ModuleApplication -> ShowS # show :: ModuleApplication -> String # showList :: [ModuleApplication] -> ShowS #
KillRange ModuleApplication #
Methods killRange :: KillRangeT ModuleApplication #
AllNames ModuleApplication #
Methods allNames :: ModuleApplication -> Seq QName #
ExprLike ModuleApplication #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> ModuleApplication -> m ModuleApplication # foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication # mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication #
ToConcrete ModuleApplication ModuleApplication #
Methods toConcrete :: ModuleApplication -> AbsToCon ModuleApplication # bindToConcrete :: ModuleApplication -> (ModuleApplication -> AbsToCon b) -> AbsToCon b #

data Pragma #

Constructors

OptionsPragma [String]
BuiltinPragma String Expr
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 QName
DisplayPragma QName [NamedArg Pattern] Expr

Instances

Eq Pragma #
Methods (==) :: Pragma -> Pragma -> Bool # (/=) :: Pragma -> Pragma -> Bool #
Data Pragma #
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 #
Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
ExprLike Pragma #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pragma -> m Pragma # foldExpr :: Monoid m => (Expr -> m) -> Pragma -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> Pragma -> m Pragma # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma #
ToAbstract Pragma [Pragma] #
Methods toAbstract :: Pragma -> ScopeM [Pragma] #

data LetBinding #

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo Name 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 Name	Only used for highlighting. Refers to the first occurrence of `x` in `let x : A; x = e`.

Instances

Eq LetBinding #
Methods (==) :: LetBinding -> LetBinding -> Bool # (/=) :: LetBinding -> LetBinding -> Bool #
Data LetBinding #
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 #
Methods showsPrec :: Int -> LetBinding -> ShowS # show :: LetBinding -> String # showList :: [LetBinding] -> ShowS #
KillRange LetBinding #
Methods killRange :: KillRangeT LetBinding #
HasRange LetBinding #
Methods getRange :: LetBinding -> Range #
SubstExpr LetBinding #
Methods substExpr :: [(Name, Expr)] -> LetBinding -> LetBinding #
AllNames LetBinding #
Methods allNames :: LetBinding -> Seq QName #
ExprLike LetBinding #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LetBinding -> m LetBinding # foldExpr :: Monoid m => (Expr -> m) -> LetBinding -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> LetBinding -> m LetBinding # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding #
UniverseBi Declaration LetBinding #
Methods universeBi :: Declaration -> [LetBinding] #
ToConcrete LetBinding [Declaration] #
Methods toConcrete :: LetBinding -> AbsToCon [Declaration] # bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
ToAbstract LetDef [LetBinding] #
Methods toAbstract :: LetDef -> ScopeM [LetBinding] #
ToAbstract LetDefs [LetBinding] #
Methods toAbstract :: LetDefs -> ScopeM [LetBinding] #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) #
Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) #

type TypeSignature = Declaration #

Only Axioms.

type Constructor = TypeSignature #

type Field = TypeSignature #

data LamBinding #

A lambda binding is either domain free or typed.

Constructors

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

Instances

Eq LamBinding #
Methods (==) :: LamBinding -> LamBinding -> Bool # (/=) :: LamBinding -> LamBinding -> Bool #
Data LamBinding #
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 #
Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
KillRange LamBinding #
Methods killRange :: KillRangeT LamBinding #
HasRange LamBinding #
Methods getRange :: LamBinding -> Range #
LensHiding LamBinding #
Methods getHiding :: LamBinding -> Hiding # setHiding :: Hiding -> LamBinding -> LamBinding # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding #
AllNames LamBinding #
Methods allNames :: LamBinding -> Seq QName #
ExprLike LamBinding #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LamBinding -> m LamBinding # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding #
UniverseBi Declaration LamBinding #
Methods universeBi :: Declaration -> [LamBinding] #
ToAbstract LamBinding LamBinding #
Methods toAbstract :: LamBinding -> ScopeM LamBinding #
ToConcrete LamBinding [LamBinding] #
Methods toConcrete :: LamBinding -> AbsToCon [LamBinding] # bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b #

data TypedBindings #

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

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

Instances

Eq TypedBindings #
Methods (==) :: TypedBindings -> TypedBindings -> Bool # (/=) :: TypedBindings -> TypedBindings -> Bool #
Data TypedBindings #
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 #
Methods showsPrec :: Int -> TypedBindings -> ShowS # show :: TypedBindings -> String # showList :: [TypedBindings] -> ShowS #
KillRange TypedBindings #
Methods killRange :: KillRangeT TypedBindings #
HasRange TypedBindings #
Methods getRange :: TypedBindings -> Range #
LensHiding TypedBindings #
Methods getHiding :: TypedBindings -> Hiding # setHiding :: Hiding -> TypedBindings -> TypedBindings # mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings #
SubstExpr TypedBindings #
Methods substExpr :: [(Name, Expr)] -> TypedBindings -> TypedBindings #
AllNames TypedBindings #
Methods allNames :: TypedBindings -> Seq QName #
ExprLike TypedBindings #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBindings -> m TypedBindings # foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings # mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings #
Reify Telescope Telescope #
Methods reify :: Telescope -> TCM Telescope # reifyWhen :: Bool -> Telescope -> TCM Telescope #
ToAbstract TypedBindings TypedBindings #
Methods toAbstract :: TypedBindings -> ScopeM TypedBindings #
ToConcrete TypedBindings [TypedBindings] #
Methods toConcrete :: TypedBindings -> AbsToCon [TypedBindings] # bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings #
Methods toAbstract :: (Dom r, Name) -> WithNames TypedBindings #

data TypedBinding #

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 Name] 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 #
Methods (==) :: TypedBinding -> TypedBinding -> Bool # (/=) :: TypedBinding -> TypedBinding -> Bool #
Data TypedBinding #
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 #
Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
KillRange TypedBinding #
Methods killRange :: KillRangeT TypedBinding #
HasRange TypedBinding #
Methods getRange :: TypedBinding -> Range #
SubstExpr TypedBinding #
Methods substExpr :: [(Name, Expr)] -> TypedBinding -> TypedBinding #
AllNames TypedBinding #
Methods allNames :: TypedBinding -> Seq QName #
ExprLike TypedBinding #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> TypedBinding -> m TypedBinding # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding -> m TypedBinding # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding #
PrettyTCM TypedBinding #
Methods prettyTCM :: TypedBinding -> TCM Doc #
UniverseBi Declaration TypedBinding #
Methods universeBi :: Declaration -> [TypedBinding] #
ToConcrete TypedBinding TypedBinding #
Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding # bindToConcrete :: TypedBinding -> (TypedBinding -> AbsToCon b) -> AbsToCon b #
ToAbstract TypedBinding TypedBinding #
Methods toAbstract :: TypedBinding -> ScopeM TypedBinding #

type Telescope = [TypedBindings] #

data NamedDotPattern #

Constructors

NamedDot Name Term Type

Instances

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

data StrippedDotPattern #

Constructors

StrippedDot Expr Term Type

Instances

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

data Clause' lhs #

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
clauseNamedDots :: [NamedDotPattern]
Only in with-clauses where we inherit some already checked dot patterns from the parent. These live in the context of the parent clause left-hand side.
clauseStrippedDots :: [StrippedDotPattern]
In with-clauses where a dot pattern from the parent clause is repeated in the with-clause. In this case it's not actually part of the clause, but it still needs to be checked (Issue 142).
clauseRHS :: RHS
clauseWhereDecls :: [Declaration]
clauseCatchall :: Bool

Instances

Functor Clause' #
Methods fmap :: (a -> b) -> Clause' a -> Clause' b # (<$) :: a -> Clause' b -> Clause' a #
Foldable Clause' #
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' #
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 #
Methods allNames :: Clause -> Seq QName #
LHSToSpine Clause SpineClause #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause # spineToLhs :: SpineClause -> Clause #
Reify NamedClause Clause #
Methods reify :: NamedClause -> TCM Clause # reifyWhen :: Bool -> NamedClause -> TCM Clause #
ToAbstract Clause Clause #
Methods toAbstract :: Clause -> ScopeM Clause #
Eq lhs => Eq (Clause' lhs) #
Methods (==) :: Clause' lhs -> Clause' lhs -> Bool # (/=) :: Clause' lhs -> Clause' lhs -> Bool #
Data lhs => Data (Clause' lhs) #
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) #
Methods showsPrec :: Int -> Clause' lhs -> ShowS # show :: Clause' lhs -> String # showList :: [Clause' lhs] -> ShowS #
KillRange a => KillRange (Clause' a) #
Methods killRange :: KillRangeT (Clause' a) #
HasRange a => HasRange (Clause' a) #
Methods getRange :: Clause' a -> Range #
ExprLike a => ExprLike (Clause' a) #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Clause' a -> m (Clause' a) # foldExpr :: Monoid m => (Expr -> m) -> Clause' a -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> Clause' a -> m (Clause' a) # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a #
Reify (QNamed Clause) Clause #
Methods reify :: QNamed Clause -> TCM Clause # reifyWhen :: Bool -> QNamed Clause -> TCM Clause #
ToAbstract (QNamed Clause) Clause #
Methods toAbstract :: QNamed Clause -> WithNames Clause #
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] #
Methods toConcrete :: Clause' a -> AbsToCon [Declaration] # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
ToAbstract [QNamed Clause] [Clause] #
Methods toAbstract :: [QNamed Clause] -> WithNames [Clause] #

type Clause = Clause' LHS #

type SpineClause = Clause' SpineLHS #

data RHS #

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`. rewriteRHS :: RHS The RHS should not be another `RewriteRHS`. rewriteWhereDecls :: [Declaration] The where clauses are attached to the `RewriteRHS` by

Instances

Eq RHS #
Methods (==) :: RHS -> RHS -> Bool # (/=) :: RHS -> RHS -> Bool #
Data RHS #
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 #
Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
KillRange RHS #
Methods killRange :: KillRangeT RHS #
HasRange RHS #
Methods getRange :: RHS -> Range #
AllNames RHS #
Methods allNames :: RHS -> Seq QName #
ExprLike RHS #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> RHS -> m RHS # foldExpr :: Monoid m => (Expr -> m) -> RHS -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> RHS -> m RHS # mapExpr :: (Expr -> Expr) -> RHS -> RHS #
ToAbstract AbstractRHS RHS #
Methods toAbstract :: AbstractRHS -> ScopeM RHS #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) #
Methods toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration]) # bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #

data SpineLHS #

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] Function parameters (patterns). spLhsWithPats :: [Pattern] `with` patterns (after `\|`).

Instances

Eq SpineLHS #
Methods (==) :: SpineLHS -> SpineLHS -> Bool # (/=) :: SpineLHS -> SpineLHS -> Bool #
Data SpineLHS #
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 #
Methods showsPrec :: Int -> SpineLHS -> ShowS # show :: SpineLHS -> String # showList :: [SpineLHS] -> ShowS #
KillRange SpineLHS #
Methods killRange :: KillRangeT SpineLHS #
HasRange SpineLHS #
Methods getRange :: SpineLHS -> Range #
ExprLike SpineLHS #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> SpineLHS -> m SpineLHS # foldExpr :: Monoid m => (Expr -> m) -> SpineLHS -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> SpineLHS -> m SpineLHS # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS #
LHSToSpine LHS SpineLHS #	LHS instance.
Methods lhsToSpine :: LHS -> SpineLHS # spineToLhs :: SpineLHS -> LHS #
LHSToSpine Clause SpineClause #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause # spineToLhs :: SpineClause -> Clause #
ToConcrete SpineLHS LHS #
Methods toConcrete :: SpineLHS -> AbsToCon LHS # bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b #

data LHS #

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. lhsWithPats :: [Pattern] `with` patterns (after `\|`).

Instances

Eq LHS #
Methods (==) :: LHS -> LHS -> Bool # (/=) :: LHS -> LHS -> Bool #
Data LHS #
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 #
Methods showsPrec :: Int -> LHS -> ShowS # show :: LHS -> String # showList :: [LHS] -> ShowS #
KillRange LHS #
Methods killRange :: KillRangeT LHS #
HasRange LHS #
Methods getRange :: LHS -> Range #
AllNames Clause #
Methods allNames :: Clause -> Seq QName #
ExprLike LHS #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHS -> m LHS # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS # mapExpr :: (Expr -> Expr) -> LHS -> LHS #
LHSToSpine LHS SpineLHS #	LHS instance.
Methods lhsToSpine :: LHS -> SpineLHS # spineToLhs :: SpineLHS -> LHS #
LHSToSpine Clause SpineClause #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause # spineToLhs :: SpineClause -> Clause #
ToConcrete LHS LHS #
Methods toConcrete :: LHS -> AbsToCon LHS # bindToConcrete :: LHS -> (LHS -> AbsToCon b) -> AbsToCon b #
Reify NamedClause Clause #
Methods reify :: NamedClause -> TCM Clause # reifyWhen :: Bool -> NamedClause -> TCM Clause #
ToAbstract Clause Clause #
Methods toAbstract :: Clause -> ScopeM Clause #
ToAbstract LeftHandSide LHS #
Methods toAbstract :: LeftHandSide -> ScopeM LHS #
Reify (QNamed Clause) Clause #
Methods reify :: QNamed Clause -> TCM Clause # reifyWhen :: Bool -> QNamed Clause -> TCM Clause #
ToAbstract (QNamed Clause) Clause #
Methods toAbstract :: QNamed Clause -> WithNames Clause #
ToAbstract [QNamed Clause] [Clause] #
Methods toAbstract :: [QNamed Clause] -> WithNames [Clause] #

data LHSCore' e #

The lhs minus with-patterns in projection-application 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 branch. lhsPatsRight :: [NamedArg (Pattern' e)] Further applied to patterns.

Instances

Functor LHSCore' #
Methods fmap :: (a -> b) -> LHSCore' a -> LHSCore' b # (<$) :: a -> LHSCore' b -> LHSCore' a #
Foldable LHSCore' #
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' #
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 #
Methods toConcrete :: LHSCore -> AbsToCon Pattern # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b #
ToAbstract LHSCore (LHSCore' Expr) #
Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) #
Eq e => Eq (LHSCore' e) #
Methods (==) :: LHSCore' e -> LHSCore' e -> Bool # (/=) :: LHSCore' e -> LHSCore' e -> Bool #
Data e => Data (LHSCore' e) #
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) #
Methods showsPrec :: Int -> LHSCore' e -> ShowS # show :: LHSCore' e -> String # showList :: [LHSCore' e] -> ShowS #
KillRange e => KillRange (LHSCore' e) #
Methods killRange :: KillRangeT (LHSCore' e) #
HasRange (LHSCore' e) #
Methods getRange :: LHSCore' e -> Range #
ExprLike a => ExprLike (LHSCore' a) #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) # foldExpr :: Monoid m => (Expr -> m) -> LHSCore' a -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> LHSCore' a -> m (LHSCore' a) # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) #
Methods toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr) #

type LHSCore = LHSCore' Expr #

class LHSToSpine a b where #

Convert a focused lhs to spine view and back.

Minimal complete definition

lhsToSpine, spineToLhs

Methods

lhsToSpine :: a -> b #

spineToLhs :: b -> a #

Instances

LHSToSpine LHS SpineLHS #	LHS instance.
Methods lhsToSpine :: LHS -> SpineLHS # spineToLhs :: SpineLHS -> LHS #
LHSToSpine Clause SpineClause #	Clause instance.
Methods lhsToSpine :: Clause -> SpineClause # spineToLhs :: SpineClause -> Clause #
LHSToSpine a b => LHSToSpine [a] [b] #	List instance (for clauses).
Methods lhsToSpine :: [a] -> [b] # spineToLhs :: [b] -> [a] #

lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)] #

spineToLhsCore :: IsProjP e => QNamed [NamedArg (Pattern' e)] -> LHSCore' e #

lhsCoreApp :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e #

Add applicative patterns (non-projection patterns) to the right.

lhsCoreAddSpine :: IsProjP e => LHSCore' e -> [NamedArg (Pattern' e)] -> LHSCore' e #

Add projection and applicative patterns to the right.

lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e] #

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern #

Used in AbstractToConcrete.

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore #

Patterns

data Pattern' e #

Parameterised over the type of dot patterns.

Constructors

VarP Name
ConP ConPatInfo AmbiguousQName [NamedArg (Pattern' e)]
ProjP PatInfo ProjOrigin AmbiguousQName	Destructor pattern `d`.
DefP PatInfo AmbiguousQName [NamedArg (Pattern' 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 Name (Pattern' e)
DotP PatInfo Origin e	Dot pattern `.e`: the Origin keeps track whether this dot pattern was written by the user or inserted by the system (e.g. while expanding the ellipsis in a with clause).
AbsurdP PatInfo
LitP Literal
PatternSynP PatInfo QName [NamedArg (Pattern' e)]
RecP PatInfo [FieldAssignment' (Pattern' e)]

Instances

Functor Pattern' #
Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b # (<$) :: a -> Pattern' b -> Pattern' a #
Foldable Pattern' #
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' #
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 #
Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP #
ExpandPatternSynonyms Pattern #
Methods expandPatternSynonyms :: Pattern -> TCM Pattern #
IsFlexiblePattern Pattern #
Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Pattern -> TCM Bool #
UniverseBi Declaration Pattern #
Methods universeBi :: Declaration -> [Pattern] #
ToConcrete Pattern Pattern #
Methods toConcrete :: Pattern -> AbsToCon Pattern # bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b #
UniverseBi Declaration (Pattern' Void) #
Methods universeBi :: Declaration -> [Pattern' Void] #
APatternLike a (Pattern' a) #
Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) #
ToAbstract Pattern (Pattern' Expr) #
Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) #
ToAbstract Pattern (Names, Pattern) #
Methods toAbstract :: Pattern -> WithNames (Names, Pattern) #
Eq e => Eq (Pattern' e) #
Methods (==) :: Pattern' e -> Pattern' e -> Bool # (/=) :: Pattern' e -> Pattern' e -> Bool #
Data e => Data (Pattern' e) #
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) #
Methods showsPrec :: Int -> Pattern' e -> ShowS # show :: Pattern' e -> String # showList :: [Pattern' e] -> ShowS #
KillRange e => KillRange (Pattern' e) #
Methods killRange :: KillRangeT (Pattern' e) #
SetRange (Pattern' a) #
Methods setRange :: Range -> Pattern' a -> Pattern' a #
HasRange (Pattern' e) #
Methods getRange :: Pattern' e -> Range #
IsProjP (Pattern' e) #
Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) #
IsProjP e => MaybePostfixProjP (Pattern' e) #
Methods maybePostfixProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) #
ExprLike a => ExprLike (Pattern' a) #
Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> Pattern' a -> m (Pattern' a) # foldExpr :: Monoid m => (Expr -> m) -> Pattern' a -> m # traverseExpr :: Monad m => (Expr -> m Expr) -> Pattern' a -> m (Pattern' a) # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a #
NamesIn (Pattern' a) #
Methods namesIn :: Pattern' a -> Set QName #
ToAbstract (Pattern' Expr) (Pattern' Expr) #
Methods toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr) #

type Pattern = Pattern' Expr #

type Patterns = [NamedArg Pattern] #

class MaybePostfixProjP a where #

Minimal complete definition

maybePostfixProjP

Methods

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

Instances

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

class AllNames a where #

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 #

Instances

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

axiomName :: Declaration -> QName #

The name defined by the given axiom.

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

class AnyAbstract a where #

Are we in an abstract block?

In that case some definition is abstract.

Minimal complete definition

anyAbstract

Methods

anyAbstract :: a -> Bool #

Instances

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

nameExpr :: AbstractName -> Expr #

Turn an AbstractName to an expression.

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

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

patternToExpr :: Pattern -> Expr #

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

type PatternSynDefns = Map QName PatternSynDefn #

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

substPattern :: [(Name, Pattern)] -> Pattern -> Pattern #

class SubstExpr a where #

Minimal complete definition

substExpr

Methods

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

Instances

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

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

module Agda.Syntax.Abstract.Name