Safe Haskell | None |
---|
- type Color = Term
- type ArgInfo = ArgInfo Color
- type Arg a = Arg Color a
- type Dom a = Dom Color a
- type NamedArg a = NamedArg Color a
- type Args = [Arg Term]
- type NamedArgs = [NamedArg Term]
- data ConHead = ConHead {}
- class LensConName a where
- getConName :: a -> QName
- setConName :: QName -> a -> a
- mapConName :: (QName -> QName) -> a -> a
- data Term
- data Elim' a
- type Elim = Elim' Term
- type Elims = [Elim]
- data Abs a
- data Type' a = El {}
- type Type = Type' Term
- data Tele a
- type Telescope = Tele (Dom Type)
- mapAbsNamesM :: Applicative m => (String -> m String) -> Tele a -> m (Tele a)
- mapAbsNames :: (String -> String) -> Tele a -> Tele a
- replaceEmptyName :: String -> Tele a -> Tele a
- data Sort
- newtype Level = Max [PlusLevel]
- data PlusLevel
- data LevelAtom
- newtype MetaId = MetaId {}
- data Blocked t
- = Blocked MetaId t
- | NotBlocked t
- data Clause = Clause {}
- clausePats :: Clause -> [Arg Pattern]
- data ClauseBodyF a
- = Body a
- | Bind (Abs (ClauseBodyF a))
- | NoBody
- type ClauseBody = ClauseBodyF Term
- data Pattern
- namedVarP :: String -> Named RString Pattern
- type ConPatternInfo = Maybe (Bool, Arg Type)
- patternVars :: Arg Pattern -> [Arg (Either String Term)]
- properlyMatching :: Pattern -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> 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
- dontCare :: Term -> Term
- typeDontCare :: Type
- topSort :: Type
- set0 :: Type' Term
- set :: Integer -> Type' Term
- prop :: Type' Term
- sort :: Sort -> Type' Term
- varSort :: Int -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- impossibleTerm :: String -> Int -> Term
- sgTel :: Dom (String, Type) -> Telescope
- 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
- class Suggest a b where
- unSpine :: Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- argFromElim :: Elim -> Arg Term
- isApplyElim :: Elim -> Maybe (Arg Term)
- allApplyElims :: Elims -> Maybe Args
- splitApplyElims :: Elims -> (Args, Elims)
- class IsProjElim e where
- isProjElim :: e -> Maybe QName
- dropProjElims :: IsProjElim e => [e] -> [e]
- argsFromElims :: Elims -> Args
- module Agda.Syntax.Abstract.Name
- module Agda.Utils.Pointer
Documentation
Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.
class LensConName a whereSource
getConName :: a -> QNameSource
setConName :: QName -> a -> aSource
mapConName :: (QName -> QName) -> a -> aSource
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 !Int Elims |
|
Lam ArgInfo (Abs Term) | Terms are beta normal. Relevance is ignored |
Lit Literal | |
Def QName Elims |
|
Con ConHead Args | c vs |
Pi (Dom Type) (Abs Type) | dependent or non-dependent function space |
Sort Sort | |
Level Level | |
MetaV !MetaId Elims | |
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 |
Eliminations, subsuming applications and projections.
Functor Elim' | |
Typeable1 Elim' | |
Foldable Elim' | |
Traversable Elim' | |
IsProjElim Elim | |
Subst Elim | |
IsPrefixOf Elims | |
PrettyTCM Elim | |
MentionsMeta Elim | |
InstantiateFull Elim | |
Normalise Elim | |
Simplify Elim | |
Reduce Elim | |
Instantiate Elim | |
UniverseBi Elims Pattern | |
UniverseBi Elims Term | |
Reify Elim Expr | |
Eq (Elim' Term) | |
Ord (Elim' Term) | |
Show a => Show (Elim' a) | |
Sized a => Sized (Elim' a) | |
KillRange a => KillRange (Elim' a) | |
Free a => Free (Elim' a) | |
GetDefs a => GetDefs (Elim' a) | |
TermLike a => TermLike (Elim' a) | |
AbstractTerm a => AbstractTerm (Elim' a) | |
KillVar a => KillVar (Elim' a) | |
GenC a => GenC (Elim' a) | |
Match a => Match (Elim' a) | |
EmbPrj a => EmbPrj (Elim' a) | |
Injectible a => Injectible (Elim' a) | |
Evaluate a => Evaluate (Elim' a) | |
Occurs a => Occurs (Elim' a) | |
SynEq a => SynEq (Elim' a) | |
HasPolarity a => HasPolarity (Elim' a) | |
ComputeOccurrences a => ComputeOccurrences (Elim' a) | |
Unquote a => Unquote (Elim' a) | |
ShrinkC a b => ShrinkC (Elim' a) (Elim' b) |
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.
Types are terms with a sort annotation.
Sequence of types. An argument of the first type is bound in later types and so on.
Functor Tele | |
Typeable1 Tele | |
Foldable Tele | |
Traversable Tele | |
TeleNoAbs Telescope | |
Abstract Telescope | |
KillVar Telescope | |
GenC Telescope | |
AddContext Telescope | |
PrettyTCM Telescope | |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices. |
Reduce Telescope | |
Instantiate Telescope | |
EmbPrj Telescope | |
ShrinkC Telescope Telescope | |
Reify 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) | |
MentionsMeta a => MentionsMeta (Tele a) | |
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) | |
(Subst a, Normalise a) => Normalise (Tele a) | |
(Subst a, Simplify a) => Simplify (Tele a) | |
ComputeOccurrences a => ComputeOccurrences (Tele a) | |
SubstHH a b => SubstHH (Tele a) (Tele b) |
mapAbsNamesM :: Applicative m => (String -> m String) -> Tele a -> m (Tele a)Source
replaceEmptyName :: String -> Tele a -> Tele aSource
Sorts.
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 |
A level is a maximum expression of 0..n plus expressions each of which is a number or an atom plus a number.
MetaLevel MetaId Elims | |
BlockedLevel MetaId Term | |
NeutralLevel Term | |
UnreducedLevel Term | Introduced by |
A meta variable identifier is just a natural number.
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) | |
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
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)
Terms in dot patterns are valid in the clause telescope.
For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!
Clause | |
|
Show Clause | |
Typeable Clause | |
KillRange Clause | |
HasRange Clause | |
FunArity Clause | Get the number of initial |
GetDefs Clause | |
GetBody 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 | |
FunArity [Clause] | Get the number of common initial |
UniverseBi ([Type], [Clause]) Pattern | |
UniverseBi ([Type], [Clause]) Term |
clausePats :: Clause -> [Arg Pattern]Source
data ClauseBodyF a Source
Body a | |
Bind (Abs (ClauseBodyF a)) | |
NoBody | for absurd clauses. |
Functor ClauseBodyF | |
Typeable1 ClauseBodyF | |
Foldable ClauseBodyF | |
Traversable ClauseBodyF | |
Free ClauseBody | |
GetDefs ClauseBody | |
GetBody 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 | |
Simplify ClauseBody | |
EmbPrj ClauseBody | |
Reify ClauseBody RHS | |
Show a => Show (ClauseBodyF a) | |
KillRange a => KillRange (ClauseBodyF a) |
type ClauseBody = ClauseBodyF TermSource
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
.
type ConPatternInfo = Maybe (Bool, Arg Type)Source
The ConPatternInfo
states whether the constructor belongs to
a record type (Just
) or data type (Nothing
).
In the former case, the Bool
says whether the record pattern
orginates from the expansion of an implicit pattern.
The Type
is the type of the whole record pattern.
The scope used for the type is given by any outer scope
plus the clause's telescope (clauseTel
).
properlyMatching :: Pattern -> BoolSource
Does the pattern perform a match that could fail?
Absurd Lambda
Absurd lambdas are internally represented as identity with variable name ().
isAbsurdBody :: Abs Term -> BoolSource
Pointers and Sharing
ignoreSharing :: Term -> TermSource
ignoreSharingType :: Type -> TypeSource
sharedType :: Type -> TypeSource
updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)Source
Typically m would be TCM and f would be Blocked.
pointerChain :: Term -> [Ptr Term]Source
Smart constructors
A dummy type.
impossibleTerm :: String -> Int -> TermSource
Handling blocked terms.
blockingMeta :: Blocked t -> Maybe MetaIdSource
notBlocked :: a -> Blocked aSource
ignoreBlocking :: Blocked a -> aSource
Simple operations on terms and types.
stripDontCare :: Term -> TermSource
Removing a topmost DontCare
constructor.
argName :: Type -> StringSource
Suggest a name for the first argument of a function of the given type.
Pick the better name suggestion, i.e., the one that is not just underscore.
Eliminations.
hasElims :: Term -> Maybe (Elims -> Term, Elims)Source
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
class IsProjElim e whereSource
isProjElim :: e -> Maybe QNameSource
IsProjElim Elim | |
IsProjElim e => IsProjElim (MaybeReduced e) |
dropProjElims :: IsProjElim e => [e] -> [e]Source
Discard Proj f
entries.
argsFromElims :: Elims -> ArgsSource
Discards Proj f
entries.
Show instances.
Sized instances.
KillRange instances.
UniverseBi instances.
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer