Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Substitute

Contents

Application
Abstraction
Explicit substitutions
Substitution and raisingshiftingweakening
Telescopes
Functions on abstractions
Syntactic equality and order
Level stuff
Boring instances

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

Nothing

Methods

apply :: t -> Args -> t Source

applyE :: t -> Elims -> t Source

Instances

Apply Permutation
Apply ClauseBody
Apply Clause
Apply Sort
Apply Type
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 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)

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

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

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

Eliminate a constructed term.

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

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 c Term -> Term Source

piApply :: Type -> Args -> Type Source

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

Abstraction

class Abstract t where Source

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

Methods

abstract :: Telescope -> t -> t Source

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 :: Telescope -> [Arg Pattern] Source

namedTelVars :: Telescope -> [NamedArg Pattern] Source

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

Explicit substitutions

idS :: Substitution Source

wkS :: Int -> Substitution -> Substitution Source

raiseS :: Int -> Substitution Source

consS :: Term -> Substitution -> Substitution Source

singletonS :: Term -> Substitution Source

liftS :: Int -> Substitution -> Substitution Source

dropS :: Int -> Substitution -> Substitution Source

composeS :: Substitution -> Substitution -> Substitution Source

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

splitS :: Int -> Substitution -> (Substitution, Substitution) Source

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

prependS :: Empty -> [Maybe Term] -> Substitution -> Substitution Source

parallelS :: [Term] -> Substitution Source

compactS :: Empty -> [Maybe Term] -> Substitution Source

lookupS :: Substitution -> Nat -> Term Source

Substitution and raisingshiftingweakening

class Subst t where Source

Apply a substitution.

Methods

applySubst :: Substitution -> t -> t Source

Instances

Subst Bool
Subst ()
Subst Name
Subst Substitution
Subst Pattern
Subst ClauseBody
Subst Clause
Subst LevelAtom
Subst PlusLevel
Subst Level
Subst Sort
Subst Type
Subst Elim
Subst Term
Subst DisplayTerm
Subst DisplayForm
Subst Constraint
Subst AsBinding
Subst DotPatternInst
Subst ProblemRest
Subst Equality
Subst SizeConstraint
Subst SizeMeta
Subst a => Subst [a]
Subst a => Subst (Maybe a)
Subst a => Subst (Ptr a)
Subst t => Subst (Blocked t)
Subst a => Subst (Tele a)
Subst a => Subst (Abs a)
Subst a => Subst (Dom a)
Subst a => Subst (Arg a)
Subst (Problem' p)
Subst a => Subst (HomHet a)
(Subst a, Subst b) => Subst (a, b)
Subst (SizeExpr' NamedRigid SizeMeta)	Only for `raise`.
Subst a => Subst (Named name a)
(Subst a, Subst b, Subst c) => Subst (a, b, c)
(Subst a, Subst b, Subst c, Subst d) => Subst (a, b, c, d)

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

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

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

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

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

Telescopes

type TelView = TelV Type Source

data TelV a Source

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)
Typeable (* -> *) TelV

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

type ListTel = ListTel' ArgName Source

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

telFromList :: ListTel -> Telescope Source

telToList :: Telescope -> ListTel Source

telToArgs :: Telescope -> [Arg ArgName] Source

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

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

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

telView' :: Type -> TelView Source

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

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

mkLam :: Arg ArgName -> Term -> Term Source

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

telePi :: Telescope -> Type -> Type Source

Uses free variable analysis to introduce noAbs bindings.

telePi_ :: Telescope -> Type -> Type Source

Everything will be a Abs.

teleLam :: Telescope -> Term -> Term Source

class TeleNoAbs a where Source

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term Source

Instances

TeleNoAbs Telescope
TeleNoAbs ListTel

dLub :: Sort -> Abs Sort -> Sort Source

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 Source

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst t => Abs t -> Term -> t 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 => Empty -> Abs t -> t Source

Instantiate an abstraction that doesn't use its argument.

absBody :: Subst t => Abs t -> t 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 :: Subst 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.

class GetBody a where Source

Methods to retrieve the clauseBody.

Methods

getBody :: a -> Maybe Term Source

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

getBodyUnraised :: a -> Maybe Term Source

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

Instances