Safe Haskell	None
Language	Haskell98

QuickSpec.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, MeasureFuns f, Int, [Var])
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
- | App !f ![Term f]
isApp :: Term f -> Bool
isVar :: Term f -> Bool
terms :: Symbolic f a => a -> [Term f]
funs :: Symbolic f a => a -> [f]
vars :: Symbolic f a => a -> [Var]
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
subterms :: Term f -> [Term f]
properSubterms :: 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
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 Arity f where
- arity :: f -> Int
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

(Eq a, Eq b) => Eq (a :+: b) Source #
Instance details Defined in QuickSpec.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.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.Term Methods pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc # pPrint :: (fun1 :+: fun2) -> Doc # pPrintList :: PrettyLevel -> [fun1 :+: fun2] -> Doc #
(Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Term Methods arity :: (fun1 :+: fun2) -> Int #
(PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Term Methods termStyle :: (fun1 :+: fun2) -> TermStyle #
(Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Term Methods typ :: (fun1 :+: fun2) -> Type Source # otherTypesDL :: (fun1 :+: fun2) -> DList Type Source # typeSubst_ :: (Var -> Builder TyCon) -> (fun1 :+: fun2) -> fun1 :+: fun2 Source #
(Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Term Methods size :: (fun1 :+: fun2) -> Int Source #

newtype MeasureFuns f Source #

A helper for Measure.

Constructors

MeasureFuns (Term f)

Instances

Ord f => Eq (MeasureFuns f) Source #
Instance details Defined in QuickSpec.Term Methods (==) :: MeasureFuns f -> MeasureFuns f -> Bool # (/=) :: MeasureFuns f -> MeasureFuns f -> Bool #
Ord f => Ord (MeasureFuns f) Source #
Instance details Defined in QuickSpec.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, 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.

class Sized a where Source #

Methods

size :: a -> Int Source #

Instances

Sized fun => Sized (Extended fun) Source #
Instance details Defined in QuickSpec.Pruning.UntypedTwee Methods size :: Extended fun -> Int Source #
Sized fun => Sized (Term fun) Source #
Instance details Defined in QuickSpec.Pruning.UntypedTwee Methods size :: Term fun -> Int Source #
Sized f => Sized (Term f) Source #
Instance details Defined in QuickSpec.Term Methods size :: Term f -> Int Source #
(Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.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

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

data Var Source #

A variable, which has a type and a number.

Constructors

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

Instances

Eq Var Source #
Instance details Defined in QuickSpec.Term Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in QuickSpec.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 #
Show Var Source #
Instance details Defined in QuickSpec.Term Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #
Generic Var Source #
Instance details Defined in QuickSpec.Term Associated Types type Rep Var :: Type -> Type # Methods from :: Var -> Rep Var x # to :: Rep Var x -> Var #
CoArbitrary Var Source #
Instance details Defined in QuickSpec.Term Methods coarbitrary :: Var -> Gen b -> Gen b #
Pretty Var Source #
Instance details Defined in QuickSpec.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Var -> Doc # pPrint :: Var -> Doc # pPrintList :: PrettyLevel -> [Var] -> Doc #
Typed Var Source #
Instance details Defined in QuickSpec.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.Term type Rep Var = D1 (MetaData "Var" "QuickSpec.Term" "quickspec-2.1.1-8ayCzcvVUjmFxcf6Z16wEZ" 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
App !f ![Term f]

Instances

Functor Term Source #
Instance details Defined in QuickSpec.Term Methods fmap :: (a -> b) -> Term a -> Term b # (<$) :: a -> Term b -> Term a #
Symbolic f (Term f) Source #
Instance details Defined in QuickSpec.Term Methods termsDL :: Term f -> DList (Term f) Source # subst :: (Var -> Term f) -> Term f -> Term f Source #
Eq f => Eq (Term f) Source #
Instance details Defined in QuickSpec.Term Methods (==) :: Term f -> Term f -> Bool # (/=) :: Term f -> Term f -> Bool #
Ord f => Ord (Term f) Source #
Instance details Defined in QuickSpec.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 #
Show f => Show (Term f) Source #
Instance details Defined in QuickSpec.Term Methods showsPrec :: Int -> Term f -> ShowS # show :: Term f -> String # showList :: [Term f] -> ShowS #
PrettyTerm f => Pretty (Term f) Source #
Instance details Defined in QuickSpec.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc # pPrint :: Term f -> Doc # pPrintList :: PrettyLevel -> [Term f] -> Doc #
Typed f => Typed (Term f) Source #
Instance details Defined in QuickSpec.Term Methods typ :: Term f -> Type Source # otherTypesDL :: Term f -> DList Type Source # typeSubst_ :: (Var -> Builder TyCon) -> Term f -> Term f Source #
Sized f => Sized (Term f) Source #
Instance details Defined in QuickSpec.Term Methods size :: Term f -> Int Source #

isApp :: Term f -> Bool Source #

Is a term an application (i.e. not a variable)?

isVar :: Term f -> Bool Source #

Is a term a variable?

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.

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.

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.

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.

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

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 #
Pretty Integer
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Integer -> Doc # pPrint :: Integer -> Doc # pPrintList :: PrettyLevel -> [Integer] -> Doc #
Pretty Ordering
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> Ordering -> Doc # pPrint :: Ordering -> Doc # pPrintList :: PrettyLevel -> [Ordering] -> Doc #
Pretty ()
Instance details Defined in Text.PrettyPrint.HughesPJClass Methods pPrintPrec :: PrettyLevel -> Rational -> () -> Doc # pPrint :: () -> Doc # pPrintList :: PrettyLevel -> [()] -> Doc #
Pretty Id
Instance details Defined in Twee.Base Methods pPrintPrec :: PrettyLevel -> Rational -> Id -> Doc # pPrint :: Id -> Doc # pPrintList :: PrettyLevel -> [Id] -> Doc #
Pretty TyCon Source #
Instance details Defined in QuickSpec.Type Methods pPrintPrec :: PrettyLevel -> Rational -> TyCon -> Doc # pPrint :: TyCon -> Doc # pPrintList :: PrettyLevel -> [TyCon] -> Doc #
Pretty Var Source #
Instance details Defined in QuickSpec.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Var -> Doc # pPrint :: Var -> Doc # pPrintList :: PrettyLevel -> [Var] -> 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 (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 #
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 #
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 #
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 #
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 #
Function f => Pretty (Reduction f)
Instance details Defined in Twee.Rule Methods pPrintPrec :: PrettyLevel -> Rational -> Reduction f -> Doc # pPrint :: Reduction f -> Doc # pPrintList :: PrettyLevel -> [Reduction f] -> Doc #
Function f => Pretty (Resulting f)
Instance details Defined in Twee.Rule Methods pPrintPrec :: PrettyLevel -> Rational -> Resulting f -> Doc # pPrint :: Resulting f -> Doc # pPrintList :: PrettyLevel -> [Resulting 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 #
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 #
PrettyTerm f => Pretty (Lemma f)
Instance details Defined in Twee.Proof Methods pPrintPrec :: PrettyLevel -> Rational -> Lemma f -> Doc # pPrint :: Lemma f -> Doc # pPrintList :: PrettyLevel -> [Lemma f] -> Doc #
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 #
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 #
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 #
Pretty f => Pretty (Extended f)
Instance details Defined in Twee.Base Methods pPrintPrec :: PrettyLevel -> Rational -> Extended f -> Doc # pPrint :: Extended f -> Doc # pPrintList :: PrettyLevel -> [Extended f] -> Doc #
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 #
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 #
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 #
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 #
Pretty a => Pretty (Poly a) Source #
Instance details Defined in QuickSpec.Type Methods pPrintPrec :: PrettyLevel -> Rational -> Poly a -> Doc # pPrint :: Poly a -> Doc # pPrintList :: PrettyLevel -> [Poly a] -> Doc #
PrettyTerm f => Pretty (Term f) Source #
Instance details Defined in QuickSpec.Term Methods pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc # pPrint :: Term f -> Doc # pPrintList :: PrettyLevel -> [Term f] -> 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 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 fun1, Pretty fun2) => Pretty (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Term Methods pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc # pPrint :: (fun1 :+: fun2) -> Doc # pPrintList :: PrettyLevel -> [fun1 :+: fun2] -> 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 Arity f where #

For types which have a notion of arity.

Methods

arity :: f -> Int #

Measure the arity.

Instances

Arity f => Arity (Extended f)
Instance details Defined in Twee.Base Methods arity :: Extended f -> Int #
Arity f => Arity (Fun f)
Instance details Defined in Twee.Base Methods arity :: Fun f -> Int #
(Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.Term Methods arity :: (fun1 :+: fun2) -> Int #

class EqualsBonus f #

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

Instances

EqualsBonus f => EqualsBonus (Extended f)
Instance details Defined in Twee.Base Methods hasEqualsBonus :: Extended f -> Bool # isEquals :: Extended f -> Bool # isTrue :: Extended f -> Bool # isFalse :: Extended f -> Bool #
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

PrettyTerm TyCon Source #
Instance details Defined in QuickSpec.Type Methods termStyle :: TyCon -> TermStyle #
PrettyTerm f => PrettyTerm (Extended f)
Instance details Defined in Twee.Base Methods termStyle :: Extended f -> TermStyle #
PrettyTerm f => PrettyTerm (Fun f)
Instance details Defined in Twee.Pretty Methods termStyle :: Fun f -> TermStyle #
(PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) Source #
Instance details Defined in QuickSpec.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