| 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.
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: ConHead -> ConInfo -> Args -> 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
- projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
- type TelView = TelV Type
- data TelV a = TelV {}
- 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
- class TeleNoAbs a where
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- pts :: Sort -> Sort -> Sort
- sLub :: Sort -> Sort -> Sort
- dLub :: Sort -> Abs Sort -> Sort
- lvlView :: Term -> Level
- levelMax :: [PlusLevel] -> Level
- sortTm :: Sort -> Term
- levelSort :: Level -> Sort
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term
- 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
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.
Abstraction
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #
abstractArgs :: Abstract a => Args -> a -> a Source #
Substitution and raisingshiftingweakening
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 #
Projections
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.
Telescopes
Telescope view of a type
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.
Creating telescopes from lists of types
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 #
Abstracting in terms and types
telePi :: Telescope -> Type -> Type Source #
Uses free variable analysis to introduce NoAbs bindings.
class TeleNoAbs a where Source #
Performs void (noAbs) abstraction over telescope.
Minimal complete definition
Telescope typing
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.
Clauses
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.
Syntactic equality and order
Level stuff
pts :: Sort -> Sort -> Sort Source #
The `rule', if Agda is considered as a functional
pure type system (pts).
TODO: This needs to be properly implemented, requiring
refactoring of Agda's handling of levels.
Without impredicativity or SizeUniv, Agda's pts rule is
just the least upper bound, which is total and commutative.
The handling of levels relies on this simplification.
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.
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
| Functor Substitution' Source # | |
| Foldable Substitution' Source # | |
| Traversable Substitution' Source # | |
| KillRange Substitution Source # | |
| InstantiateFull Substitution Source # | |
| Data a => Data (Substitution' a) Source # | |
| Show a => Show (Substitution' a) Source # | |
| Null (Substitution' a) Source # | |
| Pretty a => Pretty (Substitution' a) Source # | |
| TermSize a => TermSize (Substitution' a) Source # | |
| (Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # | |
type Substitution = Substitution' Term Source #