Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Compiler.Treeless.Subst

Contents

Orphan instances

Synopsis

newtype UnderLambda = UnderLambda Any
newtype SeqArg = SeqArg All
data Occurs = Occurs Int UnderLambda SeqArg
once :: Occurs
inSeq :: Occurs -> Occurs
underLambda :: Occurs -> Occurs
class HasFree a where
- freeVars :: a -> Map Int Occurs
freeIn :: HasFree a => Int -> a -> Bool
occursIn :: HasFree a => Int -> a -> Occurs
data Binder a = Binder Int a
newtype InSeq a = InSeq a
tryStrengthen :: (HasFree a, Subst a) => Int -> a -> Maybe a

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 Source # Methods applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source #
Subst TTerm Source #
Instance details Associated Types type SubstArg TTerm Source # 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 #