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

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 (Arg Expr) Expr
  - | Pi Telescope Expr
  - | Set Range
  - | Prop Range
  - | SetN Range Integer
  - | PropN 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
  - | Generalized Expr
- 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]
- isSingleIdentifierP :: Pattern -> Maybe Name
- removeSingletonRawAppP :: Pattern -> Pattern
- type LamBinding = LamBinding' TypedBinding
- data LamBinding' a
  - = DomainFree (NamedArg BoundName)
  - | DomainFull a
- type TypedBinding = TypedBinding' Expr
- data TypedBinding' e
  - = TBind Range [NamedArg 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
  - bnameFixity :: Fixity'
  }
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type Telescope = [TypedBinding]
- countTelVars :: Telescope -> Nat
- lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
- makePi :: Telescope -> Expr -> Expr
- data Declaration
  - = TypeSig ArgInfo Name Expr
  - | Generalize Range [TypeSignature]
  - | Field IsInstance Name (Arg Expr)
  - | FunClause LHS RHS WhereClause Bool
  - | DataSig Range Induction Name [LamBinding] Expr
  - | Data Range Induction Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
  - | DataDef Range Induction Name [LamBinding] [TypeSignatureOrInstanceBlock]
  - | RecordSig Range Name [LamBinding] Expr
  - | RecordDef Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
  - | Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] 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 Telescope [Declaration]
  - | UnquoteDecl Range [Name] Expr
  - | UnquoteDef Range [Name] Expr
  - | Pragma Pragma
- data ModuleApplication
  - = SectionApp Range Telescope Expr
  - | RecordModuleInstance 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' a = AsName {
  - asName :: a
  - asRange :: Range
  }
- type AsName = AsName' (Either Expr Name)
- 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]
  - | EqualP Range [(Expr, Expr)]
  - | 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]
  - | ForeignPragma Range String String
  - | CompilePragma Range String QName String
  - | StaticPragma Range QName
  - | InlinePragma Range Bool QName
  - | ImpossiblePragma Range
  - | EtaPragma Range QName
  - | WarningOnUsage Range QName String
  - | InjectivePragma Range QName
  - | DisplayPragma Range Pattern Expr
  - | CatchallPragma Range
  - | TerminationCheckPragma Range (TerminationCheck Name)
  - | NoPositivityCheckPragma Range
  - | PolarityPragma Range Name [Occurrence]
  - | NoUniverseCheckPragma Range
- 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 Source #

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 (Arg 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, ..`
PropN Range Integer | ex: `Prop0, Prop1, ..`
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.
Generalized Expr |

Instances

Data Expr Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr Source #

toConstr :: Expr -> Constr Source #

dataTypeOf :: Expr -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) Source #

gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr Source #

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

data OpApp e Source #

Constructors

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

Instances

Functor OpApp Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> OpApp a -> OpApp b Source # (<$) :: a -> OpApp b -> OpApp a Source #
Foldable OpApp Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => OpApp m -> m Source #

foldMap :: Monoid m => (a -> m) -> OpApp a -> m Source #

foldr :: (a -> b -> b) -> b -> OpApp a -> b Source #

foldr' :: (a -> b -> b) -> b -> OpApp a -> b Source #

foldl :: (b -> a -> b) -> b -> OpApp a -> b Source #

foldl' :: (b -> a -> b) -> b -> OpApp a -> b Source #

foldr1 :: (a -> a -> a) -> OpApp a -> a Source #

foldl1 :: (a -> a -> a) -> OpApp a -> a Source #

toList :: OpApp a -> [a] Source #

null :: OpApp a -> Bool Source #

length :: OpApp a -> Int Source #

elem :: Eq a => a -> OpApp a -> Bool Source #

maximum :: Ord a => OpApp a -> a Source #

minimum :: Ord a => OpApp a -> a Source #

sum :: Num a => OpApp a -> a Source #

product :: Num a => OpApp a -> a Source #

Traversable OpApp Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> OpApp a -> f (OpApp b) Source # sequenceA :: Applicative f => OpApp (f a) -> f (OpApp a) Source # mapM :: Monad m => (a -> m b) -> OpApp a -> m (OpApp b) Source # sequence :: Monad m => OpApp (m a) -> m (OpApp a) Source #
Data e => Data (OpApp e) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OpApp e) Source #

toConstr :: OpApp e -> Constr Source #

dataTypeOf :: OpApp e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OpApp e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (OpApp e)) Source #

gmapT :: (forall b. Data b => b -> b) -> OpApp e -> OpApp e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpApp e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> OpApp e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpApp e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpApp e -> m (OpApp e) Source #

Show a => Show (OpApp a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> OpApp a -> ShowS Source # show :: OpApp a -> String Source # showList :: [OpApp a] -> ShowS Source #
NFData a => NFData (OpApp a) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: OpApp a -> () Source #
Pretty (OpApp Expr) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpApp Expr -> Doc Source # prettyPrec :: Int -> OpApp Expr -> Doc Source # prettyList :: [OpApp Expr] -> Doc Source #
KillRange e => KillRange (OpApp e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source #
HasRange e => HasRange (OpApp e) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: OpApp e -> Range Source #
ExprLike a => ExprLike (OpApp a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a) Source # foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m Source #

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

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView Source #

data AppView Source #

The `Expr` is not an application.

Constructors

AppView Expr [NamedArg Expr] |

isSingleIdentifierP :: Pattern -> Maybe Name Source #

removeSingletonRawAppP :: Pattern -> Pattern Source #

# Bindings

type LamBinding = LamBinding' TypedBinding Source #

A lambda binding is either domain free or typed.

data LamBinding' a Source #

Constructors

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

Instances

Functor LamBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b Source # (<$) :: a -> LamBinding' b -> LamBinding' a Source #
Foldable LamBinding' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => LamBinding' m -> m Source #

foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m Source #

foldr :: (a -> b -> b) -> b -> LamBinding' a -> b Source #

foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b Source #

foldl :: (b -> a -> b) -> b -> LamBinding' a -> b Source #

foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b Source #

foldr1 :: (a -> a -> a) -> LamBinding' a -> a Source #

foldl1 :: (a -> a -> a) -> LamBinding' a -> a Source #

toList :: LamBinding' a -> [a] Source #

null :: LamBinding' a -> Bool Source #

length :: LamBinding' a -> Int Source #

elem :: Eq a => a -> LamBinding' a -> Bool Source #

maximum :: Ord a => LamBinding' a -> a Source #

minimum :: Ord a => LamBinding' a -> a Source #

sum :: Num a => LamBinding' a -> a Source #

product :: Num a => LamBinding' a -> a Source #

Traversable LamBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) Source # sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) Source # mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) Source # sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) Source #
Pretty LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
KillRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding Source #
HasRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source #
LensHiding LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
ExprLike LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source #
ToConcrete LamBinding LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon LamBinding0 Source # bindToConcrete :: LamBinding -> (LamBinding0 -> AbsToCon b) -> AbsToCon b Source #
ToAbstract LamBinding LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding Source #
Data a => Data (LamBinding' a) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LamBinding' a) Source #

toConstr :: LamBinding' a -> Constr Source #

dataTypeOf :: LamBinding' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LamBinding' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LamBinding' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> LamBinding' a -> LamBinding' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LamBinding' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding' a -> m (LamBinding' a) Source #

Show (LamBinding' TypedBinding) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding' TypedBinding -> ShowS Source # show :: LamBinding' TypedBinding -> String Source # showList :: [LamBinding' TypedBinding] -> ShowS Source #
NFData a => NFData (LamBinding' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamBinding' a -> () Source #

type TypedBinding = TypedBinding' Expr Source #

A typed binding.

data TypedBinding' e Source #

Constructors

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

Instances

Functor TypedBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b Source # (<$) :: a -> TypedBinding' b -> TypedBinding' a Source #
Foldable TypedBinding' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => TypedBinding' m -> m Source #

foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m Source #

foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b Source #

foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b Source #

foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b Source #

foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b Source #

foldr1 :: (a -> a -> a) -> TypedBinding' a -> a Source #

foldl1 :: (a -> a -> a) -> TypedBinding' a -> a Source #

toList :: TypedBinding' a -> [a] Source #

null :: TypedBinding' a -> Bool Source #

length :: TypedBinding' a -> Int Source #

elem :: Eq a => a -> TypedBinding' a -> Bool Source #

maximum :: Ord a => TypedBinding' a -> a Source #

minimum :: Ord a => TypedBinding' a -> a Source #

sum :: Num a => TypedBinding' a -> a Source #

product :: Num a => TypedBinding' a -> a Source #

Traversable TypedBinding' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b) Source # sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a) Source # mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b) Source # sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a) Source #
Pretty TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source #
Pretty LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source #
KillRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT TypedBinding Source #
KillRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamBinding Source #
SetRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source #
HasRange TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source #
HasRange LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamBinding -> Range Source #
LensRelevance TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRelevance :: TypedBinding -> Relevance Source # setRelevance :: Relevance -> TypedBinding -> TypedBinding Source # mapRelevance :: (Relevance -> Relevance) -> TypedBinding -> TypedBinding Source #
LensHiding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
LensHiding LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
ExprLike LamBinding Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source #
ToConcrete TypedBinding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: TypedBinding -> AbsToCon TypedBinding0 Source # bindToConcrete :: TypedBinding -> (TypedBinding0 -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LamBinding LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LamBinding -> AbsToCon LamBinding0 Source # bindToConcrete :: LamBinding -> (LamBinding0 -> AbsToCon b) -> AbsToCon b Source #
ToAbstract TypedBinding TypedBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBinding0 -> ScopeM TypedBinding Source #
ToAbstract LamBinding LamBinding Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding Source #
Data e => Data (TypedBinding' e) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedBinding' e) Source #

toConstr :: TypedBinding' e -> Constr Source #

dataTypeOf :: TypedBinding' e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedBinding' e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (TypedBinding' e)) Source #

gmapT :: (forall b. Data b => b -> b) -> TypedBinding' e -> TypedBinding' e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding' e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TypedBinding' e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding' e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding' e -> m (TypedBinding' e) Source #

Show (TypedBinding' Expr) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding' Expr -> ShowS Source # show :: TypedBinding' Expr -> String Source # showList :: [TypedBinding' Expr] -> ShowS Source #
Show (LamBinding' TypedBinding) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding' TypedBinding -> ShowS Source # show :: LamBinding' TypedBinding -> String Source # showList :: [LamBinding' TypedBinding] -> ShowS Source #
NFData a => NFData (TypedBinding' a) Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: TypedBinding' a -> () Source #
ExprLike a => ExprLike (TypedBinding' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a) Source # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m Source #

type RecordAssignment = Either FieldAssignment ModuleAssignment Source #

type RecordAssignments = [RecordAssignment] Source #

type FieldAssignment = FieldAssignment' Expr Source #

data FieldAssignment' a Source #

Constructors

FieldAssignment |

Fields

- _nameFieldA :: Name
- _exprFieldA :: a

Instances

Functor FieldAssignment' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b Source # (<$) :: a -> FieldAssignment' b -> FieldAssignment' a Source #
Foldable FieldAssignment' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => FieldAssignment' m -> m Source #

foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m Source #

foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b Source #

foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b Source #

foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b Source #

foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b Source #

foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a Source #

foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a Source #

toList :: FieldAssignment' a -> [a] Source #

null :: FieldAssignment' a -> Bool Source #

length :: FieldAssignment' a -> Int Source #

elem :: Eq a => a -> FieldAssignment' a -> Bool Source #

maximum :: Ord a => FieldAssignment' a -> a Source #

minimum :: Ord a => FieldAssignment' a -> a Source #

sum :: Num a => FieldAssignment' a -> a Source #

product :: Num a => FieldAssignment' a -> a Source #

Traversable FieldAssignment' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b) Source #

sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a) Source #

mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b) Source #

sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a) Source #

ExprLike FieldAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment Source # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m Source #
SubstExpr Assign Source # |
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Assign -> Assign Source #
APatternLike a b => APatternLike a (FieldAssignment' b) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods foldrAPattern :: Monoid m => (Pattern' a -> m -> m) -> FieldAssignment' b -> m Source # traverseAPatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> FieldAssignment' b -> m (FieldAssignment' b) Source #
Eq a => Eq (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: FieldAssignment' a -> FieldAssignment' a -> Bool Source # (/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool Source #
Data a => Data (FieldAssignment' a) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FieldAssignment' a) Source #

toConstr :: FieldAssignment' a -> Constr Source #

dataTypeOf :: FieldAssignment' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (FieldAssignment' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FieldAssignment' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> FieldAssignment' a -> FieldAssignment' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FieldAssignment' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> FieldAssignment' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FieldAssignment' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FieldAssignment' a -> m (FieldAssignment' a) Source #

Show a => Show (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> FieldAssignment' a -> ShowS Source # show :: FieldAssignment' a -> String Source # showList :: [FieldAssignment' a] -> ShowS Source #
NFData a => NFData (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: FieldAssignment' a -> () Source #
Pretty a => Pretty (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: FieldAssignment' a -> Doc Source # prettyPrec :: Int -> FieldAssignment' a -> Doc Source # prettyList :: [FieldAssignment' a] -> Doc Source #
KillRange a => KillRange (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) Source #
HasRange a => HasRange (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range Source #
CPatternLike p => CPatternLike (FieldAssignment' p) Source # |

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source #

ExprLike a => ExprLike (FieldAssignment' a) Source # |

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a) Source #

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment' a -> m Source #

traverseExpr :: (Applicative m, Monad m) => (Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a) Source #

mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a Source #

MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source #
EmbPrj a => EmbPrj (FieldAssignment' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: FieldAssignment' a -> S Int32 Source # icod_ :: FieldAssignment' a -> S Int32 Source # value :: Int32 -> R (FieldAssignment' a) Source #
NamesIn a => NamesIn (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: FieldAssignment' a -> Set QName Source #
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) Source #
ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: FieldAssignment' a -> AbsToCon (FieldAssignment' c) Source # bindToConcrete :: FieldAssignment' a -> (FieldAssignment' c -> AbsToCon b) -> AbsToCon b Source #
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: FieldAssignment' c -> ScopeM (FieldAssignment' a) Source #

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

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

data ModuleAssignment Source #

Constructors

ModuleAssignment |

Fields

- _qnameModA :: QName
- _exprModA :: [Expr]
- _importDirModA :: ImportDirective

Instances

Data ModuleAssignment Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleAssignment Source #

toConstr :: ModuleAssignment -> Constr Source #

dataTypeOf :: ModuleAssignment -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleAssignment) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleAssignment) Source #

gmapT :: (forall b. Data b => b -> b) -> ModuleAssignment -> ModuleAssignment Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleAssignment -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ModuleAssignment -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleAssignment -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleAssignment -> m ModuleAssignment Source #

Show ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleAssignment -> ShowS Source # show :: ModuleAssignment -> String Source # showList :: [ModuleAssignment] -> ShowS Source #
NFData ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: ModuleAssignment -> () Source #
Pretty ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ModuleAssignment -> Doc Source # prettyPrec :: Int -> ModuleAssignment -> Doc Source # prettyList :: [ModuleAssignment] -> Doc Source #
KillRange ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT ModuleAssignment Source #
HasRange ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range Source #
ExprLike ModuleAssignment Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m Source #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) Source #

data BoundName Source #

Constructors

BName |

Fields

- boundName :: Name
- bnameFixity :: Fixity'

Instances

Eq BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: BoundName -> BoundName -> Bool Source # (/=) :: BoundName -> BoundName -> Bool Source #
Data BoundName Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoundName Source #

toConstr :: BoundName -> Constr Source #

dataTypeOf :: BoundName -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoundName) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoundName) Source #

gmapT :: (forall b. Data b => b -> b) -> BoundName -> BoundName Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoundName -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> BoundName -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BoundName -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoundName -> m BoundName Source #

Show BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> BoundName -> ShowS Source # show :: BoundName -> String Source # showList :: [BoundName] -> ShowS Source #
NFData BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: BoundName -> () Source #
Pretty BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: BoundName -> Doc Source # prettyPrec :: Int -> BoundName -> Doc Source # prettyList :: [BoundName] -> Doc Source #
KillRange BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT BoundName Source #
HasRange BoundName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: BoundName -> Range Source #
ToConcrete BindName BoundName Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: BindName -> AbsToCon BoundName Source # bindToConcrete :: BindName -> (BoundName -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (NewName BoundName) BindName Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM BindName Source #

mkBoundName_ :: Name -> BoundName Source #

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

type Telescope = [TypedBinding] Source #

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

countTelVars :: Telescope -> Nat Source #

lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope Source #

We can try to get a `Telescope` from a `[LamBinding]`. If we have a type annotation already, we're happy. Otherwise we manufacture a binder with an underscore for the type.

makePi :: Telescope -> Expr -> Expr Source #

Smart constructor for `Pi`: check whether the `Telescope` is empty

# Declarations

data Declaration Source #

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)
Generalize Range [TypeSignature] | Variables to be generalized, can be hidden and/or irrelevant.
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] Expr [TypeSignatureOrInstanceBlock] |
DataDef Range Induction Name [LamBinding] [TypeSignatureOrInstanceBlock] |
RecordSig Range Name [LamBinding] Expr | lone record signature in mutual block
RecordDef Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration] |
Record Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] 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 Telescope [Declaration] |
UnquoteDecl Range [Name] Expr |
UnquoteDef Range [Name] Expr |
Pragma Pragma |

Instances

Data Declaration Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration Source #

toConstr :: Declaration -> Constr Source #

dataTypeOf :: Declaration -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) Source #

gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration Source #

Show Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Declaration -> ShowS Source # show :: Declaration -> String Source # showList :: [Declaration] -> ShowS Source #
NFData Declaration Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Declaration -> () Source #
Pretty Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source #
Pretty WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source #
KillRange Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Declaration Source #
KillRange WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause Source #
HasRange Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Declaration -> Range Source #
HasRange WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source #
ExprLike Declaration Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source #
ToConcrete WhereDeclarations WhereClause Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause Source # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LetBinding [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LetBinding -> AbsToCon [Declaration] Source # bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
ToConcrete Declaration [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Declaration -> AbsToCon [Declaration0] Source # bindToConcrete :: Declaration -> ([Declaration0] -> AbsToCon b) -> AbsToCon b Source #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source #
Show (WhereClause' [Declaration]) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause' [Declaration] -> ShowS Source # show :: WhereClause' [Declaration] -> String Source # showList :: [WhereClause' [Declaration]] -> ShowS Source #
ToConcrete (Constr Constructor) Declaration Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Constr Constructor -> AbsToCon Declaration Source # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (TopLevel [Declaration]) TopLevelInfo Source # | 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 Source #
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Clause' a -> AbsToCon [Declaration] Source # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b Source #
ToAbstract [Declaration] [Declaration] Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [Declaration0] -> ScopeM [Declaration] Source #

data ModuleApplication Source #

Constructors

SectionApp Range Telescope Expr

    tel. M args

RecordModuleInstance Range QName

    M {{...}}

Instances

Data ModuleApplication Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication Source #

toConstr :: ModuleApplication -> Constr Source #

dataTypeOf :: ModuleApplication -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication) Source #

gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication Source #

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

type TypeSignature = Declaration Source #

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration Source #

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name Source #

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 Source #

type ImportedName = ImportedName' Name Name Source #

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

type Renaming = Renaming' Name Name Source #

data AsName' a Source #

The content of the `as`-clause of the import statement.

Constructors

AsName |

Fields

- asName :: a

  The "as" name.

- asRange :: Range

  The range of the "as" keyword. Retained for highlighting purposes.

Instances

Functor AsName' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> AsName' a -> AsName' b Source # (<$) :: a -> AsName' b -> AsName' a Source #
Foldable AsName' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => AsName' m -> m Source #

foldMap :: Monoid m => (a -> m) -> AsName' a -> m Source #

foldr :: (a -> b -> b) -> b -> AsName' a -> b Source #

foldr' :: (a -> b -> b) -> b -> AsName' a -> b Source #

foldl :: (b -> a -> b) -> b -> AsName' a -> b Source #

foldl' :: (b -> a -> b) -> b -> AsName' a -> b Source #

foldr1 :: (a -> a -> a) -> AsName' a -> a Source #

foldl1 :: (a -> a -> a) -> AsName' a -> a Source #

toList :: AsName' a -> [a] Source #

null :: AsName' a -> Bool Source #

length :: AsName' a -> Int Source #

elem :: Eq a => a -> AsName' a -> Bool Source #

maximum :: Ord a => AsName' a -> a Source #

minimum :: Ord a => AsName' a -> a Source #

sum :: Num a => AsName' a -> a Source #

product :: Num a => AsName' a -> a Source #

Traversable AsName' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> AsName' a -> f (AsName' b) Source # sequenceA :: Applicative f => AsName' (f a) -> f (AsName' a) Source # mapM :: Monad m => (a -> m b) -> AsName' a -> m (AsName' b) Source # sequence :: Monad m => AsName' (m a) -> m (AsName' a) Source #
NFData AsName Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: AsName -> () Source #
KillRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT AsName Source #
HasRange AsName Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: AsName -> Range Source #
Data a => Data (AsName' a) Source # |

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' a -> c (AsName' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AsName' a) Source #

toConstr :: AsName' a -> Constr Source #

dataTypeOf :: AsName' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AsName' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AsName' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> AsName' a -> AsName' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AsName' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AsName' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AsName' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AsName' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AsName' a -> m (AsName' a) Source #

Show a => Show (AsName' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> AsName' a -> ShowS Source # show :: AsName' a -> String Source # showList :: [AsName' a] -> ShowS Source #

type AsName = AsName' (Either Expr Name) Source #

From the parser, we get an expression for the `as`-`Name`, which we have to parse into a `Name`.

data OpenShortHand Source #

Constructors

DoOpen |
DontOpen |

Instances

Eq OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete Methods (==) :: OpenShortHand -> OpenShortHand -> Bool Source # (/=) :: OpenShortHand -> OpenShortHand -> Bool Source #
Data OpenShortHand Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpenShortHand Source #

toConstr :: OpenShortHand -> Constr Source #

dataTypeOf :: OpenShortHand -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpenShortHand) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpenShortHand) Source #

gmapT :: (forall b. Data b => b -> b) -> OpenShortHand -> OpenShortHand Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpenShortHand -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> OpenShortHand -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpenShortHand -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpenShortHand -> m OpenShortHand Source #

Show OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete Methods showsPrec :: Int -> OpenShortHand -> ShowS Source # show :: OpenShortHand -> String Source # showList :: [OpenShortHand] -> ShowS Source #
Pretty OpenShortHand Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source #

type RewriteEqn = Expr Source #

type WithExpr = Expr Source #

data LHS Source #

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 Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS Source #

toConstr :: LHS -> Constr Source #

dataTypeOf :: LHS -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) Source #

gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS Source #

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

data Pattern Source #

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}

EqualP Range [(Expr, Expr)] | `i = i1` i.e. cubical face lattice generator
EllipsisP Range | `...`, only as left-most pattern.
WithP Range Pattern | `| p`, for with-patterns.

Instances

Data Pattern Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pattern Source #

toConstr :: Pattern -> Constr Source #

dataTypeOf :: Pattern -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pattern) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pattern) Source #

gmapT :: (forall b. Data b => b -> b) -> Pattern -> Pattern Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Pattern -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern Source #

Show Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Pattern -> ShowS Source # show :: Pattern -> String Source # showList :: [Pattern] -> ShowS Source #
NFData Pattern Source # | Ranges are not forced.
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: Pattern -> () Source #
Pretty Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: Pattern -> Doc Source # prettyPrec :: Int -> Pattern -> Doc Source # prettyList :: [Pattern] -> Doc Source #
KillRange Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT Pattern Source #
SetRange Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods setRange :: Range -> Pattern -> Pattern Source #
HasRange Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: Pattern -> Range Source #
CPatternLike Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Pattern -> m Source # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Pattern -> m Pattern Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Pattern -> m Pattern Source #
IsWithP Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isWithP :: Pattern -> Maybe Pattern Source #
HasEllipsis Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool Source #
IsEllipsis Pattern Source # | Is the pattern just `...`?
Instance details Defined in Agda.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool Source #
IsExpr Pattern Source # |
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Pattern -> ExprView Pattern Source # unExprView :: ExprView Pattern -> Pattern Source #
ToConcrete Pattern Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Pattern -> AbsToCon Pattern0 Source # bindToConcrete :: Pattern -> (Pattern0 -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LHSCore Pattern Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: LHSCore -> AbsToCon Pattern Source # bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b Source #
ToAbstract Pattern (Pattern' Expr) Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) Source #

data LHSCore Source #

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

data LamClause Source #

Constructors

LamClause |

Fields

- lamLHS :: LHS
- lamRHS :: RHS
- lamWhere :: WhereClause

  always `NoWhere` (see parser)

- lamCatchAll :: Bool

Instances

Data LamClause Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamClause Source #

toConstr :: LamClause -> Constr Source #

dataTypeOf :: LamClause -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamClause) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamClause) Source #

gmapT :: (forall b. Data b => b -> b) -> LamClause -> LamClause Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamClause -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LamClause -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LamClause -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamClause -> m LamClause Source #

Show LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamClause -> ShowS Source # show :: LamClause -> String Source # showList :: [LamClause] -> ShowS Source #
NFData LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: LamClause -> () Source #
Pretty LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: LamClause -> Doc Source # prettyPrec :: Int -> LamClause -> Doc Source # prettyList :: [LamClause] -> Doc Source #
KillRange LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT LamClause Source #
HasRange LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: LamClause -> Range Source #
ExprLike LamClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamClause -> LamClause Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamClause -> m LamClause Source # foldExpr :: Monoid m => (Expr -> m) -> LamClause -> m Source #

type RHS = RHS' Expr Source #

data RHS' e Source #

Constructors

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

Instances

Functor RHS' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> RHS' a -> RHS' b Source # (<$) :: a -> RHS' b -> RHS' a Source #
Foldable RHS' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => RHS' m -> m Source #

foldMap :: Monoid m => (a -> m) -> RHS' a -> m Source #

foldr :: (a -> b -> b) -> b -> RHS' a -> b Source #

foldr' :: (a -> b -> b) -> b -> RHS' a -> b Source #

foldl :: (b -> a -> b) -> b -> RHS' a -> b Source #

foldl' :: (b -> a -> b) -> b -> RHS' a -> b Source #

foldr1 :: (a -> a -> a) -> RHS' a -> a Source #

foldl1 :: (a -> a -> a) -> RHS' a -> a Source #

toList :: RHS' a -> [a] Source #

null :: RHS' a -> Bool Source #

length :: RHS' a -> Int Source #

elem :: Eq a => a -> RHS' a -> Bool Source #

maximum :: Ord a => RHS' a -> a Source #

minimum :: Ord a => RHS' a -> a Source #

sum :: Num a => RHS' a -> a Source #

product :: Num a => RHS' a -> a Source #

Traversable RHS' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> RHS' a -> f (RHS' b) Source # sequenceA :: Applicative f => RHS' (f a) -> f (RHS' a) Source # mapM :: Monad m => (a -> m b) -> RHS' a -> m (RHS' b) Source # sequence :: Monad m => RHS' (m a) -> m (RHS' a) Source #
Pretty RHS Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: RHS -> Doc Source # prettyPrec :: Int -> RHS -> Doc Source # prettyList :: [RHS] -> Doc Source #
KillRange RHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT RHS Source #
HasRange RHS Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: RHS -> Range Source #
ToAbstract RHS AbstractRHS Source # |
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS Source #
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) Source # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b Source #
Data e => Data (RHS' e) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RHS' e) Source #

toConstr :: RHS' e -> Constr Source #

dataTypeOf :: RHS' e -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RHS' e)) Source #

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (RHS' e)) Source #

gmapT :: (forall b. Data b => b -> b) -> RHS' e -> RHS' e Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS' e -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> RHS' e -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS' e -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS' e -> m (RHS' e) Source #

Show (RHS' Expr) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> RHS' Expr -> ShowS Source # show :: RHS' Expr -> String Source # showList :: [RHS' Expr] -> ShowS Source #
NFData a => NFData (RHS' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: RHS' a -> () Source #
ExprLike a => ExprLike (RHS' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RHS' a -> m (RHS' a) Source # foldExpr :: Monoid m => (Expr -> m) -> RHS' a -> m Source #

type WhereClause = WhereClause' [Declaration] Source #

data WhereClause' decls Source #

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' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b Source # (<$) :: a -> WhereClause' b -> WhereClause' a Source #
Foldable WhereClause' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => WhereClause' m -> m Source #

foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m Source #

foldr :: (a -> b -> b) -> b -> WhereClause' a -> b Source #

foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b Source #

foldl :: (b -> a -> b) -> b -> WhereClause' a -> b Source #

foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b Source #

foldr1 :: (a -> a -> a) -> WhereClause' a -> a Source #

foldl1 :: (a -> a -> a) -> WhereClause' a -> a Source #

toList :: WhereClause' a -> [a] Source #

null :: WhereClause' a -> Bool Source #

length :: WhereClause' a -> Int Source #

elem :: Eq a => a -> WhereClause' a -> Bool Source #

maximum :: Ord a => WhereClause' a -> a Source #

minimum :: Ord a => WhereClause' a -> a Source #

sum :: Num a => WhereClause' a -> a Source #

product :: Num a => WhereClause' a -> a Source #

Traversable WhereClause' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) Source # sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) Source # mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) Source # sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) Source #
Pretty WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source #
KillRange WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT WhereClause Source #
HasRange WhereClause Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: WhereClause -> Range Source #
ToConcrete WhereDeclarations WhereClause Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: WhereDeclarations -> AbsToCon WhereClause Source # bindToConcrete :: WhereDeclarations -> (WhereClause -> AbsToCon b) -> AbsToCon b Source #
Data decls => Data (WhereClause' decls) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (WhereClause' decls) Source #

toConstr :: WhereClause' decls -> Constr Source #

dataTypeOf :: WhereClause' decls -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (WhereClause' decls)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (WhereClause' decls)) Source #

gmapT :: (forall b. Data b => b -> b) -> WhereClause' decls -> WhereClause' decls Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereClause' decls -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WhereClause' decls -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereClause' decls -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereClause' decls -> m (WhereClause' decls) Source #

Show (WhereClause' [Declaration]) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause' [Declaration] -> ShowS Source # show :: WhereClause' [Declaration] -> String Source # showList :: [WhereClause' [Declaration]] -> ShowS Source #
NFData a => NFData (WhereClause' a) Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: WhereClause' a -> () Source #
Null (WhereClause' a) Source # | 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 Source # null :: WhereClause' a -> Bool Source #
ExprLike a => ExprLike (WhereClause' a) Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) Source # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m Source #

data ExprWhere Source #

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 Source #

Constructors

DoBind Range Pattern Expr [LamClause]

    p ← e where cs

DoThen Expr |
DoLet Range [Declaration] |

Instances

Data DoStmt Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoStmt Source #

toConstr :: DoStmt -> Constr Source #

dataTypeOf :: DoStmt -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoStmt) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoStmt) Source #

gmapT :: (forall b. Data b => b -> b) -> DoStmt -> DoStmt Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoStmt -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DoStmt -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DoStmt -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoStmt -> m DoStmt Source #

Show DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods showsPrec :: Int -> DoStmt -> ShowS Source # show :: DoStmt -> String Source # showList :: [DoStmt] -> ShowS Source #
NFData DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods rnf :: DoStmt -> () Source #
Pretty DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: DoStmt -> Doc Source # prettyPrec :: Int -> DoStmt -> Doc Source # prettyList :: [DoStmt] -> Doc Source #
KillRange DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods killRange :: KillRangeT DoStmt Source #
HasRange DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete Methods getRange :: DoStmt -> Range Source #
ExprLike DoStmt Source # |
Instance details Defined in Agda.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt Source # traverseExpr :: Monad m => (Expr -> m Expr) -> DoStmt -> m DoStmt Source # foldExpr :: Monoid m => (Expr -> m) -> DoStmt -> m Source #

data Pragma Source #

Constructors

OptionsPragma Range [String] |
BuiltinPragma Range String QName |
RewritePragma Range [QName] |
ForeignPragma Range String String | first string is backend name
CompilePragma Range String QName String | first string is backend name
StaticPragma Range QName |
InlinePragma Range Bool QName | INLINE or NOINLINE
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).
WarningOnUsage Range QName String | Applies to the named function
InjectivePragma Range QName | Mark a definition as injective for the pattern matching unifier.
DisplayPragma Range Pattern Expr | Display lhs as rhs (modifies the printer).
CatchallPragma Range | Applies to the following function clause.
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.
NoPositivityCheckPragma Range | Applies to the following data/record type or mutual block.
PolarityPragma Range Name [Occurrence] |
NoUniverseCheckPragma Range | Applies to the following data/record type.

Instances

Data Pragma Source # |

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma Source #

toConstr :: Pragma -> Constr Source #

dataTypeOf :: Pragma -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) Source #

gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma Source #

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

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

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

data ThingWithFixity x Source #

Decorating something with `Fixity'`.

Constructors

ThingWithFixity x Fixity' |

Instances

Functor ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b Source # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a Source #
Foldable ThingWithFixity Source # |

Instance details

Defined in Agda.Syntax.Fixity

Methods

fold :: Monoid m => ThingWithFixity m -> m Source #

foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m Source #

foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b Source #

foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b Source #

foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a Source #

toList :: ThingWithFixity a -> [a] Source #

null :: ThingWithFixity a -> Bool Source #

length :: ThingWithFixity a -> Int Source #

elem :: Eq a => a -> ThingWithFixity a -> Bool Source #

maximum :: Ord a => ThingWithFixity a -> a Source #

minimum :: Ord a => ThingWithFixity a -> a Source #

sum :: Num a => ThingWithFixity a -> a Source #

product :: Num a => ThingWithFixity a -> a Source #

Traversable ThingWithFixity Source # |
Instance details Defined in Agda.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) Source # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) Source # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) Source # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) Source #
Data x => Data (ThingWithFixity x) Source # |

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) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ThingWithFixity x) Source #

toConstr :: ThingWithFixity x -> Constr Source #

dataTypeOf :: ThingWithFixity x -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ThingWithFixity x)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ThingWithFixity x)) Source #

gmapT :: (forall b. Data b => b -> b) -> ThingWithFixity x -> ThingWithFixity x Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ThingWithFixity x -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ThingWithFixity x -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ThingWithFixity x -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ThingWithFixity x -> m (ThingWithFixity x) Source #

Show x => Show (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS Source # show :: ThingWithFixity x -> String Source # showList :: [ThingWithFixity x] -> ShowS Source #
Pretty (ThingWithFixity Name) Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source #
KillRange x => KillRange (ThingWithFixity x) Source # |
Instance details Defined in Agda.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source #

type HoleContent = HoleContent' Expr Source #

data HoleContent' e Source #

Extended content of an interaction hole.

Constructors

HoleContentExpr e

    e

HoleContentRewrite [e]

    rewrite e0 | ... | en

Instances

Functor HoleContent' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods fmap :: (a -> b) -> HoleContent' a -> HoleContent' b Source # (<$) :: a -> HoleContent' b -> HoleContent' a Source #
Foldable HoleContent' Source # |

Instance details

Defined in Agda.Syntax.Concrete

Methods

fold :: Monoid m => HoleContent' m -> m Source #

foldMap :: Monoid m => (a -> m) -> HoleContent' a -> m Source #

foldr :: (a -> b -> b) -> b -> HoleContent' a -> b Source #

foldr' :: (a -> b -> b) -> b -> HoleContent' a -> b Source #

foldl :: (b -> a -> b) -> b -> HoleContent' a -> b Source #

foldl' :: (b -> a -> b) -> b -> HoleContent' a -> b Source #

foldr1 :: (a -> a -> a) -> HoleContent' a -> a Source #

foldl1 :: (a -> a -> a) -> HoleContent' a -> a Source #

toList :: HoleContent' a -> [a] Source #

null :: HoleContent' a -> Bool Source #

length :: HoleContent' a -> Int Source #

elem :: Eq a => a -> HoleContent' a -> Bool Source #

maximum :: Ord a => HoleContent' a -> a Source #

minimum :: Ord a => HoleContent' a -> a Source #

sum :: Num a => HoleContent' a -> a Source #

product :: Num a => HoleContent' a -> a Source #

Traversable HoleContent' Source # |
Instance details Defined in Agda.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> HoleContent' a -> f (HoleContent' b) Source # sequenceA :: Applicative f => HoleContent' (f a) -> f (HoleContent' a) Source # mapM :: Monad m => (a -> m b) -> HoleContent' a -> m (HoleContent' b) Source # sequence :: Monad m => HoleContent' (m a) -> m (HoleContent' a) Source #
ToAbstract HoleContent HoleContent Source # | Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: HoleContent0 -> ScopeM HoleContent Source #

topLevelModuleName :: Module -> TopLevelModuleName Source #

Computes the top-level module name.

Precondition: The `Declaration` 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]) Source #

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