From 89c942e81e6e97b1cc0699d98202a9d4f5306acb Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Fri, 11 Dec 2020 13:44:04 +0000
Subject: [PATCH] Start implementing unification

---
 props.cabal         |  5 +++--
 src/Props/Prolog.hs | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+), 2 deletions(-)
 create mode 100644 src/Props/Prolog.hs

diff --git a/props.cabal b/props.cabal
index ef355c2..581e772 100644
--- a/props.cabal
+++ b/props.cabal
@@ -1,10 +1,10 @@
 cabal-version: 1.18
 
--- This file has been generated from package.yaml by hpack version 0.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.2.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 03958e185b40527fc635759af663a90da5cd82cead9a9fd30ce5ab3e91b53f83
+-- hash: 78cab4f7dbc3221eeb49550721e77438db654b072638fcbe9a383fd915dbf277
 
 name:           props
 version:        0.1.0.0
@@ -24,6 +24,7 @@ library
   exposed-modules:
       Props.Lambda.Display
       Props.Lambda.Term
+      Props.Prolog
   other-modules:
       Paths_props
   hs-source-dirs:
diff --git a/src/Props/Prolog.hs b/src/Props/Prolog.hs
new file mode 100644
index 0000000..80faa2b
--- /dev/null
+++ b/src/Props/Prolog.hs
@@ -0,0 +1,33 @@
+module Props.Prolog where
+
+import           Control.Monad
+
+import qualified Data.Map      as Map
+
+data Term
+  = Variable String
+  | Statement String [Term]
+  deriving (Show)
+
+type VarMap = Map.Map String Term
+
+lookupTerm :: VarMap -> Term -> Term
+lookupTerm _   t@(Statement _ _) = t
+lookupTerm env t@(Variable s) = case env Map.!? s of
+  Nothing -> t
+  Just t' -> lookupTerm env t'
+
+unifyStatements :: String -> [Term] -> String -> [Term] -> VarMap -> [VarMap]
+unifyStatements a as b bs env = do
+  guard $ a == b
+  guard $ length as == length bs
+  foldr (>=>) pure (zipWith unify as bs) env
+
+unify :: Term -> Term -> VarMap -> [VarMap]
+unify t1 t2 env = case (lookupTerm env t1, lookupTerm env t2) of
+  (Statement a as, Statement b bs) -> unifyStatements a as b bs env
+  (Variable a, b) -> [Map.insert a b env]
+  (a, Variable b) -> [Map.insert b a env]
+
+unify' :: Term -> Term -> [VarMap]
+unify' t1 t2 = unify t1 t2 Map.empty