- data Term
- data Type = El Sort Term
- data Sort
- data Blocked t
- = Blocked MetaId t
- | NotBlocked t
- type Args = [Arg Term]
- data Telescope
- data Abs a = Abs {}
- telFromList :: [Arg (String, Type)] -> Telescope
- telToList :: Telescope -> [Arg (String, Type)]
- data Clause = Clause {}
- data ClauseBody
- = Body Term
- | Bind (Abs ClauseBody)
- | NoBind ClauseBody
- | NoBody
- data Pattern
- newtype MetaId = MetaId Nat
- arity :: Type -> Nat
- argName :: Type -> String
- data FunView
- funView :: Term -> FunView
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- ignoreBlocking :: Blocked a -> a
- teleLam :: Telescope -> Term -> Term
- getSort :: Type -> Sort
- unEl :: Type -> Term
- sSuc :: Sort -> Sort
- sLub :: Sort -> Sort -> Sort
- impossibleTerm :: String -> Int -> Term
- module Agda.Syntax.Abstract.Name
Documentation
Raw values.
Def
is used for both defined and undefined constants.
Assume there is a type declaration and a definition for
every constant, even if the definition is an empty
list of clauses.
Var Nat Args | |
Lam Hiding (Abs Term) | terms are beta normal |
Lit Literal | |
Def QName Args | |
Con QName Args | |
Pi (Arg Type) (Abs Type) | |
Fun (Arg Type) Type | |
Sort Sort | |
MetaV MetaId Args |
Something where a meta variable may block reduction.
Blocked MetaId t | |
NotBlocked t |
Functor Blocked | |
Typeable1 Blocked | |
Applicative Blocked | |
Foldable Blocked | |
Traversable Blocked | |
Eq t => Eq (Blocked t) | |
Data t => Data (Blocked t) | |
Ord t => Ord (Blocked t) | |
Show t => Show (Blocked t) | |
KillRange a => KillRange (Blocked a) | |
Raise t => Raise (Blocked t) | |
Subst t => Subst (Blocked t) | |
Apply t => Apply (Blocked t) | |
Instantiate a => Instantiate (Blocked a) | |
PrettyTCM a => PrettyTCM (Blocked a) | |
ShrinkC a b => ShrinkC (Blocked a) (Blocked b) |
Sequence of types. An argument of the first type is bound in later types and so on.
The body has (at least) one free variable.
Functor Abs | |
Typeable1 Abs | |
Foldable Abs | |
Traversable Abs | |
Eq a => Eq (Abs a) | |
Data a => Data (Abs a) | |
Ord a => Ord (Abs a) | |
Show a => Show (Abs a) | |
Sized a => Sized (Abs a) | |
KillRange a => KillRange (Abs a) | |
Free a => Free (Abs a) | |
TermLike a => TermLike (Abs a) | |
Strict a => Strict (Abs a) | |
Raise t => Raise (Abs t) | |
(Data a, Subst a) => Subst (Abs a) | |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) | |
KillVar a => KillVar (Abs a) | |
GenC a => GenC (Abs a) | |
EmbPrj a => EmbPrj (Abs a) | |
InstantiateFull t => InstantiateFull (Abs t) | |
Normalise t => Normalise (Abs t) | |
Reduce t => Reduce (Abs t) | |
Instantiate t => Instantiate (Abs t) | |
Occurs a => Occurs (Abs a) | |
ComputeOccurrences a => ComputeOccurrences (Abs a) | |
HasPolarity a => HasPolarity (Abs a) | |
ShrinkC a b => ShrinkC (Abs a) (Abs b) | |
Reify i a => Reify (Abs i) (Name, a) |
A clause is a list of patterns and the clause body should Bind
or
NoBind
in the order the variables occur in the patterns. The NoBind
constructor is an optimisation to avoid substituting for variables that
aren't used.
The telescope contains the types of the pattern variables and the permutation is how to get from the order the variables occur in the patterns to the order they occur in the telescope. For the purpose of the permutation dot patterns counts as variables. TODO: change this!
Clause | |
|
data ClauseBody Source
Patterns are variables, constructors, or wildcards.
QName
is used in ConP
rather than Name
since
a constructor might come from a particular namespace.
This also meshes well with the fact that values (i.e.
the arguments we are matching with) use QName
.
argName :: Type -> StringSource
Suggest a name for the first argument of a function of the given type.
Views
Smart constructors
blockingMeta :: Blocked t -> Maybe MetaIdSource
notBlocked :: a -> Blocked aSource
ignoreBlocking :: Blocked a -> aSource
impossibleTerm :: String -> Int -> TermSource
module Agda.Syntax.Abstract.Name