diff --git a/src/Language/Bergamot/Rules.purs b/src/Language/Bergamot/Rules.purs
new file mode 100644
index 0000000..de5b087
--- /dev/null
+++ b/src/Language/Bergamot/Rules.purs
@@ -0,0 +1,42 @@
+module Language.Bergamot.Rules where
+
+import Prelude
+
+import Language.Bergamot.Syntax (Expr)
+
+import Control.Monad.State.Trans (runStateT)
+import Control.Monad.State.Class (class MonadState, gets, modify)
+import Control.Monad.Unify.Class (class MonadUnify, fresh)
+import Data.List (List)
+import Data.Traversable (class Traversable, traverse)
+import Data.Foldable (class Foldable)
+import Data.Map (Map, lookup, insert)
+import Data.Map as Map
+import Data.Tuple (fst)
+import Data.Newtype (class Newtype)
+import Data.Maybe (Maybe(..))
+
+newtype Rule k = MkRule { name :: String, head :: Expr k, tail :: List (Expr k) }
+derive instance Newtype (Rule k) _
+derive instance Functor Rule
+derive instance Foldable Rule
+derive instance Traversable Rule
+
+type Metavariable = String
+type Metavariables k = Map Metavariable k
+
+newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree k) }
+
+metavariable :: forall k f m. MonadState (Metavariables k) m => MonadUnify k f m => Metavariable -> m k
+metavariable s = do
+    r <- gets (lookup s)
+    case r of
+        Just v -> pure v
+        Nothing -> do
+           v <- fresh
+           modify (insert s v) *> pure v
+
+-- note: unification expression ef not the same as functor-to-instantiate f, this way we can instantiate
+-- things that contain expression etc.
+instantiate :: forall k f ef m. Traversable f => MonadUnify k ef m => f Metavariable -> m (f k)
+instantiate f = map fst $ runStateT (traverse metavariable f) Map.empty
diff --git a/src/Language/Bergamot/Syntax.purs b/src/Language/Bergamot/Syntax.purs
index 91030ce..b701f1c 100644
--- a/src/Language/Bergamot/Syntax.purs
+++ b/src/Language/Bergamot/Syntax.purs
@@ -2,39 +2,11 @@ module Language.Bergamot.Syntax where
 
 import Prelude
 
-import Control.Plus (class Plus, empty)
-import Control.Monad (class Monad)
-import Control.Monad.State.Trans (StateT, runStateT)
-import Control.Monad.State.Class (class MonadState, gets, modify)
-import Control.Apply (class Apply, apply, lift2)
-import Control.Alt (class Alt, alt)
-import Control.Alternative (class Alternative)
-import Control.Applicative (class Applicative, pure, (*>))
-import Control.Bind (class Bind, bind, join, (>>=))
-import Control.MonadPlus (class MonadPlus)
-import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask, asks)
-import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
-import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..), fresh, unify, reify)
-import Control.Monad.Reader.Trans (ReaderT, runReaderT)
-import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
-import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce)
-import Control.Monad.State.Trans (StateT(..), runStateT)
-import Data.List (List(..), (:), fromFoldable)
-import Data.Functor (class Functor, (<$>), map)
-import Data.Eq (class Eq)
-import Data.Ord (class Ord)
-import Data.Traversable (class Traversable, sequence, traverse, oneOf)
-import Data.Foldable (class Foldable, foldr, foldl, foldMap, any, intercalate)
-import Data.Monoid ((<>), mempty)
-import Data.Map (Map, lookup, insert)
-import Data.Map as Map
-import Data.Set (Set, singleton, union)
-import Data.Tuple (Tuple(..), fst)
-import Data.Tuple.Nested ((/\))
-import Data.Lazy (Lazy, defer, force)
-import Data.Newtype (class Newtype, un, over2)
-import Data.Maybe (Maybe(..), fromMaybe, isJust)
-import Data.Bifunctor (rmap)
+import Control.Monad.Unify.Class (class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..))
+import Data.Foldable (class Foldable)
+import Data.Traversable (class Traversable)
+import Data.Lazy (defer)
+import Data.List (List(..), (:))
 
 data Expr v
     = Var v
@@ -67,83 +39,3 @@ instance UnificationVariable k => Unifiable k Expr where
           combine (_:_) Nil = (Var Fail) : Nil
           combine Nil (_:_) = (Var Fail) : Nil
           combine (x:xs) (y:ys) = alongside x y : combine xs ys
-
--- note: unification expression ef not the same as functor-to-instantiate f, this way we can instantiate
--- things that contain expression etc.
-instantiate :: forall k f ef m. Traversable f => MonadUnify k ef m => f Metavariable -> m (f k)
-instantiate f = map fst $ runStateT (traverse metavariable f) Map.empty
-
-newtype Rule k = MkRule { name :: String, head :: Expr k, tail :: List (Expr k) }
-derive instance Newtype (Rule k) _
-derive instance Functor Rule
-derive instance Foldable Rule
-derive instance Traversable Rule
-
-type UnifierEnv = { rules :: Array (Rule Metavariable), fuel :: Int }
-newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT UnifierEnv (SFKT Maybe)) a)
-
-derive instance Newtype (Unifier a) _
-derive newtype instance Functor Unifier
-derive newtype instance Apply Unifier
-derive newtype instance Applicative Unifier
-derive newtype instance Alt Unifier
-derive newtype instance Plus Unifier
-derive newtype instance Alternative Unifier
-derive newtype instance Bind Unifier
-derive newtype instance Monad Unifier
-derive newtype instance MonadPlus Unifier
-derive newtype instance MonadUnify IntVar Expr Unifier
-
--- >:(
-instance MonadAsk UnifierEnv Unifier where
-    ask = MkUnifier $ MkUnifyT ask
-
--- >:(
-instance MonadReader UnifierEnv Unifier where
-    local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
-
--- >:(
-instance MonadLogic Unifier where
-    msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
-    interleave = over2 MkUnifier (over2 MkUnifyT interleave)
-
-spend :: forall a. Unifier a -> Unifier a
-spend m = do
-    n <- asks _.fuel
-    if n > 0 then local (_ { fuel = n - 1}) m else empty
-
-type Metavariable = String
-type Metavariables k = Map Metavariable k
-
-metavariable :: forall k f m. MonadState (Metavariables k) m => MonadUnify k f m => Metavariable -> m k
-metavariable s = do
-    r <- gets (lookup s)
-    case r of
-        Just v -> pure v
-        Nothing -> do
-           v <- fresh
-           modify (insert s v) *> pure v
-
-
-newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree k) }
-
-match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
-match rs e = oneOf $ map (matchSingle e) rs
-    where
-      matchSingle e' rule = spend $ do
-         MkRule {head, tail} <- instantiate rule
-         _ <- unify e' head
-         witnesses <- traverse (match rs) tail
-         pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses }
-
-reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
-reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
-    claim' <- reify claim
-    witnesses' <- traverse reifyProofTree witnesses
-    pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
-
-query :: Expr Metavariable -> Unifier (ProofTree IntVar)
-query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
-
-runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
-runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))
diff --git a/src/Language/Bergamot/Unifier.purs b/src/Language/Bergamot/Unifier.purs
new file mode 100644
index 0000000..c0112f2
--- /dev/null
+++ b/src/Language/Bergamot/Unifier.purs
@@ -0,0 +1,78 @@
+module Language.Bergamot.Unifier where
+
+import Prelude
+
+import Language.Bergamot.Rules (Metavariable, ProofTree(..), Rule(..), instantiate)
+import Language.Bergamot.Syntax (Expr, IntVar)
+
+import Control.Plus (class Plus, empty)
+import Control.Apply (lift2)
+import Control.Alt (class Alt)
+import Control.Alternative (class Alternative)
+import Control.MonadPlus (class MonadPlus)
+import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask, asks)
+import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
+import Control.Monad.Unify.Class (class MonadUnify, unify, reify)
+import Control.Monad.Reader.Trans (ReaderT, runReaderT)
+import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
+import Control.Monad.Logic.Trans (SFKT, runSFKTOnce)
+import Control.Monad.State.Trans (StateT(..), runStateT)
+import Data.Traversable (traverse, oneOf)
+import Data.Tuple (fst)
+import Data.Newtype (class Newtype, un, over2)
+import Data.Maybe (Maybe)
+import Data.Bifunctor (rmap)
+
+type UnifierEnv = { rules :: Array (Rule Metavariable), fuel :: Int }
+newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT UnifierEnv (SFKT Maybe)) a)
+
+derive instance Newtype (Unifier a) _
+derive newtype instance Functor Unifier
+derive newtype instance Apply Unifier
+derive newtype instance Applicative Unifier
+derive newtype instance Alt Unifier
+derive newtype instance Plus Unifier
+derive newtype instance Alternative Unifier
+derive newtype instance Bind Unifier
+derive newtype instance Monad Unifier
+derive newtype instance MonadPlus Unifier
+derive newtype instance MonadUnify IntVar Expr Unifier
+
+-- >:(
+instance MonadAsk UnifierEnv Unifier where
+    ask = MkUnifier $ MkUnifyT ask
+
+-- >:(
+instance MonadReader UnifierEnv Unifier where
+    local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
+
+-- >:(
+instance MonadLogic Unifier where
+    msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
+    interleave = over2 MkUnifier (over2 MkUnifyT interleave)
+
+spend :: forall a. Unifier a -> Unifier a
+spend m = do
+    n <- asks _.fuel
+    if n > 0 then local (_ { fuel = n - 1}) m else empty
+
+match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
+match rs e = oneOf $ map (matchSingle e) rs
+    where
+      matchSingle e' rule = spend $ do
+         MkRule {head, tail} <- instantiate rule
+         _ <- unify e' head
+         witnesses <- traverse (match rs) tail
+         pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses }
+
+reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
+reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
+    claim' <- reify claim
+    witnesses' <- traverse reifyProofTree witnesses
+    pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
+
+query :: Expr Metavariable -> Unifier (ProofTree IntVar)
+query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
+
+runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
+runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))
diff --git a/test/Main.purs b/test/Main.purs
index db781a9..b208b33 100644
--- a/test/Main.purs
+++ b/test/Main.purs
@@ -2,6 +2,8 @@ module Test.Main where
 
 import Prelude
 import Language.Bergamot.Syntax
+import Language.Bergamot.Rules
+import Language.Bergamot.Unifier
 import Control.Monad.Logic.Trans
 import Control.Monad.Logic.Class
 import Control.Monad.Unify.Trans