Safe Haskell	Safe-Inferred
Language	Haskell2010

QuickSpec.Internal.Term

Description

This module is internal to QuickSpec.

Typed terms and operations on them.

Synopsis

data a :+: b
- = Inl a
- | Inr b
newtype MeasureFuns f = MeasureFuns (Term f)
type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var])
data OrId f
- = Id
- | NotId f
class Sized a where
- size :: a -> Int
class Symbolic f a | a -> f where
- termsDL :: a -> DList (Term f)
- subst :: (Var -> Term f) -> a -> a
data Var = V {
- var_ty :: !Type
- var_id :: !Int
}
data Term f
- = Var !Var
- | Fun !f
- | !(Term f) :$: !(Term f)
pattern (:@:) :: Term f -> [Term f] -> Term f
match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
terms :: Symbolic f a => a -> [Term f]
funs :: Symbolic f a => a -> [f]
vars :: Symbolic f a => a -> [Var]
getApp :: Term f -> (Term f, [Term f])
freeVar :: Symbolic f a => a -> Int
occ :: (Eq f, Symbolic f a) => f -> a -> Int
occVar :: Symbolic f a => Var -> a -> Int
mapVar :: (Var -> Var) -> Term f -> Term f
mapFun :: (f -> g) -> Term f -> Term g
flatMapFun :: (f -> Term g) -> Term f -> Term g
eliminateId :: Term (OrId f) -> Maybe (Term f)
subterms :: Term f -> [Term f]
properSubterms :: Term f -> [Term f]
subtermsFO :: Term f -> [Term f]
properSubtermsFO :: Term f -> [Term f]
canonicalise :: Symbolic fun a => a -> a
evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a
depth :: Term f -> Int
measure :: (Sized f, Typed f) => Term f -> Measure f
compareFuns :: Ord f => Term f -> Term f -> Ordering
class Pretty a where
- pPrintPrec :: PrettyLevel -> Rational -> a -> Doc
- pPrint :: a -> Doc
- pPrintList :: PrettyLevel -> [a] -> Doc
class EqualsBonus f
prettyPrint :: Pretty a => a -> IO ()
class Pretty f => PrettyTerm f where
- termStyle :: f -> TermStyle
newtype TermStyle = TermStyle {
- pPrintTerm :: forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc
}
module Twee.Pretty

Documentation

data a :+: b Source #

A sum type. Intended to be used to build the type of function symbols. Comes with instances that are useful for QuickSpec.

Constructors

Inl a
Inr b

Instances

Instances details

(Eq a, Eq b) => Eq (a :+: b) Source #
Instance details Defined in QuickSpec.Internal.Term Methods (==) :: (a :+: b) -> (a :+: b) -> Bool # (/=) :: (a :+: b) -> (a :+: b) -> Bool #
(Ord a, Ord b) => Ord (a :+: b) Source #
Instance details Defined in QuickSpec.Internal.Term Methods compare :: (a :+: b) -> (a :+: b) -> Ordering # (<) :: (a :+: b) -> (a :+: b) -> Bool # (<=) :: (a :+: b) -> (a :+: b) -> Bool # (>) :: (a :+: b) -> (a :+: b) -> Bool # (>=) :: (a :+: b) -> (a :+: b) -> Bool # max :: (a :+: b) -> (a :+: b) -> a :+: b # min :: (a :+: b) -> (a :+: b) -> a :+: b #
(Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc # pPrint :: (fun1 :+: fun2) -> Doc # pPrintList :: PrettyLevel -> [fun1 :+: fun2] -> Doc #
(Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods size :: (fun1 :+: fun2) -> Int Source #
(Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods typ :: (fun1 :+: fun2) -> Type Source # otherTypesDL :: (fun1 :+: fun2) -> DList Type Source # typeSubst_ :: (Var -> Builder TyCon) -> (fun1 :+: fun2) -> fun1 :+: fun2 Source #
(PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods termStyle :: (fun1 :+: fun2) -> TermStyle #

newtype MeasureFuns f Source #

A helper for Measure.

Constructors

MeasureFuns (Term f)

Instances

Instances details

Ord f => Eq (MeasureFuns f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods (==) :: MeasureFuns f -> MeasureFuns f -> Bool # (/=) :: MeasureFuns f -> MeasureFuns f -> Bool #
Ord f => Ord (MeasureFuns f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods compare :: MeasureFuns f -> MeasureFuns f -> Ordering # (<) :: MeasureFuns f -> MeasureFuns f -> Bool # (<=) :: MeasureFuns f -> MeasureFuns f -> Bool # (>) :: MeasureFuns f -> MeasureFuns f -> Bool # (>=) :: MeasureFuns f -> MeasureFuns f -> Bool # max :: MeasureFuns f -> MeasureFuns f -> MeasureFuns f # min :: MeasureFuns f -> MeasureFuns f -> MeasureFuns f #

type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var]) Source #

A standard term ordering - size, skeleton, generality. Satisfies the property: if measure (schema t) < measure (schema u) then t < u.

data OrId f Source #

A type representing functions which may be the identity.

Constructors

Id
NotId f

class Sized a where Source #

Methods

size :: a -> Int Source #

Instances

Instances details

Sized f => Sized (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods size :: Term f -> Int Source #
(Labelled fun, Sized fun) => Sized (Term fun) Source #
Instance details Defined in QuickSpec.Internal.Pruning.UntypedTwee Methods size :: Term fun -> Int Source #
(Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods size :: (fun1 :+: fun2) -> Int Source #

class Symbolic f a | a -> f where Source #

A class for things that contain terms.

Methods

termsDL :: a -> DList (Term f) Source #

A different list of all terms contained in the thing.

subst :: (Var -> Term f) -> a -> a Source #

Apply a substitution to all terms in the thing.

Instances

Instances details

Symbolic f (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods termsDL :: Term f -> DList (Term f) Source # subst :: (Var -> Term f) -> Term f -> Term f Source #
Symbolic f a => Symbolic f [a] Source #
Instance details Defined in QuickSpec.Internal.Term Methods termsDL :: [a] -> DList (Term f) Source # subst :: (Var -> Term f) -> [a] -> [a] Source #

data Var Source #

A variable, which has a type and a number.

Constructors

V
Fields var_ty :: !Type var_id :: !Int

Instances

Instances details

CoArbitrary Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods coarbitrary :: Var -> Gen b -> Gen b #
Generic Var Source #
Instance details Defined in QuickSpec.Internal.Term Associated Types type Rep Var :: Type -> Type # Methods from :: Var -> Rep Var x # to :: Rep Var x -> Var #
Show Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #
Eq Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods compare :: Var -> Var -> Ordering # (<) :: Var -> Var -> Bool # (<=) :: Var -> Var -> Bool # (>) :: Var -> Var -> Bool # (>=) :: Var -> Var -> Bool # max :: Var -> Var -> Var # min :: Var -> Var -> Var #
Pretty Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Var -> Doc # pPrint :: Var -> Doc # pPrintList :: PrettyLevel -> [Var] -> Doc #
Typed Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods typ :: Var -> Type Source # otherTypesDL :: Var -> DList Type Source # typeSubst_ :: (Var0 -> Builder TyCon) -> Var -> Var Source #
type Rep Var Source #
Instance details Defined in QuickSpec.Internal.Term type Rep Var = D1 ('MetaData "Var" "QuickSpec.Internal.Term" "quickspec-2.2-IZSjQ5lmka18t2AqwSyTXi" 'False) (C1 ('MetaCons "V" 'PrefixI 'True) (S1 ('MetaSel ('Just "var_ty") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type) :*: S1 ('MetaSel ('Just "var_id") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)))

data Term f Source #

A typed term.

Constructors

Var !Var
Fun !f
!(Term f) :$: !(Term f)

Instances

Instances details

Foldable Term Source #
Instance details Defined in QuickSpec.Internal.Term Methods fold :: Monoid m => Term m -> m # foldMap :: Monoid m => (a -> m) -> Term a -> m # foldMap' :: Monoid m => (a -> m) -> Term a -> m # foldr :: (a -> b -> b) -> b -> Term a -> b # foldr' :: (a -> b -> b) -> b -> Term a -> b # foldl :: (b -> a -> b) -> b -> Term a -> b # foldl' :: (b -> a -> b) -> b -> Term a -> b # foldr1 :: (a -> a -> a) -> Term a -> a # foldl1 :: (a -> a -> a) -> Term a -> a # toList :: Term a -> [a] # null :: Term a -> Bool # length :: Term a -> Int # elem :: Eq a => a -> Term a -> Bool # maximum :: Ord a => Term a -> a # minimum :: Ord a => Term a -> a # sum :: Num a => Term a -> a # product :: Num a => Term a -> a #
Traversable Term Source #
Instance details Defined in QuickSpec.Internal.Term Methods traverse :: Applicative f => (a -> f b) -> Term a -> f (Term b) # sequenceA :: Applicative f => Term (f a) -> f (Term a) # mapM :: Monad m => (a -> m b) -> Term a -> m (Term b) # sequence :: Monad m => Term (m a) -> m (Term a) #
Functor Term Source #
Instance details Defined in QuickSpec.Internal.Term Methods fmap :: (a -> b) -> Term a -> Term b # (<$) :: a -> Term b -> Term a #
Symbolic f (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods termsDL :: Term f -> DList (Term f) Source # subst :: (Var -> Term f) -> Term f -> Term f Source #
Show f => Show (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods showsPrec :: Int -> Term f -> ShowS # show :: Term f -> String # showList :: [Term f] -> ShowS #
Eq f => Eq (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods (==) :: Term f -> Term f -> Bool # (/=) :: Term f -> Term f -> Bool #
Ord f => Ord (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods compare :: Term f -> Term f -> Ordering # (<) :: Term f -> Term f -> Bool # (<=) :: Term f -> Term f -> Bool # (>) :: Term f -> Term f -> Bool # (>=) :: Term f -> Term f -> Bool # max :: Term f -> Term f -> Term f # min :: Term f -> Term f -> Term f #
PrettyTerm f => Pretty (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc # pPrint :: Term f -> Doc # pPrintList :: PrettyLevel -> [Term f] -> Doc #
Sized f => Sized (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods size :: Term f -> Int Source #
(PrettyTerm f, Typed f) => Apply (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods tryApply :: Term f -> Term f -> Maybe (Term f) Source #
Typed f => Typed (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods typ :: Term f -> Type Source # otherTypesDL :: Term f -> DList Type Source # typeSubst_ :: (Var -> Builder TyCon) -> Term f -> Term f Source #

pattern (:@:) :: Term f -> [Term f] -> Term f Source #

Decompose a term into a head and a list of arguments.

match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f)) Source #

unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f)) Source #

terms :: Symbolic f a => a -> [Term f] Source #

All terms contained in a Symbolic.

funs :: Symbolic f a => a -> [f] Source #

All function symbols appearing in a Symbolic, in order of appearance, with duplicates included.

vars :: Symbolic f a => a -> [Var] Source #

All variables appearing in a Symbolic, in order of appearance, with duplicates included.

getApp :: Term f -> (Term f, [Term f]) Source #

freeVar :: Symbolic f a => a -> Int Source #

Compute the number of a variable which does not appear in the Symbolic.

occ :: (Eq f, Symbolic f a) => f -> a -> Int Source #

Count how many times a given function symbol occurs.

occVar :: Symbolic f a => Var -> a -> Int Source #

Count how many times a given variable occurs.

mapVar :: (Var -> Var) -> Term f -> Term f Source #

Map a function over variables.

mapFun :: (f -> g) -> Term f -> Term g Source #

Map a function over function symbols.

flatMapFun :: (f -> Term g) -> Term f -> Term g Source #

Map a function over function symbols.

eliminateId :: Term (OrId f) -> Maybe (Term f) Source #

Eliminate the identity function from a term.

subterms :: Term f -> [Term f] Source #

Find all subterms of a term. Includes the term itself.

properSubterms :: Term f -> [Term f] Source #

Find all subterms of a term. Does not include the term itself.

subtermsFO :: Term f -> [Term f] Source #

properSubtermsFO :: Term f -> [Term f] Source #

canonicalise :: Symbolic fun a => a -> a Source #

Renames variables so that they appear in a canonical order. Also makes sure that variables of different types have different numbers.

evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a Source #

Evaluate a term, given a valuation for variables and function symbols.

depth :: Term f -> Int Source #

measure :: (Sized f, Typed f) => Term f -> Measure f Source #

Compute the term ordering for a term.

compareFuns :: Ord f => Term f -> Term f -> Ordering Source #

A helper for Measure.

class Pretty a where #

Pretty printing class. The precedence level is used in a similar way as in the Show class. Minimal complete definition is either pPrintPrec or pPrint.

Minimal complete definition

pPrintPrec | pPrint

Methods

pPrintPrec :: PrettyLevel -> Rational -> a -> Doc #

pPrint :: a -> Doc #

pPrintList :: PrettyLevel -> [a] -> Doc #

Instances

Instances details

Pretty Ordering
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Ordering -> Doc # pPrint :: Ordering -> Doc # pPrintList :: PrettyLevel -> [Ordering] -> Doc #
Pretty Var Source #
Instance details Defined in QuickSpec.Internal.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Var -> Doc # pPrint :: Var -> Doc # pPrintList :: PrettyLevel -> [Var] -> Doc #
Pretty TyCon Source #
Instance details Defined in QuickSpec.Internal.Type Methods pPrintPrec :: PrettyLevel -> Rational -> TyCon -> Doc # pPrint :: TyCon -> Doc # pPrintList :: PrettyLevel -> [TyCon] -> Doc #
Pretty Id
Instance details Defined in Twee.Base Methods pPrintPrec :: PrettyLevel -> Rational -> Id -> Doc # pPrint :: Id -> Doc # pPrintList :: PrettyLevel -> [Id] -> Doc #
Pretty Integer
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Integer -> Doc # pPrint :: Integer -> Doc # pPrintList :: PrettyLevel -> [Integer] -> Doc #
Pretty ()
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> () -> Doc # pPrint :: () -> Doc # pPrintList :: PrettyLevel -> [()] -> Doc #
Pretty Bool
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Bool -> Doc # pPrint :: Bool -> Doc # pPrintList :: PrettyLevel -> [Bool] -> Doc #
Pretty Char
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Char -> Doc # pPrint :: Char -> Doc # pPrintList :: PrettyLevel -> [Char] -> Doc #
Pretty Double
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Double -> Doc # pPrint :: Double -> Doc # pPrintList :: PrettyLevel -> [Double] -> Doc #
Pretty Float
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Float -> Doc # pPrint :: Float -> Doc # pPrintList :: PrettyLevel -> [Float] -> Doc #
Pretty Int
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Int -> Doc # pPrint :: Int -> Doc # pPrintList :: PrettyLevel -> [Int] -> Doc #
PrettyTerm f => Pretty (Term f) Source #
Instance details Defined in QuickSpec.Internal.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc # pPrint :: Term f -> Doc # pPrintList :: PrettyLevel -> [Term f] -> Doc #
Pretty a => Pretty (Poly a) Source #
Instance details Defined in QuickSpec.Internal.Type Methods pPrintPrec :: PrettyLevel -> Rational -> Poly a -> Doc # pPrint :: Poly a -> Doc # pPrintList :: PrettyLevel -> [Poly a] -> Doc #
Function f => Pretty (Active f)
Instance details Defined in Twee Methods pPrintPrec :: PrettyLevel -> Rational -> Active f -> Doc # pPrint :: Active f -> Doc # pPrintList :: PrettyLevel -> [Active f] -> Doc #
Function f => Pretty (Message f)
Instance details Defined in Twee Methods pPrintPrec :: PrettyLevel -> Rational -> Message f -> Doc # pPrint :: Message f -> Doc # pPrintList :: PrettyLevel -> [Message f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (CriticalPair f)
Instance details Defined in Twee.CP Methods pPrintPrec :: PrettyLevel -> Rational -> CriticalPair f -> Doc # pPrint :: CriticalPair f -> Doc # pPrintList :: PrettyLevel -> [CriticalPair f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Atom f)
Instance details Defined in Twee.Constraints Methods pPrintPrec :: PrettyLevel -> Rational -> Atom f -> Doc # pPrint :: Atom f -> Doc # pPrintList :: PrettyLevel -> [Atom f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Branch f)
Instance details Defined in Twee.Constraints Methods pPrintPrec :: PrettyLevel -> Rational -> Branch f -> Doc # pPrint :: Branch f -> Doc # pPrintList :: PrettyLevel -> [Branch f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Formula f)
Instance details Defined in Twee.Constraints Methods pPrintPrec :: PrettyLevel -> Rational -> Formula f -> Doc # pPrint :: Formula f -> Doc # pPrintList :: PrettyLevel -> [Formula f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Model f)
Instance details Defined in Twee.Constraints Methods pPrintPrec :: PrettyLevel -> Rational -> Model f -> Doc # pPrint :: Model f -> Doc # pPrintList :: PrettyLevel -> [Model f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Equation f)
Instance details Defined in Twee.Equation Methods pPrintPrec :: PrettyLevel -> Rational -> Equation f -> Doc # pPrint :: Equation f -> Doc # pPrintList :: PrettyLevel -> [Equation f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (HighlightedTerm f)
Instance details Defined in Twee.Pretty Methods pPrintPrec :: PrettyLevel -> Rational -> HighlightedTerm f -> Doc # pPrint :: HighlightedTerm f -> Doc # pPrintList :: PrettyLevel -> [HighlightedTerm f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Axiom f)
Instance details Defined in Twee.Proof Methods pPrintPrec :: PrettyLevel -> Rational -> Axiom f -> Doc # pPrint :: Axiom f -> Doc # pPrintList :: PrettyLevel -> [Axiom f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Derivation f)
Instance details Defined in Twee.Proof Methods pPrintPrec :: PrettyLevel -> Rational -> Derivation f -> Doc # pPrint :: Derivation f -> Doc # pPrintList :: PrettyLevel -> [Derivation f] -> Doc #
Function f => Pretty (Presentation f)
Instance details Defined in Twee.Proof Methods pPrintPrec :: PrettyLevel -> Rational -> Presentation f -> Doc # pPrint :: Presentation f -> Doc # pPrintList :: PrettyLevel -> [Presentation f] -> Doc #
Function f => Pretty (Proof f)
Instance details Defined in Twee.Proof Methods pPrintPrec :: PrettyLevel -> Rational -> Proof f -> Doc # pPrint :: Proof f -> Doc # pPrintList :: PrettyLevel -> [Proof f] -> Doc #
(Labelled f, PrettyTerm f) => Pretty (Rule f)
Instance details Defined in Twee.Rule Methods pPrintPrec :: PrettyLevel -> Rational -> Rule f -> Doc # pPrint :: Rule f -> Doc # pPrintList :: PrettyLevel -> [Rule f] -> Doc #
Pretty a => Pretty (Maybe a)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Maybe a -> Doc # pPrint :: Maybe a -> Doc # pPrintList :: PrettyLevel -> [Maybe a] -> Doc #
Pretty a => Pretty [a]
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> [a] -> Doc # pPrint :: [a] -> Doc # pPrintList :: PrettyLevel -> [[a]] -> Doc #
(Pretty a, Pretty b) => Pretty (Either a b)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Either a b -> Doc # pPrint :: Either a b -> Doc # pPrintList :: PrettyLevel -> [Either a b] -> Doc #
(Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc # pPrint :: (fun1 :+: fun2) -> Doc # pPrintList :: PrettyLevel -> [fun1 :+: fun2] -> Doc #
(Pretty a, Pretty b) => Pretty (a, b)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b) -> Doc # pPrint :: (a, b) -> Doc # pPrintList :: PrettyLevel -> [(a, b)] -> Doc #
(Pretty a, Pretty b, Pretty c) => Pretty (a, b, c)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b, c) -> Doc # pPrint :: (a, b, c) -> Doc # pPrintList :: PrettyLevel -> [(a, b, c)] -> Doc #
(Pretty a, Pretty b, Pretty c, Pretty d) => Pretty (a, b, c, d)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d) -> Doc # pPrint :: (a, b, c, d) -> Doc # pPrintList :: PrettyLevel -> [(a, b, c, d)] -> Doc #
(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e) => Pretty (a, b, c, d, e)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e) -> Doc # pPrint :: (a, b, c, d, e) -> Doc # pPrintList :: PrettyLevel -> [(a, b, c, d, e)] -> Doc #
(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e, Pretty f) => Pretty (a, b, c, d, e, f)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e, f) -> Doc # pPrint :: (a, b, c, d, e, f) -> Doc # pPrintList :: PrettyLevel -> [(a, b, c, d, e, f)] -> Doc #
(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e, Pretty f, Pretty g) => Pretty (a, b, c, d, e, f, g)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e, f, g) -> Doc # pPrint :: (a, b, c, d, e, f, g) -> Doc # pPrintList :: PrettyLevel -> [(a, b, c, d, e, f, g)] -> Doc #
(Pretty a, Pretty b, Pretty c, Pretty d, Pretty e, Pretty f, Pretty g, Pretty h) => Pretty (a, b, c, d, e, f, g, h)
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> (a, b, c, d, e, f, g, h) -> Doc # pPrint :: (a, b, c, d, e, f, g, h) -> Doc # pPrintList :: PrettyLevel -> [(a, b, c, d, e, f, g, h)] -> Doc #

class EqualsBonus f #

A hack for encoding Horn clauses. See Score. The default implementation of hasEqualsBonus should work OK.

Instances

Instances details

(Labelled f, EqualsBonus f) => EqualsBonus (Fun f)
Instance details Defined in Twee.Base Methods hasEqualsBonus :: Fun f -> Bool # isEquals :: Fun f -> Bool # isTrue :: Fun f -> Bool # isFalse :: Fun f -> Bool #

prettyPrint :: Pretty a => a -> IO () #

Print a value to the console.

class Pretty f => PrettyTerm f where #

A class for customising the printing of function symbols.

Minimal complete definition

Nothing

Methods

termStyle :: f -> TermStyle #

The style of the function symbol. Defaults to curried.

Instances

Instances details

PrettyTerm TyCon Source #
Instance details Defined in QuickSpec.Internal.Type Methods termStyle :: TyCon -> TermStyle #
(PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Internal.Term Methods termStyle :: (fun1 :+: fun2) -> TermStyle #

newtype TermStyle #

Defines how to print out a function symbol.

Constructors

TermStyle
Fields pPrintTerm :: forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc Renders a function application. Takes the following arguments in this order: Pretty-printing level, current precedence, pretty-printed function symbol and list of arguments to the function.

module Twee.Pretty