Agda-2.6.4.1: 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 #