-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Please see the README on GitHub at
--   <a>https://github.com/jkoppel/ecta#readme</a>
@package ecta
@version 1.0.0.3

module Data.HashTable.Extended
getKeys :: HashTable h => IOHashTable h k v -> IO [k]
resetHashTable :: AnyHashTable -> IO ()
data AnyHashTable
[AnyHashTable] :: (HashTable h, Eq k, Hashable k) => IOHashTable h k v -> AnyHashTable

module Data.Interned.Extended.HashTableBased
type Id = Int

-- | Tried using the BasicHashtable size function to remove need for this
--   IORef ( see
--   <a>https://github.com/gregorycollins/hashtables/pull/68</a> ), but it
--   was slower
data Cache t
Cache :: !IORef Id -> !CuckooHashTable (Description t) t -> Cache t
[fresh] :: Cache t -> !IORef Id
[content] :: Cache t -> !CuckooHashTable (Description t) t
freshCache :: IO (Cache t)
cacheSize :: Cache t -> IO Int
resetCache :: Interned t => Cache t -> IO ()
class (Eq (Description t), Hashable (Description t)) => Interned t where {
    data family Description t;
    type family Uninterned t;
}
describe :: Interned t => Uninterned t -> Description t
identify :: Interned t => Id -> Uninterned t -> t
cache :: Interned t => Cache t
intern :: Interned t => Uninterned t -> t

module Data.Interned.Extended.SingleThreaded
intern :: Interned t => Uninterned t -> t


-- | Lightweight union-find implementation suitable for use with
--   nondeterminism
module Data.Persistent.UnionFind
data UVarGen
initUVarGen :: UVarGen
nextUVar :: UVarGen -> (UVarGen, UVar)
data UVar
uvarToInt :: UVar -> Int
intToUVar :: Int -> UVar
data UnionFind
empty :: UnionFind
withInitialValues :: [UVar] -> UnionFind
union :: UVar -> UVar -> UnionFind -> UnionFind
find :: UVar -> UnionFind -> (UVar, UnionFind)
instance GHC.Show.Show Data.Persistent.UnionFind.UVarGen
instance GHC.Classes.Ord Data.Persistent.UnionFind.UVarGen
instance GHC.Classes.Eq Data.Persistent.UnionFind.UVarGen
instance GHC.Show.Show Data.Persistent.UnionFind.UVar
instance GHC.Classes.Ord Data.Persistent.UnionFind.UVar
instance GHC.Classes.Eq Data.Persistent.UnionFind.UVar
instance GHC.Show.Show Data.Persistent.UnionFind.UnionFind
instance GHC.Classes.Ord Data.Persistent.UnionFind.UnionFind
instance GHC.Classes.Eq Data.Persistent.UnionFind.UnionFind

module Data.Text.Extended.Pretty
class Pretty a
pretty :: Pretty a => a -> Text
instance GHC.Show.Show a => Data.Text.Extended.Pretty.Pretty a

module Data.Memoization.Metrics
data CacheMetrics
CacheMetrics :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> CacheMetrics
[queryCount] :: CacheMetrics -> {-# UNPACK #-} !Int
[missCount] :: CacheMetrics -> {-# UNPACK #-} !Int
instance GHC.Show.Show Data.Memoization.Metrics.CacheMetrics
instance GHC.Classes.Ord Data.Memoization.Metrics.CacheMetrics
instance GHC.Classes.Eq Data.Memoization.Metrics.CacheMetrics
instance Data.Text.Extended.Pretty.Pretty Data.Memoization.Metrics.CacheMetrics


-- | Quick-and-dirty, thread-unsafe, hash-based memoization.
module Data.Memoization
data MemoCacheTag
NameTag :: Text -> MemoCacheTag
resetAllCaches :: IO ()
memoIO :: forall a b. (Eq a, Hashable a) => MemoCacheTag -> (a -> b) -> IO (a -> IO b)
memo :: (Eq a, Hashable a) => MemoCacheTag -> (a -> b) -> a -> b
memo2 :: (Eq a, Hashable a, Eq b, Hashable b) => MemoCacheTag -> (a -> b -> c) -> a -> b -> c
instance GHC.Generics.Generic Data.Memoization.MemoCacheTag
instance GHC.Show.Show Data.Memoization.MemoCacheTag
instance GHC.Classes.Ord Data.Memoization.MemoCacheTag
instance GHC.Classes.Eq Data.Memoization.MemoCacheTag
instance Data.Hashable.Class.Hashable Data.Memoization.MemoCacheTag
instance Data.Text.Extended.Pretty.Pretty Data.Memoization.MemoCacheTag

module Utility.Fixpoint
fix :: (Show a, Eq a) => Int -> (a -> a) -> a -> a
fixUnbounded :: Eq a => (a -> a) -> a -> a
fixMaybe :: Eq a => (a -> Maybe a) -> a -> Maybe a


-- | Representations of paths in an FTA, data structures for equality
--   constraints over paths, algorithms for saturating these constraints
module Data.ECTA.Internal.Paths
data Path
Path :: ![Int] -> Path
pattern EmptyPath :: Path
pattern ConsPath :: Int -> Path -> Path
unPath :: Path -> [Int]
path :: [Int] -> Path

-- | TODO: Should this be redone as a lens-library traversal? | TODO: I am
--   unhappy about this Emptyable design; makes one question whether this
--   should be a typeclass at all. (Terms/ECTAs differ in that there is
--   always an ECTA Node that represents the value at a path)
class Pathable t t' | t -> t' where {
    type family Emptyable t';
}
getPath :: Pathable t t' => Path -> t -> Emptyable t'
getAllAtPath :: Pathable t t' => Path -> t -> [t']
modifyAtPath :: Pathable t t' => (t' -> t') -> Path -> t -> t
pathHeadUnsafe :: Path -> Int
pathTailUnsafe :: Path -> Path
isSubpath :: Path -> Path -> Bool
isStrictSubpath :: Path -> Path -> Bool

-- | Read `substSubpath p1 p2 p3` as `[p1/p2]p3`
--   
--   `substSubpath replacement toReplace target` takes <tt>toReplace</tt>,
--   a prefix of target, and returns a new path in which <tt>toReplace</tt>
--   has been replaced by <tt>replacement</tt>.
--   
--   Undefined if toReplace is not a prefix of target
substSubpath :: Path -> Path -> Path -> Path

-- | Precondition: A nonempty cell exists
smallestNonempty :: Vector PathTrie -> Int

-- | Precondition: A nonempty cell exists
largestNonempty :: Vector PathTrie -> Int
getMaxNonemptyIndex :: PathTrie -> Maybe Int
data PathTrie
EmptyPathTrie :: PathTrie
TerminalPathTrie :: PathTrie
PathTrieSingleChild :: {-# UNPACK #-} !Int -> !PathTrie -> PathTrie
PathTrie :: !Vector PathTrie -> PathTrie
isEmptyPathTrie :: PathTrie -> Bool
isTerminalPathTrie :: PathTrie -> Bool

-- | Precondition: No path in the input is a subpath of another
toPathTrie :: [Path] -> PathTrie
fromPathTrie :: PathTrie -> [Path]
pathTrieDescend :: PathTrie -> Int -> PathTrie
data PathEClass
PathEClass' :: !PathTrie -> [Path] -> PathEClass
[getPathTrie] :: PathEClass -> !PathTrie
[getOrigPaths] :: PathEClass -> [Path]

-- | TODO: This pattern (and the caching of the original path list) is a
--   temporary affair until we convert all clients of PathEclass to fully
--   be based on tries
pattern PathEClass :: [Path] -> PathEClass
unPathEClass :: PathEClass -> [Path]
hasSubsumingMember :: PathEClass -> PathEClass -> Bool

-- | Extends the subsumption ordering to a total ordering by using the
--   default lexicographic comparison for incomparable elements. | TODO:
--   Optimization opportunity: Redundant work in the hasSubsumingMember
--   calls
completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering
data EqConstraints
EqConstraints :: [PathEClass] -> EqConstraints

-- | Must be sorted
[getEclasses] :: EqConstraints -> [PathEClass]
EqContradiction :: EqConstraints
pattern EmptyConstraints :: EqConstraints
rawMkEqConstraints :: [[Path]] -> EqConstraints
unsafeGetEclasses :: EqConstraints -> [PathEClass]
hasSubsumingMemberListBased :: [Path] -> [Path] -> Bool

-- | The real contradiction condition is a cycle in the subsumption
--   ordering. But, after congruence closure, this will reduce into a
--   self-cycle in the subsumption ordering.
--   
--   TODO; Prove this.
isContradicting :: [[Path]] -> Bool
mkEqConstraints :: [[Path]] -> EqConstraints
combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints
eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints
constraintsAreContradictory :: EqConstraints -> Bool
constraintsImply :: EqConstraints -> EqConstraints -> Bool
subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass]
unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass]
instance GHC.Generics.Generic Data.ECTA.Internal.Paths.Path
instance GHC.Show.Show Data.ECTA.Internal.Paths.Path
instance GHC.Classes.Ord Data.ECTA.Internal.Paths.Path
instance GHC.Classes.Eq Data.ECTA.Internal.Paths.Path
instance GHC.Generics.Generic Data.ECTA.Internal.Paths.PathTrie
instance GHC.Show.Show Data.ECTA.Internal.Paths.PathTrie
instance GHC.Classes.Eq Data.ECTA.Internal.Paths.PathTrie
instance GHC.Generics.Generic Data.ECTA.Internal.Paths.PathEClass
instance GHC.Show.Show Data.ECTA.Internal.Paths.PathEClass
instance GHC.Generics.Generic Data.ECTA.Internal.Paths.EqConstraints
instance GHC.Show.Show Data.ECTA.Internal.Paths.EqConstraints
instance GHC.Classes.Ord Data.ECTA.Internal.Paths.EqConstraints
instance GHC.Classes.Eq Data.ECTA.Internal.Paths.EqConstraints
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.Paths.EqConstraints
instance Data.Text.Extended.Pretty.Pretty Data.ECTA.Internal.Paths.EqConstraints
instance GHC.Classes.Eq Data.ECTA.Internal.Paths.PathEClass
instance GHC.Classes.Ord Data.ECTA.Internal.Paths.PathEClass
instance Data.Text.Extended.Pretty.Pretty Data.ECTA.Internal.Paths.PathEClass
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.Paths.PathEClass
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.Paths.PathTrie
instance GHC.Classes.Ord Data.ECTA.Internal.Paths.PathTrie
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.Paths.Path
instance Data.Text.Extended.Pretty.Pretty Data.ECTA.Internal.Paths.Path

module Data.ECTA.Paths
data Path
pattern EmptyPath :: Path
pattern ConsPath :: Int -> Path -> Path
unPath :: Path -> [Int]
path :: [Int] -> Path

-- | TODO: Should this be redone as a lens-library traversal? | TODO: I am
--   unhappy about this Emptyable design; makes one question whether this
--   should be a typeclass at all. (Terms/ECTAs differ in that there is
--   always an ECTA Node that represents the value at a path)
class Pathable t t' | t -> t' where {
    type family Emptyable t';
}
getPath :: Pathable t t' => Path -> t -> Emptyable t'
getAllAtPath :: Pathable t t' => Path -> t -> [t']
modifyAtPath :: Pathable t t' => (t' -> t') -> Path -> t -> t
pathHeadUnsafe :: Path -> Int
pathTailUnsafe :: Path -> Path
isSubpath :: Path -> Path -> Bool
data PathTrie
TerminalPathTrie :: PathTrie
isEmptyPathTrie :: PathTrie -> Bool
isTerminalPathTrie :: PathTrie -> Bool
getMaxNonemptyIndex :: PathTrie -> Maybe Int

-- | Precondition: No path in the input is a subpath of another
toPathTrie :: [Path] -> PathTrie
fromPathTrie :: PathTrie -> [Path]
pathTrieDescend :: PathTrie -> Int -> PathTrie
data PathEClass
unPathEClass :: PathEClass -> [Path]
hasSubsumingMember :: PathEClass -> PathEClass -> Bool

-- | Extends the subsumption ordering to a total ordering by using the
--   default lexicographic comparison for incomparable elements. | TODO:
--   Optimization opportunity: Redundant work in the hasSubsumingMember
--   calls
completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering
data EqConstraints
pattern EmptyConstraints :: EqConstraints
unsafeGetEclasses :: EqConstraints -> [PathEClass]
mkEqConstraints :: [[Path]] -> EqConstraints
combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints
eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints
constraintsAreContradictory :: EqConstraints -> Bool
constraintsImply :: EqConstraints -> EqConstraints -> Bool
subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass]
unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass]

module Data.ECTA.Internal.Term
data Symbol
Symbol' :: {-# UNPACK #-} !InternedText -> Symbol
pattern Symbol :: Text -> Symbol
data Term
Term :: !Symbol -> ![Term] -> Term
instance GHC.Classes.Ord Data.ECTA.Internal.Term.Symbol
instance GHC.Classes.Eq Data.ECTA.Internal.Term.Symbol
instance GHC.Generics.Generic Data.ECTA.Internal.Term.Term
instance GHC.Show.Show Data.ECTA.Internal.Term.Term
instance GHC.Read.Read Data.ECTA.Internal.Term.Term
instance GHC.Classes.Ord Data.ECTA.Internal.Term.Term
instance GHC.Classes.Eq Data.ECTA.Internal.Term.Term
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.Term.Term
instance Data.Text.Extended.Pretty.Pretty Data.ECTA.Internal.Term.Term
instance Data.ECTA.Internal.Paths.Pathable Data.ECTA.Internal.Term.Term Data.ECTA.Internal.Term.Term
instance Data.Text.Extended.Pretty.Pretty Data.ECTA.Internal.Term.Symbol
instance GHC.Show.Show Data.ECTA.Internal.Term.Symbol
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.Term.Symbol
instance Data.String.IsString Data.ECTA.Internal.Term.Symbol
instance GHC.Read.Read Data.ECTA.Internal.Term.Symbol

module Data.ECTA.Term
data Symbol
pattern Symbol :: Text -> Symbol
data Term
Term :: !Symbol -> ![Term] -> Term


-- | These were used in an earlier version of the enumeration algorithm,
--   but no longer.
--   
--   They are being kept around just in case.
module Data.ECTA.Internal.Paths.Zipper
unionPathTrie :: PathTrie -> PathTrie -> Maybe PathTrie
data InvertedPathTrie
PathZipperRoot :: InvertedPathTrie
PathTrieAt :: {-# UNPACK #-} !Int -> !PathTrie -> !InvertedPathTrie -> InvertedPathTrie
data PathTrieZipper
PathTrieZipper :: !PathTrie -> !InvertedPathTrie -> PathTrieZipper
emptyPathTrieZipper :: PathTrieZipper
pathTrieToZipper :: PathTrie -> PathTrieZipper
zipperCurPathTrie :: PathTrieZipper -> PathTrie
pathTrieZipperDescend :: PathTrieZipper -> Int -> PathTrieZipper

-- | The semantics of this may not be what you expect: Path trie zippers do
--   not support editing currently, only traversing. The value at the
--   cursor (as well as the index) is ignored except when traversing above
--   the root, where it uses those values to extend the path trie upwards.
pathTrieZipperAscend :: PathTrieZipper -> Int -> PathTrieZipper
unionPathTrieZipper :: PathTrieZipper -> PathTrieZipper -> Maybe PathTrieZipper
instance GHC.Show.Show Data.ECTA.Internal.Paths.Zipper.InvertedPathTrie
instance GHC.Classes.Ord Data.ECTA.Internal.Paths.Zipper.InvertedPathTrie
instance GHC.Classes.Eq Data.ECTA.Internal.Paths.Zipper.InvertedPathTrie
instance GHC.Show.Show Data.ECTA.Internal.Paths.Zipper.PathTrieZipper
instance GHC.Classes.Ord Data.ECTA.Internal.Paths.Zipper.PathTrieZipper
instance GHC.Classes.Eq Data.ECTA.Internal.Paths.Zipper.PathTrieZipper

module Data.ECTA.Internal.ECTA.Type
data RecNodeId

-- | Reference to the <a>Id</a> of an interned <a>Mu</a> node
RecInt :: !Id -> RecNodeId

-- | Reference to an as-yet uninterned <a>Mu</a> node, for which the
--   <a>Id</a> is not yet known
--   
--   The <a>Int</a> argument is used to distinguish between multiple nested
--   <a>Mu</a> nodes.
--   
--   NOTE: This is intentionally not an <a>Id</a>: it does not refer to the
--   <a>Id</a> of any interned node.
RecUnint :: Int -> RecNodeId

-- | Placeholder variable that we use <i>only</i> for depth calculations
--   
--   The invariant that this is used <i>only</i> for depth calculations,
--   along with the observation that depth calculation does not depend on
--   the exact choice of variable, justifies subtituting any other variable
--   for <a>RecDepth</a> in terms containing <a>RecDepth</a> in all
--   contexts.
RecDepth :: RecNodeId

-- | Refer to Mu-node-to-be-constructed during intersection
--   
--   TODO: It is obviously not very elegant to have a constructor here
--   specifically for one algorithm. Ideally, we would parameterize
--   <a>Node</a> with the type of the identifiers in it. This might be
--   useful also to rule out many other cases (specifically, most of the
--   time we are dealing with fully interned nodes, and so the only
--   constructor we expect is <a>RecInt</a>).
RecIntersect :: IntersectId -> RecNodeId
data Edge
InternedEdge :: !Id -> !UninternedEdge -> Edge
[edgeId] :: Edge -> !Id
[uninternedEdge] :: Edge -> !UninternedEdge
pattern Edge :: Symbol -> [Node] -> Edge
data UninternedEdge
UninternedEdge :: !Symbol -> ![Node] -> !EqConstraints -> UninternedEdge
[uEdgeSymbol] :: UninternedEdge -> !Symbol
[uEdgeChildren] :: UninternedEdge -> ![Node]
[uEdgeEcs] :: UninternedEdge -> !EqConstraints
mkEdge :: Symbol -> [Node] -> EqConstraints -> Edge
emptyEdge :: Edge
edgeChildren :: Edge -> [Node]
edgeEcs :: Edge -> EqConstraints
edgeSymbol :: Edge -> Symbol
setChildren :: Edge -> [Node] -> Edge
data Node
InternedNode :: {-# UNPACK #-} !InternedNode -> Node
EmptyNode :: Node
InternedMu :: {-# UNPACK #-} !InternedMu -> Node
Rec :: !RecNodeId -> Node
pattern Node :: [Edge] -> Node

-- | Pattern only a Mu constructor
--   
--   When we go underneath a Mu constructor, we need to bind the
--   corresponding Rec node to something: that's why pattern matching on
--   <a>Mu</a> yields a function. Code that wants to traverse the term
--   as-is should match on the interned constructors instead (and then deal
--   with the dangling references).
--   
--   An identity function
--   
--   <pre>
--   foo (Mu f) = Mu f
--   </pre>
--   
--   will run in O(1) time:
--   
--   <pre>
--   foo (Mu f) = Mu f
--     -- { expand view patern }
--   foo node | Just f &lt;- matchMu node = createMu f
--     -- { case for @InternedMu mu@ }
--   foo (InternedMu mu) | Just f &lt;- matchMu (InternedMu m) = createMu f
--     -- { definition of matchMu }
--   foo (InternedMu mu) = let f = \n' -&gt;
--                            if | n' == Rec (RecUnint (numNestedMu (internedMuBody mu))) -&gt;
--                                  internedMuShape mu
--                              | n' == Rec RecDepth -&gt;
--                                  internedMuShape mu
--                              | otherwise -&gt;
--                                  substFree (internedMuId mu) n' (internedMuBody mu)
--                         in createMu f
--     -- { definition of createMu }
--   foo (InternedMu mu) = intern $ UninternedMu (f . Rec)
--   </pre>
--   
--   At this point, <a>intern</a> will call `shape (f . Rec)`, which will
--   call `f . Rec` twice: once with <a>RecDepth</a> to compute the depth,
--   and then once again with that depth to substitute a placeholder. Both
--   of these special cases will use <a>internedMuShape</a> (and moreover,
--   the depth calculation on <a>internedMuShape</a> is <tt>O(1)</tt>).
pattern Mu :: (Node -> Node) -> Node
data InternedNode
MkInternedNode :: {-# UNPACK #-} !Id -> ![Edge] -> !Int -> !Set RecNodeId -> InternedNode

-- | The <a>Id</a> of the node itself
[internedNodeId] :: InternedNode -> {-# UNPACK #-} !Id

-- | All outgoing edges
[internedNodeEdges] :: InternedNode -> ![Edge]

-- | Maximum Mu nesting depth in the term
[internedNodeNumNestedMu] :: InternedNode -> !Int

-- | Free variables in the term
[internedNodeFree] :: InternedNode -> !Set RecNodeId
data InternedMu
MkInternedMu :: {-# UNPACK #-} !Id -> !Node -> !Node -> InternedMu

-- | <a>Id</a> of the node itself
[internedMuId] :: InternedMu -> {-# UNPACK #-} !Id

-- | The body of the <a>Mu</a>
--   
--   Recursive occurrences to this node should be
--   
--   <pre>
--   Rec (RecNodeId internedMuId)
--   </pre>
[internedMuBody] :: InternedMu -> !Node

-- | The body of the <a>Mu</a>, before it was assigned an <a>Id</a>
--   
--   Invariant:
--   
--   <pre>
--      substFree internedMuId (Rec (RecUnint (numNestedMu internedMuBody)) internedMuBody
--   == internedMuShape
--   </pre>
[internedMuShape] :: InternedMu -> !Node
data UninternedNode
UninternedNode :: ![Edge] -> UninternedNode
UninternedEmptyNode :: UninternedNode

-- | Recursive node
--   
--   The function should be parametric in the Id:
--   
--   <pre>
--   substFree i (Rec j) (f i) == f j
--   </pre>
--   
--   See <a>shape</a> for additional discussion.
UninternedMu :: !RecNodeId -> Node -> UninternedNode

-- | Context-free references to a <a>Mu</a> node introduced by
--   <tt>intersect</tt>
--   
--   Background: This is a generalization of the idea to be able to refer
--   to the "immediately enclosing binder", and then only deal with graphs
--   with the property that we never need to refer past that enclosing
--   binder. This too would allow us to refer to a <a>Mu</a> node without
--   knowing its <a>Id</a>, at the cost of requiring a substitution when we
--   discover that <a>Id</a> to return this into a <a>RecInt</a>. The
--   generalization is that all we need to <i>some</i> way to refer to that
--   <a>Mu</a> node concretely, without <a>Id</a>, but we can: intersection
--   introduces <a>Mu</a> whenever it encounters a <a>Mu</a> on the left or
--   the right, /and will then not introduce another <a>Mu</a> for that
--   same intersection problem (at least, not in the same scope). This
--   means that the <a>Id</a> of the left and right operand will indeed
--   uniquely identify the <a>Mu</a> node to be constructed by
--   <tt>intersect</tt>.
--   
--   Furthermore, since we cache the free variables in a term, we have a
--   cheap check to see if we need the <a>Mu</a> node at all. This means
--   that <i>if</i> the input graphs satisfy the property that there are
--   references past <a>Mu</a> nodes, the output should too: we will not
--   introduce redundant <a>Mu</a> nodes.
--   
--   NOTE: Although intersect has three cases in which it introduces
--   <a>Mu</a> nodes (<a>Mu</a> in both operands, <a>Mu</a> in the left, or
--   <a>Mu</a> in the right), we don't need that distinction here: we just
--   need to know the <a>Id</a> of the two operands, so that if we see a
--   call to intersect again <i>with those same two operands</i> (no matter
--   what kind of nodes they are), we can refer to the newly constructed
--   <a>Mu</a> node.
data IntersectId
pattern IntersectId :: Id -> Id -> IntersectId
nodeIdentity :: Node -> Id

-- | Maximum number of nested Mus in the term
--   
--   @O(1) provided that there are no unbounded Mu chains in the term.
numNestedMu :: Node -> Int

-- | Substitution
--   
--   <tt>substFree i n</tt> will replace all occurrences of <tt>Rec
--   (RecNodeId i)</tt> by <tt>n</tt>. We appeal to the uniqueness of node
--   IDs and assume that all occurrences of <tt>i</tt> must be free (in
--   other words, that any occurrences of <a>Mu</a> will have a
--   <i>different</i> identifier.
--   
--   Postcondition:
--   
--   <pre>
--   substFree i (Rec (RecNodeId i)) == id
--   </pre>
substFree :: RecNodeId -> Node -> Node -> Node

-- | Free variables in the term
--   
--   <tt>O(1) in the size of the graph, provided that there are no
--   unbounded Mu chains in the term. </tt>O(log n)@ in the number of free
--   variables in the graph, which we expect to be orders of magnitude
--   smaller than the size of the graph (indeed, we don't expect more than
--   a handful).
freeVars :: Node -> Set RecNodeId

-- | An optimized Node constructor that avoids the interning/preprocessing
--   of the Node constructor when nothing changes
modifyNode :: Node -> ([Edge] -> [Edge]) -> Node

-- | Construct recursive node
--   
--   Implementation note: <a>createMu</a> and <a>matchMu</a> interact in
--   non-trivial ways; see docs of the <a>Mu</a> pattern synonym for
--   performance considerations.
createMu :: (Node -> Node) -> Node
instance GHC.Generics.Generic Data.ECTA.Internal.ECTA.Type.IntersectId
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.IntersectId
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Type.IntersectId
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Type.IntersectId
instance GHC.Generics.Generic Data.ECTA.Internal.ECTA.Type.RecNodeId
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.RecNodeId
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Type.RecNodeId
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Type.RecNodeId
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.InternedMu
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.InternedNode
instance GHC.Generics.Generic Data.ECTA.Internal.ECTA.Type.UninternedEdge
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.UninternedEdge
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Type.UninternedEdge
instance GHC.Generics.Generic (Data.Interned.Extended.HashTableBased.Description Data.ECTA.Internal.ECTA.Type.Edge)
instance GHC.Classes.Eq (Data.Interned.Extended.HashTableBased.Description Data.ECTA.Internal.ECTA.Type.Edge)
instance GHC.Generics.Generic (Data.Interned.Extended.HashTableBased.Description Data.ECTA.Internal.ECTA.Type.Node)
instance GHC.Classes.Eq (Data.Interned.Extended.HashTableBased.Description Data.ECTA.Internal.ECTA.Type.Node)
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Type.UninternedNode
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Type.UninternedNode
instance Data.Interned.Extended.HashTableBased.Interned Data.ECTA.Internal.ECTA.Type.Node
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.Edge
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Type.Edge
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Type.Edge
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Type.Edge
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Type.Node
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Type.Node
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Type.Node
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Type.Node
instance Data.Hashable.Class.Hashable (Data.Interned.Extended.HashTableBased.Description Data.ECTA.Internal.ECTA.Type.Node)
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Type.UninternedEdge
instance Data.Interned.Extended.HashTableBased.Interned Data.ECTA.Internal.ECTA.Type.Edge
instance Data.Hashable.Class.Hashable (Data.Interned.Extended.HashTableBased.Description Data.ECTA.Internal.ECTA.Type.Edge)
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Type.RecNodeId
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Type.IntersectId

module Utility.HashJoin

-- | PRECONDITION: (h x == h y) =&gt; x == y
nubById :: (a -> Int) -> [a] -> [a]
nubByIdSinglePass :: forall a. (a -> Int) -> [a] -> [a]
hashClusterIdNub :: (a -> Int) -> (a -> Int) -> [a] -> [[a]]
clusterByHash :: (a -> Int) -> [a] -> [[a]]
hashJoin :: (a -> Int) -> (a -> a -> b) -> [a] -> [a] -> [b]

module Data.ECTA.Internal.ECTA.Operations

-- | Warning: Linear in number of paths, exponential in size of graph. Only
--   use for very small graphs.
pathsMatching :: (Node -> Bool) -> Node -> [Path]

-- | Precondition: For all i, f (Rec i) is either a Rec node meant to
--   represent the enclosing Mu, or contains no Rec node not beneath
--   another Mu.
mapNodes :: (Node -> Node) -> Node -> Node
crush :: forall m. Monoid m => (Node -> m) -> Node -> m
onNormalNodes :: Monoid m => (Node -> m) -> Node -> m
unfoldOuterRec :: Node -> Node
refold :: Node -> Node
nodeEdges :: Node -> [Edge]
unfoldBounded :: Int -> Node -> Node
nodeCount :: Node -> Int
edgeCount :: Node -> Int
maxIndegree :: Node -> Int
union :: [Node] -> Node
nodeRepresents :: Node -> Term -> Bool
edgeRepresents :: Edge -> Term -> Bool
intersect :: Node -> Node -> Node
dropRedundantEdges :: [Edge] -> [Edge]
intersectEdge :: Edge -> Edge -> Maybe Edge
requirePath :: Path -> Node -> Node
requirePathList :: Path -> [Node] -> [Node]
withoutRedundantEdges :: Node -> Node
reducePartially :: Node -> Node
reduceEdgeIntersection :: EqConstraints -> Edge -> Edge
reduceEqConstraints :: EqConstraints -> EqConstraints -> [Node] -> [Node]
getSubnodeById :: Node -> Id -> Maybe Node
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Operations.IntersectionDom
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Operations.IntersectionDom
instance Data.Hashable.Class.Hashable Data.ECTA.Internal.ECTA.Operations.IntersectionDom
instance Data.ECTA.Internal.Paths.Pathable Data.ECTA.Internal.ECTA.Type.Node Data.ECTA.Internal.ECTA.Type.Node
instance Data.ECTA.Internal.Paths.Pathable [Data.ECTA.Internal.ECTA.Type.Node] Data.ECTA.Internal.ECTA.Type.Node

module Data.ECTA.Internal.ECTA.Visualization

-- | To visualize an FTA: 1) Call `prettyPrintDot $ toDot fta` from GHCI 2)
--   Copy the output to viz-js.jom or another GraphViz implementation
toDot :: Node -> Graph
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Visualization.PartialGraph
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Visualization.FglNodeLabel
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Visualization.FglNodeLabel
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Visualization.FglNodeLabel
instance GHC.Base.Semigroup Data.ECTA.Internal.ECTA.Visualization.PartialGraph
instance GHC.Base.Monoid Data.ECTA.Internal.ECTA.Visualization.PartialGraph

module Data.ECTA.Internal.ECTA.Enumeration
data TermFragment
TermFragmentNode :: !Symbol -> ![TermFragment] -> TermFragment
TermFragmentUVar :: UVar -> TermFragment
termFragToTruncatedTerm :: TermFragment -> Term
data SuspendedConstraint
SuspendedConstraint :: !PathTrie -> !UVar -> SuspendedConstraint
scGetPathTrie :: SuspendedConstraint -> PathTrie
scGetUVar :: SuspendedConstraint -> UVar
descendScs :: Int -> Seq SuspendedConstraint -> Seq SuspendedConstraint
data UVarValue
UVarUnenumerated :: !Maybe Node -> !Seq SuspendedConstraint -> UVarValue
[contents] :: UVarValue -> !Maybe Node
[constraints] :: UVarValue -> !Seq SuspendedConstraint
UVarEnumerated :: !TermFragment -> UVarValue
[termFragment] :: UVarValue -> !TermFragment
UVarEliminated :: UVarValue
data EnumerationState
EnumerationState :: UVarGen -> UnionFind -> Seq UVarValue -> EnumerationState
[_uvarCounter] :: EnumerationState -> UVarGen
[_uvarRepresentative] :: EnumerationState -> UnionFind
[_uvarValues] :: EnumerationState -> Seq UVarValue
uvarCounter :: Lens' EnumerationState UVarGen
uvarRepresentative :: Lens' EnumerationState UnionFind
uvarValues :: Lens' EnumerationState (Seq UVarValue)
initEnumerationState :: Node -> EnumerationState
type EnumerateM = StateT EnumerationState []
getUVarRepresentative :: UVar -> EnumerateM UVar
assimilateUvarVal :: UVar -> UVar -> EnumerateM ()
mergeNodeIntoUVarVal :: UVar -> Node -> Seq SuspendedConstraint -> EnumerateM ()
getUVarValue :: UVar -> EnumerateM UVarValue
getTermFragForUVar :: UVar -> EnumerateM TermFragment
runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)]
enumerateNode :: Seq SuspendedConstraint -> Node -> EnumerateM TermFragment
enumerateEdge :: Seq SuspendedConstraint -> Edge -> EnumerateM TermFragment
firstExpandableUVar :: EnumerateM ExpandableUVarResult
enumerateOutUVar :: UVar -> EnumerateM TermFragment
enumerateOutFirstExpandableUVar :: EnumerateM ()
enumerateFully :: EnumerateM ()
expandTermFrag :: TermFragment -> EnumerateM Term
expandUVar :: UVar -> EnumerateM Term
getAllTruncatedTerms :: Node -> [Term]
getAllTerms :: Node -> [Term]

-- | Inefficient enumeration
--   
--   For ECTAs with <a>Mu</a> nodes may produce an infinite list or may
--   loop indefinitely, depending on the ECTAs. For example, for
--   
--   <pre>
--   createMu $ \r -&gt; Node [Edge "f" [r], Edge "a" []]
--   </pre>
--   
--   it will produce
--   
--   <pre>
--   [ Term "a" []
--   , Term "f" [Term "a" []]
--   , Term "f" [Term "f" [Term "a" []]]
--   , ...
--   ]
--   </pre>
--   
--   This happens to work currently because non-recursive edges are
--   interned before recursive edges.
--   
--   TODO: It would be much nicer if this did fair enumeration. It would
--   avoid the beforementioned dependency on interning order, and it would
--   give better enumeration for examples such as
--   
--   <pre>
--   Node [Edge "h" [
--       createMu $ \r -&gt; Node [Edge "f" [r], Edge "a" []]
--     , createMu $ \r -&gt; Node [Edge "g" [r], Edge "b" []]
--     ]]
--   </pre>
--   
--   This will currently produce
--   
--   <pre>
--   [ Term "h" [Term "a" [], Term "b" []]
--   , Term "h" [Term "a" [], Term "g" [Term "b" []]]
--   , Term "h" [Term "a" [], Term "g" [Term "g" [Term "b" []]]]
--   , ..
--   ]
--   </pre>
--   
--   where it always unfolds the <i>second</i> argument to <tt>h</tt>,
--   never the first.
naiveDenotation :: Node -> [Term]
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Enumeration.TermFragment
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Enumeration.TermFragment
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Enumeration.TermFragment
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Enumeration.SuspendedConstraint
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Enumeration.SuspendedConstraint
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Enumeration.SuspendedConstraint
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Enumeration.UVarValue
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Enumeration.UVarValue
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Enumeration.UVarValue
instance GHC.Show.Show Data.ECTA.Internal.ECTA.Enumeration.EnumerationState
instance GHC.Classes.Ord Data.ECTA.Internal.ECTA.Enumeration.EnumerationState
instance GHC.Classes.Eq Data.ECTA.Internal.ECTA.Enumeration.EnumerationState


-- | Equality-constrained deterministic finite tree automata
--   
--   Specialized to DAGs, plus at most one globally unique recursive node
module Data.ECTA
data Edge
pattern Edge :: Symbol -> [Node] -> Edge
mkEdge :: Symbol -> [Node] -> EqConstraints -> Edge
edgeChildren :: Edge -> [Node]
edgeSymbol :: Edge -> Symbol
data Node
EmptyNode :: Node
pattern Node :: [Edge] -> Node
nodeEdges :: Node -> [Edge]

-- | Maximum number of nested Mus in the term
--   
--   @O(1) provided that there are no unbounded Mu chains in the term.
numNestedMu :: Node -> Int

-- | Construct recursive node
--   
--   Implementation note: <a>createMu</a> and <a>matchMu</a> interact in
--   non-trivial ways; see docs of the <a>Mu</a> pattern synonym for
--   performance considerations.
createMu :: (Node -> Node) -> Node

-- | Warning: Linear in number of paths, exponential in size of graph. Only
--   use for very small graphs.
pathsMatching :: (Node -> Bool) -> Node -> [Path]

-- | Precondition: For all i, f (Rec i) is either a Rec node meant to
--   represent the enclosing Mu, or contains no Rec node not beneath
--   another Mu.
mapNodes :: (Node -> Node) -> Node -> Node
refold :: Node -> Node
unfoldBounded :: Int -> Node -> Node
crush :: forall m. Monoid m => (Node -> m) -> Node -> m
onNormalNodes :: Monoid m => (Node -> m) -> Node -> m
nodeCount :: Node -> Int
edgeCount :: Node -> Int
maxIndegree :: Node -> Int
union :: [Node] -> Node
intersect :: Node -> Node -> Node
withoutRedundantEdges :: Node -> Node
reducePartially :: Node -> Node
type EnumerateM = StateT EnumerationState []
runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)]
enumerateFully :: EnumerateM ()
getAllTerms :: Node -> [Term]
getAllTruncatedTerms :: Node -> [Term]

-- | Inefficient enumeration
--   
--   For ECTAs with <a>Mu</a> nodes may produce an infinite list or may
--   loop indefinitely, depending on the ECTAs. For example, for
--   
--   <pre>
--   createMu $ \r -&gt; Node [Edge "f" [r], Edge "a" []]
--   </pre>
--   
--   it will produce
--   
--   <pre>
--   [ Term "a" []
--   , Term "f" [Term "a" []]
--   , Term "f" [Term "f" [Term "a" []]]
--   , ...
--   ]
--   </pre>
--   
--   This happens to work currently because non-recursive edges are
--   interned before recursive edges.
--   
--   TODO: It would be much nicer if this did fair enumeration. It would
--   avoid the beforementioned dependency on interning order, and it would
--   give better enumeration for examples such as
--   
--   <pre>
--   Node [Edge "h" [
--       createMu $ \r -&gt; Node [Edge "f" [r], Edge "a" []]
--     , createMu $ \r -&gt; Node [Edge "g" [r], Edge "b" []]
--     ]]
--   </pre>
--   
--   This will currently produce
--   
--   <pre>
--   [ Term "h" [Term "a" [], Term "b" []]
--   , Term "h" [Term "a" [], Term "g" [Term "b" []]]
--   , Term "h" [Term "a" [], Term "g" [Term "g" [Term "b" []]]]
--   , ..
--   ]
--   </pre>
--   
--   where it always unfolds the <i>second</i> argument to <tt>h</tt>,
--   never the first.
naiveDenotation :: Node -> [Term]

-- | To visualize an FTA: 1) Call `prettyPrintDot $ toDot fta` from GHCI 2)
--   Copy the output to viz-js.jom or another GraphViz implementation
toDot :: Node -> Graph

module Application.TermSearch.Type
data TypeSkeleton
TVar :: Text -> TypeSkeleton
TFun :: TypeSkeleton -> TypeSkeleton -> TypeSkeleton
TCons :: Text -> [TypeSkeleton] -> TypeSkeleton
data Benchmark
Benchmark :: Text -> Int -> Term -> [(Text, TypeSkeleton)] -> TypeSkeleton -> Benchmark
[bmName] :: Benchmark -> Text
[bmSize] :: Benchmark -> Int
[bmSolution] :: Benchmark -> Term
[bmArguments] :: Benchmark -> [(Text, TypeSkeleton)]
[bmGoalType] :: Benchmark -> TypeSkeleton
type Argument = (Symbol, Node)
data Mode
Normal :: Mode
HKTV :: Mode
Lambda :: Mode
data AblationType
Default :: AblationType
NoReduction :: AblationType
NoEnumeration :: AblationType
NoOptimize :: AblationType
instance GHC.Generics.Generic Application.TermSearch.Type.TypeSkeleton
instance Data.Data.Data Application.TermSearch.Type.TypeSkeleton
instance GHC.Read.Read Application.TermSearch.Type.TypeSkeleton
instance GHC.Show.Show Application.TermSearch.Type.TypeSkeleton
instance GHC.Classes.Ord Application.TermSearch.Type.TypeSkeleton
instance GHC.Classes.Eq Application.TermSearch.Type.TypeSkeleton
instance GHC.Read.Read Application.TermSearch.Type.Benchmark
instance GHC.Show.Show Application.TermSearch.Type.Benchmark
instance GHC.Classes.Ord Application.TermSearch.Type.Benchmark
instance GHC.Classes.Eq Application.TermSearch.Type.Benchmark
instance GHC.Generics.Generic Application.TermSearch.Type.Mode
instance Data.Data.Data Application.TermSearch.Type.Mode
instance GHC.Show.Show Application.TermSearch.Type.Mode
instance GHC.Classes.Ord Application.TermSearch.Type.Mode
instance GHC.Classes.Eq Application.TermSearch.Type.Mode
instance GHC.Generics.Generic Application.TermSearch.Type.AblationType
instance Data.Data.Data Application.TermSearch.Type.AblationType
instance GHC.Show.Show Application.TermSearch.Type.AblationType
instance GHC.Classes.Ord Application.TermSearch.Type.AblationType
instance GHC.Classes.Eq Application.TermSearch.Type.AblationType
instance Data.Hashable.Class.Hashable Application.TermSearch.Type.TypeSkeleton

module Application.TermSearch.Utils
typeConst :: Text -> Node
constrType0 :: Text -> Node
constrType1 :: Text -> Node -> Node
constrType2 :: Text -> Node -> Node -> Node
maybeType :: Node -> Node
listType :: Node -> Node
theArrowNode :: Node
arrowType :: Node -> Node -> Node
appType :: Node -> Node -> Node
mkDatatype :: Text -> [Node] -> Node
constFunc :: Symbol -> Node -> Edge
constArg :: Symbol -> Node -> Edge
var1 :: Node
var2 :: Node
var3 :: Node
var4 :: Node
varAcc :: Node
mkGroups :: [(Text, TypeSkeleton)] -> (Map TypeSkeleton Text, Map Text Text)
getRepOf :: [(Text, [Text])] -> Text -> Text
replicatorTau :: Node
replicator :: Node
loop1 :: Node
loop2 :: Node

module Application.TermSearch.Dataset
typeToFta :: TypeSkeleton -> Node
speciallyTreatedFunctions :: [Text]
hooglePlusComponents :: [(Text, TypeSkeleton)]
augumentedComponents :: [(Text, TypeSkeleton)]
hoogleComponents :: Map TypeSkeleton Text
groupMapping :: Map Text Text

module Application.TermSearch.TermSearch
tau :: Node
allConstructors :: [(Text, Int)]
generalize :: Node -> Node
app :: Node -> Node -> Node
applyOperator :: Node
hoogleComps :: [Edge]
anyFunc :: Node
filterType :: Node -> Node -> Node
termsK :: Node -> Bool -> Int -> [Node]
relevantTermK :: Node -> Bool -> Int -> [Argument] -> [Node]
relevantTermsOfSize :: Node -> [Argument] -> Int -> Node
relevantTermsUptoK :: Node -> [Argument] -> Int -> Node
prettyTerm :: Term -> Term
dropTypes :: Node -> Node
getText :: Symbol -> Text
fromJustFunc :: Node
maybeFunctions :: [Symbol]
listReps :: [Text]
isListFunction :: Symbol -> Bool
maybeReps :: [Text]
isMaybeFunction :: Symbol -> Bool
anyListFunc :: Node
anyNonListFunc :: Node
anyNonNilFunc :: Node
anyNonNothingFunc :: Node
reduceFully :: Node -> Node
checkSolution :: Term -> [Term] -> IO ()
reduceFullyAndLog :: Node -> IO Node
f1 :: Edge
f2 :: Edge
f3 :: Edge
f4 :: Edge
f5 :: Edge
f6 :: Edge
f7 :: Edge
f8 :: Edge
f9 :: Edge
f10 :: Edge
f11 :: Edge
f12 :: Edge
f13 :: Edge
f14 :: Edge
f15 :: Edge
f16 :: Edge
f17 :: Edge
f18 :: Edge
f19 :: Edge
f20 :: Edge
f21 :: Edge
f22 :: Edge
f23 :: Edge
f24 :: Edge
f25 :: Edge
f26 :: Edge
f27 :: Edge
f28 :: Edge
f29 :: Edge
f30 :: Edge
toMappedName :: Text -> Text
prettyPrintAllTerms :: AblationType -> Term -> Node -> IO ()
substTerm :: Term -> Term
parseHoogleComponent :: Text -> TypeSkeleton -> Edge

module Application.TermSearch.Evaluation
runBenchmark :: Benchmark -> AblationType -> Int -> IO ()


-- | A very bad SAT solver written by reduction to ECTA
--   
--   Also a constructive proof of the NP-hardness of finding a term
--   represented by an ECTA
module Application.SAT
data Var
mkVar :: Text -> Var

-- | Our construction generalizes to arbitrary NNF formulas, and possibly
--   to arbitrary SAT, but we don't need to bother; just CNF is good enough
data CNF
And :: [Clause] -> CNF
data Clause
Or :: [Lit] -> Clause
data Lit
PosLit :: Var -> Lit
NegLit :: Var -> Lit

-- | Encoding: formula(assnNode, formulaNode)
--   
--   assnNode: * One edge, with one child per literal (2*numVars total) *
--   Each literal has two choices, true or false * Use constraints to force
--   each positive/negative pair of literals to match. * E.g.: x1 node =
--   choice of (0, a) or (1, b). ~x1 node = choice of (0, b) or (1, a) If
--   x1<i>~x1 have indices 0</i>1, then the constraint 0.1=1.1 constrains
--   x1<i>~x1 to be either true</i>false or false/true
--   
--   formulaNode: * One edge, having one child per clause
--   
--   Clause nodes: * One edge per literal in the clause, each corresponding
--   to a choice of which variable makes the clause true. * Each edge has
--   2*numVars children containing a copy of the assnNode, followed by a
--   single child containing "1" * Constrain said final child to be equal
--   to the truth value of the corresponding literal in those 2*numVars
--   children which copy the assnNode
--   
--   Top level constraints: * Constrain the variable nodes in each clause
--   node to be equal to the global variable assignments.
toEcta :: CNF -> Node
allSolutions :: CNF -> HashSet (HashMap Var Bool)
ex1 :: CNF
ex2 :: CNF
ex3 :: CNF
instance GHC.Generics.Generic Application.SAT.Var
instance GHC.Show.Show Application.SAT.Var
instance GHC.Classes.Ord Application.SAT.Var
instance GHC.Classes.Eq Application.SAT.Var
instance GHC.Generics.Generic Application.SAT.Lit
instance GHC.Show.Show Application.SAT.Lit
instance GHC.Classes.Ord Application.SAT.Lit
instance GHC.Classes.Eq Application.SAT.Lit
instance GHC.Generics.Generic Application.SAT.Clause
instance GHC.Show.Show Application.SAT.Clause
instance GHC.Classes.Ord Application.SAT.Clause
instance GHC.Classes.Eq Application.SAT.Clause
instance GHC.Generics.Generic Application.SAT.CNF
instance GHC.Show.Show Application.SAT.CNF
instance GHC.Classes.Ord Application.SAT.CNF
instance GHC.Classes.Eq Application.SAT.CNF
instance GHC.Base.Semigroup Application.SAT.LitPaths
instance GHC.Base.Monoid Application.SAT.LitPaths
instance Application.SAT.FoldAlg Application.SAT.CNF
instance Application.SAT.FoldAlg Application.SAT.Clause
instance Application.SAT.FoldAlg Application.SAT.Lit
instance Data.Hashable.Class.Hashable Application.SAT.CNF
instance Data.Hashable.Class.Hashable Application.SAT.Clause
instance Data.Hashable.Class.Hashable Application.SAT.Lit
instance Data.Text.Extended.Pretty.Pretty Application.SAT.Lit
instance Data.Hashable.Class.Hashable Application.SAT.Var
instance Data.String.IsString Application.SAT.Var