diff --git a/src/syntax/EGraphs.jl b/src/syntax/EGraphs.jl
new file mode 100644
index 00000000..e1e402e9
--- /dev/null
+++ b/src/syntax/EGraphs.jl
@@ -0,0 +1,8 @@
+module EGraphs 
+
+export EGraph, ETerm, EClass, EType, EConstant, EId, 
+       add!, merge!, rebuild!
+
+include("egraphs/east.jl")
+
+end # module
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index afb866a3..84c012b9 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -1,6 +1,6 @@
 module GATs
 export Constant, AlgTerm, AlgType, AlgAST,
-  TypeScope, TypeCtx, AlgSort, AlgSorts,
+  TypeScope, TypeCtx, AlgSort, AlgSorts, MethodApp,
   AlgDeclaration, AlgTermConstructor, AlgTypeConstructor, AlgAccessor, AlgAxiom,
   sortsignature, getdecl,
   GATSegment, GAT, Presentation, gettheory, gettypecontext, allmethods, resolvemethod,
diff --git a/src/syntax/egraphs/algebraic.jl b/src/syntax/egraphs/algebraic.jl
new file mode 100644
index 00000000..34cedec7
--- /dev/null
+++ b/src/syntax/egraphs/algebraic.jl
@@ -0,0 +1,45 @@
+"""
+This module contains facilities for working with *algebraic* theories, i.e.
+theories where none of the type constructors have arguments.
+
+Type inference and checking are much easier for such theories.
+"""
+
+using ...Syntax
+
+"""
+Returns whether a theory is algebraic
+"""
+function is_algebraic(theory::Theory)::Bool
+  for j in theory.judgments
+    if j.head isa TypCon
+      length(j.head.args) == 0 || return false
+    end
+  end
+  true
+end
+
+"""
+Infer the typ of a trm in an algebraic theory and context.
+
+Throw an error if type cannot be inferred.
+"""
+function typ_infer(theory::Theory, t::Trm; context::Context = Context())
+  if iscontext(t.head)
+    context.ctx[index(t.head)][2]
+  else
+    j = theory.judgments[index(t.head)]
+    j.head isa TrmCon || error("head of $t must be a term constructor")
+    args = t.args
+    length(args) == length(j.head.args) ||
+      error("wrong number of args for top-level term constructor in $t")
+    argtyps = map(args) do arg
+      typ_infer(theory, args; context)
+    end
+    expected_argtyps = Typ[j.ctx[i][2] for i in j.head.args]
+    argtyps == expected_argtyps ||
+      error("arguments to $t are wrong type: expected $expected_argtyps, got $argtyps")
+    j.head.typ
+  end
+end
+
diff --git a/src/syntax/egraphs/east.jl b/src/syntax/egraphs/east.jl
new file mode 100644
index 00000000..b35ba676
--- /dev/null
+++ b/src/syntax/egraphs/east.jl
@@ -0,0 +1,308 @@
+using MLStyle
+using DataStructures
+using StructEquality
+
+using ..Scopes
+using ..GATs
+using ..ExprInterop
+
+"""
+An index into the union-find data structure component of an E-graph. Each
+e-class is associated to a set of EIds, including a canonical one. This set is
+stored by the union-find.
+"""
+const EId = Int # TODO make a struct which subtypes integer or roll out our own IntDisjointSets
+
+"""
+An EType is in the context of a GAT, which the `head` of the `MethodApp` refers
+to. For each parameter there is an e-term.
+"""
+@struct_hash_equal struct EType
+  body::MethodApp{EId}
+end
+
+EType(a::Ident,b::Ident,c::Vector{EId}) = EType(MethodApp(a,b,c))
+
+@struct_hash_equal struct EConstant 
+  value::Any
+  type::EType
+end
+
+"""
+ETerms in are interpreted in a Presentation. In the case of a MethodApp, the 
+head/method refer to term constructors or accessors of the theory.
+"""
+@struct_hash_equal struct ETerm
+  body::Union{Ident, MethodApp{EId}, EConstant}
+end
+
+ETerm(a::Ident,b::Ident,c::Vector{EId}) = ETerm(MethodApp(a,b,c))
+
+const Parents = Dict{ETerm, EId}
+
+"""
+`reps` A representation of an equivalence class of e-terms. 
+`parents` caches all the e IDs which directly refer to a given term (as opposed 
+to some reference in a nested term)
+"""
+mutable struct EClass
+  reps::Set{ETerm}
+  type::EType
+  parents::Parents
+  function EClass(reps::Set{ETerm}, type::EType, parents::Parents=Parents())
+    new(reps, type, parents)
+  end
+end
+
+function add_parent!(ec::EClass, etrm::ETerm, i::EId)
+  ec.parents[etrm] = i
+end
+
+
+"""
+Stores a congruent partial equivalence relation on terms in the context of
+`presentation`
+"""
+struct EGraph
+  presentation::Presentation
+  eqrel::IntDisjointSets{EId}
+  eclasses::Dict{EId, EClass}
+  hashcons::Dict{ETerm, EId}
+  worklist::Vector{EId}
+  isclean::Ref{Bool}
+  function EGraph(pres::Presentation)
+    new(pres, IntDisjointSets{EId}(0), Dict{EId, EClass}(), Dict{ETerm, EId}(), EId[], Ref(true))
+  end
+end
+
+EGraph(T::GAT) = EGraph(Presentation(T)) # Theory without any further context
+
+"""
+Update e-term to refer to canonical e-ids
+"""
+function canonicalize!(eg::EGraph, etrm::ETerm)
+  (@match etrm.body begin
+    x::Union{Constant, Ident} => x
+    MethodApp(head, method, args) =>
+      MethodApp{EId}(head, method, find_root!.(Ref(eg.eqrel), args))
+  end) |> ETerm
+end
+
+function etypeof(eg::EGraph, i::EId)
+  eg.eclasses[i].type
+end
+
+"""
+This computes the inferred context for an etrm.
+
+For example, if `f` is an id with etyp `Hom(x,y)` and `g` is an id with etyp
+`Hom(y,z)`, then context(eg, :(g ∘ f)) computes the context `[x,y,z,f,g]`.
+
+The tricky thing comes from term formers like
+
+weaken(x)::Term(n) ⊣ [n::Nat, x::Term(S(n))]
+
+We get the ETyp for x from the e-graph, and then we have to ematch its argument
+with `S(n)` to figure out what `n` is... The problem is that in general `S` will
+not be injective, so this is ambiguous!
+
+What we are going to do for now is say that types in the context of a term former
+can't be nested. I.e., we only allow types of the form `Term(n)`, not `Term(S(n))`.
+
+Fortunately, I don't think we care about any theories with this kind of context
+former.
+
+To fix this issue, you should instead declare term constructors like
+
+```
+weaken(n, x)::Term(n) ⊣ [n::Nat, x::Term(S(n))]
+```
+"""
+function econtext(eg::EGraph, m::MethodApp{EId})
+  termcon = getvalue(eg.presentation[m.method])
+  typeof(termcon) == AlgTermConstructor ||
+    error("head of $etrm is not a term constructor")
+  length(m.args) == length(termcon.args) ||
+    error("wrong number of args for term constructor in $etrm")
+  ectx = zeros(EId, length(termcon.localcontext)) 
+  # initialize result with top-level arguments
+  toexpand = Tuple{AlgType, EType}[]
+  for (lid, eid) in zip(termcon.args, m.args)
+    ectx[lid.val] = eid
+    push!(toexpand, (getvalue(termcon[lid]), etypeof(eg, eid)))
+  end
+  while !isempty(toexpand)
+    (algtype, etype) = pop!(toexpand)
+    for (arg, id) in zip(algtype.body.args, etype.body.args)
+      id = find_root!(eg.eqrel, id)
+      @match arg.body begin
+        _::Constant => nothing
+        x::Ident => begin
+          i = getlid(x).val
+          if ectx[i] != 0
+            ectx[i] == id ||
+              error("contradictory inference of context for $m; could not unify $(ectx[i]) and $id")
+          else
+            ectx[i] = id
+          end
+          push!(toexpand, (getvalue(termcon[x]), etypeof(eg, id)))
+        end
+        _::MethodApp => error("we don't do that kind of thing over here")
+      end
+    end
+  end
+  all(!=(0), ectx) || error("could not fully infer context")
+  ectx
+end
+
+function compute_etype(eg::EGraph, eterm::ETerm)::EType
+  @match eterm.body begin
+    x::Ident => begin
+      algtype = getvalue(eg.presentation[x]).body
+      EType(algtype.head, algtype.method, add!.(Ref(eg), argsof(algtype)))
+    end
+    c::EConstant => c.type
+    m::MethodApp{EId} => begin
+      ectx = econtext(eg, m)
+      termcon = getvalue(eg.presentation[m.method])
+      type_body = termcon.type.body
+      EType(
+        type_body.head,
+        type_body.method,
+        EId[subst!(eg, arg, ectx, gettag(termcon.localcontext)) for arg in type_body.args]
+      )
+    end
+  end
+end
+
+"""
+Returns the `EId` corresponding to the term resulting from the substitution
+in `term` of the idents in the scope refered to by `tag` according to the
+values in `ectx`
+
+Note: this is similar logic to `add!`: perhaps combine the two by making `ectx`
+and `tag` optional?
+"""
+function subst!(eg::EGraph, term::AlgTerm, ectx::Vector{EId}, tag::ScopeTag)
+  @match term.body begin
+    x::Ident && if gettag(x) == tag end => ectx[getlid(x).val]
+    c::Union{Constant, Ident} => add!(eg, c)
+    m::MethodApp => begin
+      args = EId[subst!(eg, arg, ectx, tag) for arg in trm.args]
+      add!(eg, ETerm(m.head, m.method, args))
+    end
+  end
+end
+
+"""
+Add eterm to an egraph.
+"""
+function add!(eg::EGraph, eterm::ETerm)
+  eterm = canonicalize!(eg, eterm)
+  if haskey(eg.hashcons, eterm)
+    eg.hashcons[eterm]
+  else
+    etype = compute_etype(eg, eterm)
+    id = push!(eg.eqrel)
+    if eterm.body isa MethodApp
+      for argid in eterm.body.args
+        add_parent!(eg.eclasses[argid], eterm, id)
+      end
+    end
+    eg.hashcons[eterm] = id
+    eg.eclasses[id] = EClass(Set([eterm]), etype)
+    id
+  end
+end
+
+function add!(eg::EGraph, term::AlgTerm)
+  @match term.body begin
+    x::Ident => add!(eg, ETerm(x))
+    c::Constant => begin
+      tb = c.type.body
+      ec = EConstant(c.value, EType(tb.head, tb.method, add!.(Ref(eg), tb.args)))
+      add!(eg, ETerm(ec))
+    end
+    m::MethodApp => add!(eg, ETerm(m.head, m.method, add!.(Ref(eg), m.args)))
+  end
+end
+
+function add!(eg::EGraph, term::Union{Expr, Symbol})
+  add!(eg, fromexpr(eg.presentation, term, AlgTerm))
+end
+
+find!(eg::EGraph, i::EId) = find_root!(eg.eqrel, i)
+
+"""
+Merge the eclasses associated with two eIDs. 
+"""
+function Base.merge!(eg::EGraph, id1::EId, id2::EId)
+  eg.isclean[] = false
+  id1, id2 = find!.(Ref(eg), (id1, id2))
+  if id1 == id2
+    return id1
+  end
+
+  id = union!(eg.eqrel, id1, id2)
+  id1, id2 = (id == id1) ? (id2, id1) : (id1, id2)
+  push!(eg.worklist, id)
+  ec1 = eg.eclasses[id1]
+  ec2 = eg.eclasses[id2]
+  union!(ec2.reps, ec1.reps)
+  merge!(ec2.parents, ec1.parents)
+  delete!(eg.eclasses, id1)
+  id
+end
+
+"""
+Reinforces the e-graph invariants (i.e., ensures that the equivalence relation
+is congruent).
+"""
+function rebuild!(eg::EGraph)
+  while !isempty(eg.worklist)
+    todo = [ find!(eg, i) for i in eg.worklist ]
+    empty!(eg.worklist)
+    for i in todo
+      repair!(eg, i)
+    end
+  end
+  eg.isclean[] = true
+end
+
+function repair!(eg::EGraph, i::EId)
+  for (p_etrm, _) in eg.eclasses[i].parents
+    delete!(eg.hashcons, p_etrm)
+    p_etrm = canonicalize!(eg, p_etrm)
+    eg.hashcons[p_etrm] = find!(eg, i)
+  end
+
+  new_parents = Parents()
+
+  for (p_etrm, p_eclass) in eg.eclasses[i].parents
+    p_etrm = canonicalize(eg, p_etrm)
+    if p_etrm ∈ keys(new_parents)
+      merge!(eg, p_eclass, new_parents[p_etrm])
+    end
+    new_parents[p_etrm] = find!(eg, p_eclass)
+  end
+
+  eg.eclasses[i].parents = new_parents
+end
+
+# Extraction
+function extract(eg::EGraph, t::EType; chooser=only)::AlgType
+  body = t.body
+  AlgType(body.head, body.method, extract.(Ref(eg), body.args; chooser))
+end
+
+function extract(eg::EGraph, t::ETerm; chooser=only)::AlgTerm
+  @match t.body begin 
+    x::Ident => AlgTerm(x)
+    c::EConstant => Constant(c.value, extract(eg, c.type; chooser))
+    m::MethodApp => AlgTerm(m.head, m.method, extract.(Ref(eg), m.args; chooser))
+  end
+end
+
+function extract(eg::EGraph, id::EId; chooser=only)::AlgTerm
+  extract(eg, chooser(eg.eclasses[id].reps))
+end
\ No newline at end of file
diff --git a/src/syntax/egraphs/ematching.jl b/src/syntax/egraphs/ematching.jl
new file mode 100644
index 00000000..68b4bd57
--- /dev/null
+++ b/src/syntax/egraphs/ematching.jl
@@ -0,0 +1,327 @@
+# EMatching is the hard part of EGraphs
+#
+# Here we follow a strategy similar to egg, but modified somewhat for our uses.
+#
+# We take a pattern, which is a Trm in a Context, and we attempt to find an
+# assignment of an enode to each term in the context.
+#
+# For instance, we might look for the term `(a * b) * c` in the context
+# `[a,b,c::U]` or for the term `f ∘ id(a)` in the context
+# `[a,b::Ob,f::Hom(a,b)]`.
+#
+# Note that not all variables in the context are referenced directly in the
+# term; i.e. `b` is never referenced. Thus, ematching must take into account both
+# terms and types.
+
+using ..EGraphs
+using ...Syntax
+
+using MLStyle
+
+struct Reg
+  idx::Int
+end
+
+@as_record Reg
+
+Base.:+(r::Reg, i::Int) = Reg(r.idx + i)
+
+struct Machine
+  reg::Vector{Id}
+  lookup::Vector{Id}
+  matches::Vector{Vector{Id}}
+  limit::Union{Some{Int}, Nothing}
+  function Machine(;limit=nothing)
+    new(Id[], Id[], Vector{Id}[], limit)
+  end
+end
+
+Base.getindex(m::Machine, r::Reg) = m.reg[r.idx]
+
+Base.setindex!(m::Machine, r::Reg, i::Id) = (m.reg[r.idx] = i)
+
+struct FinishedMatching <: Exception
+end
+
+function submit_match!(m::Machine, subst::Vector{Reg})
+  match = Id[m[r] for r in subst]
+  push!(m.matches, match)
+  if !isnothing(m.limit) && length(m.matches) >= m.limit.value
+    throw(FinishedMatching())
+  end
+end
+
+@data Instruction begin
+  # Iterate through all of the terms in the eclass bound to `i` that have term
+  # constructor `trmcon`.
+  #
+  # For each term, assign the registers past `out` to the arguments of that term,
+  # and run the rest of the instructions.
+  Bind(trmcon::Lvl, i::Reg, out::Reg)
+
+  # Check if the eclass bound to `i` is the same as the eclass bound to `j`
+  Compare(i::Reg, j::Reg)
+
+  # Each element of `term` is either a register or an ETrm where the ids
+  # refer to earlier elements of `term`. Fill out a lookup vector of ids the same
+  # length as `term` by:
+  # - For each Reg, just look up the id in the EGraph
+  # - For each ETrm, look up its arguments in the lookup vector, and then lookup
+  # the completed ETrm in the EGraph
+  #
+  # At the end, put the last id in the lookup vector into `reg`.
+  Lookup(term::Vector{Union{Reg, ETrm}}, reg::Reg)
+
+  # Iterate through every eclass in the egraph.
+  #
+  # For each eclass, assign its id to `out`, truncate the list of registers,
+  # and run the rest of the instructions.
+  #
+  # Note: we can probably get better performance by only iterating through eclasses
+  # with a certain ETyp, or that come from a certain constructor.
+  Scan(out::Reg)
+end
+
+struct Program
+  instructions::Vector{Instruction}
+  subst::Vector{Reg}
+end
+
+run!(m::Machine, eg::EGraph, prog::Program) = run!(m, eg, prog.instructions, prog.subst)
+
+function run!(m::Machine, eg::EGraph, instructions::AbstractVector{Instruction}, subst::Vector{Reg})
+  for idx in eachindex(instructions)
+    @match instructions[idx] begin
+      Bind(trmcon, i, out) => begin
+        eclass = eg.eclasses[find!(eg, m[i])]
+        remaining = @view instructions[idx+1:end]
+        for etrm in eclass.reps
+          if etrm.head != trmcon
+            continue
+          end
+          resize!(m.reg, out.idx - 1)
+          append!(m.reg, etrm.args)
+          run!(m, eg, remaining, subst)
+        end
+        return
+      end
+      Compare(i, j) => begin
+        if find!(eg, m[i]) != find!(eg, m[j])
+          return
+        end
+      end
+      Lookup(term, reg) => begin
+        empty!(m.lookup)
+        for x in trm
+          @match x begin
+            Reg(_) => push!(m.lookup, find!(eg, m[x]))
+            ETrm(head, args) => begin
+              etrm = ETrm(head, Id[m.lookup[i] for i in args])
+              @match get(eg.hashcons, etrm, nothing) begin
+                nothing => return
+                id => push!(m.lookup, id)
+              end
+            end
+          end
+        end
+        if lookup[end] != find!(eg, m[reg])
+          return
+        end
+      end
+      Scan(out) => begin
+        remaining = @view instructions[idx+1:end]
+        for (id, eclass) in eg.eclasses
+          resize!(m.reg, out.idx - 1)
+          push!(m.reg, id)
+          run!(m, eg, remaining, subst)
+        end
+        return
+      end
+    end
+  end
+  submit_match!(m, subst)
+end
+
+struct Compiler
+  v2r::Dict{Lvl, Reg}
+  free_vars::Vector{Set{Lvl}}
+  subtree_size::Vector{Int}
+  todo_nodes::Dict{Tuple{Int, Reg}, ETrm}
+  instructions::Vector{Instruction}
+  next_reg::Reg
+  theory::Theory
+  function Compiler(theory::Theory)
+    new(
+      Dict{Lvl, Reg}(),
+      Set{Lvl}[],
+      Int[],
+      Dict{Tuple{Int, Reg}, ETrm}(),
+      Instruction[],
+      Reg(1),
+      theory
+    )
+  end
+end
+
+struct Pattern
+  trm::Trm
+  ctx::Context
+end
+
+function trm_to_vec!(trm::Trm, vec::Vector{ETrm})
+  ids = Vector{Id}(trm_to_vec!.(trm.args, Ref(vec)))
+  push!(vec, ETrm(trm.head, ids))
+  length(vec)
+end
+
+function vec_to_trm(vec::Vector{ETrm}, id::Id)
+  etrm = vec[id]
+  args = Vector{Trm}(vec_to_term(Ref(vec), etrm.args))
+  Trm(etrm.head, args)
+end
+
+function load_pattern!(c::Compiler, patvec::Vector{ETrm})
+  n = length(patvec)
+
+  for etrm in patvec
+    free = Set{Lvl}()
+    size = 0
+    hd = etrm.head
+    if is_context(hd)
+      push!(free, hd)
+    else
+      size = 1
+      for arg in etrm.args
+        union!(free, c.free_vars[arg])
+        size += c.subtree_size[arg]
+      end
+    end
+    push!(c.free_vars, free)
+    push!(c.subtree_size, size)
+  end
+end
+
+
+function add_todo!(c::Compiler, patvec::Vector{ETrm}, id::Id, reg::Reg)
+  etrm = patvec[id]
+  hd = etrm.head
+  if is_context(hd)
+    @match get(c.v2r, hd, nothing) begin
+      nothing => (c.v2r[hd] = reg)
+      j => push!(c.instructions, Compare(reg, j))
+    end
+  else
+    c.todo_nodes[(id, reg)] = etrm
+  end
+end
+
+# return an element x of xs such that f(x) is maximal
+function maxby(f, xs)
+  if isempty(xs)
+    return nothing
+  end
+  next = iterate(xs)
+  maxfound, state = next
+  maxval = f(maxfound)
+  while true
+    next = iterate(xs, state)
+    if !isnothing(next)
+      x, state = next
+      fx = f(x)
+      if fx > maxval
+        maxfound, maxval = x, fx
+      end
+    else
+      break
+    end
+  end
+  maxfound
+end
+
+# We take the max todo according to this key
+# - prefer zero free variables
+# - prefer more free variables
+# - prefer smaller
+#
+# Free variables here means variables that are
+# free in the term that have not been bound yet
+# in c.v2r
+#
+# Why? Idk, this is how it works in egg
+function next!(c::Compiler)
+  function key(idreg::Tuple{Id, Reg})
+    id = idreg[1]
+    n_bound = length(filter(v -> v in keys(c.v2r), c.free_vars[id]))
+    n_free = length(c.free_vars[id]) - n_bound
+    (n_free == 0, n_free, -c.subtree_size[id])
+  end
+
+  k = maxby(key, keys(c.todo_nodes))
+  if isnothing(k)
+    return nothing
+  end
+  v = c.todo_nodes[k]
+  delete!(c.todo_nodes, k)
+  (k,v)
+end
+
+is_ground_now(c::Compiler, id::Id) = all(v ∈ keys(c.v2r) for v in c.free_vars[id])
+
+function extract(patvec::Vector{ETrm}, i::Id)
+  trm = vec_to_trm(patvec, i)
+  vec = ETrm[]
+  trm_to_vec!(trm, vec)
+  vec
+end
+
+# Returns a Program
+function compile(T::Type{<:AbstractTheory}, pat::Pattern)
+  patvec = ETrm[]
+  trm_to_vec!(pat.trm, patvec)
+
+  c = Compiler(gettheory(T))
+
+  load_pattern!(c, patvec)
+
+  next_out = c.next_reg
+
+  add_todo!(c, patvec, length(patvec), next_out)
+
+  while true
+    @match next!(c) begin
+      nothing => break
+      ((id, reg), etrm) => begin
+        if is_ground_now(c, id) && (length(etrm.args) != 0)
+          extracted = extract(patvec, id)
+          push!(
+            c.instructions,
+            Lookup(
+              Union{ETrm, Reg}[is_context(t.head) ? c.v2r[t.head] : t for t in extracted],
+              reg
+            )
+          )
+        else
+          out = next_out
+          next_out += length(etrm.args)
+          push!(
+            c.instructions,
+            Bind(
+              etrm.head,
+              reg,
+              out + 1
+            )
+          )
+          for (i, child) in enumerate(etrm.args)
+            add_todo!(c, patvec, child, out + i)
+          end
+        end
+      end
+    end
+  end
+
+  # for testing, return the compiler
+  Program(
+    c.instructions,
+    Reg[r for (v,r) in sort([c.v2r...]; by=vr -> index(vr[1]))]
+  )
+end
diff --git a/src/syntax/egraphs/eqsat.jl b/src/syntax/egraphs/eqsat.jl
new file mode 100644
index 00000000..e2ed2c86
--- /dev/null
+++ b/src/syntax/egraphs/eqsat.jl
@@ -0,0 +1,9 @@
+
+"""
+Equality Saturation
+
+We want to be able to do the following
+
+rules = Rules(ThCategory, [(:assoc, :<=>), (:idr, :=>), (:idl, :=>)])
+
+"""
\ No newline at end of file
diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl
index 94796d15..a0543327 100644
--- a/src/syntax/gats/ast.jl
+++ b/src/syntax/gats/ast.jl
@@ -22,6 +22,8 @@ in fact be `AlgTerm`.
   args::Vector{T}
 end
 
+@as_record MethodApp
+
 headof(t::MethodApp) = t.head
 methodof(t::MethodApp) = t.method
 argsof(t::MethodApp) = t.args
diff --git a/src/syntax/module.jl b/src/syntax/module.jl
index b5ee07a3..2e836932 100644
--- a/src/syntax/module.jl
+++ b/src/syntax/module.jl
@@ -8,6 +8,7 @@ include("GATs.jl")
 include("Presentations.jl")
 include("TheoryInterface.jl")
 include("TheoryMaps.jl")
+include("EGraphs.jl")
 
 @reexport using .Scopes
 @reexport using .ExprInterop
@@ -15,5 +16,6 @@ include("TheoryMaps.jl")
 @reexport using .Presentations
 @reexport using .TheoryInterface
 @reexport using .TheoryMaps
+@reexport using .EGraphs
 
 end
diff --git a/test/syntax/EGraphs.jl b/test/syntax/EGraphs.jl
new file mode 100644
index 00000000..731f0419
--- /dev/null
+++ b/test/syntax/EGraphs.jl
@@ -0,0 +1,81 @@
+module TestEGraphs
+
+using Test
+
+using GATlab
+
+@present P(ThMonoid) begin
+  (a,b,c)
+end
+
+eg = EGraph(P)
+
+i1 = add!(eg, :(a ⋅ b))
+i2 = add!(eg, :c)
+merge!(eg, i1, i2)
+rebuild!(eg)
+i3 = add!(eg, :(c ⋅ c))
+i4 = add!(eg, :(c ⋅ (a ⋅ b)))
+
+@test i3 == i4
+
+@present C(ThCategory) begin
+  (x,y,z) :: Ob
+  f :: Hom(x,y)
+  g :: Hom(y,z)
+end
+
+eg = EGraph(C)
+
+i1 = add!(eg, :(f ⋅ g))
+
+EGraphs.etypeof(eg, i1)
+
+EGraphs.extract(eg, EGraphs.etypeof(eg, i1); chooser=first)
+
+@test_throws Exception add!(eg, :(g ⋅ f))
+
+merge!(eg, add!(eg, :x), add!(eg, :z))
+
+i2 = add!(eg, :(g ⋅ f))
+
+# # E Matching
+# ############
+
+# @theory C <: ThCategory begin
+#   x::Ob
+#   y::Ob
+#   z::Ob
+#   f::Hom(x,y)
+#   g::Hom(x,x)
+#   h::Hom(y,y)
+# end
+
+# eg = EGraph(C.T)
+
+# id = add!(eg, @term C (f ⋅ id(y)))
+
+# compose_lvl = (@term C (f ⋅ h)).head
+# id_lvl = (@term C id(x)).head
+
+# instructions = [Scan(Reg(1)), Bind(compose_lvl, Reg(1), Reg(2)), Bind(id_lvl, Reg(3), Reg(4))]
+
+# m = Machine()
+
+# run!(m, eg, instructions, [Reg(4), Reg(2)])
+
+# @test m.matches[1] == [add!(eg, @term C y), add!(eg, @term C f)]
+
+# Γ = @context ThCategory [a::Ob, b::Ob, α::Hom(a,b)]
+# t = @term ThCategory Γ (α ⋅ id(b))
+# pat = Pattern(t, Γ)
+# prog = compile(ThCategory.T, pat)
+
+# m = Machine()
+
+# push!(m.reg, id)
+# run!(m, eg, prog)
+
+# @test m.matches[1] == [add!(eg, @term C y), add!(eg, @term C f)]
+
+end # module