Clarify exports

src/core.jl

@@ -1,4 +1,6 @@
-export Variable
+import Base: match
+
+export Variable, match
 
 
 const Σ = Symbol
@@ -11,13 +13,39 @@ abstract type AbstractMatcher end
 abstract type AbstractSubproblem end
 
 
+mutable struct Variable end
+
+
+const Substitution = Dict{Variable,AbstractTerm}
+
+struct Matches{S<:AbstractSubproblem}
+    p::Substitution
+    s::S
+end
+Base.IteratorSize(::Type{<:Matches}) = Base.SizeUnknown()
+
+struct Fail end
+Base.iterate(::Fail) = nothing
+Base.length(::Fail) = 0
+const fail = Fail()
+
+"""
+    match(pattern::AbstractMatcher, term::AbstractTerm)
+
+Match `term` against `pattern`, producing an iterator containing all matches.
+"""
+function match(p::AbstractMatcher, t::AbstractTerm)
+    σ = Substitution()
+    s = match!(σ, p, t)
+    s === nothing && return fail
+    Matches(σ, s)
+end
+
+
 struct EmptySubproblem <: AbstractSubproblem end
 Base.iterate(m::Matches{EmptySubproblem}) = (m.p, nothing)
 Base.iterate(::Matches{EmptySubproblem}, ::Any) = nothing
 
-
-mutable struct Variable end
-
 vars(x::Variable) = Set([x])
 compile(x::Variable, V) = (x, push!(copy(V), x))
 @inline function match!(σ, x::Variable, t::AbstractTerm)
@@ -32,17 +60,3 @@ end
 >ₜ(::Variable, ::AbstractTerm) = false
 >ₜ(::AbstractTerm, ::Variable) = true
 >ₜ(x::Variable, y::Variable) = objectid(x) > objectid(y)
-
-
-const Substitution = Dict{Variable,AbstractTerm}
-
-struct Matches{S<:AbstractSubproblem}
-    p::Substitution
-    s::S
-end
-Base.IteratorSize(::Type{<:Matches}) = Base.SizeUnknown()
-
-struct Fail end
-Base.iterate(::Fail) = nothing
-Base.length(::Fail) = 0
-const fail = Fail()

src/interface.jl

@@ -1,3 +1,6 @@
+export compile
+
+
 """
     theory(T::Type{<:AbstractTerm}) -> Theory
 
@@ -50,27 +53,15 @@ Compile `t` to a matcher.
 """
 compile(t) = compile(t, Set{Variable}())[1]
 
-"""
-    match(pattern::AbstractMatcher, term::AbstractTerm)
-
-Match `term` against `pattern`, producing an iterator containing all matches.
-
-!!! note
-
-    The iterator should only be nonempty when `pattern` and `term` are derived from the
-    same theory.
-"""
-function match(p::AbstractMatcher, t::AbstractTerm)
-    σ = Substitution()
-    s = match!(σ, p, t)
-    s === nothing && return fail
-    Matches(σ, s)
-end
-
 """
     match!(σ, pattern::AbstractMatcher, term::AbstractTerm) -> Union{AbstractSubproblem,Nothing}
 
 Match `term` against `pattern` given the partial substitution `σ`, mutating `σ` and
 producing a subproblem to solve or producing `nothing` if a match is impossible.
+
+!!! note
+
+    Unless `pattern` and `term` are derived from the same theory, `match!` should
+    necessarily produce `nothing`.
 """
 match!(::Any, ::AbstractMatcher, ::AbstractTerm) = nothing

test/match.jl

@@ -219,9 +219,9 @@ TESTS = [
 
 @testset "$set" for (set, tests) ∈ TESTS
     @testset "$pattern" for (pattern, cases) ∈ tests
-        m = Terms.compile(pattern)
+        m = compile(pattern)
         @testset "$term" for (term, ms) ∈ cases
-            matches = Terms.match(m, term)
+            matches = match(m, term)
             @test Set(matches) == Set(matches)  # immutability of iterator
             @test Set(matches) == Set(ms)
         end