Language.Fixpoint.Types

Top level serialization

class Fixpoint a

toFixpoint

data FInfo a

Rendering

showFix

traceFix

resultDoc

Symbols

data Symbol

anfPrefix

tempPrefix

vv

intKvar

symChars

isNonSymbol

nonSymbol

isNontrivialVV

symbolText

symbolString

Creating Symbols

dummySymbol

intSymbol

tempSymbol

qualifySymbol

suffixSymbol

Embedding to Fixpoint Types

data Sort

data FTycon

type TCEmb a

intFTyCon

boolFTyCon

realFTyCon

strFTyCon

propFTyCon

appFTyCon

fTyconSymbol

symbolFTycon

fApp

fObj

Expressions and Predicates

data SymConst

data Constant

data Bop

data Brel

data Expr

data Pred

eVar

eProp

pAnd

pOr

pIte

isTautoPred

symConstLits

zero

Generalizing Embedding with Typeclasses

class Symbolic a

class Expression a

class Predicate a

Constraints and Solutions

data SubC a

data WfC a

sid

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

mapSEnvWithKey

insertSEnv

deleteSEnv

memberSEnv

lookupSEnv

intersectWithSEnv

filterSEnv

lookupSEnvWithDistance

type FEnv

insertFEnv

data IBindEnv

type BindId

emptyIBindEnv

insertsIBindEnv

deleteIBindEnv

data BindEnv

rawBindEnv

insertBindEnv

emptyBindEnv

mapBindEnv

Refinements

data Refa

data SortedReft

data Reft

class Reftable r

Constructing Refinements

trueSortedReft

trueRefa

trueReft

exprReft

notExprReft

uexprReft

symbolReft

propReft

predReft

isFunctionSortedReft

isNonTrivialSortedReft

isTautoReft

isSingletonReft

isEVar

isFalse

flattenRefas

squishRefas

shiftVV

Substitutions

data Subst

class Subable a

mkSubst

substExcept

substfExcept

subst1Except

sortSubst

Visitors

reftKVars

Functions on Result

colorResult

Cut KVars

data Kuts

ksEmpty

ksUnion

Qualifiers

data Qualifier

FQ Definitions

data Def a

Located Values

data Located a

type LocSymbol

type LocText

dummyLoc

dummyPos

dummyName

isDummy