Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Substitute

Contents

Synopsis

Documentation

canProject :: QName -> Term -> Maybe (Arg Term) #

If $v$ is a record value, canProject f v returns its field f.

conApp :: ConHead -> ConInfo -> Args -> Elims -> Term #

Eliminate a constructed term.

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.

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

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)

Projections

projDropParsApply :: Projection -> ProjOrigin -> Args -> Term #

projDropParsApply proj o args = projDropPars proj o `apply' args

This function is an optimization, saving us from construction lambdas we immediately remove through application.

Telescopes

data TelV a #

Constructors

TelV 

Fields

Instances

Functor TelV # 

Methods

fmap :: (a -> b) -> TelV a -> TelV b #

(<$) :: a -> TelV b -> TelV a #

(Subst t a, Eq a) => Eq (TelV a) # 

Methods

(==) :: TelV a -> TelV a -> Bool #

(/=) :: TelV a -> TelV a -> Bool #

(Subst t a, Ord a) => Ord (TelV a) # 

Methods

compare :: TelV a -> TelV a -> Ordering #

(<) :: TelV a -> TelV a -> Bool #

(<=) :: TelV a -> TelV a -> Bool #

(>) :: TelV a -> TelV a -> Bool #

(>=) :: TelV a -> TelV a -> Bool #

max :: TelV a -> TelV a -> TelV a #

min :: TelV a -> TelV a -> TelV a #

Show a => Show (TelV a) # 

Methods

showsPrec :: Int -> TelV a -> ShowS #

show :: TelV a -> String #

showList :: [TelV a] -> ShowS #

type ListTel' a = [Dom (a, Type)] #

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.

telView' :: Type -> TelView #

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.

mkPi :: Dom (ArgName, Type) -> Type -> Type #

mkPi dom t = telePi (telFromList [dom]) t

telePi :: Telescope -> Type -> Type #

Uses free variable analysis to introduce noAbs bindings.

telePi_ :: Telescope -> Type -> Type #

Everything will be a Abs.

class TeleNoAbs a where #

Performs void (noAbs) abstraction over telescope.

Minimal complete definition

teleNoAbs

Methods

teleNoAbs :: a -> Term -> Term #

Instances

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

pts :: Sort -> Sort -> Sort #

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.

sLub :: Sort -> Sort -> Sort #

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.

data Substitution' a #

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS

Empty substitution, lifts from the empty context. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : ()

a :# (Substitution' a) infixr 4

Substitution extension, `cons'. Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A

Strengthen Empty (Substitution' a)

Strengthening substitution. First argument is IMPOSSIBLE. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A

Wk !Int (Substitution' a)

Weakning substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ

Lift !Int (Substitution' a)

Lifting substitution. Use this to go under a binder. Lift 1 ρ == var 0 :# Wk 1 ρ. Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ

Instances

Functor Substitution' # 

Methods

fmap :: (a -> b) -> Substitution' a -> Substitution' b #

(<$) :: a -> Substitution' b -> Substitution' a #

Foldable Substitution' # 

Methods

fold :: Monoid m => Substitution' m -> 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' # 

Methods

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) #

KillRange Substitution # 
InstantiateFull Substitution # 
Show a => Show (Substitution' a) # 
Pretty a => Pretty (Substitution' a) # 
Null (Substitution' a) # 
TermSize a => TermSize (Substitution' a) # 
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) # 

Orphan instances

Eq NotBlocked # 
Eq LevelAtom # 
Eq PlusLevel # 
Eq Level # 

Methods

(==) :: Level -> Level -> Bool #

(/=) :: Level -> Level -> Bool #

Eq Sort # 

Methods

(==) :: Sort -> Sort -> Bool #

(/=) :: Sort -> Sort -> Bool #

Eq Term #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Methods

(==) :: Term -> Term -> Bool #

(/=) :: Term -> Term -> Bool #

Eq Candidate # 
Eq Section # 

Methods

(==) :: Section -> Section -> Bool #

(/=) :: Section -> Section -> Bool #

Eq Constraint # 
Ord NotBlocked # 
Ord LevelAtom # 
Ord PlusLevel # 
Ord Level # 

Methods

compare :: Level -> Level -> Ordering #

(<) :: Level -> Level -> Bool #

(<=) :: Level -> Level -> Bool #

(>) :: Level -> Level -> Bool #

(>=) :: Level -> Level -> Bool #

max :: Level -> Level -> Level #

min :: Level -> Level -> Level #

Ord Sort # 

Methods

compare :: Sort -> Sort -> Ordering #

(<) :: Sort -> Sort -> Bool #

(<=) :: Sort -> Sort -> Bool #

(>) :: Sort -> Sort -> Bool #

(>=) :: Sort -> Sort -> Bool #

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Ord Term # 

Methods

compare :: Term -> Term -> Ordering #

(<) :: Term -> Term -> Bool #

(<=) :: Term -> Term -> Bool #

(>) :: Term -> Term -> Bool #

(>=) :: Term -> Term -> Bool #

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

DeBruijn DeBruijnPattern # 
Abstract Permutation # 
Abstract Clause # 

Methods

abstract :: Telescope -> Clause -> Clause #

Abstract Sort # 

Methods

abstract :: Telescope -> Sort -> Sort #

Abstract Telescope # 
Abstract Type # 

Methods

abstract :: Telescope -> Type -> Type #

Abstract Term # 

Methods

abstract :: Telescope -> Term -> Term #

Abstract CompiledClauses # 
Abstract FunctionInverse # 
Abstract PrimFun # 
Abstract Defn # 

Methods

abstract :: Telescope -> Defn -> Defn #

Abstract ProjLams # 
Abstract Projection # 
Abstract Definition # 
Abstract RewriteRule #

tel ⊢ (Γ ⊢ lhs ↦ rhs : t) becomes tel, Γ ⊢ lhs ↦ rhs : t) we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.

Apply Permutation # 
Apply Clause # 

Methods

apply :: Clause -> Args -> Clause #

applyE :: Clause -> Elims -> Clause #

Apply Sort # 

Methods

apply :: Sort -> Args -> Sort #

applyE :: Sort -> Elims -> Sort #

Apply Term # 

Methods

apply :: Term -> Args -> Term #

applyE :: Term -> Elims -> Term #

Apply CompiledClauses # 
Apply FunctionInverse # 
Apply PrimFun # 
Apply Defn # 

Methods

apply :: Defn -> Args -> Defn #

applyE :: Defn -> Elims -> Defn #

Apply ProjLams # 
Apply Projection # 
Apply Definition # 
Apply RewriteRule # 
Apply DisplayTerm # 
Subst DeBruijnPattern DeBruijnPattern # 
Subst Term () # 

Methods

applySubst :: Substitution' Term -> () -> () #

Subst Term String # 
Subst Term Name # 
Subst Term EqualityView # 
Subst Term ConPatternInfo # 
Subst Term Pattern # 
Subst Term LevelAtom # 
Subst Term PlusLevel # 
Subst Term Level # 
Subst Term Sort # 
Subst Term Term # 
Subst Term NamedDotPattern # 
Subst Term Candidate # 
Subst Term ModuleParameters # 
Subst Term RewriteRule # 
Subst Term NLPType # 
Subst Term NLPat # 
Subst Term DisplayTerm # 
Subst Term DisplayForm # 
Subst Term Constraint # 
Subst t a => Subst t [a] # 

Methods

applySubst :: Substitution' t -> [a] -> [a] #

Subst t a => Subst t (Maybe a) # 

Methods

applySubst :: Substitution' t -> Maybe a -> Maybe a #

Subst t a => Subst t (Dom a) # 

Methods

applySubst :: Substitution' t -> Dom a -> Dom a #

Subst t a => Subst t (Arg a) # 

Methods

applySubst :: Substitution' t -> Arg a -> Arg a #

Subst t a => Subst t (Abs a) # 

Methods

applySubst :: Substitution' t -> Abs a -> Abs a #

Subst t a => Subst t (Elim' a) # 

Methods

applySubst :: Substitution' t -> Elim' a -> Elim' a #

Subst t a => Subst t (Tele a) # 

Methods

applySubst :: Substitution' t -> Tele a -> Tele a #

Subst t a => Subst t (Blocked a) # 

Methods

applySubst :: Substitution' t -> Blocked a -> Blocked a #

Subst t a => Subst t (Ptr a) # 

Methods

applySubst :: Substitution' t -> Ptr a -> Ptr a #

Subst a a => Subst a (Substitution' a) # 
Subst Term a => Subst Term (Type' a) # 
(Subst t a, Subst t b) => Subst t (a, b) # 

Methods

applySubst :: Substitution' t -> (a, b) -> (a, b) #

(Ord k, Subst t a) => Subst t (Map k a) # 

Methods

applySubst :: Substitution' t -> Map k a -> Map k a #

Subst t a => Subst t (Named name a) # 

Methods

applySubst :: Substitution' t -> Named name a -> Named name a #

(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) # 

Methods

applySubst :: Substitution' t -> (a, b, c) -> (a, b, c) #

(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) # 

Methods

applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d) #

Eq (Substitution' Term) # 
Eq t => Eq (Blocked t) # 

Methods

(==) :: Blocked t -> Blocked t -> Bool #

(/=) :: Blocked t -> Blocked t -> Bool #

(Subst t a, Eq a) => Eq (Tele a) # 

Methods

(==) :: Tele a -> Tele a -> Bool #

(/=) :: Tele a -> Tele a -> Bool #

Eq a => Eq (Type' a) #

Syntactic Type equality, ignores sort annotations.

Methods

(==) :: Type' a -> Type' a -> Bool #

(/=) :: Type' a -> Type' a -> Bool #

(Subst t a, Eq a) => Eq (Abs a) # 

Methods

(==) :: Abs a -> Abs a -> Bool #

(/=) :: Abs a -> Abs a -> Bool #

(Subst t a, Eq a) => Eq (Elim' a) # 

Methods

(==) :: Elim' a -> Elim' a -> Bool #

(/=) :: Elim' a -> Elim' a -> Bool #

Ord (Substitution' Term) # 
Ord t => Ord (Blocked t) # 

Methods

compare :: Blocked t -> Blocked t -> Ordering #

(<) :: Blocked t -> Blocked t -> Bool #

(<=) :: Blocked t -> Blocked t -> Bool #

(>) :: Blocked t -> Blocked t -> Bool #

(>=) :: Blocked t -> Blocked t -> Bool #

max :: Blocked t -> Blocked t -> Blocked t #

min :: Blocked t -> Blocked t -> Blocked t #

(Subst t a, Ord a) => Ord (Tele a) # 

Methods

compare :: Tele a -> Tele a -> Ordering #

(<) :: Tele a -> Tele a -> Bool #

(<=) :: Tele a -> Tele a -> Bool #

(>) :: Tele a -> Tele a -> Bool #

(>=) :: Tele a -> Tele a -> Bool #

max :: Tele a -> Tele a -> Tele a #

min :: Tele a -> Tele a -> Tele a #

Ord a => Ord (Type' a) # 

Methods

compare :: Type' a -> Type' a -> Ordering #

(<) :: Type' a -> Type' a -> Bool #

(<=) :: Type' a -> Type' a -> Bool #

(>) :: Type' a -> Type' a -> Bool #

(>=) :: Type' a -> Type' a -> Bool #

max :: Type' a -> Type' a -> Type' a #

min :: Type' a -> Type' a -> Type' a #

(Subst t a, Ord a) => Ord (Abs a) # 

Methods

compare :: Abs a -> Abs a -> Ordering #

(<) :: Abs a -> Abs a -> Bool #

(<=) :: Abs a -> Abs a -> Bool #

(>) :: Abs a -> Abs a -> Bool #

(>=) :: Abs a -> Abs a -> Bool #

max :: Abs a -> Abs a -> Abs a #

min :: Abs a -> Abs a -> Abs a #

(Subst t a, Ord a) => Ord (Elim' a) # 

Methods

compare :: Elim' a -> Elim' a -> Ordering #

(<) :: Elim' a -> Elim' a -> Bool #

(<=) :: Elim' a -> Elim' a -> Bool #

(>) :: Elim' a -> Elim' a -> Bool #

(>=) :: Elim' a -> Elim' a -> Bool #

max :: Elim' a -> Elim' a -> Elim' a #

min :: Elim' a -> Elim' a -> Elim' a #

Abstract t => Abstract [t] # 

Methods

abstract :: Telescope -> [t] -> [t] #

Abstract [Occurrence] # 
Abstract [Polarity] # 

Methods

abstract :: Telescope -> [Polarity] -> [Polarity] #

Abstract t => Abstract (Maybe t) # 

Methods

abstract :: Telescope -> Maybe t -> Maybe t #

DoDrop a => Abstract (Drop a) # 

Methods

abstract :: Telescope -> Drop a -> Drop a #

Abstract a => Abstract (Case a) # 

Methods

abstract :: Telescope -> Case a -> Case a #

Abstract a => Abstract (WithArity a) # 

Methods

abstract :: Telescope -> WithArity a -> WithArity a #

Apply t => Apply [t] # 

Methods

apply :: [t] -> Args -> [t] #

applyE :: [t] -> Elims -> [t] #

Apply [NamedArg (Pattern' a)] #

Make sure we only drop variable patterns.

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] #

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] #

Apply [Occurrence] # 
Apply [Polarity] # 

Methods

apply :: [Polarity] -> Args -> [Polarity] #

applyE :: [Polarity] -> Elims -> [Polarity] #

Apply t => Apply (Maybe t) # 

Methods

apply :: Maybe t -> Args -> Maybe t #

applyE :: Maybe t -> Elims -> Maybe t #

Apply a => Apply (Ptr a) # 

Methods

apply :: Ptr a -> Args -> Ptr a #

applyE :: Ptr a -> Elims -> Ptr a #

DoDrop a => Apply (Drop a) # 

Methods

apply :: Drop a -> Args -> Drop a #

applyE :: Drop a -> Elims -> Drop a #

Apply t => Apply (Blocked t) # 

Methods

apply :: Blocked t -> Args -> Blocked t #

applyE :: Blocked t -> Elims -> Blocked t #

Subst Term a => Apply (Tele a) # 

Methods

apply :: Tele a -> Args -> Tele a #

applyE :: Tele a -> Elims -> Tele a #

Apply a => Apply (Case a) # 

Methods

apply :: Case a -> Args -> Case a #

applyE :: Case a -> Elims -> Case a #

Apply a => Apply (WithArity a) # 

Methods

apply :: WithArity a -> Args -> WithArity a #

applyE :: WithArity a -> Elims -> WithArity a #

Abstract v => Abstract (Map k v) # 

Methods

abstract :: Telescope -> Map k v -> Map k v #

Abstract v => Abstract (HashMap k v) # 

Methods

abstract :: Telescope -> HashMap k v -> HashMap k v #

(Apply a, Apply b) => Apply (a, b) # 

Methods

apply :: (a, b) -> Args -> (a, b) #

applyE :: (a, b) -> Elims -> (a, b) #

Apply v => Apply (Map k v) # 

Methods

apply :: Map k v -> Args -> Map k v #

applyE :: Map k v -> Elims -> Map k v #

Apply v => Apply (HashMap k v) # 

Methods

apply :: HashMap k v -> Args -> HashMap k v #

applyE :: HashMap k v -> Elims -> HashMap k v #

(Apply a, Apply b, Apply c) => Apply (a, b, c) # 

Methods

apply :: (a, b, c) -> Args -> (a, b, c) #

applyE :: (a, b, c) -> Elims -> (a, b, c) #