Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete

Contents

Expressions
Bindings
Declarations

Description

The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.

Synopsis

data Expr
- = Ident QName
- | Lit Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe String)
- | RawApp Range [Expr]
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))]
- | WithApp Range Expr [Expr]
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range [LamBinding] Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range [LamClause]
- | Fun Range Expr Expr
- | Pi Telescope Expr
- | Set Range
- | Prop Range
- | SetN Range Integer
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range [Declaration] (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range Expr
- | DoBlock Range [DoStmt]
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | ETel Telescope
- | QuoteGoal Range Name Expr
- | QuoteContext Range
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr [Expr]
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
data OpApp e
- = SyntaxBindingLambda Range [LamBinding] e
- | Ordinary e
fromOrdinary :: e -> OpApp e -> e
module Agda.Syntax.Concrete.Name
appView :: Expr -> AppView
data AppView = AppView Expr [NamedArg Expr]
type LamBinding = LamBinding' TypedBindings
data LamBinding' a
- = DomainFree ArgInfo BoundName
- | DomainFull a
type TypedBindings = TypedBindings' TypedBinding
data TypedBindings' a = TypedBindings Range (Arg a)
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
- = TBind Range [WithHiding BoundName] e
- | TLet Range [Declaration]
type RecordAssignment = Either FieldAssignment ModuleAssignment
type RecordAssignments = [RecordAssignment]
type FieldAssignment = FieldAssignment' Expr
data FieldAssignment' a = FieldAssignment {
- _nameFieldA :: Name
- _exprFieldA :: a
}
nameFieldA :: Lens' Name (FieldAssignment' a)
exprFieldA :: Lens' a (FieldAssignment' a)
data ModuleAssignment = ModuleAssignment {
- _qnameModA :: QName
- _exprModA :: [Expr]
- _importDirModA :: ImportDirective
}
data BoundName = BName {
- boundName :: Name
- boundLabel :: Name
- bnameFixity :: Fixity'
}
mkBoundName_ :: Name -> BoundName
mkBoundName :: Name -> Fixity' -> BoundName
type Telescope = [TypedBindings]
countTelVars :: Telescope -> Nat
data Declaration
- = TypeSig ArgInfo Name Expr
- | Field IsInstance Name (Arg Expr)
- | FunClause LHS RHS WhereClause Bool
- | DataSig Range Induction Name [LamBinding] Expr
- | Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name [LamBinding] Expr
- | Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] (Maybe Expr) [Declaration]
- | Infix Fixity [Name]
- | Syntax Name Notation
- | PatternSyn Range Name [Arg Name] Pattern
- | Mutual Range [Declaration]
- | Abstract Range [Declaration]
- | Private Range Origin [Declaration]
- | InstanceB Range [Declaration]
- | Macro Range [Declaration]
- | Postulate Range [TypeSignatureOrInstanceBlock]
- | Primitive Range [TypeSignature]
- | Open Range QName ImportDirective
- | Import Range QName (Maybe AsName) !OpenShortHand ImportDirective
- | ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective
- | Module Range QName [TypedBindings] [Declaration]
- | UnquoteDecl Range [Name] Expr
- | UnquoteDef Range [Name] Expr
- | Pragma Pragma
data ModuleApplication
- = SectionApp Range [TypedBindings] Expr
- | RecordModuleIFS Range QName
type TypeSignature = Declaration
type TypeSignatureOrInstanceBlock = Declaration
type ImportDirective = ImportDirective' Name Name
type Using = Using' Name Name
type ImportedName = ImportedName' Name Name
type Renaming = Renaming' Name Name
data AsName = AsName {
- asName :: Name
- asRange :: Range
}
data OpenShortHand
- = DoOpen
- | DontOpen
type RewriteEqn = Expr
type WithExpr = Expr
data LHS = LHS {
- lhsOriginalPattern :: Pattern
- lhsRewriteEqn :: [RewriteEqn]
- lhsWithExpr :: [WithExpr]
}
data Pattern
- = IdentP QName
- | QuoteP Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP Range [Pattern]
- | OpAppP Range QName (Set Name) [NamedArg Pattern]
- | HiddenP Range (Named_ Pattern)
- | InstanceP Range (Named_ Pattern)
- | ParenP Range Pattern
- | WildP Range
- | AbsurdP Range
- | AsP Range Name Pattern
- | DotP Range Expr
- | LitP Literal
- | RecP Range [FieldAssignment' Pattern]
- | EllipsisP Range
- | WithP Range Pattern
data LHSCore
- = LHSHead {
  - lhsDefName :: QName
  - lhsPats :: [NamedArg Pattern]
  }
- | LHSProj {
  - lhsDestructor :: QName
  - lhsPatsLeft :: [NamedArg Pattern]
  - lhsFocus :: NamedArg LHSCore
  - lhsPats :: [NamedArg Pattern]
  }
- | LHSWith {
  - lhsHead :: LHSCore
  - lhsWithPatterns :: [Pattern]
  - lhsPats :: [NamedArg Pattern]
  }
data LamClause = LamClause {
- lamLHS :: LHS
- lamRHS :: RHS
- lamWhere :: WhereClause
- lamCatchAll :: Bool
}
type RHS = RHS' Expr
data RHS' e
- = AbsurdRHS
- | RHS e
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
- = NoWhere
- | AnyWhere decls
- | SomeWhere Name Access decls
data ExprWhere = ExprWhere Expr WhereClause
data DoStmt
- = DoBind Range Pattern Expr [LamClause]
- | DoThen Expr
- | DoLet Range [Declaration]
data Pragma
- = OptionsPragma Range [String]
- | BuiltinPragma Range String QName
- | RewritePragma Range [QName]
- | CompiledDataPragma Range QName String [String]
- | CompiledTypePragma Range QName String
- | CompiledPragma Range QName String
- | CompiledExportPragma Range QName String
- | CompiledJSPragma Range QName String
- | CompiledUHCPragma Range QName String
- | CompiledDataUHCPragma Range QName String [String]
- | HaskellCodePragma Range String
- | ForeignPragma Range String String
- | CompilePragma Range String QName String
- | StaticPragma Range QName
- | InjectivePragma Range QName
- | InlinePragma Range Bool QName
- | ImportPragma Range String
- | ImportUHCPragma Range String
- | ImpossiblePragma Range
- | EtaPragma Range QName
- | TerminationCheckPragma Range (TerminationCheck Name)
- | WarningOnUsage Range QName String
- | CatchallPragma Range
- | DisplayPragma Range Pattern Expr
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
type Module = ([Pragma], [Declaration])
data ThingWithFixity x = ThingWithFixity x Fixity'
type HoleContent = HoleContent' Expr
data HoleContent' e
- = HoleContentExpr e
- | HoleContentRewrite [e]
topLevelModuleName :: Module -> TopLevelModuleName
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])

Expressions

data Expr #

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName	ex: `x`
Lit Literal	ex: `1` or `"foo"`
QuestionMark Range (Maybe Nat)	ex: `?` or `{! ... !}`
Underscore Range (Maybe String)	ex: `_` or `_A_5`
RawApp Range [Expr]	before parsing operators
App Range Expr (NamedArg Expr)	ex: `e e`, `e {e}`, or `e {x = e}`
OpApp Range QName (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))]	ex: `e + e` The `QName` is possibly ambiguous, but it must correspond to one of the names in the set.
WithApp Range Expr [Expr]	ex: `e \| e1 \| .. \| en`
HiddenArg Range (Named_ Expr)	ex: `{e}` or `{x=e}`
InstanceArg Range (Named_ Expr)	ex: `{{e}}` or `{{x=e}}`
Lam Range [LamBinding] Expr	ex: `\x {y} -> e` or `\(x:A){y:B} -> e`
AbsurdLam Range Hiding	ex: `\ ()`
ExtendedLam Range [LamClause]	ex: `\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }`
Fun Range Expr Expr	ex: `e -> e` or `.e -> e` (NYI: `{e} -> e`)
Pi Telescope Expr	ex: `(xs:e) -> e` or `{xs:e} -> e`
Set Range	ex: `Set`
Prop Range	ex: `Prop`
SetN Range Integer	ex: `Set0, Set1, ..`
Rec Range RecordAssignments	ex: `record {x = a; y = b}`, or `record { x = a; M1; M2 }`
RecUpdate Range Expr [FieldAssignment]	ex: `record e {x = a; y = b}`
Let Range [Declaration] (Maybe Expr)	ex: `let Ds in e`, missing body when parsing do-notation let
Paren Range Expr	ex: `(e)`
IdiomBrackets Range Expr	ex: `(\| e \|)`
DoBlock Range [DoStmt]	ex: `do x <- m1; m2`
Absurd Range	ex: `()` or `{}`, only in patterns
As Range Name Expr	ex: `x@p`, only in patterns
Dot Range Expr	ex: `.p`, only in patterns
ETel Telescope	only used for printing telescopes
QuoteGoal Range Name Expr	ex: `quoteGoal x in e`
QuoteContext Range	ex: `quoteContext`
Quote Range	ex: `quote`, should be applied to a name
QuoteTerm Range	ex: `quoteTerm`, should be applied to a term
Tactic Range Expr [Expr]	tactic solve \| subgoal1 \| .. \| subgoalN
Unquote Range	ex: `unquote`, should be applied to a term of type `Term`
DontCare Expr	to print irrelevant things
Equal Range Expr Expr	ex: `a = b`, used internally in the parser
Ellipsis Range	`...`, used internally to parse patterns.

Instances

Data Expr #
Instance details Defined in Agda.Syntax.Concrete 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 RHS #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
Show TypedBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
Show TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBindings -> ShowS # show :: TypedBindings -> String # showList :: [TypedBindings] -> ShowS #
Show LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Show Expr #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
NFData Expr #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Expr -> () #
Pretty RHS #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RHS -> Doc # prettyPrec :: Int -> RHS -> Doc # prettyList :: [RHS] -> Doc #
Pretty TypedBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc # prettyPrec :: Int -> TypedBinding -> Doc # prettyList :: [TypedBinding] -> Doc #
Pretty TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBindings -> Doc # prettyPrec :: Int -> TypedBindings -> Doc # prettyList :: [TypedBindings] -> Doc #
Pretty LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc # prettyPrec :: Int -> LamBinding -> Doc # prettyList :: [LamBinding] -> Doc #
Pretty Expr #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Expr -> Doc # prettyPrec :: Int -> Expr -> Doc # prettyList :: [Expr] -> Doc #
KillRange RHS #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS #
KillRange TypedBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding #
KillRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBindings #
KillRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding #
KillRange Expr #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Expr #
SetRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBindings -> TypedBindings #
HasRange RHS #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range #
HasRange TypedBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range #
HasRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBindings -> Range #
HasRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range #
HasRange Expr #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Expr -> Range #
LensRelevance TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBindings -> Relevance # setRelevance :: Relevance -> TypedBindings -> TypedBindings # mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings #
LensHiding TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBindings -> Hiding # setHiding :: Hiding -> TypedBindings -> TypedBindings # mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings #
LensHiding LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding # setHiding :: Hiding -> LamBinding -> LamBinding # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding #
IsExpr Expr #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Expr -> ExprView Expr # unExprView :: ExprView Expr -> Expr #
ExprLike TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings # foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m #
ExprLike LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m #
ExprLike Expr #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Expr -> Expr # traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr # foldExpr :: Monoid m => (Expr -> m) -> Expr -> m #
ExprLike FieldAssignment #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m #
ToConcrete InteractionId Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: InteractionId -> AbsToCon Expr # bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b #
ToConcrete TypedBinding TypedBinding #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding0 # bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b #
ToConcrete Expr Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Expr -> AbsToCon Expr0 # bindToConcrete :: Expr -> (Expr0 -> AbsToCon b) -> AbsToCon b #
ToConcrete NamedMeta Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: NamedMeta -> AbsToCon Expr # bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b #
ToAbstract HoleContent HoleContent #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: HoleContent0 -> ScopeM HoleContent #
ToAbstract RHS AbstractRHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS #
ToAbstract TypedBinding TypedBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBinding0 -> ScopeM TypedBinding #
ToAbstract TypedBindings TypedBindings #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBindings0 -> ScopeM TypedBindings #
ToAbstract LamBinding LamBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding #
ToAbstract Expr Expr #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Expr0 -> ScopeM Expr #
ToConcrete TypedBindings [TypedBindings] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBindings -> AbsToCon [TypedBindings0] # bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b #
ToConcrete LamBinding [LamBinding] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon [LamBinding0] # bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b #
ToAbstract LHSCore (LHSCore' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) #
ToAbstract Pattern (Pattern' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #
Pretty (OpApp Expr) #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpApp Expr -> Doc # prettyPrec :: Int -> OpApp Expr -> Doc # prettyList :: [OpApp Expr] -> Doc #
ToAbstract (Pattern' Expr) (Pattern' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern' Expr0 -> ScopeM (Pattern' Expr) #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore' Expr0 -> ScopeM (LHSCore' Expr) #

data OpApp e #

Constructors

SyntaxBindingLambda Range [LamBinding] e	An abstraction inside a special syntax declaration (see Issue 358 why we introduce this).
Ordinary e

Instances

Functor OpApp #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> OpApp a -> OpApp b # (<$) :: a -> OpApp b -> OpApp a #
Foldable OpApp #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => OpApp m -> m # foldMap :: Monoid m => (a -> m) -> OpApp a -> m # foldr :: (a -> b -> b) -> b -> OpApp a -> b # foldr' :: (a -> b -> b) -> b -> OpApp a -> b # foldl :: (b -> a -> b) -> b -> OpApp a -> b # foldl' :: (b -> a -> b) -> b -> OpApp a -> b # foldr1 :: (a -> a -> a) -> OpApp a -> a # foldl1 :: (a -> a -> a) -> OpApp a -> a # toList :: OpApp a -> [a] # null :: OpApp a -> Bool # length :: OpApp a -> Int # elem :: Eq a => a -> OpApp a -> Bool # maximum :: Ord a => OpApp a -> a # minimum :: Ord a => OpApp a -> a # sum :: Num a => OpApp a -> a # product :: Num a => OpApp a -> a #
Traversable OpApp #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> OpApp a -> f (OpApp b) # sequenceA :: Applicative f => OpApp (f a) -> f (OpApp a) # mapM :: Monad m => (a -> m b) -> OpApp a -> m (OpApp b) # sequence :: Monad m => OpApp (m a) -> m (OpApp a) #
Data e => Data (OpApp e) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpApp e -> c (OpApp e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e) # toConstr :: OpApp e -> Constr # dataTypeOf :: OpApp e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e)) # gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r # gmapQ :: (forall d. Data d => d -> u) -> OpApp e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> OpApp e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) #
NFData a => NFData (OpApp a) #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: OpApp a -> () #
Pretty (OpApp Expr) #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpApp Expr -> Doc # prettyPrec :: Int -> OpApp Expr -> Doc # prettyList :: [OpApp Expr] -> Doc #
KillRange e => KillRange (OpApp e) #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) #
HasRange e => HasRange (OpApp e) #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: OpApp e -> Range #
ExprLike a => ExprLike (OpApp a) #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a # traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a) # foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m #

fromOrdinary :: e -> OpApp e -> e #

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView #

data AppView #

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr]

Bindings

type LamBinding = LamBinding' TypedBindings #

A lambda binding is either domain free or typed.

data LamBinding' a #

Constructors

DomainFree ArgInfo BoundName	. `x` or `{x}` or `.x` or `.{x}` or `{.x}`
DomainFull a	. `(xs : e)` or `{xs : e}`

Instances

Functor LamBinding' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b # (<$) :: a -> LamBinding' b -> LamBinding' a #
Show LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Foldable LamBinding' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => LamBinding' m -> m # foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m # foldr :: (a -> b -> b) -> b -> LamBinding' a -> b # foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b # foldl :: (b -> a -> b) -> b -> LamBinding' a -> b # foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b # foldr1 :: (a -> a -> a) -> LamBinding' a -> a # foldl1 :: (a -> a -> a) -> LamBinding' a -> a # toList :: LamBinding' a -> [a] # null :: LamBinding' a -> Bool # length :: LamBinding' a -> Int # elem :: Eq a => a -> LamBinding' a -> Bool # maximum :: Ord a => LamBinding' a -> a # minimum :: Ord a => LamBinding' a -> a # sum :: Num a => LamBinding' a -> a # product :: Num a => LamBinding' a -> a #
Traversable LamBinding' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) # sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) # mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) # sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) #
Pretty LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc # prettyPrec :: Int -> LamBinding -> Doc # prettyList :: [LamBinding] -> Doc #
KillRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding #
HasRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range #
LensHiding LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding # setHiding :: Hiding -> LamBinding -> LamBinding # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding #
ExprLike LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m #
ToAbstract LamBinding LamBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding #
ToConcrete LamBinding [LamBinding] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon [LamBinding0] # bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b #
Data a => Data (LamBinding' a) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding' a -> c (LamBinding' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LamBinding' a) # toConstr :: LamBinding' a -> Constr # dataTypeOf :: LamBinding' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LamBinding' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LamBinding' a)) # gmapT :: (forall b. Data b => b -> b) -> LamBinding' a -> LamBinding' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r # gmapQ :: (forall d. Data d => d -> u) -> LamBinding' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) #
NFData a => NFData (LamBinding' a) #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamBinding' a -> () #

type TypedBindings = TypedBindings' TypedBinding #

A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.

If the individual binding contains hiding information as well, the Hiding in TypedBindings must be the unit NotHidden.

data TypedBindings' a #

Constructors

TypedBindings Range (Arg a)

. (xs : e) or {xs : e} or something like (x {y} _ : e).

Instances

Functor TypedBindings' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> TypedBindings' a -> TypedBindings' b # (<$) :: a -> TypedBindings' b -> TypedBindings' a #
Show TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBindings -> ShowS # show :: TypedBindings -> String # showList :: [TypedBindings] -> ShowS #
Show LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Foldable TypedBindings' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => TypedBindings' m -> m # foldMap :: Monoid m => (a -> m) -> TypedBindings' a -> m # foldr :: (a -> b -> b) -> b -> TypedBindings' a -> b # foldr' :: (a -> b -> b) -> b -> TypedBindings' a -> b # foldl :: (b -> a -> b) -> b -> TypedBindings' a -> b # foldl' :: (b -> a -> b) -> b -> TypedBindings' a -> b # foldr1 :: (a -> a -> a) -> TypedBindings' a -> a # foldl1 :: (a -> a -> a) -> TypedBindings' a -> a # toList :: TypedBindings' a -> [a] # null :: TypedBindings' a -> Bool # length :: TypedBindings' a -> Int # elem :: Eq a => a -> TypedBindings' a -> Bool # maximum :: Ord a => TypedBindings' a -> a # minimum :: Ord a => TypedBindings' a -> a # sum :: Num a => TypedBindings' a -> a # product :: Num a => TypedBindings' a -> a #
Traversable TypedBindings' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TypedBindings' a -> f (TypedBindings' b) # sequenceA :: Applicative f => TypedBindings' (f a) -> f (TypedBindings' a) # mapM :: Monad m => (a -> m b) -> TypedBindings' a -> m (TypedBindings' b) # sequence :: Monad m => TypedBindings' (m a) -> m (TypedBindings' a) #
Pretty TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBindings -> Doc # prettyPrec :: Int -> TypedBindings -> Doc # prettyList :: [TypedBindings] -> Doc #
Pretty LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc # prettyPrec :: Int -> LamBinding -> Doc # prettyList :: [LamBinding] -> Doc #
KillRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBindings #
KillRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding #
SetRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBindings -> TypedBindings #
HasRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBindings -> Range #
HasRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range #
LensRelevance TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBindings -> Relevance # setRelevance :: Relevance -> TypedBindings -> TypedBindings # mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings #
LensHiding TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBindings -> Hiding # setHiding :: Hiding -> TypedBindings -> TypedBindings # mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings #
LensHiding LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding # setHiding :: Hiding -> LamBinding -> LamBinding # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding #
ExprLike TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings # foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m #
ExprLike LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m #
ToAbstract TypedBindings TypedBindings #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBindings0 -> ScopeM TypedBindings #
ToAbstract LamBinding LamBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding #
ToConcrete TypedBindings [TypedBindings] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBindings -> AbsToCon [TypedBindings0] # bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b #
ToConcrete LamBinding [LamBinding] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon [LamBinding0] # bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b #
Data a => Data (TypedBindings' a) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBindings' a -> c (TypedBindings' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedBindings' a) # toConstr :: TypedBindings' a -> Constr # dataTypeOf :: TypedBindings' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedBindings' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypedBindings' a)) # gmapT :: (forall b. Data b => b -> b) -> TypedBindings' a -> TypedBindings' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBindings' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBindings' a -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedBindings' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBindings' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBindings' a -> m (TypedBindings' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBindings' a -> m (TypedBindings' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBindings' a -> m (TypedBindings' a) #
NFData a => NFData (TypedBindings' a) #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: TypedBindings' a -> () #

type TypedBinding = TypedBinding' Expr #

A typed binding.

data TypedBinding' e #

Constructors

TBind Range [WithHiding BoundName] e	Binding `(x1 ... xn : A)`.
TLet Range [Declaration]	Let binding `(let Ds)` or `(open M args)`.

Instances

Functor TypedBinding' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b # (<$) :: a -> TypedBinding' b -> TypedBinding' a #
Show TypedBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
Show TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBindings -> ShowS # show :: TypedBindings -> String # showList :: [TypedBindings] -> ShowS #
Show LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
Foldable TypedBinding' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => TypedBinding' m -> m # foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m # foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b # foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b # foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b # foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b # foldr1 :: (a -> a -> a) -> TypedBinding' a -> a # foldl1 :: (a -> a -> a) -> TypedBinding' a -> a # toList :: TypedBinding' a -> [a] # null :: TypedBinding' a -> Bool # length :: TypedBinding' a -> Int # elem :: Eq a => a -> TypedBinding' a -> Bool # maximum :: Ord a => TypedBinding' a -> a # minimum :: Ord a => TypedBinding' a -> a # sum :: Num a => TypedBinding' a -> a # product :: Num a => TypedBinding' a -> a #
Traversable TypedBinding' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b) # sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a) # mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b) # sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a) #
Pretty TypedBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc # prettyPrec :: Int -> TypedBinding -> Doc # prettyList :: [TypedBinding] -> Doc #
Pretty TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBindings -> Doc # prettyPrec :: Int -> TypedBindings -> Doc # prettyList :: [TypedBindings] -> Doc #
Pretty LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc # prettyPrec :: Int -> LamBinding -> Doc # prettyList :: [LamBinding] -> Doc #
KillRange TypedBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding #
KillRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBindings #
KillRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding #
SetRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBindings -> TypedBindings #
HasRange TypedBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range #
HasRange TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBindings -> Range #
HasRange LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range #
LensRelevance TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBindings -> Relevance # setRelevance :: Relevance -> TypedBindings -> TypedBindings # mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings #
LensHiding TypedBindings #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBindings -> Hiding # setHiding :: Hiding -> TypedBindings -> TypedBindings # mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings #
LensHiding LamBinding #
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding # setHiding :: Hiding -> LamBinding -> LamBinding # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding #
ExprLike TypedBindings #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings # foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m #
ExprLike LamBinding #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m #
ToConcrete TypedBinding TypedBinding #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding0 # bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b #
ToAbstract TypedBinding TypedBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBinding0 -> ScopeM TypedBinding #
ToAbstract TypedBindings TypedBindings #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBindings0 -> ScopeM TypedBindings #
ToAbstract LamBinding LamBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding #
ToConcrete TypedBindings [TypedBindings] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBindings -> AbsToCon [TypedBindings0] # bindToConcrete :: TypedBindings -> ([TypedBindings0] -> AbsToCon b) -> AbsToCon b #
ToConcrete LamBinding [LamBinding] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon [LamBinding0] # bindToConcrete :: LamBinding -> ([LamBinding0] -> AbsToCon b) -> AbsToCon b #
Data e => Data (TypedBinding' e) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding' e -> c (TypedBinding' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedBinding' e) # toConstr :: TypedBinding' e -> Constr # dataTypeOf :: TypedBinding' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedBinding' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (TypedBinding' e)) # gmapT :: (forall b. Data b => b -> b) -> TypedBinding' e -> TypedBinding' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedBinding' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) #
NFData a => NFData (TypedBinding' a) #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: TypedBinding' a -> () #
ExprLike a => ExprLike (TypedBinding' a) #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a) # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m #

type RecordAssignment = Either FieldAssignment ModuleAssignment #

type RecordAssignments = [RecordAssignment] #

type FieldAssignment = FieldAssignment' Expr #

data FieldAssignment' a #

Constructors

FieldAssignment
Fields _nameFieldA :: Name _exprFieldA :: a

Instances

Functor FieldAssignment' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b # (<$) :: a -> FieldAssignment' b -> FieldAssignment' a #
Foldable FieldAssignment' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => FieldAssignment' m -> m # foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m # foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b # foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b # foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b # foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b # foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a # foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a # toList :: FieldAssignment' a -> [a] # null :: FieldAssignment' a -> Bool # length :: FieldAssignment' a -> Int # elem :: Eq a => a -> FieldAssignment' a -> Bool # maximum :: Ord a => FieldAssignment' a -> a # minimum :: Ord a => FieldAssignment' a -> a # sum :: Num a => FieldAssignment' a -> a # product :: Num a => FieldAssignment' a -> a #
Traversable FieldAssignment' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b) # sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a) # mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b) # sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a) #
ExprLike FieldAssignment #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m #
SubstExpr Assign #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Assign -> Assign #
APatternLike a b => APatternLike a (FieldAssignment' b) #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> FieldAssignment' b -> m # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> FieldAssignment' b -> m (FieldAssignment' b) #
Eq a => Eq (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: FieldAssignment' a -> FieldAssignment' a -> Bool # (/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool #
Data a => Data (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FieldAssignment' a -> c (FieldAssignment' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FieldAssignment' a) # toConstr :: FieldAssignment' a -> Constr # dataTypeOf :: FieldAssignment' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FieldAssignment' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FieldAssignment' a)) # gmapT :: (forall b. Data b => b -> b) -> FieldAssignment' a -> FieldAssignment' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r # gmapQ :: (forall d. Data d => d -> u) -> FieldAssignment' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FieldAssignment' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) #
Show a => Show (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> FieldAssignment' a -> ShowS # show :: FieldAssignment' a -> String # showList :: [FieldAssignment' a] -> ShowS #
NFData a => NFData (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: FieldAssignment' a -> () #
Pretty a => Pretty (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: FieldAssignment' a -> Doc # prettyPrec :: Int -> FieldAssignment' a -> Doc # prettyList :: [FieldAssignment' a] -> Doc #
KillRange a => KillRange (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) #
HasRange a => HasRange (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range #
CPatternLike p => CPatternLike (FieldAssignment' p) #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) #
ExprLike a => ExprLike (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a) # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment' a -> m # traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a) # mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a #
MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a #
EmbPrj a => EmbPrj (FieldAssignment' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Int32 # icod_ :: FieldAssignment' a -> S Int32 # value :: Int32 -> R (FieldAssignment' a) #
NamesIn a => NamesIn (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: FieldAssignment' a -> Set QName #
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) #
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) #
ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: FieldAssignment' a -> AbsToCon (FieldAssignment' c) # bindToConcrete :: FieldAssignment' a -> (FieldAssignment' c -> AbsToCon b) -> AbsToCon b #
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: FieldAssignment' c -> ScopeM (FieldAssignment' a) #

nameFieldA :: Lens' Name (FieldAssignment' a) #

exprFieldA :: Lens' a (FieldAssignment' a) #

data ModuleAssignment #

Constructors

ModuleAssignment
Fields _qnameModA :: QName _exprModA :: [Expr] _importDirModA :: ImportDirective

Instances

Data ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleAssignment -> c ModuleAssignment # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleAssignment # toConstr :: ModuleAssignment -> Constr # dataTypeOf :: ModuleAssignment -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleAssignment) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleAssignment) # gmapT :: (forall b. Data b => b -> b) -> ModuleAssignment -> ModuleAssignment # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleAssignment -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleAssignment -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment #
NFData ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleAssignment -> () #
Pretty ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleAssignment -> Doc # prettyPrec :: Int -> ModuleAssignment -> Doc # prettyList :: [ModuleAssignment] -> Doc #
KillRange ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleAssignment #
HasRange ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range #
ExprLike ModuleAssignment #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment # foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) #

data BoundName #

Constructors

BName
Fields boundName :: Name boundLabel :: Name for implicit function types the label matters and can't be alpha-renamed bnameFixity :: Fixity'

Instances

Eq BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: BoundName -> BoundName -> Bool # (/=) :: BoundName -> BoundName -> Bool #
Data BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoundName -> c BoundName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoundName # toConstr :: BoundName -> Constr # dataTypeOf :: BoundName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoundName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoundName) # gmapT :: (forall b. Data b => b -> b) -> BoundName -> BoundName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r # gmapQ :: (forall d. Data d => d -> u) -> BoundName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BoundName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName #
Show BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> BoundName -> ShowS # show :: BoundName -> String # showList :: [BoundName] -> ShowS #
NFData BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: BoundName -> () #
Pretty BoundName #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: BoundName -> Doc # prettyPrec :: Int -> BoundName -> Doc # prettyList :: [BoundName] -> Doc #
KillRange BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT BoundName #
HasRange BoundName #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: BoundName -> Range #
ToAbstract (NewName BoundName) Name #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM Name #

mkBoundName_ :: Name -> BoundName #

mkBoundName :: Name -> Fixity' -> BoundName #

type Telescope = [TypedBindings] #

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.

countTelVars :: Telescope -> Nat #

Declarations

data Declaration #

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.

Constructors

TypeSig ArgInfo Name Expr	Axioms and functions can be irrelevant. (Hiding should be NotHidden)
Field IsInstance Name (Arg Expr)	Record field, can be hidden and/or irrelevant.
FunClause LHS RHS WhereClause Bool
DataSig Range Induction Name [LamBinding] Expr	lone data signature in mutual block
Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]
RecordSig Range Name [LamBinding] Expr	lone record signature in mutual block
Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] (Maybe Expr) [Declaration]	The optional name is a name for the record constructor.
Infix Fixity [Name]
Syntax Name Notation	notation declaration for a name
PatternSyn Range Name [Arg Name] Pattern
Mutual Range [Declaration]
Abstract Range [Declaration]
Private Range Origin [Declaration]	In Agda.Syntax.Concrete.Definitions we generate private blocks temporarily, which should be treated different that user-declared private blocks. Thus the `Origin`.
InstanceB Range [Declaration]
Macro Range [Declaration]
Postulate Range [TypeSignatureOrInstanceBlock]
Primitive Range [TypeSignature]
Open Range QName ImportDirective
Import Range QName (Maybe AsName) !OpenShortHand ImportDirective
ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective
Module Range QName [TypedBindings] [Declaration]
UnquoteDecl Range [Name] Expr
UnquoteDef Range [Name] Expr
Pragma Pragma

Instances

Data Declaration #
Instance details Defined in Agda.Syntax.Concrete 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 #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS #
Show WhereClause #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS # show :: WhereClause -> String # showList :: [WhereClause] -> ShowS #
NFData Declaration #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Declaration -> () #
Pretty Declaration #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Declaration -> Doc # prettyPrec :: Int -> Declaration -> Doc # prettyList :: [Declaration] -> Doc #
Pretty WhereClause #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc # prettyPrec :: Int -> WhereClause -> Doc # prettyList :: [WhereClause] -> Doc #
KillRange Declaration #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Declaration #
KillRange WhereClause #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause #
HasRange Declaration #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range #
HasRange WhereClause #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range #
ExprLike Declaration #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Declaration -> Declaration # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m #
ToConcrete WhereDeclarations WhereClause #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b #
ToConcrete LetBinding [Declaration] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LetBinding -> AbsToCon [Declaration] # bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
ToConcrete Declaration [Declaration] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Declaration -> AbsToCon [Declaration0] # bindToConcrete :: Declaration -> ([Declaration0] -> AbsToCon b) -> AbsToCon b #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #
ToConcrete (Constr Constructor) Declaration #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Constr Constructor -> AbsToCon Declaration # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b #
ToAbstract (TopLevel [Declaration]) TopLevelInfo #	Top-level declarations are always `(import\|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file`
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo #
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Clause' a -> AbsToCon [Declaration] # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b #
ToAbstract [Declaration] [Declaration] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [Declaration0] -> ScopeM [Declaration] #

data ModuleApplication #

Constructors

SectionApp Range [TypedBindings] Expr	tel. M args
RecordModuleIFS Range QName	M {{...}}

Instances

Data ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete 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 #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleApplication -> ShowS # show :: ModuleApplication -> String # showList :: [ModuleApplication] -> ShowS #
NFData ModuleApplication #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleApplication -> () #
Pretty ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleApplication -> Doc # prettyPrec :: Int -> ModuleApplication -> Doc # prettyList :: [ModuleApplication] -> Doc #
KillRange ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleApplication #
HasRange ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleApplication -> Range #
ExprLike ModuleApplication #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication # foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m #
ToConcrete ModuleApplication ModuleApplication #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: ModuleApplication -> AbsToCon ModuleApplication0 # bindToConcrete :: ModuleApplication -> (ModuleApplication0 -> AbsToCon b) -> AbsToCon b #

type TypeSignature = Declaration #

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration #

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name #

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

type Using = Using' Name Name #

type ImportedName = ImportedName' Name Name #

An imported name can be a module or a defined name.

type Renaming = Renaming' Name Name #

data AsName #

Constructors

AsName
Fields asName :: Name The "as" name. asRange :: Range The range of the "as" keyword. Retained for highlighting purposes.

Instances

Data AsName #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AsName -> c AsName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AsName # toConstr :: AsName -> Constr # dataTypeOf :: AsName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AsName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AsName) # gmapT :: (forall b. Data b => b -> b) -> AsName -> AsName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AsName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AsName -> r # gmapQ :: (forall d. Data d => d -> u) -> AsName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AsName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AsName -> m AsName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName -> m AsName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName -> m AsName #
Show AsName #
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> AsName -> ShowS # show :: AsName -> String # showList :: [AsName] -> ShowS #
NFData AsName #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () #
KillRange AsName #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName #
HasRange AsName #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range #

data OpenShortHand #

Constructors

DoOpen
DontOpen

Instances

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

type RewriteEqn = Expr #

type WithExpr = Expr #

data LHS #

Left hand sides can be written in infix style. For example:

n + suc m = suc (n + m)
(f ∘ g) x = f (g x)

We use fixity information to see which name is actually defined.

Constructors

LHS	Original pattern (including with-patterns), rewrite equations and with-expressions.
Fields lhsOriginalPattern :: Pattern e.g. `f ps \| wps` lhsRewriteEqn :: [RewriteEqn] `rewrite e` (many) lhsWithExpr :: [WithExpr] `with e` (many)

Instances

Data LHS #
Instance details Defined in Agda.Syntax.Concrete 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 #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LHS -> ShowS # show :: LHS -> String # showList :: [LHS] -> ShowS #
NFData LHS #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LHS -> () #
Pretty LHS #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LHS -> Doc # prettyPrec :: Int -> LHS -> Doc # prettyList :: [LHS] -> Doc #
KillRange LHS #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LHS #
HasRange LHS #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHS -> Range #
HasEllipsis LHS #	Does the lhs contain an ellipsis?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool #
ExprLike LHS #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LHS -> LHS # traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS # foldExpr :: Monoid m => (Expr -> m) -> LHS -> m #
ToConcrete LHS LHS #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHS -> AbsToCon LHS0 # bindToConcrete :: LHS -> (LHS0 -> AbsToCon b) -> AbsToCon b #
ToConcrete SpineLHS LHS #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: SpineLHS -> AbsToCon LHS # bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b #

data Pattern #

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName	`c` or `x`
QuoteP Range	quote
AppP Pattern (NamedArg Pattern)	`p p'` or `p {x = p'}`
RawAppP Range [Pattern]	`p1..pn` before parsing operators
OpAppP Range QName (Set Name) [NamedArg Pattern]	eg: `p => p'` for operator `_=>_` The `QName` is possibly ambiguous, but it must correspond to one of the names in the set.
HiddenP Range (Named_ Pattern)	`{p}` or `{x = p}`
InstanceP Range (Named_ Pattern)	`{{p}}` or `{{x = p}}`
ParenP Range Pattern	(p)
WildP Range	_
AbsurdP Range	()
AsP Range Name Pattern	`x@p` unused
DotP Range Expr	.e
LitP Literal	`0`, `1`, etc.
RecP Range [FieldAssignment' Pattern]	record {x = p; y = q}
EllipsisP Range	`...`, only as left-most pattern.
WithP Range Pattern	`\| p`, for with-patterns.

Instances

Data Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern -> c Pattern # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pattern # toConstr :: Pattern -> Constr # dataTypeOf :: Pattern -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pattern) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pattern) # gmapT :: (forall b. Data b => b -> b) -> Pattern -> Pattern # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r # gmapQ :: (forall d. Data d => d -> u) -> Pattern -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern #
Show Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #
NFData Pattern #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pattern -> () #
Pretty Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pattern -> Doc # prettyPrec :: Int -> Pattern -> Doc # prettyList :: [Pattern] -> Doc #
KillRange Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pattern #
SetRange Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> Pattern -> Pattern #
HasRange Pattern #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pattern -> Range #
CPatternLike Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern #
IsWithP Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Pattern -> Maybe Pattern #
HasEllipsis Pattern #
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool #
IsEllipsis Pattern #	Is the pattern just `...`?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool #
IsExpr Pattern #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Pattern -> ExprView Pattern # unExprView :: ExprView Pattern -> Pattern #
ToConcrete Pattern Pattern #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Pattern -> AbsToCon Pattern0 # bindToConcrete :: Pattern -> (Pattern0 -> AbsToCon b) -> AbsToCon b #
ToConcrete LHSCore Pattern #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHSCore -> AbsToCon Pattern # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b #
ToAbstract Pattern (Pattern' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) #

data LHSCore #

Processed (operator-parsed) intermediate form of the core f ps of LHS. Corresponds to lhsOriginalPattern.

Constructors

LHSHead
Fields lhsDefName :: QName f lhsPats :: [NamedArg Pattern] ps
LHSProj
Fields lhsDestructor :: QName Record projection. lhsPatsLeft :: [NamedArg Pattern] Patterns for record indices (currently none). lhsFocus :: NamedArg LHSCore Main argument. lhsPats :: [NamedArg Pattern] ps
LHSWith
Fields lhsHead :: LHSCore lhsWithPatterns :: [Pattern] Non-empty; at least one `(\| p)`. lhsPats :: [NamedArg Pattern] ps

Instances

Show LHSCore #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LHSCore -> ShowS # show :: LHSCore -> String # showList :: [LHSCore] -> ShowS #
Pretty LHSCore #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LHSCore -> Doc # prettyPrec :: Int -> LHSCore -> Doc # prettyList :: [LHSCore] -> Doc #
HasRange LHSCore #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LHSCore -> Range #
ToAbstract LHSCore (LHSCore' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) #

data LamClause #

Constructors

LamClause
Fields lamLHS :: LHS lamRHS :: RHS lamWhere :: WhereClause always `NoWhere` (see parser) lamCatchAll :: Bool

Instances

Data LamClause #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamClause -> c LamClause # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamClause # toConstr :: LamClause -> Constr # dataTypeOf :: LamClause -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamClause) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamClause) # gmapT :: (forall b. Data b => b -> b) -> LamClause -> LamClause # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r # gmapQ :: (forall d. Data d => d -> u) -> LamClause -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LamClause -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause #
NFData LamClause #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamClause -> () #
Pretty LamClause #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamClause -> Doc # prettyPrec :: Int -> LamClause -> Doc # prettyList :: [LamClause] -> Doc #
KillRange LamClause #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamClause #
HasRange LamClause #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamClause -> Range #
ExprLike LamClause #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamClause -> LamClause # traverseExpr :: Monad m => (Expr -> m Expr) -> LamClause -> m LamClause # foldExpr :: Monoid m => (Expr -> m) -> LamClause -> m #

type RHS = RHS' Expr #

data RHS' e #

Constructors

AbsurdRHS	No right hand side because of absurd match.
RHS e

Instances

Functor RHS' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> RHS' a -> RHS' b # (<$) :: a -> RHS' b -> RHS' a #
Show RHS #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
Foldable RHS' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => RHS' m -> m # foldMap :: Monoid m => (a -> m) -> RHS' a -> m # foldr :: (a -> b -> b) -> b -> RHS' a -> b # foldr' :: (a -> b -> b) -> b -> RHS' a -> b # foldl :: (b -> a -> b) -> b -> RHS' a -> b # foldl' :: (b -> a -> b) -> b -> RHS' a -> b # foldr1 :: (a -> a -> a) -> RHS' a -> a # foldl1 :: (a -> a -> a) -> RHS' a -> a # toList :: RHS' a -> [a] # null :: RHS' a -> Bool # length :: RHS' a -> Int # elem :: Eq a => a -> RHS' a -> Bool # maximum :: Ord a => RHS' a -> a # minimum :: Ord a => RHS' a -> a # sum :: Num a => RHS' a -> a # product :: Num a => RHS' a -> a #
Traversable RHS' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> RHS' a -> f (RHS' b) # sequenceA :: Applicative f => RHS' (f a) -> f (RHS' a) # mapM :: Monad m => (a -> m b) -> RHS' a -> m (RHS' b) # sequence :: Monad m => RHS' (m a) -> m (RHS' a) #
Pretty RHS #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RHS -> Doc # prettyPrec :: Int -> RHS -> Doc # prettyList :: [RHS] -> Doc #
KillRange RHS #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS #
HasRange RHS #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range #
ToAbstract RHS AbstractRHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b #
Data e => Data (RHS' e) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS' e -> c (RHS' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e) # toConstr :: RHS' e -> Constr # dataTypeOf :: RHS' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e)) # gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r # gmapQ :: (forall d. Data d => d -> u) -> RHS' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) #
NFData a => NFData (RHS' a) #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: RHS' a -> () #
ExprLike a => ExprLike (RHS' a) #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a # traverseExpr :: Monad m => (Expr -> m Expr) -> RHS' a -> m (RHS' a) # foldExpr :: Monoid m => (Expr -> m) -> RHS' a -> m #

type WhereClause = WhereClause' [Declaration] #

data WhereClause' decls #

Constructors

NoWhere	No `where` clauses.
AnyWhere decls	Ordinary `where`.
SomeWhere Name Access decls	Named where: `module M where`. The `Access` flag applies to the `Name` (not the module contents!) and is propagated from the parent function.

Instances

Functor WhereClause' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b # (<$) :: a -> WhereClause' b -> WhereClause' a #
Show WhereClause #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS # show :: WhereClause -> String # showList :: [WhereClause] -> ShowS #
Foldable WhereClause' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => WhereClause' m -> m # foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m # foldr :: (a -> b -> b) -> b -> WhereClause' a -> b # foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b # foldl :: (b -> a -> b) -> b -> WhereClause' a -> b # foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b # foldr1 :: (a -> a -> a) -> WhereClause' a -> a # foldl1 :: (a -> a -> a) -> WhereClause' a -> a # toList :: WhereClause' a -> [a] # null :: WhereClause' a -> Bool # length :: WhereClause' a -> Int # elem :: Eq a => a -> WhereClause' a -> Bool # maximum :: Ord a => WhereClause' a -> a # minimum :: Ord a => WhereClause' a -> a # sum :: Num a => WhereClause' a -> a # product :: Num a => WhereClause' a -> a #
Traversable WhereClause' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) # sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) # mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) # sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) #
Pretty WhereClause #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc # prettyPrec :: Int -> WhereClause -> Doc # prettyList :: [WhereClause] -> Doc #
KillRange WhereClause #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause #
HasRange WhereClause #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range #
ToConcrete WhereDeclarations WhereClause #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b #
Data decls => Data (WhereClause' decls) #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereClause' decls -> c (WhereClause' decls) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WhereClause' decls) # toConstr :: WhereClause' decls -> Constr # dataTypeOf :: WhereClause' decls -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WhereClause' decls)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WhereClause' decls)) # gmapT :: (forall b. Data b => b -> b) -> WhereClause' decls -> WhereClause' decls # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r # gmapQ :: (forall d. Data d => d -> u) -> WhereClause' decls -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereClause' decls -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) #
NFData a => NFData (WhereClause' a) #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause' a -> () #
Null (WhereClause' a) #	A `WhereClause` is `null` when the `where` keyword is absent. An empty list of declarations does not count as `null` here.
Instance details Defined in Agda.Syntax.Concrete Methods empty :: WhereClause' a # null :: WhereClause' a -> Bool #
ExprLike a => ExprLike (WhereClause' a) #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m #

data ExprWhere #

An expression followed by a where clause. Currently only used to give better a better error message in interaction.

Constructors

ExprWhere Expr WhereClause

data DoStmt #

Constructors

DoBind Range Pattern Expr [LamClause]	p ← e where cs
DoThen Expr
DoLet Range [Declaration]

Instances

Data DoStmt #
Instance details Defined in Agda.Syntax.Concrete Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoStmt -> c DoStmt # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoStmt # toConstr :: DoStmt -> Constr # dataTypeOf :: DoStmt -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoStmt) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoStmt) # gmapT :: (forall b. Data b => b -> b) -> DoStmt -> DoStmt # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r # gmapQ :: (forall d. Data d => d -> u) -> DoStmt -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DoStmt -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt #
NFData DoStmt #
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: DoStmt -> () #
Pretty DoStmt #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: DoStmt -> Doc # prettyPrec :: Int -> DoStmt -> Doc # prettyList :: [DoStmt] -> Doc #
KillRange DoStmt #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT DoStmt #
HasRange DoStmt #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: DoStmt -> Range #
ExprLike DoStmt #
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt # traverseExpr :: Monad m => (Expr -> m Expr) -> DoStmt -> m DoStmt # foldExpr :: Monoid m => (Expr -> m) -> DoStmt -> m #

data Pragma #

Constructors

OptionsPragma Range [String]
BuiltinPragma Range String QName
RewritePragma Range [QName]
CompiledDataPragma Range QName String [String]
CompiledTypePragma Range QName String
CompiledPragma Range QName String
CompiledExportPragma Range QName String
CompiledJSPragma Range QName String
CompiledUHCPragma Range QName String
CompiledDataUHCPragma Range QName String [String]
HaskellCodePragma Range String
ForeignPragma Range String String	first string is backend name
CompilePragma Range String QName String	first string is backend name
StaticPragma Range QName
InjectivePragma Range QName
InlinePragma Range Bool QName	INLINE or NOINLINE
ImportPragma Range String	Invariant: The string must be a valid Haskell module name.
ImportUHCPragma Range String	same as above, but for the UHC backend
ImpossiblePragma Range	Throws an internal error in the scope checker.
EtaPragma Range QName	For coinductive records, use pragma instead of regular `eta-equality` definition (as it is might make Agda loop).
TerminationCheckPragma Range (TerminationCheck Name)	Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block.
WarningOnUsage Range QName String	Applies to the named function
CatchallPragma Range	Applies to the following function clause.
DisplayPragma Range Pattern Expr
NoPositivityCheckPragma Range	Applies to the following data/record type or mutual block.
PolarityPragma Range Name [Occurrence]

Instances

Data Pragma #
Instance details Defined in Agda.Syntax.Concrete 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 #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
NFData Pragma #	Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pragma -> () #
Pretty Pragma #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pragma -> Doc # prettyPrec :: Int -> Pragma -> Doc # prettyList :: [Pragma] -> Doc #
KillRange Pragma #
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pragma #
HasRange Pragma #
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pragma -> Range #
ToConcrete RangeAndPragma Pragma #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RangeAndPragma -> AbsToCon Pragma # bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b #
ToAbstract Pragma [Pragma] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pragma0 -> ScopeM [Pragma] #

type Module = ([Pragma], [Declaration]) #

Modules: Top-level pragmas plus other top-level declarations.

data ThingWithFixity x #

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity #
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a #
Foldable ThingWithFixity #
Instance details Defined in Agda.Syntax.Fixity Methods fold :: Monoid m => ThingWithFixity m -> m # foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m # foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a # foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a # toList :: ThingWithFixity a -> [a] # null :: ThingWithFixity a -> Bool # length :: ThingWithFixity a -> Int # elem :: Eq a => a -> ThingWithFixity a -> Bool # maximum :: Ord a => ThingWithFixity a -> a # minimum :: Ord a => ThingWithFixity a -> a # sum :: Num a => ThingWithFixity a -> a # product :: Num a => ThingWithFixity a -> a #
Traversable ThingWithFixity #
Instance details Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) #
Data x => Data (ThingWithFixity x) #
Instance details Defined in Agda.Syntax.Fixity Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ThingWithFixity x -> c (ThingWithFixity x) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) # toConstr :: ThingWithFixity x -> Constr # dataTypeOf :: ThingWithFixity x -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) # gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r # gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) #
Show x => Show (ThingWithFixity x) #
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS # show :: ThingWithFixity x -> String # showList :: [ThingWithFixity x] -> ShowS #
Pretty (ThingWithFixity Name) #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc # prettyPrec :: Int -> ThingWithFixity Name -> Doc # prettyList :: [ThingWithFixity Name] -> Doc #
KillRange x => KillRange (ThingWithFixity x) #
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) #

type HoleContent = HoleContent' Expr #

data HoleContent' e #

Extended content of an interaction hole.

Constructors

HoleContentExpr e	e
HoleContentRewrite [e]	rewrite e0 \| ... \| en

Instances

Functor HoleContent' #
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> HoleContent' a -> HoleContent' b # (<$) :: a -> HoleContent' b -> HoleContent' a #
Foldable HoleContent' #
Instance details Defined in Agda.Syntax.Concrete Methods fold :: Monoid m => HoleContent' m -> m # foldMap :: Monoid m => (a -> m) -> HoleContent' a -> m # foldr :: (a -> b -> b) -> b -> HoleContent' a -> b # foldr' :: (a -> b -> b) -> b -> HoleContent' a -> b # foldl :: (b -> a -> b) -> b -> HoleContent' a -> b # foldl' :: (b -> a -> b) -> b -> HoleContent' a -> b # foldr1 :: (a -> a -> a) -> HoleContent' a -> a # foldl1 :: (a -> a -> a) -> HoleContent' a -> a # toList :: HoleContent' a -> [a] # null :: HoleContent' a -> Bool # length :: HoleContent' a -> Int # elem :: Eq a => a -> HoleContent' a -> Bool # maximum :: Ord a => HoleContent' a -> a # minimum :: Ord a => HoleContent' a -> a # sum :: Num a => HoleContent' a -> a # product :: Num a => HoleContent' a -> a #
Traversable HoleContent' #
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> HoleContent' a -> f (HoleContent' b) # sequenceA :: Applicative f => HoleContent' (f a) -> f (HoleContent' a) # mapM :: Monad m => (a -> m b) -> HoleContent' a -> m (HoleContent' b) # sequence :: Monad m => HoleContent' (m a) -> m (HoleContent' a) #
ToAbstract HoleContent HoleContent #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: HoleContent0 -> ScopeM HoleContent #

topLevelModuleName :: Module -> TopLevelModuleName #

Computes the top-level module name.

Precondition: The Module has to be well-formed. This means that there are only allowed declarations before the first module declaration, typically import declarations. See spanAllowedBeforeModule.

spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration]) #

Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.