Language.Fixpoint.Types

Top level serialization

class Fixpoint a

toFixpoint

data FInfo a

Rendering

showFix

traceFix

resultDoc

Symbols

data Symbol

data KVar

anfPrefix

tempPrefix

vv

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

sortFTycon

intFTyCon

boolFTyCon

realFTyCon

intSort

realSort

propSort

boolSort

strSort

listFTyCon

appFTyCon

isListTC

isFAppTyTC

fTyconSymbol

symbolFTycon

fTyconSort

fApp

fObj

Expressions and Predicates

data SymConst

data Constant

data Bop

data Brel

data Expr

data Pred

eVar

eProp

pAnd

pOr

pIte

isTautoPred

symConstLits

Generalizing Embedding with Typeclasses

class Symbolic a

class Expression a

class Predicate a

Constraints

data WfC a

data SubC a

subcId

sid

sgrd

senv

slhs

srhs

subC

lhsCs

rhsCs

wfC

type Tag

Accessing Constraints

envCs

addIds

sinfo

trueSubCKvar

removeLhsKvars

Solutions

data Result a

data FixResult a

type FixSolution

Environments

data SEnv a

data SESearch a

emptySEnv

toListSEnv

fromListSEnv

mapSEnvWithKey

insertSEnv

deleteSEnv

memberSEnv

lookupSEnv

intersectWithSEnv

filterSEnv

lookupSEnvWithDistance

type FEnv

insertFEnv

data IBindEnv

type BindId

type BindMap a

emptyIBindEnv

insertsIBindEnv

deleteIBindEnv

elemsIBindEnv

data BindEnv

beBinds

insertBindEnv

emptyBindEnv

lookupBindEnv

mapBindEnv

adjustBindEnv

bindEnvFromList

bindEnvToList

unionIBindEnv

Refinements

data Refa

data SortedReft

data Reft

class Reftable r

raConjuncts

Constructing Refinements

refa

reft

trueSortedReft

trueRefa

trueReft

exprReft

notExprReft

uexprReft

symbolReft

usymbolReft

propReft

predReft

reftPred

reftBind

isFunctionSortedReft

functionSort

isNonTrivial

isSingletonReft

isEVar

isFalse

flattenRefas

squishRefas

conjuncts

shiftVV

mapPredReft

Substitutions

data Subst

class Subable a

mkSubst

isEmptySubst

substExcept

substfExcept

subst1Except

sortSubst

targetSubstSyms

Functions on Result

colorResult

Cut KVars

data Kuts

ksEmpty

ksUnion

Qualifiers

data Qualifier

Located Values

data Located a

type LocSymbol

type LocText

locAt

dummyLoc

dummyPos

dummyName

isDummy