| Safe Haskell | Safe-Inferred |
|---|---|
| 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
- applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
- defApp :: QName -> Elims -> Elims -> Term
- argToDontCare :: Arg Term -> Term
- relToDontCare :: LensRelevance a => a -> 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 => Impossible -> Permutation -> Substitution' a
- renamingR :: DeBruijn a => Permutation -> Substitution' a
- renameP :: Subst a => Impossible -> Permutation -> a -> a
- applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
- applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
- applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
- fromPatternSubstitution :: PatternSubstitution -> Substitution
- applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
- usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
- usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
- projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
- telView' :: Type -> TelView
- telView'UpTo :: Int -> Type -> TelView
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
- bindsToTel1 :: List1 Name -> Dom Type -> ListTel
- namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
- namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
- domFromNamedArgName :: NamedArg Name -> Dom ()
- mkPiSort :: Dom Type -> Abs Type -> Sort
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- mkLam :: Arg ArgName -> Term -> Term
- lamView :: Term -> ([Arg ArgName], Term)
- unlamView :: [Arg ArgName] -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- telePiVisible :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Sort -> Maybe Sort
- univSort :: Sort -> Sort
- sort :: Sort -> Type
- ssort :: Level -> Type
- isSmallSort :: Sort -> Maybe (Bool, IsFibrant)
- fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant
- funSort' :: Sort -> Sort -> Maybe Sort
- funSort :: Sort -> Sort -> Sort
- piSort' :: Dom Term -> Sort -> Abs Sort -> Maybe Sort
- piSort :: Dom Term -> Sort -> Abs Sort -> Sort
- levelMax :: Integer -> [PlusLevel] -> Level
- levelLub :: Level -> Level -> Level
- levelTm :: Level -> Term
- module Agda.TypeChecking.Substitute.Class
- module Agda.TypeChecking.Substitute.DeBruijn
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term
Documentation
applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t Source #
Apply Elims while using the given function to report ill-typed
redexes.
Recursive calls for applyE and applySubst happen at type t to
propagate the same strategy to subtrees.
canProject :: QName -> Term -> Maybe (Arg Term) Source #
If $v$ is a record value, canProject f v
returns its field f.
conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term Source #
Eliminate a constructed term.
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.
relToDontCare :: LensRelevance a => a -> Term -> Term Source #
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 => Impossible -> 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 a => Impossible -> Permutation -> a -> a Source #
The permutation should permute the corresponding context. (right-to-left list)
applySubstTerm :: forall t. (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t Source #
applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a Source #
applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a Source #
applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a Source #
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a Source #
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> 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.
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope Source #
Turn a typed binding (x1 .. xn : A) into a telescope.
telePi :: Telescope -> Type -> Type Source #
Uses free variable analysis to introduce NoAbs bindings.
telePiVisible :: Telescope -> Type -> Type Source #
Only abstract the visible components of the telescope,
and all that bind variables. Everything will be an Abs!
Caution: quadratic time!
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.
univSort' :: Sort -> Maybe Sort Source #
univSort' univInf s gets the next higher sort of s, if it is
known (i.e. it is not just UnivSort s).
Precondition: s is reduced
isSmallSort :: Sort -> Maybe (Bool, IsFibrant) Source #
Returns Nothing for unknown (meta) sorts, and otherwise returns
Just (b,f) where b indicates smallness and f fibrancy.
I.e., b is True for (relatively) small sorts like Set l and
Prop l, and instead b is False for large sorts such as Setω.
funSort' :: Sort -> Sort -> Maybe Sort Source #
Compute the sort of a function type from the sorts of its domain and codomain.
piSort' :: Dom Term -> Sort -> Abs Sort -> Maybe Sort Source #
Compute the sort of a pi type from the sorts of its domain and codomain.
levelLub :: Level -> Level -> Level Source #
Given two levels a and b, compute a ⊔ b and return its
canonical form.
data Substitution' a Source #
Substitutions.
Constructors
| IdS | Identity substitution.
|
| EmptyS Impossible | Empty substitution, lifts from the empty context. First argument is |
| a :# (Substitution' a) infixr 4 | Substitution extension, ` |
| Strengthen Impossible (Substitution' a) | Strengthening substitution. First argument is |
| Wk !Int (Substitution' a) | Weakening 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 #