| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Substitute
Contents
Description
This module contains the definition of hereditary substitution and application operating on internal syntax which is in β-normal form (β including projection reductions).
Further, it contains auxiliary functions which rely on substitution but not on reduction.
Synopsis
- class TeleNoAbs a where
- data TelV a = TelV {}
- type TelView = TelV Type
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: ConHead -> ConInfo -> Elims -> Elims -> Term
- defApp :: QName -> Elims -> Elims -> Term
- argToDontCare :: Arg Term -> Term
- piApply :: Type -> Args -> Type
- telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
- namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
- abstractArgs :: Abstract a => Args -> a -> a
- renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
- renamingR :: DeBruijn a => Permutation -> Substitution' a
- renameP :: Subst t a => Empty -> Permutation -> a -> a
- applyNLPatSubst :: Subst Term a => Substitution' NLPat -> a -> a
- fromPatternSubstitution :: PatternSubstitution -> Substitution
- applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a
- usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
- projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
- telView' :: Type -> TelView
- telView'UpTo :: Int -> Type -> TelView
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a
- bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- mkLam :: Arg ArgName -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Sort -> Maybe Sort
- univSort :: Sort -> Sort
- funSort' :: Sort -> Sort -> Maybe Sort
- funSort :: Sort -> Sort -> Sort
- piSort' :: Sort -> Abs Sort -> Maybe Sort
- piSort :: Sort -> Abs Sort -> Sort
- levelMax :: [PlusLevel] -> Level
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term
- levelSucView :: Level -> Maybe Level
- module Agda.TypeChecking.Substitute.Class
- module Agda.TypeChecking.Substitute.DeBruijn
- data Substitution' a
- = IdS
- | EmptyS Empty
- | a :# (Substitution' a)
- | Strengthen Empty (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term
Documentation
Performs void (noAbs) abstraction over telescope.
Minimal complete definition
canProject :: QName -> Term -> Maybe (Arg Term) #
If $v$ is a record value, canProject f v
returns its field f.
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.
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] #
abstractArgs :: Abstract a => Args -> a -> a #
renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a #
If permute π : [a]Γ -> [a]Δ, then applySubst (renaming _ π) : Term Γ -> Term Δ
renamingR :: DeBruijn a => Permutation -> Substitution' a #
If permute π : [a]Γ -> [a]Δ, then applySubst (renamingR π) : Term Δ -> Term Γ
renameP :: Subst t a => Empty -> Permutation -> a -> a #
The permutation should permute the corresponding context. (right-to-left list)
applyNLPatSubst :: Subst Term a => Substitution' NLPat -> a -> a #
applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a #
usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a #
projDropParsApply :: Projection -> ProjOrigin -> Args -> Term #
projDropParsApply proj o args =projDropParsproj o `apply'args
This function is an optimization, saving us from construction lambdas we immediately remove through application.
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.
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a #
Turn a typed binding (x1 .. xn : A) into a telescope.
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 #
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] #
Given arguments vs : tel (vector typing), extract their individual types.
Returns Nothing is tel is not long enough.
compiledClauseBody :: Clause -> Maybe Term #
In compiled clauses, the variables in the clause body are relative to the pattern variables (including dot patterns) instead of the clause telescope.
funSort' :: Sort -> Sort -> Maybe Sort #
Compute the sort of a function type from the sorts of its domain and codomain.
piSort' :: Sort -> Abs Sort -> Maybe Sort #
Compute the sort of a pi type from the sorts of its domain and codomain.
unLevelAtom :: LevelAtom -> Term #
levelSucView :: Level -> Maybe Level #
data Substitution' a #
Substitutions.
Constructors
| IdS | Identity substitution.
|
| EmptyS Empty | Empty substitution, lifts from the empty context. First argument is |
| a :# (Substitution' a) infixr 4 | Substitution extension, ` |
| Strengthen Empty (Substitution' a) | Strengthening substitution. First argument is |
| Wk !Int (Substitution' a) | Weakning substitution, lifts to an extended context.
|
| Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Instances
type Substitution = Substitution' Term #