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

Safe Haskell | Safe-Infered

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 :: Functor f => Tele (f a) -> [f Pattern]
- abstractArgs :: Abstract a => Args -> a -> a
- type Substitution = [Term]
- class Subst t where
  - substs :: Substitution -> t -> t
  - substUnder :: Nat -> Term -> t -> t
- idSub :: Telescope -> Substitution
- subst :: Subst t => Term -> t -> t
- class Raise t where
  - raiseFrom :: Nat -> Nat -> t -> t
  - renameFrom :: Nat -> (Nat -> Nat) -> t -> t
- raise :: Raise t => Nat -> t -> t
- rename :: Raise t => (Nat -> Nat) -> t -> t
- data TelV a = TelV (Tele (Arg a)) a
- type TelView = TelV Type
- telFromList :: [Arg (String, Type)] -> Telescope
- telToList :: Telescope -> [Arg (String, Type)]
- telView' :: Type -> TelView
- 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 :: Raise t => Abs t -> t
- mkAbs :: (Raise a, Free a) => String -> a -> Abs a
- reAbs :: (Raise a, Free a) => Abs a -> Abs a
- 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 t => Apply (Maybe t) |
Subst a => Apply (Tele a) |
Apply t => Apply (Blocked t) |
Apply a => Apply (Case 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 Telescope |
Abstract Sort |
Abstract Type |
Abstract Term |
Abstract CompiledClauses |
Abstract FunctionInverse |
Abstract PrimFun |
Abstract Defn |
Abstract Definition |
Abstract t => Abstract [t] |
Abstract t => Abstract (Maybe t) |
Abstract a => Abstract (Case a) |
Abstract v => Abstract (Map k v) |

telVars :: Functor f => Tele (f a) -> [f Pattern]

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

type Substitution = [Term]

Substitutions.

class Subst t where

Substitute a term for the nth free variable.

Methods

substs :: Substitution -> t -> t

substUnder :: Nat -> Term -> t -> t

Instances

Subst Pattern |
Subst ClauseBody |
Subst LevelAtom |
Subst PlusLevel |
Subst Level |
Subst Sort |
Subst Type |
Subst Term |
Subst DisplayTerm |
Subst Equality |
Subst AsBinding |
Subst DotPatternInst |
Subst a => Subst [a] |
Subst a => Subst (Maybe a) |
Subst a => Subst (Arg a) |
Subst a => Subst (Abs a) |
Subst a => Subst (Tele a) |
Subst t => Subst (Blocked t) |
Subst a => Subst (HomHet a) |
(Subst a, Subst b) => Subst (a, b) |

idSub :: Telescope -> Substitution

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

class Raise t where

Add `k` to index of each open variable in `x`.

Methods

raiseFrom :: Nat -> Nat -> t -> t

renameFrom :: Nat -> (Nat -> Nat) -> t -> t

Instances

Raise () |
Raise Pattern |
Raise ClauseBody |
Raise LevelAtom |
Raise PlusLevel |
Raise Level |
Raise Sort |
Raise Elim |
Raise Type |
Raise Term |
Raise DisplayTerm |
Raise DisplayForm |
Raise Constraint |
Raise AsBinding |
Raise t => Raise [t] |
Raise t => Raise (Maybe t) |
Raise t => Raise (Arg t) |
Raise t => Raise (Abs t) |
Raise a => Raise (Tele a) |
Raise t => Raise (Blocked t) |
Raise (Problem' p) |
Raise a => Raise (HomHet a) |
(Raise a, Raise b) => Raise (a, b) |
Raise v => Raise (Map k v) |

raise :: Raise t => Nat -> t -> t

rename :: Raise t => (Nat -> Nat) -> t -> t

data TelV a

Constructors

TelV (Tele (Arg a)) a |

Instances

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

type TelView = TelV Type

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

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

telView' :: Type -> TelView

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 :: Raise t => Abs t -> t

mkAbs :: (Raise a, Free a) => String -> a -> Abs a

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

sLub :: Sort -> Sort -> Sort

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term