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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Internal

Synopsis

- class TermSize a where
  - termSize :: a -> Int
  - tsize :: a -> Sum Int
- class IsProjElim e where
  - isProjElim :: e -> Maybe (ProjOrigin, QName)
- class Suggest a b where
  - suggest :: a -> b -> String
- class SgTel a where
  - sgTel :: a -> Telescope
- class TelToArgs a where
  - telToArgs :: a -> [Arg ArgName]
- type ListTel = ListTel' ArgName
- type ListTel' a = [Dom (a, Type)]
- data IntervalView
  - = IZero
  - | IOne
  - | IMin (Arg Term) (Arg Term)
  - | IMax (Arg Term) (Arg Term)
  - | INeg (Arg Term)
  - | OTerm Term
- data PathView
  - = PathType {
    - pathSort :: Sort
    - pathName :: QName
    - pathLevel :: Arg Term
    - pathType :: Arg Term
    - pathLhs :: Arg Term
    - pathRhs :: Arg Term
    }
  - | OType Type
- data EqualityView
  - = EqualityType {
    - eqtSort :: Sort
    - eqtName :: QName
    - eqtParams :: [Arg Term]
    - eqtType :: Arg Term
    - eqtLhs :: Arg Term
    - eqtRhs :: Arg Term
    }
  - | OtherType Type
- type PatternSubstitution = Substitution' DeBruijnPattern
- type Substitution = Substitution' Term
- data Substitution' a
  - = IdS
  - | EmptyS Empty
  - | a :# (Substitution' a)
  - | Strengthen Empty (Substitution' a)
  - | Wk !Int (Substitution' a)
  - | Lift !Int (Substitution' a)
- class PatternVars a b | b -> a where
  - patternVars :: b -> [Arg (Either a Term)]
- data ConPatternInfo = ConPatternInfo {
  - conPRecord :: Maybe PatOrigin
  - conPFallThrough :: Bool
  - conPType :: Maybe (Arg Type)
  - conPLazy :: Bool
  }
- type DeBruijnPattern = Pattern' DBPatVar
- data DBPatVar = DBPatVar {
  - dbPatVarName :: PatVarName
  - dbPatVarIndex :: Int
  }
- type Pattern = Pattern' PatVarName
- data Pattern' x
  - = VarP PatOrigin x
  - | DotP PatOrigin Term
  - | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
  - | LitP Literal
  - | ProjP ProjOrigin QName
  - | IApplyP PatOrigin Term Term x
  - | DefP PatOrigin QName [NamedArg (Pattern' x)]
- data PatOrigin
  - = PatOSystem
  - | PatOSplit
  - | PatOVar Name
  - | PatODot
  - | PatOWild
  - | PatOCon
  - | PatORec
  - | PatOLit
  - | PatOAbsurd
- type PatVarName = ArgName
- data Clause = Clause {
  - clauseLHSRange :: Range
  - clauseFullRange :: Range
  - clauseTel :: Telescope
  - namedClausePats :: NAPs
  - clauseBody :: Maybe Term
  - clauseType :: Maybe (Arg Type)
  - clauseCatchall :: Bool
  - clauseUnreachable :: Maybe Bool
  }
- type NAPs = [NamedArg DeBruijnPattern]
- type Blocked_ = Blocked ()
- data Blocked t
  - = Blocked {
    - theBlockingMeta :: MetaId
    - ignoreBlocking :: t
    }
  - | NotBlocked {
    - blockingStatus :: NotBlocked
    - ignoreBlocking :: t
    }
- data NotBlocked
  - = StuckOn Elim
  - | Underapplied
  - | AbsurdMatch
  - | MissingClauses
  - | ReallyNotBlocked
- data LevelAtom
  - = MetaLevel MetaId Elims
  - | BlockedLevel MetaId Term
  - | NeutralLevel NotBlocked Term
  - | UnreducedLevel Term
- data PlusLevel
  - = ClosedLevel Integer
  - | Plus Integer LevelAtom
- newtype Level = Max [PlusLevel]
- data Sort
  - = Type Level
  - | Prop Level
  - | Inf
  - | SizeUniv
  - | PiSort Sort (Abs Sort)
  - | UnivSort Sort
  - | MetaS !MetaId Elims
  - | DefS QName Elims
  - | DummyS String
- type Telescope = Tele (Dom Type)
- data Tele a
  - = EmptyTel
  - | ExtendTel a (Abs (Tele a))
- class LensSort a where
  - lensSort :: Lens' Sort a
  - getSort :: a -> Sort
- type Type = Type' Term
- data Type' a = El {
  - _getSort :: Sort
  - unEl :: a
  }
- data Abs a
  - = Abs {
    - absName :: ArgName
    - unAbs :: a
    }
  - | NoAbs {
    - absName :: ArgName
    - unAbs :: a
    }
- type ArgName = String
- type Elims = [Elim]
- type Elim = Elim' Term
- data Elim' a
  - = Apply (Arg a)
  - | Proj ProjOrigin QName
  - | IApply a a a
- type ConInfo = ConOrigin
- data Term
  - = Var !Int Elims
  - | Lam ArgInfo (Abs Term)
  - | Lit Literal
  - | Def QName Elims
  - | Con ConHead ConInfo Elims
  - | Pi (Dom Type) (Abs Type)
  - | Sort Sort
  - | Level Level
  - | MetaV !MetaId Elims
  - | DontCare Term
  - | Dummy String
- class LensConName a where
  - getConName :: a -> QName
  - setConName :: QName -> a -> a
  - mapConName :: (QName -> QName) -> a -> a
- data ConHead = ConHead {
  - conName :: QName
  - conInductive :: Induction
  - conFields :: [Arg QName]
  }
- type NamedArgs = [NamedArg Term]
- type Args = [Arg Term]
- argNameToString :: ArgName -> String
- stringToArgName :: String -> ArgName
- appendArgNames :: ArgName -> ArgName -> ArgName
- nameToArgName :: Name -> ArgName
- namedArgName :: NamedArg Name -> ArgName
- stuckOn :: Elim -> NotBlocked -> NotBlocked
- clausePats :: Clause -> [Arg DeBruijnPattern]
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- varP :: a -> Pattern' a
- dotP :: Term -> Pattern' a
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- absurdP :: Int -> DeBruijnPattern
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- patternOrigin :: Pattern' x -> Maybe PatOrigin
- properlyMatching :: DeBruijnPattern -> Bool
- isEqualityType :: EqualityView -> Bool
- isPathType :: PathView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- absurdPatternName :: PatVarName
- isAbsurdPatternName :: PatVarName -> Bool
- var :: Nat -> Term
- dontCare :: Term -> Term
- dummyTerm' :: String -> Int -> Term
- dummyLevel' :: String -> Int -> Level
- dummyTerm :: String -> Int -> Term
- dummyLevel :: String -> Int -> Level
- dummySort :: String -> Int -> Sort
- dummyType :: String -> Int -> Type
- dummyDom :: String -> Int -> Dom Type
- unreducedLevel :: Term -> Level
- topSort :: Type
- sort :: Sort -> Type
- varSort :: Int -> Sort
- tmSort :: Term -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- mkProp :: Integer -> Sort
- isSort :: Term -> Maybe Sort
- impossibleTerm :: String -> Int -> Term
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- telToList :: Tele (Dom t) -> [Dom (ArgName, t)]
- listTel :: Lens' ListTel Telescope
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- stripDontCare :: Term -> Term
- arity :: Type -> Nat
- unSpine :: Term -> Term
- unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- isApplyElim :: Elim' a -> Maybe (Arg a)
- isApplyElim' :: Empty -> Elim' a -> Arg a
- allApplyElims :: [Elim' a] -> Maybe [Arg a]
- splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
- argsFromElims :: Elims -> Args
- allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
- pDom :: LensHiding a => a -> Doc -> Doc
- module Agda.Syntax.Abstract.Name
- newtype MetaId = MetaId {
  - metaId :: Nat
  }

# Documentation

class TermSize a where Source #

The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).

Not counting towards the term size are:

- sort and color annotations,
- projections.

Minimal complete definition

tsize

Methods

termSize :: a -> Int Source #

tsize :: a -> Sum Int Source #

Instances

TermSize LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: LevelAtom -> Int Source # tsize :: LevelAtom -> Sum Int Source #
TermSize PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
TermSize Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
TermSize Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
TermSize Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Term -> Int Source # tsize :: Term -> Sum Int Source #
(Foldable t, TermSize a) => TermSize (t a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: t a -> Int Source # tsize :: t a -> Sum Int Source #
TermSize a => TermSize (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #

class IsProjElim e where Source #

Methods

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

Instances

IsProjElim Elim Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source #
IsProjElim e => IsProjElim (MaybeReduced e) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) Source #

class Suggest a b where Source #

Pick the better name suggestion, i.e., the one that is not just underscore.

Methods

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

Instances

Suggest String String Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: String -> String -> String Source #
Suggest String (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: String -> Abs b -> String Source #
Suggest Name (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Name -> Abs b -> String Source #
Suggest (Abs a) (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Abs a -> Abs b -> String Source #

class SgTel a where Source #

Constructing a singleton telescope.

Methods

sgTel :: a -> Telescope Source #

Instances

SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #

class TelToArgs a where Source #

Drop the types from a telescope.

Methods

telToArgs :: a -> [Arg ArgName] Source #

Instances

TelToArgs ListTel Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #

type ListTel = ListTel' ArgName Source #

type ListTel' a = [Dom (a, Type)] Source #

Telescope as list.

data IntervalView Source #

Constructors

IZero |
IOne |
IMin (Arg Term) (Arg Term) |
IMax (Arg Term) (Arg Term) |
INeg (Arg Term) |
OTerm Term |

Instances

Show IntervalView Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> IntervalView -> ShowS Source # show :: IntervalView -> String Source # showList :: [IntervalView] -> ShowS Source #

data PathView Source #

View type as path type.

Constructors

PathType |

Fields

- pathSort :: Sort

  Sort of this type.

- pathName :: QName

  Builtin PATH.

- pathLevel :: Arg Term

  Hidden

- pathType :: Arg Term

  Hidden

- pathLhs :: Arg Term

  NotHidden

- pathRhs :: Arg Term

  NotHidden

OType Type | reduced

data EqualityView Source #

View type as equality type.

Constructors

EqualityType |

Fields

- eqtSort :: Sort

  Sort of this type.

- eqtName :: QName

  Builtin EQUALITY.

- eqtParams :: [Arg Term]

  Hidden. Empty or `Level`.

- eqtType :: Arg Term

  Hidden

- eqtLhs :: Arg Term

  NotHidden

- eqtRhs :: Arg Term

  NotHidden

OtherType Type | reduced

Instances

Free EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => EqualityView -> FreeM c Source #
TermLike EqualityView Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView Source # foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m Source #
PrettyTCM EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: EqualityView -> TCM Doc Source #
InstantiateFull EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: EqualityView -> ReduceM EqualityView Source #
Normalise EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: EqualityView -> ReduceM EqualityView Source #
Simplify EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: EqualityView -> ReduceM EqualityView Source #
Reduce EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source #
Instantiate EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: EqualityView -> ReduceM EqualityView Source #
Subst Term EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView Source #

type PatternSubstitution = Substitution' DeBruijnPattern Source #

type Substitution = Substitution' Term Source #

data Substitution' a Source #

Substitutions.

Constructors

IdS | Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Empty | Empty substitution, lifts from the empty context. First argument is `(throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 614))`. 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 `(throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 627))`. 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 # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b Source # (<$) :: a -> Substitution' b -> Substitution' a Source #
Foldable Substitution' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Substitution' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Substitution' a -> m Source #

foldr :: (a -> b -> b) -> b -> Substitution' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Substitution' a -> b Source #

foldl :: (b -> a -> b) -> b -> Substitution' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Substitution' a -> b Source #

foldr1 :: (a -> a -> a) -> Substitution' a -> a Source #

foldl1 :: (a -> a -> a) -> Substitution' a -> a Source #

toList :: Substitution' a -> [a] Source #

null :: Substitution' a -> Bool Source #

length :: Substitution' a -> Int Source #

elem :: Eq a => a -> Substitution' a -> Bool Source #

maximum :: Ord a => Substitution' a -> a Source #

minimum :: Ord a => Substitution' a -> a Source #

sum :: Num a => Substitution' a -> a Source #

product :: Num a => Substitution' a -> a Source #

Traversable Substitution' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) Source # sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) Source # mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) Source # sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) Source #
KillRange Substitution Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution Source #
InstantiateFull Substitution Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
Subst a a => Subst a (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' a -> Substitution' a -> Substitution' a Source #
Eq (Substitution' Term) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution' Term -> Substitution' Term -> Bool Source # (/=) :: Substitution' Term -> Substitution' Term -> Bool Source #
Data a => Data (Substitution' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Substitution' a -> c (Substitution' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Substitution' a) Source #

toConstr :: Substitution' a -> Constr Source #

dataTypeOf :: Substitution' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Substitution' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Substitution' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Substitution' a -> Substitution' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Substitution' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Substitution' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a) Source #

Ord (Substitution' Term) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution' Term -> Substitution' Term -> Ordering Source #

(<) :: Substitution' Term -> Substitution' Term -> Bool Source #

(<=) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>=) :: Substitution' Term -> Substitution' Term -> Bool Source #

max :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

min :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

Show a => Show (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Substitution' a -> ShowS Source # show :: Substitution' a -> String Source # showList :: [Substitution' a] -> ShowS Source #
Null (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
Pretty a => Pretty (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source #
TermSize a => TermSize (Substitution' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #
EmbPrj a => EmbPrj (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source #
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Substitution' a -> TCM Doc Source #

class PatternVars a b | b -> a where Source #

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

Methods

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

Instances

PatternVars a b => PatternVars a [b] Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: [b] -> [Arg (Either a Term)] Source #
PatternVars a (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] Source #
PatternVars a (Arg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] 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 `PatOrigin` says whether the record pattern orginates from the expansion of an implicit pattern. The `Type` is the type of the whole record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (`clauseTel`).

Constructors

ConPatternInfo |

Fields

- conPRecord :: Maybe PatOrigin

  `Nothing` if data constructor. `Just` if record constructor.

- conPFallThrough :: Bool

  Should the match block on non-canonical terms or can it proceed to the catch-all clause?

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

- conPLazy :: Bool

  Lazy patterns are generated by the forcing translation (`forcingTranslation`) and are dropped by the clause compiler (TODO: not yet) (`compileClauses`) when the variables they bind are unused. The GHC backend compiles lazy matches to lazy patterns in Haskell (TODO: not yet).

Instances

Data ConPatternInfo Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatternInfo Source #

toConstr :: ConPatternInfo -> Constr Source #

dataTypeOf :: ConPatternInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatternInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConPatternInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo Source #

Show ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConPatternInfo -> ShowS Source # show :: ConPatternInfo -> String Source # showList :: [ConPatternInfo] -> ShowS Source #
KillRange ConPatternInfo Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConPatternInfo Source #
EmbPrj ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Int32 Source # icod_ :: ConPatternInfo -> S Int32 Source # value :: Int32 -> R ConPatternInfo Source #
InstantiateFull ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source #
Normalise ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source #
Subst Term ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo Source #

type DeBruijnPattern = Pattern' DBPatVar Source #

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar |

Fields

- dbPatVarName :: PatVarName
- dbPatVarIndex :: Int

Instances

Eq DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: DBPatVar -> DBPatVar -> Bool Source # (/=) :: DBPatVar -> DBPatVar -> Bool Source #
Data DBPatVar Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DBPatVar -> c DBPatVar Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DBPatVar Source #

toConstr :: DBPatVar -> Constr Source #

dataTypeOf :: DBPatVar -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DBPatVar) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DBPatVar) Source #

gmapT :: (forall b. Data b => b -> b) -> DBPatVar -> DBPatVar Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DBPatVar -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DBPatVar -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DBPatVar -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DBPatVar -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DBPatVar -> m DBPatVar Source #

Show DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> DBPatVar -> ShowS Source # show :: DBPatVar -> String Source # showList :: [DBPatVar] -> ShowS Source #
Pretty DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: DBPatVar -> Doc Source # prettyPrec :: Int -> DBPatVar -> Doc Source # prettyList :: [DBPatVar] -> Doc Source #
KillRange DBPatVar Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT DBPatVar Source #
DeBruijn DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> DeBruijnPattern Source # debruijnNamedVar :: String -> Int -> DeBruijnPattern Source # deBruijnView :: DeBruijnPattern -> Maybe Int Source #
DeBruijn DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> DBPatVar Source # debruijnNamedVar :: String -> Int -> DBPatVar Source # deBruijnView :: DBPatVar -> Maybe Int Source #
EmbPrj DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DBPatVar -> S Int32 Source # icod_ :: DBPatVar -> S Int32 Source # value :: Int32 -> R DBPatVar Source #
PrettyTCM DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: DBPatVar -> TCM Doc Source #
InstantiateFull DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DBPatVar -> ReduceM DBPatVar Source #
Normalise DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DBPatVar -> ReduceM DBPatVar Source #
UsableSizeVars DeBruijnPattern Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars MaskedDeBruijnPatterns Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #
Subst DeBruijnPattern DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern Source #
LabelPatVars Pattern DeBruijnPattern Int Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern Source # unlabelPatVars :: DeBruijnPattern -> Pattern Source #
UsableSizeVars [DeBruijnPattern] Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #
UsableSizeVars (Masked DeBruijnPattern) Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #

type Pattern Source #

Arguments

= Pattern' PatVarName | The `PatVarName` is a name suggestion.

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 PatOrigin x

    x

DotP PatOrigin 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.
IApplyP PatOrigin Term Term x | Path elimination pattern, like `VarP` but keeps track of endpoints.
DefP PatOrigin QName [NamedArg (Pattern' x)] | Used for HITs, the QName should be the one from primHComp.

Instances

Functor Pattern' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b Source # (<$) :: a -> Pattern' b -> Pattern' a Source #
Foldable Pattern' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Pattern' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Pattern' a -> m Source #

foldr :: (a -> b -> b) -> b -> Pattern' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Pattern' a -> b Source #

foldl :: (b -> a -> b) -> b -> Pattern' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Pattern' a -> b Source #

foldr1 :: (a -> a -> a) -> Pattern' a -> a Source #

foldl1 :: (a -> a -> a) -> Pattern' a -> a Source #

toList :: Pattern' a -> [a] Source #

null :: Pattern' a -> Bool Source #

length :: Pattern' a -> Int Source #

elem :: Eq a => a -> Pattern' a -> Bool Source #

maximum :: Ord a => Pattern' a -> a Source #

minimum :: Ord a => Pattern' a -> a Source #

sum :: Num a => Pattern' a -> a Source #

product :: Num a => Pattern' a -> a Source #

Traversable Pattern' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) Source # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) Source # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) Source # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) Source #
DeBruijn DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> DeBruijnPattern Source # debruijnNamedVar :: String -> Int -> DeBruijnPattern Source # deBruijnView :: DeBruijnPattern -> Maybe Int Source #
DeBruijn SplitPattern Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods deBruijnVar :: Int -> SplitPattern Source # debruijnNamedVar :: String -> Int -> SplitPattern Source # deBruijnView :: SplitPattern -> Maybe Int Source #
UsableSizeVars DeBruijnPattern Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: DeBruijnPattern -> TerM VarSet Source #
UsableSizeVars MaskedDeBruijnPatterns Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source #
UniverseBi Elims Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Pattern] Source #
UniverseBi Args Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Pattern] Source #
Subst DeBruijnPattern DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern Source #
Subst Term Pattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Pattern -> Pattern Source #
Subst SplitPattern SplitPattern Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern Source #
LabelPatVars Pattern DeBruijnPattern Int Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Pattern -> State [Int] DeBruijnPattern Source # unlabelPatVars :: DeBruijnPattern -> Pattern Source #
PatternVars a (NamedArg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either a Term)] Source #
PatternVars a (Arg (Pattern' a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)] Source #
PatternLike a (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) Source #
Conversion TOM (Arg Pattern) (Pat O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #
Eq a => Eq (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Pattern' a -> Pattern' a -> Bool Source # (/=) :: Pattern' a -> Pattern' a -> Bool Source #
Data x => Data (Pattern' x) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' x) Source #

toConstr :: Pattern' x -> Constr Source #

dataTypeOf :: Pattern' x -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' x)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Pattern' x)) Source #

gmapT :: (forall b. Data b => b -> b) -> Pattern' x -> Pattern' x Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Pattern' x -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' x -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) Source #

Show x => Show (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Pattern' x -> ShowS Source # show :: Pattern' x -> String Source # showList :: [Pattern' x] -> ShowS Source #
Pretty a => Pretty (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Pattern' a -> Doc Source # prettyPrec :: Int -> Pattern' a -> Doc Source # prettyList :: [Pattern' a] -> Doc Source #
KillRange a => KillRange (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) Source #
IsProjP (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
CountPatternVars (Pattern' x) Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source #
EmbPrj a => EmbPrj (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Pattern' a -> S Int32 Source # icod_ :: Pattern' a -> S Int32 Source # value :: Int32 -> R (Pattern' a) Source #
PrettyTCM a => PrettyTCM (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Pattern' a -> TCM Doc Source #
NamesIn (Pattern' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Pattern' a -> Set QName Source #
InstantiateFull a => InstantiateFull (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) Source #
Normalise a => Normalise (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Pattern' a -> ReduceM (Pattern' a) Source #
NormaliseProjP (Pattern' x) Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source #
UsableSizeVars [DeBruijnPattern] Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source #
UsableSizeVars (Masked DeBruijnPattern) Source # |
Instance details Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source #
IsFlexiblePattern (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern' a -> TCM Bool Source #
PatternVarModalities (Pattern' x) x Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Pattern' x -> [(x, Modality)] Source #
UniverseBi ([Type], [Clause]) Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] Source #

data PatOrigin Source #

Origin of the pattern: what did the user write in this position?

Constructors

PatOSystem | Pattern inserted by the system
PatOSplit | Pattern generated by case split
PatOVar Name | User wrote a variable pattern
PatODot | User wrote a dot pattern
PatOWild | User wrote a wildcard pattern
PatOCon | User wrote a constructor pattern
PatORec | User wrote a record pattern
PatOLit | User wrote a literal pattern
PatOAbsurd | User wrote an absurd pattern

Instances

Eq PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: PatOrigin -> PatOrigin -> Bool Source # (/=) :: PatOrigin -> PatOrigin -> Bool Source #
Data PatOrigin Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatOrigin -> c PatOrigin Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatOrigin Source #

toConstr :: PatOrigin -> Constr Source #

dataTypeOf :: PatOrigin -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatOrigin) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin) Source #

gmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> PatOrigin -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PatOrigin -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin Source #

Show PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatOrigin -> ShowS Source # show :: PatOrigin -> String Source # showList :: [PatOrigin] -> ShowS Source #
KillRange PatOrigin Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PatOrigin Source #
EmbPrj PatOrigin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatOrigin -> S Int32 Source # icod_ :: PatOrigin -> S Int32 Source # value :: Int32 -> R PatOrigin Source #

type PatVarName = ArgName Source #

Pattern variables.

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

- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope

  `Δ`: The types of the pattern variables in dependency order.

- namedClausePats :: NAPs

  `Δ ⊢ 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.

- clauseUnreachable :: Maybe Bool

  Clause has been labelled as unreachable by the coverage checker. `Nothing` means coverage checker has not run yet (clause may be unreachable). `Just False` means clause is not unreachable. `Just True` means clause is unreachable.

Instances

Data Clause Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause Source #

toConstr :: Clause -> Constr Source #

dataTypeOf :: Clause -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause) Source #

gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause Source #

Show Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Clause -> ShowS Source # show :: Clause -> String Source # showList :: [Clause] -> ShowS Source #
Null Clause Source # | A `null` clause is one with no patterns and no rhs. Should not exist in practice.
Instance details Defined in Agda.Syntax.Internal Methods empty :: Clause Source # null :: Clause -> Bool Source #
Pretty Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Clause -> Doc Source # prettyPrec :: Int -> Clause -> Doc Source # prettyList :: [Clause] -> Doc Source #
KillRange Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Clause Source #
HasRange Clause Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: Clause -> Range Source #
Free Clause Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Clause -> FreeM c Source #
Abstract Clause Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Clause -> Clause Source #
Abstract FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Apply Clause Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Clause -> Args -> Clause Source # applyE :: Clause -> Elims -> Clause Source #
Apply FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
GetDefs Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Clause -> m () Source #
FunArity Clause Source # | Get the number of initial `Apply` patterns in a clause.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: Clause -> Int Source #
Free Clause Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Clause -> FreeT
EmbPrj Clause Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Clause -> S Int32 Source # icod_ :: Clause -> S Int32 Source # value :: Int32 -> R Clause Source #
PrettyTCM Clause Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Clause -> TCM Doc Source #
NamesIn Clause Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Clause -> Set QName Source #
DropArgs Clause Source # | NOTE: does not work for recursive functions.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Clause -> Clause Source #
DropArgs FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source #
InstantiateFull Clause Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Clause -> ReduceM Clause Source #
InstantiateFull FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source #
NormaliseProjP Clause Source # |
Instance details Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause Source #
ComputeOccurrences Clause Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Clause -> OccM OccurrencesBuilder Source #
Occurs Clause Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Clause -> TCM Clause Source # metaOccurs :: MetaId -> Clause -> TCM () Source #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
FunArity [Clause] Source # | Get the number of common initial `Apply` patterns in a list of clauses.
Instance details Defined in Agda.Syntax.Internal.Pattern Methods funArity :: [Clause] -> Int Source #
PrettyTCM (QNamed Clause) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: QNamed Clause -> TCM Doc Source #
Reify (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause Source #
UniverseBi ([Type], [Clause]) Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] Source #
UniverseBi ([Type], [Clause]) Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Term] Source #

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

type Blocked_ = Blocked () Source #

``Blocked` t` without the `t`.

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 # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Blocked a -> Blocked b Source # (<$) :: a -> Blocked b -> Blocked a Source #
Applicative Blocked Source # | Blocking by a meta is dominant.
Instance details Defined in Agda.Syntax.Internal Methods pure :: a -> Blocked a Source # (<*>) :: Blocked (a -> b) -> Blocked a -> Blocked b Source # liftA2 :: (a -> b -> c) -> Blocked a -> Blocked b -> Blocked c Source # (*>) :: Blocked a -> Blocked b -> Blocked b Source # (<*) :: Blocked a -> Blocked b -> Blocked a Source #
Foldable Blocked Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Blocked m -> m Source #

foldMap :: Monoid m => (a -> m) -> Blocked a -> m Source #

foldr :: (a -> b -> b) -> b -> Blocked a -> b Source #

foldr' :: (a -> b -> b) -> b -> Blocked a -> b Source #

foldl :: (b -> a -> b) -> b -> Blocked a -> b Source #

foldl' :: (b -> a -> b) -> b -> Blocked a -> b Source #

foldr1 :: (a -> a -> a) -> Blocked a -> a Source #

foldl1 :: (a -> a -> a) -> Blocked a -> a Source #

toList :: Blocked a -> [a] Source #

null :: Blocked a -> Bool Source #

length :: Blocked a -> Int Source #

elem :: Eq a => a -> Blocked a -> Bool Source #

maximum :: Ord a => Blocked a -> a Source #

minimum :: Ord a => Blocked a -> a Source #

sum :: Num a => Blocked a -> a Source #

product :: Num a => Blocked a -> a Source #

Traversable Blocked Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Blocked a -> f (Blocked b) Source # sequenceA :: Applicative f => Blocked (f a) -> f (Blocked a) Source # mapM :: Monad m => (a -> m b) -> Blocked a -> m (Blocked b) Source # sequence :: Monad m => Blocked (m a) -> m (Blocked a) Source #
Semigroup Blocked_ Source # |
Instance details Defined in Agda.Syntax.Internal Methods (<>) :: Blocked_ -> Blocked_ -> Blocked_ Source # sconcat :: NonEmpty Blocked_ -> Blocked_ Source # stimes :: Integral b => b -> Blocked_ -> Blocked_ Source #
Monoid Blocked_ Source # |
Instance details Defined in Agda.Syntax.Internal Methods mempty :: Blocked_ Source # mappend :: Blocked_ -> Blocked_ -> Blocked_ Source # mconcat :: [Blocked_] -> Blocked_ Source #
Subst t a => Subst t (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Blocked a -> Blocked a Source #
Eq t => Eq (Blocked t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Blocked t -> Blocked t -> Bool Source # (/=) :: Blocked t -> Blocked t -> Bool Source #
Show t => Show (Blocked t) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Blocked t -> ShowS Source # show :: Blocked t -> String Source # showList :: [Blocked t] -> ShowS Source #
KillRange a => KillRange (Blocked a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source #
Apply t => Apply (Blocked t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
TermLike a => TermLike (Blocked a) Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods 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 # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Blocked a -> TCM Doc Source #
Instantiate a => Instantiate (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) Source #

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

Eq NotBlocked Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: NotBlocked -> NotBlocked -> Bool Source # (/=) :: NotBlocked -> NotBlocked -> Bool Source #
Data NotBlocked Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NotBlocked -> c NotBlocked Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NotBlocked Source #

toConstr :: NotBlocked -> Constr Source #

dataTypeOf :: NotBlocked -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NotBlocked) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NotBlocked) Source #

gmapT :: (forall b. Data b => b -> b) -> NotBlocked -> NotBlocked Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NotBlocked -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NotBlocked -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> NotBlocked -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NotBlocked -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NotBlocked -> m NotBlocked Source #

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

Eq LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: LevelAtom -> LevelAtom -> Bool Source # (/=) :: LevelAtom -> LevelAtom -> Bool Source #
Data LevelAtom Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LevelAtom -> c LevelAtom Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LevelAtom Source #

toConstr :: LevelAtom -> Constr Source #

dataTypeOf :: LevelAtom -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LevelAtom) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LevelAtom) Source #

gmapT :: (forall b. Data b => b -> b) -> LevelAtom -> LevelAtom Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LevelAtom -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LevelAtom -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LevelAtom -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LevelAtom -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LevelAtom -> m LevelAtom Source #

Ord LevelAtom Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: LevelAtom -> LevelAtom -> Ordering Source #

(<) :: LevelAtom -> LevelAtom -> Bool Source #

(<=) :: LevelAtom -> LevelAtom -> Bool Source #

(>) :: LevelAtom -> LevelAtom -> Bool Source #

(>=) :: LevelAtom -> LevelAtom -> Bool Source #

max :: LevelAtom -> LevelAtom -> LevelAtom Source #

min :: LevelAtom -> LevelAtom -> LevelAtom Source #

Show LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> LevelAtom -> ShowS Source # show :: LevelAtom -> String Source # showList :: [LevelAtom] -> ShowS Source #
NFData LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: LevelAtom -> () Source #
Pretty LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: LevelAtom -> Doc Source # prettyPrec :: Int -> LevelAtom -> Doc Source # prettyList :: [LevelAtom] -> Doc Source #
KillRange LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT LevelAtom Source #
TermSize LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: LevelAtom -> Int Source # tsize :: LevelAtom -> Sum Int Source #
DeBruijn LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> LevelAtom Source # debruijnNamedVar :: String -> Int -> LevelAtom Source # deBruijnView :: LevelAtom -> Maybe Int Source #
PrecomputeFreeVars LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: LevelAtom -> FV LevelAtom Source #
Free LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => LevelAtom -> FreeM c Source #
TermLike LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> LevelAtom -> m LevelAtom Source # foldTerm :: Monoid m => (Term -> m) -> LevelAtom -> m Source #
GetDefs LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => LevelAtom -> m () Source #
Free LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: LevelAtom -> FreeT
EmbPrj LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: LevelAtom -> S Int32 Source # icod_ :: LevelAtom -> S Int32 Source # value :: Int32 -> R LevelAtom Source #
NamesIn LevelAtom Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: LevelAtom -> Set QName Source #
UnFreezeMeta LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: LevelAtom -> TCM () Source #
IsInstantiatedMeta LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: LevelAtom -> TCM Bool Source #
MentionsMeta LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> LevelAtom -> Bool Source #
InstantiateFull LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: LevelAtom -> ReduceM LevelAtom Source #
Normalise LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: LevelAtom -> ReduceM LevelAtom Source #
Simplify LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: LevelAtom -> ReduceM LevelAtom Source #
Reduce LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: LevelAtom -> ReduceM LevelAtom Source # reduceB' :: LevelAtom -> ReduceM (Blocked LevelAtom) Source #
Instantiate LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: LevelAtom -> ReduceM LevelAtom Source #
SynEq LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom) synEq' :: LevelAtom -> LevelAtom -> SynEqM (LevelAtom, LevelAtom)
ForceNotFree LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => LevelAtom -> m LevelAtom
UsableRelevance LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> LevelAtom -> TCM Bool Source #
ComputeOccurrences LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: LevelAtom -> OccM OccurrencesBuilder Source #
HasPolarity LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> LevelAtom -> TCM [Polarity] Source #
FoldRigid LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> LevelAtom -> TCM m Source #
Occurs LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> LevelAtom -> TCM LevelAtom Source # metaOccurs :: MetaId -> LevelAtom -> TCM () Source #
AbsTerm LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> LevelAtom -> LevelAtom Source #
Subst Term LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> LevelAtom -> LevelAtom Source #

data PlusLevel Source #

Constructors

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

Instances

Eq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: PlusLevel -> PlusLevel -> Bool Source # (/=) :: PlusLevel -> PlusLevel -> Bool Source #
Data PlusLevel Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlusLevel -> c PlusLevel Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlusLevel Source #

toConstr :: PlusLevel -> Constr Source #

dataTypeOf :: PlusLevel -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PlusLevel) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlusLevel) Source #

gmapT :: (forall b. Data b => b -> b) -> PlusLevel -> PlusLevel Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlusLevel -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlusLevel -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> PlusLevel -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PlusLevel -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlusLevel -> m PlusLevel Source #

Ord PlusLevel Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: PlusLevel -> PlusLevel -> Ordering Source #

(<) :: PlusLevel -> PlusLevel -> Bool Source #

(<=) :: PlusLevel -> PlusLevel -> Bool Source #

(>) :: PlusLevel -> PlusLevel -> Bool Source #

(>=) :: PlusLevel -> PlusLevel -> Bool Source #

max :: PlusLevel -> PlusLevel -> PlusLevel Source #

min :: PlusLevel -> PlusLevel -> PlusLevel Source #

Show PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PlusLevel -> ShowS Source # show :: PlusLevel -> String Source # showList :: [PlusLevel] -> ShowS Source #
NFData PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: PlusLevel -> () Source #
Pretty PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: PlusLevel -> Doc Source # prettyPrec :: Int -> PlusLevel -> Doc Source # prettyList :: [PlusLevel] -> Doc Source #
KillRange PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT PlusLevel Source #
TermSize PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: PlusLevel -> Int Source # tsize :: PlusLevel -> Sum Int Source #
DeBruijn PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> PlusLevel Source # debruijnNamedVar :: String -> Int -> PlusLevel Source # deBruijnView :: PlusLevel -> Maybe Int Source #
PrecomputeFreeVars PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source #
Free PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => PlusLevel -> FreeM c Source #
TermLike PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> PlusLevel -> m PlusLevel Source # foldTerm :: Monoid m => (Term -> m) -> PlusLevel -> m Source #
GetDefs PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => PlusLevel -> m () Source #
Free PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: PlusLevel -> FreeT
EmbPrj PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PlusLevel -> S Int32 Source # icod_ :: PlusLevel -> S Int32 Source # value :: Int32 -> R PlusLevel Source #
NamesIn PlusLevel Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: PlusLevel -> Set QName Source #
UnFreezeMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: PlusLevel -> TCM () Source #
IsInstantiatedMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: PlusLevel -> TCM Bool Source #
MentionsMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> PlusLevel -> Bool Source #
InstantiateFull PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #
Normalise PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: PlusLevel -> ReduceM PlusLevel Source #
Simplify PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel Source #
Reduce PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel Source # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #
Instantiate PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: PlusLevel -> ReduceM PlusLevel Source #
SynEq PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel) synEq' :: PlusLevel -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
ForceNotFree PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => PlusLevel -> m PlusLevel
UsableRelevance PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> PlusLevel -> TCM Bool Source #
ComputeOccurrences PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: PlusLevel -> OccM OccurrencesBuilder Source #
HasPolarity PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> PlusLevel -> TCM [Polarity] Source #
FoldRigid PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> PlusLevel -> TCM m Source #
Occurs PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> PlusLevel -> TCM PlusLevel Source # metaOccurs :: MetaId -> PlusLevel -> TCM () Source #
AbsTerm PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> PlusLevel -> PlusLevel Source #
Subst Term PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> PlusLevel -> PlusLevel 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

Eq Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Level -> Level -> Bool Source # (/=) :: Level -> Level -> Bool Source #
Data Level Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Level -> c Level Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Level Source #

toConstr :: Level -> Constr Source #

dataTypeOf :: Level -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Level) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Level) Source #

gmapT :: (forall b. Data b => b -> b) -> Level -> Level Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Level -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Level -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Level -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Level -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Level -> m Level Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Level -> m Level Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Level -> m Level Source #

Ord Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Level -> Level -> Ordering Source # (<) :: Level -> Level -> Bool Source # (<=) :: Level -> Level -> Bool Source # (>) :: Level -> Level -> Bool Source # (>=) :: Level -> Level -> Bool Source # max :: Level -> Level -> Level Source # min :: Level -> Level -> Level Source #
Show Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Level -> ShowS Source # show :: Level -> String Source # showList :: [Level] -> ShowS Source #
NFData Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Level -> () Source #
Pretty Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Level -> Doc Source # prettyPrec :: Int -> Level -> Doc Source # prettyList :: [Level] -> Doc Source #
KillRange Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Level Source #
TermSize Level Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Level -> Int Source # tsize :: Level -> Sum Int Source #
DeBruijn Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Level Source # debruijnNamedVar :: String -> Int -> Level Source # deBruijnView :: Level -> Maybe Int Source #
PrecomputeFreeVars Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source #
Free Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Level -> FreeM c Source #
TermLike Level Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Level -> m Level Source # foldTerm :: Monoid m => (Term -> m) -> Level -> m Source #
GetDefs Level Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Level -> m () Source #
Free Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Level -> FreeT
EmbPrj Level Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Level -> S Int32 Source # icod_ :: Level -> S Int32 Source # value :: Int32 -> R Level Source #
PrettyTCM Level Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Level -> TCM Doc Source #
NamesIn Level Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Level -> Set QName Source #
UnFreezeMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Level -> TCM () Source #
IsInstantiatedMeta Level Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Level -> TCM Bool Source #
MentionsMeta Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Level -> Bool Source #
InstantiateFull Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Level -> ReduceM Level Source #
Normalise Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Level -> ReduceM Level Source #
Simplify Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level Source #
Reduce Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level Source # reduceB' :: Level -> ReduceM (Blocked Level) Source #
Instantiate Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Level -> ReduceM Level Source #
SynEq Level Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Level -> Level -> SynEqM (Level, Level) synEq' :: Level -> Level -> SynEqM (Level, Level)
ForceNotFree Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Level -> m Level
Match Level Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Level -> Level -> MaybeT TCM [WithOrigin Term] Source #
UsableModality Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Level -> TCM Bool Source #
UsableRelevance Level Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Level -> TCM Bool Source #
ComputeOccurrences Level Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Level -> OccM OccurrencesBuilder Source #
HasPolarity Level Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Level -> TCM [Polarity] Source #
FoldRigid Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Level -> TCM m Source #
Occurs Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Level -> TCM Level Source # metaOccurs :: MetaId -> Level -> TCM () Source #
AbsTerm Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Level -> Level Source #
Subst Term Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Level -> Level Source #
Reify Level Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Level -> TCM Expr Source # reifyWhen :: Bool -> Level -> TCM Expr Source #
Match () NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #

data Sort Source #

Sorts.

Constructors

Type Level | `Set ℓ`.
Prop Level | `Prop ℓ`.
Inf | `Setω`.
SizeUniv | `SizeUniv`, a sort inhabited by type `Size`.
PiSort Sort (Abs Sort) | Sort of the pi type.
UnivSort Sort | Sort of another sort.
MetaS !MetaId Elims |
DefS QName Elims | A postulated sort.
DummyS String | A (part of a) term or type which is only used for internal purposes. Replaces the abuse of `Prop` for a dummy sort. The `String` typically describes the location where we create this dummy, but can contain other information as well.

Instances

Eq Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Sort -> Sort -> Bool Source # (/=) :: Sort -> Sort -> Bool Source #
Data Sort Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sort -> c Sort Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sort Source #

toConstr :: Sort -> Constr Source #

dataTypeOf :: Sort -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sort) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort) Source #

gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Sort -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sort -> m Sort Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort Source #

Ord Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Sort -> Sort -> Ordering Source # (<) :: Sort -> Sort -> Bool Source # (<=) :: Sort -> Sort -> Bool Source # (>) :: Sort -> Sort -> Bool Source # (>=) :: Sort -> Sort -> Bool Source # max :: Sort -> Sort -> Sort Source # min :: Sort -> Sort -> Sort Source #
Show Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Sort -> ShowS Source # show :: Sort -> String Source # showList :: [Sort] -> ShowS Source #
NFData Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Sort -> () Source #
Pretty Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Sort -> Doc Source # prettyPrec :: Int -> Sort -> Doc Source # prettyList :: [Sort] -> Doc Source #
KillRange Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Sort Source #
TermSize Sort Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Sort -> Int Source # tsize :: Sort -> Sum Int Source #
PrecomputeFreeVars Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source #
Free Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Sort -> FreeM c Source #
Abstract Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Sort -> Sort Source #
Apply Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
TermLike Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Sort -> m Sort Source # foldTerm :: Monoid m => (Term -> m) -> Sort -> m Source #
GetDefs Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Sort -> m () Source #
Free Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Sort -> FreeT
EmbPrj Sort Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Sort -> S Int32 Source # icod_ :: Sort -> S Int32 Source # value :: Int32 -> R Sort Source #
PrettyTCM Sort Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Sort -> TCM Doc Source #
NamesIn Sort Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Sort -> Set QName Source #
UnFreezeMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Sort -> TCM () Source #
MentionsMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Sort -> Bool Source #
InstantiateFull Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort Source #
Normalise Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Sort -> ReduceM Sort Source #
Simplify Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort Source #
Reduce Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort Source # reduceB' :: Sort -> ReduceM (Blocked Sort) Source #
Instantiate Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort Source #
SynEq Sort Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Sort -> Sort -> SynEqM (Sort, Sort) synEq' :: Sort -> Sort -> SynEqM (Sort, Sort)
ForceNotFree Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Sort -> m Sort
Match Sort Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Sort -> Sort -> MaybeT TCM [WithOrigin Term] Source #
UsableModality Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Sort -> TCM Bool Source #
UsableRelevance Sort Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Sort -> TCM Bool Source #
FoldRigid Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Sort -> TCM m Source #
Occurs Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Sort -> TCM Sort Source # metaOccurs :: MetaId -> Sort -> TCM () Source #
AbsTerm Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Sort -> Sort Source #
Subst Term Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Sort -> Sort Source #
Reify Sort Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Sort -> TCM Expr Source # reifyWhen :: Bool -> Sort -> TCM Expr Source #
Match () NLPat Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Sort -> NLM () Source #
PatternFrom () Sort NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPat Source #

type Telescope = Tele (Dom Type) 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 # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Tele a -> Tele b Source # (<$) :: a -> Tele b -> Tele a Source #
Foldable Tele Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Tele m -> m Source #

foldMap :: Monoid m => (a -> m) -> Tele a -> m Source #

foldr :: (a -> b -> b) -> b -> Tele a -> b Source #

foldr' :: (a -> b -> b) -> b -> Tele a -> b Source #

foldl :: (b -> a -> b) -> b -> Tele a -> b Source #

foldl' :: (b -> a -> b) -> b -> Tele a -> b Source #

foldr1 :: (a -> a -> a) -> Tele a -> a Source #

foldl1 :: (a -> a -> a) -> Tele a -> a Source #

toList :: Tele a -> [a] Source #

null :: Tele a -> Bool Source #

length :: Tele a -> Int Source #

elem :: Eq a => a -> Tele a -> Bool Source #

maximum :: Ord a => Tele a -> a Source #

minimum :: Ord a => Tele a -> a Source #

sum :: Num a => Tele a -> a Source #

product :: Num a => Tele a -> a Source #

Traversable Tele Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Tele a -> f (Tele b) Source # sequenceA :: Applicative f => Tele (f a) -> f (Tele a) Source # mapM :: Monad m => (a -> m b) -> Tele a -> m (Tele b) Source # sequence :: Monad m => Tele (m a) -> m (Tele a) Source #
TelToArgs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc Source #
TeleNoAbs Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
AddContext Telescope Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Instantiate Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Reify Telescope Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope Source # reifyWhen :: Bool -> Telescope0 -> TCM Telescope Source #
Subst t a => Subst t (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Tele a -> Tele a Source #
(Subst t a, Eq a) => Eq (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Tele a -> Tele a -> Bool Source # (/=) :: Tele a -> Tele a -> Bool Source #
Data a => Data (Tele a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tele a -> c (Tele a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Tele a) Source #

toConstr :: Tele a -> Constr Source #

dataTypeOf :: Tele a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Tele a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Tele a -> Tele a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Tele a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Tele a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) Source #

(Subst t a, Ord a) => Ord (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Tele a -> Tele a -> Ordering Source # (<) :: Tele a -> Tele a -> Bool Source # (<=) :: Tele a -> Tele a -> Bool Source # (>) :: Tele a -> Tele a -> Bool Source # (>=) :: Tele a -> Tele a -> Bool Source # max :: Tele a -> Tele a -> Tele a Source # min :: Tele a -> Tele a -> Tele a Source #
Show a => Show (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Tele a -> ShowS Source # show :: Tele a -> String Source # showList :: [Tele a] -> ShowS Source #
Null (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods empty :: Tele a Source # null :: Tele a -> Bool Source #
Pretty a => Pretty (Tele (Dom a)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Tele (Dom a) -> Doc Source # prettyPrec :: Int -> Tele (Dom a) -> Doc Source # prettyList :: [Tele (Dom a)] -> Doc Source #
Sized (Tele a) Source # | The size of a telescope is its length (as a list).
Instance details Defined in Agda.Syntax.Internal Methods size :: Tele a -> Int Source #
KillRange a => KillRange (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Tele a) Source #
Free a => Free (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Tele a -> FreeM c Source #
Subst Term a => Apply (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Tele a -> Args -> Tele a Source # applyE :: Tele a -> Elims -> Tele a Source #
TermLike a => TermLike (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Tele a -> m (Tele a) Source # foldTerm :: Monoid m => (Term -> m) -> Tele a -> m Source #
Free a => Free (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Tele a -> FreeT
EmbPrj a => EmbPrj (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Tele a -> S Int32 Source # icod_ :: Tele a -> S Int32 Source # value :: Int32 -> R (Tele a) Source #
NamesIn a => NamesIn (Tele a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Tele a -> Set QName Source #
AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a Source # contextSize :: KeepNames Telescope -> Nat Source #
MentionsMeta a => MentionsMeta (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Tele a -> Bool Source #
(Subst t a, InstantiateFull a) => InstantiateFull (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Tele a -> ReduceM (Tele a) Source #
(Subst t a, Normalise a) => Normalise (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Tele a -> ReduceM (Tele a) Source #
(Subst t a, Simplify a) => Simplify (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Tele a -> ReduceM (Tele a) Source #
ComputeOccurrences a => ComputeOccurrences (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Tele a -> OccM OccurrencesBuilder 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 # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Dom a) Source # getSort :: Dom a -> Sort Source #
LensSort a => LensSort (Arg a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Arg a) Source # getSort :: Arg a -> Sort Source #
LensSort (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Type' a) Source # getSort :: Type' a -> Sort Source #
LensSort a => LensSort (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Abs a) Source # getSort :: Abs a -> Sort Source #

type Type = Type' Term Source #

data Type' a Source #

Types are terms with a sort annotation.

Constructors

El |

Fields

- _getSort :: Sort
- unEl :: a

Instances

Functor Type' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Type' a -> Type' b Source # (<$) :: a -> Type' b -> Type' a Source #
Foldable Type' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Type' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Type' a -> m Source #

foldr :: (a -> b -> b) -> b -> Type' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Type' a -> b Source #

foldl :: (b -> a -> b) -> b -> Type' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Type' a -> b Source #

foldr1 :: (a -> a -> a) -> Type' a -> a Source #

foldl1 :: (a -> a -> a) -> Type' a -> a Source #

toList :: Type' a -> [a] Source #

null :: Type' a -> Bool Source #

length :: Type' a -> Int Source #

elem :: Eq a => a -> Type' a -> Bool Source #

maximum :: Ord a => Type' a -> a Source #

minimum :: Ord a => Type' a -> a Source #

sum :: Num a => Type' a -> a Source #

product :: Num a => Type' a -> a Source #

Traversable Type' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Type' a -> f (Type' b) Source # sequenceA :: Applicative f => Type' (f a) -> f (Type' a) Source # mapM :: Monad m => (a -> m b) -> Type' a -> m (Type' b) Source # sequence :: Monad m => Type' (m a) -> m (Type' a) Source #
NFData Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () Source #
Decoration Type' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverseF :: Functor m => (a -> m b) -> Type' a -> m (Type' b) Source # distributeF :: Functor m => Type' (m a) -> m (Type' a) Source #
Pretty Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source # prettyList :: [Type] -> Doc Source #
TelToArgs ListTel Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
PrecomputeFreeVars Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Type Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type Source #
TermLike Type Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source # foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #
GetDefs Type Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () Source #
Free Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Type -> FreeT
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc Source #
PrettyTCM Type Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type -> TCM Doc Source #
TeleNoAbs ListTel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
AddContext Telescope Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
UnFreezeMeta Type Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Type -> TCM () Source #
MentionsMeta Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Type -> Bool Source #
Normalise Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type -> ReduceM Type Source #
Simplify Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type -> ReduceM Type Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reduce Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Instantiate Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Instantiate Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type -> ReduceM Type Source #
SynEq Type Source # | Syntactic equality ignores sorts.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
ForceNotFree Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type
ComputeOccurrences Type Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
HasPolarity Type Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Type -> TCM [Polarity] Source #
FoldRigid Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m Source #
Occurs Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
ToTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> Term) Source # toTermR :: TCM (Type -> ReduceM Term) Source #
PrimTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term Source #
AbsTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type Source #
Reify Telescope Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope Source # reifyWhen :: Bool -> Telescope0 -> TCM Telescope Source #
Reify Type Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Match () NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #
Match Type NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #
PatternFrom () Type NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #
PatternFrom Type Term NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Subst Term a => Subst Term (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Type' a -> Type' a Source #
Conversion MOT (Exp O) Type Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Eq a => Eq (Type' a) Source # | Syntactic `Type` equality, ignores sort annotations.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Type' a -> Type' a -> Bool Source # (/=) :: Type' a -> Type' a -> Bool Source #
Data a => Data (Type' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type' a -> c (Type' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Type' a) Source #

toConstr :: Type' a -> Constr Source #

dataTypeOf :: Type' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Type' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Type' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Type' a -> Type' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Type' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type' a -> m (Type' a) Source #

Ord a => Ord (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Type' a -> Type' a -> Ordering Source # (<) :: Type' a -> Type' a -> Bool Source # (<=) :: Type' a -> Type' a -> Bool Source # (>) :: Type' a -> Type' a -> Bool Source # (>=) :: Type' a -> Type' a -> Bool Source # max :: Type' a -> Type' a -> Type' a Source # min :: Type' a -> Type' a -> Type' a Source #
Show a => Show (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Type' a -> ShowS Source # show :: Type' a -> String Source # showList :: [Type' a] -> ShowS Source #
KillRange a => KillRange (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Type' a) Source #
SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
LensSort (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Type' a) Source # getSort :: Type' a -> Sort Source #
Free a => Free (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Type' a -> FreeM c Source #
EmbPrj a => EmbPrj (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Type' a -> S Int32 Source # icod_ :: Type' a -> S Int32 Source # value :: Int32 -> R (Type' a) Source #
PrettyTCM (Type' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type' NLPat -> TCM Doc Source #
NamesIn a => NamesIn (Type' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Type' a -> Set QName Source #
IsSizeType a => IsSizeType (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Type' a -> TCM (Maybe BoundedSize) Source #
AddContext (Dom (String, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a Source # contextSize :: Dom Type -> Nat Source #
AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a Source # contextSize :: KeepNames Telescope -> Nat Source #
InstantiateFull a => InstantiateFull (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Type' a -> ReduceM (Type' a) Source #
UsableRelevance a => UsableModality (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Type' a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Type' a -> TCM Bool Source #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #
UniverseBi ([Type], [Clause]) Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] Source #
UniverseBi ([Type], [Clause]) Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Term] Source #
PatternFrom (Type, Term) Elims [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #
Match (Type, Term) [Elim' NLPat] Elims Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () 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 # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Abs a -> Abs b Source # (<$) :: a -> Abs b -> Abs a Source #
Foldable Abs Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Abs m -> m Source #

foldMap :: Monoid m => (a -> m) -> Abs a -> m Source #

foldr :: (a -> b -> b) -> b -> Abs a -> b Source #

foldr' :: (a -> b -> b) -> b -> Abs a -> b Source #

foldl :: (b -> a -> b) -> b -> Abs a -> b Source #

foldl' :: (b -> a -> b) -> b -> Abs a -> b Source #

foldr1 :: (a -> a -> a) -> Abs a -> a Source #

foldl1 :: (a -> a -> a) -> Abs a -> a Source #

toList :: Abs a -> [a] Source #

null :: Abs a -> Bool Source #

length :: Abs a -> Int Source #

elem :: Eq a => a -> Abs a -> Bool Source #

maximum :: Ord a => Abs a -> a Source #

minimum :: Ord a => Abs a -> a Source #

sum :: Num a => Abs a -> a Source #

product :: Num a => Abs a -> a Source #

Traversable Abs Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Abs a -> f (Abs b) Source # sequenceA :: Applicative f => Abs (f a) -> f (Abs a) Source # mapM :: Monad m => (a -> m b) -> Abs a -> m (Abs b) Source # sequence :: Monad m => Abs (m a) -> m (Abs a) Source #
Decoration Abs Source # |
Instance details Defined in Agda.Syntax.Internal 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 # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: String -> Abs b -> String Source #
Suggest Name (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Name -> Abs b -> String Source #
Subst t a => Subst t (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Abs a -> Abs a Source #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) Source #
(Subst t a, Eq a) => Eq (Abs a) Source # | Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Abs a -> Abs a -> Bool Source # (/=) :: Abs a -> Abs a -> Bool Source #
Data a => Data (Abs a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Abs a -> c (Abs a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Abs a) Source #

toConstr :: Abs a -> Constr Source #

dataTypeOf :: Abs a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Abs a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Abs a -> Abs a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Abs a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Abs a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) Source #

(Subst t a, Ord a) => Ord (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Abs a -> Abs a -> Ordering Source # (<) :: Abs a -> Abs a -> Bool Source # (<=) :: Abs a -> Abs a -> Bool Source # (>) :: Abs a -> Abs a -> Bool Source # (>=) :: Abs a -> Abs a -> Bool Source # max :: Abs a -> Abs a -> Abs a Source # min :: Abs a -> Abs a -> Abs a Source #
Show a => Show (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Abs a -> ShowS Source # show :: Abs a -> String Source # showList :: [Abs a] -> ShowS Source #
Sized a => Sized (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods size :: Abs a -> Int Source #
KillRange a => KillRange (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) Source #
LensSort a => LensSort (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods lensSort :: Lens' Sort (Abs a) Source # getSort :: Abs a -> Sort Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Abs a -> FV (Abs a) Source #
Free a => Free (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Abs a -> FreeM c Source #
TermLike a => TermLike (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Abs a -> m (Abs a) Source # foldTerm :: Monoid m => (Term -> m) -> Abs a -> m Source #
GetDefs a => GetDefs (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Abs a -> m () Source #
Free a => Free (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Abs a -> FreeT
EmbPrj a => EmbPrj (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Abs a -> S Int32 Source # icod_ :: Abs a -> S Int32 Source # value :: Int32 -> R (Abs a) Source #
NamesIn a => NamesIn (Abs a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Abs a -> Set QName Source #
UnFreezeMeta a => UnFreezeMeta (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Abs a -> TCM () Source #
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising.
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Abs a -> TCM Bool Source #
MentionsMeta t => MentionsMeta (Abs t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Abs t -> Bool Source #
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Normalise a) => Normalise (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Simplify a) => Simplify (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Abs a -> ReduceM (Abs a) Source #
(Subst t a, Reduce a) => Reduce (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Abs a -> ReduceM (Abs a) Source # reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #
Instantiate t => Instantiate (Abs t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Abs t -> ReduceM (Abs t) Source #
(Subst t a, SynEq a) => SynEq (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a) synEq' :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)
(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a)
(Subst t a, UsableModality a) => UsableModality (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Abs a -> TCM Bool Source #
(Subst t a, UsableRelevance a) => UsableRelevance (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Abs a -> TCM Bool Source #
ComputeOccurrences a => ComputeOccurrences (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Abs a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Abs a -> TCM [Polarity] Source #
(Subst t a, FoldRigid a) => FoldRigid (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Abs a -> TCM m Source #
(Occurs a, Subst t a) => Occurs (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Abs a -> TCM (Abs a) Source # metaOccurs :: MetaId -> Abs a -> TCM () Source #
(Subst Term a, AbsTerm a) => AbsTerm (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Abs a -> Abs a Source #
Suggest (Abs a) (Abs b) Source # |
Instance details Defined in Agda.Syntax.Internal Methods suggest :: Abs a -> Abs b -> String Source #
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Abs i -> TCM (Name, a) Source # reifyWhen :: Bool -> Abs i -> TCM (Name, a) Source #

type ArgName = String Source #

Names in binders and arguments.

type Elims Source #

Arguments

= [Elim] | eliminations ordered left-to-right.

type Elim = Elim' Term 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.
IApply a a a | IApply x y r, x and y are the endpoints

Instances

Functor Elim' Source # |
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Elim' a -> Elim' b Source # (<$) :: a -> Elim' b -> Elim' a Source #
Foldable Elim' Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Elim' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Elim' a -> m Source #

foldr :: (a -> b -> b) -> b -> Elim' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Elim' a -> b Source #

foldl :: (b -> a -> b) -> b -> Elim' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Elim' a -> b Source #

foldr1 :: (a -> a -> a) -> Elim' a -> a Source #

foldl1 :: (a -> a -> a) -> Elim' a -> a Source #

toList :: Elim' a -> [a] Source #

null :: Elim' a -> Bool Source #

length :: Elim' a -> Int Source #

elem :: Eq a => a -> Elim' a -> Bool Source #

maximum :: Ord a => Elim' a -> a Source #

minimum :: Ord a => Elim' a -> a Source #

sum :: Num a => Elim' a -> a Source #

product :: Num a => Elim' a -> a Source #

Traversable Elim' Source # |
Instance details Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Elim' a -> f (Elim' b) Source # sequenceA :: Applicative f => Elim' (f a) -> f (Elim' a) Source # mapM :: Monad m => (a -> m b) -> Elim' a -> m (Elim' b) Source # sequence :: Monad m => Elim' (m a) -> m (Elim' a) Source #
IsProjElim Elim Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source #
PrettyTCM Elim Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim -> TCM Doc Source #
MentionsMeta Elim Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Elim -> Bool Source #
Normalise Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim -> ReduceM Elim Source #
Simplify Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim -> ReduceM Elim Source #
Reduce Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Instantiate Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim -> ReduceM Elim Source #
IsPrefixOf Elims Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
UniverseBi Elims Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Pattern] Source #
UniverseBi Elims Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Term] Source #
Subst t a => Subst t (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Elim' a -> Elim' a Source #
(Subst t a, Eq a) => Eq (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Elim' a -> Elim' a -> Bool Source # (/=) :: Elim' a -> Elim' a -> Bool Source #
Data a => Data (Elim' a) Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Elim' a -> c (Elim' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Elim' a) Source #

toConstr :: Elim' a -> Constr Source #

dataTypeOf :: Elim' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Elim' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> Elim' a -> Elim' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Elim' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Elim' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) Source #

(Subst t a, Ord a) => Ord (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Elim' a -> Elim' a -> Ordering Source # (<) :: Elim' a -> Elim' a -> Bool Source # (<=) :: Elim' a -> Elim' a -> Bool Source # (>) :: Elim' a -> Elim' a -> Bool Source # (>=) :: Elim' a -> Elim' a -> Bool Source # max :: Elim' a -> Elim' a -> Elim' a Source # min :: Elim' a -> Elim' a -> Elim' a Source #
Show a => Show (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Elim' a -> ShowS Source # show :: Elim' a -> String Source # showList :: [Elim' a] -> ShowS Source #
NFData a => NFData (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Elim' a -> () Source #
Pretty tm => Pretty (Elim' tm) Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Elim' tm -> Doc Source # prettyPrec :: Int -> Elim' tm -> Doc Source # prettyList :: [Elim' tm] -> Doc Source #
KillRange a => KillRange (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Elim' a) Source #
LensOrigin (Elim' a) Source # | This instance cheats on `Proj`, use with care. `Proj`s are always assumed to be `UserWritten`, since they have no `ArgInfo`. Same for IApply
Instance details Defined in Agda.Syntax.Internal Methods getOrigin :: Elim' a -> Origin Source # setOrigin :: Origin -> Elim' a -> Elim' a Source # mapOrigin :: (Origin -> Origin) -> Elim' a -> Elim' a Source #
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Elim' a -> FV (Elim' a) Source #
Free a => Free (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Elim' a -> FreeM c Source #
TermLike a => TermLike (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source # foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #
GetDefs a => GetDefs (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Elim' a -> m () Source #
Free a => Free (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Elim' a -> FreeT
EmbPrj a => EmbPrj (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Elim' a -> S Int32 Source # icod_ :: Elim' a -> S Int32 Source # value :: Int32 -> R (Elim' a) Source #
PrettyTCM (Elim' NLPat) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' NLPat -> TCM Doc Source #
PrettyTCM (Elim' DisplayTerm) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' DisplayTerm -> TCM Doc Source #
NamesIn a => NamesIn (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Elim' a -> Set QName Source #
InstantiateFull a => InstantiateFull (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Elim' a -> ReduceM (Elim' a) Source #
SynEq a => SynEq (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a) synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)
(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)
(SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a Source #
Match a => Match (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Elim' a -> Elim' a -> MaybeT TCM [WithOrigin Term] Source #
UsableModality a => UsableModality (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Elim' a -> TCM Bool Source #
UsableRelevance a => UsableRelevance (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Elim' a -> TCM Bool Source #
ForcedVariables a => ForcedVariables (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Forcing Methods forcedVariables :: Elim' a -> [(Modality, Nat)] Source #
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Elim' a -> OccM OccurrencesBuilder Source #
HasPolarity a => HasPolarity (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Elim' a -> TCM [Polarity] Source #
FoldRigid a => FoldRigid (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Elim' a -> TCM m Source #
Occurs a => Occurs (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Elim' a -> TCM (Elim' a) Source # metaOccurs :: MetaId -> Elim' a -> TCM () Source #
AbsTerm a => AbsTerm (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Elim' a -> Elim' a Source #
PatternVarModalities a x => PatternVarModalities (Elim' a) x Source # |
Instance details Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Elim' a -> [(x, Modality)] Source #
Reify i a => Reify (Elim' i) (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Elim' i -> TCM (Elim' a) Source # reifyWhen :: Bool -> Elim' i -> TCM (Elim' a) Source #
PatternFrom (Type, Term) Elims [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #
Match (Type, Term) [Elim' NLPat] Elims Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

type ConInfo = ConOrigin 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 Elims | `c es` or `record { fs = es }` `es` allows only Apply and IApply eliminations, and IApply only for data constructors.
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`.
Dummy String | A (part of a) term or type which is only used for internal purposes. Replaces the `Sort Prop` hack. The `String` typically describes the location where we create this dummy, but can contain other information as well.

Instances

Eq Term Source # | Syntactic `Term` equality, ignores stuff below `DontCare` and sharing.
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Term -> Term -> Bool Source # (/=) :: Term -> Term -> Bool Source #
Data Term Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term Source #

toConstr :: Term -> Constr Source #

dataTypeOf :: Term -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) Source #

gmapT :: (forall b. Data b => b -> b) -> Term -> Term Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term Source #

Ord Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: Term -> Term -> Ordering Source # (<) :: Term -> Term -> Bool Source # (<=) :: Term -> Term -> Bool Source # (>) :: Term -> Term -> Bool Source # (>=) :: Term -> Term -> Bool Source # max :: Term -> Term -> Term Source # min :: Term -> Term -> Term Source #
Show Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Term -> ShowS Source # show :: Term -> String Source # showList :: [Term] -> ShowS Source #
NFData Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Type -> () Source #
NFData Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Term -> () Source #
Pretty Type Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source # prettyList :: [Type] -> Doc Source #
Pretty Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Term -> Doc Source # prettyPrec :: Int -> Term -> Doc Source # prettyList :: [Term] -> Doc Source #
Pretty CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
KillRange Substitution Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution Source #
KillRange Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Term Source #
KillRange CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses Source #
TermSize Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Term -> Int Source # tsize :: Term -> Sum Int Source #
IsProjElim Elim Source # |
Instance details Defined in Agda.Syntax.Internal Methods isProjElim :: Elim -> Maybe (ProjOrigin, QName) Source #
TelToArgs ListTel Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: ListTel -> [Arg ArgName] Source #
TelToArgs Telescope Source # |
Instance details Defined in Agda.Syntax.Internal Methods telToArgs :: Telescope -> [Arg ArgName] Source #
DeBruijn Term Source # | We can substitute `Term`s for variables.
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Term Source # debruijnNamedVar :: String -> Int -> Term Source # deBruijnView :: Term -> Maybe Int Source #
PrecomputeFreeVars Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source #
PrecomputeFreeVars Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Term -> FV Term Source #
Free Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Term -> FreeM c Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Type Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type Source #
Abstract Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Term -> Term Source #
Abstract CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Apply Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Term -> Args -> Term Source # applyE :: Term -> Elims -> Term Source #
Apply CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
TermLike Type Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Type -> m Type Source # foldTerm :: Monoid m => (Term -> m) -> Type -> m Source #
TermLike Term Source # |
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Term -> m Term Source # foldTerm :: Monoid m => (Term -> m) -> Term -> m Source #
GetDefs Type Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Type -> m () Source #
GetDefs Term Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Term -> m () Source #
Free Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Type -> FreeT
Free Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods freeVars' :: Term -> FreeT
EmbPrj Term Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Term -> S Int32 Source # icod_ :: Term -> S Int32 Source # value :: Int32 -> R Term Source #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Int32 Source # icod_ :: CompiledClauses -> S Int32 Source # value :: Int32 -> R CompiledClauses Source #
PrettyTCM Telescope Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Telescope -> TCM Doc Source #
PrettyTCM Type Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type -> TCM Doc Source #
PrettyTCM Elim Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim -> TCM Doc Source #
PrettyTCM Term Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Term -> TCM Doc Source #
NamesIn Term Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Term -> Set QName Source #
NamesIn CompiledClauses Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompiledClauses -> Set QName Source #
TeleNoAbs ListTel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #
PiApplyM Term Source # |
Instance details Defined in Agda.TypeChecking.Telescope Methods piApplyM :: MonadReduce m => Type -> Term -> m Type Source #
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Telescope -> Telescope Source #
DropArgs Term Source # | Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> Term -> Term Source #
DropArgs CompiledClauses Source # | To drop the first `n` arguments in a compiled clause, we reduce the split argument indices by `n` and drop `n` arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source #
IsSizeType Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.SizedTypes Methods isSizeType :: Term -> TCM (Maybe BoundedSize) Source #
AddContext Telescope Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Telescope -> tcm a -> tcm a Source # contextSize :: Telescope -> Nat Source #
UnFreezeMeta Type Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Type -> TCM () Source #
UnFreezeMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: Term -> TCM () Source #
IsInstantiatedMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: Term -> TCM Bool Source #
MentionsMeta Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Type -> Bool Source #
MentionsMeta Elim Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Elim -> Bool Source #
MentionsMeta Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Term -> Bool Source #
InstantiateFull Substitution Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
InstantiateFull Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Term -> ReduceM Term Source #
InstantiateFull CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source #
Normalise Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type -> ReduceM Type Source #
Normalise Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim -> ReduceM Elim Source #
Normalise Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Term -> ReduceM Term Source #
Simplify Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type -> ReduceM Type Source #
Simplify Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim -> ReduceM Elim Source #
Simplify Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Term -> ReduceM Term Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reduce Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Reduce Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Reduce Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Term -> ReduceM Term Source # reduceB' :: Term -> ReduceM (Blocked Term) Source #
Instantiate Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Telescope -> ReduceM Telescope Source #
Instantiate Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type -> ReduceM Type Source #
Instantiate Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim -> ReduceM Elim Source #
Instantiate Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Term -> ReduceM Term Source #
SynEq Type Source # | Syntactic equality ignores sorts.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Type -> Type -> SynEqM (Type, Type) synEq' :: Type -> Type -> SynEqM (Type, Type)
SynEq Term Source # | Syntactic term equality ignores `DontCare` stuff.
Instance details Defined in Agda.TypeChecking.SyntacticEquality Methods synEq :: Term -> Term -> SynEqM (Term, Term) synEq' :: Term -> Term -> SynEqM (Term, Term)
ForceNotFree Type Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Type -> m Type
ForceNotFree Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Term -> m Term
SubstWithOrigin Term Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term Source #
Match Term Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Term -> Term -> MaybeT TCM [WithOrigin Term] Source #
UsableModality Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableMod :: Modality -> Term -> TCM Bool Source #
UsableRelevance Term Source # |
Instance details Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: Relevance -> Term -> TCM Bool Source #
ForcedVariables Term Source # | Assumes that the term is in normal form.
Instance details Defined in Agda.TypeChecking.Forcing Methods forcedVariables :: Term -> [(Modality, Nat)] Source #
ComputeOccurrences Type Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Type -> OccM OccurrencesBuilder Source #
ComputeOccurrences Term Source # |
Instance details Defined in Agda.TypeChecking.Positivity Methods occurrences :: Term -> OccM OccurrencesBuilder Source #
HasPolarity Type Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Type -> TCM [Polarity] Source #
HasPolarity Term Source # |
Instance details Defined in Agda.TypeChecking.Polarity Methods polarities :: Nat -> Term -> TCM [Polarity] Source #
FoldRigid Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Type -> TCM m Source #
FoldRigid Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods foldRigid :: Monoid (TCM m) => (Nat -> TCM m) -> Term -> TCM m Source #
Occurs Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Type -> TCM Type Source # metaOccurs :: MetaId -> Type -> TCM () Source #
Occurs Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Term -> TCM Term Source # metaOccurs :: MetaId -> Term -> TCM () Source #
ToTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> Term) Source # toTermR :: TCM (Type -> ReduceM Term) Source #
ToTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Term -> Term) Source # toTermR :: TCM (Term -> ReduceM Term) Source #
PrimTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term Source #
ReduceAndEtaContract Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods reduceAndEtaContract :: Term -> TCM Term Source #
NoProjectedVar Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars Methods noProjectedVar :: Term -> Either ProjVarExc () Source #
AbsTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type Source #
AbsTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Term -> Term Source #
IsPrefixOf Elims Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
IsPrefixOf Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Term -> Term -> Maybe Elims Source #
IsPrefixOf Args Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #
UniverseBi Elims Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Pattern] Source #
UniverseBi Elims Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Elims -> [Term] Source #
UniverseBi Args Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Pattern] Source #
UniverseBi Args Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: Args -> [Term] Source #
Subst Term () Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> () -> () Source #
Subst Term String Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> String -> String Source #
Subst Term Range Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Range -> Range Source #
Subst Term QName Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods applySubst :: Substitution' Term -> QName -> QName Source #
Subst Term Name Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Name -> Name Source #
Subst Term EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView Source #
Subst Term ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo Source #
Subst Term Pattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Pattern -> Pattern Source #
Subst Term LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> LevelAtom -> LevelAtom Source #
Subst Term PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> PlusLevel -> PlusLevel Source #
Subst Term Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Level -> Level Source #
Subst Term Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Sort -> Sort Source #
Subst Term Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Term -> Term Source #
Subst Term ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq Source #
Subst Term Candidate Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate Source #
Subst Term DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm Source #
Subst Term DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm Source #
Subst Term Constraint Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Constraint -> Constraint Source #
Subst Term AbsurdPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AbsurdPattern -> AbsurdPattern Source #
Subst Term DotPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> DotPattern -> DotPattern Source #
Subst Term AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AsBinding -> AsBinding Source #
Subst Term SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint Source #
Subst Term SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeMeta -> SizeMeta Source #
Subst Term CType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods applySubst :: Substitution' Term -> CType -> CType Source #
Subst Term LType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods applySubst :: Substitution' Term -> LType -> LType Source #
Reify Telescope Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope Source # reifyWhen :: Bool -> Telescope0 -> TCM Telescope Source #
Reify Type Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Reify Term Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Term -> TCM Expr Source # reifyWhen :: Bool -> Term -> TCM Expr Source #
Match () NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #
Match Type NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #
PatternFrom () Type NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #
PatternFrom Type Term NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Subst Term a => Subst Term (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Type' a -> Type' a Source #
Subst Term (Problem a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> Problem a -> Problem a Source #
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Term -> TCM (Pattern' a) Source #
Conversion MOT (Exp O) Type Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Subst Term (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #
Eq (Substitution' Term) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution' Term -> Substitution' Term -> Bool Source # (/=) :: Substitution' Term -> Substitution' Term -> Bool Source #
Ord (Substitution' Term) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

compare :: Substitution' Term -> Substitution' Term -> Ordering Source #

(<) :: Substitution' Term -> Substitution' Term -> Bool Source #

(<=) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>) :: Substitution' Term -> Substitution' Term -> Bool Source #

(>=) :: Substitution' Term -> Substitution' Term -> Bool Source #

max :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

min :: Substitution' Term -> Substitution' Term -> Substitution' Term Source #

SgTel (Dom (ArgName, Type)) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom (ArgName, Type) -> Telescope Source #
SgTel (Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: Dom Type -> Telescope Source #
AddContext (Dom (String, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (String, Type) -> tcm a -> tcm a Source # contextSize :: Dom (String, Type) -> Nat Source #
AddContext (Dom (Name, Type)) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom (Name, Type) -> tcm a -> tcm a Source # contextSize :: Dom (Name, Type) -> Nat Source #
AddContext (Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => Dom Type -> tcm a -> tcm a Source # contextSize :: Dom Type -> Nat Source #
AddContext (KeepNames Telescope) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => KeepNames Telescope -> tcm a -> tcm a Source # contextSize :: KeepNames Telescope -> Nat Source #
SubstWithOrigin (Arg Term) Source # |
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term Source #
UniverseBi [Term] Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: [Term] -> [Term] Source #
SgTel (ArgName, Dom Type) Source # |
Instance details Defined in Agda.Syntax.Internal Methods sgTel :: (ArgName, Dom Type) -> Telescope Source #
AddContext ([NamedArg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([NamedArg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([NamedArg Name], Type) -> Nat Source #
AddContext ([Arg Name], Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Arg Name], Type) -> tcm a -> tcm a Source # contextSize :: ([Arg Name], Type) -> Nat Source #
AddContext ([WithHiding Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([WithHiding Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([WithHiding Name], Dom Type) -> Nat Source #
AddContext ([Name], Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => ([Name], Dom Type) -> tcm a -> tcm a Source # contextSize :: ([Name], Dom Type) -> Nat Source #
AddContext (String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (String, Dom Type) -> Nat Source #
AddContext (Name, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (Name, Dom Type) -> tcm a -> tcm a Source # contextSize :: (Name, Dom Type) -> Nat Source #
AddContext (KeepNames String, Dom Type) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: (MonadTCM tcm, MonadDebug tcm) => (KeepNames String, Dom Type) -> tcm a -> tcm a Source # contextSize :: (KeepNames String, Dom Type) -> Nat Source #
UniverseBi ([Type], [Clause]) Pattern Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Pattern] Source #
UniverseBi ([Type], [Clause]) Term Source # |
Instance details Defined in Agda.Syntax.Internal Methods universeBi :: ([Type], [Clause]) -> [Term] Source #
PatternFrom (Type, Term) Elims [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #
Match (Type, Term) [Elim' NLPat] Elims Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () 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 # |
Instance details Defined in Agda.Syntax.Internal Methods getConName :: ConHead -> QName Source # setConName :: QName -> ConHead -> ConHead Source # mapConName :: (QName -> QName) -> ConHead -> ConHead 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 :: [Arg QName]

  The name of the record fields. Empty list for data constructors. `Arg` is stored since the info in the constructor args might not be accurate because of subtyping (issue #2170).

Instances

Eq ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods (==) :: ConHead -> ConHead -> Bool Source # (/=) :: ConHead -> ConHead -> Bool Source #
Data ConHead Source # |

Instance details

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConHead -> c ConHead Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConHead Source #

toConstr :: ConHead -> Constr Source #

dataTypeOf :: ConHead -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConHead) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead) Source #

gmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConHead -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConHead -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead Source #

Ord ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods compare :: ConHead -> ConHead -> Ordering Source # (<) :: ConHead -> ConHead -> Bool Source # (<=) :: ConHead -> ConHead -> Bool Source # (>) :: ConHead -> ConHead -> Bool Source # (>=) :: ConHead -> ConHead -> Bool Source # max :: ConHead -> ConHead -> ConHead Source # min :: ConHead -> ConHead -> ConHead Source #
Show ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConHead -> ShowS Source # show :: ConHead -> String Source # showList :: [ConHead] -> ShowS Source #
Pretty ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods pretty :: ConHead -> Doc Source # prettyPrec :: Int -> ConHead -> Doc Source # prettyList :: [ConHead] -> Doc Source #
KillRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT ConHead Source #
SetRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods setRange :: Range -> ConHead -> ConHead Source #
HasRange ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods getRange :: ConHead -> Range Source #
LensConName ConHead Source # |
Instance details Defined in Agda.Syntax.Internal Methods getConName :: ConHead -> QName Source # setConName :: QName -> ConHead -> ConHead Source # mapConName :: (QName -> QName) -> ConHead -> ConHead Source #
EmbPrj ConHead Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConHead -> S Int32 Source # icod_ :: ConHead -> S Int32 Source # value :: Int32 -> R ConHead Source #
PrettyTCM ConHead Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ConHead -> TCM Doc Source #
NamesIn ConHead Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: ConHead -> Set QName Source #
InstantiateFull ConHead Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConHead -> ReduceM ConHead Source #

type NamedArgs = [NamedArg Term] Source #

type Args = [Arg Term] Source #

Type of argument lists.

argNameToString :: ArgName -> String Source #

stringToArgName :: String -> ArgName Source #

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

nameToArgName :: Name -> ArgName Source #

namedArgName :: NamedArg Name -> ArgName Source #

stuckOn :: Elim -> NotBlocked -> NotBlocked Source #

When trying to reduce `f es`, on match failed on one elimination `e ∈ es` that came with info `r :: NotBlocked`. `stuckOn e r` produces the new `NotBlocked` info.

`MissingClauses` must be propagated, as this is blockage that can be lifted in the future (as more clauses are added).

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

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

patVarNameToString :: PatVarName -> String Source #

nameToPatVarName :: Name -> PatVarName Source #

varP :: a -> Pattern' a Source #

dotP :: Term -> Pattern' a Source #

namedVarP :: PatVarName -> Named_ Pattern Source #

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #

absurdP :: Int -> DeBruijnPattern Source #

Make an absurd pattern with the given de Bruijn index.

noConPatternInfo :: ConPatternInfo Source #

toConPatternInfo :: ConInfo -> ConPatternInfo Source #

Build partial `ConPatternInfo` from `ConInfo`

fromConPatternInfo :: ConPatternInfo -> ConInfo Source #

Build `ConInfo` from `ConPatternInfo`.

patternOrigin :: Pattern' x -> Maybe PatOrigin Source #

Retrieve the origin of a pattern

properlyMatching :: DeBruijnPattern -> Bool Source #

Does the pattern perform a match that could fail?

isEqualityType :: EqualityView -> Bool Source #

isPathType :: PathView -> Bool Source #

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 #

var :: Nat -> Term Source #

An unapplied variable.

dontCare :: Term -> Term Source #

Add `DontCare` is it is not already a `DontCare`.

dummyTerm' :: String -> Int -> Term Source #

Aux: A dummy term to constitute a dummy termlevelsort/type.

dummyLevel' :: String -> Int -> Level Source #

Aux: A dummy level to constitute a level/sort.

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

A dummy term created at location. Note: use macro (dummyTerm "srcfullAgdaSyntaxInternal.hs" 763) !

dummyLevel :: String -> Int -> Level Source #

A dummy level created at location. Note: use macro (dummyLevel "srcfullAgdaSyntaxInternal.hs" 768) !

dummySort :: String -> Int -> Sort Source #

A dummy sort created at location. Note: use macro (dummySort "srcfullAgdaSyntaxInternal.hs" 773) !

dummyType :: String -> Int -> Type Source #

A dummy type created at location. Note: use macro (dummyType "srcfullAgdaSyntaxInternal.hs" 778) !

dummyDom :: String -> Int -> Dom Type Source #

Context entries without a type have this dummy type. Note: use macro (dummyDom "srcfullAgdaSyntaxInternal.hs" 783) !

unreducedLevel :: Term -> Level Source #

topSort :: Type Source #

Top sort (Setomega).

sort :: Sort -> Type Source #

varSort :: Int -> Sort Source #

tmSort :: Term -> Sort Source #

levelSuc :: Level -> Level Source #

mkType :: Integer -> Sort Source #

mkProp :: Integer -> Sort Source #

isSort :: Term -> Maybe Sort Source #

impossibleTerm :: String -> Int -> Term 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 #

telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope Source #

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

telToList :: Tele (Dom t) -> [Dom (ArgName, t)] Source #

Convert a telescope to its list form.

listTel :: Lens' ListTel Telescope Source #

Lens to edit a `Telescope` as a list.

blockingMeta :: Blocked t -> Maybe MetaId Source #

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

notBlocked :: a -> Blocked a Source #

stripDontCare :: Term -> Term Source #

Removing a topmost `DontCare` constructor.

arity :: Type -> Nat Source #

Doesn't do any reduction.

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.

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

Drop `Apply` constructor. (Safe)

isApplyElim' :: Empty -> Elim' a -> Arg a Source #

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

Drop `Apply` constructors. (Safe)

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

Split at first non-`Apply`

argsFromElims :: Elims -> Args Source #

Discards `Proj f` entries.

allProjElims :: Elims -> Maybe [(ProjOrigin, QName)] Source #

Drop `Proj` constructors. (Safe)

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

module Agda.Syntax.Abstract.Name

newtype MetaId Source #

A meta variable identifier is just a natural number.

Constructors

MetaId |

Fields

- metaId :: Nat

Instances

Enum MetaId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

succ :: MetaId -> MetaId Source #

pred :: MetaId -> MetaId Source #

toEnum :: Int -> MetaId Source #

fromEnum :: MetaId -> Int Source #

enumFrom :: MetaId -> [MetaId] Source #

enumFromThen :: MetaId -> MetaId -> [MetaId] Source #

enumFromTo :: MetaId -> MetaId -> [MetaId] Source #

enumFromThenTo :: MetaId -> MetaId -> MetaId -> [MetaId] Source #

Eq MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: MetaId -> MetaId -> Bool Source # (/=) :: MetaId -> MetaId -> Bool Source #
Integral MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods quot :: MetaId -> MetaId -> MetaId Source # rem :: MetaId -> MetaId -> MetaId Source # div :: MetaId -> MetaId -> MetaId Source # mod :: MetaId -> MetaId -> MetaId Source # quotRem :: MetaId -> MetaId -> (MetaId, MetaId) Source # divMod :: MetaId -> MetaId -> (MetaId, MetaId) Source # toInteger :: MetaId -> Integer Source #
Data MetaId Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId Source #

toConstr :: MetaId -> Constr Source #

dataTypeOf :: MetaId -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) Source #

gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId Source #

Num MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods (+) :: MetaId -> MetaId -> MetaId Source # (-) :: MetaId -> MetaId -> MetaId Source # (*) :: MetaId -> MetaId -> MetaId Source # negate :: MetaId -> MetaId Source # abs :: MetaId -> MetaId Source # signum :: MetaId -> MetaId Source # fromInteger :: Integer -> MetaId Source #
Ord MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods compare :: MetaId -> MetaId -> Ordering Source # (<) :: MetaId -> MetaId -> Bool Source # (<=) :: MetaId -> MetaId -> Bool Source # (>) :: MetaId -> MetaId -> Bool Source # (>=) :: MetaId -> MetaId -> Bool Source # max :: MetaId -> MetaId -> MetaId Source # min :: MetaId -> MetaId -> MetaId Source #
Real MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational Source #
Show MetaId Source # | Show non-record version of this newtype.
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> MetaId -> ShowS Source # show :: MetaId -> String Source # showList :: [MetaId] -> ShowS Source #
NFData MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods rnf :: MetaId -> () Source #
Pretty MetaId Source # |
Instance details Defined in Agda.Syntax.Common Methods pretty :: MetaId -> Doc Source # prettyPrec :: Int -> MetaId -> Doc Source # prettyList :: [MetaId] -> Doc Source #
GetDefs MetaId Source # |
Instance details Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source #
HasFresh MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MetaId TCState Source # nextFresh' :: MetaId -> MetaId Source #
EmbPrj MetaId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: MetaId -> S Int32 Source # icod_ :: MetaId -> S Int32 Source # value :: Int32 -> R MetaId Source #
PrettyTCM MetaId Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MetaId -> TCM Doc Source #
UnFreezeMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MetaId -> TCM () Source #
IsInstantiatedMeta MetaId Source # |
Instance details Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: MetaId -> TCM Bool Source #
FromTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
ToTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> Term) Source # toTermR :: TCM (MetaId -> ReduceM Term) Source #
PrimTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term Source #
Unquote MetaId Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM MetaId Source #
Reify MetaId Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MetaId -> TCM Expr Source # reifyWhen :: Bool -> MetaId -> TCM Expr Source #