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 Range Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe String)
- | RawApp Range (List2 Expr)
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set Name) OpAppArgs
- | WithApp Range Expr [Expr]
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range (List1 LamBinding) Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range Erased (List1 LamClause)
- | Fun Range (Arg Expr) Expr
- | Pi Telescope1 Expr
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range (List1 Declaration) (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range [Expr]
- | DoBlock Range (List1 DoStmt)
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | DoubleDot Range Expr
- | ETel Telescope
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
- | Generalized Expr
data OpApp e
- = SyntaxBindingLambda Range (List1 LamBinding) e
- | Ordinary e
fromOrdinary :: e -> OpApp e -> e
type OpAppArgs = OpAppArgs' Expr
type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))]
module Agda.Syntax.Concrete.Name
data AppView = AppView Expr [NamedArg Expr]
appView :: Expr -> AppView
unAppView :: AppView -> Expr
rawApp :: List1 Expr -> Expr
rawAppP :: List1 Pattern -> Pattern
isSingleIdentifierP :: Pattern -> Maybe Name
removeParenP :: Pattern -> Pattern
isPattern :: Expr -> Maybe Pattern
isAbsurdP :: Pattern -> Maybe (Range, Hiding)
isBinderP :: Pattern -> Maybe Binder
exprToPatternWithHoles :: Expr -> Pattern
returnExpr :: Expr -> Maybe Expr
data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
}
type Binder = Binder' BoundName
mkBinder_ :: Name -> Binder
mkBinder :: a -> Binder' a
type LamBinding = LamBinding' TypedBinding
data LamBinding' a
- = DomainFree (NamedArg Binder)
- | DomainFull a
dropTypeAndModality :: LamBinding -> [LamBinding]
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
- = TBind Range (List1 (NamedArg Binder)) e
- | TLet Range (List1 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'
- bnameTactic :: TacticAttribute
}
mkBoundName_ :: Name -> BoundName
mkBoundName :: Name -> Fixity' -> BoundName
type TacticAttribute = Maybe Expr
type Telescope = [TypedBinding]
type Telescope1 = List1 TypedBinding
lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
makePi :: Telescope -> Expr -> Expr
mkLam :: Range -> [LamBinding] -> Expr -> Expr
mkLet :: Range -> [Declaration] -> Expr -> Expr
mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e)
data RecordDirective
- = Induction (Ranged Induction)
- | Constructor Name IsInstance
- | Eta (Ranged HasEta0)
- | PatternOrCopattern Range
isRecordDirective :: Declaration -> Maybe RecordDirective
type RecordDirectives = RecordDirectives' (Name, IsInstance)
data Declaration
- = TypeSig ArgInfo TacticAttribute Name Expr
- | FieldSig IsInstance TacticAttribute Name (Arg Expr)
- | Generalize Range [TypeSignature]
- | Field Range [FieldSignature]
- | FunClause LHS RHS WhereClause Bool
- | DataSig Range Name [LamBinding] Expr
- | Data Range Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
- | DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name [LamBinding] Expr
- | RecordDef Range Name RecordDirectives [LamBinding] [Declaration]
- | Record Range Name RecordDirectives [LamBinding] Expr [Declaration]
- | RecordDirective RecordDirective
- | Infix Fixity (List1 Name)
- | Syntax Name Notation
- | PatternSyn Range Name [Arg Name] Pattern
- | Mutual Range [Declaration]
- | InterleavedMutual Range [Declaration]
- | Abstract Range [Declaration]
- | Private Range Origin [Declaration]
- | InstanceB Range [Declaration]
- | LoneConstructor 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
type RenamingDirective = RenamingDirective' Name Name
type HidingDirective = HidingDirective' Name Name
data AsName' a = AsName {
- asName :: a
- asRange :: Range
}
type AsName = AsName' (Either Expr Name)
data OpenShortHand
- = DoOpen
- | DontOpen
type RewriteEqn = RewriteEqn' () Name Pattern Expr
type WithExpr = Named Name (Arg Expr)
data LHS = LHS {
- lhsOriginalPattern :: Pattern
- lhsRewriteEqn :: [RewriteEqn]
- lhsWithExpr :: [WithExpr]
}
data Pattern
- = IdentP QName
- | QuoteP Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP Range (List2 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 Range Literal
- | RecP Range [FieldAssignment' Pattern]
- | EqualP Range [(Expr, Expr)]
- | EllipsisP Range (Maybe Pattern)
- | 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]
  }
- | LHSEllipsis {
  - lhsEllipsisRange :: Range
  - lhsEllipsisPat :: LHSCore
  }
observeHiding :: Expr -> WithHiding Expr
observeRelevance :: Expr -> (Relevance, Expr)
observeModifiers :: Expr -> Arg Expr
data LamClause = LamClause {
- lamLHS :: [Pattern]
- lamRHS :: RHS
- lamCatchAll :: Bool
}
type RHS = RHS' Expr
data RHS' e
- = AbsurdRHS
- | RHS e
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
- = NoWhere
- | AnyWhere Range decls
- | SomeWhere Range Name Access decls
data ExprWhere = ExprWhere Expr WhereClause
data DoStmt
- = DoBind Range Pattern Expr [LamClause]
- | DoThen Expr
- | DoLet Range (List1 Declaration)
data Pragma
- = OptionsPragma Range [String]
- | BuiltinPragma Range RString QName
- | RewritePragma Range Range [QName]
- | ForeignPragma Range RString String
- | CompilePragma Range RString QName String
- | StaticPragma Range QName
- | InlinePragma Range Bool QName
- | ImpossiblePragma Range [String]
- | EtaPragma Range QName
- | WarningOnUsage Range QName Text
- | WarningOnImport Range Text
- | InjectivePragma Range QName
- | DisplayPragma Range Pattern Expr
- | CatchallPragma Range
- | TerminationCheckPragma Range (TerminationCheck Name)
- | NoCoverageCheckPragma Range
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
- | NoUniverseCheckPragma Range
data Module = Mod {
- modPragmas :: [Pragma]
- modDecls :: [Declaration]
}
data ThingWithFixity x = ThingWithFixity x Fixity'
type HoleContent = HoleContent' () Name Pattern Expr
data HoleContent' qn nm p e
- = HoleContentExpr e
- | HoleContentRewrite [RewriteEqn' qn nm p 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 Range Literal	ex: `1` or `"foo"`
QuestionMark Range (Maybe Nat)	ex: `?` or `{! ... !}`
Underscore Range (Maybe String)	ex: `_` or `_A_5`
RawApp Range (List2 Expr)	before parsing operators
App Range Expr (NamedArg