Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Syntax.Internal
Contents
- 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]
- type ArgName = String
- argNameToString :: ArgName -> String
- stringToArgName :: String -> ArgName
- appendArgNames :: ArgName -> ArgName -> ArgName
- nameToArgName :: Name -> ArgName
- data Abs a
- data Type' a = El {}
- type Type = Type' Term
- class LensSort a where
- data Tele a
- type Telescope = Tele (Dom Type)
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- data Sort
- newtype Level = Max [PlusLevel]
- data PlusLevel
- data LevelAtom
- newtype MetaId = MetaId {}
- data NotBlocked
- data Blocked t
- = Blocked {
- theBlockingMeta :: MetaId
- ignoreBlocking :: t
- | NotBlocked { }
- = Blocked {
- type Blocked_ = Blocked ()
- stuckOn :: Elim -> NotBlocked -> NotBlocked
- data Clause = Clause {}
- clausePats :: Clause -> [Arg Pattern]
- data ClauseBodyF a
- = Body a
- | Bind (Abs (ClauseBodyF a))
- | NoBody
- type ClauseBody = ClauseBodyF Term
- type PatVarName = ArgName
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- data Pattern' x
- type Pattern = Pattern' PatVarName
- type DeBruijnPattern = Pattern' (Int, PatVarName)
- namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
- data ConPatternInfo = ConPatternInfo {}
- noConPatternInfo :: ConPatternInfo
- patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)]
- properlyMatching :: Pattern -> Bool
- data Substitution
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- absurdPatternName :: PatVarName
- isAbsurdPatternName :: PatVarName -> 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
- prop :: Type
- sort :: Sort -> Type
- varSort :: Int -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- impossibleTerm :: String -> Int -> Term
- class SgTel a where
- hackReifyToMeta :: Term
- isHackReifyToMeta :: Term -> Bool
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked 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
- class TermSize a where
- module Agda.Syntax.Abstract.Name
- module Agda.Utils.Pointer
Documentation
data ConHead
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.
Constructors
ConHead | |
class LensConName a where
Minimal complete definition
Methods
getConName :: a -> QName
setConName :: QName -> a -> a
mapConName :: (QName -> QName) -> a -> a
Instances
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 Elims |
|
Lam ArgInfo (Abs Term) | Terms are beta normal. Relevance is ignored |
ExtLam [Clause] Args | Only used by unquote --> reify. Should never appear elsewhere. |
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 |
Instances
data Elim' a
Eliminations, subsuming applications and projections.
Instances
argNameToString :: ArgName -> String
stringToArgName :: String -> ArgName
appendArgNames :: ArgName -> ArgName -> ArgName
nameToArgName :: Name -> ArgName
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
data Type' a
Types are terms with a sort annotation.
Instances
class LensSort a where
Minimal complete definition
data Tele a
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
Functor Tele | |
Foldable Tele | |
Traversable Tele | |
TeleNoAbs Telescope | |
Abstract Telescope | |
KillVar Telescope | |
GenC Telescope | |
AddContext Telescope | |
PrettyTCM Telescope | |
EmbPrj Telescope | |
Reduce Telescope | |
Instantiate Telescope | |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices. |
ShrinkC Telescope Telescope | |
Reify Telescope Telescope | |
Show a => Show (Tele a) | |
Null (Tele a) | |
Sized (Tele a) | The size of a telescope is its length (as a list). |
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 => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
A traversal for the names in a telescope.
mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
replaceEmptyName :: ArgName -> Tele a -> Tele a
data Sort
Sorts.
Constructors
Type Level |
|
Prop | Dummy sort. |
Inf |
|
SizeUniv |
|
DLub Sort (Abs Sort) | Dependent least upper bound. 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 PlusLevel
expressions
each of which is a number or an atom plus a number.
The empty maximum is the canonical representation for level 0.
Instances
data PlusLevel
Constructors
ClosedLevel Integer |
|
Plus Integer LevelAtom |
|
Instances
data LevelAtom
An atomic term of type Level
.
Constructors
MetaLevel MetaId Elims | A meta variable targeting |
BlockedLevel MetaId Term | A term of type |
NeutralLevel NotBlocked Term | A neutral term of type |
UnreducedLevel Term | Introduced by |
Instances
newtype MetaId
A meta variable identifier is just a natural number.
data NotBlocked
Even if we are not stuck on a meta during reduction we can fail to reduce a definition by pattern matching for another reason.
Constructors
StuckOn Elim | The |
Underapplied | Not enough arguments were supplied to complete the matching. |
AbsurdMatch | We matched an absurd clause, results in a neutral |
MissingClauses | We ran out of clauses, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match. |
ReallyNotBlocked | Reduction was not blocked, we reached a whnf
which can be anything but a stuck |
Instances
Show NotBlocked | |
Monoid NotBlocked |
|
data Blocked t
Something where a meta variable may block reduction.
Constructors
Blocked | |
Fields
| |
NotBlocked | |
Fields
|
Instances
Functor Blocked | |
Applicative Blocked | Blocking by a meta is dominant. |
Foldable Blocked | |
Traversable Blocked | |
Monoid Blocked_ | |
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) |
stuckOn :: Elim -> NotBlocked -> NotBlocked
When trying to reduce f es
, on match failed on one
elimination e ∈ es
that came with info r :: NotBlocked
.
stuckOn e r
produces the new NotBlocked
info.
MissingClauses
must be propagated, as this is blockage
that can be lifted in the future (as more clauses are added).
is also propagated, since it provides more
precise information as StuckOn
e0StuckOn e
(as e0
is the original
reason why reduction got stuck and usually a subterm of e
).
An information like StuckOn (Apply (Arg info (Var i [])))
(stuck on a variable) could be used by the lhs/coverage checker
to trigger a split on that (pattern) variable.
In the remaining cases for r
, we are terminally stuck
due to StuckOn e
. Propagating
does not
seem useful.AbsurdMatch
Underapplied
must not be propagated, as this would mean
that f es
is underapplied, which is not the case (it is stuck).
Note that Underapplied
can only arise when projection patterns were
missing to complete the original match (in e
).
(Missing ordinary pattern would mean the e
is of function type,
but we cannot match against something of function type.)
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 namedClausePats)
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!
Constructors
Clause | |
Fields
|
Instances
Show Clause | |
Null Clause | A |
KillRange Clause | |
HasRange Clause | |
Free Clause | |
GetDefs Clause | |
FunArity Clause | Get the number of initial |
GetBody Clause | |
Subst Clause | |
Abstract Clause | |
Abstract FunctionInverse | |
Apply Clause | |
Apply FunctionInverse | |
PrettyTCM Clause | |
PrettyTCM NamedClause | |
EmbPrj Clause | |
EmbPrj FunctionInverse | |
InstantiateFull Clause | |
InstantiateFull FunctionInverse | |
DropArgs Clause | NOTE: does not work for recursive functions. |
DropArgs FunctionInverse | |
Occurs Clause | |
ComputeOccurrences Clause | |
Unquote Clause | |
Reify NamedClause Clause | |
FunArity [Clause] | Get the number of common initial |
UniverseBi ([Type], [Clause]) Pattern | |
UniverseBi ([Type], [Clause]) Term |
clausePats :: Clause -> [Arg Pattern]
data ClauseBodyF a
Constructors
Body a | |
Bind (Abs (ClauseBodyF a)) | |
NoBody | for absurd clauses. |
Instances
Functor ClauseBodyF | |
Foldable ClauseBodyF | |
Traversable ClauseBodyF | |
Null ClauseBody | |
Free ClauseBody | |
GetDefs ClauseBody | |
GetBody ClauseBody | |
Subst ClauseBody | |
Abstract ClauseBody | |
Apply ClauseBody | |
PrettyTCM ClauseBody | |
EmbPrj ClauseBody | |
InstantiateFull ClauseBody | |
Normalise ClauseBody | |
Simplify ClauseBody | |
DropArgs ClauseBody | NOTE: does not go into the body, so does not work for recursive functions. |
Reify ClauseBody RHS | |
Show a => Show (ClauseBodyF a) | |
KillRange a => KillRange (ClauseBodyF a) |
type ClauseBody = ClauseBodyF Term
type PatVarName = ArgName
Pattern variables.
nameToPatVarName :: Name -> PatVarName
data Pattern' x
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
.
Constructors
VarP x | x |
DotP Term | .t |
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)] |
|
LitP Literal | E.g. |
ProjP QName | Projection copattern. Can only appear by itself. |
Instances
type Pattern
Arguments
= Pattern' PatVarName | The |
type DeBruijnPattern = Pattern' (Int, PatVarName)
Type used when numbering pattern variables.
namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
data ConPatternInfo
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
).
Constructors
ConPatternInfo | |
Fields
|
patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)]
properlyMatching :: Pattern -> Bool
Does the pattern perform a match that could fail?
Explicit substitutions
data Substitution
Substitutions.
Constructors
IdS | Identity substitution.
|
EmptyS | Empty substitution, lifts from the empty context.
Apply this to closed terms you want to use in a non-empty context.
|
Term :# Substitution infixr 4 | Substitution extension, ` |
Strengthen Empty Substitution | Strengthening substitution. First argument is |
Wk !Int Substitution | Weakning substitution, lifts to an extended context.
|
Lift !Int Substitution | Lifting substitution. Use this to go under a binder.
|
Absurd Lambda
absurdBody :: Abs Term
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool
Pointers and Sharing
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
Smart constructors
typeDontCare :: Type
A dummy type.
impossibleTerm :: String -> Int -> Term
class SgTel a where
Constructing a singleton telescope.
isHackReifyToMeta :: Term -> Bool
Handling blocked terms.
blockingMeta :: Blocked t -> Maybe MetaId
notBlocked :: a -> Blocked a
Simple operations on terms and types.
stripDontCare :: Term -> Term
Removing a topmost DontCare
constructor.
class Suggest a b where
Pick the better name suggestion, i.e., the one that is not just underscore.
Eliminations.
hasElims :: Term -> Maybe (Elims -> Term, Elims)
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
argFromElim :: Elim -> Arg Term
Drop Apply
constructor. (Unsafe!)
allApplyElims :: Elims -> Maybe Args
Drop Apply
constructors. (Safe)
splitApplyElims :: Elims -> (Args, Elims)
Split at first non-Apply
class IsProjElim e where
Methods
isProjElim :: e -> Maybe QName
Instances
IsProjElim Elim | |
IsProjElim e => IsProjElim (MaybeReduced e) |
dropProjElims :: IsProjElim e => [e] -> [e]
Discard Proj f
entries.
argsFromElims :: Elims -> Args
Discards Proj f
entries.
Null instances.
Show instances.
Sized instances and TermSize.
class TermSize a where
The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).
Not counting towards the term size are:
- sort and color annotations,
- projections.
Minimal complete definition
KillRange instances.
UniverseBi instances.
Simple pretty printing
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer