rest-rewrite-0.3.0: Rewriting library with online termination checking
Contents
Index
Index
<.
Language.REST.Internal.OpOrdering
=.
Language.REST.Internal.OpOrdering
>.
Language.REST.Internal.OpOrdering
Add
Language.REST.SMT
addConstraint
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Lazy
4 (Function)
Language.REST.WQOConstraints.Strict
adtOC
Language.REST.WQOConstraints.ADT
adtOC'
Language.REST.WQOConstraints.ADT
adtRPO
Language.REST
AlreadyImplied
Language.REST.Internal.WQO
And
Language.REST.SMT
App
Language.REST.RuntimeTerm
app
Language.REST.SMT
apply
Language.REST.RewriteRule
askCmds
Language.REST.SMT
bfs
Language.REST.Internal.WorkStrategy
bfs'
Language.REST.Internal.WorkStrategy
bimapConstraints
Language.REST.OCAlgebra
cached
Language.REST.WQOConstraints.ADT
cached'
Language.REST.WQOConstraints.ADT
canOrient
Language.REST.Core
cgen
Language.REST
CheckSat
Language.REST.SMT
checkSat
Language.REST.SMT
checkSat'
Language.REST.SMT
cmapConstraints
Language.REST.WQOConstraints
commandString
Language.REST.SMT
commutesLast
Language.REST.Internal.WorkStrategy
Const
Language.REST.SMT
ConstraintGen
Language.REST.WQOConstraints
ConstraintsADT
Language.REST.WQOConstraints.ADT
contains
Language.REST.Core
Contradicts
Language.REST.Internal.WQO
contramap
Language.REST.OCAlgebra
cost
Language.REST.WQOConstraints.ADT
cs
Language.REST.WQOConstraints.ADT
Dag
Language.REST.Dot
DeclareVar
Language.REST.SMT
delete
Language.REST.Internal.MultiSet
deleteMany
Language.REST.Internal.MultiSet
descendents
Language.REST.Internal.PartialOrder
difference
Language.REST.WQOConstraints.Strict
DiGraph
1 (Type/Class)
Language.REST.Dot
2 (Data Constructor)
Language.REST.Dot
distinctElems
Language.REST.Internal.MultiSet
dnfSize
Language.REST.WQOConstraints.ADT
DotPath
Language.REST.Dot
Edge
1 (Type/Class)
Language.REST.Dot
2 (Data Constructor)
Language.REST.Dot
edgeColor
Language.REST.Dot
edgeLabel
Language.REST.Dot
edgeString
Language.REST.Dot
edgeStyle
Language.REST.Dot
EF
Language.REST.ExploredTerms
elems
1 (Function)
Language.REST.Internal.PartialOrder
2 (Function)
Language.REST.Internal.EquivalenceClass
3 (Function)
Language.REST.Internal.WQO
4 (Function)
Language.REST.WQOConstraints
5 (Function)
Language.REST.WQOConstraints.Strict
empty
1 (Function)
Language.REST.ExploredTerms
2 (Function)
Language.REST.Internal.MultiSet
3 (Function)
Language.REST.Internal.PartialOrder
4 (Function)
Language.REST.Internal.WQO
,
Language.REST.Internal.OpOrdering
endNode
Language.REST.RESTDot
EQ
Language.REST.Types
Equal
Language.REST.SMT
EquivalenceClass
Language.REST.Internal.EquivalenceClass
etStrategy
Language.REST.Rest
eval
Language.REST.Core
ExploreAlways
Language.REST.ExploredTerms
ExploredTerms
Language.REST.ExploredTerms
ExploreFuncs
Language.REST.ExploredTerms
ExploreLessConstrained
Language.REST.ExploredTerms
ExploreOnce
Language.REST.ExploredTerms
ExploreStrategy
Language.REST.ExploredTerms
ExploreWhenNeeded
Language.REST.ExploredTerms
exprString
Language.REST.SMT
exRefine
Language.REST.ExploredTerms
ExtendOrderingResult
Language.REST.Internal.WQO
filter
Language.REST.Internal.MultiSet
from
Language.REST.Dot
fromList
1 (Function)
Language.REST.Internal.MultiSet
2 (Function)
Language.REST.Internal.EquivalenceClass
fromPLE
Language.REST.Path
fuelOC
Language.REST.OCAlgebra
GCMonad
Language.REST.WQOConstraints.ADT
GCResult
Language.REST.WQOConstraints.ADT
GCState
1 (Type/Class)
Language.REST.WQOConstraints.ADT
2 (Data Constructor)
Language.REST.WQOConstraints.ADT
getConstraints
Language.REST.WQOConstraints.ADT
getConstraints'
Language.REST.WQOConstraints.ADT
getECs
Language.REST.Internal.WQO
getModel
Language.REST.SMT
getName
Language.REST.Internal.Rewrite
getNodeID
Language.REST.RESTDot
getOrdering
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.Strict
getPO
Language.REST.Internal.WQO
getRelation
Language.REST.Internal.WQO
getVars
Language.REST
GetWork
Language.REST.Internal.WorkStrategy
graphString
Language.REST.Dot
GraphType
Language.REST.Dot
Greater
Language.REST.SMT
GT
Language.REST.Types
gt
Language.REST.Internal.PartialOrder
GTE
1 (Data Constructor)
Language.REST.SMT
2 (Data Constructor)
Language.REST.Types
head
Language.REST.Internal.EquivalenceClass
HideRejects
Language.REST.RESTDot
Implies
Language.REST.SMT
initRes
Language.REST.Rest
insert
1 (Function)
Language.REST.ExploredTerms
2 (Function)
Language.REST.Internal.MultiSet
3 (Function)
Language.REST.Internal.PartialOrder
4 (Function)
Language.REST.Internal.EquivalenceClass
5 (Function)
Language.REST.Internal.WQO
insertMaybe
Language.REST.Internal.WQO
insertUnsafe
Language.REST.Internal.PartialOrder
Intersect
Language.REST.WQOConstraints.ADT
intersect
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Lazy
4 (Function)
Language.REST.WQOConstraints.Strict
intersectAll
Language.REST.WQOConstraints
intersectRelation
Language.REST.WQOConstraints
isEmpty
Language.REST.Internal.PartialOrder
isMember
Language.REST.Internal.EquivalenceClass
isSat
Language.REST.OCAlgebra
isSatisfiable
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Lazy
4 (Function)
Language.REST.WQOConstraints.Strict
isSingleton
Language.REST.Internal.EquivalenceClass
isSubsetOf
Language.REST.Internal.EquivalenceClass
isUnsatisfiable
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.Strict
kbo
Language.REST.KBO
kboGTE
Language.REST.KBO
killZ3
Language.REST.SMT
label
Language.REST.Dot
labelColor
Language.REST.Dot
LazyOC
Language.REST.WQOConstraints.Lazy
lazyOC
Language.REST.WQOConstraints.Lazy
lift
Language.REST.OCToAbstract
liftC
Language.REST.WQOConstraints
lpo
Language.REST.LPO
lpoStrict
Language.REST.LPO
maxDepth
Language.REST.WQOConstraints.ADT
member
Language.REST.Internal.MultiSet
merge
Language.REST.Internal.WQO
,
Language.REST.Internal.OpOrdering
mergeAll
Language.REST.Internal.WQO
MetaTerm
1 (Type/Class)
Language.REST.MetaTerm
2 (Type/Class)
Language.REST.Core
Min
Language.REST.Dot
minDepth
Language.REST.WQOConstraints.ADT
mkGraph
Language.REST.Dot
modelParser
Language.REST.SMT
ms
Language.REST.WQOConstraints.ADT
MultiSet
Language.REST.Internal.MultiSet
multisetOrder
Language.REST.Internal.MultisetOrder
named
Language.REST.Internal.Rewrite
noConstraints
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Lazy
4 (Function)
Language.REST.WQOConstraints.Strict
Node
1 (Type/Class)
Language.REST.Dot
2 (Data Constructor)
Language.REST.Dot
NodeID
Language.REST.Dot
nodeID
Language.REST.Dot
nodeString
Language.REST.Dot
nodeStyle
Language.REST.Dot
notStrongerThan
1 (Function)
Language.REST.OCAlgebra
2 (Function)
Language.REST.Internal.WQO
3 (Function)
Language.REST.WQOConstraints
4 (Function)
Language.REST.WQOConstraints.ADT
5 (Function)
Language.REST.WQOConstraints.Strict
notVisitedFirst
Language.REST.Internal.WorkStrategy
notVisitedFirst'
Language.REST.Internal.WorkStrategy
null
1 (Function)
Language.REST.Internal.MultiSet
2 (Function)
Language.REST.Internal.WQO
numOrderings
Language.REST.WQOConstraints
OC
Language.REST.WQOConstraints
OCAlgebra
1 (Type/Class)
Language.REST.OCAlgebra
2 (Data Constructor)
Language.REST.OCAlgebra
ocImpl
Language.REST.Rest
Op
1 (Type/Class)
Language.REST.Op
2 (Data Constructor)
Language.REST.Op
opEQ
Language.REST.Internal.OpOrdering
opGT
Language.REST.Internal.OpOrdering
opInsert
Language.REST.Internal.OpOrdering
OpOrdering
Language.REST.Internal.OpOrdering
Or
Language.REST.SMT
ordering
Language.REST.Path
orderings
Language.REST.Internal.WQO
orient
Language.REST.Core
orient'
Language.REST.Core
parens
Language.REST.SMT
parseFunDef
Language.REST.SMT
parseModel
Language.REST.SMT
parseOO
Language.REST.Internal.OpOrdering
PartialOrder
Language.REST.Internal.PartialOrder
Path
Language.REST.Path
PathsResult
1 (Type/Class)
Language.REST.Rest
2 (Data Constructor)
Language.REST.Rest
pathsResult
Language.REST.Rest
PathTerm
1 (Type/Class)
Language.REST.Path
2 (Data Constructor)
Language.REST.Path
pathTerm
Language.REST.Path
pathTerms
Language.REST.Path
permits
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Strict
Pop
Language.REST.SMT
possibilities
Language.REST.Internal.MultisetOrder
PPArgs
1 (Type/Class)
Language.REST.Types
2 (Data Constructor)
Language.REST.Types
ppCustom
Language.REST.Types
ppInfixOps
Language.REST.Types
ppReplace
Language.REST.Types
prettyPrint
Language.REST.Types
PrettyPrinter
1 (Type/Class)
Language.REST.RESTDot
2 (Data Constructor)
Language.REST.RESTDot
printOrd
Language.REST.RESTDot
printRule
Language.REST.RESTDot
printTerm
Language.REST.RESTDot
Push
Language.REST.SMT
QEQ
Language.REST.Internal.WQO
QGT
Language.REST.Internal.WQO
QORelation
Language.REST.Internal.WQO
re
Language.REST.Rest
readModel
Language.REST.SMT
refine
Language.REST.OCAlgebra
rejected
Language.REST.Path
rejectedNodes
Language.REST.RESTDot
rejNodeID
Language.REST.RESTDot
Relation
Language.REST.Types
relevantConstraints
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Strict
relevantTo
Language.REST.Internal.WQO
removeEqBy
Language.REST.Internal.Util
replaceUnsafe
Language.REST.Internal.PartialOrder
rest
Language.REST.Rest
RESTParams
1 (Type/Class)
Language.REST.Rest
2 (Data Constructor)
Language.REST.Rest
Rewrite
1 (Type/Class)
Language.REST.Internal.Rewrite
2 (Data Constructor)
Language.REST.Internal.Rewrite
RewriteRule
Language.REST.RewriteRule
rpo
Language.REST.RPO
rpoGTE
Language.REST.RPO
rpoGTE'
Language.REST.RPO
rpoTerm
Language.REST.RPO
ru
Language.REST.Rest
rule
Language.REST.Path
runStateConstraints
Language.REST.WQOConstraints
RuntimeTerm
Language.REST.RuntimeTerm
runtimeTerm
Language.REST.Path
RWApp
Language.REST.MetaTerm
Sat
Language.REST.WQOConstraints.ADT
shouldExplore
Language.REST.ExploredTerms
showHash
Language.REST.OCToAbstract
showRejects
Language.REST.RESTDot
ShowRejectsOpt
Language.REST.RESTDot
ShowRejectsWithoutRule
Language.REST.RESTDot
ShowRejectsWithRule
Language.REST.RESTDot
simplify
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
singleton
1 (Function)
Language.REST.Internal.MultiSet
2 (Function)
Language.REST.Internal.EquivalenceClass
3 (Function)
Language.REST.Internal.WQO
4 (Function)
Language.REST.WQOConstraints
5 (Function)
Language.REST.WQOConstraints.Lazy
6 (Function)
Language.REST.WQOConstraints.Strict
size
Language.REST.ExploredTerms
smtAdd
Language.REST.SMT
smtAnd
Language.REST.SMT
SMTAssert
Language.REST.SMT
SMTCommand
Language.REST.SMT
SMTExpr
Language.REST.SMT
smtFalse
Language.REST.SMT
smtGTE
Language.REST.SMT
smtTrue
Language.REST.SMT
SMTVar
1 (Type/Class)
Language.REST.SMT
2 (Data Constructor)
Language.REST.SMT
SolverHandle
Language.REST.SMT
spawnZ3
Language.REST.SMT
Step
1 (Type/Class)
Language.REST.Path
2 (Data Constructor)
Language.REST.Path
StrictOC
Language.REST.WQOConstraints.Strict
strictOC
Language.REST.WQOConstraints.Strict
strictOC'
Language.REST.WQOConstraints.Strict
subLabel
Language.REST.Dot
subPaths
Language.REST.RESTDot
Subst
Language.REST.Internal.Rewrite
subst
Language.REST.Internal.Rewrite
subsumes
Language.REST.ExploredTerms
subTerms
Language.REST.RuntimeTerm
syms
Language.REST.Core
synGTE
Language.REST.RPO
target
Language.REST.Rest
term
Language.REST.Path
termOps
Language.REST.MetaTerm
termPathStr
Language.REST.Core
terms
Language.REST.Rest
termsResult
Language.REST.Rest
to
Language.REST.Dot
toDescsList
Language.REST.Internal.PartialOrder
toEdges
Language.REST.RESTDot
toFormula
Language.REST.SMT
toGraph
Language.REST.RESTDot
toList
1 (Function)
Language.REST.Internal.MultiSet
2 (Function)
Language.REST.Internal.PartialOrder
3 (Function)
Language.REST.Internal.EquivalenceClass
ToMetaTerm
Language.REST.MetaTerm
toMetaTerm
Language.REST.MetaTerm
toNodes
Language.REST.RESTDot
toOccurList
Language.REST.Internal.MultiSet
toOrderedSet
Language.REST.Types
top
Language.REST.OCAlgebra
ToRuntimeTerm
Language.REST.RuntimeTerm
toRuntimeTerm
Language.REST.RuntimeTerm
toSet
Language.REST.Internal.MultiSet
ToSMT
Language.REST.SMT
toSMT
Language.REST.SMT
ToSMTVar
Language.REST.SMT
toSMTVar
Language.REST.SMT
toUntyped
Language.REST.SMT
trace'
Language.REST.WQOConstraints.ADT
Tree
Language.REST.Dot
UAdd
Language.REST.SMT
UAnd
Language.REST.SMT
UConst
Language.REST.SMT
UEqual
Language.REST.SMT
UGreater
Language.REST.SMT
UGTE
Language.REST.SMT
UImplies
Language.REST.SMT
unify
Language.REST.Internal.Rewrite
unifyAll
Language.REST.Internal.Rewrite
Union
Language.REST.WQOConstraints.ADT
union
1 (Function)
Language.REST.ExploredTerms
2 (Function)
Language.REST.OCAlgebra
3 (Function)
Language.REST.Internal.EquivalenceClass
4 (Function)
Language.REST.WQOConstraints
5 (Function)
Language.REST.WQOConstraints.ADT
6 (Function)
Language.REST.WQOConstraints.Lazy
7 (Function)
Language.REST.WQOConstraints.Strict
unionAll
Language.REST.WQOConstraints
unionDisjointUnsafe
Language.REST.Internal.PartialOrder
Unsat
Language.REST.WQOConstraints.ADT
unsatisfiable
1 (Function)
Language.REST.WQOConstraints
2 (Function)
Language.REST.WQOConstraints.ADT
3 (Function)
Language.REST.WQOConstraints.Lazy
4 (Function)
Language.REST.WQOConstraints.Strict
UntypedExpr
Language.REST.SMT
UOr
Language.REST.SMT
UVar
Language.REST.SMT
ValidExtension
Language.REST.Internal.WQO
Var
1 (Data Constructor)
Language.REST.SMT
2 (Data Constructor)
Language.REST.MetaTerm
vars
Language.REST.SMT
varsEQ
Language.REST
visited
Language.REST.ExploredTerms
withZ3
Language.REST.SMT
WorkStrategy
1 (Type/Class)
Language.REST.Internal.WorkStrategy
,
Language.REST.Rest
2 (Data Constructor)
Language.REST.Internal.WorkStrategy
,
Language.REST.Rest
workStrategy
Language.REST.Rest
WQO
1 (Type/Class)
Language.REST.Internal.WQO
2 (Type/Class)
Language.REST.WQOConstraints.ADT
WQOConstraints
Language.REST.WQOConstraints
writeDot
Language.REST.RESTDot
Z3Model
Language.REST.SMT