Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Substitute.Class

Synopsis

Application

class Apply t where Source #

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Minimal complete definition

applyE

Methods

apply :: t -> Args -> t Source #

applyE :: t -> Elims -> t Source #

Instances

Instances details
Apply Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Sort -> Args -> Sort Source #

applyE :: Sort -> Elims -> Sort 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

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Defn -> Args -> Defn Source #

applyE :: Defn -> Elims -> Defn Source #

Apply ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply t => Apply [t] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [t] -> Args -> [t] Source #

applyE :: [t] -> Elims -> [t] Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply t => Apply (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Maybe t -> Args -> Maybe t Source #

applyE :: Maybe t -> Elims -> Maybe t Source #

Apply t => Apply (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Maybe t -> Args -> Maybe t Source #

applyE :: Maybe t -> Elims -> Maybe t Source #

DoDrop a => Apply (Drop a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Drop a -> Args -> Drop a Source #

applyE :: Drop a -> Elims -> Drop 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 #

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 #

Apply a => Apply (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Case a -> Args -> Case a Source #

applyE :: Case a -> Elims -> Case a Source #

Apply a => Apply (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

(Apply a, Apply b) => Apply (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: (a, b) -> Args -> (a, b) Source #

applyE :: (a, b) -> Elims -> (a, b) Source #

Apply v => Apply (Map k v) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Map k v -> Args -> Map k v Source #

applyE :: Map k v -> Elims -> Map k v Source #

Apply v => Apply (HashMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: HashMap k v -> Args -> HashMap k v Source #

applyE :: HashMap k v -> Elims -> HashMap k v Source #

(Apply a, Apply b, Apply c) => Apply (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: (a, b, c) -> Args -> (a, b, c) Source #

applyE :: (a, b, c) -> Elims -> (a, b, c) Source #

applys :: Apply t => t -> [Term] -> t Source #

Apply to some default arguments.

apply1 :: Apply t => t -> Term -> t Source #

Apply to a single default argument.

Abstraction

class Abstract t where Source #

(abstract args v) apply args --> v[args].

Methods

abstract :: Telescope -> t -> t Source #

Instances

Instances details
Abstract Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract RewriteRule Source #

tel ⊢ (Γ ⊢ lhs ↦ rhs : t) becomes tel, Γ ⊢ lhs ↦ rhs : t) we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.

Instance details

Defined in Agda.TypeChecking.Substitute

Abstract t => Abstract [t] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> [t] -> [t] Source #

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract t => Abstract (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Maybe t -> Maybe t Source #

DoDrop a => Abstract (Drop a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Drop a -> Drop a Source #

Abstract a => Abstract (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Case a -> Case a Source #

Abstract a => Abstract (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract v => Abstract (Map k v) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Map k v -> Map k v Source #

Abstract v => Abstract (HashMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> HashMap k v -> HashMap k v Source #

Substitution and shifting/weakening/strengthening

class DeBruijn t => Subst t a | a -> t where Source #

Apply a substitution.

Minimal complete definition

Nothing

Methods

applySubst :: Substitution' t -> a -> a Source #

default applySubst :: (a ~ f b, Functor f, Subst t b) => Substitution' t -> a -> a Source #

Instances

Instances details
Subst TTerm TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Subst TTerm TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Subst DeBruijnPattern DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst BraveTerm BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Subst Term Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Subst Term Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Subst Term AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst Term SizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst Term SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst Term CType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Subst Term LType Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Data

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst SplitPattern SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Subst t a => Subst t (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst t a => Subst t [a] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> [a] -> [a] Source #

Subst t a => Subst t (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Maybe a -> Maybe a Source #

Subst t a => Subst t (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Arg a -> Arg a 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 #

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 => Subst t (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Tele a -> Tele a Source #

Subst t a => Subst t (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst t a => Subst t (LevelAtom' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst t a => Subst t (PlusLevel' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst t a => Subst t (Level' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

(Coercible a Term, Subst t a) => Subst t (Sort' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Sort' a -> Sort' a Source #

Subst a a => Subst a (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

(Subst t a, Subst t b) => Subst t (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> (a, b) -> (a, b) Source #

(Ord k, Subst t a) => Subst t (Map k a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Map k a -> Map k a Source #

(Subst t a, Subst t b) => Subst t (Dom' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Dom' a b -> Dom' a b Source #

Subst t a => Subst t (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Named name a -> Named name a Source #

(Coercible a Term, Subst t a, Subst t b) => Subst t (Type'' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> Type'' a b -> Type'' a b Source #

Subst Term (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> (a, b, c) -> (a, b, c) Source #

(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d) Source #

raise :: Subst t a => Nat -> a -> a Source #

Raise de Bruijn index, i.e. weakening

raiseFrom :: Subst t a => Nat -> Nat -> a -> a Source #

subst :: Subst t a => Int -> t -> a -> a Source #

Replace de Bruijn index i by a Term in something.

strengthen :: Subst t a => Empty -> a -> a Source #

substUnder :: Subst t a => Nat -> t -> a -> a Source #

Replace what is now de Bruijn index 0, but go under n binders. substUnder n u == subst n (raise n u).

Identity instances

Explicit substitutions

singletonS :: DeBruijn a => Int -> a -> Substitution' a Source #

To replace index n by term u, do applySubst (singletonS n u). Γ, Δ ⊢ u : A --------------------------------- Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ

inplaceS :: Subst a a => Int -> a -> Substitution' a Source #

Single substitution without disturbing any deBruijn indices. Γ, A, Δ ⊢ u : A --------------------------------- Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ

liftS :: Int -> Substitution' a -> Substitution' a Source #

Lift a substitution under k binders.

dropS :: Int -> Substitution' a -> Substitution' a Source #

        Γ ⊢ ρ : Δ, Ψ
     -------------------
     Γ ⊢ dropS |Ψ| ρ : Δ
  

composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a Source #

applySubst (ρ composeS σ) v == applySubst ρ (applySubst σ v)

(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4 Source #

prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a Source #

     Γ ⊢ ρ : Δ  Γ ⊢ reverse vs : Θ
     ----------------------------- (treating Nothing as having any type)
       Γ ⊢ prependS vs ρ : Δ, Θ
  

strengthenS :: Empty -> Int -> Substitution' a Source #

Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ

lookupS :: Subst a a => Substitution' a -> Nat -> a Source #

listS :: Subst a a => [(Int, a)] -> Substitution' a Source #

lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.

Functions on abstractions

absApp :: Subst t a => Abs a -> t -> a Source #

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst t a => Abs a -> t -> a Source #

Instantiate an abstraction. Lazy in the term, which allow it to be IMPOSSIBLE in the case where the variable shouldn't be used but we cannot use noabsApp. Used in Apply.

noabsApp :: Subst t a => Empty -> Abs a -> a Source #

Instantiate an abstraction that doesn't use its argument.

absBody :: Subst t a => Abs a -> a Source #

mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a Source #

reAbs :: (Subst t a, Free a) => Abs a -> Abs a Source #

underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b Source #

underAbs k a b applies k to a and the content of abstraction b and puts the abstraction back. a is raised if abstraction was proper such that at point of application of k and the content of b are at the same context. Precondition: a and b are at the same context at call time.

underLambdas :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term Source #

underLambdas n k a b drops n initial Lams from b, performs operation k on a and the body of b, and puts the Lams back. a is raised correctly according to the number of abstractions.