| 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
class TeleNoAbs a where Source #
Performs void (noAbs) abstraction over telescope.
Minimal complete definition
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.
piApply :: Type -> Args -> Type Source #
(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] Source #
abstractArgs :: Abstract a => Args -> a -> a Source #
renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a Source #
If permute π : [a]Γ -> [a]Δ, then applySubst (renaming _ π) : Term Γ -> Term Δ
renamingR :: DeBruijn a => Permutation -> Substitution' a Source #
If permute π : [a]Γ -> [a]Δ, then applySubst (renamingR π) : Term Δ -> Term Γ
renameP :: Subst t a => Empty -> Permutation -> a -> a Source #
The permutation should permute the corresponding context. (right-to-left list)
applyNLPatSubst :: Subst Term a => Substitution' NLPat -> a -> a Source #
applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a Source #
projDropParsApply :: Projection -> ProjOrigin -> Args -> Term Source #
projDropParsApply proj o args =projDropParsproj o `apply'args
This function is an optimization, saving us from construction lambdas we immediately remove through application.
telView' :: Type -> TelView Source #
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 Source #
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 Source #
Turn a typed binding (x1 .. xn : A) into a telescope.
bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a Source #
Turn a typed binding (x1 .. xn : A) into a telescope.
bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel Source #
telePi :: Telescope -> Type -> Type Source #
Uses free variable analysis to introduce NoAbs bindings.
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] Source #
Given arguments vs : tel (vector typing), extract their individual types.
Returns Nothing is tel is not long enough.
compiledClauseBody :: Clause -> Maybe Term Source #
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 Source #
Compute the sort of a function type from the sorts of its domain and codomain.
piSort' :: Sort -> Abs Sort -> Maybe Sort Source #
Compute the sort of a pi type from the sorts of its domain and codomain.
unLevelAtom :: LevelAtom -> Term Source #
data Substitution' a Source #
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 Source #