rest-rewrite-0.4.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
adtOC
Language.REST.WQOConstraints.ADT
adtRPO
Language.REST
AlreadyImplied
Language.REST.Internal.WQO
And
Language.REST.SMT
App
Language.REST.RuntimeTerm
apply
Language.REST.RewriteRule
bfs
Language.REST.Internal.WorkStrategy
bimapConstraints
Language.REST.OCAlgebra
checkSat
Language.REST.SMT
checkSat'
Language.REST.SMT
cmapConstraints
Language.REST.WQOConstraints
Const
Language.REST.SMT
ConstraintGen
Language.REST.WQOConstraints
ConstraintsADT
Language.REST.WQOConstraints.ADT
contains
Language.REST.RuntimeTerm
Contradicts
Language.REST.Internal.WQO
contramap
Language.REST.OCAlgebra
Dag
Language.REST.Dot
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
Edge
1 (Type/Class)
Language.REST.Dot
2 (Data Constructor)
Language.REST.Dot
edgeColor
Language.REST.Dot
edgeLabel
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
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
EQ
Language.REST.Types
Equal
Language.REST.SMT
EquivalenceClass
Language.REST.Internal.EquivalenceClass
etStrategy
Language.REST.Rest
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
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
getECs
Language.REST.Internal.WQO
getModel
Language.REST.SMT
getOrdering
Language.REST.WQOConstraints
getPO
Language.REST.Internal.WQO
getRelation
Language.REST.Internal.WQO
GetWork
Language.REST.Internal.WorkStrategy
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
includeInResult
Language.REST.Rest
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
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.Lazy
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
ListT
1 (Type/Class)
Language.REST.Internal.ListT
2 (Data Constructor)
Language.REST.Internal.ListT
lpo
Language.REST.LPO
lpoStrict
Language.REST.LPO
member
Language.REST.Internal.MultiSet
merge
Language.REST.Internal.WQO
mergeAll
Language.REST.Internal.WQO
MetaTerm
Language.REST.MetaTerm
Min
Language.REST.Dot
mkGraph
Language.REST.Dot
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.Lazy
3 (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
nodeStyle
Language.REST.Dot
notStrongerThan
1 (Function)
Language.REST.OCAlgebra
2 (Function)
Language.REST.Internal.WQO
3 (Function)
Language.REST.WQOConstraints
notVisitedFirst
Language.REST.Internal.WorkStrategy
null
1 (Function)
Language.REST.Internal.MultiSet
2 (Function)
Language.REST.Internal.WQO
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
OpOrdering
Language.REST.Internal.OpOrdering
Or
Language.REST.SMT
ordering
Language.REST.Path
orderings
Language.REST.Internal.WQO
orient
Language.REST.Core
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.Strict
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
QEQ
Language.REST.Internal.WQO
QGT
Language.REST.Internal.WQO
QORelation
Language.REST.Internal.WQO
re
Language.REST.Rest
refine
Language.REST.OCAlgebra
rejected
Language.REST.Path
Relation
Language.REST.Types
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
RESTResult
Language.REST.Rest
resultTerms
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
ru
Language.REST.Rest
rule
Language.REST.Path
runListT
Language.REST.Internal.ListT
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
showRejects
Language.REST.RESTDot
ShowRejectsOpt
Language.REST.RESTDot
ShowRejectsWithoutRule
Language.REST.RESTDot
ShowRejectsWithRule
Language.REST.RESTDot
singleton
1 (Function)
Language.REST.Internal.MultiSet
2 (Function)
Language.REST.Internal.EquivalenceClass
3 (Function)
Language.REST.Internal.WQO
4 (Function)
Language.REST.WQOConstraints
size
Language.REST.ExploredTerms
smtAdd
Language.REST.SMT
smtAnd
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
Subst
Language.REST.Internal.Rewrite
subst
Language.REST.Internal.Rewrite
subsumes
Language.REST.ExploredTerms
subTerms
Language.REST.RuntimeTerm
synGTE
Language.REST.RPO
target
Language.REST.Rest
term
Language.REST.Path
TermsResult
Language.REST.Rest
termsResult
Language.REST.Rest
to
Language.REST.Dot
toDescsList
Language.REST.Internal.PartialOrder
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
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
Tree
Language.REST.Dot
unify
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
unionAll
Language.REST.WQOConstraints
unionDisjointUnsafe
Language.REST.Internal.PartialOrder
Unsat
Language.REST.WQOConstraints.ADT
unsatisfiable
Language.REST.WQOConstraints
ValidExtension
Language.REST.Internal.WQO
Var
1 (Data Constructor)
Language.REST.SMT
2 (Data Constructor)
Language.REST.MetaTerm
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
Language.REST.Internal.WQO
WQOConstraints
Language.REST.WQOConstraints
writeDot
Language.REST.RESTDot
Z3Model
Language.REST.SMT