| 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
- data TelV a = TelV {}
- type TelView = TelV Type
- class TeleNoAbs a where
- data SizeOfSort = SizeOfSort {
- szSortUniv :: Univ
- szSortSize :: Integer
- pattern SmallSort :: Univ -> SizeOfSort
- pattern LargeSort :: Univ -> Integer -> SizeOfSort
- sort :: Sort -> Type
- mkLam :: Arg ArgName -> Term -> Term
- funSort :: Sort -> Sort -> Sort
- renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a
- piSort :: Dom Term -> Sort -> Abs Sort -> Sort
- univSort :: Sort -> Sort
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- lamView :: Term -> ([Arg ArgName], Term)
- applyTermE :: forall t. (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
- defApp :: QName -> Elims -> Elims -> Term
- conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
- canProject :: QName -> Term -> Maybe (Arg Term)
- relToDontCare :: LensRelevance a => a -> Term -> Term
- argToDontCare :: Arg Term -> Term
- piApply :: Type -> Args -> Type
- applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
- teleLam :: Telescope -> Term -> Term
- telePi_ :: Telescope -> Type -> Type
- namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
- telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
- abstractArgs :: Abstract a => Args -> a -> 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
- levelTm :: Level -> Term
- 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
- absV :: Dom a -> ArgName -> TelV a -> TelV a
- 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
- domFromNamedArgName :: NamedArg Name -> Dom ()
- namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
- mkPiSort :: Dom Type -> Abs Type -> Sort
- unlamView :: [Arg ArgName] -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePiVisible :: Telescope -> Type -> Type
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Sort -> Either Blocker Sort
- ssort :: Level -> Type
- sizeOfSort :: Sort -> Either Blocker SizeOfSort
- isSmallSort :: Sort -> Bool
- funSort' :: Sort -> Sort -> Either Blocker Sort
- levelLub :: Level -> Level -> Level
- piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
- levelMax :: Integer -> [PlusLevel] -> Level
- module Agda.TypeChecking.Substitute.Class
- module Agda.TypeChecking.Substitute.DeBruijn
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible !Int (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term
Documentation
data SizeOfSort Source #
A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).
Constructors
| SizeOfSort | |
Fields
| |
pattern SmallSort :: Univ -> SizeOfSort Source #
renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a Source #
If permute π : [a]Γ -> [a]Δ, then applySubst (renaming _ π) : Term Γ -> Term Δ
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.
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.
conApp :: forall t. (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term Source #
Eliminate a constructed term.
canProject :: QName -> Term -> Maybe (Arg Term) Source #
If v is a record or constructed value, canProject f v
returns its field f.
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.
applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a Source #
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #
abstractArgs :: Abstract a => Args -> a -> a Source #
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 #
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.
absV :: Dom a -> ArgName -> TelV a -> TelV a Source #
Add given binding to the front of the telescope.
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 -> Either Blocker 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
sizeOfSort :: Sort -> Either Blocker SizeOfSort Source #
Returns Left blocker for unknown (blocked) sorts, and otherwise
returns Right s where s indicates the size and fibrancy.
isSmallSort :: Sort -> Bool Source #
funSort' :: Sort -> Sort -> Either Blocker Sort Source #
Compute the sort of a function type from the sorts of its domain and codomain.
This function should only be called on reduced sorts,
since the LevelUniv rules should only apply when the sort does not reduce to Set.
levelLub :: Level -> Level -> Level Source #
Given two levels a and b, compute a ⊔ b and return its
canonical form.
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort Source #
Compute the sort of a pi type from the sorts of its domain
and codomain.
This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort doesn't reduce to Set
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 !Int (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 #