Safe Haskell | None |
---|
Agda.Syntax.Internal
Contents
- data Term
- data Type = El Sort Term
- data Elim
- topSort :: Type
- data Sort
- newtype Level = Max [PlusLevel]
- data PlusLevel
- data LevelAtom
- data Blocked t
- = Blocked MetaId t
- | NotBlocked t
- type Args = [Arg Term]
- data Tele a
- type Telescope = Tele (Arg Type)
- data Abs a
- unAbs :: Abs a -> a
- absName :: Abs a -> String
- data Clause = Clause {}
- data ClauseBody
- data Pattern
- newtype MetaId = MetaId Nat
- arity :: Type -> Nat
- argName :: Type -> String
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- ignoreBlocking :: Blocked a -> a
- set0 :: Type
- set :: Integer -> Type
- prop :: Type
- sort :: Sort -> Type
- varSort :: Nat -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- getSort :: Type -> Sort
- unEl :: Type -> Term
- 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) | |
Sort Sort | |
Level Level | |
MetaV MetaId Args | |
DontCare Term | irrelevant stuff |
Instances
Eq Term | Syntactic equality, ignores stuff below |
Data Term | |
Ord Term | |
Show Term | |
Typeable Term | |
Sized Term | |
KillRange Term | |
Free Term | |
TermLike Term | |
Strict Term | |
Raise Term | |
Subst Term | |
Abstract Term | |
Apply Term | |
AbstractTerm Term | |
KillVar Term | |
GenC Term | |
EmbPrj Term | |
PrettyTCM Term | |
InstantiateFull Term | |
Normalise Term | |
Reduce Term | |
Instantiate Term | |
Match Term | |
MentionsMeta Term | |
Occurs Term | |
ComputeOccurrences Term | |
HasPolarity Term | |
Unquote Term | |
ApplyHH Term | |
UReduce Term | |
StripAllProjections Term | |
ShrinkC Term Term | |
Reify Term Expr | |
SubstHH Term (HomHet Term) |
data Type
Instances
data Elim
data Sort
Constructors
Type Level | |
Prop | |
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
newtype Level
Instances
data PlusLevel
Constructors
ClosedLevel Integer | |
Plus Integer LevelAtom |
Instances
data LevelAtom
Constructors
MetaLevel MetaId Args | |
BlockedLevel MetaId Term | |
NeutralLevel Term | |
UnreducedLevel Term |
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) | |
PrettyTCM a => PrettyTCM (Blocked a) | |
Instantiate a => Instantiate (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 | |
Foldable Tele | |
Traversable Tele | |
Abstract Telescope | |
KillVar Telescope | |
GenC Telescope | |
EmbPrj Telescope | |
PrettyTCM Telescope | |
Reduce Telescope | |
Instantiate Telescope | |
ShrinkC Telescope Telescope | |
Reify Telescope Telescope | |
(Raise a, Eq a) => Eq (Tele a) | |
Data a => Data (Tele a) | |
(Raise 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) | |
(Raise a, InstantiateFull a) => InstantiateFull (Tele a) | |
(Raise a, Normalise a) => Normalise (Tele a) | |
MentionsMeta a => MentionsMeta (Tele a) | |
ComputeOccurrences a => ComputeOccurrences (Tele a) | |
SubstHH a b => SubstHH (Tele a) (Tele b) |
data Abs a
The body has (at least) one free variable.
Instances
Functor Abs | |
Typeable1 Abs | |
Foldable Abs | |
Traversable Abs | |
(Raise a, Eq a) => Eq (Abs a) | |
Data a => Data (Abs a) | |
(Raise 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) | |
(Raise a, AbstractTerm a) => AbstractTerm (Abs a) | |
KillVar a => KillVar (Abs a) | |
GenC a => GenC (Abs a) | |
EmbPrj a => EmbPrj (Abs a) | |
(Raise t, InstantiateFull t) => InstantiateFull (Abs t) | |
(Raise t, Normalise t) => Normalise (Abs t) | |
(Raise t, Reduce t) => Reduce (Abs t) | |
Instantiate t => Instantiate (Abs t) | |
MentionsMeta t => MentionsMeta (Abs t) | |
Occurs a => Occurs (Abs a) | |
ComputeOccurrences a => ComputeOccurrences (Abs a) | |
HasPolarity a => HasPolarity (Abs a) | |
Unquote a => Unquote (Abs a) | |
ShrinkC a b => ShrinkC (Abs a) (Abs b) | |
SubstHH a b => SubstHH (Abs a) (Abs b) | |
(Free i, Reify i a) => Reify (Abs i) (Name, a) |
data Clause
A clause is a list of patterns and the clause body should Bind
.
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
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
Smart constructors
blockingMeta :: Blocked t -> Maybe MetaId
notBlocked :: a -> Blocked a
ignoreBlocking :: Blocked a -> a
impossibleTerm :: String -> Int -> Term
module Agda.Syntax.Abstract.Name