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

Safe Haskell | None

Agda.TypeChecking.Substitute

Synopsis

- class Apply t where
  - apply :: t -> Args -> t
- piApply :: Type -> Args -> Type
- class Abstract t where
  - abstract :: Telescope -> t -> t
- telVars :: Telescope -> [Arg Pattern]
- abstractArgs :: Abstract a => Args -> a -> a
- data Substitution
  - = IdS
  - | EmptyS
  - | Wk !Int Substitution
  - | Term :# Substitution
  - | Lift !Int Substitution
- idS :: Substitution
- wkS :: Int -> Substitution -> Substitution
- raiseS :: Int -> Substitution
- singletonS :: Term -> Substitution
- liftS :: Int -> Substitution -> Substitution
- dropS :: Int -> Substitution -> Substitution
- composeS :: Substitution -> Substitution -> Substitution
- splitS :: Int -> Substitution -> (Substitution, Substitution)
- (++#) :: [Term] -> Substitution -> Substitution
- parallelS :: [Term] -> Substitution
- lookupS :: Substitution -> Nat -> Term
- class Subst t where
  - applySubst :: Substitution -> t -> t
- raise :: Subst t => Nat -> t -> t
- raiseFrom :: Subst t => Nat -> Nat -> t -> t
- subst :: Subst t => Term -> t -> t
- substUnder :: Subst t => Nat -> Term -> t -> t
- data TelV a = TelV (Tele (Dom a)) a
- type TelView = TelV Type
- telFromList :: [Dom (String, Type)] -> Telescope
- telToList :: Telescope -> [Dom (String, Type)]
- telView' :: Type -> TelView
- mkPi :: Dom (String, Type) -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- dLub :: Sort -> Abs Sort -> Sort
- absApp :: Subst t => Abs t -> Term -> t
- absBody :: Subst t => Abs t -> t
- mkAbs :: (Subst a, Free a) => String -> a -> Abs a
- reAbs :: (Subst a, Free a) => Abs a -> Abs a
- underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
- underLambdas :: Subst a => Int -> (a -> Term -> Term) -> a -> Term -> Term
- sLub :: Sort -> Sort -> Sort
- lvlView :: Term -> Level
- levelMax :: [PlusLevel] -> Level
- sortTm :: Sort -> Term
- levelSort :: Level -> Sort
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term

# Documentation

class Apply t where

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

Methods

apply :: t -> Args -> t

Instances

Apply Permutation |
Apply ClauseBody |
Apply Clause |
Apply Sort |
Apply Type |
Apply Term |
Apply CompiledClauses |
Apply FunctionInverse |
Apply PrimFun |
Apply Defn |
Apply Definition |
Apply DisplayTerm |
Apply t => Apply [t] |
Apply [Occurrence] |
Apply [Polarity] |
Apply t => Apply (Maybe t) |
Apply a => Apply (Ptr 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) |

piApply :: Type -> Args -> Type

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

class Abstract t where

`(abstract args v) 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 Definition |
Abstract t => Abstract [t] |
Abstract [Occurrence] |
Abstract [Polarity] |
Abstract t => Abstract (Maybe t) |
Abstract a => Abstract (Case a) |
Abstract a => Abstract (WithArity a) |
Abstract v => Abstract (Map k v) |

telVars :: Telescope -> [Arg Pattern]

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

data Substitution

Substitutions.

Constructors

IdS |
EmptyS |
Wk !Int Substitution |
Term :# Substitution |
Lift !Int Substitution |

Instances

Eq Substitution |
Ord Substitution |
Show Substitution |
Sized Substitution |
KillRange Substitution |
Subst Substitution |

idS :: Substitution

wkS :: Int -> Substitution -> Substitution

raiseS :: Int -> Substitution

singletonS :: Term -> Substitution

liftS :: Int -> Substitution -> Substitution

dropS :: Int -> Substitution -> Substitution

composeS :: Substitution -> Substitution -> Substitution

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

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

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

parallelS :: [Term] -> Substitution

lookupS :: Substitution -> Nat -> Term

class Subst t where

Apply a substitution.

Methods

applySubst :: Substitution -> t -> t

Instances

Subst () |
Subst Pattern |
Subst ClauseBody |
Subst LevelAtom |
Subst PlusLevel |
Subst Level |
Subst Sort |
Subst Type |
Subst Elim |
Subst Term |
Subst DisplayTerm |
Subst DisplayForm |
Subst Constraint |
Subst Substitution |
Subst AsBinding |
Subst DotPatternInst |
Subst ProblemRest |
Subst Equality |
Subst a => Subst [a] |
Subst a => Subst (Maybe a) |
Subst a => Subst (Ptr a) |
Subst a => Subst (Arg a) |
Subst a => Subst (Dom a) |
Subst t => Subst (Blocked t) |
Subst a => Subst (Tele a) |
Subst a => Subst (Abs a) |
Subst (Problem' p) |
Subst a => Subst (HomHet a) |
(Subst a, Subst b) => Subst (a, b) |

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

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

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

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

data TelV a

Constructors

TelV (Tele (Dom a)) a |

Instances

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

type TelView = TelV Type

telFromList :: [Dom (String, Type)] -> Telescope

telToList :: Telescope -> [Dom (String, Type)]

telView' :: Type -> TelView

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

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

telePi :: Telescope -> Type -> Type

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

teleLam :: Telescope -> 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`.

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

Instantiate an abstraction

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

mkAbs :: (Subst a, Free a) => String -> 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 `Lam`s from `b`, performs operation `k` on `a` and the body of `b`, and puts the `Lam`s back. `a` is raised correctly according to the number of abstractions.

sLub :: Sort -> Sort -> Sort

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term