Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 {}
- sort :: Sort -> Type
- mkLam :: Arg ArgName -> Term -> Term
- funSort :: Sort -> Sort -> Sort
- renaming :: 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 :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
- defApp :: QName -> Elims -> Elims -> Term
- conApp :: (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 :: (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
- type TelView = TelV Type
- 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
- class TeleNoAbs a where
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Sort -> Either Blocker Sort
- ssort :: Level -> Type
- data SizeOfSort = SizeOfSort {
- szSortUniv :: Univ
- szSortSize :: Integer
- pattern SmallSort :: Univ -> SizeOfSort
- pattern LargeSort :: Univ -> Integer -> SizeOfSort
- 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
renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a Source #
If permute π : [a]Γ -> [a]Δ
, then applySubst (renaming _ π) : Term Γ -> Term Δ
applyTermE :: (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 :: (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 :: (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 =projDropPars
proj 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
data SizeOfSort Source #
A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).
SizeOfSort | |
|
pattern SmallSort :: Univ -> SizeOfSort Source #
pattern LargeSort :: Univ -> Integer -> SizeOfSort Source #
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.
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
KillRange Substitution Source # | |||||
Defined in Agda.Syntax.Internal | |||||
InstantiateFull Substitution Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
Functor Substitution' Source # | |||||
Defined in Agda.Syntax.Internal fmap :: (a -> b) -> Substitution' a -> Substitution' b (<$) :: a -> Substitution' b -> Substitution' a # | |||||
Foldable Substitution' Source # | |||||
Defined in Agda.Syntax.Internal fold :: Monoid m => Substitution' m -> m foldMap :: Monoid m => (a -> m) -> Substitution' a -> m foldMap' :: Monoid m => (a -> m) -> Substitution' a -> m foldr :: (a -> b -> b) -> b -> Substitution' a -> b foldr' :: (a -> b -> b) -> b -> Substitution' a -> b foldl :: (b -> a -> b) -> b -> Substitution' a -> b foldl' :: (b -> a -> b) -> b -> Substitution' a -> b foldr1 :: (a -> a -> a) -> Substitution' a -> a foldl1 :: (a -> a -> a) -> Substitution' a -> a toList :: Substitution' a -> [a] null :: Substitution' a -> Bool length :: Substitution' a -> Int elem :: Eq a => a -> Substitution' a -> Bool maximum :: Ord a => Substitution' a -> a minimum :: Ord a => Substitution' a -> a sum :: Num a => Substitution' a -> a product :: Num a => Substitution' a -> a | |||||
Traversable Substitution' Source # | |||||
Defined in Agda.Syntax.Internal traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) | |||||
Eq Substitution | |||||
Defined in Agda.TypeChecking.Substitute (==) :: Substitution -> Substitution -> Bool (/=) :: Substitution -> Substitution -> Bool | |||||
Ord Substitution | |||||
Defined in Agda.TypeChecking.Substitute compare :: Substitution -> Substitution -> Ordering (<) :: Substitution -> Substitution -> Bool (<=) :: Substitution -> Substitution -> Bool (>) :: Substitution -> Substitution -> Bool (>=) :: Substitution -> Substitution -> Bool max :: Substitution -> Substitution -> Substitution min :: Substitution -> Substitution -> Substitution | |||||
Pretty a => Pretty (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source # | |||||
TermSize a => TermSize (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source # | |||||
NamesIn a => NamesIn (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal.Names namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source # | |||||
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source # | |||||
EmbPrj a => EmbPrj (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source # | |||||
EndoSubst a => Subst (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute
applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source # | |||||
Null (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal empty :: Substitution' a Source # null :: Substitution' a -> Bool Source # | |||||
NFData a => NFData (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal rnf :: Substitution' a -> () | |||||
Generic (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal
from :: Substitution' a -> Rep (Substitution' a) x to :: Rep (Substitution' a) x -> Substitution' a | |||||
Show a => Show (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal showsPrec :: Int -> Substitution' a -> ShowS show :: Substitution' a -> String showList :: [Substitution' a] -> ShowS | |||||
type SubstArg (Substitution' a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep (Substitution' a) Source # | |||||
Defined in Agda.Syntax.Internal type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))))) |
type Substitution = Substitution' Term Source #