Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Clause 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 Definition 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 DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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 #

TermSubst 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

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

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 [t] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

applyE :: [t] -> Elims -> [t] 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 (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 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 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 Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract PrimFun 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 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 System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Maybe t -> Maybe 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 [t] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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 (SubstArg a) => Subst a where Source #

Apply a substitution.

Minimal complete definition

Nothing

Associated Types

type SubstArg a Source #

Methods

applySubst :: Substitution' (SubstArg a) -> a -> a Source #

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

Instances

Instances details
Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq Source #

Subst Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Name Source #

Subst QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg QName Source #

Subst BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg BraveTerm Source #

Subst ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo Source #

Subst DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern Source #

Subst EqualityTypeData Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityTypeData Source #

Subst EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityView Source #

Subst Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Pattern Source #

Subst Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term Source #

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range Source #

Subst TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TAlt Source #

Subst TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TTerm Source #

Subst SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern Source #

Subst Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Candidate Source #

Subst CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg CompareAs Source #

Subst Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Constraint Source #

Subst DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DisplayForm Source #

Subst DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DisplayTerm Source #

Subst LetBinding Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg LetBinding Source #

Subst NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPSort Source #

Subst NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPType Source #

Subst NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPat Source #

Subst RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg RewriteRule Source #

Subst CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg CType Source #

Subst LType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg LType Source #

Subst AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AbsurdPattern Source #

Subst AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AsBinding Source #

Subst DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg DotPattern Source #

Subst SizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint Source #

Subst SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeMeta Source #

Subst () Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg () Source #

Methods

applySubst :: Substitution' (SubstArg ()) -> () -> () Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Arg a) Source #

Methods

applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (WithHiding a) Source #

Subst a => Subst (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a) Source #

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Level' a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (PlusLevel' a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Sort' a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) Source #

Subst a => Subst (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Elim' a) Source #

Subst t => Subst (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

Associated Types

type SubstArg (SingleLevel' t) Source #

Subst a => Subst (AbsN a) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Associated Types

type SubstArg (AbsN a) Source #

Subst (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg (Problem a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Maybe a) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg [a] Source #

Methods

applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a] Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Named name a) Source #

Methods

applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b) Source #

Methods

applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Type'' a b) Source #

Methods

applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta) Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Map k a) Source #

Methods

applySubst :: Substitution' (SubstArg (Map k a)) -> Map k a -> Map k a Source #

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b) Source #

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b, c) Source #

Methods

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b, c, d) Source #

Methods

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

type SubstWith t a = (Subst a, SubstArg a ~ t) Source #

Simple constraint alias for a Subst instance a with arg type t.

type EndoSubst a = SubstWith a a Source #

Subst instance whose agument type is itself

type TermSubst a = SubstWith Term a Source #

Subst instance whose argument type is Term

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

Raise de Bruijn index, i.e. weakening

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

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

Replace de Bruijn index i by a Term in something.

strengthen :: Subst a => Impossible -> a -> a Source #

substUnder :: Subst a => Nat -> SubstArg a -> 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 :: EndoSubst 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 :: EndoSubst 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 => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a Source #

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

parallelS :: DeBruijn a => [a] -> Substitution' a Source #

       Γ ⊢ reverse vs : Δ
     -----------------------------
       Γ ⊢ parallelS vs ρ : Γ, Δ
  

Note the Γ in Γ, Δ.

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

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

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

A "smart" variant of Strengthen. If strengthenS is applied to a substitution with an outermost Strengthen constructor, then the "error message" of that constructor is discarded in favour of the Impossible argument of this function.

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

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

raiseFromS :: Nat -> Nat -> Substitution' a Source #

Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ

Functions on abstractions

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

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst a => Abs a -> SubstArg a -> 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 a => Impossible -> Abs a -> a Source #

Instantiate an abstraction that doesn't use its argument.

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

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

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

underAbs :: Subst 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 :: TermSubst 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.