Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal

Contents

Synopsis

Documentation

type Args = [Arg Term] Source #

Type of argument lists.

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.

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 #

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 # 
Pretty Elim Source # 
Pretty Term Source # 
KillRange Substitution Source # 
KillRange Term Source # 
TermSize Term Source # 
IsProjElim Elim 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 Terms for variables.

NamesIn Term Source # 

Methods

namesIn :: Term -> Set QName Source #

TeleNoAbs Telescope 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 # 
IsSizeType Term Source # 
DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

MentionsMeta Type Source # 
MentionsMeta Elim Source # 
MentionsMeta Term Source # 
PrettyTCM Telescope 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 # 
InstantiateFull Term Source # 
Normalise Type Source # 
Normalise Elim Source # 
Normalise Term Source # 
Simplify Type Source # 
Simplify Elim Source # 
Simplify Term Source # 
Reduce Telescope Source # 
Reduce Type Source # 
Reduce Elim Source # 
Reduce Term Source # 
Instantiate Telescope Source # 
Instantiate Type Source # 
Instantiate Elim Source # 
Instantiate 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 # 
Evaluate 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 # 
Occurs Term Source # 
ComputeOccurrences Type Source # 
ComputeOccurrences Term Source # 
ToTerm Type Source # 
ToTerm Term Source # 
PrimTerm Type Source # 

Methods

primTerm :: Type -> TCM Term Source #

NoProjectedVar Term Source # 
AbsTerm Type Source # 

Methods

absTerm :: Term -> Type -> Type Source #

AbsTerm Term Source # 

Methods

absTerm :: Term -> Term -> Term Source #

IsPrefixOf Elims Source # 
IsPrefixOf Term Source # 
IsPrefixOf Args Source # 
ForcedVariables Term Source #

Assumes that the term is in normal form.

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 # 
Subst Term DotPatternInst Source # 
Subst Term ProblemRest Source # 
Subst Term SizeConstraint Source # 
Subst Term SizeMeta Source # 
Reify Telescope Telescope Source # 
Reify Type Expr Source # 
Reify Term 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 # 
PatternFrom Term NLPat Source # 
Subst Term (Problem' p) Source # 
Subst Term (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

SgTel (Dom (ArgName, Type)) Source # 
SgTel (Dom Type) 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 # 
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] #

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 # 
IsProjElim Elim Source # 
MentionsMeta Elim Source # 
PrettyTCM Elim Source # 

Methods

prettyTCM :: Elim -> TCM Doc Source #

Normalise Elim Source # 
Simplify Elim Source # 
Reduce Elim Source # 
Instantiate Elim Source # 
IsPrefixOf 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 # 
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 # 
PrettyTCM (Elim' DisplayTerm) Source # 
InstantiateFull a => InstantiateFull (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 # 
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 # 
ComputeOccurrences a => ComputeOccurrences (Elim' a) 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 # 

type Elims Source #

Arguments

 = [Elim]

eliminations ordered left-to-right.

type ArgName = String Source #

Names in binders and arguments.

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

NoAbs 

Fields

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 # 
LensSort a => LensSort (Abs a) 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.

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 # 
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

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 # 
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 # 
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.

MentionsMeta Type Source # 
PrettyTCM Telescope Source # 
PrettyTCM Type Source # 

Methods

prettyTCM :: Type -> TCM Doc Source #

Normalise Type Source # 
Simplify Type Source # 
Reduce Telescope Source # 
Reduce Type Source # 
Instantiate Telescope Source # 
Instantiate 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 # 
ComputeOccurrences Type Source # 
ToTerm Type Source # 
PrimTerm Type Source # 

Methods

primTerm :: Type -> TCM Term Source #

AbsTerm Type Source # 

Methods

absTerm :: Term -> Type -> Type Source #

Reify Telescope Telescope Source # 
Reify Type Expr Source # 
Match NLPType Type Source # 

Methods

match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () Source #

PatternFrom Type 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 # 
SgTel (Dom (ArgName, Type)) Source # 
SgTel (Dom Type) Source # 
LensSort (Type' a) 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 # 
PrettyTCM (Type' NLPat) Source # 
InstantiateFull a => InstantiateFull (Type' a) Source # 
Free' a c => Free' (Type' a) c Source # 

Methods

freeVars' :: Type' a -> FreeM c Source #

SgTel (ArgName, Dom Type) 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] #

class LensSort a where Source #

Minimal complete definition

lensSort

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 # 
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.

PrettyTCM Telescope Source # 
Reduce Telescope Source # 
Instantiate Telescope Source # 
Reify Telescope 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 # 
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 # 
(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 # 
Free' a c => Free' (Tele a) c Source # 

Methods

freeVars' :: Tele a -> FreeM c Source #

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

A traversal for the names in a telescope.

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 # 
KillRange Sort Source # 
TermSize Sort 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 # 
PrettyTCM Sort Source # 

Methods

prettyTCM :: Sort -> TCM Doc Source #

InstantiateFull Sort Source # 
Normalise Sort Source # 
Simplify Sort Source # 
Reduce Sort Source # 
Instantiate 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 # 
AbsTerm Sort Source # 

Methods

absTerm :: Term -> Sort -> Sort Source #

Free' Sort c Source # 

Methods

freeVars' :: Sort -> FreeM c Source #

Reify Sort Expr Source # 
Match NLPat Sort Source # 

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM () Source #

PatternFrom Sort 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 # 
KillRange Level Source # 
TermSize Level 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 # 
NamesIn Level Source # 

Methods

namesIn :: Level -> Set QName Source #

UnFreezeMeta Level Source # 

Methods

unfreezeMeta :: Level -> TCM () Source #

IsInstantiatedMeta Level Source # 
MentionsMeta Level Source # 
PrettyTCM Level Source # 

Methods

prettyTCM :: Level -> TCM Doc Source #

InstantiateFull Level Source # 
Normalise Level Source # 
Simplify Level Source # 
Reduce Level Source # 
Instantiate 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 # 
ComputeOccurrences Level Source # 
AbsTerm Level Source # 

Methods

absTerm :: Term -> Level -> Level Source #

Free' Level c Source # 

Methods

freeVars' :: Level -> FreeM c Source #

Reify Level 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 # 
NFData PlusLevel Source # 

Methods

rnf :: PlusLevel -> () #

Pretty PlusLevel Source # 
KillRange PlusLevel Source # 
TermSize PlusLevel Source # 
GetDefs PlusLevel Source # 

Methods

getDefs :: MonadGetDefs m => PlusLevel -> m () Source #

TermLike PlusLevel Source # 
Free PlusLevel Source # 

Methods

freeVars' :: PlusLevel -> FreeT

DeBruijn PlusLevel Source # 
NamesIn PlusLevel Source # 
UnFreezeMeta PlusLevel Source # 
IsInstantiatedMeta PlusLevel Source # 
MentionsMeta PlusLevel Source # 
InstantiateFull PlusLevel Source # 
Normalise PlusLevel Source # 
Simplify PlusLevel Source # 
Reduce PlusLevel Source # 
Instantiate PlusLevel Source # 
SynEq PlusLevel Source # 
HasPolarity PlusLevel Source # 
FoldRigid PlusLevel Source # 

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m Source #

Occurs PlusLevel Source # 
ComputeOccurrences PlusLevel Source # 
AbsTerm PlusLevel Source # 
Free' PlusLevel 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 # 
NFData LevelAtom Source # 

Methods

rnf :: LevelAtom -> () #

Pretty LevelAtom Source # 
KillRange LevelAtom Source # 
TermSize LevelAtom Source # 
GetDefs LevelAtom Source # 

Methods

getDefs :: MonadGetDefs m => LevelAtom -> m () Source #

TermLike LevelAtom Source # 
Free LevelAtom Source # 

Methods

freeVars' :: LevelAtom -> FreeT

DeBruijn LevelAtom Source # 
NamesIn LevelAtom Source # 
UnFreezeMeta LevelAtom Source # 
IsInstantiatedMeta LevelAtom Source # 
MentionsMeta LevelAtom Source # 
InstantiateFull LevelAtom Source # 
Normalise LevelAtom Source # 
Simplify LevelAtom Source # 
Reduce LevelAtom Source # 
Instantiate LevelAtom Source # 
SynEq LevelAtom Source # 
HasPolarity LevelAtom Source # 
FoldRigid LevelAtom Source # 

Methods

foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m Source #

Occurs LevelAtom Source # 
ComputeOccurrences LevelAtom Source # 
AbsTerm LevelAtom Source # 
Free' LevelAtom 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.

data Blocked t Source #

Something where a meta variable may block reduction.

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 # 
Monoid Blocked_ Source # 
HasOptions NLM 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 # 
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 # 

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

Instances

Show Clause Source # 
Pretty Clause Source # 
Null Clause Source #

A null clause is one with no patterns and no rhs. Should not exist in practice.

KillRange Clause Source # 
HasRange Clause 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 # 
DropArgs Clause Source #

NOTE: does not work for recursive functions.

Methods

dropArgs :: Int -> Clause -> Clause Source #

DropArgs FunctionInverse Source # 
PrettyTCM Clause Source # 
InstantiateFull Clause Source # 
InstantiateFull FunctionInverse Source # 
NormaliseProjP Clause Source # 
Occurs Clause Source # 
ComputeOccurrences Clause 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 # 
Reify (QNamed Clause) Clause Source # 
UniverseBi ([Type], [Clause]) Pattern Source # 

Methods

universeBi :: ([Type], [Clause]) -> [Pattern] #

UniverseBi ([Type], [Clause]) Term Source # 

Methods

universeBi :: ([Type], [Clause]) -> [Term] #

type PatVarName = ArgName Source #

Pattern variables.

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 # 
UniverseBi Elims Pattern Source # 

Methods

universeBi :: Elims -> [Pattern] #

UniverseBi Args Pattern Source # 

Methods

universeBi :: Args -> [Pattern] #

LabelPatVars Pattern DeBruijnPattern Int 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 # 
KillRange a => KillRange (Pattern' a) Source # 
IsProjP (Pattern' a) 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 # 
Normalise a => Normalise (Pattern' a) Source # 
NormaliseProjP (Pattern' x) Source # 
IsFlexiblePattern (Pattern' a) Source # 
UniverseBi ([Type], [Clause]) Pattern Source # 

Methods

universeBi :: ([Type], [Clause]) -> [Pattern] #

type Pattern Source #

Arguments

 = Pattern' PatVarName

The PatVarName is a name suggestion.

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.

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 # 
InstantiateFull Substitution Source # 
Show a => Show (Substitution' a) Source # 
Pretty a => Pretty (Substitution' a) Source # 
Null (Substitution' a) Source # 
TermSize a => TermSize (Substitution' a) Source # 
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # 

Views

Absurd Lambda

absurdBody :: Abs Term Source #

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

Pointers and Sharing

ignoreSharing :: Term -> Term Source #

Remove top-level Shared data constructors.

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 #

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).

sSuc :: Sort -> Sort Source #

Get the next higher sort.

class SgTel a where Source #

Constructing a singleton telescope.

Minimal complete definition

sgTel

Methods

sgTel :: a -> Telescope Source #

Handling blocked terms.

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 # 
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

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 #

KillRange instances.

UniverseBi instances.

Simple pretty printing

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

NFData instances

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId 

Fields

Instances

Enum MetaId Source # 
Eq MetaId Source # 

Methods

(==) :: MetaId -> MetaId -> Bool #

(/=) :: MetaId -> MetaId -> Bool #

Integral MetaId Source # 
Num MetaId Source # 
Ord MetaId Source # 
Real MetaId Source # 
Show MetaId Source #

Show non-record version of this newtype.

NFData MetaId Source # 

Methods

rnf :: MetaId -> () #

Pretty MetaId Source # 
GetDefs MetaId Source # 

Methods

getDefs :: MonadGetDefs m => MetaId -> m () Source #

HasFresh MetaId Source # 
UnFreezeMeta MetaId Source # 

Methods

unfreezeMeta :: MetaId -> TCM () Source #

IsInstantiatedMeta MetaId Source # 
PrettyTCM MetaId Source # 
FromTerm MetaId Source # 
ToTerm MetaId Source # 
PrimTerm MetaId Source # 
Unquote MetaId Source # 
Reify MetaId Expr Source #