Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Syntax.Internal
Contents
- type Color = Term
- type ArgInfo = ArgInfo Color
- type Arg a = Arg Color a
- type Dom a = Dom Color a
- type NamedArg a = NamedArg Color a
- 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
- 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
- newtype MetaId = MetaId {}
- data Blocked t
- = Blocked MetaId t
- | NotBlocked t
- data Clause = Clause {}
- clausePats :: Clause -> [Arg Pattern]
- data ClauseBodyF a
- = Body a
- | Bind (Abs (ClauseBodyF a))
- | NoBody
- type ClauseBody = ClauseBodyF Term
- type PatVarName = ArgName
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- data Pattern
- namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
- type ConPatternInfo = Maybe (Bool, Arg Type)
- patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)]
- properlyMatching :: Pattern -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- absurdPatternName :: PatVarName
- isAbsurdPatternName :: PatVarName -> Bool
- ignoreSharing :: Term -> Term
- ignoreSharingType :: Type -> Type
- shared :: Term -> Term
- sharedType :: Type -> Type
- updateSharedFM :: (Monad m, Applicative 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
- set0 :: Type' Term
- set :: Integer -> Type' Term
- prop :: Type' Term
- sort :: Sort -> Type' Term
- varSort :: Int -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- impossibleTerm :: String -> Int -> Term
- sgTel :: Dom (ArgName, Type) -> Telescope
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- ignoreBlocking :: Blocked a -> a
- stripDontCare :: Term -> Term
- arity :: Type -> Nat
- argName :: Type -> String
- 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
- module Agda.Syntax.Abstract.Name
- module Agda.Utils.Pointer
Documentation
data ConHead
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
data Term
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
data Elim' a
Eliminations, subsuming applications and projections.
Instances
Functor Elim' | |
Foldable Elim' | |
Traversable Elim' | |
IsProjElim Elim | |
Subst Elim | |
IsPrefixOf Elims | |
PrettyTCM Elim | |
MentionsMeta Elim | |
InstantiateFull Elim | |
Normalise Elim | |
Simplify Elim | |
Reduce Elim | |
Instantiate Elim | |
UniverseBi Elims Pattern | |
UniverseBi Elims Term | |
Reify Elim Expr | |
Eq (Elim' Term) | |
Ord (Elim' Term) | |
Show a => Show (Elim' a) | |
Sized a => Sized (Elim' a) | |
KillRange a => KillRange (Elim' a) | |
Free a => Free (Elim' a) | |
GetDefs a => GetDefs (Elim' a) | |
TermLike a => TermLike (Elim' a) | |
AbstractTerm a => AbstractTerm (Elim' a) | |
KillVar a => KillVar (Elim' a) | |
GenC a => GenC (Elim' a) | |
EmbPrj a => EmbPrj (Elim' a) | |
Match a => Match (Elim' a) | |
Injectible a => Injectible (Elim' a) | |
Evaluate a => Evaluate (Elim' a) | |
Occurs a => Occurs (Elim' a) | |
SynEq a => SynEq (Elim' a) | |
HasPolarity a => HasPolarity (Elim' a) | |
ComputeOccurrences a => ComputeOccurrences (Elim' a) | |
Unquote a => Unquote (Elim' a) | |
ShrinkC a b => ShrinkC (Elim' a) (Elim' b) | |
Typeable (* -> *) Elim' |
argNameToString :: ArgName -> String
stringToArgName :: String -> ArgName
appendArgNames :: ArgName -> ArgName -> ArgName
nameToArgName :: Name -> ArgName
data Abs a
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
data Type' a
Types are terms with a sort annotation.
Instances
data Tele a
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 | |
Abstract Telescope | |
KillVar Telescope | |
GenC Telescope | |
AddContext Telescope | |
PrettyTCM Telescope | |
EmbPrj Telescope | |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices. |
Reduce Telescope | |
Instantiate Telescope | |
ShrinkC Telescope Telescope | |
Reify Telescope Telescope | |
(Subst a, Eq a) => Eq (Tele a) | |
(Subst a, Ord a) => Ord (Tele a) | |
Show a => Show (Tele a) | |
Sized (Tele a) | |
KillRange a => KillRange (Tele a) | |
Free a => Free (Tele a) | |
Subst a => Subst (Tele a) | |
Subst a => Apply (Tele a) | |
MentionsMeta a => MentionsMeta (Tele a) | |
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) | |
(Subst a, Normalise a) => Normalise (Tele a) | |
(Subst a, Simplify a) => Simplify (Tele a) | |
ComputeOccurrences a => ComputeOccurrences (Tele a) | |
SubstHH a b => SubstHH (Tele a) (Tele b) | |
Typeable (* -> *) Tele |
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
Sorts.
Constructors
Type Level | |
Prop | |
Inf | |
DLub Sort (Abs Sort) | if the free variable occurs in the second sort the whole thing should reduce to Inf, otherwise it's the normal Lub |
Instances
newtype Level
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
data PlusLevel
Constructors
ClosedLevel Integer | |
Plus Integer LevelAtom |
Instances
data LevelAtom
Constructors
MetaLevel MetaId Elims | |
BlockedLevel MetaId Term | |
NeutralLevel Term | |
UnreducedLevel Term | Introduced by |
Instances
newtype MetaId
A meta variable identifier is just a natural number.
data Blocked t
Something where a meta variable may block reduction.
Constructors
Blocked MetaId t | |
NotBlocked t |
Instances
Functor Blocked | |
Applicative Blocked | |
Foldable Blocked | |
Traversable Blocked | |
Eq t => Eq (Blocked t) | |
Ord t => Ord (Blocked t) | |
Show t => Show (Blocked t) | |
KillRange a => KillRange (Blocked a) | |
Subst t => Subst (Blocked t) | |
Apply t => Apply (Blocked t) | |
PrettyTCM a => PrettyTCM (Blocked a) | |
Instantiate a => Instantiate (Blocked a) | |
ShrinkC a b => ShrinkC (Blocked a) (Blocked b) | |
Typeable (* -> *) Blocked |
Definitions
data Clause
A clause is a list of patterns and the clause body should Bind
.
The telescope contains the types of the pattern variables and the permutation is 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 clausPats)
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 | |
KillRange Clause | |
HasRange Clause | |
FunArity Clause | Get the number of initial |
GetDefs Clause | |
GetBody Clause | |
Abstract Clause | |
Abstract FunctionInverse | |
Apply Clause | |
Apply FunctionInverse | |
PrettyTCM NamedClause | |
EmbPrj Clause | |
EmbPrj FunctionInverse | |
DropArgs Clause | NOTE: does not work for recursive functions. |
DropArgs FunctionInverse | |
InstantiateFull Clause | |
InstantiateFull FunctionInverse | |
Occurs Clause | |
ComputeOccurrences Clause | |
Typeable * Clause | |
Reify NamedClause Clause | |
FunArity [Clause] | Get the number of common initial |
UniverseBi ([Type], [Clause]) Pattern | |
UniverseBi ([Type], [Clause]) Term |
clausePats :: Clause -> [Arg Pattern]
data ClauseBodyF a
Constructors
Body a | |
Bind (Abs (ClauseBodyF a)) | |
NoBody | for absurd clauses. |
Instances
Functor ClauseBodyF | |
Foldable ClauseBodyF | |
Traversable ClauseBodyF | |
Free ClauseBody | |
GetDefs ClauseBody | |
GetBody ClauseBody | |
Subst ClauseBody | |
Abstract ClauseBody | |
Apply ClauseBody | |
PrettyTCM ClauseBody | |
EmbPrj ClauseBody | |
DropArgs ClauseBody | NOTE: does not go into the body, so does not work for recursive functions. |
InstantiateFull ClauseBody | |
Normalise ClauseBody | |
Simplify ClauseBody | |
Reify ClauseBody RHS | |
Show a => Show (ClauseBodyF a) | |
KillRange a => KillRange (ClauseBodyF a) | |
Typeable (* -> *) ClauseBodyF |
type ClauseBody = ClauseBodyF Term
type PatVarName = ArgName
Pattern variables.
nameToPatVarName :: Name -> PatVarName
data Pattern
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
.
namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
type ConPatternInfo = Maybe (Bool, Arg Type)
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
).
patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)]
properlyMatching :: Pattern -> Bool
Does the pattern perform a match that could fail?
Absurd Lambda
absurdBody :: Abs Term
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool
Pointers and Sharing
ignoreSharing :: Term -> Term
ignoreSharingType :: Type -> Type
sharedType :: Type -> Type
updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)
Typically m would be TCM and f would be Blocked.
updateShared :: (Term -> Term) -> Term -> Term
pointerChain :: Term -> [Ptr Term]
compressPointerChain :: Term -> Term
Smart constructors
typeDontCare :: Type
A dummy type.
impossibleTerm :: String -> Int -> Term
Handling blocked terms.
blockingMeta :: Blocked t -> Maybe MetaId
notBlocked :: a -> Blocked a
ignoreBlocking :: Blocked a -> a
Simple operations on terms and types.
stripDontCare :: Term -> Term
Removing a topmost DontCare
constructor.
class Suggest a b where
Pick the better name suggestion, i.e., the one that is not just underscore.
Eliminations.
hasElims :: Term -> Maybe (Elims -> Term, Elims)
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
argFromElim :: Elim -> Arg Term
Drop Apply
constructor. (Unsafe!)
allApplyElims :: Elims -> Maybe Args
Drop Apply
constructors. (Safe)
splitApplyElims :: Elims -> (Args, Elims)
Split at first non-Apply
class IsProjElim e where
Methods
isProjElim :: e -> Maybe 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.
Show instances.
Sized instances.
KillRange instances.
UniverseBi instances.
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer