Safe Haskell | None |
---|
Agda.Syntax.Internal
Contents
- data Term
- type Args = [Arg Term]
- data Elim
- data Abs a
- data Type = El {}
- data Tele a
- type Telescope = Tele (Dom Type)
- data Sort
- newtype Level = Max [PlusLevel]
- data PlusLevel
- data LevelAtom
- newtype MetaId = MetaId Nat
- data Blocked t
- = Blocked MetaId t
- | NotBlocked t
- data Clause = Clause {}
- data ClauseBody
- data Pattern
- patternVars :: Arg Pattern -> [Arg (Either String Term)]
- properlyMatching :: Pattern -> Bool
- ignoreSharing :: Term -> Term
- ignoreSharingType :: Type -> Type
- shared :: Term -> Term
- sharedType :: Type -> Type
- updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)
- updateSharedM :: Monad m => (Term -> m Term) -> Term -> m Term
- updateShared :: (Term -> Term) -> Term -> Term
- pointerChain :: Term -> [Ptr Term]
- compressPointerChain :: Term -> Term
- var :: Nat -> Term
- typeDontCare :: Type
- topSort :: Type
- set0 :: Type
- set :: Integer -> Type
- prop :: Type
- sort :: Sort -> Type
- varSort :: Int -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- impossibleTerm :: String -> Int -> Term
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- ignoreBlocking :: Blocked a -> a
- stripDontCare :: Term -> Term
- arity :: Type -> Nat
- argName :: Type -> String
- module Agda.Syntax.Abstract.Name
- module Agda.Utils.Pointer
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 !Int Args |
|
Lam Hiding (Abs Term) | terms are beta normal |
Lit Literal | |
Def QName Args |
|
Con QName Args | c vs |
Pi (Dom Type) (Abs Type) | dependent or non-dependent function space |
Sort Sort | |
Level Level | |
MetaV !MetaId Args | |
DontCare Term | Irrelevant stuff in relevant position, but created
in an irrelevant context. Basically, an internal
version of the irrelevance axiom |
Shared !(Ptr Term) | Explicit sharing |
Instances
Eq Term | Syntactic equality, ignores stuff below |
Ord Term | |
Show Term | |
Typeable Term | |
Sized Term | |
KillRange Term | |
Free Term | |
TermLike Term | |
Subst Term | |
Abstract Term | |
Apply Term | |
AbstractTerm Term | |
PrettyTCM Term | |
InstantiateFull Term | |
Normalise Term | |
Reduce Term | |
Instantiate Term | |
Match Term | |
MentionsMeta Term | |
EmbPrj Term | |
Occurs Term | |
ComputeOccurrences Term | |
HasPolarity Term | |
Unquote Term | |
ApplyHH Term | |
UReduce Term | |
StripAllProjections Term | |
KillVar Term | |
GenC Term | |
UniverseBi Args Pattern | |
UniverseBi Args Term | |
Reify Term Expr | |
ShrinkC Term Term | |
SubstHH Term (HomHet Term) | |
UniverseBi [Term] Term | |
UniverseBi ([Type], [Clause]) Term |
data Elim
Eliminations, subsuming applications and projections. Used for a view which exposes the head of a neutral term.
data Abs a
Binder.
Abs
: The bound variable might appear in the body.
NoAbs
is pseudo-binder, it does not introduce a fresh variable,
similar to the const
of Haskell.
Constructors
Abs | The body has (at least) one free variable.
Danger: |
NoAbs | |
Instances
Functor Abs | |
Typeable1 Abs | |
Foldable Abs | |
Traversable Abs | |
(Subst a, Eq a) => Eq (Abs a) | |
(Subst 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) | |
Subst a => Subst (Abs a) | |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) | |
(Subst t, InstantiateFull t) => InstantiateFull (Abs t) | |
(Subst t, Normalise t) => Normalise (Abs t) | |
(Subst t, Reduce t) => Reduce (Abs t) | |
Instantiate t => Instantiate (Abs t) | |
MentionsMeta t => MentionsMeta (Abs t) | |
EmbPrj a => EmbPrj (Abs a) | |
(Occurs a, Subst a) => Occurs (Abs a) | |
ComputeOccurrences a => ComputeOccurrences (Abs a) | |
HasPolarity a => HasPolarity (Abs a) | |
Unquote a => Unquote (Abs a) | |
KillVar a => KillVar (Abs a) | |
GenC a => GenC (Abs a) | |
SubstHH a b => SubstHH (Abs a) (Abs b) | |
ShrinkC a b => ShrinkC (Abs a) (Abs b) | |
(Free i, Reify i a) => Reify (Abs i) (Name, a) |
data Type
Types are terms with a sort annotation.
Instances
Eq Type | |
Ord Type | |
Show Type | |
Typeable Type | |
Error Type | |
Sized Type | |
KillRange Type | |
Free Type | |
TermLike Type | |
Subst Type | |
Abstract Telescope | |
Abstract Type | |
Apply Type | |
AbstractTerm Type | |
PrettyTCM Telescope | |
PrettyTCM Type | |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices. |
InstantiateFull Type | |
Normalise Type | |
Reduce Telescope | |
Reduce Type | |
Instantiate Telescope | |
Instantiate Type | |
MentionsMeta Type | |
EmbPrj Telescope | |
EmbPrj Type | |
Occurs Type | |
ComputeOccurrences Type | |
HasPolarity Type | |
Unquote Type | |
ToTerm Type | |
PrimTerm Type | |
ApplyHH Type | |
UReduce Type | |
KillVar Telescope | |
KillVar Type | |
GenC Telescope | |
GenC Type | |
Reify Telescope Telescope | |
Reify Type Expr | |
ShrinkC Telescope Telescope | |
ShrinkC Type Type | |
SubstHH Type (HomHet Type) | |
UniverseBi ([Type], [Clause]) Pattern | |
UniverseBi ([Type], [Clause]) Term |
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 | |
PrettyTCM Telescope | |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices. |
Reduce Telescope | |
Instantiate Telescope | |
EmbPrj Telescope | |
KillVar Telescope | |
GenC Telescope | |
Reify Telescope Telescope | |
ShrinkC Telescope Telescope | |
(Subst a, Eq a) => Eq (Tele a) | |
(Subst a, Ord a) => Ord (Tele a) | |
Show a => Show (Tele a) | |
Sized (Tele a) | |
KillRange a => KillRange (Tele a) | |
Free a => Free (Tele a) | |
Subst a => Subst (Tele a) | |
Subst a => Apply (Tele a) | |
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) | |
(Subst 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 Sort
Sorts.
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
A level is a maximum expression of 0..n plus expressions each of which is a number or an atom plus a number.
Instances
data PlusLevel
Constructors
ClosedLevel Integer | |
Plus Integer LevelAtom |
Instances
data LevelAtom
Constructors
MetaLevel MetaId Args | |
BlockedLevel MetaId Term | |
NeutralLevel Term | |
UnreducedLevel Term |
Instances
newtype MetaId
A meta variable identifier is just a natural number.
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) | |
Ord t => Ord (Blocked t) | |
Show t => Show (Blocked t) | |
KillRange a => KillRange (Blocked a) | |
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) |
Definitions
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.
clauseTel ~ permute clausePerm (patternVars clausPats)
For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!
Constructors
Clause | |
Fields
|
Instances
Show Clause | |
Typeable Clause | |
HasRange Clause | |
Abstract Clause | |
Abstract FunctionInverse | |
Apply Clause | |
Apply FunctionInverse | |
PrettyTCM NamedClause | |
DropArgs Clause | NOTE: does not work for recursive functions. |
DropArgs FunctionInverse | |
InstantiateFull Clause | |
InstantiateFull FunctionInverse | |
EmbPrj Clause | |
EmbPrj FunctionInverse | |
Occurs Clause | |
ComputeOccurrences Clause | |
Reify NamedClause Clause | |
UniverseBi ([Type], [Clause]) Pattern | |
UniverseBi ([Type], [Clause]) Term |
data ClauseBody
Instances
Show ClauseBody | |
Typeable ClauseBody | |
Free ClauseBody | |
Subst ClauseBody | |
Abstract ClauseBody | |
Apply ClauseBody | |
PrettyTCM ClauseBody | |
DropArgs ClauseBody | NOTE: does not go into the body, so does not work for recursive functions. |
InstantiateFull ClauseBody | |
Normalise ClauseBody | |
EmbPrj ClauseBody | |
Reify ClauseBody RHS |
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
.
properlyMatching :: Pattern -> Bool
Does the pattern perform a match that could fail?
Smart constructors
ignoreSharing :: Term -> Term
ignoreSharingType :: Type -> Type
sharedType :: Type -> Type
updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)
Typically m would be TCM and f would be Blocked.
updateShared :: (Term -> Term) -> Term -> Term
pointerChain :: Term -> [Ptr Term]
compressPointerChain :: Term -> Term
typeDontCare :: Type
A dummy type.
impossibleTerm :: String -> Int -> Term
Handling blocked terms.
blockingMeta :: Blocked t -> Maybe MetaId
notBlocked :: a -> Blocked a
ignoreBlocking :: Blocked a -> a
Simple operations on terms and types.
stripDontCare :: Term -> Term
Removing a topmost DontCare
constructor.
Show instances.
Sized instances.
KillRange instances.
UniverseBi instances.
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer