liquid-fixpoint-0.7.0.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.PrettyPrint

Synopsis

Documentation

traceFix :: Fixpoint a => String -> a -> a Source #

class Fixpoint a where Source #

Minimal complete definition

toFix

Methods

toFix :: a -> Doc Source #

simplify :: a -> a Source #

Instances

Fixpoint Bool Source # 
Fixpoint Double Source # 
Fixpoint Int Source # 

Methods

toFix :: Int -> Doc Source #

simplify :: Int -> Int Source #

Fixpoint Integer Source # 
Fixpoint () Source # 

Methods

toFix :: () -> Doc Source #

simplify :: () -> () Source #

Fixpoint Symbol Source # 
Fixpoint DataDecl Source # 
Fixpoint DataCtor Source # 
Fixpoint DataField Source # 
Fixpoint Sort Source # 
Fixpoint FTycon Source # 
Fixpoint Expr Source # 
Fixpoint Bop Source # 

Methods

toFix :: Bop -> Doc Source #

simplify :: Bop -> Bop Source #

Fixpoint Brel Source # 
Fixpoint Constant Source # 
Fixpoint SymConst Source # 
Fixpoint Subst Source # 
Fixpoint KVar Source # 
Fixpoint Packs Source # 
Fixpoint BindEnv Source # 
Fixpoint IBindEnv Source # 
Fixpoint TheorySymbol Source # 
Fixpoint Rewrite Source # 
Fixpoint Equation Source # 
Fixpoint AxiomEnv Source # 
Fixpoint Kuts Source # 
Fixpoint Qualifier Source # 
Fixpoint a => Fixpoint [a] Source # 

Methods

toFix :: [a] -> Doc Source #

simplify :: [a] -> [a] Source #

Fixpoint a => Fixpoint (Maybe a) Source # 

Methods

toFix :: Maybe a -> Doc Source #

simplify :: Maybe a -> Maybe a Source #

(Ord a, Hashable a, Fixpoint a) => Fixpoint (HashSet a) Source # 
Fixpoint a => Fixpoint (Located a) Source # 
(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # 
Fixpoint a => Fixpoint (SEnv a) Source # 

Methods

toFix :: SEnv a -> Doc Source #

simplify :: SEnv a -> SEnv a Source #

Fixpoint a => Fixpoint (SimpC a) Source # 

Methods

toFix :: SimpC a -> Doc Source #

simplify :: SimpC a -> SimpC a Source #

Fixpoint a => Fixpoint (SubC a) Source # 

Methods

toFix :: SubC a -> Doc Source #

simplify :: SubC a -> SubC a Source #

Fixpoint a => Fixpoint (WfC a) Source # 

Methods

toFix :: WfC a -> Doc Source #

simplify :: WfC a -> WfC a Source #

(Fixpoint a, Fixpoint b) => Fixpoint (a, b) Source # 

Methods

toFix :: (a, b) -> Doc Source #

simplify :: (a, b) -> (a, b) Source #

(Fixpoint a, Fixpoint b, Fixpoint c) => Fixpoint (a, b, c) Source # 

Methods

toFix :: (a, b, c) -> Doc Source #

simplify :: (a, b, c) -> (a, b, c) Source #

data Tidy Source #

Constructors

Lossy 
Full 

Instances

Eq Tidy Source # 

Methods

(==) :: Tidy -> Tidy -> Bool #

(/=) :: Tidy -> Tidy -> Bool #

Ord Tidy Source # 

Methods

compare :: Tidy -> Tidy -> Ordering #

(<) :: Tidy -> Tidy -> Bool #

(<=) :: Tidy -> Tidy -> Bool #

(>) :: Tidy -> Tidy -> Bool #

(>=) :: Tidy -> Tidy -> Bool #

max :: Tidy -> Tidy -> Tidy #

min :: Tidy -> Tidy -> Tidy #

class PPrint a where Source #

Implement either pprintTidy or pprintPrec

Methods

pprintTidy :: Tidy -> a -> Doc Source #

pprintPrec :: Int -> Tidy -> a -> Doc Source #

Instances

PPrint Bool Source # 
PPrint Float Source # 
PPrint Int Source # 

Methods

pprintTidy :: Tidy -> Int -> Doc Source #

pprintPrec :: Int -> Tidy -> Int -> Doc Source #

PPrint Integer Source # 
PPrint () Source # 

Methods

pprintTidy :: Tidy -> () -> Doc Source #

pprintPrec :: Int -> Tidy -> () -> Doc Source #

PPrint Text Source # 
PPrint Doc Source # 

Methods

pprintTidy :: Tidy -> Doc -> Doc Source #

pprintPrec :: Int -> Tidy -> Doc -> Doc Source #

PPrint DocTable Source # 
PPrint SrcSpan Source # 
PPrint Error Source # 
PPrint Symbol Source # 
PPrint DataDecl Source # 
PPrint DataCtor Source # 
PPrint DataField Source # 
PPrint FTycon Source # 
PPrint Expr Source # 
PPrint Bop Source # 

Methods

pprintTidy :: Tidy -> Bop -> Doc Source #

pprintPrec :: Int -> Tidy -> Bop -> Doc Source #

PPrint Brel Source # 
PPrint Constant Source # 
PPrint SymConst Source # 
PPrint KVSub Source # 
PPrint Subst Source # 
PPrint KVar Source # 
PPrint Packs Source # 
PPrint IBindEnv Source # 
PPrint SmtSort Source # 
PPrint Sem Source # 

Methods

pprintTidy :: Tidy -> Sem -> Doc Source #

pprintPrec :: Int -> Tidy -> Sem -> Doc Source #

PPrint TheorySymbol Source # 
PPrint Trigger Source # 
PPrint Equation Source # 
PPrint Qualifier Source # 
PPrint GFixSolution Source # 
PPrint Command Source # 
PPrint BindPred Source # 
PPrint BIndex Source # 
PPrint KIndex Source # 
PPrint EQual Source # 
PPrint Cube Source # 
PPrint QBind Source # 
PPrint Rank Source # 
PPrint KVGraph Source # 
PPrint CVertex Source # 
PPrint a => PPrint [a] Source # 

Methods

pprintTidy :: Tidy -> [a] -> Doc Source #

pprintPrec :: Int -> Tidy -> [a] -> Doc Source #

PPrint a => PPrint (Maybe a) Source # 

Methods

pprintTidy :: Tidy -> Maybe a -> Doc Source #

pprintPrec :: Int -> Tidy -> Maybe a -> Doc Source #

PPrint a => PPrint (HashSet a) Source # 
PPrint a => PPrint (Located a) Source # 
PPrint a => PPrint (SEnv a) Source # 

Methods

pprintTidy :: Tidy -> SEnv a -> Doc Source #

pprintPrec :: Int -> Tidy -> SEnv a -> Doc Source #

PPrint a => PPrint (Triggered a) Source # 
Fixpoint a => PPrint (SimpC a) Source # 

Methods

pprintTidy :: Tidy -> SimpC a -> Doc Source #

pprintPrec :: Int -> Tidy -> SimpC a -> Doc Source #

Fixpoint a => PPrint (SubC a) Source # 

Methods

pprintTidy :: Tidy -> SubC a -> Doc Source #

pprintPrec :: Int -> Tidy -> SubC a -> Doc Source #

Fixpoint a => PPrint (WfC a) Source # 

Methods

pprintTidy :: Tidy -> WfC a -> Doc Source #

pprintPrec :: Int -> Tidy -> WfC a -> Doc Source #

PPrint (Elims a) Source # 

Methods

pprintTidy :: Tidy -> Elims a -> Doc Source #

pprintPrec :: Int -> Tidy -> Elims a -> Doc Source #

PPrint (Worklist a) Source # 
(PPrint a, PPrint b) => PPrint (a, b) Source # 

Methods

pprintTidy :: Tidy -> (a, b) -> Doc Source #

pprintPrec :: Int -> Tidy -> (a, b) -> Doc Source #

(PPrint a, PPrint b) => PPrint (HashMap a b) Source # 

Methods

pprintTidy :: Tidy -> HashMap a b -> Doc Source #

pprintPrec :: Int -> Tidy -> HashMap a b -> Doc Source #

(PPrint a, PPrint b) => PPrint (Sol a b) Source # 

Methods

pprintTidy :: Tidy -> Sol a b -> Doc Source #

pprintPrec :: Int -> Tidy -> Sol a b -> Doc Source #

(PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) Source # 

Methods

pprintTidy :: Tidy -> (a, b, c) -> Doc Source #

pprintPrec :: Int -> Tidy -> (a, b, c) -> Doc Source #

(PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d) Source # 

Methods

pprintTidy :: Tidy -> (a, b, c, d) -> Doc Source #

pprintPrec :: Int -> Tidy -> (a, b, c, d) -> Doc Source #

(PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e) Source # 

Methods

pprintTidy :: Tidy -> (a, b, c, d, e) -> Doc Source #

pprintPrec :: Int -> Tidy -> (a, b, c, d, e) -> Doc Source #

pprint :: PPrint a => a -> Doc Source #

Top-level pretty printer

showpp :: PPrint a => a -> String Source #

showTable :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> String Source #

tracepp :: PPrint a => String -> a -> a Source #

Please do not alter this.

notracepp :: PPrint a => String -> a -> a Source #

pprintKVs :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc Source #

class PTable a where Source #

Minimal complete definition

ptable

Methods

ptable :: a -> DocTable Source #