| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Substitute
Contents
- 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
- fromPatternSubstitution :: PatternSubstitution -> Substitution
- applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a
- projDropParsApply :: Projection -> ProjOrigin -> Args -> Term
- 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
- telToArgs :: Telescope -> [Arg ArgName]
- 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
- telView' :: Type -> TelView
- telView'UpTo :: Int -> Type -> TelView
- 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
- 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
- | 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)
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
telFromList :: ListTel -> Telescope Source #
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 #
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.
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
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 substitution, lifts from the empty context.
Apply this to closed terms you want to use in a non-empty context.
|
| 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 # | |
| Show a => Show (Substitution' a) Source # | |
| Pretty a => Pretty (Substitution' a) Source # | |
| Null (Substitution' a) Source # | |
| TermSize a => TermSize (Substitution' a) Source # | |
| (Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # | |
type Substitution = Substitution' Term Source #