liquid-fixpoint-0.8.0.2: 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 # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Fixpoint Double Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Fixpoint Int Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

toFix :: Int -> Doc Source #

simplify :: Int -> Int Source #

Fixpoint Integer Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Fixpoint () Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

toFix :: () -> Doc Source #

simplify :: () -> () Source #

Fixpoint Text Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

Fixpoint SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Fixpoint Doc Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: Doc -> Doc Source #

simplify :: Doc -> Doc Source #

Fixpoint Symbol Source #
NOTE: SymbolText
Use symbolSafeText if you want it to machine-readable, but symbolText if you want it to be human-readable.
Instance details

Defined in Language.Fixpoint.Types.Names

Fixpoint DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Fixpoint Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

Fixpoint Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

toFix :: Bop -> Doc Source #

simplify :: Bop -> Bop Source #

Fixpoint Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Fixpoint Packs Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Fixpoint EBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Fixpoint BindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Fixpoint IBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Fixpoint TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Fixpoint Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint Kuts Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint a => Fixpoint [a] Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

toFix :: [a] -> Doc Source #

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

Fixpoint a => Fixpoint (Maybe a) Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

toFix :: Maybe a -> Doc Source #

simplify :: Maybe a -> Maybe a Source #

(Ord a, Hashable a, Fixpoint a) => Fixpoint (HashSet a) Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Fixpoint a => Fixpoint (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Fixpoint a => Fixpoint (SEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

toFix :: SEnv a -> Doc Source #

simplify :: SEnv a -> SEnv a Source #

Fixpoint a => Fixpoint (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: SimpC a -> Doc Source #

simplify :: SimpC a -> SimpC a Source #

Fixpoint a => Fixpoint (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: SubC a -> Doc Source #

simplify :: SubC a -> SubC a Source #

Fixpoint a => Fixpoint (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: WfC a -> Doc Source #

simplify :: WfC a -> WfC a Source #

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

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

Fixpoint (HashMap SubcId [AutoRewrite]) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

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

Defined in Language.Fixpoint.Types.PrettyPrint

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 # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

Ord Tidy Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

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

Minimal complete definition

Nothing

Methods

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

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

Instances
PPrint Bool Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

PPrint Float Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

PPrint Int Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

PPrint Integer Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

PPrint () Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

PPrint Text Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

PPrint SourcePos Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

PPrint Doc Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

PPrint DocTable Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

PPrint SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

PPrint Symbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Names

PPrint TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint SortedReft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

PPrint Reft Source # 
Instance details

Defined in Language.Fixpoint.Types.Substitutions

PPrint Expr Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Bop Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

PPrint Brel Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Constant Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint SymConst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint KVSub Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Subst Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint KVar Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

PPrint Trigger Source # 
Instance details

Defined in Language.Fixpoint.Types.Triggers

PPrint Templates Source # 
Instance details

Defined in Language.Fixpoint.Types.Templates

PPrint Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

PPrint Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

PPrint Packs Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

PPrint IBindEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

PPrint SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

PPrint Sem Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

PPrint TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

PPrint Rewrite Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Equation Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint AxiomEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint QualPattern Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint QualParam Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Qualifier Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint GFixSolution Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

PPrint Command Source # 
Instance details

Defined in Language.Fixpoint.Smt.Types

PPrint BindPred Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint BIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint KIndex Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint EQual Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint Cube Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint EbindSol Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint QBind Source # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

PPrint Bind Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

PPrint Pred Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

PPrint Rank Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

PPrint KVGraph Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

PPrint CVertex Source # 
Instance details

Defined in Language.Fixpoint.Graph.Types

PPrint a => PPrint [a] Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

PPrint a => PPrint (Maybe a) Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

PPrint a => PPrint (HashSet a) Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Show a => PPrint (Trie a) Source # 
Instance details

Defined in Language.Fixpoint.Utils.Trie

Methods

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

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

PPrint a => PPrint (Located a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

PPrint a => PPrint (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

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

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

PPrint a => PPrint (Triggered a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Triggers

PPrint a => PPrint (SEnv a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Environments

Methods

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

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

Fixpoint a => PPrint (SimpC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Fixpoint a => PPrint (SubC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

Fixpoint a => PPrint (WfC a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

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

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

PPrint (Cstr a) Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

PPrint (Var a) Source # 
Instance details

Defined in Language.Fixpoint.Horn.Types

Methods

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

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

PPrint (Elims a) Source # 
Instance details

Defined in Language.Fixpoint.Graph.Deps

Methods

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

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

PPrint (Worklist a) Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

(PPrint a, PPrint b) => PPrint (Either a b) Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

(PPrint a, PPrint b) => PPrint (a, b) Source # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

Methods

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

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

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

Defined in Language.Fixpoint.Types.PrettyPrint

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 # 
Instance details

Defined in Language.Fixpoint.Types.Solutions

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 # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

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 # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

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 # 
Instance details

Defined in Language.Fixpoint.Types.PrettyPrint

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 #

Methods

ptable :: a -> DocTable Source #

Instances
PTable Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Stats

PTable Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

PTable (SInfo a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Methods

ptable :: SInfo a -> DocTable Source #

PTable (Worklist a) Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist