Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 -> IntMap 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 Source # mappend :: UnderLambda -> UnderLambda -> UnderLambda Source # mconcat :: [UnderLambda] -> UnderLambda Source #
Semigroup UnderLambda Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: UnderLambda -> UnderLambda -> UnderLambda Source # sconcat :: NonEmpty UnderLambda -> UnderLambda Source # stimes :: Integral b => b -> UnderLambda -> UnderLambda Source #
Show UnderLambda Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods showsPrec :: Int -> UnderLambda -> ShowS Source # show :: UnderLambda -> String Source # showList :: [UnderLambda] -> ShowS Source #
Eq UnderLambda Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (==) :: UnderLambda -> UnderLambda -> Bool Source # (/=) :: UnderLambda -> UnderLambda -> Bool Source #
Ord UnderLambda Source # |

Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

compare :: UnderLambda -> UnderLambda -> Ordering Source #

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

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

(>) :: UnderLambda -> UnderLambda -> Bool Source #

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

max :: UnderLambda -> UnderLambda -> UnderLambda Source #

min :: UnderLambda -> UnderLambda -> UnderLambda Source #

newtype SeqArg Source #

Constructors

SeqArg All |

#### Instances

Instances details

Monoid SeqArg Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods mempty :: SeqArg Source # mappend :: SeqArg -> SeqArg -> SeqArg Source # mconcat :: [SeqArg] -> SeqArg Source #
Semigroup SeqArg Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: SeqArg -> SeqArg -> SeqArg Source # sconcat :: NonEmpty SeqArg -> SeqArg Source # stimes :: Integral b => b -> SeqArg -> SeqArg Source #
Show SeqArg Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods showsPrec :: Int -> SeqArg -> ShowS Source # show :: SeqArg -> String Source # showList :: [SeqArg] -> ShowS Source #
Eq SeqArg Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (==) :: SeqArg -> SeqArg -> Bool Source # (/=) :: SeqArg -> SeqArg -> Bool Source #
Ord SeqArg Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods compare :: SeqArg -> SeqArg -> Ordering Source # (<) :: SeqArg -> SeqArg -> Bool Source # (<=) :: SeqArg -> SeqArg -> Bool Source # (>) :: SeqArg -> SeqArg -> Bool Source # (>=) :: SeqArg -> SeqArg -> Bool Source # max :: SeqArg -> SeqArg -> SeqArg Source # min :: SeqArg -> SeqArg -> SeqArg Source #

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 Source # mappend :: Occurs -> Occurs -> Occurs Source # mconcat :: [Occurs] -> Occurs Source #
Semigroup Occurs Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: Occurs -> Occurs -> Occurs Source # sconcat :: NonEmpty Occurs -> Occurs Source # stimes :: Integral b => b -> Occurs -> Occurs Source #
Show Occurs Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods showsPrec :: Int -> Occurs -> ShowS Source # show :: Occurs -> String Source # showList :: [Occurs] -> ShowS Source #
Eq Occurs Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (==) :: Occurs -> Occurs -> Bool Source # (/=) :: Occurs -> Occurs -> Bool Source #
Ord Occurs Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods compare :: Occurs -> Occurs -> Ordering Source # (<) :: Occurs -> Occurs -> Bool Source # (<=) :: Occurs -> Occurs -> Bool Source # (>) :: Occurs -> Occurs -> Bool Source # (>=) :: Occurs -> Occurs -> Bool Source # max :: Occurs -> Occurs -> Occurs Source # min :: Occurs -> Occurs -> Occurs Source #

once :: Occurs Source #

inSeq :: Occurs -> Occurs Source #

underLambda :: Occurs -> Occurs Source #

class HasFree a where Source #

Methods

freeVars :: a -> IntMap Occurs Source #

#### Instances

Instances details

HasFree TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TAlt -> IntMap Occurs Source #
HasFree TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TTerm -> IntMap Occurs Source #
HasFree Int Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: Int -> IntMap Occurs Source #
HasFree a => HasFree (Binder a) Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: Binder a -> IntMap Occurs Source #
HasFree a => HasFree (InSeq a) Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: InSeq a -> IntMap Occurs Source #
HasFree a => HasFree [a] Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: [a] -> IntMap Occurs Source #
(HasFree a, HasFree b) => HasFree (a, b) Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: (a, b) -> IntMap 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 -> IntMap 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 -> IntMap 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 #