diff --git a/rest-rewrite.cabal b/rest-rewrite.cabal
--- a/rest-rewrite.cabal
+++ b/rest-rewrite.cabal
@@ -1,6 +1,6 @@
 name:               rest-rewrite
 build-type:         Simple
-version:            0.3.0
+version:            0.4.0
 cabal-version:      2.0
 category:           Rewriting
 maintainer:         Zack Grannan <zgrannan@cs.ubc.ca>
@@ -22,6 +22,7 @@
     Language.REST.Dot
     Language.REST.ExploredTerms
     Language.REST.Internal.EquivalenceClass
+    Language.REST.Internal.ListT
     Language.REST.Internal.MultiSet
     Language.REST.Internal.MultisetOrder
     Language.REST.Internal.OpOrdering
diff --git a/src/Language/REST.hs b/src/Language/REST.hs
--- a/src/Language/REST.hs
+++ b/src/Language/REST.hs
@@ -2,47 +2,16 @@
 
 module Language.REST where
 
-import Control.Monad.Identity
-import Data.Hashable
-import Data.Maybe
-import qualified Data.HashSet as S
-
 import Language.REST.OCAlgebra (OCAlgebra)
 import Language.REST.OCToAbstract
-import Language.REST.WQOConstraints
 import Language.REST.WQOConstraints.ADT (ConstraintsADT, adtOC)
 import Language.REST.RPO
 import Language.REST.RuntimeTerm
 import Language.REST.Op
-import Language.REST.Internal.OpOrdering
-import qualified Language.REST.Internal.WQO as WQO
 import System.IO (Handle)
 
 
+-- | 'adtRPO' Is an ordering constraint algebra derived from the recursive
+-- path ordering; it is a useful general-purpose OCA.
 adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO
 adtRPO z3 = lift (adtOC z3) rpo
--- lazyRPO = lift lazyOC rpo
--- strictRPO = lift strictOC rpo
-
--- Assume vars are arity 0, which is usually correct
-getVars :: RuntimeTerm -> S.HashSet Op
-getVars (App op []) = S.singleton op
-getVars (App _op xs) = S.unions (map getVars xs)
-
-
-varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO.WQO Op
-varsEQ t1 t2 =
-  let
-    vars = getVars t1 `S.union` getVars t2
-  in
-    fromJust $ WQO.mergeAll (map (uncurry (=.)) (pairs (S.toList vars)))
-  where
-    pairs xs | length xs < 2 = []
-    pairs xs | otherwise = zip xs (tail xs)
-
-cgen :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity
-cgen impl r oc t1 t2 =
-  let
-    Identity rpoc = rpo impl r oc t1 t2
-  in
-    return $ addConstraint impl (varsEQ t1 t2) rpoc
diff --git a/src/Language/REST/Core.hs b/src/Language/REST/Core.hs
--- a/src/Language/REST/Core.hs
+++ b/src/Language/REST/Core.hs
@@ -1,59 +1,17 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ImplicitParams #-}
 
+-- | Core REST functions
 module Language.REST.Core where
 
-import Prelude hiding (GT, EQ)
-
-import           Debug.Trace                    ( trace )
-import qualified Data.List                     as L
-import qualified Data.HashSet                      as S
-
 import           Language.REST.OCAlgebra
-import           Language.REST.Types
-import qualified Language.REST.MetaTerm as MT
-import           Language.REST.Internal.Rewrite
-import           Language.REST.RuntimeTerm as RT
-import           Language.REST.RewriteRule
-
-type MetaTerm = MT.MetaTerm
-
-
-contains :: RuntimeTerm -> RuntimeTerm -> Bool
-contains t1 t2 | t1 == t2 = True
-contains (App _ ts) t     = any (contains t) ts
-
-
-orient' :: Show oc => (?impl :: OCAlgebra oc RuntimeTerm m) => oc -> [RuntimeTerm] -> oc
-orient' oc0 ts0 = go oc0 (zip ts0 (tail ts0))
-  where
-    go oc []            = oc
-    go oc ((t0, t1):ts) = go (refine ?impl oc t0 t1) ts
+import           Language.REST.RuntimeTerm
 
-orient :: Show oc =>  OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc
-orient impl = orient' (top impl)
+-- | @orient impl ts@ generates the constraints on an ordering defined by the
+--   OCA `impl`, that ensures each term in the path `ts` is smaller than or
+--   equal to the previous one.
+orient :: OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc
+orient impl ts0 = go (top impl) (zip ts0 (tail ts0))
    where
-     ?impl = impl
-
-canOrient :: forall oc m . Show oc
-  => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool
-canOrient terms = trace ("Try to orient " ++ termPathStr terms) $ isSat ?impl (orient ?impl terms)
-
-syms :: MetaTerm -> S.HashSet String
-syms (MT.Var s)      = S.singleton s
-syms (MT.RWApp _ xs) = S.unions (map syms xs)
-
-termPathStr :: [RuntimeTerm] -> String
-termPathStr terms = L.intercalate " --> \n" (map pp terms)
-  where
-    pp = prettyPrint (PPArgs [] [] (const Nothing))
-
-eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm
-eval rws t0 =
-  do
-    result <- mapM (apply t0) (S.toList rws)
-    case S.toList $ S.unions result of
-      []      -> return t0
-      (t : _) -> eval rws t
+    go oc []            = oc
+    go oc ((t0, t1):ts) = go (refine impl oc t0 t1) ts
diff --git a/src/Language/REST/Dot.hs b/src/Language/REST/Dot.hs
--- a/src/Language/REST/Dot.hs
+++ b/src/Language/REST/Dot.hs
@@ -2,7 +2,15 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-module Language.REST.Dot where
+-- | This module contains functionality for generating GraphViz graphs
+module Language.REST.Dot
+  ( mkGraph
+  , DiGraph(..)
+  , Edge(..)
+  , GraphType(..)
+  , Node(..)
+  , NodeID
+  ) where
 
 import GHC.Generics
 import Data.Hashable
@@ -11,12 +19,24 @@
 import Text.Printf
 import System.Process
 
-data DiGraph = DiGraph String (S.Set Node) (S.Set Edge);
+-- | A GraphViz directed graph
+data DiGraph = DiGraph
+  String -- ^ Filename
+  (S.Set Node)
+  (S.Set Edge);
 
 type NodeID =  String
 
-data GraphType = Tree | Dag | Min deriving (Read)
+-- | The way the graph will be rendered
+data GraphType =
+    Tree -- ^ Standard representation
+  | Dag  -- ^ In 'Dag', If two equal terms `n` steps from the root are the same, they are
+         --   represented by the same node, even if they were reached via different
+         --   paths
+  | Min  -- ^ Each unique term is represented by the same node
+  deriving (Read)
 
+-- | A GraphViz node
 data Node = Node 
     { nodeID     :: NodeID
     , label      :: String
@@ -24,6 +44,7 @@
     , labelColor :: String
     } deriving (Eq, Ord, Show, Generic, Hashable)
 
+-- A GraphViz edge
 data Edge = Edge
     { from      :: NodeID
     , to        :: NodeID
@@ -33,8 +54,6 @@
     , edgeStyle :: String
     } deriving (Eq, Ord, Show, Generic, Hashable)
 
-type DotPath = [Node]
-
 nodeString :: Node -> String
 nodeString (Node nid elabel style color) =
     printf "\t%s [label=\"%s\"\nstyle=\"%s\"\ncolor=\"%s\"];" nid elabel style color
@@ -68,6 +87,8 @@
         edgesString = intercalate "\n" (map edgeString (S.toList edges))
 
 
+-- | @mkGraph name graph@ generates the @.dot@ file for @graph@, and renders
+--   the resulting graph to a @png@ file using the @dot@ utility
 mkGraph :: String -> DiGraph -> IO ()
 mkGraph name graph = do
   let dotfile = printf "graphs/%s.dot" name
diff --git a/src/Language/REST/ExploredTerms.hs b/src/Language/REST/ExploredTerms.hs
--- a/src/Language/REST/ExploredTerms.hs
+++ b/src/Language/REST/ExploredTerms.hs
@@ -21,18 +21,34 @@
 
 import Prelude hiding (lookup)
 
+-- | 'ExploreStrategy' defines how 'shouldExplore' should decide whether or not
+-- | to consider rewrites from a given term
 data ExploreStrategy =
-  ExploreAlways | ExploreLessConstrained | ExploreWhenNeeded | ExploreOnce
+    ExploreAlways -- ^ Always explore, even when it's not necessary.
+  | ExploreLessConstrained -- ^ Explore terms unless the constraints are stricter.
+                           -- This may stil explore unnecessary paths, the terms
+                           -- were already fully explored with the different constraints.
+  | ExploreWhenNeeded -- ^ Explore terms unless the constraints are stricter OR if all
+                      --   terms reachable via transitive rewrites were already explored.
+  | ExploreOnce -- ^ Explore each term only once. This may cause some terms not to be
+                --   explored if the terms leading to them were initially visited at
+                --   strict constraints.
 
+
 data ExploreFuncs term c m = EF
-  { union           :: c -> c -> c
+  { -- | When a term @t@ is visited at constraints @c0@, and then at constraints
+    --   @c1@, the constraints for term @t@ is set to @c0 `union` c1@
+    union           :: c -> c -> c
     -- | @c0 `subsumes` c1@ if @c0@ permits all orderings permited by @c1@
   , subsumes        :: c -> c -> m Bool
+    -- | @'exRefine' c t u@ strengthens constraints @c@ to permit the rewrite step
+    --   from @t@ to @u@. This is used to determine if considering term @u@ by rewriting
+    --   from @t@ would permit more rewrite applications.
   , exRefine        :: c -> term -> term -> c
   }
 
--- A mapping of terms, to the rewritten terms that need to be fully explored
--- in order for this term to be fully explored
+-- | A mapping of terms, to the rewritten terms that need to be fully explored
+-- | in order for this term to be fully explored
 data ExploredTerms term c m =
   ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs term c m) ExploreStrategy
 
@@ -54,7 +70,8 @@
 lookup t (ET etMap _ _) = M.lookup t etMap
 
 -- | @isFullyExplored t c M = not explorable(t, c)@ where @explorable@ is
--- defined as in the REST paper.
+-- defined as in the REST paper. Also incorporates an optimization described
+-- here: https://github.com/zgrannan/rest/issues/9
 isFullyExplored :: forall term c m . (Monad m, Eq term, Hashable term, Hashable c, Eq c, Show c) =>
   term -> c -> ExploredTerms term c m -> m Bool
 isFullyExplored t0 oc0 et@(ET _ (EF{subsumes,exRefine}) _) = result where
@@ -89,6 +106,9 @@
   -- There exists a reachable term that has never previously been seen; not fully explored
   go _ _        | otherwise = return False
 
+-- | @'shouldExplore' t c et@ determines if rewrites originating from term @t@ at
+--   constraints @c@ should be considered, given the already explored terms of @et@
+--   and the associated 'ExploreStrategy'
 shouldExplore :: forall term c m . (Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) =>
   term -> c -> ExploredTerms term c m -> m Bool
 shouldExplore t oc et@(ET _ EF{subsumes} strategy) =
diff --git a/src/Language/REST/Internal/ListT.hs b/src/Language/REST/Internal/ListT.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/REST/Internal/ListT.hs
@@ -0,0 +1,44 @@
+-- | Defines a version of the ListT monad transformer, used in the REST search
+
+module Language.REST.Internal.ListT where
+
+import           Control.Applicative
+import           Control.Monad.Trans
+
+data ListT m a = ListT {
+  runListT :: m [a]
+}
+
+instance (Monad m) => Functor (ListT m) where
+  fmap f (ListT mxs) = ListT $ do
+    xs <- mxs
+    return $ map f xs
+
+instance (Monad m) => Applicative (ListT m) where
+  pure x                    = ListT (return [x])
+  (ListT mf) <*> (ListT mx) = ListT $ do
+    fs <- mf
+    xs <- mx
+    return $ do
+      f <- fs
+      map f xs
+
+instance (Monad m) => Monad (ListT m) where
+  return x         = ListT (return [x])
+  (ListT mxs) >>= f = ListT $ do
+    xs <- mxs
+    res <- mapM (runListT . f) xs
+    return $ concat res
+
+instance (Monad m) => Alternative (ListT m) where
+  empty                       = ListT (return [])
+  (ListT mxs) <|> (ListT mys) = ListT $ do
+    xs <- mxs
+    if not $ null xs
+      then mxs
+      else mys
+
+instance MonadTrans ListT where
+  lift mx = ListT $ do
+    x <- mx
+    return [x]
diff --git a/src/Language/REST/Internal/MultiSet.hs b/src/Language/REST/Internal/MultiSet.hs
--- a/src/Language/REST/Internal/MultiSet.hs
+++ b/src/Language/REST/Internal/MultiSet.hs
@@ -31,9 +31,14 @@
 instance Show a => Show (MultiSet a) where
   show ms = "{" ++ L.intercalate ", " (map show $ toList ms) ++ "}"
 
+-- | @delete k m@ removes a single instance of @k@ from the multiset @m.
+--   If @k is not in the multiset, the original multiset is returned
 delete :: (Hashable a, Eq a) => a -> MultiSet a -> MultiSet a
 delete k = deleteMany k 1
 
+-- | @delete k n m@ removes @n@ instances of @k@ from the multiset @m@.
+--   If there are less than @n@ instances of @k@ in the multiset, all
+--   instances are removed.
 deleteMany :: (Hashable a, Eq a) => a -> Int -> MultiSet a -> MultiSet a
 deleteMany k v (MultiSet ms) | Just c <- M.lookup k ms
                              , c > v = MultiSet $ M.insert k (c - v) ms
@@ -56,6 +61,8 @@
 null :: MultiSet a -> Bool
 null (MultiSet ms) = M.null ms
 
+-- | @member k m@ returns @true@ iff there is at least one instance of @k@
+--   in @m@
 member :: (Eq a, Hashable a) => a -> MultiSet a -> Bool
 member k (MultiSet ms) = M.member k ms
 
diff --git a/src/Language/REST/Internal/MultisetOrder.hs b/src/Language/REST/Internal/MultisetOrder.hs
--- a/src/Language/REST/Internal/MultisetOrder.hs
+++ b/src/Language/REST/Internal/MultisetOrder.hs
@@ -3,7 +3,10 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
 
-module Language.REST.Internal.MultisetOrder (multisetOrder, possibilities) where
+-- | This module defines a constraint generator for a multiset
+--   quasi-ordering. For more details, please see the definition
+--   of @mul@ in section 4.2.1 of the paper.
+module Language.REST.Internal.MultisetOrder (multisetOrder) where
 
 import GHC.Generics
 import qualified Data.List as L
@@ -49,6 +52,10 @@
       (possibilities GTE xs (filter (not . flip elem ys') ys))
 
 
+-- | Given a [constraint generator]("Language.REST.WQOConstraints#t:ConstraintGen") @cgen@ that generates constraints a WQO on
+--   @base@ implied by a relation between elements of @lifted@, @'multisetOrder' cgen@
+--   yields a constraint generator on elements of base implied by a relation between
+--   multisets of @lifted@.
 multisetOrder :: forall oc base lifted m . (Ord lifted, Ord base, Show base, Eq base, Hashable base, Hashable lifted, Eq lifted, Show (oc base), Eq (oc base),  Monad m) =>
      ConstraintGen oc base lifted m
   -> ConstraintGen oc base (MultiSet lifted) m
diff --git a/src/Language/REST/Internal/OpOrdering.hs b/src/Language/REST/Internal/OpOrdering.hs
--- a/src/Language/REST/Internal/OpOrdering.hs
+++ b/src/Language/REST/Internal/OpOrdering.hs
@@ -3,12 +3,11 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
-
+-- | This module defines an interface for 'WQO's on 'Op'erators,
+--   for example, that are used as the precedence for an [RPQO]("Language.REST.RPO").
 module Language.REST.Internal.OpOrdering (
     empty
-  , merge
   , OpOrdering
-  , opInsert
   , opGT
   , opEQ
   , (=.)
@@ -31,33 +30,31 @@
 type OpOrdering   = WQO Op
 
 
+-- | @opGT o f g@ returns @true@ if @f > g@ in @o@
 opGT :: OpOrdering -> Op -> Op -> Bool
 opGT s f g = getRelation s f g == Just QGT
 
+-- | @opEQ o f g@ returns @true@ if @f = g@ in @o@
 opEQ :: OpOrdering -> Op -> Op -> Bool
 opEQ s f g = getRelation s f g == Just QEQ
 
-
-opInsert :: OpOrdering -> Op -> Op -> QORelation -> Maybe OpOrdering
-opInsert o f g r =
-  case WQO.insert o (f, g, r) of
-    ValidExtension o' -> Just o'
-    _                 -> Nothing
-
--- The following only are valid if f /= g.
-
--- precondition : f /= g
+-- |  @f >. g@ generates a new ordering with @f@ greater than @g@.
+--   This function is undefined if f == g.
 (>.) :: Op -> Op -> OpOrdering
 (>.) f g = fromJust $ WQO.singleton (f, g, QGT)
 
--- precondition : f /= g
+-- |  @f =. g@ generates a new ordering with @f@ equal to @g@.
+--   This function is undefined if f == g.
 (=.) :: Op -> Op -> OpOrdering
 (=.) f g = fromJust $ WQO.singleton (f, g, QEQ)
 
--- precondition : f /= g
+-- |  @f <. g@ generates a new ordering with @f@ less than @g@.
+--   This function is undefined if f == g.
 (<.) :: Op -> Op -> OpOrdering
 (<.) f g = g >. f
 
+-- | @parseOO str@ returns the ordering defined by @str@. If the input describes
+--   /any/ ordering, (i.e "f = f"), then this function returns 'Nothing'.
 parseOO :: String -> Maybe OpOrdering
 parseOO str =
   case parse parser "" str of
diff --git a/src/Language/REST/Internal/Rewrite.hs b/src/Language/REST/Internal/Rewrite.hs
--- a/src/Language/REST/Internal/Rewrite.hs
+++ b/src/Language/REST/Internal/Rewrite.hs
@@ -3,7 +3,13 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 
-module Language.REST.Internal.Rewrite where
+module Language.REST.Internal.Rewrite
+  ( Rewrite(..)
+  , Subst
+  , named
+  , subst
+  , unify
+  ) where
 
 import GHC.Generics (Generic)
 
@@ -17,17 +23,24 @@
 import Language.REST.RuntimeTerm
 
 
+-- | @Rewrite t u s@ defines a rewrite rule \( t \rightarrow u \), with
+--   an optional name @s@.
 data Rewrite = Rewrite MetaTerm MetaTerm (Maybe String)
   deriving (Eq, Ord, Generic, Hashable, Show)
 
+-- | 'Subst' is a mapping from variable names to 'RuntimeTerm's.
+--   Normally this would be generated by unifying the left-hand-side of
+--   a 'Rewrite' with a term.
 type Subst = M.HashMap String RuntimeTerm
 
-getName :: Rewrite -> Maybe String
-getName (Rewrite _t _u n) = n
-
+-- | @named r n@ assigns the name @n@ to rule @r@, replacing any
+--   existing name
 named :: Rewrite -> String -> Rewrite
 named (Rewrite t u _) n = Rewrite t u (Just n)
 
+-- | @subst s m@ replaces the variables in the 'MetaTerm' @m@ with 'RuntimeTerm's
+--   in the substitution 's'. This function returns an error if any variables in 'm'
+--   do not have a substituion
 subst :: Subst -> MetaTerm -> RuntimeTerm
 subst s (MT.Var v)  | Just t <- M.lookup v s = t
                     | otherwise
@@ -42,6 +55,9 @@
   | otherwise
   = Nothing
 
+-- | @unify m r su@ extends the substitution @su@ to generate a new
+--   substitution that unifies @m@ and @r@. Returns 'Nothing' if su
+--   cannot be extended to unify the terms.
 unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
 unify (MT.Var s) term su | M.lookup s su == Just term
   = Just su
diff --git a/src/Language/REST/Internal/Util.hs b/src/Language/REST/Internal/Util.hs
--- a/src/Language/REST/Internal/Util.hs
+++ b/src/Language/REST/Internal/Util.hs
@@ -2,6 +2,10 @@
 
 import qualified Data.List as L
 
+-- | @removeEqBy f xs ys@ removes elements from @xs@ and @ys@ such that for each
+--  element x removed from xs, an element y is removed from ys such @f x y@.
+--  In other words in the result @(xs', ys')@, there does not exist any @x@ in
+--  @xs'@, @y@ in @ys'@ such that @f x y@.
 removeEqBy :: (Eq a) => (a -> a -> Bool) -> [a] -> [a] -> ([a], [a])
 removeEqBy _ [] ys = ([], ys)
 removeEqBy f (x : xs) ys
diff --git a/src/Language/REST/Internal/WQO.hs b/src/Language/REST/Internal/WQO.hs
--- a/src/Language/REST/Internal/WQO.hs
+++ b/src/Language/REST/Internal/WQO.hs
@@ -173,6 +173,8 @@
 type ECMap a = M.Map (EquivalenceClass a) (EquivalenceClass a)
 
 {-# SPECIALISE notStrongerThan :: WQO Op -> WQO Op -> Bool #-}
+-- |  @w1 `notStrongerThan` w2@ if it is possible to extend @w1@ with additional
+--    relations to obtain @w2@
 notStrongerThan :: forall a . (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
 notStrongerThan w1 w2 | w1 == w2 = True
 notStrongerThan (WQO ecs po) (WQO ecs' po') = result where
@@ -251,6 +253,9 @@
   | AlreadyImplied
   | Contradicts
 
+-- | @relevantTo wqo as bs@ returns a new WQO that contains only the necessary
+--   relations to relate elements from @as@ with elements in @bs@ as they are
+--   related in @wqo@.
 relevantTo :: (Ord a, Eq a, Hashable a) => WQO a -> S.Set a -> S.Set a -> WQO a
 relevantTo wqo0 as bs = go empty cartesianProduct where
 
diff --git a/src/Language/REST/Internal/WorkStrategy.hs b/src/Language/REST/Internal/WorkStrategy.hs
--- a/src/Language/REST/Internal/WorkStrategy.hs
+++ b/src/Language/REST/Internal/WorkStrategy.hs
@@ -1,21 +1,30 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-module Language.REST.Internal.WorkStrategy where
+module Language.REST.Internal.WorkStrategy (
+  GetWork,
+  WorkStrategy(..),
+  bfs,
+  notVisitedFirst) where
 
 import Language.REST.ExploredTerms as ET
 import Language.REST.Path
-import Language.REST.Internal.Rewrite
 
 import Data.Hashable
 import qualified Data.List as L
 
 type GetWork m rule term oc = [Path rule term oc] -> ExploredTerms term oc m -> (Path rule term oc, [Path rule term oc])
 
+-- | 'WorkStrategy' defines the procedure for choosing which pending path REST explores
 newtype WorkStrategy rule term oc = WorkStrategy (forall m . GetWork m rule term oc)
 
+-- | Explore the rewrite tree in BFS style. Using this strategy enables finding the
+--   shortest rewrite path to a desired term.
 bfs :: WorkStrategy rule term oc
 bfs = WorkStrategy bfs'
 
+-- | Prioritize searching for terms that haven't been seen before. This strategy may
+--   explore all reachable terms earlier, reducing the need to explore down the remaining
+--   unexplored paths.
 notVisitedFirst :: (Eq term, Eq rule, Eq oc, Hashable term) => WorkStrategy rule term oc
 notVisitedFirst = WorkStrategy notVisitedFirst'
 
@@ -28,12 +37,3 @@
   case L.find (\p -> not (ET.visited (runtimeTerm p) et)) paths of
     Just p  -> (p, L.delete p paths)
     Nothing -> (head paths, tail paths)
-
-commutesLast :: forall term oc . (Eq term, Eq oc, Hashable term) => WorkStrategy Rewrite term oc
-commutesLast = WorkStrategy go where
-  go paths et =
-    case L.find (\p -> not (ET.visited (runtimeTerm p) et || fromComm p)) paths of
-        Just p  -> (p, L.delete p paths)
-        Nothing -> (head paths, tail paths)
-  fromComm ([], _)    = False
-  fromComm (steps, _) = (getName . rule . last) steps == Just "mpComm"
diff --git a/src/Language/REST/KBO.hs b/src/Language/REST/KBO.hs
--- a/src/Language/REST/KBO.hs
+++ b/src/Language/REST/KBO.hs
@@ -25,6 +25,9 @@
   toConstraint (sym, n) = toSMT sym `smtGTE` (Const n)
 
 
+-- | @kboGTE t u@ returns the SMT expression describing constraints
+-- on the weights of function symbols such that @t@ is greater than @u@
+-- in the KBO ordering.
 kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool
 kboGTE t u = arityConstraints t `smtAnd` arityConstraints u `smtAnd` (size tOps `smtGTE` size uOps)
   where
@@ -32,6 +35,7 @@
     size ops     = smtAdd (map toSMT ops)
 
 
+-- | OCA for a quasi-order extension to the Knuth-Bendix ordering
 kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO
 kbo solver = OCAlgebra
   {  isSat           = checkSat' solver
diff --git a/src/Language/REST/LPO.hs b/src/Language/REST/LPO.hs
--- a/src/Language/REST/LPO.hs
+++ b/src/Language/REST/LPO.hs
@@ -82,8 +82,11 @@
       go ui = lpo' strict oc GT cs t ui
 
 
+-- | Constraint generator for a quasi-order extension to the Lexicographic path ordering
 lpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity
 lpo oc r cs t u = return $ lpo' False oc r cs t u
 
+-- | Constraint generator for a strict version of the quasi-order extension to
+--   the Lexicographic path ordering.
 lpoStrict :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity
 lpoStrict oc r cs t u = return $ lpo' True oc r cs t u
diff --git a/src/Language/REST/MetaTerm.hs b/src/Language/REST/MetaTerm.hs
--- a/src/Language/REST/MetaTerm.hs
+++ b/src/Language/REST/MetaTerm.hs
@@ -6,11 +6,11 @@
 import Data.String
 import Data.Hashable
 import GHC.Generics (Generic)
-import qualified Data.Set as S
 
 import Language.REST.Op
 import Language.REST.RuntimeTerm
 
+-- | A MetaTerm is a term with variables; used for 'Rewrite' rules
 data MetaTerm =
     Var String
   | RWApp Op [MetaTerm] deriving (Eq, Ord, Show, Generic, Hashable)
@@ -18,6 +18,7 @@
 instance IsString MetaTerm where
   fromString = Var
 
+-- | Helper class, enabling conversion of 'RuntimeTerm's to 'MetaTerm's
 class ToMetaTerm a where
   toMetaTerm :: a -> MetaTerm
 
@@ -26,9 +27,3 @@
 
 instance ToMetaTerm RuntimeTerm where
   toMetaTerm (App f xs) = RWApp f (map toMetaTerm xs)
-
-termOps :: ToMetaTerm a => a -> S.Set Op
-termOps = go . toMetaTerm where
-  go :: MetaTerm -> S.Set Op
-  go (Var _)         = S.empty
-  go (RWApp op trms) = S.insert op (S.unions (map go trms))
diff --git a/src/Language/REST/OCAlgebra.hs b/src/Language/REST/OCAlgebra.hs
--- a/src/Language/REST/OCAlgebra.hs
+++ b/src/Language/REST/OCAlgebra.hs
@@ -2,18 +2,22 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 module Language.REST.OCAlgebra where
 
+-- | The "Ordering Constraint Algebra", as described in section 4.2 of the paper.
+--  @OCAlgebra c a m@ is an OCA with language of constraints @c@, applied to terms
+--  of type @a@. @m@ is the computation context for @isSat@.
 data OCAlgebra c a m = OCAlgebra
-  {
-    isSat  :: c -> m Bool
-  , refine :: c -> a -> a -> c
-  , top    :: c
+  { isSat  :: c -> m Bool       -- ^ Checks if the constraints are satisfiable
+  , refine :: c -> a -> a -> c  -- ^ @refine c t u@ strengthens @c@ to permit @t >= u@
+  , top    :: c                 -- ^ Initial constraints for use in REST
 
-  -- For explore optimizations, if not required just make it return 2nd param
-  , union  :: c -> c -> c
-  -- If not required return False
-  , notStrongerThan :: c -> c -> m Bool
+  , union  :: c -> c -> c       -- ^ Computes the union of constraints; used in 'ExploredTerms' as an optimization
+                                --   A safe default implementation is @union c1 c2 = c2@
+
+  , notStrongerThan :: c -> c -> m Bool -- ^ @c1 `notStrongerThan c2@ if @c1@ permits all orderings allowed by @c2@
+                                        -- A safe default implementation is @notStrongerThan _ _ = return false@
   }
 
+-- | @fuelOC n@ is an OCA that permits @n@ rewrite steps
 fuelOC :: (Monad m) => Int -> OCAlgebra Int a m
 fuelOC initFuel = OCAlgebra isSat' refine' initFuel union' notStrongerThan'
   where
@@ -22,30 +26,34 @@
     union'  c c'          = max c c'
     notStrongerThan' c c' = return $ c >= c'
 
+-- | @contramap f oca@ transforms an OCA of terms of type @a@ terms of type @b@,
+--   by using @f@ to convert terms of @b@ to equivalent ones of @a@
 contramap :: forall c a b m .
      (b -> a)
   -> OCAlgebra c a m
   -> OCAlgebra c b m
-contramap f aoc = aoc{refine = refine'}
+contramap f oca = oca{refine = refine'}
   where
     refine' :: c -> b -> b -> c
-    refine' c t1 t2 = refine aoc c (f t1) (f t2)
+    refine' c t1 t2 = refine oca c (f t1) (f t2)
 
+-- | @bimapConstraints to from oca@ yields an oca using @d@ to track constraints; @to@ and @from@ should
+--   define an isomorphism between c and d
 bimapConstraints :: forall c d a m .
      (c -> d)
   -> (d -> c)
   -> OCAlgebra c a m
   -> OCAlgebra d a m
-bimapConstraints to from aoc = OCAlgebra isSat' refine' (to (top aoc)) union' notStrongerThan'
+bimapConstraints to from oca = OCAlgebra isSat' refine' (to (top oca)) union' notStrongerThan'
   where
     isSat' :: d -> m Bool
-    isSat' c = isSat aoc (from c)
+    isSat' c = isSat oca (from c)
 
     refine' :: d -> a -> a -> d
-    refine' c t1 t2 = to $ refine aoc (from c) t1 t2
+    refine' c t1 t2 = to $ refine oca (from c) t1 t2
 
     union' :: d -> d -> d
-    union' c1 c2 = to $ union aoc (from c1) (from c2)
+    union' c1 c2 = to $ union oca (from c1) (from c2)
 
     notStrongerThan' :: d -> d -> m Bool
-    notStrongerThan' c1 c2 = notStrongerThan aoc (from c1) (from c2)
+    notStrongerThan' c1 c2 = notStrongerThan oca (from c1) (from c2)
diff --git a/src/Language/REST/OCToAbstract.hs b/src/Language/REST/OCToAbstract.hs
--- a/src/Language/REST/OCToAbstract.hs
+++ b/src/Language/REST/OCToAbstract.hs
@@ -15,9 +15,9 @@
 import Language.REST.Types
 import Language.REST.SMT (ToSMTVar)
 
-showHash :: Show a => a -> String
-showHash = show . hash . show
-
+-- | @lift@ takes a representation of constraints on a WQO over @base@,
+--   alongside a function used to generate constraints to permit a relation on terms @lifted@,
+--   and returns the corresponding Ordering Constraints Algebra
 lift :: forall impl base lifted m . (ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted, Show base, Show (impl base)) =>
      OC.WQOConstraints impl m
   -> OC.ConstraintGen impl base lifted Identity
diff --git a/src/Language/REST/Op.hs b/src/Language/REST/Op.hs
--- a/src/Language/REST/Op.hs
+++ b/src/Language/REST/Op.hs
@@ -11,6 +11,7 @@
 import GHC.Generics (Generic)
 import Language.REST.SMT
 
+-- | The operators used in 'RuntimeTerm' and 'MetaTerm'
 newtype Op = Op Text deriving (Eq, Ord, Hashable, Generic)
 
 instance Show Op where
diff --git a/src/Language/REST/Path.hs b/src/Language/REST/Path.hs
--- a/src/Language/REST/Path.hs
+++ b/src/Language/REST/Path.hs
@@ -8,25 +8,33 @@
 import GHC.Generics (Generic)
 import Data.Hashable
 
+-- | @Step@ represents an intermediate step in a 'Path' explored by REST
 data Step rule term a = Step {
-    term     :: PathTerm rule term
-  , rule     :: rule
-  , ordering :: a
-  , fromPLE  :: Bool
+    term     :: PathTerm rule term -- ^ The "from" term in this path
+  , rule     :: rule               -- ^ The rule generating the next term
+  , ordering :: a                  -- ^ The generated constraints from applying the rule
+  , fromPLE  :: Bool               -- ^ Whether the term was derived from a provably terminating eval function
 } deriving (Eq, Ord, Generic, Hashable)
 
 
+-- | @PathTerm@ is the term explored at a path
 data PathTerm rule term = PathTerm
     {  pathTerm :: term
+    ,  rejected :: S.HashSet (term, rule) -- ^ The orderings FROM pathTerm that were rejected.
+                                          -- TODO: This should be removed, as it's really only used
+                                          --       in the visualization
 
-       -- The orderings FROM pathTerm that were rejected
-    ,  rejected :: S.HashSet (term, rule)
     } deriving (Eq, Ord, Generic, Hashable)
 
+-- | A path explored by REST.
+-- The head of the 1st part of the tuple is the initial term.
+-- The 2nd part of the tuple is the last term.
 type Path rule term a = ([Step rule term a], PathTerm rule term)
 
+-- | Extracts the list of terms from the path
 pathTerms :: Path rule term a -> [term]
 pathTerms (xs, x) = map pathTerm $ map term xs ++ [x]
 
+-- | Extracts the last (most recently generated) term
 runtimeTerm :: Path rule term a -> term
 runtimeTerm (_, pt) = pathTerm pt
diff --git a/src/Language/REST/RESTDot.hs b/src/Language/REST/RESTDot.hs
--- a/src/Language/REST/RESTDot.hs
+++ b/src/Language/REST/RESTDot.hs
@@ -1,8 +1,15 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-module Language.REST.RESTDot where
 
+-- | This module is responsible for rendering GraphViz graphs corresponding to an
+--   execution of the REST algorithm.
+module Language.REST.RESTDot (
+    PrettyPrinter(..)
+  , ShowRejectsOpt(..)
+  , writeDot
+  ) where
+
 import Data.List
 import Data.Hashable
 import qualified Data.Set as S
@@ -11,10 +18,14 @@
 import Language.REST.Dot
 import Language.REST.Path
 
+-- | Controls how rejected paths should be visualized
 data ShowRejectsOpt =
-  ShowRejectsWithRule | ShowRejectsWithoutRule | HideRejects
+    ShowRejectsWithRule     -- ^ Display rejected paths, and the rule that generated them
+  | ShowRejectsWithoutRule  -- ^ Display rejected paths, but don't display the rule that generated them
+  | HideRejects             -- ^ Do not show rejected paths
   deriving Eq
 
+-- | Controls how rules, terms, orderings, and rejected paths should be displayed
 data PrettyPrinter rule term ord = PrettyPrinter
   { printRule    :: rule -> String
   , printTerm    :: term -> String
@@ -102,6 +113,7 @@
       unions :: (Ord a, Eq a, Hashable a) => S.Set (S.Set a) -> S.Set a
       unions = S.unions . S.toList
 
+-- | @writeDot name gt printer paths@ generates a graphViz graph from @paths@ with name @name@.
 writeDot :: (Hashable rule, Hashable term, Ord a, Hashable a) =>
   String -> GraphType -> PrettyPrinter rule term a -> S.Set (Path rule term a) -> IO ()
 writeDot name gt printer paths = mkGraph name (toGraph gt printer paths)
diff --git a/src/Language/REST/RPO.hs b/src/Language/REST/RPO.hs
--- a/src/Language/REST/RPO.hs
+++ b/src/Language/REST/RPO.hs
@@ -6,7 +6,9 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ImplicitParams #-}
 
-module Language.REST.RPO (rpo, rpoTerm, rpoGTE, rpoGTE', synGTE) where
+-- | This module contains the implementation of the Recursive Path Quasi-Ordering,
+--   defined in section 4.2.1 of the REST paper
+module Language.REST.RPO (rpo, rpoGTE, synGTE) where
 
 import Prelude hiding (EQ, GT)
 
@@ -75,6 +77,8 @@
       modify (\st -> st{ rpoCache = M.insert key result (rpoCache st)})
       return result
 
+-- | The constraint generator for RPQO. That is, given terms @t@, @u@, @rpo@ generates
+--   the constraints on n RPQO ≥ᵣ such that t ≥ᵣ u.
 rpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RT.RuntimeTerm Identity
 rpo = runStateConstraints (cmapConstraints rpoTerm rpo') (RPOState M.empty 0)
 
@@ -102,6 +106,8 @@
         , rpoMul oc GTE cs'                             ts               (MS.singleton u)
         ]
 
+-- | @rpoGTE impl t u@ generates the constraints a WQO over 'Op' (via @impl@) that ensures
+--   that t ≥ᵣ u in the result RPQO ≥ᵣ.
 rpoGTE
   :: (?impl::WQOConstraints oc m, Hashable (oc Op), Eq (oc Op), Show (oc Op))
   => RT.RuntimeTerm
@@ -124,6 +130,8 @@
 synEQ :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
 synEQ o l r = synGTE' o l r && synGTE' o r l
 
+-- | Performs the (concrete) RPQO calculation. @synGTE o t u@ returns
+--   true iff t ≥ᵣ u using an RPQO with precedence @o@.
 synGTE :: OpOrdering -> RT.RuntimeTerm -> RT.RuntimeTerm -> Bool
 synGTE o t u = synGTE' o (rpoTerm t) (rpoTerm u)
 
diff --git a/src/Language/REST/Rest.hs b/src/Language/REST/Rest.hs
--- a/src/Language/REST/Rest.hs
+++ b/src/Language/REST/Rest.hs
@@ -6,18 +6,20 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# OPTIONS_GHC -Wno-error=deprecations #-}
 
+-- | This module contains the core REST algorithm
 module Language.REST.Rest (
     rest
   , pathsResult
   , termsResult
-  , terms
   , PathsResult(..)
+  , TermsResult
   , WorkStrategy(..)
   , RESTParams(..)
+  , RESTResult(..)
   ) where
 
 import           Control.Monad
-import           Control.Monad.List
+import           Control.Monad.Trans
 import Data.Hashable
 import qualified Data.HashSet as S
 import qualified Data.List    as L
@@ -28,30 +30,40 @@
 import Language.REST.RewriteRule
 import Language.REST.Path
 import Language.REST.ExploredTerms as ET
+import Language.REST.Internal.ListT
 import Language.REST.Internal.WorkStrategy
 
+-- | The set of all 'Path's explored by REST.
 newtype PathsResult rule term oc = PathsResult (S.HashSet (Path rule term oc))
 
+-- | The set of all terms explored by REST.
 newtype TermsResult rule term oc = TermsResult (S.HashSet term)
 
+-- | An initial (empty) instance of 'PathsResult'
 pathsResult :: PathsResult rule term oc
 pathsResult = PathsResult S.empty
 
+-- | An initial (empty) instance of 'TermsResult'
 termsResult :: TermsResult rule term oc
 termsResult = TermsResult S.empty
 
+--  | This class encapsulates the mechanism for REST to store the result of its computation.
+-- For example, we include two instances: 'PathsResult', which stores each 'Path' generated
+-- by REST (useful for debugging and visualization); and 'TermsResult', which only stores the
+-- resulting terms (which uses less memory and is likely more performant).
 class RESTResult a where
+  -- | Includes a term in the result
   includeInResult :: (Hashable oc, Eq oc, Hashable rule, Eq rule, Hashable term, Eq term) => Path rule term oc -> a rule term oc -> a rule term oc
-  terms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term
+  -- | Obtains the terms explored by REST
+  resultTerms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term
 
 instance RESTResult PathsResult where
   includeInResult p (PathsResult s) = PathsResult (S.insert p s)
-  terms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s)
-
+  resultTerms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s)
 
 instance RESTResult TermsResult where
   includeInResult p (TermsResult s) = TermsResult (S.union s (S.fromList $ pathTerms p))
-  terms (TermsResult s)             = s
+  resultTerms (TermsResult s)       = s
 
 
 data RESTState m rule term oc et rtype = RESTState
@@ -71,6 +83,7 @@
   , etStrategy   :: ExploreStrategy
   }
 
+-- @rest params terms@ performs the REST search from initial term @term@ with parameters@params@.
 rest :: forall m rule term oc rtype .
   ( MonadIO m
   , RewriteRule m rule term
diff --git a/src/Language/REST/RewriteRule.hs b/src/Language/REST/RewriteRule.hs
--- a/src/Language/REST/RewriteRule.hs
+++ b/src/Language/REST/RewriteRule.hs
@@ -4,5 +4,10 @@
 
 import qualified Data.HashSet as S
 
+-- | A class for datatypes that can be used as rewrite rules
 class RewriteRule m rule term where
+  -- | @apply term rule@ returns the set of resulting terms that can be generated
+  --   from @term@ using @rule@. Multiple terms are possible if the rule applies to
+  --   multiple subterms. The result is embedded in a computation context @m@;
+  --   this enables support for SMT-based conditional rewriting, for example.
   apply :: term -> rule -> m (S.HashSet term)
diff --git a/src/Language/REST/RuntimeTerm.hs b/src/Language/REST/RuntimeTerm.hs
--- a/src/Language/REST/RuntimeTerm.hs
+++ b/src/Language/REST/RuntimeTerm.hs
@@ -1,7 +1,13 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
 
-module Language.REST.RuntimeTerm where
+module Language.REST.RuntimeTerm
+  ( RuntimeTerm(..)
+  , ToRuntimeTerm(..)
+  , subTerms
+  , contains
+  )
+where
 
 import           Data.Hashable
 import           GHC.Generics (Generic)
@@ -10,12 +16,14 @@
 
 import           Language.REST.Op
 
+-- | Ground terms
 data RuntimeTerm = App Op [RuntimeTerm] deriving (Eq, Ord, Generic, Hashable)
 
 instance Show RuntimeTerm where
   show (App op []) = show op
   show (App op ts) = printf "%s(%s)" (show op) $ L.intercalate ", " (map show ts)
 
+-- | Transformable to a ground term
 class ToRuntimeTerm a where
   toRuntimeTerm :: a -> RuntimeTerm
 
@@ -25,6 +33,11 @@
 instance ToRuntimeTerm RuntimeTerm where
   toRuntimeTerm = id
 
+-- | @subTerms t@ returns a list of pairs @(s, f)@, where @s@ is a subterm of @t@,
+-- and @f@ is a function that takes a replacement @s'@ for @s@, and generates a new
+-- term where @s@ is replaced with @s'@ in @t@. Also includes the pair (t, id),
+-- representing the term itself.
+-- TODO: Consider more efficient implementations
 subTerms :: RuntimeTerm -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]
 subTerms t@(App f ts) = (t, id) : concatMap st [0..length ts - 1]
   where
@@ -37,3 +50,9 @@
         go2 (srt, toFull) = (srt, go . toFull)
       in
         map go2 (subTerms ti)
+
+
+-- | @t `contains` u@ iff @t == u@ or @u@ is a subterm of @t@
+contains :: RuntimeTerm -> RuntimeTerm -> Bool
+contains t1 t2 | t1 == t2 = True
+contains (App _ ts) t     = any (contains t) ts
diff --git a/src/Language/REST/SMT.hs b/src/Language/REST/SMT.hs
--- a/src/Language/REST/SMT.hs
+++ b/src/Language/REST/SMT.hs
@@ -12,7 +12,29 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module Language.REST.SMT where
+-- | This module contains functionality for creating SMTLIB expressions and interacting
+--   with an SMT solver.
+module Language.REST.SMT
+  (
+    checkSat
+  , checkSat'
+  , getModel
+  , parseModel
+  , killZ3
+  , spawnZ3
+  , smtAdd
+  , smtAnd
+  , smtFalse
+  , smtGTE
+  , smtTrue
+  , withZ3
+  , SolverHandle
+  , SMTExpr(..)
+  , SMTVar(..)
+  , ToSMT(..)
+  , ToSMTVar(..)
+  , Z3Model
+) where
 
 import Control.Monad.IO.Class
 import Data.Hashable
@@ -27,6 +49,8 @@
 import GHC.Generics (Generic)
 import GHC.IO.Handle
 
+-- | A model returned by Z3 corresponding to a satisfiable
+--   set of constraints. Untyped.
 type Z3Model = M.Map String String
 
 parens :: Text.Parsec.Prim.Stream s m Char => ParsecT s u m a -> ParsecT s u m a
@@ -54,23 +78,16 @@
   defs <- endBy parseFunDef spaces
   return $ M.fromList defs
 
-readModel :: Handle -> IO String
-readModel handle = go "" where
-  closedTerm t = length (filter (== '(') t) == length (filter (== ')') t)
-  go buf = do
-    line <- hGetLine handle
-    let buf' = buf ++ line ++ "\n"
-    if closedTerm buf'
-    then return buf'
-    else go buf'
-
+-- | Parses Z3's model string into a 'Z3Model'.
 parseModel :: String -> Z3Model
 parseModel str = case parse modelParser "" str of
   Left err -> error (show err)
   Right t  -> t
 
+-- | An SMT variable
 newtype SMTVar a = SMTVar T.Text deriving (Eq, Ord)
 
+-- | SMTLib expressions
 data SMTExpr a where
     And     :: [SMTExpr Bool] -> SMTExpr Bool
     Add     :: [SMTExpr Int]  -> SMTExpr Int
@@ -153,16 +170,20 @@
 smtTrue :: SMTExpr Bool
 smtTrue  = And []
 
+-- | Returns an SMT expression that adds all elements in the list. If the list is empty,
+--   returns @Const 0@.
 smtAdd :: [SMTExpr Int] -> SMTExpr Int
 smtAdd [] = Const 0
 smtAdd ts = Add ts
 
+-- | `smtAnd t u` returns an smt expression representing \( t \land u \).
 smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
 smtAnd (And xs) (And ys) = And $ L.nub (xs ++ ys)
 smtAnd (And xs) e        = And $ L.nub (xs ++ [e])
 smtAnd e        (And ys) = And $ L.nub (e:ys)
 smtAnd t        u        = And [t, u]
 
+-- | `smtGTE t u` returns an SMT expression \( t \geqslant u \). If @t == u@, returns 'smtTrue'.
 smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
 smtGTE t u | t == u    = smtTrue
 smtGTE t u | otherwise = GTE t u
@@ -195,17 +216,22 @@
 askCmds expr = varDecls ++ [SMTAssert expr, CheckSat] where
   varDecls = map DeclareVar $ S.toList (vars expr)
 
+-- | The handle (stdIn, stdOut) used for interacting with Z3
 type SolverHandle = (Handle, Handle)
 
-spawnZ3 :: IO (Handle, Handle)
+-- | Instantiates a Z3 instance, returning the solver handle for interaction
+spawnZ3 :: IO SolverHandle
 spawnZ3 = do
   (Just stdIn, Just stdOut, _, _) <- createProcess (proc "z3" ["-in"]) {std_in = CreatePipe, std_out = CreatePipe}
   return (stdIn, stdOut)
 
-killZ3 :: (Handle, b) -> IO ()
+-- | Kills the Z3 instance by closing the standard input stream
+killZ3 :: SolverHandle -> IO ()
 killZ3 (stdIn, _) = hClose stdIn
 
-withZ3 :: MonadIO m => ((Handle, Handle) -> m b) -> m b
+-- | @withZ3 f@ instantiates a Z3 instance, runs @f@ with that instance,
+--   and then closes the instance and returns the result
+withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b
 withZ3 f =
   do
     z3     <- liftIO $ spawnZ3
@@ -213,11 +239,14 @@
     liftIO $ killZ3 z3
     return result
 
+-- | @getModel@ instructs an instantiated SMT solver to produce its model.
 getModel :: Handle -> IO ()
 getModel stdIn = do
   hPutStr stdIn "(get-model)\n"
   hFlush stdIn
 
+-- | @checkSat' handles expr@ checks satisfiability of @expr@ in an instantiated SMT solver.
+--   This is wrapped in a @push@ / @pop@, so it does not change the SMT environment
 checkSat' :: (Handle,  Handle) -> SMTExpr Bool -> IO Bool
 checkSat' (stdIn, stdOut) expr = do
   sendCommands $ Push:askCmds expr
@@ -237,6 +266,8 @@
       hPutStr stdIn $ (T.unpack (T.intercalate "\n" (map commandString cmds))) ++ "\n"
       hFlush stdIn
 
+-- | @checkSat expr@ launches Z3, to checks satisfiability of @expr@, terminating Z3
+--   afterwards. Just a utility wrapper for `checkSat'`
 checkSat :: SMTExpr Bool -> IO Bool
 checkSat expr = do
   z3     <- spawnZ3
@@ -244,9 +275,14 @@
   killZ3 z3
   return result
 
+-- | This class allows elements of type @a@ to be used as SMT /vaiables/ of type @b@.
+--   For example, the instance @ToSMTVar Op Int@ allows 'RuntimeTerm' operators to be
+--   represented as 'Int' variables.
 class ToSMTVar a b | a -> b where
   toSMTVar :: a -> SMTVar b
 
+-- | This class allows elements of type @a@ to be used as SMT expressions of type
+--   @b@
 class ToSMT a b where
   toSMT :: a -> SMTExpr b
 
diff --git a/src/Language/REST/Types.hs b/src/Language/REST/Types.hs
--- a/src/Language/REST/Types.hs
+++ b/src/Language/REST/Types.hs
@@ -28,9 +28,20 @@
 import           Language.REST.Op
 import           Language.REST.MetaTerm as MT
 
+-- | Arguments used for pretty-printing terms
 data PPArgs = PPArgs
-  { ppReplace  :: [(T.Text, T.Text)]
+  {
+    -- | A list of pairs @(search, rep)@. If any operator starts with @search@
+    --   for some element in the list, during the printing the operator is
+    --   printed with the corresponding @rep@ in place of @search@.
+    ppReplace  :: [(T.Text, T.Text)]
+
+    -- | A list of pairs @(search, rep)@. If any operator matches @search@, then it's
+    --   corresponding term is printed in infix style with operator @rep@.
   , ppInfixOps :: [(T.Text, T.Text)]
+
+    -- | Used to override printing for some terms. When @ppCustom m = Just s@, then @m@
+    --   be printed as @s@.
   , ppCustom   :: MetaTerm -> Maybe T.Text
   }
 
diff --git a/src/Language/REST/WQOConstraints.hs b/src/Language/REST/WQOConstraints.hs
--- a/src/Language/REST/WQOConstraints.hs
+++ b/src/Language/REST/WQOConstraints.hs
@@ -1,13 +1,14 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE FlexibleContexts #-}
+
+-- | This module includes a typeclass for implementations of constraints on 'WQO's
 module Language.REST.WQOConstraints
   (
     WQOConstraints(..)
   , ConstraintGen
   , liftC
   , cmapConstraints
-  , numOrderings
   , isUnsatisfiable
   , intersectAll
   , unionAll
@@ -20,7 +21,6 @@
 import Control.Monad.State.Strict
 import qualified Data.List as L
 import Data.Hashable
-import qualified Data.Set as S
 
 import Prelude hiding (GT, EQ)
 
@@ -30,45 +30,63 @@
 
 type WQO = WQO.WQO
 
-trace' :: String -> a -> a
-trace' _ x = x
-
+-- | @WQOConstraints impl m@ defines an implementation for tracking and checking
+--   satisfiability of constraints on arbitrary type @a@. Namely, instances of
+--   @impl a@ are used to keep track of constraints. Satisfiability checking and
+--   other computations are embedded in a computational context @m@.
 data WQOConstraints impl m = OC
-  { addConstraint       :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
+  {
+    -- | @addConstraint wqo c@ adds constraints to @c@ to also permit the WQO @w@.
+    addConstraint       :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
+
+    -- | @intersect c1 c2@ returns constraints to permit only WQOs permitted by both @c1@ and
+    --   @c2@. Therefore the resulting constraints are stronger (less likely to be
+    --   satisifiable).
   , intersect           :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
+    -- | @isSatisfiable c@ returns true iff @c@ permits any WQO
   , isSatisfiable       :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool
+
+    -- | @c1 `notStrongerThan` c2@ iff any ordering permitted by @c1@ is also permitted
+    --   by @c2@
   , notStrongerThan     :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool
+    -- | @noConstraints@ returns an instance of constraints that permits any WQO
   , noConstraints       :: forall a. (Eq a, Ord a, Hashable a) => impl a
+
   , permits             :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool
-  , relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a -> S.Set a -> impl a
+    -- | @c1 `union` c2@ returns constraints that permit WQOs permitted by /either/
+    --  @c1@ or @c2@. The resulting constraints are therefore weaker (more likely to
+    --  be satisfiable)
   , union               :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
+
+    -- | @unsatisfiable@ returns an instance of constraints that does not permit any WQO
   , unsatisfiable       :: forall a. impl a
-  , elems               :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a
+
+    -- | @getOrdering c@ returns a concrete ordering satisfying the constraints, if one exists
   , getOrdering         :: forall a. impl a -> Maybe (WQO a)
-  , simplify            :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a
   }
 
-numOrderings :: (Show a, Ord a, Eq a, Ord a, Hashable a) => S.Set a -> WQOConstraints oc m -> oc a -> Int
-numOrderings elems impl oc = S.size $ S.filter (permits impl oc) (WQO.orderings elems)
-
+-- | Returns true iff the constraints do not permit any WQO.
 isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool
 isUnsatisfiable OC{isSatisfiable} c = not <$> isSatisfiable c
 
+-- | Returns the constraints that permit a given WQO
 singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a
 singleton OC{addConstraint, noConstraints} c = addConstraint c noConstraints
 
+-- | Given a list of constraints @ocs@, returns constraints that permit only the WQOs
+--   permitted by each @oc@ in @ocs@
 intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
 intersectAll OC{noConstraints} []     = noConstraints
-intersectAll OC{intersect}     (x:xs) = L.foldl' go x xs
-  where
-    go t1 t2 = trace' ("Intersect " ++ (show t1)) $ intersect t1 t2
+intersectAll OC{intersect}     (x:xs) = L.foldl' intersect x xs
 
+-- | Given a list of constraints @ocs@, returns constraints that permit the WQOs
+--   permitted by any @oc@ in @ocs@
 unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
 unionAll OC{unsatisfiable} []     = unsatisfiable
-unionAll OC{union}         (x:xs) = L.foldl' go x xs
-  where
-    go t1 t2 = trace' ("Union " ++ (show t1)) $ union t1 t2
+unionAll OC{union}         (x:xs) = L.foldl' union x xs
 
+-- | @intersectRelation oc impl (f, g, r)@ strengthens constraints represented by @impl@
+--   to also ensure that @f@ and @g@ are related via relation @r@ in permitted WQOs.
 intersectRelation ::
   (Ord a, Eq a, Ord a, Hashable a, Show a) =>
   WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a
@@ -84,21 +102,21 @@
       wqo2 <- WQO.singleton (f, g, WQO.QEQ)
       return $ union oc (singleton oc wqo1) (singleton oc wqo2)
 
-
-
--- ConstraintGen impl R >= t u returns the constraints on >= that guarantee
+-- | ConstraintGen impl R >= t u returns the constraints on >= that guarantee
 -- the resulting relation >=', we have:
 --   1. x >= y implies x >=' y
 --   2. t lift(R(>=')) u
 -- Where R generates { == , >=, > } from the underlying ordering
 -- R is used to enable optimizations
-
 type ConstraintGen oc base lifted m =
   forall m' . (WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base))
 
+-- | @cmapConstraints@ takes a transformation @f@ from @lifted' to lifted@, and transforms
+-- a constraint generator on terms of types @lifted@ into one on terms of types @lifted'@
 cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m
 cmapConstraints f cgen impl r oc t u = cgen impl r oc (f t) (f u)
 
+-- | @liftc f imp@ lifts the computations of @imp@ from context @m@ to context @m'@
 liftC :: (m Bool  -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m'
 liftC f oc = oc{
     isSatisfiable   = isSatisfiable'
@@ -108,5 +126,7 @@
     isSatisfiable'   c1    = f (isSatisfiable oc c1)
     notStrongerThan' c1 c2 = f (notStrongerThan oc c1 c2)
 
+-- @runStateConstriants initState cgen@ transforms a constraint generator in the 'State'
+-- monad to one in the 'Identity' monad by using initial state @initState@'
 runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity
 runStateConstraints cgen initState impl r oc t u = Identity $ evalState (cgen impl r oc t u) initState
diff --git a/src/Language/REST/WQOConstraints/ADT.hs b/src/Language/REST/WQOConstraints/ADT.hs
--- a/src/Language/REST/WQOConstraints/ADT.hs
+++ b/src/Language/REST/WQOConstraints/ADT.hs
@@ -7,11 +7,17 @@
 
 #define OPTIMIZE_WQO
 
-module Language.REST.WQOConstraints.ADT where
+module Language.REST.WQOConstraints.ADT
+  (  ConstraintsADT(..)
+  , addConstraint
+  , adtOC
+  , intersect
+  , union
+  )
+where
 
 import GHC.Generics (Generic)
 
-import Debug.Trace
 import Data.Hashable
 import Control.Monad.State.Lazy
 import qualified Data.Set as S
@@ -26,10 +32,14 @@
 
 type WQO = WQO.WQO
 
+-- | Represents constraints over a WQO on @a@
 data ConstraintsADT a =
+ -- | @Sat wqo@ represents satisfiable constraints: those that permit each relation in @wqo@.
     Sat (WQO a)
   | Unsat
+    -- | @Union c1 c2@ permits orderings of P1 and orderings of P2
   | Union (ConstraintsADT a) (ConstraintsADT a)
+    -- | @Intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2
   | Intersect (ConstraintsADT a) (ConstraintsADT a)
   deriving (Eq, Ord, Generic, Hashable)
 
@@ -46,16 +56,7 @@
 cost (Sat wqo)           = S.size $ WQO.elems wqo
 cost Unsat               = 100
 
-minDepth :: ConstraintsADT a -> Int
-minDepth (Union lhs rhs)     = 1 + min (minDepth lhs) (minDepth rhs)
-minDepth (Intersect lhs rhs) = 1 + min (minDepth lhs) (minDepth rhs)
-minDepth _                   = 1
-
-maxDepth :: ConstraintsADT a -> Int
-maxDepth (Union lhs rhs)     = 1 + max (maxDepth lhs) (maxDepth rhs)
-maxDepth (Intersect lhs rhs) = 1 + max (maxDepth lhs) (maxDepth rhs)
-maxDepth _                   = 1
-
+-- | @intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2
 intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
 
 #ifdef OPTIMIZE_WQO
@@ -92,6 +93,7 @@
 #endif
 intersect t1 t2            = Intersect t1 t2
 
+-- | @union c1 c2@ permits orderings of P1 and orderings of P2
 union :: Eq a => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
 union (Sat w) _            | w == WQO.empty = Sat w
 union _            (Sat w) | w == WQO.empty = Sat w
@@ -103,14 +105,11 @@
 union c1 c2 | c1 == c2 = c1
 union c1 c2            = Union c1 c2
 
+-- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@
 addConstraint
  :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a
 addConstraint o c = intersect (Sat o) c
 
-relevantConstraints
-  :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> S.Set a -> S.Set a -> ConstraintsADT a
-relevantConstraints c _ _ = c
-
 notStrongerThan
   :: (Eq a, ToSMTVar a Int)
   => ConstraintsADT a
@@ -126,9 +125,6 @@
 unsatisfiable :: ConstraintsADT a
 unsatisfiable = Unsat
 
-trace' :: String -> a -> a
-trace' = trace
-
 {-# SPECIALIZE getConstraints :: ConstraintsADT Op -> [WQO Op] #-}
 getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a]
 getConstraints adt = -- trace' ("Get constraints, size : " ++ (show $ dnfSize adt)) $
@@ -199,28 +195,6 @@
         then (lhs, rhs)
         else (rhs, lhs)
 
-dnfSize :: ConstraintsADT a -> Int
-dnfSize (Sat _w)       = 1
-dnfSize Unsat         = 0
-dnfSize (Union w1 w2) = dnfSize w1 + dnfSize w2
-dnfSize (Intersect w1 w2) = dnfSize w1 * dnfSize w2
-
--- toDNF (Union lhs rhs) = S.union (toDNF lhs) (toDNF rhs)
--- toDNF (Intersect lhs rhs) =
---   let
---     ldnf = toDNF lhs
---     rdnf = toDNF rhs
---   in
---     S.unions
-
-simplify :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a
-simplify _adt = undefined
--- simplify adt = case getConstraints adt of
---   []     -> Unsat
---   (x:xs) -> foldl go (Sat x) xs
---   where
---     go a x = Union (Sat x) a
-
 permits
   :: (Ord a, Hashable a, Show a)
   => ConstraintsADT a
@@ -230,23 +204,14 @@
 
 isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool
 isSatisfiable s = toSMT s
-  -- trace (show (minDepth s) ++ " " ++ show (maxDepth s)) $ not $ null $ getConstraints s
 
 instance (Eq a, Hashable a,  Show a) => Show (ConstraintsADT a) where
-  -- show s = go 0 s where
-  --   go n (Sat w)         = indent n $ show w
-  --   go n Unsat           = indent n $ "⊥"
-  --   go n (Union w t )    = indent n $ printf "∪\n%s\n%s" (go (n+1) w) (go (n+1) t)
-  --   go n (Intersect w t) = indent n $ printf "∩\n%s\n%s" (go (n+1) w) (go (n+1) t)
-
-  --   indent 0 s = s
-  --   indent n s = take (n - 1) (repeat '|') ++ '+':s
-
   show (Sat w)         = show w
   show Unsat           = "⊥"
   show (Union w t )    = printf "(%s ∨\n %s)" (show w) (show t)
   show (Intersect w t) = printf "(%s ∧ %s)" (show w) (show t)
 
+-- | See 'ConstraintsADT'
 adtOC :: (Handle, Handle) -> OC.WQOConstraints ConstraintsADT IO
 adtOC z3 = OC.liftC (checkSat' z3) adtOC'
 
@@ -258,9 +223,6 @@
   notStrongerThan
   noConstraints
   permits
-  relevantConstraints
   union
   unsatisfiable
   undefined
-  undefined
-  simplify
diff --git a/src/Language/REST/WQOConstraints/Lazy.hs b/src/Language/REST/WQOConstraints/Lazy.hs
--- a/src/Language/REST/WQOConstraints/Lazy.hs
+++ b/src/Language/REST/WQOConstraints/Lazy.hs
@@ -3,22 +3,20 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
+-- | This module defines "Lazy" constraints on a WQO; the intention is that
+--   computations on this type do only the necessary amount of work to determine
+--   satisfiability (deferring further computations in a thunk).
 module Language.REST.WQOConstraints.Lazy (
       lazyOC
     , addConstraint
-    , intersect
     , isSatisfiable
     , noConstraints
-    , singleton
-    , union
-    , unsatisfiable
     , LazyOC
     ) where
 
 import Text.Printf
 import GHC.Generics (Generic)
 import Data.Hashable
-import qualified Data.Set as S
 
 import qualified Language.REST.Internal.WQO as WQO
 import qualified Language.REST.WQOConstraints as OC
@@ -31,8 +29,11 @@
 
 type Thunk a = ADT.ConstraintsADT a
 
+-- | Implementation of "Lazy" ordering constraints.
 data LazyOC a =
     Unsat
+    -- @Sat wqo thunk@ represent satisfiable constraints; @wqo@ is a candidate.
+    -- @Thunk@ represents the other satisfiable constraints, if any.
   | Sat (WQO a) (Thunk a)
   deriving (Eq, Ord, Generic, Hashable)
 
@@ -44,14 +45,9 @@
 eval (ADT.Sat w)   = Sat w ADT.Unsat
 eval ADT.Unsat     = Unsat
 eval (ADT.Union lhs rhs) =
-  case eval t1 of
-    Sat w t1' -> Sat w (ADT.union t1' t2)
-    Unsat     -> eval t2
-  where
-    (t1, t2) = (lhs, rhs)
-      -- if ADT.minDepth lhs < ADT.minDepth rhs
-      -- then (lhs, rhs)
-      -- else (rhs, lhs)
+  case eval lhs of
+    Sat w t1' -> Sat w (ADT.union t1' rhs)
+    Unsat     -> eval rhs
 
 eval (ADT.Intersect t1 t2)       =
   case (eval t1, eval t2) of
@@ -76,6 +72,7 @@
   show Unsat     = "⊥"
   show (Sat s r) = printf "%s ∨ lazy(%s)" (show s) (show r)
 
+-- | Returns a new instance of 'LazyOC' permitting all WQOs
 noConstraints :: LazyOC a
 noConstraints = Sat (WQO.empty) ADT.Unsat
 
@@ -92,28 +89,24 @@
 intersect :: (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a
 intersect t1 t2 = eval $ ADT.intersect (toADT t1) (toADT t2)
 
+-- | Returns @true@ if any orderings are permitted
 isSatisfiable :: LazyOC a -> Bool
 isSatisfiable (Sat _ _) = True
 isSatisfiable Unsat     = False
 
-singleton :: WQO a -> LazyOC a
-singleton c = Sat c ADT.Unsat
-
-relevantConstraints
-  :: (Eq a, Ord a, Hashable a) => LazyOC a -> S.Set a -> S.Set a -> LazyOC a
-relevantConstraints c _ _ = c
-
 notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool
 notStrongerThan _     Unsat = return True
 notStrongerThan t1    t2    = return $ t1 == t2
 
-addConstraint :: (Ord a, Hashable a) => ADT.WQO a -> LazyOC a -> LazyOC a
+-- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@
+addConstraint :: (Ord a, Hashable a) => WQO a -> LazyOC a -> LazyOC a
 addConstraint o c = eval $ ADT.addConstraint o (toADT c)
 
 permits :: (Ord a, Hashable a) => LazyOC a -> WQO.WQO a -> Bool
 permits Unsat _            = False
 permits (Sat s1 thunk) wqo = s1 `WQO.notStrongerThan` wqo || permits (eval thunk) wqo
 
+-- | See 'LazyOC'
 lazyOC :: Monad m => OC.WQOConstraints LazyOC m
 lazyOC = OC.OC
   addConstraint
@@ -122,9 +115,6 @@
   notStrongerThan
   noConstraints
   permits
-  relevantConstraints
   union
   unsatisfiable
-  undefined
   getOrdering
-  id
diff --git a/src/Language/REST/WQOConstraints/Strict.hs b/src/Language/REST/WQOConstraints/Strict.hs
--- a/src/Language/REST/WQOConstraints/Strict.hs
+++ b/src/Language/REST/WQOConstraints/Strict.hs
@@ -3,24 +3,17 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
+-- | This module defines an implemenation for representing constraints on a 'WQO';
+--   in this case represented by a set of "extendable" WQOs each satisfying the constraints.
+--   For more details see 'StrictOC'
 module Language.REST.WQOConstraints.Strict (
       strictOC
     , strictOC'
-    , addConstraint
     , difference
-    , getOrdering
-    , intersect
-    , isSatisfiable
     , isUnsatisfiable
     , noConstraints
-    , notStrongerThan
     , permits
-    , relevantConstraints
-    , union
-    , unsatisfiable
-    , singleton
     , StrictOC
-    , elems
     ) where
 
 import Control.Monad.Identity
@@ -40,7 +33,19 @@
 -- The constraints are represented as a set ws of WQOs
 -- The constraints permit any WQO w that is a valid extension of some (w' in wqos)
 
-
+-- | @StrictOC ws@ represents constraints on a WQO. Each element of @ws@ is a WQO
+--   that satisfies the constraints. @StrictOC ws@ permits a WQO @w@ if there exists
+--   a @w'@ in @ws@ such that @w'@ can be extended to yield @w@.
+--
+--   This implementation is similar to disjunctive normal form representation of
+--   logical formulas; except in this case each "conjunction" is a valid WQO, and thus
+--   "satisfiable". Therefore @StrictOC ws@ satisfies /some/ WQO iff @ws@ is not empty.
+--
+--   Two potential downsides to this implementation are:
+--   1. The size of @ws@ can grow quickly; an inherent issue of DNF
+--   2. Related, calculating the entire set @ws@ is computationally expensive,
+--      and often unnecessary for RESTs use-case, where continuing the path only
+--      requires knowing if /any/ WQO is permitted.
 data StrictOC a = StrictOC (S.Set (WQO a))
   deriving (Eq, Ord, Generic, Hashable)
 
@@ -48,22 +53,20 @@
   show (StrictOC cs) | S.null cs             = "unsatisfiable"
   show (StrictOC cs) | S.member WQO.empty cs = "no constraints"
   show (StrictOC cs) = L.intercalate " ∨ \n" (map show (S.toList cs))
-    -- where
-      -- show' o@(OpOrdering s) = if S.size s > 1 then printf "(%s)" (show o) else show o
 
 getOrdering :: StrictOC a -> Maybe (WQO a)
 getOrdering (StrictOC o) =
   listToMaybe (S.toList o)
 
-elems :: Ord a => StrictOC a -> S.Set a
-elems (StrictOC sets) = S.unions $ map WQO.elems (S.toList sets)
-
+-- | Constraints that permit any 'WQO'. In this case implemented by
+--   a singleton set containing an empty WQO.
 noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a
 noConstraints = StrictOC (S.singleton (WQO.empty))
 
 unsatisfiable :: StrictOC a
 unsatisfiable = StrictOC S.empty
 
+-- | Returns @true@ iff @strictOC ws@ does not permit any WQOs; i.e., if @ws@ is empty.
 isUnsatisfiable :: Eq a => StrictOC a -> Bool
 isUnsatisfiable c = c == unsatisfiable
 
@@ -96,8 +99,8 @@
             else go (x : include) xs
 
 
--- The intersection of two constraints `a` and `b` is new constraints that only
--- permits the orderings permitted by both `a` and `b`
+-- | The intersection of two constraints `a` and `b` is new constraints that only
+--   permits the orderings permitted by both `a` and `b`
 intersect :: (Show a, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a
 intersect (StrictOC lhs) (StrictOC rhs) = result
   -- trace (printf "%s intersect %s yields %s" (show lhs) (show rhs) (show result)) result
@@ -113,26 +116,13 @@
   c'  <-  S.toList oc
   maybeToList $ WQO.merge c c'
 
-singleton :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a
-singleton c = addConstraint c noConstraints
-
-relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> S.Set a -> S.Set a -> StrictOC a
-relevantConstraints (StrictOC oc0) as bs = go (S.toList oc0) unsatisfiable
-  where
-    go :: [WQO a] -> StrictOC a -> StrictOC a
-    go []          oc   = oc
-    go (o : rest) exist =
-      let
-        o' = WQO.relevantTo o as bs
-      in
-        if WQO.null o'
-        then noConstraints
-        else go rest (union (singleton o) exist)
-
+-- | @StrictOC ws@ permits a 'WQO' @w@ if there exists a @w'@ in @ws@
+--   that can be extended to equal @w@
 permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool
 permits (StrictOC permitted) desired =
   any (`WQO.notStrongerThan` desired) (S.toList permitted)
 
+-- | An implementation of 'StrictOC'; for any computational context
 strictOC :: Monad m => OC.WQOConstraints StrictOC m
 strictOC = OC.OC
   addConstraint
@@ -141,12 +131,11 @@
   notStrongerThan
   noConstraints
   permits
-  relevantConstraints
   union
   unsatisfiable
-  elems
   getOrdering
-  id
 
+-- | An implementation of 'StrictOC' in the 'Identity' monad; usable in pure
+--   computations.
 strictOC' :: OC.WQOConstraints StrictOC Identity
 strictOC' = strictOC
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -36,9 +36,11 @@
 import Language.REST.Op
 import Language.REST.RPO
 import Language.REST.Internal.OpOrdering
+import Language.REST.RewriteRule
 import Language.REST.RuntimeTerm
 import Language.REST.MetaTerm as MT
 import Language.REST.Internal.Rewrite
+import Language.REST.Internal.WQO
 import Language.REST.Rest
 import Language.REST.SMT
 import qualified Language.REST.WQOConstraints.ADT as AC
@@ -46,6 +48,13 @@
 import qualified Data.Maybe as Mb
 import qualified Data.HashSet as S
 
+
+-- | 'canOrient' returns true iff the ordering constraint algebra permits an ordering
+--   that orients, the path, i.e., the constraints generated by 'orient' are satisfiable.
+canOrient :: forall oc m . Show oc
+  => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool
+canOrient terms = isSat ?impl (orient ?impl terms)
+
 diverges :: (Show oc) => OCAlgebra oc RuntimeTerm IO -> [RuntimeTerm] -> IO Bool
 diverges impl ts = not <$> (isSat impl $ orient impl ts)
 
@@ -53,7 +62,7 @@
   => OCAlgebra oc RuntimeTerm IO
   -> S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm)
 rewrites impl evalRWs userRWs t0 =
-  terms <$> fst <$> rest
+  resultTerms <$> fst <$> rest
     RESTParams
       { re           = evalRWs
       , ru           = userRWs
@@ -115,6 +124,14 @@
     return $ not $ disjoint rw1 rw2
   where
     disjoint s1 s2 = S.null $ s1 `S.intersection` s2
+
+eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm
+eval rws t0 =
+  do
+    result <- mapM (apply t0) (S.toList rws)
+    case S.toList $ S.unions result of
+      []      -> return t0
+      (t : _) -> eval rws t
 
 arithTests :: (Show oc, Hashable oc, Eq oc) => OCAlgebra oc RuntimeTerm IO -> [(String, IO Bool)]
 arithTests impl =