Language.Fixpoint.Types

Top level serialization

class Fixpoint a

toFixpoint

data FInfo a

Rendering

showFix

traceFix

resultDoc

Embedding to Fixpoint Types

data Sort

data FTycon

type TCEmb a

intFTyCon

boolFTyCon

strFTyCon

propFTyCon

stringFTycon

fTyconString

Symbols

data Symbol

anfPrefix

tempPrefix

vv

intKvar

symChars

isNonSymbol

nonSymbol

isNontrivialVV

stringSymbol

symbolString

Creating Symbols

dummySymbol

intSymbol

tempSymbol

qualifySymbol

stringSymbolRaw

suffixSymbol

Expressions and Predicates

data SymConst

data Constant

data Bop

data Brel

data Expr

data Pred

eVar

eProp

pAnd

pOr

pIte

isTautoPred

Generalizing Embedding with Typeclasses

class Symbolic a

class Expression a

class Predicate a

Constraints and Solutions

data SubC a

data WfC a

subC

lhsCs

rhsCs

wfC

type Tag

data FixResult a

type FixSolution

addIds

sinfo

trueSubCKvar

removeLhsKvars

Environments

data SEnv a

data SESearch a

emptySEnv

toListSEnv

fromListSEnv

mapSEnv

insertSEnv

deleteSEnv

memberSEnv

lookupSEnv

intersectWithSEnv

filterSEnv

lookupSEnvWithDistance

type FEnv

insertFEnv

data IBindEnv

type BindId

insertsIBindEnv

deleteIBindEnv

emptyIBindEnv

data BindEnv

insertBindEnv

emptyBindEnv

Refinements

data Refa

data SortedReft

data Reft

class Reftable r

Constructing Refinements

trueSortedReft

trueRefa

exprReft

notExprReft

symbolReft

propReft

predReft

isFunctionSortedReft

isNonTrivialSortedReft

isTautoReft

isSingletonReft

isEVar

isFalse

flattenRefas

squishRefas

shiftVV

Substitutions

data Subst

class Subable a

emptySubst

mkSubst

catSubst

substExcept

substfExcept

subst1Except

sortSubst

Visitors

reftKVars

Functions on Result

colorResult

Cut KVars

data Kuts

ksEmpty

ksUnion

Qualifiers

data Qualifier