Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Internal

Contents

Blocked Terms
Definitions
Explicit substitutions
Views
Absurd Lambda
Pointers and Sharing
Smart constructors
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

Synopsis

Documentation

type Args = [Arg Term] Source #

Type of argument lists.

type NamedArgs = [NamedArg Term] Source #

data ConHead Source #

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
Fields conName :: QName The name of the constructor. conInductive :: Induction Record constructors can be coinductive. conFields :: [QName] The name of the record fields. Empty list for data constructors. `Arg` is not needed here since it is stored in the constructor args.

Instances

Eq ConHead Source #
Methods (==) :: ConHead -> ConHead -> Bool # (/=) :: ConHead -> ConHead -> Bool #
Ord ConHead Source #
Methods compare :: ConHead -> ConHead -> Ordering # (<) :: ConHead -> ConHead -> Bool # (<=) :: ConHead -> ConHead -> Bool # (>) :: ConHead -> ConHead -> Bool # (>=) :: ConHead -> ConHead -> Bool # max :: ConHead -> ConHead -> ConHead # min :: ConHead -> ConHead -> ConHead #
Show ConHead Source #
Methods showsPrec :: Int -> ConHead -> ShowS # show :: ConHead -> String # showList :: [ConHead] -> ShowS #
KillRange ConHead Source #
Methods killRange :: KillRangeT ConHead Source #
SetRange ConHead Source #
Methods setRange :: Range -> ConHead -> ConHead Source #
HasRange ConHead Source #
Methods getRange :: ConHead -> Range Source #
LensConName ConHead Source #
Methods getConName :: ConHead -> QName Source # setConName :: QName -> ConHead -> ConHead Source # mapConName :: (QName -> QName) -> ConHead -> ConHead Source #
NamesIn ConHead Source #
Methods namesIn :: ConHead -> Set QName Source #
PrettyTCM ConHead Source #
Methods prettyTCM :: ConHead -> TCM Doc Source #

class LensConName a where Source #

Minimal complete definition

getConName

Methods

getConName :: a -> QName Source #

setConName :: QName -> a -> a Source #

mapConName :: (QName -> QName) -> a -> a Source #

Instances

LensConName ConHead Source #
Methods getConName :: ConHead -> QName Source # setConName :: QName -> ConHead -> ConHead Source # mapConName :: (QName -> QName) -> ConHead -> ConHead Source #

data Term Source #

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	`x es` neutral
Lam ArgInfo (Abs Term)	Terms are beta normal. Relevance is ignored
Lit Literal
Def QName Elims	`f es`, possibly a delta/iota-redex
Con ConHead ConInfo Args	`c vs` or `record { fs = 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 `.irrAx : .A -> A`.
Shared !(Ptr Term)	Explicit sharing

Instances

Show Term Source #
Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
NFData Type Source #
Methods rnf :: Type -> () #
NFData Term Source #
Methods rnf :: Term -> () #
Pretty Type Source #
Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source #
Pretty Elim Source #
Methods pretty :: Elim -> Doc Source # prettyPrec :: Int -> Elim -> Doc Source #
Pretty Term Source #
Methods pretty :: Term -> Doc Source # prettyPrec :: Int -> Term -> Doc Source #
KillRange Substitution Source #
Methods killRange :: KillRangeT Substitution Source #
KillRange Term Source #
Methods killRange :: KillRangeT Term Source #
TermSize Term Source #
Methods termSize :: Term -> Int Source # tsize :: Term -> Sum Int Source #
IsProjElim Elim Source #
Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source #
GetDefs Type Source #
Methods getDefs :: MonadGetDefs m => Type -> m () Source #
GetDefs Term Source #
Methods getDefs :: MonadGetDefs m => Term -> m () Source #
TermLike Type Source #
Methods traverseTerm :: (Term -> Term) -> Type -> Type Source # traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source # foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #
TermLike Term Source #
Methods traverseTerm :: (Term -> Term) -> Term -> Term Source # traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term Source # foldTerm :: Monoid m => (Term -> m) -> Term -> m Source #
Free Type Source #
Methods freeVars' :: Type -> FreeT
Free Term Source #
Methods freeVars' :: Term -> FreeT
DeBruijn Term Source #	We can substitute `Term`s for variables.
Methods deBruijnVar :: Int -> Term Source # debruijnNamedVar :: String -> Int -> Term Source # deBruijnView :: Term -> Maybe Int Source #
NamesIn Term Source #
Methods namesIn :: Term -> Set QName Source #
TeleNoAbs Telescope Source #
Methods teleNoAbs :: Telescope -> Term -> Term Source #
TeleNoAbs ListTel Source #
Methods teleNoAbs :: ListTel -> Term -> Term Source #
AddContext Telescope Source #
Methods addContext :: MonadTCM tcm => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
UnFreezeMeta Type Source #
Methods unfreezeMeta :: Type -> TCM () Source #
UnFreezeMeta Term Source #
Methods unfreezeMeta :: Term -> TCM () Source #
IsInstantiatedMeta Term Source #
Methods isInstantiatedMeta :: Term -> TCM Bool Source #
IsSizeType Term Source #
Methods isSizeType :: Term -> TCM (Maybe BoundedSize) Source #
DropArgs Telescope Source #	NOTE: This creates telescopes with unbound de Bruijn indices.
Methods dropArgs :: Int -> Telescope -> Telescope Source #
MentionsMeta Type Source #
Methods mentionsMeta :: MetaId -> Type -> Bool Source #
MentionsMeta Elim Source #
Methods mentionsMeta :: MetaId -> Elim -> Bool Source #
MentionsMeta Term Source #
Methods mentionsMeta :: MetaId -> Term -> Bool Source #
PrettyTCM Telescope Source #
Methods prettyTCM :: Telescope -> TCM Doc Source #
PrettyTCM Type Source #
Methods prettyTCM :: Type -> TCM Doc Source #
PrettyTCM Elim Source #
Methods prettyTCM :: Elim -> TCM Doc Source #
PrettyTCM Term Source #
Methods prettyTCM :: Term -> TCM Doc Source #
InstantiateFull Substitution Source #
Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
InstantiateFull Term Source #
Methods instantiateFull' :: Term -> ReduceM Term Source #
Normalise Type Source #
Methods normalise' :: Type -> ReduceM Type Source #
Normalise Elim Source #
Methods normalise' :: Elim -> ReduceM Elim Source #
Normalise Term Source #
Methods normalise' :: Term -> ReduceM Term Source #
Simplify Type Source #
Methods simplify' :: Type -> ReduceM Type Source #
Simplify Elim Source #
Methods simplify' :: Elim -> ReduceM Elim Source #
Simplify Term Source #
Methods simplify' :: Term -> ReduceM Term Source #
Reduce Telescope Source #
Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reduce Type Source #
Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Reduce Elim Source #
Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Reduce Term Source #
Methods reduce' :: Term -> ReduceM Term Source # reduceB' :: Term -> ReduceM (Blocked Term) Source #
Instantiate Telescope Source #
Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Instantiate Type Source #
Methods instantiate' :: Type -> ReduceM Type Source #
Instantiate Elim Source #
Methods instantiate' :: Elim -> ReduceM Elim Source #
Instantiate Term Source #
Methods instantiate' :: Term -> ReduceM Term Source #
Match Term Source #
Methods match :: Term -> Term -> MaybeT TCM [Term] Source #
SynEq Type Source #	Syntactic equality ignores sorts.
Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
SynEq Term Source #	Syntactic term equality ignores `DontCare` stuff.
Methods synEq :: Term -> Term -> SynEqM (Term, Term) synEq' :: Term -> Term -> SynEqM (Term, Term)
Injectible Term Source #
Methods (<:) :: Term -> Term -> ReaderT * (Map QName InjectiveFun) (Compile TCM) InjConstraints Source #
Evaluate Term Source #
Methods evaluate :: Term -> Compile TCM Term Source #
HasPolarity Type Source #
Methods polarities :: Nat -> Type -> TCM [Polarity] Source #
HasPolarity Term Source #
Methods polarities :: Nat -> Term -> TCM [Polarity] Source #
FoldRigid Type Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m Source #
FoldRigid Term Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Term -> TCM m Source #
Occurs Type Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
Occurs Term Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Term -> TCM Term Source # metaOccurs :: MetaId -> Term -> TCM () Source #
ComputeOccurrences Type Source #
Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
ComputeOccurrences Term Source #
Methods occurrences :: Term -> OccM OccurrencesBuilder Source #
ToTerm Type Source #
Methods toTerm :: TCM (Type -> Term) Source # toTermR :: TCM (Type -> ReduceM Term) Source #
ToTerm Term Source #
Methods toTerm :: TCM (Term -> Term) Source # toTermR :: TCM (Term -> ReduceM Term) Source #
PrimTerm Type Source #
Methods primTerm :: Type -> TCM Term Source #
NoProjectedVar Term Source #
Methods noProjectedVar :: Term -> Either ProjVarExc () Source #
AbsTerm Type Source #
Methods absTerm :: Term -> Type -> Type Source #
AbsTerm Term Source #
Methods absTerm :: Term -> Term -> Term Source #
IsPrefixOf Elims Source #
Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
IsPrefixOf Term Source #
Methods isPrefixOf :: Term -> Term -> Maybe Elims Source #
IsPrefixOf Args Source #
Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #
ForcedVariables Term Source #	Assumes that the term is in normal form.
Methods forcedVariables :: Term -> [Nat] Source #
UniverseBi Elims Pattern Source #
Methods universeBi :: Elims -> [Pattern] #
UniverseBi Elims Term Source #
Methods universeBi :: Elims -> [Term] #
UniverseBi Args Pattern Source #
Methods universeBi :: Args -> [Pattern] #
UniverseBi Args Term Source #
Methods universeBi :: Args -> [Term] #
Free' Term c Source #
Methods freeVars' :: Term -> FreeM c Source #
Subst Term AsBinding Source #
Methods applySubst :: Substitution' Term -> AsBinding -> AsBinding Source #
Subst Term DotPatternInst Source #
Methods applySubst :: Substitution' Term -> DotPatternInst -> DotPatternInst Source #
Subst Term ProblemRest Source #
Methods applySubst :: Substitution' Term -> ProblemRest -> ProblemRest Source #
Subst Term SizeConstraint Source #
Methods applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint Source #
Subst Term SizeMeta Source #
Methods applySubst :: Substitution' Term -> SizeMeta -> SizeMeta Source #
Reify Telescope Telescope Source #
Methods reify :: Telescope -> TCM Telescope Source # reifyWhen :: Bool -> Telescope -> TCM Telescope Source #
Reify Type Expr Source #
Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Reify Term Expr Source #
Methods reify :: Term -> TCM Expr Source # reifyWhen :: Bool -> Term -> TCM Expr Source #
Match NLPType Type Source #
Methods match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () Source #
Match NLPat Term Source #
Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Term -> NLM () Source #
PatternFrom Type NLPType Source #
Methods patternFrom :: Relevance -> Int -> Type -> TCM NLPType Source #
PatternFrom Term NLPat Source #
Methods patternFrom :: Relevance -> Int -> Term -> TCM NLPat Source #
Subst Term (Problem' p) Source #
Methods applySubst :: Substitution' Term -> Problem' p -> Problem' p Source #
Subst Term (SizeExpr' NamedRigid SizeMeta) Source #	Only for `raise`.
Methods applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #
SgTel (Dom (ArgName, Type)) Source #
Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source #
Methods sgTel :: Dom Type -> Telescope Source #
AddContext (Dom (String, Type)) Source #
Methods addContext :: MonadTCM tcm => Dom (String, Type) -> tcm a -> tcm a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source #
Methods addContext :: MonadTCM tcm => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source #
Methods addContext :: MonadTCM tcm => Dom Type -> tcm a -> tcm a Source # contextSize :: Dom Type -> Nat Source #
UniverseBi [Term] Term Source #
Methods universeBi :: [Term] -> [Term] #
SgTel (ArgName, Dom Type) Source #
Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([WithHiding Name], Dom Type) Source #
Methods addContext :: MonadTCM tcm => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source #
Methods addContext :: MonadTCM tcm => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source #
Methods addContext :: MonadTCM tcm => (String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source #
Methods addContext :: MonadTCM tcm => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
UniverseBi ([Type], [Clause]) Pattern Source #
Methods universeBi :: ([Type], [Clause]) -> [Pattern] #
UniverseBi ([Type], [Clause]) Term Source #
Methods universeBi :: ([Type], [Clause]) -> [Term] #

type ConInfo = ConOrigin Source #

data Elim' a Source #

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)	Application.
Proj ProjOrigin QName	Projection. `QName` is name of a record projection.

Instances

Functor Elim' Source #
Methods fmap :: (a -> b) -> Elim' a -> Elim' b # (<$) :: a -> Elim' b -> Elim' a #
Foldable Elim' Source #
Methods fold :: Monoid m => Elim' m -> m # foldMap :: Monoid m => (a -> m) -> Elim' a -> m # foldr :: (a -> b -> b) -> b -> Elim' a -> b # foldr' :: (a -> b -> b) -> b -> Elim' a -> b # foldl :: (b -> a -> b) -> b -> Elim' a -> b # foldl' :: (b -> a -> b) -> b -> Elim' a -> b # foldr1 :: (a -> a -> a) -> Elim' a -> a # foldl1 :: (a -> a -> a) -> Elim' a -> a # toList :: Elim' a -> [a] # null :: Elim' a -> Bool # length :: Elim' a -> Int # elem :: Eq a => a -> Elim' a -> Bool # maximum :: Ord a => Elim' a -> a # minimum :: Ord a => Elim' a -> a # sum :: Num a => Elim' a -> a # product :: Num a => Elim' a -> a #
Traversable Elim' Source #
Methods traverse :: Applicative f => (a -> f b) -> Elim' a -> f (Elim' b) # sequenceA :: Applicative f => Elim' (f a) -> f (Elim' a) # mapM :: Monad m => (a -> m b) -> Elim' a -> m (Elim' b) # sequence :: Monad m => Elim' (m a) -> m (Elim' a) #
Pretty Elim Source #
Methods pretty :: Elim -> Doc Source # prettyPrec :: Int -> Elim -> Doc Source #
IsProjElim Elim Source #
Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source #
MentionsMeta Elim Source #
Methods mentionsMeta :: MetaId -> Elim -> Bool Source #
PrettyTCM Elim Source #
Methods prettyTCM :: Elim -> TCM Doc Source #
Normalise Elim Source #
Methods normalise' :: Elim -> ReduceM Elim Source #
Simplify Elim Source #
Methods simplify' :: Elim -> ReduceM Elim Source #
Reduce Elim Source #
Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Instantiate Elim Source #
Methods instantiate' :: Elim -> ReduceM Elim Source #
IsPrefixOf Elims Source #
Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
UniverseBi Elims Pattern Source #
Methods universeBi :: Elims -> [Pattern] #
UniverseBi Elims Term Source #
Methods universeBi :: Elims -> [Term] #
Show a => Show (Elim' a) Source #
Methods showsPrec :: Int -> Elim' a -> ShowS # show :: Elim' a -> String # showList :: [Elim' a] -> ShowS #
NFData a => NFData (Elim' a) Source #
Methods rnf :: Elim' a -> () #
KillRange a => KillRange (Elim' a) Source #
Methods killRange :: KillRangeT (Elim' a) Source #
GetDefs a => GetDefs (Elim' a) Source #
Methods getDefs :: MonadGetDefs m => Elim' a -> m () Source #
TermLike a => TermLike (Elim' a) Source #
Methods traverseTerm :: (Term -> Term) -> Elim' a -> Elim' a Source # traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source # foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #
Free a => Free (Elim' a) Source #
Methods freeVars' :: Elim' a -> FreeT
NamesIn a => NamesIn (Elim' a) Source #
Methods namesIn :: Elim' a -> Set QName Source #
PrettyTCM (Elim' NLPat) Source #
Methods prettyTCM :: Elim' NLPat -> TCM Doc Source #
PrettyTCM (Elim' DisplayTerm) Source #
Methods prettyTCM :: Elim' DisplayTerm -> TCM Doc Source #
InstantiateFull a => InstantiateFull (Elim' a) Source #
Methods instantiateFull' :: Elim' a -> ReduceM (Elim' a) Source #
Match a => Match (Elim' a) Source #
Methods match :: Elim' a -> Elim' a -> MaybeT TCM [Term] Source #
SynEq a => SynEq (Elim' a) Source #
Methods synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a) synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)
Injectible a => Injectible (Elim' a) Source #
Methods (<:) :: Elim' a -> Elim' a -> ReaderT * (Map QName InjectiveFun) (Compile TCM) InjConstraints Source #
Evaluate a => Evaluate (Elim' a) Source #
Methods evaluate :: Elim' a -> Compile TCM (Elim' a) Source #
HasPolarity a => HasPolarity (Elim' a) Source #
Methods polarities :: Nat -> Elim' a -> TCM [Polarity] Source #
FoldRigid a => FoldRigid (Elim' a) Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Elim' a -> TCM m Source #
Occurs a => Occurs (Elim' a) Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Elim' a -> TCM (Elim' a) Source # metaOccurs :: MetaId -> Elim' a -> TCM () Source #
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source #
Methods occurrences :: Elim' a -> OccM OccurrencesBuilder Source #
RaiseNLP a => RaiseNLP (Elim' a) Source #
Methods raiseNLPFrom :: Int -> Int -> Elim' a -> Elim' a Source # raiseNLP :: Int -> Elim' a -> Elim' a Source #
AbsTerm a => AbsTerm (Elim' a) Source #
Methods absTerm :: Term -> Elim' a -> Elim' a Source #
Free' a c => Free' (Elim' a) c Source #
Methods freeVars' :: Elim' a -> FreeM c Source #
Reify i a => Reify (Elim' i) (Elim' a) Source #
Methods reify :: Elim' i -> TCM (Elim' a) Source # reifyWhen :: Bool -> Elim' i -> TCM (Elim' a) Source #
Match a b => Match (Elim' a) (Elim' b) Source #
Methods match :: Relevance -> Telescope -> Telescope -> Elim' a -> Elim' b -> NLM () Source #
PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat) Source #
Methods patternFrom :: Relevance -> Int -> Elim' a -> TCM (Elim' NLPat) Source #

type Elim = Elim' Term Source #

type Elims Source #

Arguments

= [Elim]

eliminations ordered left-to-right.

type ArgName = String Source #

Names in binders and arguments.

argNameToString :: ArgName -> String Source #

stringToArgName :: String -> ArgName Source #

appendArgNames :: ArgName -> ArgName -> ArgName Source #

nameToArgName :: Name -> ArgName Source #

data Abs a 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: `unAbs` doesn't shift variables properly
Fields absName :: ArgName unAbs :: a
NoAbs
Fields absName :: ArgName unAbs :: a

Instances

Functor Abs Source #
Methods fmap :: (a -> b) -> Abs a -> Abs b # (<$) :: a -> Abs b -> Abs a #
Foldable Abs Source #
Methods fold :: Monoid m => Abs m -> m # foldMap :: Monoid m => (a -> m) -> Abs a -> m # foldr :: (a -> b -> b) -> b -> Abs a -> b # foldr' :: (a -> b -> b) -> b -> Abs a -> b # foldl :: (b -> a -> b) -> b -> Abs a -> b # foldl' :: (b -> a -> b) -> b -> Abs a -> b # foldr1 :: (a -> a -> a) -> Abs a -> a # foldl1 :: (a -> a -> a) -> Abs a -> a # toList :: Abs a -> [a] # null :: Abs a -> Bool # length :: Abs a -> Int # elem :: Eq a => a -> Abs a -> Bool # maximum :: Ord a => Abs a -> a # minimum :: Ord a => Abs a -> a # sum :: Num a => Abs a -> a # product :: Num a => Abs a -> a #
Traversable Abs Source #
Methods traverse :: Applicative f => (a -> f b) -> Abs a -> f (Abs b) # sequenceA :: Applicative f => Abs (f a) -> f (Abs a) # mapM :: Monad m => (a -> m b) -> Abs a -> m (Abs b) # sequence :: Monad m => Abs (m a) -> m (Abs a) #
Decoration Abs Source #
Methods traverseF :: Functor m => (a -> m b) -> Abs a -> m (Abs b) Source # distributeF :: Functor m => Abs (m a) -> m (Abs a) Source #
Suggest String (Abs b) Source #
Methods suggest :: String -> Abs b -> String Source #
Suggest Name (Abs b) Source #
Methods suggest :: Name -> Abs b -> String Source #
Show a => Show (Abs a) Source #
Methods showsPrec :: Int -> Abs a -> ShowS # show :: Abs a -> String # showList :: [Abs a] -> ShowS #
Sized a => Sized (Abs a) Source #
Methods size :: Integral n => Abs a -> n Source #
KillRange a => KillRange (Abs a) Source #
Methods killRange :: KillRangeT (Abs a) Source #
LensSort a => LensSort (Abs a) Source #
Methods lensSort :: Lens' Sort (Abs a) Source # getSort :: Abs a -> Sort Source #
GetDefs a => GetDefs (Abs a) Source #
Methods getDefs :: MonadGetDefs m => Abs a -> m () Source #
TermLike a => TermLike (Abs a) Source #
Methods traverseTerm :: (Term -> Term) -> Abs a -> Abs a Source # traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a) Source # foldTerm :: Monoid m => (Term -> m) -> Abs a -> m Source #
Free a => Free (Abs a) Source #
Methods freeVars' :: Abs a -> FreeT
NamesIn a => NamesIn (Abs a) Source #
Methods namesIn :: Abs a -> Set QName Source #
UnFreezeMeta a => UnFreezeMeta (Abs a) Source #
Methods unfreezeMeta :: Abs a -> TCM () Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #	Does not worry about raising.
Methods isInstantiatedMeta :: Abs a -> TCM Bool Source #
MentionsMeta t => MentionsMeta (Abs t) Source #
Methods mentionsMeta :: MetaId -> Abs t -> Bool Source #
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) Source #
Methods instantiateFull' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Normalise a) => Normalise (Abs a) Source #
Methods normalise' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Simplify a) => Simplify (Abs a) Source #
Methods simplify' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Reduce a) => Reduce (Abs a) Source #
Methods reduce' :: Abs a -> ReduceM (Abs a) Source # reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #
Instantiate t => Instantiate (Abs t) Source #
Methods instantiate' :: Abs t -> ReduceM (Abs t) Source #
(Subst t a, SynEq a) => SynEq (Abs a) Source #
Methods synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a) synEq' :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)
Evaluate a => Evaluate (Abs a) Source #
Methods evaluate :: Abs a -> Compile TCM (Abs a) Source #
HasPolarity a => HasPolarity (Abs a) Source #
Methods polarities :: Nat -> Abs a -> TCM [Polarity] Source #
(Subst t a, FoldRigid a) => FoldRigid (Abs a) Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Abs a -> TCM m Source #
(Occurs a, Subst t a) => Occurs (Abs a) Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Abs a -> TCM (Abs a) Source # metaOccurs :: MetaId -> Abs a -> TCM () Source #
ComputeOccurrences a => ComputeOccurrences (Abs a) Source #
Methods occurrences :: Abs a -> OccM OccurrencesBuilder Source #
RaiseNLP a => RaiseNLP (Abs a) Source #
Methods raiseNLPFrom :: Int -> Int -> Abs a -> Abs a Source # raiseNLP :: Int -> Abs a -> Abs a Source #
(Subst Term a, AbsTerm a) => AbsTerm (Abs a) Source #
Methods absTerm :: Term -> Abs a -> Abs a Source #
Free' a c => Free' (Abs a) c Source #
Methods freeVars' :: Abs a -> FreeM c Source #
Suggest (Abs a) (Abs b) Source #
Methods suggest :: Abs a -> Abs b -> String Source #
(Match a b, RaiseNLP a, Subst t2 b) => Match (Abs a) (Abs b) Source #
Methods match :: Relevance -> Telescope -> Telescope -> Abs a -> Abs b -> NLM () Source #
PatternFrom a b => PatternFrom (Abs a) (Abs b) Source #
Methods patternFrom :: Relevance -> Int -> Abs a -> TCM (Abs b) Source #
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source #
Methods reify :: Abs i -> TCM (Name, a) Source # reifyWhen :: Bool -> Abs i -> TCM (Name, a) Source #

data Type' a Source #

Types are terms with a sort annotation.

Constructors

El
Fields _getSort :: Sort unEl :: a

Instances

Functor Type' Source #
Methods fmap :: (a -> b) -> Type' a -> Type' b # (<$) :: a -> Type' b -> Type' a #
Foldable Type' Source #
Methods fold :: Monoid m => Type' m -> m # foldMap :: Monoid m => (a -> m) -> Type' a -> m # foldr :: (a -> b -> b) -> b -> Type' a -> b # foldr' :: (a -> b -> b) -> b -> Type' a -> b # foldl :: (b -> a -> b) -> b -> Type' a -> b # foldl' :: (b -> a -> b) -> b -> Type' a -> b # foldr1 :: (a -> a -> a) -> Type' a -> a # foldl1 :: (a -> a -> a) -> Type' a -> a # toList :: Type' a -> [a] # null :: Type' a -> Bool # length :: Type' a -> Int # elem :: Eq a => a -> Type' a -> Bool # maximum :: Ord a => Type' a -> a # minimum :: Ord a => Type' a -> a # sum :: Num a => Type' a -> a # product :: Num a => Type' a -> a #
Traversable Type' Source #
Methods traverse :: Applicative f => (a -> f b) -> Type' a -> f (Type' b) # sequenceA :: Applicative f => Type' (f a) -> f (Type' a) # mapM :: Monad m => (a -> m b) -> Type' a -> m (Type' b) # sequence :: Monad m => Type' (m a) -> m (Type' a) #
NFData Type Source #
Methods rnf :: Type -> () #
Pretty Type Source #
Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source #
Decoration Type' Source #
Methods traverseF :: Functor m => (a -> m b) -> Type' a -> m (Type' b) Source # distributeF :: Functor m => Type' (m a) -> m (Type' a) Source #
GetDefs Type Source #
Methods getDefs :: MonadGetDefs m => Type -> m () Source #
TermLike Type Source #
Methods traverseTerm :: (Term -> Term) -> Type -> Type Source # traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source # foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #
Free Type Source #
Methods freeVars' :: Type -> FreeT
TeleNoAbs Telescope Source #
Methods teleNoAbs :: Telescope -> Term -> Term Source #
TeleNoAbs ListTel Source #
Methods teleNoAbs :: ListTel -> Term -> Term Source #
AddContext Telescope Source #
Methods addContext :: MonadTCM tcm => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
UnFreezeMeta Type Source #
Methods unfreezeMeta :: Type -> TCM () Source #
DropArgs Telescope Source #	NOTE: This creates telescopes with unbound de Bruijn indices.
Methods dropArgs :: Int -> Telescope -> Telescope Source #
MentionsMeta Type Source #
Methods mentionsMeta :: MetaId -> Type -> Bool Source #
PrettyTCM Telescope Source #
Methods prettyTCM :: Telescope -> TCM Doc Source #
PrettyTCM Type Source #
Methods prettyTCM :: Type -> TCM Doc Source #
Normalise Type Source #
Methods normalise' :: Type -> ReduceM Type Source #
Simplify Type Source #
Methods simplify' :: Type -> ReduceM Type Source #
Reduce Telescope Source #
Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reduce Type Source #
Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Instantiate Telescope Source #
Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Instantiate Type Source #
Methods instantiate' :: Type -> ReduceM Type Source #
SynEq Type Source #	Syntactic equality ignores sorts.
Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
HasPolarity Type Source #
Methods polarities :: Nat -> Type -> TCM [Polarity] Source #
FoldRigid Type Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m Source #
Occurs Type Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
ComputeOccurrences Type Source #
Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
ToTerm Type Source #
Methods toTerm :: TCM (Type -> Term) Source # toTermR :: TCM (Type -> ReduceM Term) Source #
PrimTerm Type Source #
Methods primTerm :: Type -> TCM Term Source #
AbsTerm Type Source #
Methods absTerm :: Term -> Type -> Type Source #
Reify Telescope Telescope Source #
Methods reify :: Telescope -> TCM Telescope Source # reifyWhen :: Bool -> Telescope -> TCM Telescope Source #
Reify Type Expr Source #
Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Match NLPType Type Source #
Methods match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () Source #
PatternFrom Type NLPType Source #
Methods patternFrom :: Relevance -> Int -> Type -> TCM NLPType Source #
Show a => Show (Type' a) Source #
Methods showsPrec :: Int -> Type' a -> ShowS # show :: Type' a -> String # showList :: [Type' a] -> ShowS #
KillRange a => KillRange (Type' a) Source #
Methods killRange :: KillRangeT (Type' a) Source #
SgTel (Dom (ArgName, Type)) Source #
Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source #
Methods sgTel :: Dom Type -> Telescope Source #
LensSort (Type' a) Source #
Methods lensSort :: Lens' Sort (Type' a) Source # getSort :: Type' a -> Sort Source #
NamesIn a => NamesIn (Type' a) Source #
Methods namesIn :: Type' a -> Set QName Source #
AddContext (Dom (String, Type)) Source #
Methods addContext :: MonadTCM tcm => Dom (String, Type) -> tcm a -> tcm a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source #
Methods addContext :: MonadTCM tcm => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source #
Methods addContext :: MonadTCM tcm => Dom Type -> tcm a -> tcm a Source # contextSize :: Dom Type -> Nat Source #
IsSizeType a => IsSizeType (Type' a) Source #
Methods isSizeType :: Type' a -> TCM (Maybe BoundedSize) Source #
PrettyTCM (Type' NLPat) Source #
Methods prettyTCM :: Type' NLPat -> TCM Doc Source #
InstantiateFull a => InstantiateFull (Type' a) Source #
Methods instantiateFull' :: Type' a -> ReduceM (Type' a) Source #
Free' a c => Free' (Type' a) c Source #
Methods freeVars' :: Type' a -> FreeM c Source #
SgTel (ArgName, Dom Type) Source #
Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([WithHiding Name], Dom Type) Source #
Methods addContext :: MonadTCM tcm => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source #
Methods addContext :: MonadTCM tcm => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source #
Methods addContext :: MonadTCM tcm => (String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source #
Methods addContext :: MonadTCM tcm => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
UniverseBi ([Type], [Clause]) Pattern Source #
Methods universeBi :: ([Type], [Clause]) -> [Pattern] #
UniverseBi ([Type], [Clause]) Term Source #
Methods universeBi :: ([Type], [Clause]) -> [Term] #

type Type = Type' Term Source #

class LensSort a where Source #

Minimal complete definition

lensSort

Methods

lensSort :: Lens' Sort a Source #

getSort :: a -> Sort Source #

Instances

LensSort a => LensSort (Dom a) Source #
Methods lensSort :: Lens' Sort (Dom a) Source # getSort :: Dom a -> Sort Source #
LensSort (Type' a) Source #
Methods lensSort :: Lens' Sort (Type' a) Source # getSort :: Type' a -> Sort Source #
LensSort a => LensSort (Abs a) Source #
Methods lensSort :: Lens' Sort (Abs a) Source # getSort :: Abs a -> Sort Source #

data Tele a Source #

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel
ExtendTel a (Abs (Tele a))	`Abs` is never `NoAbs`.

Instances

Functor Tele Source #
Methods fmap :: (a -> b) -> Tele a -> Tele b # (<$) :: a -> Tele b -> Tele a #
Foldable Tele Source #
Methods fold :: Monoid m => Tele m -> m # foldMap :: Monoid m => (a -> m) -> Tele a -> m # foldr :: (a -> b -> b) -> b -> Tele a -> b # foldr' :: (a -> b -> b) -> b -> Tele a -> b # foldl :: (b -> a -> b) -> b -> Tele a -> b # foldl' :: (b -> a -> b) -> b -> Tele a -> b # foldr1 :: (a -> a -> a) -> Tele a -> a # foldl1 :: (a -> a -> a) -> Tele a -> a # toList :: Tele a -> [a] # null :: Tele a -> Bool # length :: Tele a -> Int # elem :: Eq a => a -> Tele a -> Bool # maximum :: Ord a => Tele a -> a # minimum :: Ord a => Tele a -> a # sum :: Num a => Tele a -> a # product :: Num a => Tele a -> a #
Traversable Tele Source #
Methods traverse :: Applicative f => (a -> f b) -> Tele a -> f (Tele b) # sequenceA :: Applicative f => Tele (f a) -> f (Tele a) # mapM :: Monad m => (a -> m b) -> Tele a -> m (Tele b) # sequence :: Monad m => Tele (m a) -> m (Tele a) #
TeleNoAbs Telescope Source #
Methods teleNoAbs :: Telescope -> Term -> Term Source #
AddContext Telescope Source #
Methods addContext :: MonadTCM tcm => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
DropArgs Telescope Source #	NOTE: This creates telescopes with unbound de Bruijn indices.
Methods dropArgs :: Int -> Telescope -> Telescope Source #
PrettyTCM Telescope Source #
Methods prettyTCM :: Telescope -> TCM Doc Source #
Reduce Telescope Source #
Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Instantiate Telescope Source #
Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Reify Telescope Telescope Source #
Methods reify :: Telescope -> TCM Telescope Source # reifyWhen :: Bool -> Telescope -> TCM Telescope Source #
Show a => Show (Tele a) Source #
Methods showsPrec :: Int -> Tele a -> ShowS # show :: Tele a -> String # showList :: [Tele a] -> ShowS #
Pretty a => Pretty (Tele (Dom a)) Source #
Methods pretty :: Tele (Dom a) -> Doc Source # prettyPrec :: Int -> Tele (Dom a) -> Doc Source #
Null (Tele a) Source #
Methods empty :: Tele a Source # null :: Tele a -> Bool Source #
Sized (Tele a) Source #	The size of a telescope is its length (as a list).
Methods size :: Integral n => Tele a -> n Source #
KillRange a => KillRange (Tele a) Source #
Methods killRange :: KillRangeT (Tele a) Source #
Free a => Free (Tele a) Source #
Methods freeVars' :: Tele a -> FreeT
NamesIn a => NamesIn (Tele a) Source #
Methods namesIn :: Tele a -> Set QName Source #
MentionsMeta a => MentionsMeta (Tele a) Source #
Methods mentionsMeta :: MetaId -> Tele a -> Bool Source #
(Subst t a, InstantiateFull a) => InstantiateFull (Tele a) Source #
Methods instantiateFull' :: Tele a -> ReduceM (Tele a) Source #
(Subst t a, Normalise a) => Normalise (Tele a) Source #
Methods normalise' :: Tele a -> ReduceM (Tele a) Source #
(Subst t a, Simplify a) => Simplify (Tele a) Source #
Methods simplify' :: Tele a -> ReduceM (Tele a) Source #
ComputeOccurrences a => ComputeOccurrences (Tele a) Source #
Methods occurrences :: Tele a -> OccM OccurrencesBuilder Source #
Free' a c => Free' (Tele a) c Source #
Methods freeVars' :: Tele a -> FreeM c Source #

type Telescope = Tele (Dom Type) Source #

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #

A traversal for the names in a telescope.

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a Source #

replaceEmptyName :: ArgName -> Tele a -> Tele a Source #

data Sort Source #

Sorts.

Constructors

Type Level	`Set ℓ`.
Prop	Dummy sort.
Inf	`Setω`.
SizeUniv	`SizeUniv`, a sort inhabited by type `Size`.
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

Show Sort Source #
Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
NFData Sort Source #
Methods rnf :: Sort -> () #
Pretty Sort Source #
Methods pretty :: Sort -> Doc Source # prettyPrec :: Int -> Sort -> Doc Source #
KillRange Sort Source #
Methods killRange :: KillRangeT Sort Source #
TermSize Sort Source #
Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
GetDefs Sort Source #
Methods getDefs :: MonadGetDefs m => Sort -> m () Source #
Free Sort Source #
Methods freeVars' :: Sort -> FreeT
NamesIn Sort Source #
Methods namesIn :: Sort -> Set QName Source #
UnFreezeMeta Sort Source #
Methods unfreezeMeta :: Sort -> TCM () Source #
MentionsMeta Sort Source #
Methods mentionsMeta :: MetaId -> Sort -> Bool Source #
PrettyTCM Sort Source #
Methods prettyTCM :: Sort -> TCM Doc Source #
InstantiateFull Sort Source #
Methods instantiateFull' :: Sort -> ReduceM Sort Source #
Normalise Sort Source #
Methods normalise' :: Sort -> ReduceM Sort Source #
Simplify Sort Source #
Methods simplify' :: Sort -> ReduceM Sort Source #
Reduce Sort Source #
Methods reduce' :: Sort -> ReduceM Sort Source # reduceB' :: Sort -> ReduceM (Blocked Sort) Source #
Instantiate Sort Source #
Methods instantiate' :: Sort -> ReduceM Sort Source #
Match Sort Source #
Methods match :: Sort -> Sort -> MaybeT TCM [Term] Source #
SynEq Sort Source #
Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
FoldRigid Sort Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Sort -> TCM m Source #
Occurs Sort Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Sort -> TCM Sort Source # metaOccurs :: MetaId -> Sort -> TCM () Source #
AbsTerm Sort Source #
Methods absTerm :: Term -> Sort -> Sort Source #
Free' Sort c Source #
Methods freeVars' :: Sort -> FreeM c Source #
Reify Sort Expr Source #
Methods reify :: Sort -> TCM Expr Source # reifyWhen :: Bool -> Sort -> TCM Expr Source #
Match NLPat Sort Source #
Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM () Source #
PatternFrom Sort NLPat Source #
Methods patternFrom :: Relevance -> Int -> Sort -> TCM NLPat Source #

newtype Level Source #

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.

Constructors

Max [PlusLevel]

Instances

Show Level Source #
Methods showsPrec :: Int -> Level -> ShowS # show :: Level -> String # showList :: [Level] -> ShowS #
NFData Level Source #
Methods rnf :: Level -> () #
Pretty Level Source #
Methods pretty :: Level -> Doc Source # prettyPrec :: Int -> Level -> Doc Source #
KillRange Level Source #
Methods killRange :: KillRangeT Level Source #
TermSize Level Source #
Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
GetDefs Level Source #
Methods getDefs :: MonadGetDefs m => Level -> m () Source #
TermLike Level Source #
Methods traverseTerm :: (Term -> Term) -> Level -> Level Source # traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level Source # foldTerm :: Monoid m => (Term -> m) -> Level -> m Source #
Free Level Source #
Methods freeVars' :: Level -> FreeT
DeBruijn Level Source #
Methods deBruijnVar :: Int -> Level Source # debruijnNamedVar :: String -> Int -> Level Source # deBruijnView :: Level -> Maybe Int Source #
NamesIn Level Source #
Methods namesIn :: Level -> Set QName Source #
UnFreezeMeta Level Source #
Methods unfreezeMeta :: Level -> TCM () Source #
IsInstantiatedMeta Level Source #
Methods isInstantiatedMeta :: Level -> TCM Bool Source #
MentionsMeta Level Source #
Methods mentionsMeta :: MetaId -> Level -> Bool Source #
PrettyTCM Level Source #
Methods prettyTCM :: Level -> TCM Doc Source #
InstantiateFull Level Source #
Methods instantiateFull' :: Level -> ReduceM Level Source #
Normalise Level Source #
Methods normalise' :: Level -> ReduceM Level Source #
Simplify Level Source #
Methods simplify' :: Level -> ReduceM Level Source #
Reduce Level Source #
Methods reduce' :: Level -> ReduceM Level Source # reduceB' :: Level -> ReduceM (Blocked Level) Source #
Instantiate Level Source #
Methods instantiate' :: Level -> ReduceM Level Source #
Match Level Source #
Methods match :: Level -> Level -> MaybeT TCM [Term] Source #
SynEq Level Source #
Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
HasPolarity Level Source #
Methods polarities :: Nat -> Level -> TCM [Polarity] Source #
FoldRigid Level Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Level -> TCM m Source #
Occurs Level Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Level -> TCM Level Source # metaOccurs :: MetaId -> Level -> TCM () Source #
ComputeOccurrences Level Source #
Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
AbsTerm Level Source #
Methods absTerm :: Term -> Level -> Level Source #
Free' Level c Source #
Methods freeVars' :: Level -> FreeM c Source #
Reify Level Expr Source #
Methods reify :: Level -> TCM Expr Source # reifyWhen :: Bool -> Level -> TCM Expr Source #
Match NLPat Level Source #
Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Level -> NLM () Source #

data PlusLevel Source #

Constructors

ClosedLevel Integer	`n`, to represent `Setₙ`.
Plus Integer LevelAtom	`n + ℓ`.

Instances

Show PlusLevel Source #
Methods showsPrec :: Int -> PlusLevel -> ShowS # show :: PlusLevel -> String # showList :: [PlusLevel] -> ShowS #
NFData PlusLevel Source #
Methods rnf :: PlusLevel -> () #
Pretty PlusLevel Source #
Methods pretty :: PlusLevel -> Doc Source # prettyPrec :: Int -> PlusLevel -> Doc Source #
KillRange PlusLevel Source #
Methods killRange :: KillRangeT PlusLevel Source #
TermSize PlusLevel Source #
Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
GetDefs PlusLevel Source #
Methods getDefs :: MonadGetDefs m => PlusLevel -> m () Source #
TermLike PlusLevel Source #
Methods traverseTerm :: (Term -> Term) -> PlusLevel -> PlusLevel Source # traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel Source # foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m Source #
Free PlusLevel Source #
Methods freeVars' :: PlusLevel -> FreeT
DeBruijn PlusLevel Source #
Methods deBruijnVar :: Int -> PlusLevel Source # debruijnNamedVar :: String -> Int -> PlusLevel Source # deBruijnView :: PlusLevel -> Maybe Int Source #
NamesIn PlusLevel Source #
Methods namesIn :: PlusLevel -> Set QName Source #
UnFreezeMeta PlusLevel Source #
Methods unfreezeMeta :: PlusLevel -> TCM () Source #
IsInstantiatedMeta PlusLevel Source #
Methods isInstantiatedMeta :: PlusLevel -> TCM Bool Source #
MentionsMeta PlusLevel Source #
Methods mentionsMeta :: MetaId -> PlusLevel -> Bool Source #
InstantiateFull PlusLevel Source #
Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #
Normalise PlusLevel Source #
Methods normalise' :: PlusLevel -> ReduceM PlusLevel Source #
Simplify PlusLevel Source #
Methods simplify' :: PlusLevel -> ReduceM PlusLevel Source #
Reduce PlusLevel Source #
Methods reduce' :: PlusLevel -> ReduceM PlusLevel Source # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #
Instantiate PlusLevel Source #
Methods instantiate' :: PlusLevel -> ReduceM PlusLevel Source #
SynEq PlusLevel Source #
Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
HasPolarity PlusLevel Source #
Methods polarities :: Nat -> PlusLevel -> TCM [Polarity] Source #
FoldRigid PlusLevel Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m Source #
Occurs PlusLevel Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> PlusLevel -> TCM PlusLevel Source # metaOccurs :: MetaId -> PlusLevel -> TCM () Source #
ComputeOccurrences PlusLevel Source #
Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #
AbsTerm PlusLevel Source #
Methods absTerm :: Term -> PlusLevel -> PlusLevel Source #
Free' PlusLevel c Source #
Methods freeVars' :: PlusLevel -> FreeM c Source #

data LevelAtom Source #

An atomic term of type Level.

Constructors

MetaLevel MetaId Elims	A meta variable targeting `Level` under some eliminations.
BlockedLevel MetaId Term	A term of type `Level` whose reduction is blocked by a meta.
NeutralLevel NotBlocked Term	A neutral term of type `Level`.
UnreducedLevel Term	Introduced by `instantiate`, removed by `reduce`.

Instances

Show LevelAtom Source #
Methods showsPrec :: Int -> LevelAtom -> ShowS # show :: LevelAtom -> String # showList :: [LevelAtom] -> ShowS #
NFData LevelAtom Source #
Methods rnf :: LevelAtom -> () #
Pretty LevelAtom Source #
Methods pretty :: LevelAtom -> Doc Source # prettyPrec :: Int -> LevelAtom -> Doc Source #
KillRange LevelAtom Source #
Methods killRange :: KillRangeT LevelAtom Source #
TermSize LevelAtom Source #
Methods termSize :: LevelAtom -> Int Source # tsize :: LevelAtom -> Sum Int Source #
GetDefs LevelAtom Source #
Methods getDefs :: MonadGetDefs m => LevelAtom -> m () Source #
TermLike LevelAtom Source #
Methods traverseTerm :: (Term -> Term) -> LevelAtom -> LevelAtom Source # traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom Source # foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m Source #
Free LevelAtom Source #
Methods freeVars' :: LevelAtom -> FreeT
DeBruijn LevelAtom Source #
Methods deBruijnVar :: Int -> LevelAtom Source # debruijnNamedVar :: String -> Int -> LevelAtom Source # deBruijnView :: LevelAtom -> Maybe Int Source #
NamesIn LevelAtom Source #
Methods namesIn :: LevelAtom -> Set QName Source #
UnFreezeMeta LevelAtom Source #
Methods unfreezeMeta :: LevelAtom -> TCM () Source #
IsInstantiatedMeta LevelAtom Source #
Methods isInstantiatedMeta :: LevelAtom -> TCM Bool Source #
MentionsMeta LevelAtom Source #
Methods mentionsMeta :: MetaId -> LevelAtom -> Bool Source #
InstantiateFull LevelAtom Source #
Methods instantiateFull' :: LevelAtom -> ReduceM LevelAtom Source #
Normalise LevelAtom Source #
Methods normalise' :: LevelAtom -> ReduceM LevelAtom Source #
Simplify LevelAtom Source #
Methods simplify' :: LevelAtom -> ReduceM LevelAtom Source #
Reduce LevelAtom Source #
Methods reduce' :: LevelAtom -> ReduceM LevelAtom Source # reduceB' :: LevelAtom -> ReduceM (Blocked LevelAtom) Source #
Instantiate LevelAtom Source #
Methods instantiate' :: LevelAtom -> ReduceM LevelAtom Source #
SynEq LevelAtom Source #
Methods synEq :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom) synEq' :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)
HasPolarity LevelAtom Source #
Methods polarities :: Nat -> LevelAtom -> TCM [Polarity] Source #
FoldRigid LevelAtom Source #
Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m Source #
Occurs LevelAtom Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> LevelAtom -> TCM LevelAtom Source # metaOccurs :: MetaId -> LevelAtom -> TCM () Source #
ComputeOccurrences LevelAtom Source #
Methods occurrences :: LevelAtom -> OccM OccurrencesBuilder Source #
AbsTerm LevelAtom Source #
Methods absTerm :: Term -> LevelAtom -> LevelAtom Source #
Free' LevelAtom c Source #
Methods freeVars' :: LevelAtom -> FreeM c Source #

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 `Elim` is neutral and blocks a pattern match.
Underapplied	Not enough arguments were supplied to complete the matching.
AbsurdMatch	We matched an absurd clause, results in a neutral `Def`.
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 `Def`.

Instances

Show NotBlocked Source #
Methods showsPrec :: Int -> NotBlocked -> ShowS # show :: NotBlocked -> String # showList :: [NotBlocked] -> ShowS #
Semigroup NotBlocked Source #	`ReallyNotBlocked` is the unit. `MissingClauses` is dominant. `StuckOn{}` should be propagated, if tied, we take the left.
Methods (<>) :: NotBlocked -> NotBlocked -> NotBlocked # sconcat :: NonEmpty NotBlocked -> NotBlocked # stimes :: Integral b => b -> NotBlocked -> NotBlocked #
Monoid NotBlocked Source #
Methods mempty :: NotBlocked # mappend :: NotBlocked -> NotBlocked -> NotBlocked # mconcat :: [NotBlocked] -> NotBlocked #

data Blocked t Source #

Something where a meta variable may block reduction.

Constructors

Blocked
Fields theBlockingMeta :: MetaId ignoreBlocking :: t
NotBlocked
Fields blockingStatus :: NotBlocked ignoreBlocking :: t

Instances

Functor Blocked Source #
Methods fmap :: (a -> b) -> Blocked a -> Blocked b # (<$) :: a -> Blocked b -> Blocked a #
Applicative Blocked Source #	Blocking by a meta is dominant.
Methods pure :: a -> Blocked a # (<>) :: Blocked (a -> b) -> Blocked a -> Blocked b # (>) :: Blocked a -> Blocked b -> Blocked b # (<*) :: Blocked a -> Blocked b -> Blocked a #
Foldable Blocked Source #
Methods fold :: Monoid m => Blocked m -> m # foldMap :: Monoid m => (a -> m) -> Blocked a -> m # foldr :: (a -> b -> b) -> b -> Blocked a -> b # foldr' :: (a -> b -> b) -> b -> Blocked a -> b # foldl :: (b -> a -> b) -> b -> Blocked a -> b # foldl' :: (b -> a -> b) -> b -> Blocked a -> b # foldr1 :: (a -> a -> a) -> Blocked a -> a # foldl1 :: (a -> a -> a) -> Blocked a -> a # toList :: Blocked a -> [a] # null :: Blocked a -> Bool # length :: Blocked a -> Int # elem :: Eq a => a -> Blocked a -> Bool # maximum :: Ord a => Blocked a -> a # minimum :: Ord a => Blocked a -> a # sum :: Num a => Blocked a -> a # product :: Num a => Blocked a -> a #
Traversable Blocked Source #
Methods traverse :: Applicative f => (a -> f b) -> Blocked a -> f (Blocked b) # sequenceA :: Applicative f => Blocked (f a) -> f (Blocked a) # mapM :: Monad m => (a -> m b) -> Blocked a -> m (Blocked b) # sequence :: Monad m => Blocked (m a) -> m (Blocked a) #
Semigroup Blocked_ Source #
Methods (<>) :: Blocked_ -> Blocked_ -> Blocked_ # sconcat :: NonEmpty Blocked_ -> Blocked_ # stimes :: Integral b => b -> Blocked_ -> Blocked_ #
Monoid Blocked_ Source #
Methods mempty :: Blocked_ # mappend :: Blocked_ -> Blocked_ -> Blocked_ # mconcat :: [Blocked_] -> Blocked_ #
HasOptions NLM Source #
Methods pragmaOptions :: NLM PragmaOptions Source # commandLineOptions :: NLM CommandLineOptions Source #
Show t => Show (Blocked t) Source #
Methods showsPrec :: Int -> Blocked t -> ShowS # show :: Blocked t -> String # showList :: [Blocked t] -> ShowS #
KillRange a => KillRange (Blocked a) Source #
Methods killRange :: KillRangeT (Blocked a) Source #
TermLike a => TermLike (Blocked a) Source #
Methods traverseTerm :: (Term -> Term) -> Blocked a -> Blocked a Source # traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a) Source # foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m Source #
PrettyTCM a => PrettyTCM (Blocked a) Source #
Methods prettyTCM :: Blocked a -> TCM Doc Source #
Instantiate a => Instantiate (Blocked a) Source #
Methods instantiate' :: Blocked a -> ReduceM (Blocked a) Source #

type Blocked_ = Blocked () Source #

Blocked t without the t.

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 e0 is also propagated, since it provides more precise information as StuckOn 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 does not seem useful.

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

data Clause Source #

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

clauseRange :: Range
clauseTel :: Telescope
Δ: The types of the pattern variables in dependency order.
namedClausePats :: [NamedArg DeBruijnPattern]
Δ ⊢ ps. The de Bruijn indices refer to Δ.
clauseBody :: Maybe Term
Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.
clauseType :: Maybe (Arg Type)
Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. Can be Irrelevant if we encountered an irrelevant projection pattern on the lhs.
clauseCatchall :: Bool
Clause has been labelled as CATCHALL.

Instances

Show Clause Source #
Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
Pretty Clause Source #
Methods pretty :: Clause -> Doc Source # prettyPrec :: Int -> Clause -> Doc Source #
Null Clause Source #	A `null` clause is one with no patterns and no rhs. Should not exist in practice.
Methods empty :: Clause Source # null :: Clause -> Bool Source #
KillRange Clause Source #
Methods killRange :: KillRangeT Clause Source #
HasRange Clause Source #
Methods getRange :: Clause -> Range Source #
GetDefs Clause Source #
Methods getDefs :: MonadGetDefs m => Clause -> m () Source #
FunArity Clause Source #	Get the number of initial `Apply` patterns in a clause.
Methods funArity :: Clause -> Int Source #
Free Clause Source #
Methods freeVars' :: Clause -> FreeT
NamesIn Clause Source #
Methods namesIn :: Clause -> Set QName Source #
DropArgs Clause Source #	NOTE: does not work for recursive functions.
Methods dropArgs :: Int -> Clause -> Clause Source #
DropArgs FunctionInverse Source #
Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source #
PrettyTCM Clause Source #
Methods prettyTCM :: Clause -> TCM Doc Source #
InstantiateFull Clause Source #
Methods instantiateFull' :: Clause -> ReduceM Clause Source #
InstantiateFull FunctionInverse Source #
Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source #
NormaliseProjP Clause Source #
Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause Source #
Occurs Clause Source #
Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Clause -> TCM Clause Source # metaOccurs :: MetaId -> Clause -> TCM () Source #
ComputeOccurrences Clause Source #
Methods occurrences :: Clause -> OccM OccurrencesBuilder Source #
Free' Clause c Source #
Methods freeVars' :: Clause -> FreeM c Source #
FunArity [Clause] Source #	Get the number of common initial `Apply` patterns in a list of clauses.
Methods funArity :: [Clause] -> Int Source #
PrettyTCM (QNamed Clause) Source #
Methods prettyTCM :: QNamed Clause -> TCM Doc Source #
Reify (QNamed Clause) Clause Source #
Methods reify :: QNamed Clause -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause -> TCM Clause Source #
UniverseBi ([Type], [Clause]) Pattern Source #
Methods universeBi :: ([Type], [Clause]) -> [Pattern] #
UniverseBi ([Type], [Clause]) Term Source #
Methods universeBi :: ([Type], [Clause]) -> [Term] #

clausePats :: Clause -> [Arg DeBruijnPattern] Source #

type PatVarName = ArgName Source #

Pattern variables.

patVarNameToString :: PatVarName -> String Source #

nameToPatVarName :: Name -> PatVarName Source #

data Pattern' x 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)]	`c ps` The subpatterns do not contain any projection copatterns.
LitP Literal	E.g. `5`, `"hello"`.
ProjP ProjOrigin QName	Projection copattern. Can only appear by itself.

Instances

Functor Pattern' Source #
Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b # (<$) :: a -> Pattern' b -> Pattern' a #
Foldable Pattern' Source #
Methods fold :: Monoid m => Pattern' m -> m # foldMap :: Monoid m => (a -> m) -> Pattern' a -> m # foldr :: (a -> b -> b) -> b -> Pattern' a -> b # foldr' :: (a -> b -> b) -> b -> Pattern' a -> b # foldl :: (b -> a -> b) -> b -> Pattern' a -> b # foldl' :: (b -> a -> b) -> b -> Pattern' a -> b # foldr1 :: (a -> a -> a) -> Pattern' a -> a # foldl1 :: (a -> a -> a) -> Pattern' a -> a # toList :: Pattern' a -> [a] # null :: Pattern' a -> Bool # length :: Pattern' a -> Int # elem :: Eq a => a -> Pattern' a -> Bool # maximum :: Ord a => Pattern' a -> a # minimum :: Ord a => Pattern' a -> a # sum :: Num a => Pattern' a -> a # product :: Num a => Pattern' a -> a #
Traversable Pattern' Source #
Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) #
MapNamedArg Pattern' Source #
Methods mapNamedArg :: (NamedArg a -> NamedArg b) -> NamedArg (Pattern' a) -> NamedArg (Pattern' b) Source #
UniverseBi Elims Pattern Source #
Methods universeBi :: Elims -> [Pattern] #
UniverseBi Args Pattern Source #
Methods universeBi :: Args -> [Pattern] #
LabelPatVars Pattern DeBruijnPattern Int Source #
Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern Source # unlabelPatVars :: DeBruijnPattern -> Pattern Source #
Show x => Show (Pattern' x) Source #
Methods showsPrec :: Int -> Pattern' x -> ShowS # show :: Pattern' x -> String # showList :: [Pattern' x] -> ShowS #
Pretty a => Pretty (Pattern' a) Source #
Methods pretty :: Pattern' a -> Doc Source # prettyPrec :: Int -> Pattern' a -> Doc Source #
KillRange a => KillRange (Pattern' a) Source #
Methods killRange :: KillRangeT (Pattern' a) Source #
IsProjP (Pattern' a) Source #
Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #
NamesIn (Pattern' a) Source #
Methods namesIn :: Pattern' a -> Set QName Source #
PrettyTCM a => PrettyTCM (Pattern' a) Source #
Methods prettyTCM :: Pattern' a -> TCM Doc Source #
InstantiateFull a => InstantiateFull (Pattern' a) Source #
Methods instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) Source #
Normalise a => Normalise (Pattern' a) Source #
Methods normalise' :: Pattern' a -> ReduceM (Pattern' a) Source #
NormaliseProjP (Pattern' x) Source #
Methods normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source #
IsFlexiblePattern (Pattern' a) Source #
Methods maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern' a -> TCM Bool Source #
UniverseBi ([Type], [Clause]) Pattern Source #
Methods universeBi :: ([Type], [Clause]) -> [Pattern] #

type Pattern Source #

Arguments

= Pattern' PatVarName

The PatVarName is a name suggestion.

varP :: ArgName -> Pattern Source #

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar
Fields dbPatVarName :: PatVarName dbPatVarIndex :: Int

Instances

Show DBPatVar Source #
Methods showsPrec :: Int -> DBPatVar -> ShowS # show :: DBPatVar -> String # showList :: [DBPatVar] -> ShowS #
Pretty DBPatVar Source #
Methods pretty :: DBPatVar -> Doc Source # prettyPrec :: Int -> DBPatVar -> Doc Source #
KillRange DBPatVar Source #
Methods killRange :: KillRangeT DBPatVar Source #
PrettyTCM DBPatVar Source #
Methods prettyTCM :: DBPatVar -> TCM Doc Source #
InstantiateFull DBPatVar Source #
Methods instantiateFull' :: DBPatVar -> ReduceM DBPatVar Source #
Normalise DBPatVar Source #
Methods normalise' :: DBPatVar -> ReduceM DBPatVar Source #
LabelPatVars Pattern DeBruijnPattern Int Source #
Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern Source # unlabelPatVars :: DeBruijnPattern -> Pattern Source #

type DeBruijnPattern = Pattern' DBPatVar Source #

namedVarP :: PatVarName -> Named_ Pattern Source #

namedDBVarP :: Int -> PatVarName -> Named_ 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 conPRecord :: Maybe ConOrigin `Nothing` if data constructor. `Just` if record constructor. conPType :: Maybe (Arg Type) The type of the whole constructor pattern. Should be present (`Just`) if constructor pattern is is generated ordinarily by type-checking. Could be absent (`Nothing`) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.

Instances

Show ConPatternInfo Source #
Methods showsPrec :: Int -> ConPatternInfo -> ShowS # show :: ConPatternInfo -> String # showList :: [ConPatternInfo] -> ShowS #
KillRange ConPatternInfo Source #
Methods killRange :: KillRangeT ConPatternInfo Source #
InstantiateFull ConPatternInfo Source #
Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source #
Normalise ConPatternInfo Source #
Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source #

noConPatternInfo :: ConPatternInfo Source #

toConPatternInfo :: ConInfo -> ConPatternInfo Source #

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo Source #

Build ConInfo from ConPatternInfo.

patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] Source #

Extract pattern variables in left-to-right order. A DotP is also treated as variable (see docu for Clause).

properlyMatching :: DeBruijnPattern -> Bool Source #

Does the pattern perform a match that could fail?

Explicit substitutions

data Substitution' a Source #

Substitutions.

Constructors

IdS	Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS	Empty substitution, lifts from the empty context. Apply this to closed terms you want to use in a non-empty context. `Γ ⊢ EmptyS : ()`
a :# (Substitution' a) infixr 4	Substitution extension, ``cons'`. `Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A`
Strengthen Empty (Substitution' a)	Strengthening substitution. First argument is `IMPOSSIBLE`. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. `Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A`
Wk !Int (Substitution' a)	Weakning substitution, lifts to an extended context. `Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk \|Ψ\| ρ : Δ`
Lift !Int (Substitution' a)	Lifting substitution. Use this to go under a binder. `Lift 1 ρ == var 0 :# Wk 1 ρ`. `Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift \|Ψ\| ρ : Δ, Ψ`

Instances

Functor Substitution' Source #
Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b # (<$) :: a -> Substitution' b -> Substitution' a #
Foldable Substitution' Source #
Methods fold :: Monoid m => Substitution' m -> m # foldMap :: Monoid m => (a -> m) -> Substitution' a -> m # foldr :: (a -> b -> b) -> b -> Substitution' a -> b # foldr' :: (a -> b -> b) -> b -> Substitution' a -> b # foldl :: (b -> a -> b) -> b -> Substitution' a -> b # foldl' :: (b -> a -> b) -> b -> Substitution' a -> b # foldr1 :: (a -> a -> a) -> Substitution' a -> a # foldl1 :: (a -> a -> a) -> Substitution' a -> a # toList :: Substitution' a -> [a] # null :: Substitution' a -> Bool # length :: Substitution' a -> Int # elem :: Eq a => a -> Substitution' a -> Bool # maximum :: Ord a => Substitution' a -> a # minimum :: Ord a => Substitution' a -> a # sum :: Num a => Substitution' a -> a # product :: Num a => Substitution' a -> a #
Traversable Substitution' Source #
Methods traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) # sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) # mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) # sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) #
KillRange Substitution Source #
Methods killRange :: KillRangeT Substitution Source #
InstantiateFull Substitution Source #
Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
Show a => Show (Substitution' a) Source #
Methods showsPrec :: Int -> Substitution' a -> ShowS # show :: Substitution' a -> String # showList :: [Substitution' a] -> ShowS #
Pretty a => Pretty (Substitution' a) Source #
Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source #
Null (Substitution' a) Source #
Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
TermSize a => TermSize (Substitution' a) Source #
Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source #
Methods prettyTCM :: Substitution' a -> TCM Doc Source #

type Substitution = Substitution' Term Source #

type PatternSubstitution = Substitution' DeBruijnPattern Source #

Views

data EqualityView Source #

View type as equality type.

Constructors

EqualityType
Fields eqtSort :: Sort Sort of this type. eqtName :: QName Builtin EQUALITY. eqtLevel :: Arg Term Hidden eqtType :: Arg Term Hidden eqtLhs :: Arg Term NotHidden eqtRhs :: Arg Term NotHidden
OtherType Type	reduced

Instances

TermLike EqualityView Source #
Methods traverseTerm :: (Term -> Term) -> EqualityView -> EqualityView Source # traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView Source # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m Source #
PrettyTCM EqualityView Source #
Methods prettyTCM :: EqualityView -> TCM Doc Source #
InstantiateFull EqualityView Source #
Methods instantiateFull' :: EqualityView -> ReduceM EqualityView Source #
Normalise EqualityView Source #
Methods normalise' :: EqualityView -> ReduceM EqualityView Source #
Simplify EqualityView Source #
Methods simplify' :: EqualityView -> ReduceM EqualityView Source #
Reduce EqualityView Source #
Methods reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source #
Instantiate EqualityView Source #
Methods instantiate' :: EqualityView -> ReduceM EqualityView Source #
Free' EqualityView c Source #
Methods freeVars' :: EqualityView -> FreeM c Source #

isEqualityType :: EqualityView -> Bool Source #

Absurd Lambda

absurdBody :: Abs Term Source #

Absurd lambdas are internally represented as identity with variable name "()".

isAbsurdBody :: Abs Term -> Bool Source #

absurdPatternName :: PatVarName Source #

isAbsurdPatternName :: PatVarName -> Bool Source #

Pointers and Sharing

ignoreSharing :: Term -> Term Source #

Remove top-level Shared data constructors.

ignoreSharingType :: Type -> Type Source #

shared_ :: Term -> Term Source #

Introduce sharing.

updateSharedFM :: (Monad m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term) Source #

Typically m would be TCM and f would be Blocked.

updateSharedM :: Monad m => (Term -> m Term) -> Term -> m Term Source #

updateShared :: (Term -> Term) -> Term -> Term Source #

pointerChain :: Term -> [Ptr Term] Source #

compressPointerChain :: Term -> Term Source #

Smart constructors

var :: Nat -> Term Source #

An unapplied variable.

dontCare :: Term -> Term Source #

Add DontCare is it is not already a DontCare.

typeDontCare :: Type Source #

A dummy type.

topSort :: Type Source #

Top sort (Setomega).

sort :: Sort -> Type Source #

varSort :: Int -> Sort Source #

sSuc :: Sort -> Sort Source #

Get the next higher sort.

levelSuc :: Level -> Level Source #

mkType :: Integer -> Sort Source #

impossibleTerm :: String -> Int -> Term Source #

class SgTel a where Source #

Constructing a singleton telescope.

Minimal complete definition

sgTel

Methods

sgTel :: a -> Telescope Source #

Instances

SgTel (Dom (ArgName, Type)) Source #
Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source #
Methods sgTel :: Dom Type -> Telescope Source #
SgTel (ArgName, Dom Type) Source #
Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #

hackReifyToMeta :: Term Source #

isHackReifyToMeta :: Term -> Bool Source #

Handling blocked terms.

blockingMeta :: Blocked t -> Maybe MetaId Source #

blocked :: MetaId -> a -> Blocked a Source #

notBlocked :: a -> Blocked a Source #

Simple operations on terms and types.

stripDontCare :: Term -> Term Source #

Removing a topmost DontCare constructor.

arity :: Type -> Nat Source #

Doesn't do any reduction.

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

suggest

Methods

suggest :: a -> b -> String Source #

Instances

Suggest String String Source #
Methods suggest :: String -> String -> String Source #
Suggest String (Abs b) Source #
Methods suggest :: String -> Abs b -> String Source #
Suggest Name (Abs b) Source #
Methods suggest :: Name -> Abs b -> String Source #
Suggest (Abs a) (Abs b) Source #
Methods suggest :: Abs a -> Abs b -> String Source #

Eliminations.

unSpine :: Term -> Term Source #

Convert top-level postfix projections into prefix projections.

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.

argFromElim :: Elim' a -> Arg a Source #

Drop Apply constructor. (Unsafe!)

isApplyElim :: Elim' a -> Maybe (Arg a) Source #

Drop Apply constructor. (Safe)

allApplyElims :: [Elim' a] -> Maybe [Arg a] Source #

Drop Apply constructors. (Safe)

splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a]) Source #

Split at first non-Apply

class IsProjElim e where Source #

Minimal complete definition

isProjElim

Methods

isProjElim :: e -> Maybe (ProjOrigin, QName) Source #

Instances

IsProjElim Elim Source #
Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source #
IsProjElim e => IsProjElim (MaybeReduced e) Source #
Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) Source #

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)

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

tsize

Methods

termSize :: a -> Int Source #

tsize :: a -> Sum Int Source #

Instances

TermSize LevelAtom Source #
Methods termSize :: LevelAtom -> Int Source # tsize :: LevelAtom -> Sum Int Source #
TermSize PlusLevel Source #
Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
TermSize Level Source #
Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
TermSize Sort Source #
Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
TermSize Term Source #
Methods termSize :: Term -> Int Source # tsize :: Term -> Sum Int Source #
(Foldable t, TermSize a) => TermSize (t a) Source #
Methods termSize :: t a -> Int Source # tsize :: t a -> Sum Int Source #
TermSize a => TermSize (Substitution' a) Source #
Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #

KillRange instances.

UniverseBi instances.

Simple pretty printing

pDom :: LensHiding a => a -> Doc -> Doc Source #

NFData instances

module Agda.Syntax.Abstract.Name

module Agda.Utils.Pointer

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId
Fields metaId :: Nat

Instances

Enum MetaId Source #
Methods succ :: MetaId -> MetaId # pred :: MetaId -> MetaId # toEnum :: Int -> MetaId # fromEnum :: MetaId -> Int # enumFrom :: MetaId -> [MetaId] # enumFromThen :: MetaId -> MetaId -> [MetaId] # enumFromTo :: MetaId -> MetaId -> [MetaId] # enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] #
Eq MetaId Source #
Methods (==) :: MetaId -> MetaId -> Bool # (/=) :: MetaId -> MetaId -> Bool #
Integral MetaId Source #
Methods quot :: MetaId -> MetaId -> MetaId # rem :: MetaId -> MetaId -> MetaId # div :: MetaId -> MetaId -> MetaId # mod :: MetaId -> MetaId -> MetaId # quotRem :: MetaId -> MetaId -> (MetaId, MetaId) # divMod :: MetaId -> MetaId -> (MetaId, MetaId) # toInteger :: MetaId -> Integer #
Num MetaId Source #
Methods (+) :: MetaId -> MetaId -> MetaId # (-) :: MetaId -> MetaId -> MetaId # (*) :: MetaId -> MetaId -> MetaId # negate :: MetaId -> MetaId # abs :: MetaId -> MetaId # signum :: MetaId -> MetaId # fromInteger :: Integer -> MetaId #
Ord MetaId Source #
Methods compare :: MetaId -> MetaId -> Ordering # (<) :: MetaId -> MetaId -> Bool # (<=) :: MetaId -> MetaId -> Bool # (>) :: MetaId -> MetaId -> Bool # (>=) :: MetaId -> MetaId -> Bool # max :: MetaId -> MetaId -> MetaId # min :: MetaId -> MetaId -> MetaId #
Real MetaId Source #
Methods toRational :: MetaId -> Rational #
Show MetaId Source #	Show non-record version of this newtype.
Methods showsPrec :: Int -> MetaId -> ShowS # show :: MetaId -> String # showList :: [MetaId] -> ShowS #
NFData MetaId Source #
Methods rnf :: MetaId -> () #
Pretty MetaId Source #
Methods pretty :: MetaId -> Doc Source # prettyPrec :: Int -> MetaId -> Doc Source #
GetDefs MetaId Source #
Methods getDefs :: MonadGetDefs m => MetaId -> m () Source #
HasFresh MetaId Source #
Methods freshLens :: Lens' MetaId TCState Source # nextFresh' :: MetaId -> MetaId Source #
UnFreezeMeta MetaId Source #
Methods unfreezeMeta :: MetaId -> TCM () Source #
IsInstantiatedMeta MetaId Source #
Methods isInstantiatedMeta :: MetaId -> TCM Bool Source #
PrettyTCM MetaId Source #
Methods prettyTCM :: MetaId -> TCM Doc Source #
FromTerm MetaId Source #
Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
ToTerm MetaId Source #
Methods toTerm :: TCM (MetaId -> Term) Source # toTermR :: TCM (MetaId -> ReduceM Term) Source #
PrimTerm MetaId Source #
Methods primTerm :: MetaId -> TCM Term Source #
Unquote MetaId Source #
Methods unquote :: Term -> UnquoteM MetaId Source #
Reify MetaId Expr Source #
Methods reify :: MetaId -> TCM Expr Source # reifyWhen :: Bool -> MetaId -> TCM Expr Source #