Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Substitute

Contents

Orphan instances

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 {
- theTel :: Tele (Dom a)
- theCore :: a
}
type TelView = TelV Type
class TeleNoAbs a where
- teleNoAbs :: a -> Term -> Term
data SizeOfSort = SizeOfSort {
- szSortUniv :: Univ
- szSortSize :: Integer
}
pattern SmallSort :: Univ -> SizeOfSort
pattern LargeSort :: Univ -> Integer -> SizeOfSort
renamingR :: DeBruijn a => Permutation -> Substitution' a
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
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 TelV a Source #

Constructors

TelV
Fields theTel :: Tele (Dom a) theCore :: a

Instances

Instances details

Functor TelV Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods fmap :: (a -> b) -> TelV a -> TelV b (<$) :: a -> TelV b -> TelV a #
Show a => Show (TelV a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods showsPrec :: Int -> TelV a -> ShowS show :: TelV a -> String showList :: [TelV a] -> ShowS
(TermSubst a, Eq a) => Eq (TelV a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: TelV a -> TelV a -> Bool (/=) :: TelV a -> TelV a -> Bool
(TermSubst a, Ord a) => Ord (TelV a) Source #
Instance details Defined in Agda.TypeChecking.Substitute 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

type TelView = TelV Type Source #

class TeleNoAbs a where Source #

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term Source #

Instances

Instances details

TeleNoAbs ListTel Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #

data SizeOfSort Source #

A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).

Constructors

SizeOfSort
Fields szSortUniv :: Univ szSortSize :: Integer

pattern SmallSort :: Univ -> SizeOfSort Source #

pattern LargeSort :: Univ -> Integer -> SizeOfSort Source #

renamingR :: DeBruijn a => Permutation -> Substitution' a Source #

If permute π : [a]Γ -> [a]Δ, then applySubst (renamingR π) : Term Δ -> Term Γ

sort :: Sort -> Type Source #

mkLam :: Arg ArgName -> Term -> Term Source #

funSort :: Sort -> Sort -> Sort Source #

renaming :: forall a. DeBruijn a => Impossible -> Permutation -> Substitution' a Source #

If permute π : [a]Γ -> [a]Δ, then applySubst (renaming _ π) : Term Γ -> Term Δ

piSort :: Dom Term -> Sort -> Abs Sort -> Sort Source #

univSort :: Sort -> Sort Source #

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

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

lamView :: Term -> ([Arg ArgName], Term) Source #

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 #

argToDontCare :: Arg 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 #

teleLam :: Telescope -> Term -> Term Source #

Abstract over a telescope in a term, producing lambdas. Dumb abstraction: Always produces Abs, never NoAbs.

The implementation is sound because Telescope does not use NoAbs.

telePi_ :: Telescope -> Type -> Type Source #

Everything will be an Abs.

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #

telVars :: Int -> Telescope -> [Arg DeBruijnPattern] Source #

abstractArgs :: Abstract a => Args -> a -> a Source #

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 #

levelTm :: Level -> Term Source #

applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a Source #

fromPatternSubstitution :: PatternSubstitution -> Substitution Source #

applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a Source #

usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' 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.

bindsToTel :: [Name] -> Dom Type -> ListTel Source #

bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a Source #

bindsToTel1 :: List1 Name -> Dom Type -> ListTel Source #

namedBindsToTel :: [NamedArg Name] -> Type -> Telescope Source #

Turn a typed binding (x1 .. xn : A) into a telescope.

domFromNamedArgName :: NamedArg Name -> Dom () Source #

namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope Source #

mkPiSort :: Dom Type -> Abs Type -> Sort Source #

unlamView :: [Arg ArgName] -> Term -> Term Source #

telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type Source #

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

ssort :: Level -> Type 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

levelMax :: Integer -> [PlusLevel] -> Level Source #

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

data Substitution' a Source #

Substitutions.

Constructors

IdS	Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Impossible	Empty substitution, lifts from the empty context. First argument is `IMPOSSIBLE`. 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 Impossible !Int (Substitution' a)	Strengthening substitution. First argument is `IMPOSSIBLE`. In `'Strengthen err n ρ` the number `n` must be non-negative. This substitution should only be applied to values `t` for which none of the variables `0` up to `n - 1` are free in `t[ρ]`, and in that case `n` is subtracted from all free de Bruijn indices in `t[ρ]`. Γ ⊢ ρ : Δ \|Θ\| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @
Wk !Int (Substitution' a)	Weakening 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

Instances details

KillRange Substitution Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT Substitution Source #
InstantiateFull Substitution Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
Foldable Substitution' Source #
Instance details Defined in Agda.Syntax.Internal Methods 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 #
Instance details Defined in Agda.Syntax.Internal 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)
Functor Substitution' Source #
Instance details Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b (<$) :: a -> Substitution' b -> Substitution' a #
Eq Substitution
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Substitution -> Substitution -> Bool (/=) :: Substitution -> Substitution -> Bool
Ord Substitution
Instance details Defined in Agda.TypeChecking.Substitute Methods 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 #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source #
TermSize a => TermSize (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods termSize :: Substitution' a -> Int Source # tsize :: Substitution' a -> Sum Int Source #
NamesIn a => NamesIn (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source #
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #
EmbPrj a => EmbPrj (Substitution' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source #
EndoSubst a => Subst (Substitution' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (Substitution' a) Source # Methods applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source #
Null (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods empty :: Substitution' a Source # null :: Substitution' a -> Bool Source #
Generic (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal Associated Types type Rep (Substitution' a) :: Type -> Type Methods from :: Substitution' a -> Rep (Substitution' a) x to :: Rep (Substitution' a) x -> Substitution' a
Show a => Show (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Substitution' a -> ShowS show :: Substitution' a -> String showList :: [Substitution' a] -> ShowS
NFData a => NFData (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: Substitution' a -> ()
type SubstArg (Substitution' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a
type Rep (Substitution' a) Source #
Instance details Defined in Agda.Syntax.Internal type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.3.20230930-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 #

Orphan instances

Abstract Clause Source #
Instance details Methods abstract :: Telescope -> Clause -> Clause Source #
Abstract Sort Source #
Instance details Methods abstract :: Telescope -> Sort -> Sort Source #
Abstract Telescope Source #
Instance details Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Term Source #
Instance details Methods abstract :: Telescope -> Term -> Term Source #
Abstract Type Source #
Instance details Methods abstract :: Telescope -> Type -> Type Source #
Abstract CompiledClauses Source #
Instance details Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Abstract Definition Source #
Instance details Methods abstract :: Telescope -> Definition -> Definition Source #
Abstract Defn Source #
Instance details Methods abstract :: Telescope -> Defn -> Defn Source #
Abstract FunctionInverse Source #
Instance details Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Abstract NumGeneralizableArgs Source #
Instance details Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #
Abstract PrimFun Source #
Instance details Methods abstract :: Telescope -> PrimFun -> PrimFun Source #
Abstract ProjLams Source #
Instance details Methods abstract :: Telescope -> ProjLams -> ProjLams Source #
Abstract Projection Source #
Instance details 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 Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source #
Abstract System Source #
Instance details Methods abstract :: Telescope -> System -> System Source #
Abstract Permutation Source #
Instance details Methods abstract :: Telescope -> Permutation -> Permutation Source #
Apply BraveTerm Source #
Instance details Methods apply :: BraveTerm -> Args -> BraveTerm Source # applyE :: BraveTerm -> Elims -> BraveTerm Source #
Apply Clause Source #
Instance details Methods apply :: Clause -> Args -> Clause Source # applyE :: Clause -> Elims -> Clause Source #
Apply Sort Source #
Instance details Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
Apply Term Source #
Instance details Methods apply :: Term -> Args -> Term Source # applyE :: Term -> Elims -> Term Source #
Apply CompiledClauses Source #
Instance details Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
Apply Definition Source #
Instance details Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
Apply Defn Source #
Instance details Methods apply :: Defn -> Args -> Defn Source # applyE :: Defn -> Elims -> Defn Source #
Apply DisplayTerm Source #
Instance details Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source #
Apply ExtLamInfo Source #
Instance details Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #
Apply FunctionInverse Source #
Instance details Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
Apply NumGeneralizableArgs Source #
Instance details Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #
Apply PrimFun Source #
Instance details Methods apply :: PrimFun -> Args -> PrimFun Source # applyE :: PrimFun -> Elims -> PrimFun Source #
Apply ProjLams Source #
Instance details Methods apply :: ProjLams -> Args -> ProjLams Source # applyE :: ProjLams -> Elims -> ProjLams Source #
Apply Projection Source #
Instance details Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source #
Apply RewriteRule Source #
Instance details Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source #
Apply System Source #
Instance details Methods apply :: System -> Args -> System Source # applyE :: System -> Elims -> System Source #
Apply Permutation Source #
Instance details Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source #
Subst ProblemEq Source #
Instance details Associated Types type SubstArg ProblemEq Source # Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #
Subst Name Source #
Instance details Associated Types type SubstArg Name Source # Methods applySubst :: Substitution' (SubstArg Name) -> Name -> Name Source #
Subst BraveTerm Source #
Instance details Associated Types type SubstArg BraveTerm Source # Methods applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source #
Subst ConPatternInfo Source #
Instance details Associated Types type SubstArg ConPatternInfo Source # Methods applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source #
Subst DeBruijnPattern Source #
Instance details Associated Types type SubstArg DeBruijnPattern Source # Methods applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #
Subst EqualityTypeData Source #
Instance details Associated Types type SubstArg EqualityTypeData Source # Methods applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source #
Subst EqualityView Source #
Instance details Associated Types type SubstArg EqualityView Source # Methods applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source #
Subst Pattern Source #
Instance details Associated Types type SubstArg Pattern Source # Methods applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source #
Subst Term Source #
Instance details Associated Types type SubstArg Term Source # Methods applySubst :: Substitution' (SubstArg Term) -> Term -> Term Source #
Subst Range Source #
Instance details Associated Types type SubstArg Range Source # Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source #
Subst Candidate Source #
Instance details Associated Types type SubstArg Candidate Source # Methods applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate Source #
Subst CompareAs Source #
Instance details Associated Types type SubstArg CompareAs Source # Methods applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs Source #
Subst Constraint Source #
Instance details Associated Types type SubstArg Constraint Source # Methods applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint Source #
Subst DisplayForm Source #
Instance details Associated Types type SubstArg DisplayForm Source # Methods applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm Source #
Subst DisplayTerm Source #
Instance details Associated Types type SubstArg DisplayTerm Source # Methods applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm Source #
Subst LetBinding Source #
Instance details Associated Types type SubstArg LetBinding Source # Methods applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding Source #
Subst NLPSort Source #
Instance details Associated Types type SubstArg NLPSort Source # Methods applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort Source #
Subst NLPType Source #
Instance details Associated Types type SubstArg NLPType Source # Methods applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType Source #
Subst NLPat Source #
Instance details Associated Types type SubstArg NLPat Source # Methods applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat Source #
Subst RewriteRule Source #
Instance details Associated Types type SubstArg RewriteRule Source # Methods applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule Source #
Subst () Source #
Instance details Associated Types type SubstArg () Source # Methods applySubst :: Substitution' (SubstArg ()) -> () -> () Source #
DeBruijn BraveTerm Source #
Instance details Methods deBruijnVar :: Int -> BraveTerm Source # debruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> Maybe Int Source #
DeBruijn NLPat Source #
Instance details Methods deBruijnVar :: Int -> NLPat Source # debruijnNamedVar :: String -> Int -> NLPat Source # deBruijnView :: NLPat -> Maybe Int Source #
Eq Level Source #
Instance details Methods (==) :: Level -> Level -> Bool (/=) :: Level -> Level -> Bool
Eq NotBlocked Source #
Instance details Methods (==) :: NotBlocked -> NotBlocked -> Bool (/=) :: NotBlocked -> NotBlocked -> Bool
Eq PlusLevel Source #
Instance details Methods (==) :: PlusLevel -> PlusLevel -> Bool (/=) :: PlusLevel -> PlusLevel -> Bool
Eq Sort Source #
Instance details Methods (==) :: Sort -> Sort -> Bool (/=) :: Sort -> Sort -> Bool
Eq Substitution Source #
Instance details Methods (==) :: Substitution -> Substitution -> Bool (/=) :: Substitution -> Substitution -> Bool
Eq Term Source #	Syntactic `Term` equality, ignores stuff below `DontCare` and sharing.
Instance details Methods (==) :: Term -> Term -> Bool (/=) :: Term -> Term -> Bool
Eq Candidate Source #
Instance details Methods (==) :: Candidate -> Candidate -> Bool (/=) :: Candidate -> Candidate -> Bool
Eq CandidateKind Source #
Instance details Methods (==) :: CandidateKind -> CandidateKind -> Bool (/=) :: CandidateKind -> CandidateKind -> Bool
Eq Section Source #
Instance details Methods (==) :: Section -> Section -> Bool (/=) :: Section -> Section -> Bool
Ord Level Source #
Instance details 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 PlusLevel Source #
Instance details Methods compare :: PlusLevel -> PlusLevel -> Ordering (<) :: PlusLevel -> PlusLevel -> Bool (<=) :: PlusLevel -> PlusLevel -> Bool (>) :: PlusLevel -> PlusLevel -> Bool (>=) :: PlusLevel -> PlusLevel -> Bool max :: PlusLevel -> PlusLevel -> PlusLevel min :: PlusLevel -> PlusLevel -> PlusLevel
Ord Sort Source #
Instance details 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 Substitution Source #
Instance details Methods compare :: Substitution -> Substitution -> Ordering (<) :: Substitution -> Substitution -> Bool (<=) :: Substitution -> Substitution -> Bool (>) :: Substitution -> Substitution -> Bool (>=) :: Substitution -> Substitution -> Bool max :: Substitution -> Substitution -> Substitution min :: Substitution -> Substitution -> Substitution
Ord Term Source #
Instance details 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
Abstract a => Abstract (Case a) Source #
Instance details Methods abstract :: Telescope -> Case a -> Case a Source #
Abstract a => Abstract (WithArity a) Source #
Instance details Methods abstract :: Telescope -> WithArity a -> WithArity a Source #
DoDrop a => Abstract (Drop a) Source #
Instance details Methods abstract :: Telescope -> Drop a -> Drop a Source #
Abstract t => Abstract (Maybe t) Source #
Instance details Methods abstract :: Telescope -> Maybe t -> Maybe t Source #
Abstract [Polarity] Source #
Instance details Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Abstract [Occurrence] Source #
Instance details Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Abstract t => Abstract [t] Source #
Instance details Methods abstract :: Telescope -> [t] -> [t] Source #
Apply t => Apply (Blocked t) Source #
Instance details Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
TermSubst a => Apply (Tele a) Source #
Instance details Methods apply :: Tele a -> Args -> Tele a Source # applyE :: Tele a -> Elims -> Tele a Source #
Apply a => Apply (Case a) Source #
Instance details Methods apply :: Case a -> Args -> Case a Source # applyE :: Case a -> Elims -> Case a Source #
Apply a => Apply (WithArity a) Source #
Instance details Methods apply :: WithArity a -> Args -> WithArity a Source # applyE :: WithArity a -> Elims -> WithArity a Source #
DoDrop a => Apply (Drop a) Source #
Instance details Methods apply :: Drop a -> Args -> Drop a Source # applyE :: Drop a -> Elims -> Drop a Source #
Apply t => Apply (Maybe t) Source #
Instance details Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe t Source #
Apply t => Apply (Maybe t) Source #
Instance details 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 Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
Apply [Polarity] Source #
Instance details Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #
Apply [Occurrence] Source #
Instance details Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #
Apply t => Apply [t] Source #
Instance details Methods apply :: [t] -> Args -> [t] Source # applyE :: [t] -> Elims -> [t] Source #
Subst a => Subst (Arg a) Source #
Instance details Associated Types type SubstArg (Arg a) Source # Methods applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #
Subst a => Subst (WithHiding a) Source #
Instance details Associated Types type SubstArg (WithHiding a) Source # Methods applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source #
Subst a => Subst (Abs a) Source #
Instance details Associated Types type SubstArg (Abs a) Source # Methods applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #
Subst a => Subst (Blocked a) Source #
Instance details Associated Types type SubstArg (Blocked a) Source # Methods applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source #
Subst a => Subst (Level' a) Source #
Instance details Associated Types type SubstArg (Level' a) Source # Methods applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source #
Subst a => Subst (PlusLevel' a) Source #
Instance details Associated Types type SubstArg (PlusLevel' a) Source # Methods applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source #
(Coercible a Term, Subst a) => Subst (Sort' a) Source #
Instance details Associated Types type SubstArg (Sort' a) Source # Methods applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source #
EndoSubst a => Subst (Substitution' a) Source #
Instance details Associated Types type SubstArg (Substitution' a) Source # Methods applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source #
Subst a => Subst (Tele a) Source #
Instance details Associated Types type SubstArg (Tele a) Source # Methods applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source #
Subst a => Subst (Elim' a) Source #
Instance details Associated Types type SubstArg (Elim' a) Source # Methods applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a Source #
Subst a => Subst (Maybe a) Source #
Instance details Associated Types type SubstArg (Maybe a) Source # Methods applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a Source #
Subst a => Subst [a] Source #
Instance details Associated Types type SubstArg [a] Source # Methods applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a] Source #
DeBruijn a => DeBruijn (Pattern' a) Source #
Instance details Methods deBruijnVar :: Int -> Pattern' a Source # debruijnNamedVar :: String -> Int -> Pattern' a Source # deBruijnView :: Pattern' a -> Maybe Int Source #
(Subst a, Eq a) => Eq (Abs a) Source #	Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.
Instance details Methods (==) :: Abs a -> Abs a -> Bool (/=) :: Abs a -> Abs a -> Bool
Eq t => Eq (Blocked t) Source #
Instance details Methods (==) :: Blocked t -> Blocked t -> Bool (/=) :: Blocked t -> Blocked t -> Bool
Eq a => Eq (Pattern' a) Source #
Instance details Methods (==) :: Pattern' a -> Pattern' a -> Bool (/=) :: Pattern' a -> Pattern' a -> Bool
(Subst a, Eq a) => Eq (Tele a) Source #
Instance details Methods (==) :: Tele a -> Tele a -> Bool (/=) :: Tele a -> Tele a -> Bool
Eq a => Eq (Type' a) Source #	Syntactic `Type` equality, ignores sort annotations.
Instance details Methods (==) :: Type' a -> Type' a -> Bool (/=) :: Type' a -> Type' a -> Bool
(Subst a, Eq a) => Eq (Elim' a) Source #
Instance details Methods (==) :: Elim' a -> Elim' a -> Bool (/=) :: Elim' a -> Elim' a -> Bool
(Subst a, Ord a) => Ord (Abs a) Source #
Instance details 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
Ord a => Ord (Dom a) Source #
Instance details Methods compare :: Dom a -> Dom a -> Ordering (<) :: Dom a -> Dom a -> Bool (<=) :: Dom a -> Dom a -> Bool (>) :: Dom a -> Dom a -> Bool (>=) :: Dom a -> Dom a -> Bool max :: Dom a -> Dom a -> Dom a min :: Dom a -> Dom a -> Dom a
(Subst a, Ord a) => Ord (Tele a) Source #
Instance details 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) Source #
Instance details 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 a, Ord a) => Ord (Elim' a) Source #
Instance details 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 v => Abstract (Map k v) Source #
Instance details Methods abstract :: Telescope -> Map k v -> Map k v Source #
Abstract v => Abstract (HashMap k v) Source #
Instance details Methods abstract :: Telescope -> HashMap k v -> HashMap k v Source #
Apply v => Apply (Map k v) Source #
Instance details 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 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 Methods apply :: (a, b) -> Args -> (a, b) Source # applyE :: (a, b) -> Elims -> (a, b) Source #
Subst a => Subst (Named name a) Source #
Instance details Associated Types type SubstArg (Named name a) Source # 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 Associated Types type SubstArg (Dom' a b) Source # 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 Associated Types type SubstArg (Type'' a b) Source # Methods applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source #
(Ord k, Subst a) => Subst (Map k a) Source #
Instance details Associated Types type SubstArg (Map k a) Source # 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 Associated Types type SubstArg (a, b) Source # Methods applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b) Source #
(Apply a, Apply b, Apply c) => Apply (a, b, c) Source #
Instance details Methods apply :: (a, b, c) -> Args -> (a, b, c) Source # applyE :: (a, b, c) -> Elims -> (a, b, c) Source #
(Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) Source #
Instance details Associated Types type SubstArg (a, b, c) Source # 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 Associated Types type SubstArg (a, b, c, d) Source # Methods applySubst :: Substitution' (SubstArg (a, b, c, d)) -> (a, b, c, d) -> (a, b, c, d) Source #