| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Internal
Contents
- type Args = [Arg Term]
- type NamedArgs = [NamedArg Term]
- data ConHead = ConHead {}
- class LensConName a where
- 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
- 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.
Constructors
| ConHead | |
class LensConName a where Source #
Minimal complete definition
Methods
getConName :: a -> QName Source #
setConName :: QName -> a -> a Source #
mapConName :: (QName -> QName) -> a -> a Source #
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 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
Eliminations, subsuming applications and projections.
Instances
argNameToString :: ArgName -> String Source #
stringToArgName :: String -> 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.
Constructors
| Abs | The body has (at least) one free variable.
Danger: |
| NoAbs | |
Instances
Types are terms with a sort annotation.
Instances
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #
A traversal for the names in a telescope.
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 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.
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 Source # | |
| Monoid NotBlocked Source # |
|
Something where a meta variable may block reduction.
Constructors
| Blocked | |
Fields
| |
| NotBlocked | |
Fields
| |
Instances
| 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).
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 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!
Constructors
| Clause | |
Fields
| |
Instances
| 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 #
Constructors
| Body a | |
| Bind (Abs (ClauseBodyF a)) | |
| NoBody | for absurd clauses. |
Instances
| 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.
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
| 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 # | |
Arguments
| = 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).
Constructors
| ConPatternInfo | |
Fields
| |
properlyMatching :: Pattern' a -> Bool Source #
Does the pattern perform a match that could fail?
Explicit substitutions
data Substitution' a Source #
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' 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 "()".
isAbsurdPatternName :: PatVarName -> 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.
compressPointerChain :: Term -> Term Source #
Smart constructors
typeDontCare :: Type Source #
A dummy type.
Constructing a singleton telescope.
Minimal complete definition
isHackReifyToMeta :: Term -> Bool Source #
Handling blocked terms.
notBlocked :: a -> Blocked a Source #
Simple operations on terms and types.
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.
Minimal complete definition
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 #
Minimal complete definition
Methods
isProjElim :: e -> Maybe QName Source #
Instances
| 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.
class TermSize a where Source #
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
A meta variable identifier is just a natural number.
Instances
| 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 # | |