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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Substitute

Contents

Synopsis

Application

class Apply t where

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

Minimal complete definition

Nothing

Methods

apply :: t -> Args -> t

applyE :: t -> Elims -> t

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

Apply to a single argument.

canProject :: QName -> Term -> Maybe (Arg Term)

If $v$ is a record value, canProject f v returns its field f.

conApp :: ConHead -> Args -> Elims -> Term

Eliminate a constructed term.

defApp :: QName -> Elims -> Elims -> Term

defApp f us vs applies Def f us to further arguments vs, eliminating top projection redexes. If us is not empty, we cannot have a projection redex, since the record argument is the first one.

piApply :: Type -> Args -> Type

The type must contain the right number of pis without have to perform any reduction.

Abstraction

class Abstract t where

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

Methods

abstract :: Telescope -> t -> t

Instances

Abstract Permutation 
Abstract ClauseBody 
Abstract Clause 
Abstract Sort 
Abstract Telescope 
Abstract Type 
Abstract Term 
Abstract CompiledClauses 
Abstract FunctionInverse 
Abstract PrimFun 
Abstract Defn 
Abstract Projection 
Abstract Definition 
Abstract RewriteRule

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

Abstract t => Abstract [t] 
Abstract [Occurrence] 
Abstract [Polarity] 
Abstract t => Abstract (Maybe t) 
DoDrop a => Abstract (Drop a) 
Abstract a => Abstract (Case a) 
Abstract a => Abstract (WithArity a) 
Abstract v => Abstract (Map k v) 

abstractArgs :: Abstract a => Args -> a -> a

Explicit substitutions

composeS :: Substitution -> Substitution -> Substitution

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

(++#) :: [Term] -> Substitution -> Substitution infixr 4

Substitution and raisingshiftingweakening

raise :: Subst t => Nat -> t -> t

raiseFrom :: Subst t => Nat -> Nat -> t -> t

subst :: Subst t => Term -> t -> t

strengthen :: Subst t => Empty -> t -> t

substUnder :: Subst t => Nat -> Term -> t -> t

Telescopes

data TelV a

Constructors

TelV 

Fields

theTel :: Tele (Dom a)
 
theCore :: a
 

Instances

Functor TelV 
(Eq a, Subst a) => Eq (TelV a) 
(Ord a, Subst a) => Ord (TelV a) 
Show a => Show (TelV a) 

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

bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a

Turn a typed binding (x1 .. xn : A) into a telescope.

bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a

Turn a typed binding (x1 .. xn : A) into a telescope.

mkPi :: Dom (ArgName, Type) -> Type -> Type

mkPi dom t = telePi (telFromList [dom]) t

telePi :: Telescope -> Type -> Type

Uses free variable analysis to introduce noAbs bindings.

telePi_ :: Telescope -> Type -> Type

Everything will be a Abs.

class TeleNoAbs a where

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term

dLub :: Sort -> Abs Sort -> Sort

Dependent least upper bound, to assign a level to expressions like forall i -> Set i.

dLub s1 i.s2 = omega if i appears in the rigid variables of s2.

Functions on abstractions

absApp :: Subst t => Abs t -> Term -> t

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst t => Abs t -> Term -> t

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 => Empty -> Abs t -> t

Instantiate an abstraction that doesn't use its argument.

absBody :: Subst t => Abs t -> t

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

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

underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b

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 a => Int -> (a -> Term -> Term) -> a -> Term -> Term

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.

class GetBody a where

Methods to retrieve the clauseBody.

Methods

getBody :: a -> Maybe Term

Returns the properly raised clause Body, and Nothing if NoBody.

getBodyUnraised :: a -> Maybe Term

Just grabs the body, without raising the de Bruijn indices. This is useful if you want to consider the body in context clauseTel.

Syntactic equality and order

Level stuff

pts :: Sort -> Sort -> Sort

The `rule', if Agda is considered as a functional pure type system (pts).

TODO: This needs to be properly implemented, requiring refactoring of Agda's handling of levels. Without impredicativity or SizeUniv, Agda's pts rule is just the least upper bound, which is total and commutative. The handling of levels relies on this simplification.

sLub :: Sort -> Sort -> Sort

data Substitution

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS

Empty substitution, lifts from the empty context. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

Term :# Substitution infixr 4

Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

Strengthen Empty Substitution

Strengthening substitution. First argument is IMPOSSIBLE. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A

Wk !Int Substitution

Weakning substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

Lift !Int Substitution

Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ