pire-0.2.5

Safe HaskellNone
LanguageHaskell2010

Term

Documentation

data Term t a Source #

Constructors

Ide a 
Var (TVar a) 
Con t 
(Term t a) `Of` (Size t) 
Sz (Size t) 
Abs1 t (Scope () (Term t) a) 
Abs [t] (Scope Int (Term t) a) 
Op String [Term t a] 
Op2 String (Term t a) [Term t a] 
Op3 String (Term t a) (Term t a) [Term t a] 
Params [Term t a] 
TPair (Term t a) (Term t a) 
Eps Eps 
Pas [(Eps, t, Annot t a)] 
TNone 
Tt t 
Annot (Annot t a) 
Exp (Expr t a) 
Exp_ (Expr t a) (TT t a) 
Mat (Match t a) 
Mat_ (Match t a) (TT t a) 
Pat (Pattern t) 
Pat_ (Pattern t) (TT t a) 
Tel (Telescope t a) 
CDef (ConstructorDef t a) 
CDef_ (ConstructorDef t a) (TT t a) 
Dcl (Decl t a) 
Dcl_ (Decl t a) (TT t a) 
Mod (Module t a) 
Mod_ (Module t a) (TT t a) 
ARG (Arg t a) 
ARG_ (Arg t a) (TT t a) 

Instances

Ord t => SSubstitutable t (Term t t) Source # 

Methods

sapply :: SSubst t -> Term t t -> Term t t Source #

fsv :: Term t t -> Set (SVar t) Source #

Monad (Term t) Source # 

Methods

(>>=) :: Term t a -> (a -> Term t b) -> Term t b #

(>>) :: Term t a -> Term t b -> Term t b #

return :: a -> Term t a #

fail :: String -> Term t a #

Functor (Term t) Source # 

Methods

fmap :: (a -> b) -> Term t a -> Term t b #

(<$) :: a -> Term t b -> Term t a #

Applicative (Term t) Source # 

Methods

pure :: a -> Term t a #

(<*>) :: Term t (a -> b) -> Term t a -> Term t b #

liftA2 :: (a -> b -> c) -> Term t a -> Term t b -> Term t c #

(*>) :: Term t a -> Term t b -> Term t b #

(<*) :: Term t a -> Term t b -> Term t a #

Foldable (Term t) Source # 

Methods

fold :: Monoid m => Term t m -> m #

foldMap :: Monoid m => (a -> m) -> Term t a -> m #

foldr :: (a -> b -> b) -> b -> Term t a -> b #

foldr' :: (a -> b -> b) -> b -> Term t a -> b #

foldl :: (b -> a -> b) -> b -> Term t a -> b #

foldl' :: (b -> a -> b) -> b -> Term t a -> b #

foldr1 :: (a -> a -> a) -> Term t a -> a #

foldl1 :: (a -> a -> a) -> Term t a -> a #

toList :: Term t a -> [a] #

null :: Term t a -> Bool #

length :: Term t a -> Int #

elem :: Eq a => a -> Term t a -> Bool #

maximum :: Ord a => Term t a -> a #

minimum :: Ord a => Term t a -> a #

sum :: Num a => Term t a -> a #

product :: Num a => Term t a -> a #

Traversable (Term t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Term t a -> f (Term t b) #

sequenceA :: Applicative f => Term t (f a) -> f (Term t a) #

mapM :: Monad m => (a -> m b) -> Term t a -> m (Term t b) #

sequence :: Monad m => Term t (m a) -> m (Term t a) #

Eq t => Eq1 (Term t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Term t a -> Term t b -> Bool #

Ord t => Ord1 (Term t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Term t a -> Term t b -> Ordering #

Show t => Show1 (Term t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Term t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Term t a] -> ShowS #

(Eq t, Eq a) => Eq (Term t a) Source # 

Methods

(==) :: Term t a -> Term t a -> Bool #

(/=) :: Term t a -> Term t a -> Bool #

(Ord t, Ord a) => Ord (Term t a) Source # 

Methods

compare :: Term t a -> Term t a -> Ordering #

(<) :: Term t a -> Term t a -> Bool #

(<=) :: Term t a -> Term t a -> Bool #

(>) :: Term t a -> Term t a -> Bool #

(>=) :: Term t a -> Term t a -> Bool #

max :: Term t a -> Term t a -> Term t a #

min :: Term t a -> Term t a -> Term t a #

Show (Term t a -> Term t a) Source # 

Methods

showsPrec :: Int -> (Term t a -> Term t a) -> ShowS #

show :: (Term t a -> Term t a) -> String #

showList :: [Term t a -> Term t a] -> ShowS #

(Show t, Show a) => Show (Term t a) Source # 

Methods

showsPrec :: Int -> Term t a -> ShowS #

show :: Term t a -> String #

showList :: [Term t a] -> ShowS #

_ARG_ :: forall t a. Prism' (Term t a) (Arg t a, TT t a) Source #

_ARG :: forall t a. Prism' (Term t a) (Arg t a) Source #

_Mod_ :: forall t a. Prism' (Term t a) (Module t a, TT t a) Source #

_Mod :: forall t a. Prism' (Term t a) (Module t a) Source #

_Dcl_ :: forall t a. Prism' (Term t a) (Decl t a, TT t a) Source #

_Dcl :: forall t a. Prism' (Term t a) (Decl t a) Source #

_CDef_ :: forall t a. Prism' (Term t a) (ConstructorDef t a, TT t a) Source #

_CDef :: forall t a. Prism' (Term t a) (ConstructorDef t a) Source #

_Tel :: forall t a. Prism' (Term t a) (Telescope t a) Source #

_Pat_ :: forall t a. Prism' (Term t a) (Pattern t, TT t a) Source #

_Pat :: forall t a. Prism' (Term t a) (Pattern t) Source #

_Mat_ :: forall t a. Prism' (Term t a) (Match t a, TT t a) Source #

_Mat :: forall t a. Prism' (Term t a) (Match t a) Source #

_Exp_ :: forall t a. Prism' (Term t a) (Expr t a, TT t a) Source #

_Exp :: forall t a. Prism' (Term t a) (Expr t a) Source #

_Annot :: forall t a. Prism' (Term t a) (Annot t a) Source #

_Tt :: forall t a. Prism' (Term t a) t Source #

_TNone :: forall t a. Prism' (Term t a) () Source #

_Pas :: forall t a. Prism' (Term t a) [(Eps, t, Annot t a)] Source #

_Eps :: forall t a. Prism' (Term t a) Eps Source #

_TPair :: forall t a. Prism' (Term t a) (Term t a, Term t a) Source #

_Params :: forall t a. Prism' (Term t a) [Term t a] Source #

_Op3 :: forall t a. Prism' (Term t a) (String, Term t a, Term t a, [Term t a]) Source #

_Op2 :: forall t a. Prism' (Term t a) (String, Term t a, [Term t a]) Source #

_Op :: forall t a. Prism' (Term t a) (String, [Term t a]) Source #

_Abs :: forall t a. Prism' (Term t a) ([t], Scope Int (Term t) a) Source #

_Abs1 :: forall t a. Prism' (Term t a) (t, Scope () (Term t) a) Source #

_Sz :: forall t a. Prism' (Term t a) (Size t) Source #

_Of :: forall t a. Prism' (Term t a) (Term t a, Size t) Source #

_Con :: forall t a. Prism' (Term t a) t Source #

_Var :: forall t a. Prism' (Term t a) (TVar a) Source #

_Ide :: forall t a. Prism' (Term t a) a Source #