Safe Haskell | None |
---|---|
Language | Haskell98 |
- 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
- 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 DeBruijnPattern]
- data ClauseBodyF a
- = Body a
- | Bind (Abs (ClauseBodyF a))
- | NoBody
- type ClauseBody = ClauseBodyF Term
- imapClauseBody :: (Nat -> a -> b) -> ClauseBodyF a -> ClauseBodyF b
- 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
- namedDBVarP :: Int -> PatVarName -> Named (Ranged PatVarName) DeBruijnPattern
- data ConPatternInfo = ConPatternInfo {
- conPRecord :: Maybe ConPOrigin
- conPType :: Maybe (Arg Type)
- noConPatternInfo :: ConPatternInfo
- patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
- properlyMatching :: Pattern' a -> Bool
- data Substitution' a
- = IdS
- | EmptyS
- | a :# (Substitution' a)
- | Strengthen Empty (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term
- type PatternSubstitution = Substitution' DeBruijnPattern
- data EqualityView
- isEqualityType :: EqualityView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- absurdPatternName :: PatVarName
- isAbsurdPatternName :: PatVarName -> Bool
- ignoreSharing :: Term -> Term
- ignoreSharingType :: Type -> Type
- shared_ :: Term -> Term
- updateSharedFM :: (Monad 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
- 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
- notInScopeName :: ArgName -> ArgName
- 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
- allProjElims :: Elims -> Maybe [QName]
- class TermSize a where
- module Agda.Syntax.Abstract.Name
- module Agda.Utils.Pointer
- newtype MetaId = MetaId {}
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 where Source
getConName :: a -> QName Source
setConName :: QName -> a -> a Source
mapConName :: (QName -> QName) -> a -> a Source
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.
argNameToString :: ArgName -> String Source
stringToArgName :: String -> ArgName Source
appendArgNames :: ArgName -> ArgName -> ArgName Source
nameToArgName :: Name -> ArgName Source
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.
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source
A traversal for the names in a telescope.
replaceEmptyName :: ArgName -> Tele a -> Tele a Source
Sorts.
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. |
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.
ClosedLevel Integer |
|
Plus Integer LevelAtom |
|
An atomic term of type Level
.
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 |
Blocked Terms
data NotBlocked Source
Even if we are not stuck on a meta during reduction we can fail to reduce a definition by pattern matching for another reason.
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 |
Show NotBlocked Source | |
Monoid NotBlocked Source |
|
Something where a meta variable may block reduction.
Blocked | |
| |
NotBlocked | |
|
Functor Blocked Source | |
Applicative Blocked Source | Blocking by a meta is dominant. |
Foldable Blocked Source | |
Traversable Blocked Source | |
Monoid Blocked_ Source | |
HasOptions NLM Source | |
Subst t a => Subst t (Blocked a) Source | |
Show t => Show (Blocked t) Source | |
KillRange a => KillRange (Blocked a) Source | |
Apply t => Apply (Blocked t) Source | |
PrettyTCM a => PrettyTCM (Blocked a) Source | |
Instantiate a => Instantiate (Blocked a) Source | |
ShrinkC a b => ShrinkC (Blocked a) (Blocked b) Source |
stuckOn :: Elim -> NotBlocked -> NotBlocked Source
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
A clause is a list of patterns and the clause body should Bind
.
The telescope contains the types of the pattern variables and the de Bruijn indices say 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!
Clause | |
|
Show Clause Source | |
Null Clause Source | A |
KillRange Clause Source | |
HasRange Clause Source | |
GetDefs Clause Source | |
Free Clause Source | |
FunArity Clause Source | Get the number of initial |
GetBody Clause Source | |
Abstract Clause Source | |
Abstract FunctionInverse Source | |
Apply Clause Source | |
Apply FunctionInverse Source | |
NamesIn Clause Source | |
PrettyTCM Clause Source | |
PrettyTCM NamedClause Source | |
InstantiateFull Clause Source | |
InstantiateFull FunctionInverse Source | |
DropArgs Clause Source | NOTE: does not work for recursive functions. |
DropArgs FunctionInverse Source | |
ComputeOccurrences Clause Source | |
Occurs Clause Source | |
Free' Clause c Source | |
Reify NamedClause Clause Source | |
FunArity [Clause] Source | Get the number of common initial |
UniverseBi ([Type], [Clause]) Pattern Source | |
UniverseBi ([Type], [Clause]) Term Source |
clausePats :: Clause -> [Arg DeBruijnPattern] Source
data ClauseBodyF a Source
Body a | |
Bind (Abs (ClauseBodyF a)) | |
NoBody | for absurd clauses. |
Functor ClauseBodyF Source | |
Foldable ClauseBodyF Source | |
Traversable ClauseBodyF Source | |
Null ClauseBody Source | |
GetDefs ClauseBody Source | |
Free ClauseBody Source | |
GetBody ClauseBody Source | |
Abstract ClauseBody Source | |
Apply ClauseBody Source | |
PrettyTCM ClauseBody Source | |
InstantiateFull ClauseBody Source | |
Normalise ClauseBody Source | |
Simplify ClauseBody Source | |
DropArgs ClauseBody Source | NOTE: does not go into the body, so does not work for recursive functions. |
Free' ClauseBody c Source | |
Subst Term ClauseBody Source | |
Reify ClauseBody RHS Source | |
Show a => Show (ClauseBodyF a) Source | |
Pretty a => Pretty (ClauseBodyF a) Source | |
KillRange a => KillRange (ClauseBodyF a) Source | |
NamesIn a => NamesIn (ClauseBodyF a) Source |
type ClauseBody = ClauseBodyF Term Source
imapClauseBody :: (Nat -> a -> b) -> ClauseBodyF a -> ClauseBodyF b Source
type PatVarName = ArgName Source
Pattern variables.
nameToPatVarName :: Name -> PatVarName Source
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
.
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. |
Functor Pattern' Source | |
Foldable Pattern' Source | |
Traversable Pattern' Source | |
PrettyTCM DeBruijnPattern Source | |
PrettyTCM Pattern Source | |
UniverseBi Elims Pattern Source | |
UniverseBi Args Pattern Source | |
Subst Term Pattern Source | |
Show x => Show (Pattern' x) Source | |
Pretty a => Pretty (Pattern' a) Source | |
KillRange a => KillRange (Pattern' a) Source | |
IsProjP (Pattern' a) Source | |
NamesIn (Pattern' a) Source | |
InstantiateFull a => InstantiateFull (Pattern' a) Source | |
Normalise a => Normalise (Pattern' a) Source | |
IsFlexiblePattern (Pattern' a) Source | |
LabelPatVars (Pattern' x) (Pattern' (i, x)) i Source | |
UniverseBi ([Type], [Clause]) Pattern Source |
= Pattern' PatVarName | The |
type DeBruijnPattern = Pattern' (Int, PatVarName) Source
Type used when numbering pattern variables.
namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern Source
namedDBVarP :: Int -> PatVarName -> Named (Ranged PatVarName) DeBruijnPattern Source
data ConPatternInfo 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
).
ConPatternInfo | |
|
properlyMatching :: Pattern' a -> Bool Source
Does the pattern perform a match that could fail?
Explicit substitutions
data Substitution' a Source
Substitutions.
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.
|
a :# (Substitution' a) infixr 4 | Substitution extension, ` |
Strengthen Empty (Substitution' a) | Strengthening substitution. First argument is |
Wk !Int (Substitution' a) | Weakning substitution, lifts to an extended context.
|
Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Functor Substitution' Source | |
Foldable Substitution' Source | |
Traversable Substitution' Source | |
Pretty Substitution Source | |
KillRange Substitution Source | |
InstantiateFull Substitution Source | |
Subst a a => Subst a (Substitution' a) Source | |
Show a => Show (Substitution' a) Source | |
TermSize a => TermSize (Substitution' a) Source | |
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source |
type Substitution = Substitution' Term Source
Views
isEqualityType :: EqualityView -> Bool Source
Absurd Lambda
absurdBody :: Abs Term Source
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool Source
Pointers and Sharing
ignoreSharing :: Term -> Term Source
Remove top-level Shared
data constructors.
ignoreSharingType :: Type -> Type Source
updateSharedFM :: (Monad 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
compressPointerChain :: Term -> Term Source
Smart constructors
A dummy type.
impossibleTerm :: String -> Int -> Term Source
Constructing a singleton telescope.
isHackReifyToMeta :: Term -> Bool Source
Handling blocked terms.
blockingMeta :: Blocked t -> Maybe MetaId Source
notBlocked :: a -> Blocked a Source
Simple operations on terms and types.
stripDontCare :: Term -> Term Source
Removing a topmost DontCare
constructor.
notInScopeName :: ArgName -> ArgName Source
Make a name that is not in scope.
class Suggest a b where Source
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 where Source
isProjElim :: e -> Maybe QName Source
IsProjElim Elim Source | |
IsProjElim e => IsProjElim (MaybeReduced e) Source |
dropProjElims :: IsProjElim e => [e] -> [e] Source
Discard Proj f
entries.
argsFromElims :: Elims -> Args Source
Discards Proj f
entries.
Null instances.
Show instances.
Sized instances and TermSize.
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.
KillRange instances.
UniverseBi instances.
Simple pretty printing
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer
A meta variable identifier is just a natural number.
Enum MetaId Source | |
Eq MetaId Source | |
Integral MetaId Source | |
Num MetaId Source | |
Ord MetaId Source | |
Real MetaId Source | |
Show MetaId Source | Show non-record version of this newtype. |
NFData MetaId Source | |
Pretty MetaId Source | |
GetDefs MetaId Source | |
HasFresh MetaId Source | |
UnFreezeMeta MetaId Source | |
IsInstantiatedMeta MetaId Source | |
PrettyTCM MetaId Source | |
FromTerm MetaId Source | |
ToTerm MetaId Source | |
PrimTerm MetaId Source | |
Unquote MetaId Source | |
Reify MetaId Expr Source |