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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Substitute.Class

Contents

- Application
- Abstraction
- Substitution and shifting/weakening/strengthening
  - Identity instances
- Explicit substitutions
- Functions on abstractions

Synopsis

- class Apply t where
  - apply :: t -> Args -> t
  - applyE :: t -> Elims -> t
- applys :: Apply t => t -> [Term] -> t
- apply1 :: Apply t => t -> Term -> t
- apply2 :: Apply t => t -> Term -> Term -> t
- class Abstract t where
  - abstract :: Telescope -> t -> t
- class DeBruijn (SubstArg a) => Subst a where
  - type SubstArg a
  - applySubst :: Substitution' (SubstArg a) -> a -> a
- type SubstWith t a = (Subst a, SubstArg a ~ t)
- type EndoSubst a = SubstWith a a
- type TermSubst a = SubstWith Term a
- raise :: Subst a => Nat -> a -> a
- raiseFrom :: Subst a => Nat -> Nat -> a -> a
- subst :: Subst a => Int -> SubstArg a -> a -> a
- strengthen :: Subst a => Impossible -> a -> a
- substUnder :: Subst a => Nat -> SubstArg a -> a -> a
- isNoAbs :: (Free a, Subst a) => Abs a -> Maybe a
- newtype NoSubst t a = NoSubst {
  - unNoSubst :: a
  }
- idS :: Substitution' a
- wkS :: Int -> Substitution' a -> Substitution' a
- raiseS :: Int -> Substitution' a
- consS :: DeBruijn a => a -> Substitution' a -> Substitution' a
- singletonS :: DeBruijn a => Int -> a -> Substitution' a
- inplaceS :: EndoSubst a => Int -> a -> Substitution' a
- liftS :: Int -> Substitution' a -> Substitution' a
- dropS :: Int -> Substitution' a -> Substitution' a
- composeS :: EndoSubst a => Substitution' a -> Substitution' a -> Substitution' a
- splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
- (++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
- prependS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
- parallelS :: DeBruijn a => [a] -> Substitution' a
- strengthenS :: Impossible -> Int -> Substitution' a
- strengthenS' :: Impossible -> Int -> Substitution' a -> Substitution' a
- lookupS :: EndoSubst a => Substitution' a -> Nat -> a
- listS :: EndoSubst a => [(Int, a)] -> Substitution' a
- raiseFromS :: Nat -> Nat -> Substitution' a
- absApp :: Subst a => Abs a -> SubstArg a -> a
- lazyAbsApp :: Subst a => Abs a -> SubstArg a -> a
- noabsApp :: Subst a => Impossible -> Abs a -> a
- absBody :: Subst a => Abs a -> a
- mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a
- reAbs :: (Subst a, Free a) => Abs a -> Abs a

# Application

class Apply t where Source #

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Minimal complete definition

applyE

Methods

apply :: t -> Args -> t Source #

applyE :: t -> Elims -> t Source #

#### Instances

Instances details

Apply BraveTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: BraveTerm -> Args -> BraveTerm Source # applyE :: BraveTerm -> Elims -> BraveTerm Source #
Apply Clause Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Clause -> Args -> Clause Source # applyE :: Clause -> Elims -> Clause Source #
Apply Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
Apply Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Term -> Args -> Term Source # applyE :: Term -> Elims -> Term Source #
Apply CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
Apply Definition Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
Apply Defn Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Defn -> Args -> Defn Source # applyE :: Defn -> Elims -> Defn Source #
Apply DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source #
Apply ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #
Apply FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
Apply NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #
Apply PrimFun Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: PrimFun -> Args -> PrimFun Source # applyE :: PrimFun -> Elims -> PrimFun Source #
Apply ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ProjLams -> Args -> ProjLams Source # applyE :: ProjLams -> Elims -> ProjLams Source #
Apply Projection Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source #
Apply RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source #
Apply System Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: System -> Args -> System Source # applyE :: System -> Elims -> System Source #
Apply Permutation Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source #
Apply t => Apply (Blocked t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
TermSubst a => Apply (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Tele a -> Args -> Tele a Source # applyE :: Tele a -> Elims -> Tele a Source #
Apply a => Apply (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Case a -> Args -> Case a Source # applyE :: Case a -> Elims -> Case a Source #
Apply a => Apply (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: WithArity a -> Args -> WithArity a Source # applyE :: WithArity a -> Elims -> WithArity a Source #
DoDrop a => Apply (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Drop a -> Args -> Drop a Source # applyE :: Drop a -> Elims -> Drop a Source #
Apply t => Apply (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe t Source #
Apply t => Apply (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe t Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
Apply [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #
Apply [Occurrence] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #
Apply t => Apply [t] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [t] -> Args -> [t] Source # applyE :: [t] -> Elims -> [t] Source #
Apply v => Apply (Map k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Map k v -> Args -> Map k v Source # applyE :: Map k v -> Elims -> Map k v Source #
Apply v => Apply (HashMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: HashMap k v -> Args -> HashMap k v Source # applyE :: HashMap k v -> Elims -> HashMap k v Source #
(Apply a, Apply b) => Apply (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: (a, b) -> Args -> (a, b) Source # applyE :: (a, b) -> Elims -> (a, b) Source #
(Apply a, Apply b, Apply c) => Apply (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: (a, b, c) -> Args -> (a, b, c) Source # applyE :: (a, b, c) -> Elims -> (a, b, c) Source #

applys :: Apply t => t -> [Term] -> t Source #

Apply to some default arguments.

apply1 :: Apply t => t -> Term -> t Source #

Apply to a single default argument.

apply2 :: Apply t => t -> Term -> Term -> t Source #

Apply to two default arguments.

# Abstraction

class Abstract t where Source #

`(abstract args v) `apply` args --> v[args]`.

Methods

abstract :: Telescope -> t -> t Source #

#### Instances

Instances details

Abstract Clause Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Clause -> Clause Source #
Abstract Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Sort -> Sort Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Term -> Term Source #
Abstract Type Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type Source #
Abstract CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Abstract Definition Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Definition -> Definition Source #
Abstract Defn Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Defn -> Defn Source #
Abstract FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Abstract NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #
Abstract PrimFun Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> PrimFun -> PrimFun Source #
Abstract ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> ProjLams -> ProjLams Source #
Abstract Projection Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Projection -> Projection Source #
Abstract RewriteRule Source # | `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'.
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source #
Abstract System Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> System -> System Source #
Abstract Permutation Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Permutation -> Permutation Source #
Abstract a => Abstract (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Case a -> Case a Source #
Abstract a => Abstract (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> WithArity a -> WithArity a Source #
DoDrop a => Abstract (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Drop a -> Drop a Source #
Abstract t => Abstract (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Maybe t -> Maybe t Source #
Abstract [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Abstract [Occurrence] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Abstract t => Abstract [t] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [t] -> [t] Source #
Abstract v => Abstract (Map k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Map k v -> Map k v Source #
Abstract v => Abstract (HashMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> HashMap k v -> HashMap k v Source #

# Substitution and shifting/weakening/strengthening

class DeBruijn (SubstArg a) => Subst a where Source #

Apply a substitution.

Minimal complete definition

Nothing

Associated Types

type SubstArg a Source #

Methods

applySubst :: Substitution' (SubstArg a) -> a -> a Source #

default applySubst :: forall (f :: Type -> Type) b. (a ~ f b, Functor f, Subst b, SubstArg a ~ SubstArg b) => Substitution' (SubstArg a) -> a -> a Source #

#### Instances

Instances details

Subst ProblemEq Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term

Methods

applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #

Subst Name Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Name |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Name = Term

Methods

applySubst :: Substitution' (SubstArg Name) -> Name -> Name Source #

Subst QName Source # |

Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg QName |
Instance details Defined in Agda.TypeChecking.Substitute.Class type SubstArg QName = Term

Methods

applySubst :: Substitution' (SubstArg QName) -> QName -> QName Source #

Subst BraveTerm Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg BraveTerm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg BraveTerm = BraveTerm

Methods

applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source #

Subst ConPatternInfo Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ConPatternInfo = Term

Methods

applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source #

Subst DeBruijnPattern Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

Subst EqualityTypeData Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityTypeData |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityTypeData = Term

Methods

applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source #

Subst EqualityView Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityView |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityView = Term

Methods

applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source #

Subst Pattern Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Pattern |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Pattern = Term

Methods

applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source #

Subst Term Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Term = Term

Methods

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

Subst Range Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term

Methods

applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #

Subst TAlt Source # |

Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TAlt |
Instance details Defined in Agda.Compiler.Treeless.Subst type SubstArg TAlt = TTerm

Methods

applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source #

Subst TTerm Source # |

Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TTerm |
Instance details Defined in Agda.Compiler.Treeless.Subst type SubstArg TTerm = TTerm

Methods

applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm Source #

Subst SplitPattern Source # |

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern |
Instance details Defined in Agda.TypeChecking.Coverage.Match type SubstArg SplitPattern = SplitPattern

Methods

applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source #

Subst Candidate Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Candidate |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Candidate = Term

Methods

applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate Source #

Subst CompareAs Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg CompareAs |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg CompareAs = Term

Methods

applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs Source #

Subst Constraint Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Constraint |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Constraint = Term

Methods

applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint Source #

Subst DisplayForm Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DisplayForm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DisplayForm = Term

Methods

applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm Source #

Subst DisplayTerm Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DisplayTerm |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DisplayTerm = Term

Methods

applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm Source #

Subst LetBinding Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg LetBinding |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg LetBinding = Term

Methods

applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding Source #

Subst NLPSort Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPSort |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPSort = NLPat

Methods

applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort Source #

Subst NLPType Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPType |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPType = NLPat

Methods

applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType Source #

Subst NLPat Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPat |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPat = NLPat

Methods

applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat Source #

Subst RewriteRule Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg RewriteRule |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg RewriteRule = NLPat

Methods

applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule Source #

Subst ContextEntry Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ContextEntry |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ContextEntry = Term

Methods

applySubst :: Substitution' (SubstArg ContextEntry) -> ContextEntry -> ContextEntry Source #

Subst CType Source # |

Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg CType |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg CType = Term

Methods

applySubst :: Substitution' (SubstArg CType) -> CType -> CType Source #

Subst LType Source # |

Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg LType |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical type SubstArg LType = Term

Methods

applySubst :: Substitution' (SubstArg LType) -> LType -> LType Source #

Subst AbsurdPattern Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AbsurdPattern |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AbsurdPattern = Term

Methods

applySubst :: Substitution' (SubstArg AbsurdPattern) -> AbsurdPattern -> AbsurdPattern Source #

Subst AsBinding Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AsBinding |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AsBinding = Term

Methods

applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding Source #

Subst DotPattern Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg DotPattern |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg DotPattern = Term

Methods

applySubst :: Substitution' (SubstArg DotPattern) -> DotPattern -> DotPattern Source #

Subst SizeConstraint Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeConstraint = Term

Methods

applySubst :: Substitution' (SubstArg SizeConstraint) -> SizeConstraint -> SizeConstraint Source #

Subst SizeMeta Source # |

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeMeta |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg SizeMeta = Term

Methods

applySubst :: Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta Source #

Subst Boundary Source # | Substitution into a `Boundary` a priori creates a `TmBoundary` which we convert back via `varBoundary`. A priori, this is a partial operation.

Instance details

Defined in Agda.TypeChecking.Telescope

Associated Types

type SubstArg Boundary |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg Boundary = Term

Methods

applySubst :: Substitution' (SubstArg Boundary) -> Boundary -> Boundary Source #

Subst TmBoundary Source # |

Instance details

Defined in Agda.TypeChecking.Telescope

Associated Types

type SubstArg TmBoundary |
Instance details Defined in Agda.TypeChecking.Telescope type SubstArg TmBoundary = Term

Methods

applySubst :: Substitution' (SubstArg TmBoundary) -> TmBoundary -> TmBoundary Source #

Subst () Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg () |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg () = Term

Methods

applySubst :: Substitution' (SubstArg ()) -> () -> () Source #

Subst a => Subst (Arg a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Arg a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Arg a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #

Subst a => Subst (Ranged a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Ranged a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Ranged a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Ranged a)) -> Ranged a -> Ranged a Source #

Subst a => Subst (WithHiding a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (WithHiding a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (WithHiding a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source #

Subst a => Subst (Abs a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Abs a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #

Subst a => Subst (Blocked a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source #

Subst a => Subst (Level' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Level' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Level' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source #

Subst a => Subst (PlusLevel' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (PlusLevel' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (PlusLevel' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source #

(Coercible a Term, Subst a) => Subst (Sort' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Sort' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Sort' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source #

EndoSubst a => Subst (Substitution' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a

Methods

applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source #

Subst a => Subst (Tele a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Tele a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source #

Subst a => Subst (Elim' a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Elim' a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Elim' a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a Source #

Subst t => Subst (SingleLevel' t) Source # |

Instance details

Defined in Agda.TypeChecking.Level

Associated Types

type SubstArg (SingleLevel' t) |
Instance details Defined in Agda.TypeChecking.Level type SubstArg (SingleLevel' t) = SubstArg t

Methods

applySubst :: Substitution' (SubstArg (SingleLevel' t)) -> SingleLevel' t -> SingleLevel' t Source #

Subst a => Subst (AbsN a) Source # |

Instance details

Defined in Agda.TypeChecking.Names

Associated Types

type SubstArg (AbsN a) |
Instance details Defined in Agda.TypeChecking.Names type SubstArg (AbsN a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (AbsN a)) -> AbsN a -> AbsN a Source #

Subst (Problem a) Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg (Problem a) |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg (Problem a) = Term

Methods

applySubst :: Substitution' (SubstArg (Problem a)) -> Problem a -> Problem a Source #

Subst a => Subst (List1 a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (List1 a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (List1 a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (List1 a)) -> List1 a -> List1 a Source #

Subst a => Subst (Maybe a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Maybe a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Maybe a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a Source #

Subst a => Subst [a] Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg [a] |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg [a] = SubstArg a

Methods

applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a] Source #

Subst a => Subst (Named name a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Named name a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Named name a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Dom' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source #

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Type'' a b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Type'' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg (SizeExpr' NamedRigid SizeMeta) |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term

Methods

applySubst :: Substitution' (SubstArg (SizeExpr' NamedRigid SizeMeta)) -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #

DeBruijn t => Subst (NoSubst t a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg (NoSubst t a) |
Instance details Defined in Agda.TypeChecking.Substitute.Class type SubstArg (NoSubst t a) = t

Methods

applySubst :: Substitution' (SubstArg (NoSubst t a)) -> NoSubst t a -> NoSubst t a Source #

(Ord k, Subst a) => Subst (Map k a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Map k a) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Map k a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Map k a)) -> Map k a -> Map k a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (a, b) = SubstArg a

Methods

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

(Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b, c) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (a, b, c) = SubstArg a

Methods

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

(Subst a, Subst b, Subst c, Subst d, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c, SubstArg c ~ SubstArg d) => Subst (a, b, c, d) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b, c, d) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (a, b, c, d) = SubstArg a

Methods

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

type SubstWith t a = (Subst a, SubstArg a ~ t) Source #

Simple constraint alias for a `Subst` instance `a` with arg type `t`.

type EndoSubst a = SubstWith a a Source #

`Subst` instance whose agument type is itself

type TermSubst a = SubstWith Term a Source #

`Subst` instance whose argument type is `Term`

raise :: Subst a => Nat -> a -> a Source #

Raise de Bruijn index, i.e. weakening

raiseFrom :: Subst a => Nat -> Nat -> a -> a Source #

subst :: Subst a => Int -> SubstArg a -> a -> a Source #

Replace de Bruijn index i by a `Term` in something.

strengthen :: Subst a => Impossible -> a -> a Source #

substUnder :: Subst a => Nat -> SubstArg a -> a -> a Source #

Replace what is now de Bruijn index 0, but go under n binders. `substUnder n u == subst n (raise n u)`.

isNoAbs :: (Free a, Subst a) => Abs a -> Maybe a Source #

Checks whether the variable bound by the abstraction is actually used, and, if not, returns the term within, `strengthen`ed to live in the context outside the abstraction. See also `isBinderUsed`.

## Identity instances

newtype NoSubst t a Source #

Wrapper for types that do not contain variables (so applying a substitution is the identity). Useful if you have a structure of types that support substitution mixed with types that don't and need to apply a substitution to the full structure.

Constructors

NoSubst |

Fields

- unNoSubst :: a

#### Instances

Instances details

Functor (NoSubst t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods fmap :: (a -> b) -> NoSubst t a -> NoSubst t b Source # (<$) :: a -> NoSubst t b -> NoSubst t a Source #
DeBruijn t => Subst (NoSubst t a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg (NoSubst t a) |
Instance details Defined in Agda.TypeChecking.Substitute.Class type SubstArg (NoSubst t a) = t

Methods

applySubst :: Substitution' (SubstArg (NoSubst t a)) -> NoSubst t a -> NoSubst t a Source #

NFData a => NFData (NoSubst t a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods rnf :: NoSubst t a -> () Source #
Generic (NoSubst t a) Source # |

Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type Rep (NoSubst t a) |
Instance details Defined in Agda.TypeChecking.Substitute.Class type Rep (NoSubst t a) = D1 ('MetaData "NoSubst" "Agda.TypeChecking.Substitute.Class" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "NoSubst" 'PrefixI 'True) (S1 ('MetaSel ('Just "unNoSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

from :: NoSubst t a -> Rep (NoSubst t a) x Source #

to :: Rep (NoSubst t a) x -> NoSubst t a Source #

type SubstArg (NoSubst t a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class type SubstArg (NoSubst t a) = t
type Rep (NoSubst t a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class type Rep (NoSubst t a) = D1 ('MetaData "NoSubst" "Agda.TypeChecking.Substitute.Class" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "NoSubst" 'PrefixI 'True) (S1 ('MetaSel ('Just "unNoSubst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

# Explicit substitutions

idS :: Substitution' a Source #

wkS :: Int -> Substitution' a -> Substitution' a Source #

raiseS :: Int -> Substitution' a Source #

consS :: DeBruijn a => a -> Substitution' a -> Substitution' a Source #

singletonS :: DeBruijn a => Int -> a -> Substitution' a Source #

To replace index `n` by term `u`, do `applySubst (singletonS n u)`. `Γ, Δ ⊢ u : A --------------------------------- Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ`

inplaceS :: EndoSubst a => Int -> a -> Substitution' a Source #

Single substitution without disturbing any deBruijn indices. `Γ, A, Δ ⊢ u : A --------------------------------- Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ`

liftS :: Int -> Substitution' a -> Substitution' a Source #

Lift a substitution under k binders.

dropS :: Int -> Substitution' a -> Substitution' a Source #

            Γ ⊢ ρ : Δ, Ψ
         -------------------
         Γ ⊢ dropS |Ψ| ρ : Δ

composeS :: EndoSubst a => Substitution' a -> Substitution' a -> Substitution' a Source #

    applySubst (ρ composeS σ) v == applySubst ρ (applySubst σ v)

splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a) Source #

(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4 Source #

prependS :: DeBruijn a => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a Source #

         Γ ⊢ ρ : Δ  Γ ⊢ reverse vs : Θ
         ----------------------------- (treating Nothing as having any type)
           Γ ⊢ prependS vs ρ : Δ, Θ

parallelS :: DeBruijn a => [a] -> Substitution' a Source #

           Γ ⊢ reverse vs : Δ
         -----------------------------
           Γ ⊢ parallelS vs ρ : Γ, Δ

Note the `Γ` in `Γ, Δ`.

strengthenS :: Impossible -> Int -> Substitution' a Source #

Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ

strengthenS' :: Impossible -> Int -> Substitution' a -> Substitution' a Source #

A "smart" variant of `Strengthen`. If `strengthenS` is applied to a substitution with an outermost `Strengthen` constructor, then the "error message" of that constructor is discarded in favour of the `Impossible` argument of this function.

lookupS :: EndoSubst a => Substitution' a -> Nat -> a Source #

listS :: EndoSubst a => [(Int, a)] -> Substitution' a Source #

lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.

raiseFromS :: Nat -> Nat -> Substitution' a Source #

    Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ

# Functions on abstractions

absApp :: Subst a => Abs a -> SubstArg a -> a Source #

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst a => Abs a -> SubstArg a -> a Source #

Instantiate an abstraction. Lazy in the term, which allow it to be IMPOSSIBLE in the case where the variable shouldn't be used but we cannot use `noabsApp`. Used in Apply.

noabsApp :: Subst a => Impossible -> Abs a -> a Source #

Instantiate an abstraction that doesn't use its argument.

absBody :: Subst a => Abs a -> a Source #

mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a Source #

reAbs :: (Subst a, Free a) => Abs a -> Abs a Source #