| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Substitute
Contents
- class Apply t where
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: ConHead -> Args -> Elims -> Term
- defApp :: QName -> Elims -> Elims -> Term
- argToDontCare :: Arg c Term -> Term
- piApply :: Type -> Args -> Type
- class Abstract t where
- telVars :: Telescope -> [Arg Pattern]
- namedTelVars :: Telescope -> [NamedArg 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
- type TelView = TelV Type
- data TelV a = TelV {}
- type ListTel' a = [Dom (a, Type)]
- type ListTel = ListTel' ArgName
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- telToList :: Telescope -> ListTel
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- telView' :: Type -> TelView
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- class TeleNoAbs a where
- dLub :: Sort -> Abs Sort -> Sort
- absApp :: Subst t => Abs t -> Term -> t
- 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
- underLambdas :: Subst a => Int -> (a -> Term -> Term) -> a -> Term -> Term
- class GetBody a where
- sLub :: Sort -> Sort -> Sort
- lvlView :: Term -> Level
- levelMax :: [PlusLevel] -> Level
- sortTm :: Sort -> Term
- levelSort :: Level -> Sort
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term
Application
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
Minimal complete definition
Nothing
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 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.
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
(abstract args v) .apply args --> v[args]
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 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) |
namedTelVars :: Telescope -> [NamedArg Pattern] Source
abstractArgs :: Abstract a => Args -> a -> a Source
Explicit substitutions
data Substitution Source
Substitutions.
Constructors
| IdS | |
| EmptyS | |
| Wk !Int Substitution | |
| Term :# Substitution infixr 4 | |
| Lift !Int Substitution |
wkS :: Int -> Substitution -> Substitution Source
raiseS :: Int -> 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
parallelS :: [Term] -> Substitution Source
lookupS :: Substitution -> Nat -> Term Source
Substitution and raisingshiftingweakening
Apply a substitution.
Methods
applySubst :: Substitution -> t -> t Source
Instances
| Subst Bool | |
| Subst () | |
| Subst Name | |
| 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 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 |
| 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) |
substUnder :: Subst t => Nat -> Term -> t -> t Source
Telescopes
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope Source
telFromList :: ListTel -> Telescope Source
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a Source
Turn a typed binding (x1 .. xn : A) into a telescope.
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
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.
getBody returns the properly raised clause Body,
and Nothing if NoBody.
getBodyUnraised just grabs the body, without raising the de Bruijn indices.
This is useful if you want to consider the body in context clauseTel.
Instances
Syntactic equality and order
Level stuff
unLevelAtom :: LevelAtom -> Term Source