| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Internal
Contents
- Blocked Terms
- Definitions
- Explicit substitutions
- Views
- Absurd Lambda
- Pointers and Sharing
- Smart constructors
- Telescopes.
- 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)
- 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
- class PatternVars a b | b -> a where
- properlyMatching :: DeBruijnPattern -> Bool
- data Substitution' a
- = IdS
- | EmptyS Empty
- | 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
- isSort :: Term -> Maybe Sort
- impossibleTerm :: String -> Int -> Term
- hackReifyToMeta :: Term
- isHackReifyToMeta :: Term -> Bool
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- type ListTel' a = [Dom (a, Type)]
- type ListTel = ListTel' ArgName
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- telToList :: Telescope -> ListTel
- class TelToArgs a where
- class SgTel a where
- 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 # | |
| TelToArgs Telescope # | |
| TeleNoAbs Telescope # | |
| PrettyTCM Telescope # | |
| AddContext Telescope # | |
| Reduce Telescope # | |
| Instantiate Telescope # | |
| DropArgs Telescope # | NOTE: This creates telescopes with unbound de Bruijn indices. |
| Reify Telescope Telescope # | |
| Data a => Data (Tele a) # | |
| Show a => Show (Tele a) # | |
| Null (Tele a) # | |
| Pretty a => Pretty (Tele (Dom 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) # | |
| Free a => Free (Tele a) # | |
| NamesIn a => NamesIn (Tele a) # | |
| AddContext (KeepNames Telescope) # | |
| 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) # | |
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
| Data NotBlocked # | |
| 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_ # | |
| 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).
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 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
| Data Clause # | |
| Show Clause # | |
| Null Clause # | A |
| Pretty Clause # | |
| KillRange Clause # | |
| HasRange Clause # | |
| Free Clause # | |
| GetDefs Clause # | |
| FunArity Clause # | Get the number of initial |
| Free Clause # | |
| PrettyTCM Clause # | |
| NamesIn Clause # | |
| InstantiateFull Clause # | |
| InstantiateFull FunctionInverse # | |
| DropArgs Clause # | NOTE: does not work for recursive functions. |
| DropArgs FunctionInverse # | |
| NormaliseProjP Clause # | |
| ComputeOccurrences Clause # | |
| Occurs Clause # | |
| Conversion TOM Clause (Maybe ([Pat O], MExp O)) # | |
| Conversion TOM [Clause] [([Pat O], MExp O)] # | |
| 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)] |
|
| AbsurdP (Pattern' x) |
|
| LitP Literal | E.g. |
| ProjP ProjOrigin QName | Projection copattern. Can only appear by itself. |
Instances
Arguments
| = Pattern' PatVarName | The |
Type used when numbering pattern variables.
Constructors
| DBPatVar | |
Fields | |
Instances
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.
class PatternVars a b | b -> a where #
Extract pattern variables in left-to-right order.
A DotP is also treated as variable (see docu for Clause).
Minimal complete definition
Methods
patternVars :: b -> [Arg (Either a Term)] #
Instances
| PatternVars a b => PatternVars a [b] # | |
| PatternVars a (NamedArg (Pattern' a)) # | |
| PatternVars a (Arg (Pattern' a)) # | |
properlyMatching :: DeBruijnPattern -> Bool #
Does the pattern perform a match that could fail?
Explicit substitutions
data Substitution' a #
Substitutions.
Constructors
| IdS | Identity substitution.
|
| EmptyS Empty | Empty substitution, lifts from the empty context. First argument is |
| 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 # | |
| Data a => Data (Substitution' a) # | |
| Show a => Show (Substitution' a) # | |
| Null (Substitution' a) # | |
| Pretty a => Pretty (Substitution' a) # | |
| TermSize a => TermSize (Substitution' a) # | |
| (Pretty 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 #
hackReifyToMeta :: Term #
isHackReifyToMeta :: Term -> Bool #
Telescopes.
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 #
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope #
telFromList :: ListTel -> Telescope #
Convert a list telescope to a telescope.
Drop the types from a telescope.
Minimal complete definition
Constructing a singleton telescope.
Minimal complete definition
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 # | |
| Data MetaId # | |
| Num MetaId # | |
| Ord MetaId # | |
| Real MetaId # | |
| Show MetaId # | Show non-record version of this newtype. |
| NFData MetaId # | |
| Pretty MetaId # | |
| GetDefs MetaId # | |
| HasFresh MetaId # | |
| PrettyTCM MetaId # | |
| UnFreezeMeta MetaId # | |
| IsInstantiatedMeta MetaId # | |
| FromTerm MetaId # | |
| ToTerm MetaId # | |
| PrimTerm MetaId # | |
| Unquote MetaId # | |
| Reify MetaId Expr # | |