Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.PrettyPrint

Synopsis

traceFix :: Fixpoint a => String -> a -> a
class Fixpoint a where
- toFix :: a -> Doc
- simplify :: a -> a
showFix :: Fixpoint a => a -> String
data Tidy
- = Lossy
- | Full
class PPrint a where
- pprintTidy :: Tidy -> a -> Doc
- pprintPrec :: Int -> Tidy -> a -> Doc
pprint :: PPrint a => a -> Doc
showpp :: PPrint a => a -> String
showTable :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> String
tracepp :: PPrint a => String -> a -> a
notracepp :: PPrint a => String -> a -> a
pprintKVs :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc
newtype DocTable = DocTable [(Doc, Doc)]
class PTable a where
- ptable :: a -> DocTable
boxHSep :: Doc -> Doc -> Doc
boxDoc :: Box -> Doc
docBox :: Doc -> Box

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 Methods toFix :: Bool -> Doc Source # simplify :: Bool -> Bool Source #
Fixpoint Double Source #
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods toFix :: Double -> Doc Source # simplify :: Double -> Double Source #
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 Methods toFix :: Integer -> Doc Source # simplify :: Integer -> Integer Source #
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 Methods toFix :: Text -> Doc Source # simplify :: Text -> Text Source #
Fixpoint SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods toFix :: SourcePos -> Doc Source # simplify :: SourcePos -> SourcePos Source #
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 Methods toFix :: Symbol -> Doc Source # simplify :: Symbol -> Symbol Source #
Fixpoint DataDecl Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: DataDecl -> Doc Source # simplify :: DataDecl -> DataDecl Source #
Fixpoint DataCtor Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: DataCtor -> Doc Source # simplify :: DataCtor -> DataCtor Source #
Fixpoint DataField Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: DataField -> Doc Source # simplify :: DataField -> DataField Source #
Fixpoint Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: Sort -> Doc Source # simplify :: Sort -> Sort Source #
Fixpoint FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: FTycon -> Doc Source # simplify :: FTycon -> FTycon Source #
Fixpoint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: SortedReft -> Doc Source # simplify :: SortedReft -> SortedReft Source #
Fixpoint Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods toFix :: Reft -> Doc Source # simplify :: Reft -> Reft Source #
Fixpoint Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Expr -> Doc Source # simplify :: Expr -> Expr Source #
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 Methods toFix :: Brel -> Doc Source # simplify :: Brel -> Brel Source #
Fixpoint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Constant -> Doc Source # simplify :: Constant -> Constant Source #
Fixpoint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: SymConst -> Doc Source # simplify :: SymConst -> SymConst Source #
Fixpoint Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: Subst -> Doc Source # simplify :: Subst -> Subst Source #
Fixpoint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods toFix :: KVar -> Doc Source # simplify :: KVar -> KVar Source #
Fixpoint Error1 Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods toFix :: Error1 -> Doc Source # simplify :: Error1 -> Error1 Source #
Fixpoint Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: Packs -> Doc Source # simplify :: Packs -> Packs Source #
Fixpoint EBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: EBindEnv -> Doc Source # simplify :: EBindEnv -> EBindEnv Source #
Fixpoint BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: BindEnv -> Doc Source # simplify :: BindEnv -> BindEnv Source #
Fixpoint IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods toFix :: IBindEnv -> Doc Source # simplify :: IBindEnv -> IBindEnv Source #
Fixpoint TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods toFix :: TheorySymbol -> Doc Source # simplify :: TheorySymbol -> TheorySymbol Source #
Fixpoint Rewrite Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: Rewrite -> Doc Source # simplify :: Rewrite -> Rewrite Source #
Fixpoint Equation Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: Equation -> Doc Source # simplify :: Equation -> Equation Source #
Fixpoint AxiomEnv Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: AxiomEnv -> Doc Source # simplify :: AxiomEnv -> AxiomEnv Source #
Fixpoint Kuts Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: Kuts -> Doc Source # simplify :: Kuts -> Kuts Source #
Fixpoint QualParam Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: QualParam -> Doc Source # simplify :: QualParam -> QualParam Source #
Fixpoint Qualifier Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: Qualifier -> Doc Source # simplify :: Qualifier -> Qualifier Source #
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 Methods toFix :: HashSet a -> Doc Source # simplify :: HashSet a -> HashSet a Source #
Fixpoint a => Fixpoint (Located a) Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods toFix :: Located a -> Doc Source # simplify :: Located a -> Located a Source #
(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: FixResult (SubC a) -> Doc Source # simplify :: FixResult (SubC a) -> FixResult (SubC a) Source #
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 Methods toFix :: HashMap SubcId [AutoRewrite] -> Doc Source # simplify :: HashMap SubcId [AutoRewrite] -> HashMap SubcId [AutoRewrite] Source #
(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 #

showFix :: Fixpoint a => a -> String 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 Methods pprintTidy :: Tidy -> Bool -> Doc Source # pprintPrec :: Int -> Tidy -> Bool -> Doc Source #
PPrint Float Source #
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> Float -> Doc Source # pprintPrec :: Int -> Tidy -> Float -> Doc Source #
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 Methods pprintTidy :: Tidy -> Integer -> Doc Source # pprintPrec :: Int -> Tidy -> Integer -> Doc Source #
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 Methods pprintTidy :: Tidy -> Text -> Doc Source # pprintPrec :: Int -> Tidy -> Text -> Doc Source #
PPrint SourcePos Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SourcePos -> Doc Source # pprintPrec :: Int -> Tidy -> SourcePos -> Doc Source #
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 Methods pprintTidy :: Tidy -> DocTable -> Doc Source # pprintPrec :: Int -> Tidy -> DocTable -> Doc Source #
PPrint SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods pprintTidy :: Tidy -> SrcSpan -> Doc Source # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc Source #
PPrint Symbol Source #
Instance details Defined in Language.Fixpoint.Types.Names Methods pprintTidy :: Tidy -> Symbol -> Doc Source # pprintPrec :: Int -> Tidy -> Symbol -> Doc Source #
PPrint TCArgs Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> TCArgs -> Doc Source # pprintPrec :: Int -> Tidy -> TCArgs -> Doc Source #
PPrint DataDecl Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataDecl -> Doc Source # pprintPrec :: Int -> Tidy -> DataDecl -> Doc Source #
PPrint DataCtor Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataCtor -> Doc Source # pprintPrec :: Int -> Tidy -> DataCtor -> Doc Source #
PPrint DataField Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> DataField -> Doc Source # pprintPrec :: Int -> Tidy -> DataField -> Doc Source #
PPrint Sort Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Sort -> Doc Source # pprintPrec :: Int -> Tidy -> Sort -> Doc Source #
PPrint FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> FTycon -> Doc Source # pprintPrec :: Int -> Tidy -> FTycon -> Doc Source #
PPrint SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> SortedReft -> Doc Source # pprintPrec :: Int -> Tidy -> SortedReft -> Doc Source #
PPrint Reft Source #
Instance details Defined in Language.Fixpoint.Types.Substitutions Methods pprintTidy :: Tidy -> Reft -> Doc Source # pprintPrec :: Int -> Tidy -> Reft -> Doc Source #
PPrint Expr Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Expr -> Doc Source # pprintPrec :: Int -> Tidy -> Expr -> Doc Source #
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 Methods pprintTidy :: Tidy -> Brel -> Doc Source # pprintPrec :: Int -> Tidy -> Brel -> Doc Source #
PPrint Constant Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Constant -> Doc Source # pprintPrec :: Int -> Tidy -> Constant -> Doc Source #
PPrint SymConst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> SymConst -> Doc Source # pprintPrec :: Int -> Tidy -> SymConst -> Doc Source #
PPrint KVSub Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVSub -> Doc Source # pprintPrec :: Int -> Tidy -> KVSub -> Doc Source #
PPrint Subst Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> Subst -> Doc Source # pprintPrec :: Int -> Tidy -> Subst -> Doc Source #
PPrint KVar Source #
Instance details Defined in Language.Fixpoint.Types.Refinements Methods pprintTidy :: Tidy -> KVar -> Doc Source # pprintPrec :: Int -> Tidy -> KVar -> Doc Source #
PPrint Trigger Source #
Instance details Defined in Language.Fixpoint.Types.Triggers Methods pprintTidy :: Tidy -> Trigger -> Doc Source # pprintPrec :: Int -> Tidy -> Trigger -> Doc Source #
PPrint Templates Source #
Instance details Defined in Language.Fixpoint.Types.Templates Methods pprintTidy :: Tidy -> Templates -> Doc Source # pprintPrec :: Int -> Tidy -> Templates -> Doc Source #
PPrint Error1 Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error1 -> Doc Source # pprintPrec :: Int -> Tidy -> Error1 -> Doc Source #
PPrint Error Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error -> Doc Source # pprintPrec :: Int -> Tidy -> Error -> Doc Source #
PPrint Packs Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> Packs -> Doc Source # pprintPrec :: Int -> Tidy -> Packs -> Doc Source #
PPrint IBindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Environments Methods pprintTidy :: Tidy -> IBindEnv -> Doc Source # pprintPrec :: Int -> Tidy -> IBindEnv -> Doc Source #
PPrint SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> SmtSort -> Doc Source # pprintPrec :: Int -> Tidy -> SmtSort -> Doc Source #
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 Methods pprintTidy :: Tidy -> TheorySymbol -> Doc Source # pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc Source #
PPrint Rewrite Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Rewrite -> Doc Source # pprintPrec :: Int -> Tidy -> Rewrite -> Doc Source #
PPrint Equation Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Equation -> Doc Source # pprintPrec :: Int -> Tidy -> Equation -> Doc Source #
PPrint AxiomEnv Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> AxiomEnv -> Doc Source # pprintPrec :: Int -> Tidy -> AxiomEnv -> Doc Source #
PPrint QualPattern Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualPattern -> Doc Source # pprintPrec :: Int -> Tidy -> QualPattern -> Doc Source #
PPrint QualParam Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> QualParam -> Doc Source # pprintPrec :: Int -> Tidy -> QualParam -> Doc Source #
PPrint Qualifier Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> Qualifier -> Doc Source # pprintPrec :: Int -> Tidy -> Qualifier -> Doc Source #
PPrint GFixSolution Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods pprintTidy :: Tidy -> GFixSolution -> Doc Source # pprintPrec :: Int -> Tidy -> GFixSolution -> Doc Source #
PPrint Command Source #
Instance details Defined in Language.Fixpoint.Smt.Types Methods pprintTidy :: Tidy -> Command -> Doc Source # pprintPrec :: Int -> Tidy -> Command -> Doc Source #
PPrint BindPred Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BindPred -> Doc Source # pprintPrec :: Int -> Tidy -> BindPred -> Doc Source #
PPrint BIndex Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> BIndex -> Doc Source # pprintPrec :: Int -> Tidy -> BIndex -> Doc Source #
PPrint KIndex Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> KIndex -> Doc Source # pprintPrec :: Int -> Tidy -> KIndex -> Doc Source #
PPrint EQual Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> EQual -> Doc Source # pprintPrec :: Int -> Tidy -> EQual -> Doc Source #
PPrint Cube Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> Cube -> Doc Source # pprintPrec :: Int -> Tidy -> Cube -> Doc Source #
PPrint EbindSol Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> EbindSol -> Doc Source # pprintPrec :: Int -> Tidy -> EbindSol -> Doc Source #
PPrint QBind Source #
Instance details Defined in Language.Fixpoint.Types.Solutions Methods pprintTidy :: Tidy -> QBind -> Doc Source # pprintPrec :: Int -> Tidy -> QBind -> Doc Source #
PPrint Bind Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Bind -> Doc Source # pprintPrec :: Int -> Tidy -> Bind -> Doc Source #
PPrint Pred Source #
Instance details Defined in Language.Fixpoint.Horn.Types Methods pprintTidy :: Tidy -> Pred -> Doc Source # pprintPrec :: Int -> Tidy -> Pred -> Doc Source #
PPrint Rank Source #
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> Rank -> Doc Source # pprintPrec :: Int -> Tidy -> Rank -> Doc Source #
PPrint KVGraph Source #
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> KVGraph -> Doc Source # pprintPrec :: Int -> Tidy -> KVGraph -> Doc Source #
PPrint CVertex Source #
Instance details Defined in Language.Fixpoint.Graph.Types Methods pprintTidy :: Tidy -> CVertex -> Doc Source # pprintPrec :: Int -> Tidy -> CVertex -> Doc Source #
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 Methods pprintTidy :: Tidy -> HashSet a -> Doc Source # pprintPrec :: Int -> Tidy -> HashSet a -> Doc Source #
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 Methods pprintTidy :: Tidy -> Located a -> Doc Source # pprintPrec :: Int -> Tidy -> Located a -> Doc Source #
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 Methods pprintTidy :: Tidy -> Triggered a -> Doc Source # pprintPrec :: Int -> Tidy -> Triggered a -> Doc Source #
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 Methods pprintTidy :: Tidy -> Worklist a -> Doc Source # pprintPrec :: Int -> Tidy -> Worklist a -> Doc Source #
(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 #

newtype DocTable Source #

Constructors

DocTable [(Doc, Doc)]

Instances

Semigroup DocTable Source #
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods (<>) :: DocTable -> DocTable -> DocTable # sconcat :: NonEmpty DocTable -> DocTable # stimes :: Integral b => b -> DocTable -> DocTable #
Monoid DocTable Source #
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods mempty :: DocTable # mappend :: DocTable -> DocTable -> DocTable # mconcat :: [DocTable] -> DocTable #
PPrint DocTable Source #
Instance details Defined in Language.Fixpoint.Types.PrettyPrint Methods pprintTidy :: Tidy -> DocTable -> Doc Source # pprintPrec :: Int -> Tidy -> DocTable -> Doc Source #

class PTable a where Source #

Methods

ptable :: a -> DocTable Source #

Instances

PTable Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods ptable :: Stats -> DocTable Source #
PTable Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Worklist Methods ptable :: Stats -> DocTable Source #
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 Methods ptable :: Worklist a -> DocTable Source #

boxHSep :: Doc -> Doc -> Doc Source #

boxDoc :: Box -> Doc Source #

docBox :: Doc -> Box Source #