Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Treeless.Subst

Synopsis

Documentation

newtype UnderLambda Source #

Constructors

UnderLambda Any 

Instances

Instances details
Monoid UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: UnderLambda

mappend :: UnderLambda -> UnderLambda -> UnderLambda

mconcat :: [UnderLambda] -> UnderLambda

Semigroup UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: UnderLambda -> UnderLambda -> UnderLambda #

sconcat :: NonEmpty UnderLambda -> UnderLambda

stimes :: Integral b => b -> UnderLambda -> UnderLambda

Show UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> UnderLambda -> ShowS

show :: UnderLambda -> String

showList :: [UnderLambda] -> ShowS

Eq UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

(==) :: UnderLambda -> UnderLambda -> Bool

(/=) :: UnderLambda -> UnderLambda -> Bool

Ord UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: UnderLambda -> UnderLambda -> Ordering

(<) :: UnderLambda -> UnderLambda -> Bool

(<=) :: UnderLambda -> UnderLambda -> Bool

(>) :: UnderLambda -> UnderLambda -> Bool

(>=) :: UnderLambda -> UnderLambda -> Bool

max :: UnderLambda -> UnderLambda -> UnderLambda

min :: UnderLambda -> UnderLambda -> UnderLambda

newtype SeqArg Source #

Constructors

SeqArg All 

Instances

Instances details
Monoid SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: SeqArg

mappend :: SeqArg -> SeqArg -> SeqArg

mconcat :: [SeqArg] -> SeqArg

Semigroup SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: SeqArg -> SeqArg -> SeqArg #

sconcat :: NonEmpty SeqArg -> SeqArg

stimes :: Integral b => b -> SeqArg -> SeqArg

Show SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> SeqArg -> ShowS

show :: SeqArg -> String

showList :: [SeqArg] -> ShowS

Eq SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

(==) :: SeqArg -> SeqArg -> Bool

(/=) :: SeqArg -> SeqArg -> Bool

Ord SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: SeqArg -> SeqArg -> Ordering

(<) :: SeqArg -> SeqArg -> Bool

(<=) :: SeqArg -> SeqArg -> Bool

(>) :: SeqArg -> SeqArg -> Bool

(>=) :: SeqArg -> SeqArg -> Bool

max :: SeqArg -> SeqArg -> SeqArg

min :: SeqArg -> SeqArg -> SeqArg

data Occurs Source #

Constructors

Occurs Int UnderLambda SeqArg 

Instances

Instances details
Monoid Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

mempty :: Occurs

mappend :: Occurs -> Occurs -> Occurs

mconcat :: [Occurs] -> Occurs

Semigroup Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: Occurs -> Occurs -> Occurs #

sconcat :: NonEmpty Occurs -> Occurs

stimes :: Integral b => b -> Occurs -> Occurs

Show Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

showsPrec :: Int -> Occurs -> ShowS

show :: Occurs -> String

showList :: [Occurs] -> ShowS

Eq Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

(==) :: Occurs -> Occurs -> Bool

(/=) :: Occurs -> Occurs -> Bool

Ord Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: Occurs -> Occurs -> Ordering

(<) :: Occurs -> Occurs -> Bool

(<=) :: Occurs -> Occurs -> Bool

(>) :: Occurs -> Occurs -> Bool

(>=) :: Occurs -> Occurs -> Bool

max :: Occurs -> Occurs -> Occurs

min :: Occurs -> Occurs -> Occurs

once :: Occurs Source #

inSeq :: Occurs -> Occurs Source #

underLambda :: Occurs -> Occurs Source #

class HasFree a where Source #

Methods

freeVars :: a -> Map Int Occurs Source #

Instances

Instances details
HasFree TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TAlt -> Map Int Occurs Source #

HasFree TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TTerm -> Map Int Occurs Source #

HasFree Int Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Int -> Map Int Occurs Source #

HasFree a => HasFree (Binder a) Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs Source #

HasFree a => HasFree (InSeq a) Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs Source #

HasFree a => HasFree [a] Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: [a] -> Map Int Occurs Source #

(HasFree a, HasFree b) => HasFree (a, b) Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: (a, b) -> Map Int Occurs Source #

freeIn :: HasFree a => Int -> a -> Bool Source #

occursIn :: HasFree a => Int -> a -> Occurs Source #

data Binder a Source #

Constructors

Binder Int a 

Instances

Instances details
HasFree a => HasFree (Binder a) Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: Binder a -> Map Int Occurs Source #

newtype InSeq a Source #

Constructors

InSeq a 

Instances

Instances details
HasFree a => HasFree (InSeq a) Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: InSeq a -> Map Int Occurs Source #

tryStrengthen :: (HasFree a, Subst a) => Int -> a -> Maybe a Source #

Strenghtening.

Orphan instances

Subst TAlt Source # 
Instance details

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

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 #

DeBruijn TTerm Source # 
Instance details

Methods

deBruijnVar :: Int -> TTerm Source #

debruijnNamedVar :: String -> Int -> TTerm Source #

deBruijnView :: TTerm -> Maybe Int Source #