| 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) #
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.
Abstraction
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] #
abstractArgs :: Abstract a => Args -> a -> a #
Substitution and raisingshiftingweakening
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 #
Projections
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.
Telescopes
Telescope view of a type
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.
Creating telescopes from lists of types
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 #
Abstracting in terms and types
Performs void (noAbs) abstraction over telescope.
Minimal complete definition
Telescope typing
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] #
Given arguments vs : tel (vector typing), extract their individual types.
Returns Nothing is tel is not long enough.
Clauses
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.
Syntactic equality and order
Level stuff
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 #
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 #
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
| Functor Substitution' # | |
| Foldable Substitution' # | |
| Traversable Substitution' # | |
| KillRange Substitution # | |
| InstantiateFull Substitution # | |
| Data a => Data (Substitution' a) # | |
| Show a => Show (Substitution' a) # | |
| Null (Substitution' a) # | |
| Pretty a => Pretty (Substitution' a) # | |
| TermSize a => TermSize (Substitution' a) # | |
| (Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) # | |
type Substitution = Substitution' Term #