| 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
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
| 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 Source
stringToArgName :: String -> ArgName Source
appendArgNames :: ArgName -> ArgName -> 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
| 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) Source
replaceEmptyName :: ArgName -> Tele a -> Tele a Source
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
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
Constructors
| MetaLevel MetaId Elims | |
| BlockedLevel MetaId Term | |
| NeutralLevel Term | |
| UnreducedLevel Term | Introduced by |
Instances
A meta variable identifier is just a natural number.
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
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] Source
data ClauseBodyF a Source
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 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.
namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern Source
type ConPatternInfo = Maybe (Bool, Arg Type) 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).
patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)] Source
properlyMatching :: Pattern -> Bool Source
Does the pattern perform a match that could fail?
Absurd Lambda
absurdBody :: Abs Term Source
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool Source
Pointers and Sharing
ignoreSharing :: Term -> Term Source
ignoreSharingType :: Type -> Type Source
sharedType :: Type -> Type Source
updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term) Source
Typically m would be TCM and f would be Blocked.
pointerChain :: Term -> [Ptr Term] Source
compressPointerChain :: Term -> Term Source
Smart constructors
A dummy type.
impossibleTerm :: String -> Int -> Term Source
Handling blocked terms.
blockingMeta :: Blocked t -> Maybe MetaId Source
notBlocked :: a -> Blocked a Source
ignoreBlocking :: Blocked a -> a Source
Simple operations on terms and types.
stripDontCare :: Term -> Term Source
Removing a topmost DontCare constructor.
argName :: Type -> String Source
Suggest a name for the first argument of a function of the given type.
class Suggest a b where Source
Pick the better name suggestion, i.e., the one that is not just underscore.
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
Methods
isProjElim :: e -> Maybe QName Source
Instances
| IsProjElim Elim | |
| IsProjElim e => IsProjElim (MaybeReduced e) |
dropProjElims :: IsProjElim e => [e] -> [e] Source
Discard Proj f entries.
argsFromElims :: Elims -> Args Source
Discards Proj f entries.
Show instances.
Sized instances.
KillRange instances.
UniverseBi instances.
module Agda.Syntax.Abstract.Name
module Agda.Utils.Pointer