| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Abstract
Description
The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).
Synopsis
- type HoleContent = HoleContent' Expr
- class MaybePostfixProjP a where
- type Patterns = [NamedArg Pattern]
- type Pattern = Pattern' Expr
- type NAPs e = [NamedArg (Pattern' e)]
- data Pattern' e
- = VarP BindName
- | ConP ConPatInfo AmbiguousQName (NAPs e)
- | ProjP PatInfo ProjOrigin AmbiguousQName
- | DefP PatInfo AmbiguousQName (NAPs e)
- | WildP PatInfo
- | AsP PatInfo BindName (Pattern' e)
- | DotP PatInfo e
- | AbsurdP PatInfo
- | LitP Literal
- | PatternSynP PatInfo AmbiguousQName (NAPs e)
- | RecP PatInfo [FieldAssignment' (Pattern' e)]
- | WithP PatInfo (Pattern' e)
- type LHSCore = LHSCore' Expr
- data LHSCore' e
- data LHS = LHS {}
- data SpineLHS = SpineLHS {}
- data RHS
- = RHS {
- rhsExpr :: Expr
- rhsConcrete :: Maybe Expr
- | AbsurdRHS
- | WithRHS QName [Expr] [Clause]
- | RewriteRHS {
- rewriteExprs :: [(QName, Expr)]
- rewriteStrippedPats :: [ProblemEq]
- rewriteRHS :: RHS
- rewriteWhereDecls :: WhereDeclarations
- = RHS {
- type SpineClause = Clause' SpineLHS
- type Clause = Clause' LHS
- data WhereDeclarations = WhereDecls {}
- data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool
- data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
- type Telescope = [TypedBindings]
- data TypedBinding
- = TBind Range [WithHiding BindName] Expr
- | TLet Range [LetBinding]
- data TypedBindings = TypedBindings Range (Arg TypedBinding)
- data LamBinding
- type Field = TypeSignature
- type Constructor = TypeSignature
- type TypeSignature = Declaration
- data LetBinding
- data Pragma
- = OptionsPragma [String]
- | BuiltinPragma String ResolvedName
- | BuiltinNoDefPragma String QName
- | RewritePragma QName
- | CompilePragma String QName String
- | CompiledPragma QName String
- | CompiledExportPragma QName String
- | CompiledTypePragma QName String
- | CompiledDataPragma QName String [String]
- | CompiledJSPragma QName String
- | CompiledUHCPragma QName String
- | CompiledDataUHCPragma QName String [String]
- | StaticPragma QName
- | EtaPragma QName
- | InjectivePragma QName
- | InlinePragma Bool QName
- | DisplayPragma QName [NamedArg Pattern] Expr
- data ModuleApplication
- type ImportedName = ImportedName' QName ModuleName
- type Renaming = Renaming' QName ModuleName
- type ImportDirective = ImportDirective' QName ModuleName
- class GetDefInfo a where
- data Declaration
- = Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr
- | Field DefInfo QName (Arg Expr)
- | Primitive DefInfo QName Expr
- | Mutual MutualInfo [Declaration]
- | Section ModuleInfo ModuleName [TypedBindings] [Declaration]
- | Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | Import ModuleInfo ModuleName ImportDirective
- | Pragma Range Pragma
- | Open ModuleInfo ModuleName ImportDirective
- | FunDef DefInfo QName Delayed [Clause]
- | DataSig DefInfo QName Telescope Expr
- | DataDef DefInfo QName [LamBinding] [Constructor]
- | RecSig DefInfo QName Telescope Expr
- | RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) [LamBinding] Expr [Declaration]
- | PatternSynDef QName [Arg Name] (Pattern' Void)
- | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
- | UnquoteDef [DefInfo] [QName] Expr
- | ScopedDecl ScopeInfo [Declaration]
- data ScopeCopyInfo = ScopeCopyInfo {
- renModules :: Ren ModuleName
- renNames :: Ren QName
- type Ren a = [(a, a)]
- data Axiom
- type RecordAssigns = [RecordAssign]
- type RecordAssign = Either Assign ModuleName
- type Assigns = [Assign]
- type Assign = FieldAssignment' Expr
- data Expr
- = Var Name
- | Def QName
- | Proj ProjOrigin AmbiguousQName
- | Con AmbiguousQName
- | PatternSyn AmbiguousQName
- | Macro QName
- | Lit Literal
- | QuestionMark MetaInfo InteractionId
- | Underscore MetaInfo
- | Dot ExprInfo Expr
- | App AppInfo Expr (NamedArg Expr)
- | WithApp ExprInfo Expr [Expr]
- | Lam ExprInfo LamBinding Expr
- | AbsurdLam ExprInfo Hiding
- | ExtendedLam ExprInfo DefInfo QName [Clause]
- | Pi ExprInfo Telescope Expr
- | Fun ExprInfo (Arg Expr) Expr
- | Set ExprInfo Integer
- | Prop ExprInfo
- | Let ExprInfo [LetBinding] Expr
- | ETel Telescope
- | Rec ExprInfo RecordAssigns
- | RecUpdate ExprInfo Expr Assigns
- | ScopedExpr ScopeInfo Expr
- | QuoteGoal ExprInfo Name Expr
- | QuoteContext ExprInfo
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr]
- | DontCare Expr
- type Args = [NamedArg Expr]
- newtype BindName = BindName {}
- initCopyInfo :: ScopeCopyInfo
- noWhereDecls :: WhereDeclarations
- class SubstExpr a where
- type PatternSynDefns = Map QName PatternSynDefn
- type PatternSynDefn = ([Arg Name], Pattern' Void)
- class NameToExpr a where
- class AnyAbstract a where
- class AllNames a where
- axiomName :: Declaration -> QName
- app :: Expr -> [NamedArg Expr] -> Expr
- mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
- patternToExpr :: Pattern -> Expr
- lambdaLiftExpr :: [Name] -> Expr -> Expr
- insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
- class IsNoName a where
- class MkName a where
- class IsProjP a where
- newtype AmbiguousQName = AmbQ {}
- newtype ModuleName = MName {
- mnameToList :: [Name]
- data QNamed a = QNamed {}
- data QName = QName {}
- data Name = Name {
- nameId :: !NameId
- nameConcrete :: Name
- nameBindingSite :: Range
- nameFixity :: Fixity'
- unambiguous :: QName -> AmbiguousQName
- headAmbQ :: AmbiguousQName -> QName
- isAmbiguous :: AmbiguousQName -> Bool
- getUnambiguous :: AmbiguousQName -> Maybe QName
- isAnonymousModuleName :: ModuleName -> Bool
- withRangesOf :: ModuleName -> [Name] -> ModuleName
- withRangesOfQ :: ModuleName -> QName -> ModuleName
- mnameFromList :: [Name] -> ModuleName
- noModuleName :: ModuleName
- commonParentModule :: ModuleName -> ModuleName -> ModuleName
- qnameToList :: QName -> [Name]
- qnameFromList :: [Name] -> QName
- qnameToMName :: QName -> ModuleName
- mnameToQName :: ModuleName -> QName
- showQNameId :: QName -> String
- qnameToConcrete :: QName -> QName
- mnameToConcrete :: ModuleName -> QName
- toTopLevelModuleName :: ModuleName -> TopLevelModuleName
- qualifyM :: ModuleName -> ModuleName -> ModuleName
- qualifyQ :: ModuleName -> QName -> QName
- qualify :: ModuleName -> Name -> QName
- qualify_ :: Name -> QName
- isOperator :: QName -> Bool
- isSubModuleOf :: ModuleName -> ModuleName -> Bool
- isInModule :: QName -> ModuleName -> Bool
- nextName :: Name -> Name
Documentation
type HoleContent = HoleContent' Expr #
class MaybePostfixProjP a where #
Minimal complete definition
Methods
maybePostfixProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) #
Instances
| MaybePostfixProjP a => MaybePostfixProjP (Arg a) # | |
Defined in Agda.Syntax.Abstract Methods maybePostfixProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP e => MaybePostfixProjP (Pattern' e) # | |
Defined in Agda.Syntax.Abstract Methods maybePostfixProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) # | |
| MaybePostfixProjP a => MaybePostfixProjP (Named n a) # | |
Defined in Agda.Syntax.Abstract Methods maybePostfixProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) # | |
Parameterised over the type of dot patterns.
Constructors
| VarP BindName | |
| ConP ConPatInfo AmbiguousQName (NAPs e) | |
| ProjP PatInfo ProjOrigin AmbiguousQName | Destructor pattern |
| DefP PatInfo AmbiguousQName (NAPs e) | Defined pattern: function definition |
| WildP PatInfo | Underscore pattern entered by user. Or generated at type checking for implicit arguments. |
| AsP PatInfo BindName (Pattern' e) | |
| DotP PatInfo e | Dot pattern |
| AbsurdP PatInfo | |
| LitP Literal | |
| PatternSynP PatInfo AmbiguousQName (NAPs e) | |
| RecP PatInfo [FieldAssignment' (Pattern' e)] | |
| WithP PatInfo (Pattern' e) |
|
Instances
The lhs in projection-application and with-pattern view.
Parameterised over the type e of dot patterns.
Constructors
| LHSHead | The head applied to ordinary patterns. |
Fields
| |
| LHSProj | Projection. |
Fields
| |
| LHSWith | With patterns. |
Instances
| Functor LHSCore' # | |
| Foldable LHSCore' # | |
Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => LHSCore' m -> m # foldMap :: Monoid m => (a -> m) -> LHSCore' a -> m # foldr :: (a -> b -> b) -> b -> LHSCore' a -> b # foldr' :: (a -> b -> b) -> b -> LHSCore' a -> b # foldl :: (b -> a -> b) -> b -> LHSCore' a -> b # foldl' :: (b -> a -> b) -> b -> LHSCore' a -> b # foldr1 :: (a -> a -> a) -> LHSCore' a -> a # foldl1 :: (a -> a -> a) -> LHSCore' a -> a # elem :: Eq a => a -> LHSCore' a -> Bool # maximum :: Ord a => LHSCore' a -> a # minimum :: Ord a => LHSCore' a -> a # | |
| Traversable LHSCore' # | |
| ToConcrete LHSCore Pattern # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
| ToAbstract LHSCore (LHSCore' Expr) # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
| Eq e => Eq (LHSCore' e) # | |
| Data e => Data (LHSCore' e) # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore' e -> c (LHSCore' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LHSCore' e) # toConstr :: LHSCore' e -> Constr # dataTypeOf :: LHSCore' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LHSCore' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (LHSCore' e)) # gmapT :: (forall b. Data b => b -> b) -> LHSCore' e -> LHSCore' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r # gmapQ :: (forall d. Data d => d -> u) -> LHSCore' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # | |
| Show e => Show (LHSCore' e) # | |
| KillRange e => KillRange (LHSCore' e) # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) # | |
| HasRange (LHSCore' e) # | |
Defined in Agda.Syntax.Abstract | |
| ExprLike a => ExprLike (LHSCore' a) # | |
Defined in Agda.Syntax.Abstract.Views | |
| ToAbstract (LHSCore' Expr) (LHSCore' Expr) # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
The lhs of a clause in focused (projection-application) view (outside-in).
Projection patters are represented as LHSProjs.
Instances
The lhs of a clause in spine view (inside-out).
Projection patterns are contained in spLhsPats,
represented as ProjP d.
Constructors
| SpineLHS | |
Instances
| Eq SpineLHS # | |
| Data SpineLHS # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpineLHS -> c SpineLHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpineLHS # toConstr :: SpineLHS -> Constr # dataTypeOf :: SpineLHS -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpineLHS) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpineLHS) # gmapT :: (forall b. Data b => b -> b) -> SpineLHS -> SpineLHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r # gmapQ :: (forall d. Data d => d -> u) -> SpineLHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SpineLHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # | |
| Show SpineLHS # | |
| KillRange SpineLHS # | |
Defined in Agda.Syntax.Abstract Methods | |
| HasRange SpineLHS # | |
Defined in Agda.Syntax.Abstract | |
| ExprLike SpineLHS # | |
Defined in Agda.Syntax.Abstract.Views | |
| LHSToSpine LHS SpineLHS # | LHS instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
| LHSToSpine Clause SpineClause # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
| ToConcrete SpineLHS LHS # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
Constructors
| RHS | |
| AbsurdRHS | |
| WithRHS QName [Expr] [Clause] | The |
| RewriteRHS | |
Fields
| |
Instances
| Eq RHS # | Ignore |
| Data RHS # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS -> c RHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RHS # dataTypeOf :: RHS -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RHS) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RHS) # gmapT :: (forall b. Data b => b -> b) -> RHS -> RHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r # gmapQ :: (forall d. Data d => d -> u) -> RHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS -> m RHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS # | |
| Show RHS # | |
| KillRange RHS # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS # | |
| HasRange RHS # | |
Defined in Agda.Syntax.Abstract | |
| AllNames RHS # | |
| ExprLike RHS # | |
| ToAbstract AbstractRHS RHS # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: AbstractRHS -> ScopeM RHS # | |
| ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: RHS -> AbsToCon (RHS0, [Expr], [Expr], [Declaration]) # bindToConcrete :: RHS -> ((RHS0, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b # | |
type SpineClause = Clause' SpineLHS #
data WhereDeclarations #
Constructors
| WhereDecls | |
Fields
| |
Instances
We could throw away where clauses at this point and translate them to
let. It's not obvious how to remember that the let was really a
where clause though, so for the time being we keep it here.
Constructors
| Clause | |
Fields
| |
Instances
| Functor Clause' # | |
| Foldable Clause' # | |
Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Clause' m -> m # foldMap :: Monoid m => (a -> m) -> Clause' a -> m # foldr :: (a -> b -> b) -> b -> Clause' a -> b # foldr' :: (a -> b -> b) -> b -> Clause' a -> b # foldl :: (b -> a -> b) -> b -> Clause' a -> b # foldl' :: (b -> a -> b) -> b -> Clause' a -> b # foldr1 :: (a -> a -> a) -> Clause' a -> a # foldl1 :: (a -> a -> a) -> Clause' a -> a # elem :: Eq a => a -> Clause' a -> Bool # maximum :: Ord a => Clause' a -> a # minimum :: Ord a => Clause' a -> a # | |
| Traversable Clause' # | |
| AllNames Clause # | |
| LHSToSpine Clause SpineClause # | Clause instance. |
Defined in Agda.Syntax.Abstract.Pattern | |
| Reify NamedClause Clause # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
| ToAbstract Clause Clause # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Clause -> ScopeM Clause0 # | |
| Eq lhs => Eq (Clause' lhs) # | |
| Data lhs => Data (Clause' lhs) # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause' lhs -> c (Clause' lhs) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Clause' lhs) # toConstr :: Clause' lhs -> Constr # dataTypeOf :: Clause' lhs -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Clause' lhs)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Clause' lhs)) # gmapT :: (forall b. Data b => b -> b) -> Clause' lhs -> Clause' lhs # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r # gmapQ :: (forall d. Data d => d -> u) -> Clause' lhs -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause' lhs -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # | |
| Show lhs => Show (Clause' lhs) # | |
| KillRange a => KillRange (Clause' a) # | |
Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) # | |
| HasRange a => HasRange (Clause' a) # | |
Defined in Agda.Syntax.Abstract | |
| ExprLike a => ExprLike (Clause' a) # | |
Defined in Agda.Syntax.Abstract.Views | |
| Reify (QNamed Clause) Clause # | |
| ToAbstract (QNamed Clause) Clause # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Clause' a -> AbsToCon [Declaration] # bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b # | |
| ToAbstract [QNamed Clause] [Clause] # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete.
Constructors
| ProblemEq | |
Fields
| |
Instances
| Eq ProblemEq # | |
| Data ProblemEq # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq # toConstr :: ProblemEq -> Constr # dataTypeOf :: ProblemEq -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) # gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # | |
| Show ProblemEq # | |
| KillRange ProblemEq # | |
Defined in Agda.Syntax.Abstract Methods | |
| PrettyTCM ProblemEq # | |
| Subst Term ProblemEq # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq # | |
type Telescope = [TypedBindings] #
data TypedBinding #
A typed binding. Appears in dependent function spaces, typed lambdas, and
telescopes. It might be tempting to simplify this to only bind a single
name at a time, and translate, say, (x y : A) to (x : A)(y : A)
before type-checking. However, this would be slightly problematic:
- We would have to typecheck the type
Aseveral times. - If
Acontains a meta variable or hole, it would be duplicated by such a translation.
While 1. is only slightly inefficient, 2. would be an outright bug.
Duplicating A could not be done naively, we would have to make sure
that the metas of the copy are aliases of the metas of the original.
Constructors
| TBind Range [WithHiding BindName] Expr | As in telescope |
| TLet Range [LetBinding] | E.g. |
Instances
data TypedBindings #
Typed bindings with hiding information.
Constructors
| TypedBindings Range (Arg TypedBinding) | . |
Instances
data LamBinding #
A lambda binding is either domain free or typed.
Constructors
| DomainFree ArgInfo BindName | . |
| DomainFull TypedBindings | . |
Instances
type Field = TypeSignature #
type Constructor = TypeSignature #
type TypeSignature = Declaration #
Only Axioms.
data LetBinding #
Bindings that are valid in a let.
Constructors
| LetBind LetInfo ArgInfo BindName Expr Expr | LetBind info rel name type defn |
| LetPatBind LetInfo Pattern Expr | Irrefutable pattern binding. |
| LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective |
|
| LetOpen ModuleInfo ModuleName ImportDirective | only for highlighting and abstractToConcrete |
| LetDeclaredVariable BindName | Only used for highlighting. Refers to the first occurrence of
|
Instances
Constructors
| OptionsPragma [String] | |
| BuiltinPragma String ResolvedName |
|
| BuiltinNoDefPragma String QName | Builtins that do not come with a definition, but declare a name for an Agda concept. |
| RewritePragma QName | |
| CompilePragma String QName String | |
| CompiledPragma QName String | |
| CompiledExportPragma QName String | |
| CompiledTypePragma QName String | |
| CompiledDataPragma QName String [String] | |
| CompiledJSPragma QName String | |
| CompiledUHCPragma QName String | |
| CompiledDataUHCPragma QName String [String] | |
| StaticPragma QName | |
| EtaPragma QName | For coinductive records, use pragma instead of regular
|
| InjectivePragma QName | |
| InlinePragma Bool QName | |
| DisplayPragma QName [NamedArg Pattern] Expr |
Instances
| Eq Pragma # | |
| Data Pragma # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma # toConstr :: Pragma -> Constr # dataTypeOf :: Pragma -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) # gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # | |
| Show Pragma # | |
| ExprLike Pragma # | |
Defined in Agda.Syntax.Abstract.Views | |
| ToAbstract Pragma [Pragma] # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pragma0 -> ScopeM [Pragma] # | |
data ModuleApplication #
Constructors
| SectionApp Telescope ModuleName [NamedArg Expr] |
|
| RecordModuleIFS ModuleName | M {{...}} |
Instances
type ImportedName = ImportedName' QName ModuleName #
type Renaming = Renaming' QName ModuleName #
class GetDefInfo a where #
Minimal complete definition
Methods
getDefInfo :: a -> Maybe DefInfo #
Instances
| GetDefInfo Declaration # | |
Defined in Agda.Syntax.Abstract Methods getDefInfo :: Declaration -> Maybe DefInfo # | |
data Declaration #
Constructors
| Axiom Axiom DefInfo ArgInfo (Maybe [Occurrence]) QName Expr | Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments. |
| Field DefInfo QName (Arg Expr) | record field |
| Primitive DefInfo QName Expr | primitive function |
| Mutual MutualInfo [Declaration] | a bunch of mutually recursive definitions |
| Section ModuleInfo ModuleName [TypedBindings] [Declaration] | |
| Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective | The |
| Import ModuleInfo ModuleName ImportDirective | The |
| Pragma Range Pragma | |
| Open ModuleInfo ModuleName ImportDirective | only retained for highlighting purposes |
| FunDef DefInfo QName Delayed [Clause] | sequence of function clauses |
| DataSig DefInfo QName Telescope Expr | lone data signature |
| DataDef DefInfo QName [LamBinding] [Constructor] | the |
| RecSig DefInfo QName Telescope Expr | lone record signature |
| RecDef DefInfo QName (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) [LamBinding] Expr [Declaration] | The |
| PatternSynDef QName [Arg Name] (Pattern' Void) | Only for highlighting purposes |
| UnquoteDecl MutualInfo [DefInfo] [QName] Expr | |
| UnquoteDef [DefInfo] [QName] Expr | |
| ScopedDecl ScopeInfo [Declaration] | scope annotation |
Instances
data ScopeCopyInfo #
Constructors
| ScopeCopyInfo | |
Fields
| |
Instances
Is a type signature a postulate or a function signature?
Constructors
| FunSig | A function signature. |
| NoFunSig | Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally). |
Instances
| Eq Axiom # | |
| Data Axiom # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Axiom -> c Axiom # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Axiom # dataTypeOf :: Axiom -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Axiom) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Axiom) # gmapT :: (forall b. Data b => b -> b) -> Axiom -> Axiom # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Axiom -> r # gmapQ :: (forall d. Data d => d -> u) -> Axiom -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Axiom -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Axiom -> m Axiom # | |
| Ord Axiom # | |
| Show Axiom # | |
type RecordAssigns = [RecordAssign] #
type RecordAssign = Either Assign ModuleName #
type Assign = FieldAssignment' Expr #
Record field assignment f = e.
Expressions after scope checking (operators parsed, names resolved).
Constructors
| Var Name | Bound variable. |
| Def QName | Constant: axiom, function, data or record type. |
| Proj ProjOrigin AmbiguousQName | Projection (overloaded). |
| Con AmbiguousQName | Constructor (overloaded). |
| PatternSyn AmbiguousQName | Pattern synonym. |
| Macro QName | Macro. |
| Lit Literal | Literal. |
| QuestionMark MetaInfo InteractionId | Meta variable for interaction.
The |
| Underscore MetaInfo | Meta variable for hidden argument (must be inferred locally). |
| Dot ExprInfo Expr |
|
| App AppInfo Expr (NamedArg Expr) | Ordinary (binary) application. |
| WithApp ExprInfo Expr [Expr] | With application. |
| Lam ExprInfo LamBinding Expr |
|
| AbsurdLam ExprInfo Hiding |
|
| ExtendedLam ExprInfo DefInfo QName [Clause] | |
| Pi ExprInfo Telescope Expr | Dependent function space |
| Fun ExprInfo (Arg Expr) Expr | Non-dependent function space. |
| Set ExprInfo Integer |
|
| Prop ExprInfo |
|
| Let ExprInfo [LetBinding] Expr |
|
| ETel Telescope | Only used when printing telescopes. |
| Rec ExprInfo RecordAssigns | Record construction. |
| RecUpdate ExprInfo Expr Assigns | Record update. |
| ScopedExpr ScopeInfo Expr | Scope annotation. |
| QuoteGoal ExprInfo Name Expr | Binds |
| QuoteContext ExprInfo | Returns the current context. |
| Quote ExprInfo | Quote an identifier |
| QuoteTerm ExprInfo | Quote a term. |
| Unquote ExprInfo | The splicing construct: unquote ... |
| Tactic ExprInfo Expr [NamedArg Expr] [NamedArg Expr] | tactic e x1 .. xn | y1 | .. | yn |
| DontCare Expr | For printing |
Instances
Instances
| Eq BindName # | |
| Data BindName # | |
Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindName -> c BindName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindName # toConstr :: BindName -> Constr # dataTypeOf :: BindName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindName) # gmapT :: (forall b. Data b => b -> b) -> BindName -> BindName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r # gmapQ :: (forall d. Data d => d -> u) -> BindName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BindName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindName -> m BindName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName # | |
| Ord BindName # | |
Defined in Agda.Syntax.Abstract | |
| Show BindName # | |
| KillRange BindName # | |
Defined in Agda.Syntax.Abstract Methods | |
| SetRange BindName # | |
| HasRange BindName # | |
Defined in Agda.Syntax.Abstract | |
| EmbPrj BindName # | |
| ToConcrete BindName Name # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
Minimal complete definition
Instances
| SubstExpr Name # | |
| SubstExpr ModuleName # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName # | |
| SubstExpr TypedBinding # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> TypedBinding -> TypedBinding # | |
| SubstExpr TypedBindings # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> TypedBindings -> TypedBindings # | |
| SubstExpr LetBinding # | |
Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> LetBinding -> LetBinding # | |
| SubstExpr Assign # | |
| SubstExpr Expr # | |
| SubstExpr a => SubstExpr [a] # | |
Defined in Agda.Syntax.Abstract | |
| SubstExpr a => SubstExpr (Arg a) # | |
| (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) # | |
| (SubstExpr a, SubstExpr b) => SubstExpr (a, b) # | |
Defined in Agda.Syntax.Abstract | |
| SubstExpr a => SubstExpr (Named name a) # | |
type PatternSynDefns = Map QName PatternSynDefn #
class NameToExpr a where #
Minimal complete definition
Instances
| NameToExpr ResolvedName # | Assumes name is not |
Defined in Agda.Syntax.Abstract Methods nameExpr :: ResolvedName -> Expr # | |
| NameToExpr AbstractName # | Turn an |
Defined in Agda.Syntax.Abstract Methods nameExpr :: AbstractName -> Expr # | |
class AnyAbstract a where #
Are we in an abstract block?
In that case some definition is abstract.
Minimal complete definition
Methods
anyAbstract :: a -> Bool #
Instances
| AnyAbstract Declaration # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool # | |
| AnyAbstract a => AnyAbstract [a] # | |
Defined in Agda.Syntax.Abstract Methods anyAbstract :: [a] -> Bool # | |
Extracts all the names which are declared in a Declaration.
This does not include open public or let expressions, but it does
include local modules, where clauses and the names of extended
lambdas.
Minimal complete definition
Instances
axiomName :: Declaration -> QName #
The name defined by the given axiom.
Precondition: The declaration has to be a (scoped) Axiom.
patternToExpr :: Pattern -> Expr #
lambdaLiftExpr :: [Name] -> Expr -> Expr #
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name]) #
Check whether a name is the empty name "_".
Minimal complete definition
Instances
| IsNoName String # | |
Defined in Agda.Syntax.Concrete.Name | |
| IsNoName ByteString # | |
Defined in Agda.Syntax.Concrete.Name Methods isNoName :: ByteString -> Bool # | |
| IsNoName QName # | |
Defined in Agda.Syntax.Concrete.Name | |
| IsNoName Name # | |
Defined in Agda.Syntax.Concrete.Name | |
| IsNoName Name # | An abstract name is empty if its concrete name is empty. |
Defined in Agda.Syntax.Abstract.Name | |
Make a Name from some kind of string.
Minimal complete definition
Check whether we are a projection pattern.
Minimal complete definition
Methods
isProjP :: a -> Maybe (ProjOrigin, AmbiguousQName) #
Instances
| IsProjP Void # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Void -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP Expr # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP a => IsProjP (Arg a) # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Arg a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP (Pattern' a) # | |
Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP (Pattern' e) # | |
Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) # | |
| IsProjP a => IsProjP (Named n a) # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) # | |
newtype AmbiguousQName #
Ambiguous qualified names. Used for overloaded constructors.
Invariant: All the names in the list must have the same concrete,
unqualified name. (This implies that they all have the same Range).
Constructors
| AmbQ | |
Fields | |
Instances
newtype ModuleName #
A module name is just a qualified name.
The SetRange instance for module names sets all individual ranges
to the given one.
Constructors
| MName | |
Fields
| |
Instances
Something preceeded by a qualified name.
Instances
| Functor QNamed # | |
| Foldable QNamed # | |
Defined in Agda.Syntax.Abstract.Name Methods fold :: Monoid m => QNamed m -> m # foldMap :: Monoid m => (a -> m) -> QNamed a -> m # foldr :: (a -> b -> b) -> b -> QNamed a -> b # foldr' :: (a -> b -> b) -> b -> QNamed a -> b # foldl :: (b -> a -> b) -> b -> QNamed a -> b # foldl' :: (b -> a -> b) -> b -> QNamed a -> b # foldr1 :: (a -> a -> a) -> QNamed a -> a # foldl1 :: (a -> a -> a) -> QNamed a -> a # elem :: Eq a => a -> QNamed a -> Bool # maximum :: Ord a => QNamed a -> a # minimum :: Ord a => QNamed a -> a # | |
| Traversable QNamed # | |
| Show a => Show (QNamed a) # | Use |
| Pretty a => Pretty (QNamed a) # | |
Defined in Agda.Syntax.Abstract.Name | |
| PrettyTCM (QNamed Clause) # | |
| Reify (QNamed Clause) Clause # | |
| ToAbstract (QNamed Clause) Clause # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| ToAbstract [QNamed Clause] [Clause] # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show.
The SetRange instance for qualified names sets all individual
ranges (including those of the module prefix) to the given one.
Constructors
| QName | |
Fields
| |
Instances
A name is a unique identifier and a suggestion for a concrete name. The concrete name contains the source location (if any) of the name. The source location of the binding site is also recorded.
Constructors
| Name | |
Fields
| |
Instances
unambiguous :: QName -> AmbiguousQName #
A singleton "ambiguous" name.
headAmbQ :: AmbiguousQName -> QName #
Get the first of the ambiguous names.
isAmbiguous :: AmbiguousQName -> Bool #
Is a name ambiguous.
getUnambiguous :: AmbiguousQName -> Maybe QName #
Get the name if unambiguous.
isAnonymousModuleName :: ModuleName -> Bool #
A module is anonymous if the qualification path ends in an underscore.
withRangesOf :: ModuleName -> [Name] -> ModuleName #
Sets the ranges of the individual names in the module name to
match those of the corresponding concrete names. If the concrete
names are fewer than the number of module name name parts, then the
initial name parts get the range noRange.
C.D.E `withRangesOf` [A, B] returns C.D.E but with ranges set
as follows:
C:noRange.D: the range ofA.E: the range ofB.
Precondition: The number of module name name parts has to be at least as large as the length of the list.
withRangesOfQ :: ModuleName -> QName -> ModuleName #
Like withRangesOf, but uses the name parts (qualifier + name)
of the qualified name as the list of concrete names.
mnameFromList :: [Name] -> ModuleName #
commonParentModule :: ModuleName -> ModuleName -> ModuleName #
qnameToList :: QName -> [Name] #
qnameFromList :: [Name] -> QName #
qnameToMName :: QName -> ModuleName #
mnameToQName :: ModuleName -> QName #
showQNameId :: QName -> String #
qnameToConcrete :: QName -> QName #
Turn a qualified name into a concrete name. This should only be used as a fallback when looking up the right concrete name in the scope fails.
mnameToConcrete :: ModuleName -> QName #
toTopLevelModuleName :: ModuleName -> TopLevelModuleName #
Computes the TopLevelModuleName corresponding to the given
module name, which is assumed to represent a top-level module name.
Precondition: The module name must be well-formed.
qualifyM :: ModuleName -> ModuleName -> ModuleName #
qualifyQ :: ModuleName -> QName -> QName #
qualify :: ModuleName -> Name -> QName #
isOperator :: QName -> Bool #
Is the name an operator?
isSubModuleOf :: ModuleName -> ModuleName -> Bool #
isInModule :: QName -> ModuleName -> Bool #