diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..210965c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+.stack-work/
+*~
+client_session_key.aes
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..dfba359
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,18 @@
+Copyright (c) 2020 Garmelon
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software is furnished to do so,
+subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
index 639ea87..1b90f35 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,4 @@
-# props
+# propa-tools
 
-Propa tools
+Various programming paradigm related bits and bobs. May not contain any actual
+executables.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
index 0000000..f7090c2
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,4 @@
+module Main where
+
+main :: IO ()
+main = putStrLn "Hello world!"
diff --git a/package.yaml b/package.yaml
new file mode 100644
index 0000000..ea4d11c
--- /dev/null
+++ b/package.yaml
@@ -0,0 +1,34 @@
+name: propa-tools
+version: 0.1.0.0
+license: MIT
+author: Garmelon <joscha@plugh.de>
+copyright: 2020 Garmelon
+
+extra-source-files:
+- README.md
+- LICENSE
+
+extra-doc-files:
+- README.md
+
+dependencies:
+- base >= 4.7 && < 5
+- containers
+- megaparsec
+- parser-combinators
+- text
+- transformers
+
+library:
+  source-dirs: src
+
+executables:
+  propa-tools-exe:
+    main: Main.hs
+    source-dirs: app
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - propa-tools
diff --git a/propa-tools.cabal b/propa-tools.cabal
new file mode 100644
index 0000000..8a5af23
--- /dev/null
+++ b/propa-tools.cabal
@@ -0,0 +1,58 @@
+cabal-version: 1.18
+
+-- This file has been generated from package.yaml by hpack version 0.34.2.
+--
+-- see: https://github.com/sol/hpack
+
+name:           propa-tools
+version:        0.1.0.0
+author:         Garmelon <joscha@plugh.de>
+maintainer:     Garmelon <joscha@plugh.de>
+copyright:      2020 Garmelon
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    LICENSE
+extra-doc-files:
+    README.md
+
+library
+  exposed-modules:
+      Propa.Lambda.Display
+      Propa.Lambda.Term
+      Propa.Prolog.Debug
+      Propa.Prolog.Display
+      Propa.Prolog.Parse
+      Propa.Prolog.Types
+      Propa.Prolog.Unify
+  other-modules:
+      Paths_propa_tools
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , megaparsec
+    , parser-combinators
+    , text
+    , transformers
+  default-language: Haskell2010
+
+executable propa-tools-exe
+  main-is: Main.hs
+  other-modules:
+      Paths_propa_tools
+  hs-source-dirs:
+      app
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , megaparsec
+    , parser-combinators
+    , propa-tools
+    , text
+    , transformers
+  default-language: Haskell2010
diff --git a/src/Propa/Lambda/Display.hs b/src/Propa/Lambda/Display.hs
new file mode 100644
index 0000000..22cca89
--- /dev/null
+++ b/src/Propa/Lambda/Display.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | This module contains functions useful for displaying 'Term's.
+
+module Propa.Lambda.Display
+  ( Name
+  , findConstNames
+  , makeVarNamesUnique
+  , findVarNames
+  , displayTerm
+  , displayTerm'
+  ) where
+
+import           Data.Maybe
+import           Numeric.Natural
+
+import           Control.Monad.Trans.State
+import qualified Data.Set                  as Set
+import qualified Data.Text                 as T
+
+import           Propa.Lambda.Term
+
+-- | The name of a variable or a constant.
+type Name = T.Text
+
+varNames :: [Name]
+varNames = chars ++ (mappend <$> constNames <*> chars)
+  where
+    chars = map T.singleton ['a'..'z']
+
+constNames :: [Name]
+constNames = chars ++ (mappend <$> constNames <*> chars)
+  where
+    chars = map T.singleton ['A'..'Z']
+
+chooseUnique :: (Ord a) => Set.Set a -> [a] -> a
+chooseUnique taken = head . dropWhile (`Set.member` taken)
+
+makeNameUnique :: Set.Set Name -> Name -> Name
+makeNameUnique taken name
+  = chooseUnique taken
+  $ zipWith (<>) (repeat name)
+  $ "" : map (T.pack . show) [(2::Integer) ..]
+
+-- | Find names for constants that don't overlap with existing constants. Every
+-- unnamed constant is assumed to be a different constant. This means that every
+-- unnamed constant will be assigned a unique name.
+--
+-- Names for constants follow the schema @A@, @B@, ... @AA@, @AB@, ...
+findConstNames :: Term e (Maybe Name) v -> Term e Name v
+findConstNames term = evalState (helper term) (Set.fromList $ catMaybes $ consts term)
+  where
+    helper (Var i) = pure $ Var i
+    helper (Const c) = do
+      taken <- get
+      let name = fromMaybe (chooseUnique taken constNames) c
+      put $ Set.insert name taken
+      pure $ Const name
+    helper (Lambda v t) = Lambda v <$> helper t
+    helper (App l r) = App <$> helper l <*> helper r
+    helper (Ext e) = pure $ Ext e
+
+-- | Make names of existing variables unique. If the name is not already unique
+-- in the current scope, tries to make it unique by appending a number from
+-- @[2..]@.
+makeVarNamesUnique :: Term e Name (Maybe Name) -> Term e Name (Maybe Name)
+makeVarNamesUnique term = helper (Set.fromList $ consts term) term
+  where
+    helper _     (Var i) = Var i
+    helper _     (Const c) = Const c
+    helper taken (Lambda v t) = case v of
+      Nothing -> Lambda Nothing $ helper taken t
+      Just name ->
+        let newName = makeNameUnique taken name
+        in  Lambda (Just newName) $ helper (Set.insert name taken) t
+    helper taken (App l r) = App (helper taken l) (helper taken r)
+    helper _     (Ext e) = Ext e
+
+-- | Find names for unnamed variables that are unique in the current scope.
+--
+-- Names for variables follow the schema @a@, @b@, ..., @aa@, @ab@, ...
+findVarNames :: Term e Name (Maybe Name) -> Term e Name Name
+findVarNames term = helper (Set.fromList $ consts term) term
+  where
+    helper _     (Var i) = Var i
+    helper _     (Const c) = Const c
+    helper taken (Lambda v t) =
+      let name = fromMaybe (chooseUnique taken varNames) v
+      in  Lambda name $ helper (Set.insert name taken) t
+    helper taken (App l r) = App (helper taken l) (helper taken r)
+    helper _     (Ext e) = Ext e
+
+-- | Display a term using the variable and constant names provided. Does not
+-- attempt to resolve name collisions.
+displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
+displayTerm f = dTerm f []
+
+-- | Display a term. Tries to use the provided variable names where possible.
+-- Resolves name collisions.
+displayTerm' :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
+displayTerm' f = displayTerm f . findVarNames . makeVarNamesUnique . findConstNames
+
+nth :: [a] -> Natural -> Maybe a
+nth []     _ = Nothing
+nth (x:_)  0 = Just x
+nth (_:xs) n = nth xs $ n - 1
+
+varName :: [Name] -> Natural -> Name
+varName vs i = fromMaybe e $ nth vs i
+  where
+    e = "[" <> T.pack (show i) <> "]"
+
+dTerm :: (e -> T.Text) -> [Name] -> Term e Name Name -> T.Text
+dTerm _ vs (Var i) = varName vs i
+dTerm _ _  (Const c) = c
+dTerm f vs (Lambda v t) = "λ" <> v <> dLambda (v:vs) t
+  where
+    dLambda ws (Lambda w u) = " " <> w <> dLambda (w:ws) u
+    dLambda ws u            = ". " <> dTerm f ws u
+dTerm f vs (App l r) = dLeft l <> " " <> dRight r
+  where
+    dLeft t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
+    dLeft t              = dTerm f vs t
+    dRight t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
+    dRight t@(App _ _)    = "(" <> dTerm f vs t <> ")"
+    dRight t              = dTerm f vs t
+dTerm f _  (Ext e) = f e
diff --git a/src/Propa/Lambda/Term.hs b/src/Propa/Lambda/Term.hs
new file mode 100644
index 0000000..0b801d1
--- /dev/null
+++ b/src/Propa/Lambda/Term.hs
@@ -0,0 +1,56 @@
+-- | This module contains 'Term', the base type for lambda expressions. It also
+-- contains a few utility functions for operating on it.
+
+module Propa.Lambda.Term
+  ( Term(..)
+  , vars
+  , mapVars
+  , consts
+  , mapConsts
+  ) where
+
+import           Numeric.Natural
+
+-- | Lambda calculus term using De Bruijn indexing and expanded to deal with
+-- naming complexity and extensions.
+data Term e c v
+  = Var Natural
+  -- ^ Variable using a De Bruijn index
+  | Const c
+  -- ^ Constant living outside the variable namespace
+  | Lambda v (Term e c v)
+  -- ^ Lambda definition
+  | App (Term e c v) (Term e c v)
+  -- ^ Lambda application
+  | Ext e
+  -- ^ Term extension (set @e@ to 'Data.Void' if you don't need this)
+  deriving (Show)
+
+-- | All of a term's variable names in order from left to right.
+vars :: Term e c v -> [v]
+vars (Lambda v t) = v : vars t
+vars (App l r)    = vars l <> vars r
+vars _            = []
+
+-- | Map over the variable names.
+mapVars :: (a -> b) -> Term e c a -> Term e c b
+mapVars _ (Var i)      = Var i
+mapVars _ (Const c)    = Const c
+mapVars f (Lambda a t) = Lambda (f a) (mapVars f t)
+mapVars f (App l r)    = App (mapVars f l) (mapVars f r)
+mapVars _ (Ext e)      = Ext e
+
+-- | All of a term's constant names in order from left to right.
+consts :: Term e c v -> [c]
+consts (Const c)    = [c]
+consts (Lambda _ t) = consts t
+consts (App l r)    = consts l <> consts r
+consts _            = []
+
+-- | Map over the constant names.
+mapConsts :: (a -> b) -> Term e a v -> Term e b v
+mapConsts _ (Var i)      = Var i
+mapConsts f (Const c)    = Const (f c)
+mapConsts f (Lambda v t) = Lambda v (mapConsts f t)
+mapConsts f (App l r)    = App (mapConsts f l) (mapConsts f r)
+mapConsts _ (Ext e)      = Ext e
diff --git a/src/Propa/Prolog/Debug.hs b/src/Propa/Prolog/Debug.hs
new file mode 100644
index 0000000..22655b2
--- /dev/null
+++ b/src/Propa/Prolog/Debug.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Debug
+  ( parseAndRun
+  ) where
+
+import qualified Data.Text            as T
+import qualified Data.Text.IO         as T
+
+import           Propa.Prolog.Display
+import           Propa.Prolog.Parse
+import           Propa.Prolog.Unify
+
+parseAndRun :: String -> String -> IO ()
+parseAndRun dbStr statsStr = T.putStrLn $ case results of
+  Left e   -> e
+  Right [] -> "No."
+  Right rs -> T.intercalate "\n" rs
+  where
+    results = do
+      db <- parseDb "<db>" $ T.pack dbStr
+      stats <- parseStats "<query>" $ T.pack statsStr
+      pure $ map displayResult $ run db stats
diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
new file mode 100644
index 0000000..d943b34
--- /dev/null
+++ b/src/Propa/Prolog/Display.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Display
+  ( displayTerm
+  , displayTerms
+  , displayDef
+  , displayDefs
+  , displayResult
+  ) where
+
+import           Data.Char
+import           Data.List
+
+import qualified Data.Map           as Map
+import qualified Data.Text          as T
+
+import           Propa.Prolog.Types
+
+displayName :: T.Text -> T.Text
+displayName name
+  | T.all isLower name = name
+  | otherwise          = "\"" <> escaped <> "\""
+  where
+    escaped = foldl' (\s (a, b) -> T.replace a b s) name
+      [ ("\\", "\\\\")
+      , ("\n", "\\n")
+      , ("\r", "\\r")
+      , ("\t", "\\t")
+      ]
+
+displayStat :: Stat T.Text -> T.Text
+displayStat (Stat "[]" []) = "[]"
+displayStat (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b
+displayStat (Stat name []) = displayName name
+displayStat (Stat name args)
+  = displayName name
+  <> "("
+  <> T.intercalate ", " (map displayTerm args)
+  <> ")"
+
+displayList :: Term T.Text -> T.Text
+displayList (TStat (Stat "[|]" [a, b])) = "," <> displayTerm a <> displayList b
+displayList (TStat (Stat "[]" []))      = "]"
+displayList t                           = "|" <> displayTerm t <> "]"
+
+displayTerm :: Term T.Text -> T.Text
+displayTerm (TVar v)  = v
+displayTerm (TInt i)  = T.pack $ show i
+displayTerm (TStat s) = displayStat s
+
+displayTerms :: [Term T.Text] -> T.Text
+displayTerms terms = T.intercalate ",\n" (map displayTerm terms) <> "."
+
+displayDef :: Def T.Text -> T.Text
+displayDef (Def stat []) = displayStat stat <> "."
+displayDef (Def stat stats)
+  =  displayStat stat
+  <> " :-\n"
+  <> T.intercalate ",\n" (map (\t -> "    " <> displayStat t) stats)
+  <> "."
+
+displayDefs :: [Def T.Text] -> T.Text
+displayDefs = T.intercalate "\n" . map displayDef
+
+displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
+displayResult m
+  | null termsToDisplay = "Yes."
+  | otherwise           = T.intercalate "\n" termsAsStrings
+  where
+    termsToDisplay = filter (\(k, v) -> v /= TVar k) $ Map.assocs m
+    termsAsStrings = map (\(k, v) -> k <> " = " <> displayTerm v) termsToDisplay
diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
new file mode 100644
index 0000000..4b9d9c5
--- /dev/null
+++ b/src/Propa/Prolog/Parse.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Parse
+  ( parseStats
+  , parseDb
+  ) where
+
+import           Control.Monad
+import           Data.Bifunctor
+import           Data.Char
+import           Data.Void
+
+import           Control.Monad.Combinators.Expr
+import qualified Data.Text                      as T
+import           Text.Megaparsec
+import qualified Text.Megaparsec.Char           as C
+import qualified Text.Megaparsec.Char.Lexer     as L
+
+import           Propa.Prolog.Types
+
+type Parser = Parsec Void T.Text
+
+-- Lexeme stuff
+
+space :: Parser ()
+space = L.space C.space1 (L.skipLineComment "%") (L.skipBlockComment "/*" "*/")
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme space
+
+symbol :: T.Text -> Parser T.Text
+symbol = L.symbol space
+
+parens :: Parser a -> Parser a
+parens = between (symbol "(") (symbol ")")
+
+brackets :: Parser a -> Parser a
+brackets = between (symbol "[") (symbol "]")
+
+-- Names
+
+pName :: Parser T.Text
+pName = lexeme $ unquotedName <|> quotedName
+  where
+    unquotedName = takeWhile1P (Just "lowercase character") isLower
+    quotedName = fmap T.pack $ C.char '\'' *> manyTill L.charLiteral (C.char '\'')
+
+pVarName :: Parser T.Text
+pVarName = lexeme $ takeWhile1P (Just "uppercase character") isUpper
+
+-- Statements
+
+pTermToStat :: Parser (Term T.Text) -> Parser (Stat T.Text)
+pTermToStat p = do
+  term <- p
+  case term of
+    (TVar _)  -> fail "expected statement, not variable"
+    (TInt _)  -> fail "expected statement, not integer"
+    (TStat s) -> pure s
+
+-- | Parse a statement of the form @name(args)@.
+pPlainStat :: Parser (Stat T.Text)
+pPlainStat = do
+  name <- pName
+  terms <- parens (pTerm `sepBy1` symbol ",") <|> pure []
+  pure $ Stat name terms
+
+pStat :: Parser (Stat T.Text)
+pStat = pPlainStat <|> pTermToStat pTerm
+
+pStats :: Parser [Stat T.Text]
+pStats = (pStat `sepBy1` symbol ",") <* symbol "."
+
+-- Terms
+
+pCons :: Parser (Term T.Text)
+pCons = brackets $ do
+  elems <- pTerm `sepBy1` symbol ","
+  void $ symbol "|"
+  rest <- pTerm
+  pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) rest elems
+
+pList :: Parser (Term T.Text)
+pList = do
+  elems <- brackets $ pTerm `sepBy` symbol ","
+  pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems
+
+-- | Parse a term that is not an expression.
+pPlainTerm :: Parser (Term T.Text)
+pPlainTerm
+  =   (TVar <$> pVarName)
+  <|> (TInt <$> L.signed (pure ()) L.decimal)
+  <|> (TStat <$> pPlainStat)
+  <|> try pCons
+  <|> pList
+  <|> parens pTerm
+
+pTerm :: Parser (Term T.Text)
+pTerm = makeExprParser pPlainTerm
+  [ [ binary "=" ]
+  ]
+  where
+    binary name = InfixL $ (\a b -> TStat $ Stat name [a, b]) <$ symbol name
+
+-- Definitions
+
+pDef :: Parser (Def T.Text)
+pDef = do
+  stat <- pStat
+  stats <- (symbol ":-" *> (pStat `sepBy1` symbol ",")) <|> pure []
+  void $ symbol "."
+  pure $ Def stat stats
+
+pDefs :: Parser [Def T.Text]
+pDefs = many pDef
+
+-- And finally, our nice parsers
+
+parseHelper :: Parser a -> FilePath -> T.Text -> Either T.Text a
+parseHelper p path input
+  = first (T.pack . errorBundlePretty)
+  $ parse (space *> p <* eof) path input
+
+parseStats :: FilePath -> T.Text -> Either T.Text [Stat T.Text]
+parseStats = parseHelper pStats
+
+parseDb :: FilePath -> T.Text -> Either T.Text (Db T.Text)
+parseDb = parseHelper pDefs
diff --git a/src/Propa/Prolog/Types.hs b/src/Propa/Prolog/Types.hs
new file mode 100644
index 0000000..ca6236f
--- /dev/null
+++ b/src/Propa/Prolog/Types.hs
@@ -0,0 +1,60 @@
+module Propa.Prolog.Types
+  ( Stat(..)
+  , Term(..)
+  , tVar
+  , Def(..)
+  , Db
+  ) where
+
+import qualified Data.Text as T
+
+data Stat a = Stat T.Text [Term a]
+  deriving (Show, Eq)
+
+instance Functor Stat where
+  fmap f (Stat name terms) = Stat name $ fmap (fmap f) terms
+
+instance Foldable Stat where
+  foldMap f (Stat _ terms) = foldMap (foldMap f) terms
+
+instance Traversable Stat where
+  traverse f (Stat name terms) = Stat name <$> traverse (traverse f) terms
+
+data Term a
+  = TVar a
+  | TInt Integer
+  | TStat (Stat a)
+  deriving (Show, Eq)
+
+instance Functor Term where
+  fmap f (TVar a)  = TVar $ f a
+  fmap _ (TInt i)  = TInt i
+  fmap f (TStat s) = TStat $ fmap f s
+
+instance Foldable Term where
+  foldMap f (TVar a)  = f a
+  foldMap _ (TInt _)  = mempty
+  foldMap f (TStat s) = foldMap f s
+
+instance Traversable Term where
+  traverse f (TVar a)  = TVar <$> f a
+  traverse _ (TInt i)  = pure $ TInt i
+  traverse f (TStat s) = TStat <$> traverse f s
+
+tVar :: Term a -> Maybe a
+tVar (TVar v) = Just v
+tVar _        = Nothing
+
+data Def a = Def (Stat a) [Stat a]
+  deriving (Show)
+
+instance Functor Def where
+  fmap f (Def stat stats) = Def (fmap f stat) (fmap f <$> stats)
+
+instance Foldable Def where
+  foldMap f (Def stat stats) = foldMap f stat <> foldMap (foldMap f) stats
+
+instance Traversable Def where
+  traverse f (Def stat stats) = Def <$> traverse f stat <*> traverse (traverse f) stats
+
+type Db a = [Def a]
diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
new file mode 100644
index 0000000..50991ec
--- /dev/null
+++ b/src/Propa/Prolog/Unify.hs
@@ -0,0 +1,164 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Unify
+  ( run
+  ) where
+
+import           Control.Applicative
+import           Control.Monad
+import           Data.Foldable
+import           Data.List
+import           Data.Tuple
+
+import           Control.Monad.Trans.Class
+import           Control.Monad.Trans.State
+import qualified Data.Map                  as Map
+import qualified Data.Set                  as Set
+import qualified Data.Text                 as T
+
+import           Propa.Prolog.Types
+
+-- General utility functions
+
+-- | Start at a value and follow the map's entries until the end of the chain of
+-- references.
+follow :: (Ord a) => (b -> Maybe a) -> Map.Map a b -> b -> b
+follow f m b = maybe b (follow f m) $ (m Map.!?) =<< f b
+
+-- | Deduplicates the elements of a finite list. Doesn't preserve the order of
+-- the elements. Doesn't work on infinite lists.
+deduplicate :: (Ord a) => [a] -> [a]
+deduplicate = Set.toList . Set.fromList
+
+-- Now the fun begins...
+
+data Context = Context
+  { cDb     :: Db T.Text
+  , cVarIdx :: Int
+  , cTerms  :: Map.Map Int (Term Int)
+  } deriving (Show)
+
+newContext :: [Def T.Text] -> Context
+newContext db = Context db 0 Map.empty
+
+bindTerm :: Int -> Term Int -> UniM ()
+bindTerm k v = modify $ \c -> c{cTerms = Map.insert k v $ cTerms c}
+
+-- | Look up a variable, first repeatedly in the var map and then the term map.
+-- Returns statements unchanged.
+--
+-- If this returns a variable, then that variable is not bound.
+lookupTerm :: Term Int -> UniM (Term Int)
+lookupTerm t = do
+  c <- get
+  pure $ follow tVar (cTerms c) t
+
+-- | A simple state monad transformer over the list monad for easy backtracking.
+-- Needs to be changed when implementing cuts.
+type UniM = StateT Context []
+
+varMap :: (Foldable a) => a T.Text -> UniM (Map.Map T.Text Int)
+varMap a = do
+  c <- get
+  let i = cVarIdx c
+      vars = deduplicate $ toList a
+      vmap = Map.fromList $ zip vars [i..]
+  put c{cVarIdx = i + Map.size vmap}
+  pure vmap
+
+-- | Convert a definition's variables to unique integers that are not already in
+-- use in the current context.
+understand :: (Functor a, Foldable a) => a T.Text -> UniM (a Int, Map.Map T.Text Int)
+understand a = do
+  vmap <- varMap a
+  pure (fmap (vmap Map.!) a, vmap)
+
+satisfyStat :: Stat Int -> UniM ()
+satisfyStat stat = do
+  c <- get
+  (Def dStat dStats, _) <- understand =<< lift (cDb c)
+  unifyStat stat dStat
+  satisfyStats dStats
+
+satisfyStats :: [Stat Int] -> UniM ()
+satisfyStats = traverse_ satisfyStat
+
+unifyStat :: Stat Int -> Stat Int -> UniM ()
+unifyStat (Stat name1 args1) (Stat name2 args2) = do
+  guard $ name1 == name2
+  unifyTerms args1 args2
+
+unifyTerm :: Term Int -> Term Int -> UniM ()
+unifyTerm t1 t2 = do
+  t1' <- lookupTerm t1
+  t2' <- lookupTerm t2
+  case (t1', t2') of
+    (TStat s1, TStat s2)      -> unifyStat s1 s2
+    (TInt i1, TInt i2)        -> guard $ i1 == i2
+    (TVar v, TVar w) | v == w -> pure ()
+    (TVar v, t)               -> bindTerm v t
+    (t, TVar v)               -> bindTerm v t
+    (_, _)                    -> empty
+
+unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
+unifyTerms t1 t2 = do
+  guard $ length t1 == length t2
+  sequenceA_ $ zipWith unifyTerm t1 t2
+
+-- Figuring out how to display the result of the unification
+
+-- | An infinite list of possible variable names: @A@, @B@, ..., @A1@, @B1@,
+-- ..., @A2@, ...
+varNames :: [T.Text]
+varNames = do
+  num <- "" : map (T.pack . show) [(1::Integer)..]
+  char <- alphabet
+  pure $ char <> num
+  where
+    alphabet = map T.singleton ['A'..'Z']
+
+-- | Find a naming (Map from integer to name) for all variables in a list of
+-- terms based on the original variable names and the variable mapping. Attempts
+-- to map variables to known variables instead of a common unknown variable.
+findVarNaming :: Map.Map T.Text Int -> Map.Map Int (Term Int) -> [Term Int] -> Map.Map Int T.Text
+findVarNaming known vars terms =
+  let knownLookedUp :: Map.Map T.Text Int
+      knownLookedUp = Map.mapMaybe (tVar . follow tVar vars . TVar) known
+      knownNaming = Map.fromList $ reverse $ map swap $ Map.toList knownLookedUp
+      knownNames = Map.keysSet known
+      knownVars = Map.keysSet knownNaming
+      termVars = Set.fromList $ concatMap toList terms
+      unknownVars = termVars Set.\\ knownVars
+      availVarNames = filter (not . (`Set.member` knownNames)) varNames
+      unknownNaming = Map.fromList $ zip (sort $ Set.toList unknownVars) availVarNames
+  in  knownNaming <> unknownNaming
+
+-- | Recursively set variables to their most resolved term.
+resolveVars :: Term Int -> UniM (Term Int)
+resolveVars t = do
+  t2 <- lookupTerm t
+  case t2 of
+    (TVar v)                 -> pure $ TVar v
+    (TInt i)                 -> pure $ TInt i
+    (TStat (Stat name args)) -> TStat . Stat name <$> traverse resolveVars args
+
+-- | Helper type so I can resolve variables in multiple statements
+-- simultaneously.
+newtype Stats a = Stats { unStats :: [Stat a] }
+
+instance Functor Stats where
+  fmap f (Stats ts) = Stats $ fmap (fmap f) ts
+
+instance Foldable Stats where
+  foldMap f (Stats ts) = foldMap (foldMap f) ts
+
+run :: Db T.Text -> [Stat T.Text] -> [Map.Map T.Text (Term T.Text)]
+run db stats = map fst $ runStateT helper $ newContext db
+  where
+    helper = do
+      (stats2, vmap) <- understand $ Stats stats
+      satisfyStats $ unStats stats2
+      tmap <- traverse (resolveVars . TVar) vmap
+      c <- get
+      let naming = findVarNaming vmap (cTerms c) $ Map.elems tmap
+      pure $ fmap (naming Map.!) <$> tmap
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
index 0000000..602ebce
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,5 @@
+resolver:
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/23.yaml
+
+packages:
+- .
diff --git a/stack.yaml.lock b/stack.yaml.lock
new file mode 100644
index 0000000..3d6911f
--- /dev/null
+++ b/stack.yaml.lock
@@ -0,0 +1,13 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+packages: []
+snapshots:
+- completed:
+    size: 532832
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/23.yaml
+    sha256: fbb2a0519008533924c7753bd7164ddd1009f09504eb06674acad6049b46db09
+  original:
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/23.yaml