Agda.TypeChecking.Substitute

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

Instances

Apply Permutation

Apply ClauseBody

Apply Clause

Apply Sort

Apply Term

Apply CompiledClauses

Apply FunctionInverse

Apply PrimFun

Apply Defn

Apply Projection

Apply Definition

Apply RewriteRule

Apply DisplayTerm

Apply t => Apply [t]

Apply [Occurrence]

Apply [Polarity]

Apply t => Apply (Maybe t)

Apply a => Apply (Ptr a)

DoDrop a => Apply (Drop a)

Apply t => Apply (Blocked t)

Subst Term a => Apply (Tele a)

Apply a => Apply (Case a)

Apply a => Apply (WithArity a)

(Apply a, Apply b) => Apply (a, b)

Apply v => Apply (Map k v)

(Apply a, Apply b, Apply c) => Apply (a, b, c)

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

Apply to some default arguments.

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

Apply to a single default 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.

argToDontCare :: Arg Term -> Term

piApply :: Type -> Args -> Type

(x:A)->B(x) piApply [u] = B(u)

Precondition: The type must contain the right number of pis without having to perform any reduction.

piApply is potentially unsafe, the monadic piApplyM is preferable.

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)

telVars :: Int -> Telescope -> [Arg DeBruijnPattern]

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]

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

Explicit substitutions

class DeBruijn a where

Minimal complete definition

debruijnView

Methods

debruijnVar :: Int -> a

debruijnNamedVar :: String -> Int -> a

debruijnView :: a -> Maybe Int

Instances

DeBruijn Term

idS :: Substitution' a

wkS :: Int -> Substitution' a -> Substitution' a

raiseS :: Int -> Substitution' a

consS :: DeBruijn a => a -> Substitution' a -> Substitution' a

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

To replace index n by term u, do applySubst (singletonS n u).

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

Lift a substitution under k binders.

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

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

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

splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)

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

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

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

compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a

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

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

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

Substitution and raisingshiftingweakening

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

Apply a substitution.

Methods

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

Instances

Subst Term String

Subst Term ()

Subst Term Name

Subst Term EqualityView

Subst Term ConPatternInfo

Subst Term Pattern

Subst Term ClauseBody

Subst Term LevelAtom

Subst Term PlusLevel

Subst Term Level

Subst Term Sort

Subst Term Term

Subst Term Candidate

Subst Term RewriteRule

Subst Term NLPat

Subst Term DisplayTerm

Subst Term DisplayForm

Subst Term Constraint

Subst Term AsBinding

Subst Term DotPatternInst

Subst Term ProblemRest

Subst Term SizeConstraint

Subst Term SizeMeta

Subst t a => Subst t [a]

Subst t a => Subst t (Maybe a)

Subst t a => Subst t (Dom a)

Subst t a => Subst t (Arg a)

Subst t a => Subst t (Abs a)

Subst t a => Subst t (Elim' a)

Subst t a => Subst t (Tele a)

Subst t a => Subst t (Blocked a)

Subst t a => Subst t (Ptr a)

Subst a a => Subst a (Substitution' a)

Subst Term a => Subst Term (Type' a)

Subst Term (Problem' p)

(Subst t a, Subst t b) => Subst t (a, b)

Subst t a => Subst t (Named name a)

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c)

(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d)

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

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

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

Replace de Bruijn index i by a Term in something.

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

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

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

Telescopes

type TelView = TelV Type

data TelV a

Constructors

TelV

Fields

theTel :: Tele (Dom a)

theCore :: a

Instances

Functor TelV

(Subst t a, Eq a) => Eq (TelV a)

(Subst t a, Ord a) => Ord (TelV a)

Show a => Show (TelV a)

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

type ListTel = ListTel' ArgName

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

telFromList :: ListTel -> Telescope

telToList :: Telescope -> ListTel

telToArgs :: Telescope -> [Arg ArgName]

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

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

bindsToTel :: [Name] -> Dom Type -> ListTel

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

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

bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel

telView' :: Type -> TelView

Takes off all exposed function domains from the given type. This means that it does not reduce to expose Pi-types.

telView'UpTo :: Int -> Type -> TelView

telView'UpTo n t takes off the first n exposed function types of t. Takes off all (exposed ones) if n < 0.

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

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

mkLam :: Arg ArgName -> Term -> Term

telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type

telePi :: Telescope -> Type -> Type

Uses free variable analysis to introduce noAbs bindings.

telePi_ :: Telescope -> Type -> Type

Everything will be a Abs.

teleLam :: Telescope -> Term -> Term

class TeleNoAbs a where

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term

Instances

TeleNoAbs Telescope

TeleNoAbs ListTel

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

Instantiate an abstraction. Strict in the term.

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

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

Instantiate an abstraction that doesn't use its argument.

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

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

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

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

Instances

GetBody ClauseBody

GetBody Clause

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

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term

data Substitution' a

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS

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

a :# (Substitution' a) infixr 4

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

Strengthen Empty (Substitution' a)

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

Wk !Int (Substitution' a)

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

Lift !Int (Substitution' a)

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

Instances

Functor Substitution'

Foldable Substitution'

Traversable Substitution'

Pretty Substitution

KillRange Substitution

InstantiateFull Substitution

Subst a a => Subst a (Substitution' a)

Show a => Show (Substitution' a)

TermSize a => TermSize (Substitution' a)

(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a)

type Substitution = Substitution' Term