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 #