Agda.Syntax.Internal
Contents
- data Term
- data Type = El Sort Term
- data Sort
- data Blocked t
- = Blocked MetaId t
- | NotBlocked t
- type Args = [Arg Term]
- data Tele a
- type Telescope = Tele (Arg Type)
- data Abs a = Abs {}
- telFromList :: [Arg (String, Type)] -> Telescope
- telToList :: Telescope -> [Arg (String, Type)]
- data Clauses = Clauses {}
- originalClause :: Clauses -> Clause
- 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
data Term
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.
Constructors
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 | |
DontCare | nuked irrelevant and other stuff |
Instances
data Type
Instances
data Sort
Constructors
Type Term | |
Prop | |
Lub Sort Sort | |
Suc Sort | |
MetaS MetaId Args | |
Inf | |
DLub Sort (Abs Sort) | if the free variable occurs in the second sort the whole thing should reduce to Inf, otherwise it's the normal Lub |
Instances
data Blocked t
Something where a meta variable may block reduction.
Constructors
Blocked MetaId t | |
NotBlocked t |
Instances
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) |
data Tele a
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
Functor Tele | |
Typeable1 Tele | |
Abstract Telescope | |
KillVar Telescope | |
GenC Telescope | |
EmbPrj Telescope | |
Reduce Telescope | |
Instantiate Telescope | |
PrettyTCM Telescope | |
ShrinkC Telescope Telescope | |
Reify Telescope Telescope | |
Eq a => Eq (Tele a) | |
Data a => Data (Tele a) | |
Ord a => Ord (Tele a) | |
Show a => Show (Tele a) | |
Sized (Tele a) | |
KillRange a => KillRange (Tele a) | |
Free a => Free (Tele a) | |
Raise a => Raise (Tele a) | |
Subst a => Subst (Tele a) | |
Subst a => Apply (Tele a) | |
InstantiateFull a => InstantiateFull (Tele a) | |
Normalise a => Normalise (Tele a) | |
ComputeOccurrences a => ComputeOccurrences (Tele a) |
data Abs a
The body has (at least) one free variable.
Instances
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) | |
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) |
telFromList :: [Arg (String, Type)] -> Telescope
data Clauses
Pairs consisting of original and translated clauses.
Constructors
Clauses | |
Fields
|
originalClause :: Clauses -> Clause
The original clause, before translation of record patterns.
data Clause
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. (Note: This optimisation has been disabled.)
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. The body binds the variables in the order they appear in the patterns.
For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!
Constructors
Clause | |
Fields
|
data ClauseBody
Constructors
Body Term | |
Bind (Abs ClauseBody) | |
NoBind ClauseBody | |
NoBody | for absurd clauses. A |
data Pattern
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
.
newtype MetaId
Views
Smart constructors
blockingMeta :: Blocked t -> Maybe MetaId
notBlocked :: a -> Blocked a
ignoreBlocking :: Blocked a -> a
impossibleTerm :: String -> Int -> Term
module Agda.Syntax.Abstract.Name