Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Internal
Contents
- Blocked Terms
- Definitions
- Explicit substitutions
- Views
- Absurd Lambda
- Pointers and Sharing
- Smart constructors
- Handling blocked terms.
- Simple operations on terms and types.
- Eliminations.
- Null instances.
- Show instances.
- Sized instances and TermSize.
- KillRange instances.
- UniverseBi instances.
- Simple pretty printing
- NFData instances
- type Args = [Arg Term]
- type NamedArgs = [NamedArg Term]
- data ConHead = ConHead {}
- class LensConName a where
- data Term
- type ConInfo = ConOrigin
- data Elim' a
- = Apply (Arg a)
- | Proj ProjOrigin QName
- 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]
- type PatVarName = ArgName
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- data Pattern' x
- type Pattern = Pattern' PatVarName
- varP :: ArgName -> Pattern
- data DBPatVar = DBPatVar {}
- type DeBruijnPattern = Pattern' DBPatVar
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- data ConPatternInfo = ConPatternInfo {}
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
- properlyMatching :: DeBruijnPattern -> 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
- unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- argFromElim :: Elim' a -> Arg a
- isApplyElim :: Elim' a -> Maybe (Arg a)
- allApplyElims :: [Elim' a] -> Maybe [Arg a]
- splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
- class IsProjElim e where
- dropProjElims :: IsProjElim e => [e] -> [e]
- argsFromElims :: Elims -> Args
- allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
- class TermSize a where
- pDom :: LensHiding a => a -> Doc -> Doc
- 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.
Constructors
ConHead | |
class LensConName a where #
Minimal complete definition
Methods
getConName :: a -> QName #
setConName :: QName -> a -> a #
mapConName :: (QName -> QName) -> a -> a #
Instances
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 |
Lit Literal | |
Def QName Elims |
|
Con ConHead ConInfo Args |
|
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
Eliminations, subsuming applications and projections.
Constructors
Apply (Arg a) | Application. |
Proj ProjOrigin QName | Projection. |
Instances
argNameToString :: ArgName -> String #
stringToArgName :: String -> ArgName #
appendArgNames :: ArgName -> ArgName -> ArgName #
nameToArgName :: Name -> ArgName #
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
Types are terms with a sort annotation.
Instances
Minimal complete definition
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 # | |
AddContext Telescope # | |
DropArgs Telescope # | NOTE: This creates telescopes with unbound de Bruijn indices. |
PrettyTCM Telescope # | |
Reduce Telescope # | |
Instantiate Telescope # | |
Reify Telescope Telescope # | |
Show a => Show (Tele a) # | |
Pretty a => Pretty (Tele (Dom 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) # | |
NamesIn a => NamesIn (Tele a) # | |
MentionsMeta a => MentionsMeta (Tele a) # | |
(Subst t a, InstantiateFull a) => InstantiateFull (Tele a) # | |
(Subst t a, Normalise a) => Normalise (Tele a) # | |
(Subst t a, Simplify a) => Simplify (Tele a) # | |
ComputeOccurrences a => ComputeOccurrences (Tele a) # | |
Free' a c => Free' (Tele a) c # | |
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) #
A traversal for the names in a telescope.
replaceEmptyName :: ArgName -> Tele a -> Tele a #
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
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
Constructors
ClosedLevel Integer |
|
Plus Integer LevelAtom |
|
Instances
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
Blocked Terms
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 # | |
Semigroup NotBlocked # |
|
Monoid NotBlocked # | |
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 # | |
Semigroup Blocked_ # | |
Monoid Blocked_ # | |
HasOptions NLM # | |
Show t => Show (Blocked t) # | |
KillRange a => KillRange (Blocked a) # | |
TermLike a => TermLike (Blocked a) # | |
PrettyTCM a => PrettyTCM (Blocked a) # | |
Instantiate a => Instantiate (Blocked a) # | |
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
A clause is a list of patterns and the clause body.
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 telescope.
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 # | |
Pretty Clause # | |
Null Clause # | A |
KillRange Clause # | |
HasRange Clause # | |
GetDefs Clause # | |
FunArity Clause # | Get the number of initial |
Free Clause # | |
NamesIn Clause # | |
DropArgs Clause # | NOTE: does not work for recursive functions. |
DropArgs FunctionInverse # | |
PrettyTCM Clause # | |
InstantiateFull Clause # | |
InstantiateFull FunctionInverse # | |
NormaliseProjP Clause # | |
Occurs Clause # | |
ComputeOccurrences Clause # | |
Free' Clause c # | |
FunArity [Clause] # | Get the number of common initial |
PrettyTCM (QNamed Clause) # | |
Reify (QNamed Clause) Clause # | |
UniverseBi ([Type], [Clause]) Pattern # | |
UniverseBi ([Type], [Clause]) Term # | |
clausePats :: Clause -> [Arg DeBruijnPattern] #
type PatVarName = ArgName #
Pattern variables.
patVarNameToString :: PatVarName -> String #
nameToPatVarName :: Name -> PatVarName #
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 ProjOrigin QName | Projection copattern. Can only appear by itself. |
Instances
Functor Pattern' # | |
Foldable Pattern' # | |
Traversable Pattern' # | |
MapNamedArg Pattern' # | |
UniverseBi Elims Pattern # | |
UniverseBi Args Pattern # | |
LabelPatVars Pattern DeBruijnPattern Int # | |
Show x => Show (Pattern' x) # | |
Pretty a => Pretty (Pattern' a) # | |
KillRange a => KillRange (Pattern' a) # | |
IsProjP (Pattern' a) # | |
NamesIn (Pattern' a) # | |
PrettyTCM a => PrettyTCM (Pattern' a) # | |
InstantiateFull a => InstantiateFull (Pattern' a) # | |
Normalise a => Normalise (Pattern' a) # | |
NormaliseProjP (Pattern' x) # | |
IsFlexiblePattern (Pattern' a) # | |
UniverseBi ([Type], [Clause]) Pattern # | |
Arguments
= Pattern' PatVarName | The |
Type used when numbering pattern variables.
Constructors
DBPatVar | |
Fields |
type DeBruijnPattern = Pattern' DBPatVar #
namedVarP :: PatVarName -> Named_ Pattern #
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern #
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
|
toConPatternInfo :: ConInfo -> ConPatternInfo #
Build partial ConPatternInfo
from ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo #
Build ConInfo
from ConPatternInfo
.
properlyMatching :: DeBruijnPattern -> Bool #
Does the pattern perform a match that could fail?
Explicit substitutions
data Substitution' a #
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.
|
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.
|
Instances
Functor Substitution' # | |
Foldable Substitution' # | |
Traversable Substitution' # | |
KillRange Substitution # | |
InstantiateFull Substitution # | |
Show a => Show (Substitution' a) # | |
Pretty a => Pretty (Substitution' a) # | |
Null (Substitution' a) # | |
TermSize a => TermSize (Substitution' a) # | |
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) # | |
type Substitution = Substitution' Term #
Views
isEqualityType :: EqualityView -> Bool #
Absurd Lambda
absurdBody :: Abs Term #
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool #
isAbsurdPatternName :: PatVarName -> Bool #
Pointers and Sharing
ignoreSharing :: Term -> Term #
Remove top-level Shared
data constructors.
ignoreSharingType :: Type -> Type #
updateSharedFM :: (Monad m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term) #
Typically m would be TCM and f would be Blocked.
pointerChain :: Term -> [Ptr Term] #
compressPointerChain :: Term -> Term #
Smart constructors
typeDontCare :: Type #
A dummy type.
impossibleTerm :: String -> Int -> Term #
Constructing a singleton telescope.
Minimal complete definition
hackReifyToMeta :: Term #
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.
notInScopeName :: ArgName -> ArgName #
Make a name that is not in scope.
Pick the better name suggestion, i.e., the one that is not just underscore.
Minimal complete definition
Eliminations.
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term #
Convert Proj
projection eliminations
according to their ProjOrigin
into
Def
projection applications.
hasElims :: Term -> Maybe (Elims -> Term, Elims) #
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
argFromElim :: Elim' a -> Arg a #
Drop Apply
constructor. (Unsafe!)
class IsProjElim e where #
Minimal complete definition
Methods
isProjElim :: e -> Maybe (ProjOrigin, 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.
allProjElims :: Elims -> Maybe [(ProjOrigin, QName)] #
Drop Proj
constructors. (Safe)
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.
Minimal complete definition
KillRange instances.
UniverseBi instances.
Simple pretty printing
pDom :: LensHiding a => a -> Doc -> Doc #
NFData instances
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer
A meta variable identifier is just a natural number.
Instances
Enum MetaId # | |
Eq MetaId # | |
Integral MetaId # | |
Num MetaId # | |
Ord MetaId # | |
Real MetaId # | |
Show MetaId # | Show non-record version of this newtype. |
NFData MetaId # | |
Pretty MetaId # | |
GetDefs MetaId # | |
HasFresh MetaId # | |
UnFreezeMeta MetaId # | |
IsInstantiatedMeta MetaId # | |
PrettyTCM MetaId # | |
FromTerm MetaId # | |
ToTerm MetaId # | |
PrimTerm MetaId # | |
Unquote MetaId # | |
Reify MetaId Expr # | |