Start implementing unification

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:

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