Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- class TermSize a where
- class IsProjElim e where
- class Suggest a b where
- class SgTel a where
- class TelToArgs a where
- type ListTel = ListTel' ArgName
- type ListTel' a = [Dom (a, Type)]
- data EqualityView
- type PatternSubstitution = Substitution' DeBruijnPattern
- type Substitution = Substitution' Term
- data Substitution' a
- = IdS
- | EmptyS Empty
- | a :# (Substitution' a)
- | Strengthen Empty (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- class PatternVars a b | b -> a where
- data ConPatternInfo = ConPatternInfo {}
- type DeBruijnPattern = Pattern' DBPatVar
- data DBPatVar = DBPatVar {}
- type Pattern = Pattern' PatVarName
- data Pattern' x
- data PatOrigin
- = PatOSystem
- | PatOSplit
- | PatOVar Name
- | PatODot
- | PatOWild
- | PatOCon
- | PatORec
- | PatOLit
- | PatOAbsurd
- type PatVarName = ArgName
- data Clause = Clause {}
- type Blocked_ = Blocked ()
- data Blocked t
- = Blocked {
- theBlockingMeta :: MetaId
- ignoreBlocking :: t
- | NotBlocked { }
- = Blocked {
- data NotBlocked
- data LevelAtom
- data PlusLevel
- newtype Level = Max [PlusLevel]
- data Sort
- type Telescope = Tele (Dom Type)
- data Tele a
- class LensSort a where
- type Type = Type' Term
- data Type' a = El {}
- data Abs a
- type ArgName = String
- type Elims = [Elim]
- type Elim = Elim' Term
- data Elim' a
- = Apply (Arg a)
- | Proj ProjOrigin QName
- type ConInfo = ConOrigin
- data Term
- class LensConName a where
- data ConHead = ConHead {}
- type NamedArgs = [NamedArg Term]
- type Args = [Arg Term]
- argNameToString :: ArgName -> String
- stringToArgName :: String -> ArgName
- appendArgNames :: ArgName -> ArgName -> ArgName
- nameToArgName :: Name -> ArgName
- stuckOn :: Elim -> NotBlocked -> NotBlocked
- clausePats :: Clause -> [Arg DeBruijnPattern]
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- varP :: a -> Pattern' a
- dotP :: Term -> Pattern' a
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- patternOrigin :: Pattern' x -> Maybe PatOrigin
- properlyMatching :: DeBruijnPattern -> Bool
- isEqualityType :: EqualityView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- absurdPatternName :: PatVarName
- isAbsurdPatternName :: PatVarName -> Bool
- var :: Nat -> Term
- dontCare :: Term -> Term
- typeDontCare :: Type
- topSort :: Type
- sort :: Sort -> Type
- varSort :: Int -> 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
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- telToList :: Telescope -> ListTel
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- stripDontCare :: Term -> Term
- arity :: Type -> Nat
- notInScopeName :: ArgName -> ArgName
- unNotInScopeName :: ArgName -> ArgName
- 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)
- isApplyElim' :: Empty -> Elim' a -> Arg a
- allApplyElims :: [Elim' a] -> Maybe [Arg a]
- splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
- dropProjElims :: IsProjElim e => [e] -> [e]
- argsFromElims :: Elims -> Args
- allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
- pDom :: LensHiding a => a -> Doc -> Doc
- module Agda.Syntax.Abstract.Name
- newtype MetaId = MetaId {}
Documentation
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.
class IsProjElim e where Source #
isProjElim :: e -> Maybe (ProjOrigin, QName) Source #
Instances
IsProjElim Elim Source # | |
Defined in Agda.Syntax.Internal isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source # | |
IsProjElim e => IsProjElim (MaybeReduced e) Source # | |
Defined in Agda.TypeChecking.Monad.Base isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) Source # |
class Suggest a b where Source #
Pick the better name suggestion, i.e., the one that is not just underscore.
Constructing a singleton telescope.
data EqualityView Source #
View type as equality type.
EqualityType | |
OtherType Type | reduced |
Instances
Free EqualityView Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
TermLike EqualityView Source # | |
Defined in Agda.Syntax.Internal.Generic traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView Source # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m Source # | |
PrettyTCM EqualityView Source # | |
Defined in Agda.TypeChecking.Pretty | |
InstantiateFull EqualityView Source # | |
Defined in Agda.TypeChecking.Reduce | |
Normalise EqualityView Source # | |
Defined in Agda.TypeChecking.Reduce | |
Simplify EqualityView Source # | |
Defined in Agda.TypeChecking.Reduce | |
Reduce EqualityView Source # | |
Defined in Agda.TypeChecking.Reduce reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source # | |
Instantiate EqualityView Source # | |
Defined in Agda.TypeChecking.Reduce | |
Subst Term EqualityView Source # | |
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' Term -> EqualityView -> EqualityView Source # |
type Substitution = Substitution' Term Source #
data Substitution' a Source #
Substitutions.
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
class PatternVars a b | b -> a where Source #
Extract pattern variables in left-to-right order.
A DotP
is also treated as variable (see docu for Clause
).
Instances
PatternVars a b => PatternVars a [b] Source # | |
Defined in Agda.Syntax.Internal | |
PatternVars a (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
PatternVars a (Arg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal |
data ConPatternInfo Source #
The ConPatternInfo
states whether the constructor belongs to
a record type (Just
) or data type (Nothing
).
In the former case, the PatOrigin
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 | |
|
Instances
type DeBruijnPattern = Pattern' DBPatVar Source #
Type used when numbering pattern variables.
Instances
= Pattern' PatVarName | The |
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 PatOrigin x | x |
DotP PatOrigin Term | .t |
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)] |
|
LitP Literal | E.g. |
ProjP ProjOrigin QName | Projection copattern. Can only appear by itself. |
Instances
Origin of the pattern: what did the user write in this position?
PatOSystem | Pattern inserted by the system |
PatOSplit | Pattern generated by case split |
PatOVar Name | User wrote a variable pattern |
PatODot | User wrote a dot pattern |
PatOWild | User wrote a wildcard pattern |
PatOCon | User wrote a constructor pattern |
PatORec | User wrote a record pattern |
PatOLit | User wrote a literal pattern |
PatOAbsurd | User wrote an absurd pattern |
Instances
Eq PatOrigin Source # | |
Data PatOrigin Source # | |
Defined in Agda.Syntax.Internal gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatOrigin -> c PatOrigin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatOrigin # toConstr :: PatOrigin -> Constr # dataTypeOf :: PatOrigin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatOrigin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin) # gmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r # gmapQ :: (forall d. Data d => d -> u) -> PatOrigin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PatOrigin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin # | |
Show PatOrigin Source # | |
KillRange PatOrigin Source # | |
Defined in Agda.Syntax.Internal | |
EmbPrj PatOrigin Source # | |
type PatVarName = ArgName Source #
Pattern variables.
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!
Clause | |
|
Instances
Something where a meta variable may block reduction.
Blocked | |
| |
NotBlocked | |
|
Instances
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 |
Instances
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 |
Instances
ClosedLevel Integer |
|
Plus Integer LevelAtom |
|
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
Sorts.
Type Level |
|
Prop | Dummy sort. |
Inf |
|
SizeUniv |
|
PiSort Sort (Abs Sort) | Sort of the pi type. |
UnivSort Sort | Sort of another sort. |
MetaS !MetaId Elims |
Instances
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
Types are terms with a sort annotation.
Instances
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.
Instances
Eliminations, subsuming applications and projections.
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.
Var !Int Elims |
|
Lam ArgInfo (Abs Term) | Terms are beta normal. Relevance is ignored |
Lit Literal | |
Def QName Elims |
|
Con ConHead ConInfo Elims |
|
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 |
Instances
class LensConName a where Source #
getConName :: a -> QName Source #
setConName :: QName -> a -> a Source #
mapConName :: (QName -> QName) -> a -> a Source #
Instances
LensConName ConHead Source # | |
Defined in Agda.Syntax.Internal |
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.
Instances
Eq ConHead Source # | |
Data ConHead Source # | |
Defined in Agda.Syntax.Internal gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConHead -> c ConHead # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConHead # toConstr :: ConHead -> Constr # dataTypeOf :: ConHead -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConHead) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead) # gmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r # gmapQ :: (forall d. Data d => d -> u) -> ConHead -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ConHead -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead # | |
Ord ConHead Source # | |
Show ConHead Source # | |
Pretty ConHead Source # | |
KillRange ConHead Source # | |
Defined in Agda.Syntax.Internal | |
SetRange ConHead Source # | |
HasRange ConHead Source # | |
LensConName ConHead Source # | |
Defined in Agda.Syntax.Internal | |
EmbPrj ConHead Source # | |
PrettyTCM ConHead Source # | |
NamesIn ConHead Source # | |
InstantiateFull ConHead Source # | |
Defined in Agda.TypeChecking.Reduce |
argNameToString :: ArgName -> String Source #
stringToArgName :: String -> ArgName Source #
nameToArgName :: Name -> ArgName 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.)
clausePats :: Clause -> [Arg DeBruijnPattern] Source #
nameToPatVarName :: Name -> PatVarName Source #
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #
toConPatternInfo :: ConInfo -> ConPatternInfo Source #
Build partial ConPatternInfo
from ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo Source #
Build ConInfo
from ConPatternInfo
.
properlyMatching :: DeBruijnPattern -> Bool Source #
Does the pattern perform a match that could fail?
isEqualityType :: EqualityView -> Bool Source #
absurdBody :: Abs Term Source #
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdPatternName :: PatVarName -> Bool Source #
typeDontCare :: Type Source #
A dummy type.
isHackReifyToMeta :: Term -> Bool Source #
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #
A traversal for the names in a telescope.
telFromList :: ListTel -> Telescope Source #
Convert a list telescope to a telescope.
notBlocked :: a -> Blocked a Source #
notInScopeName :: ArgName -> ArgName Source #
Make a name that is not in scope.
unNotInScopeName :: ArgName -> ArgName Source #
Remove the dot from a notInScopeName. This is used when printing function types that have abstracted over not-in-scope names.
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term Source #
Convert Proj
projection eliminations
according to their ProjOrigin
into
Def
projection applications.
hasElims :: Term -> Maybe (Elims -> Term, Elims) Source #
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
dropProjElims :: IsProjElim e => [e] -> [e] Source #
Discard Proj f
entries.
argsFromElims :: Elims -> Args Source #
Discards Proj f
entries.
allProjElims :: Elims -> Maybe [(ProjOrigin, QName)] Source #
Drop Proj
constructors. (Safe)
module Agda.Syntax.Abstract.Name
A meta variable identifier is just a natural number.