From fc0ede9499a1a768729bb8fe954b6618df05ee15 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 14:16:23 +0100
Subject: [PATCH 01/39] Create basic lambda term type

---
 package.yaml        |  2 ++
 props.cabal         |  7 ++++++-
 src/Props/Lambda.hs | 23 +++++++++++++++++++++++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 src/Props/Lambda.hs

diff --git a/package.yaml b/package.yaml
index d1f1575..5062cc2 100644
--- a/package.yaml
+++ b/package.yaml
@@ -13,6 +13,8 @@ extra-doc-files:
 
 dependencies:
 - base >= 4.7 && < 5
+- containers
+- text
 
 library:
   source-dirs: src
diff --git a/props.cabal b/props.cabal
index 8063c21..bc459b3 100644
--- a/props.cabal
+++ b/props.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.18
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 057a536ac3d0fd40b3122084eee53201158527bbcd0dbac7cec33d8fd06cf208
+-- hash: 5e16e68a3016455a93f44cbee36b19144a1a414a8cb0bf4a062a1566b7119a38
 
 name:           props
 version:        0.1.0.0
@@ -23,12 +23,15 @@ extra-doc-files:
 library
   exposed-modules:
       Props
+      Props.Lambda
   other-modules:
       Paths_props
   hs-source-dirs:
       src
   build-depends:
       base >=4.7 && <5
+    , containers
+    , text
   default-language: Haskell2010
 
 executable props
@@ -40,5 +43,7 @@ executable props
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
+    , containers
     , props
+    , text
   default-language: Haskell2010
diff --git a/src/Props/Lambda.hs b/src/Props/Lambda.hs
new file mode 100644
index 0000000..1b71ce6
--- /dev/null
+++ b/src/Props/Lambda.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Props.Lambda
+  ( Term(..)
+  , displayTerm
+  ) where
+
+import qualified Data.Set  as Set
+import qualified Data.Text as T
+
+type Name = T.Text
+type PreferredName = Maybe Name
+
+-- | Lambda calculus term using De Bruijn indexing
+data Term a
+  = Var PreferredName Int
+  | Lambda PreferredName (Term a)
+  | App (Term a) (Term a)
+  | Native a
+  deriving (Show)
+
+displayTerm :: (Set.Set Name -> a -> T.Text) -> Term a -> T.Text
+displayTerm = undefined

From ed7179a846a03546e4ac8a24f13b5734304a7a89 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 16:07:56 +0100
Subject: [PATCH 02/39] Restructure and begin displaying lambdas

---
 app/Main.hs                 | 13 +++++++++++--
 props.cabal                 |  6 +++---
 src/Props.hs                |  4 ----
 src/Props/Lambda.hs         | 23 -----------------------
 src/Props/Lambda/Display.hs | 31 +++++++++++++++++++++++++++++++
 src/Props/Lambda/Term.hs    | 33 +++++++++++++++++++++++++++++++++
 6 files changed, 78 insertions(+), 32 deletions(-)
 delete mode 100644 src/Props.hs
 delete mode 100644 src/Props/Lambda.hs
 create mode 100644 src/Props/Lambda/Display.hs
 create mode 100644 src/Props/Lambda/Term.hs

diff --git a/app/Main.hs b/app/Main.hs
index d94efcc..3eacdac 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,6 +1,15 @@
 module Main where
 
-import           Props
+import Data.Void
+
+import Props.Lambda.Term
+
+yCombinator :: Term Void String String
+yCombinator = Lambda "f"
+  (App
+    (Lambda "x" (App (Var 1) (App (Var 0) (Var 0))))
+    (Lambda "x" (App (Var 1) (App (Var 0) (Var 0))))
+  )
 
 main :: IO ()
-main = putStrLn helloWorld
+main = print yCombinator
diff --git a/props.cabal b/props.cabal
index bc459b3..d0e1c22 100644
--- a/props.cabal
+++ b/props.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.18
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5e16e68a3016455a93f44cbee36b19144a1a414a8cb0bf4a062a1566b7119a38
+-- hash: 5a5ea1f94c0aefd4530bcfe91d7e5265b092b9e1b361d21bef695382fe4422a5
 
 name:           props
 version:        0.1.0.0
@@ -22,8 +22,8 @@ extra-doc-files:
 
 library
   exposed-modules:
-      Props
-      Props.Lambda
+      Props.Lambda.Display
+      Props.Lambda.Term
   other-modules:
       Paths_props
   hs-source-dirs:
diff --git a/src/Props.hs b/src/Props.hs
deleted file mode 100644
index 8caf1dc..0000000
--- a/src/Props.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module Props where
-
-helloWorld :: String
-helloWorld = "Hello World!"
diff --git a/src/Props/Lambda.hs b/src/Props/Lambda.hs
deleted file mode 100644
index 1b71ce6..0000000
--- a/src/Props/Lambda.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Props.Lambda
-  ( Term(..)
-  , displayTerm
-  ) where
-
-import qualified Data.Set  as Set
-import qualified Data.Text as T
-
-type Name = T.Text
-type PreferredName = Maybe Name
-
--- | Lambda calculus term using De Bruijn indexing
-data Term a
-  = Var PreferredName Int
-  | Lambda PreferredName (Term a)
-  | App (Term a) (Term a)
-  | Native a
-  deriving (Show)
-
-displayTerm :: (Set.Set Name -> a -> T.Text) -> Term a -> T.Text
-displayTerm = undefined
diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
new file mode 100644
index 0000000..2ed95a6
--- /dev/null
+++ b/src/Props/Lambda/Display.hs
@@ -0,0 +1,31 @@
+module Props.Lambda.Display
+  ( displayTerm
+  ) where
+
+import qualified Data.Text         as T
+
+import           Props.Lambda.Term
+
+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']
+
+findConstNames :: Term e (Maybe Name) v -> Term e Name v
+findConstNames = undefined
+
+makeVarNamesUnique :: Term e c (Maybe Name) -> Term e c (Maybe Name)
+makeVarNamesUnique = undefined
+
+findVarNames :: Term e c (Maybe Name) -> Term e c Name
+findVarNames = undefined
+
+displayTerm :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
+displayTerm = undefined
diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
new file mode 100644
index 0000000..4609016
--- /dev/null
+++ b/src/Props/Lambda/Term.hs
@@ -0,0 +1,33 @@
+module Props.Lambda.Term
+  ( Term(..)
+  , vars
+  , consts
+  ) 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 'Void' if you don't need this)
+  deriving (Show)
+
+vars :: Term e c v -> [v]
+vars (Lambda v t) = v : vars t
+vars (App l r)    = vars l <> vars r
+vars _            = []
+
+consts :: Term e c v -> [c]
+consts (Const c)    = [c]
+consts (Lambda _ t) = consts t
+consts (App l r)    = consts l <> consts r
+consts _            = []

From 7d0d51373509e5f7fb9857a9f803dffa05523693 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 17:54:58 +0100
Subject: [PATCH 03/39] Display terms with correct parentheses

---
 src/Props/Lambda/Display.hs | 43 +++++++++++++++++++++++++++++++------
 src/Props/Lambda/Term.hs    | 30 ++++++++++++++++++++++++++
 2 files changed, 67 insertions(+), 6 deletions(-)

diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
index 2ed95a6..a8630f2 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Props/Lambda/Display.hs
@@ -1,7 +1,15 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Props.Lambda.Display
-  ( displayTerm
+  ( findConstNames
+  , makeVarNamesUnique
+  , findVarNames
+  , displayTerm
   ) where
 
+import Data.Maybe
+import           Numeric.Natural
+
 import qualified Data.Text         as T
 
 import           Props.Lambda.Term
@@ -19,13 +27,36 @@ constNames = chars ++ (mappend <$> constNames <*> chars)
     chars = map T.singleton ['A'..'Z']
 
 findConstNames :: Term e (Maybe Name) v -> Term e Name v
-findConstNames = undefined
+findConstNames = mapConsts (fromMaybe "[]") -- TODO implement
 
 makeVarNamesUnique :: Term e c (Maybe Name) -> Term e c (Maybe Name)
-makeVarNamesUnique = undefined
+makeVarNamesUnique = id -- TODO implement
 
 findVarNames :: Term e c (Maybe Name) -> Term e c Name
-findVarNames = undefined
+findVarNames = mapVars (fromMaybe "[]") -- TODO implement
 
-displayTerm :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
-displayTerm = undefined
+displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
+displayTerm f = dTerm f []
+
+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 <> ". " <> dTerm f (v:vs) t
+dTerm f _  (Ext e) = f e
+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
diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
index 4609016..acdfe27 100644
--- a/src/Props/Lambda/Term.hs
+++ b/src/Props/Lambda/Term.hs
@@ -1,11 +1,19 @@
+{-# LANGUAGE OverloadedStrings#-}
+
 module Props.Lambda.Term
   ( Term(..)
   , vars
+  , mapVars
   , consts
+  , mapConsts
+  , termI
+  , termY
   ) where
 
 import           Numeric.Natural
 
+import qualified Data.Text as T
+
 -- | Lambda calculus term using De Bruijn indexing and expanded to deal with
 -- naming complexity and extensions.
 data Term e c v
@@ -26,8 +34,30 @@ vars (Lambda v t) = v : vars t
 vars (App l r)    = vars l <> vars r
 vars _            = []
 
+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
+
 consts :: Term e c v -> [c]
 consts (Const c)    = [c]
 consts (Lambda _ t) = consts t
 consts (App l r)    = consts l <> consts r
 consts _            = []
+
+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
+
+termI :: Term e T.Text T.Text
+termI = Lambda "x" (Var 0)
+
+termY :: Term e T.Text T.Text
+termY = Lambda "f" $ App
+  (Lambda "x" $ App (Var 1) $ App (Var 0) (Var 0))
+  (Lambda "x" $ App (Var 1) $ App (Var 0) (Var 0))

From 72083325ce976c3e2a306fa56e685db1688e7e16 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 18:19:18 +0100
Subject: [PATCH 04/39] Display nested lambdas together

---
 src/Props/Lambda/Display.hs | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
index a8630f2..3197aa5 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Props/Lambda/Display.hs
@@ -7,7 +7,7 @@ module Props.Lambda.Display
   , displayTerm
   ) where
 
-import Data.Maybe
+import           Data.Maybe
 import           Numeric.Natural
 
 import qualified Data.Text         as T
@@ -39,8 +39,8 @@ displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
 displayTerm f = dTerm f []
 
 nth :: [a] -> Natural -> Maybe a
-nth [] _ = Nothing
-nth (x:_) 0 = Just x
+nth []     _ = Nothing
+nth (x:_)  0 = Just x
 nth (_:xs) n = nth xs $ n - 1
 
 varName :: [Name] -> Natural -> Name
@@ -51,12 +51,15 @@ varName vs i = fromMaybe e $ nth vs 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 <> ". " <> dTerm f (v:vs) t
-dTerm f _  (Ext e) = f e
+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
+    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
+    dRight t@(App _ _)    = "(" <> dTerm f vs t <> ")"
+    dRight t              = dTerm f vs t
+dTerm f _  (Ext e) = f e

From 66c77d13b0b213ab009d131d9186f527a94e50f5 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 19:02:57 +0100
Subject: [PATCH 05/39] Reformat Term.hs

---
 src/Props/Lambda/Term.hs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
index acdfe27..4d42547 100644
--- a/src/Props/Lambda/Term.hs
+++ b/src/Props/Lambda/Term.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE OverloadedStrings#-}
+{-# LANGUAGE OverloadedStrings #-}
 
 module Props.Lambda.Term
   ( Term(..)
@@ -12,7 +12,7 @@ module Props.Lambda.Term
 
 import           Numeric.Natural
 
-import qualified Data.Text as T
+import qualified Data.Text       as T
 
 -- | Lambda calculus term using De Bruijn indexing and expanded to deal with
 -- naming complexity and extensions.
@@ -35,11 +35,11 @@ vars (App l r)    = vars l <> vars r
 vars _            = []
 
 mapVars :: (a -> b) -> Term e c a -> Term e c b
-mapVars _ (Var i) = Var i
-mapVars _ (Const c) = Const c
+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
+mapVars f (App l r)    = App (mapVars f l) (mapVars f r)
+mapVars _ (Ext e)      = Ext e
 
 consts :: Term e c v -> [c]
 consts (Const c)    = [c]
@@ -48,11 +48,11 @@ consts (App l r)    = consts l <> consts r
 consts _            = []
 
 mapConsts :: (a -> b) -> Term e a v -> Term e b v
-mapConsts _ (Var i) = Var i
-mapConsts f (Const c) = Const (f c)
+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
+mapConsts f (App l r)    = App (mapConsts f l) (mapConsts f r)
+mapConsts _ (Ext e)      = Ext e
 
 termI :: Term e T.Text T.Text
 termI = Lambda "x" (Var 0)

From b9762ddb10a96988403a9f1a086ed6595c76a3db Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 19:03:22 +0100
Subject: [PATCH 06/39] Correctly display terms

---
 package.yaml                |  1 +
 props.cabal                 |  4 ++-
 src/Props/Lambda/Display.hs | 55 +++++++++++++++++++++++++++++++++----
 3 files changed, 53 insertions(+), 7 deletions(-)

diff --git a/package.yaml b/package.yaml
index 5062cc2..b6c0015 100644
--- a/package.yaml
+++ b/package.yaml
@@ -15,6 +15,7 @@ dependencies:
 - base >= 4.7 && < 5
 - containers
 - text
+- transformers
 
 library:
   source-dirs: src
diff --git a/props.cabal b/props.cabal
index d0e1c22..ef355c2 100644
--- a/props.cabal
+++ b/props.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.18
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5a5ea1f94c0aefd4530bcfe91d7e5265b092b9e1b361d21bef695382fe4422a5
+-- hash: 03958e185b40527fc635759af663a90da5cd82cead9a9fd30ce5ab3e91b53f83
 
 name:           props
 version:        0.1.0.0
@@ -32,6 +32,7 @@ library
       base >=4.7 && <5
     , containers
     , text
+    , transformers
   default-language: Haskell2010
 
 executable props
@@ -46,4 +47,5 @@ executable props
     , containers
     , props
     , text
+    , transformers
   default-language: Haskell2010
diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
index 3197aa5..6184da4 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Props/Lambda/Display.hs
@@ -5,12 +5,15 @@ module Props.Lambda.Display
   , makeVarNamesUnique
   , findVarNames
   , displayTerm
+  , displayTerm'
   ) where
 
 import           Data.Maybe
 import           Numeric.Natural
 
-import qualified Data.Text         as T
+import           Control.Monad.Trans.State
+import qualified Data.Set                  as Set
+import qualified Data.Text                 as T
 
 import           Props.Lambda.Term
 
@@ -26,18 +29,58 @@ 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) ..]
+
 findConstNames :: Term e (Maybe Name) v -> Term e Name v
-findConstNames = mapConsts (fromMaybe "[]") -- TODO implement
+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
 
-makeVarNamesUnique :: Term e c (Maybe Name) -> Term e c (Maybe Name)
-makeVarNamesUnique = id -- TODO implement
+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
 
-findVarNames :: Term e c (Maybe Name) -> Term e c Name
-findVarNames = mapVars (fromMaybe "[]") -- TODO implement
+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
 
 displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
 displayTerm f = dTerm f []
 
+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

From d8865c49d718a3f24f7ff2e53cdb048f7f60aee0 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 19:05:31 +0100
Subject: [PATCH 07/39] Remove test terms

---
 src/Props/Lambda/Term.hs | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
index 4d42547..a6b0316 100644
--- a/src/Props/Lambda/Term.hs
+++ b/src/Props/Lambda/Term.hs
@@ -1,19 +1,13 @@
-{-# LANGUAGE OverloadedStrings #-}
-
 module Props.Lambda.Term
   ( Term(..)
   , vars
   , mapVars
   , consts
   , mapConsts
-  , termI
-  , termY
   ) where
 
 import           Numeric.Natural
 
-import qualified Data.Text       as T
-
 -- | Lambda calculus term using De Bruijn indexing and expanded to deal with
 -- naming complexity and extensions.
 data Term e c v
@@ -53,11 +47,3 @@ 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
-
-termI :: Term e T.Text T.Text
-termI = Lambda "x" (Var 0)
-
-termY :: Term e T.Text T.Text
-termY = Lambda "f" $ App
-  (Lambda "x" $ App (Var 1) $ App (Var 0) (Var 0))
-  (Lambda "x" $ App (Var 1) $ App (Var 0) (Var 0))

From d8ebda0fa93f70e3f65c983c1804be500280ae8e Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 19:26:45 +0100
Subject: [PATCH 08/39] Add documentation

---
 src/Props/Lambda/Display.hs | 21 ++++++++++++++++++++-
 src/Props/Lambda/Term.hs    |  9 ++++++++-
 2 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
index 6184da4..452d6d6 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Props/Lambda/Display.hs
@@ -1,7 +1,10 @@
 {-# LANGUAGE OverloadedStrings #-}
 
+-- | This module contains functions useful for displaying 'Term's.
+
 module Props.Lambda.Display
-  ( findConstNames
+  ( Name
+  , findConstNames
   , makeVarNamesUnique
   , findVarNames
   , displayTerm
@@ -17,6 +20,7 @@ import qualified Data.Text                 as T
 
 import           Props.Lambda.Term
 
+-- | The name of a variable or a constant.
 type Name = T.Text
 
 varNames :: [Name]
@@ -38,6 +42,11 @@ makeNameUnique taken name
   $ 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
@@ -51,6 +60,9 @@ findConstNames term = evalState (helper term) (Set.fromList $ catMaybes $ consts
     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
@@ -64,6 +76,9 @@ makeVarNamesUnique term = helper (Set.fromList $ consts term) term
     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
@@ -75,9 +90,13 @@ findVarNames term = helper (Set.fromList $ consts term) term
     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
 
diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
index a6b0316..4db56ee 100644
--- a/src/Props/Lambda/Term.hs
+++ b/src/Props/Lambda/Term.hs
@@ -1,3 +1,6 @@
+-- | This module contains 'Term', the base type for lambda expressions. It also
+-- contains a few utility functions for operating on it.
+
 module Props.Lambda.Term
   ( Term(..)
   , vars
@@ -20,14 +23,16 @@ data Term e c v
   | App (Term e c v) (Term e c v)
   -- ^ Lambda application
   | Ext e
-  -- ^ Term extension (set @e@ to 'Void' if you don't need this)
+  -- ^ 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
@@ -35,12 +40,14 @@ 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)

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 09/39] 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

From 37c1307d545a6f4147eb43a1a8e2bccbd487e75d Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Fri, 11 Dec 2020 16:50:39 +0000
Subject: [PATCH 10/39] Implement prolog-style unification

---
 app/Main.hs         |  13 +---
 src/Props/Prolog.hs | 154 +++++++++++++++++++++++++++++++++++++-------
 2 files changed, 133 insertions(+), 34 deletions(-)

diff --git a/app/Main.hs b/app/Main.hs
index 3eacdac..f7090c2 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,15 +1,4 @@
 module Main where
 
-import Data.Void
-
-import Props.Lambda.Term
-
-yCombinator :: Term Void String String
-yCombinator = Lambda "f"
-  (App
-    (Lambda "x" (App (Var 1) (App (Var 0) (Var 0))))
-    (Lambda "x" (App (Var 1) (App (Var 0) (Var 0))))
-  )
-
 main :: IO ()
-main = print yCombinator
+main = putStrLn "Hello world!"
diff --git a/src/Props/Prolog.hs b/src/Props/Prolog.hs
index 80faa2b..3ca4234 100644
--- a/src/Props/Prolog.hs
+++ b/src/Props/Prolog.hs
@@ -1,33 +1,143 @@
 module Props.Prolog where
 
 import           Control.Monad
+import           Data.Foldable
 
-import qualified Data.Map      as Map
+import           Control.Monad.Trans.Class
+import           Control.Monad.Trans.State
+import qualified Data.Map                  as Map
+import qualified Data.Set                  as Set
 
-data Term
-  = Variable String
-  | Statement String [Term]
+data Term a
+  = Var a
+  | Stat String [Term a]
   deriving (Show)
 
-type VarMap = Map.Map String Term
+instance Functor Term where
+  fmap f (Var a)          = Var $ f a
+  fmap f (Stat name args) = Stat name $ fmap (fmap f) args
 
-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'
+instance Foldable Term where
+  foldMap f (Var a)       = f a
+  foldMap f (Stat _ args) = foldMap (foldMap f) args
 
-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
+instance Traversable Term where
+  traverse f (Var a)          = Var <$> f a
+  traverse f (Stat name args) = Stat name <$> traverse (traverse f) args
 
-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]
+data Def a = Def String [Term a] [Term a]
+  deriving (Show)
 
-unify' :: Term -> Term -> [VarMap]
-unify' t1 t2 = unify t1 t2 Map.empty
+instance Functor Def where
+  fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms)
+
+instance Foldable Def where
+  foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms
+
+instance Traversable Def where
+  traverse f (Def dName dArgs dTerms)
+    =   Def dName
+    <$> traverse (traverse f) dArgs
+    <*> traverse (traverse f) dTerms
+
+data Context = Context
+  { cDb     :: [Def String]
+  , cVarIdx :: Int
+  , cVars   :: Map.Map Int Int
+  , cTerms  :: Map.Map Int (String, [Term Int])
+  } deriving (Show)
+
+newContext :: [Def String] -> Context
+newContext db = Context db 0 Map.empty Map.empty
+
+learnVar :: Int -> Int -> UniM ()
+learnVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
+
+learnTerm :: Int -> String -> [Term Int] -> UniM ()
+learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c}
+
+-- | Look up a variable, first in the var map and then the term map. Returns
+-- statements unchanged.
+--
+-- If this returns a variable, then that variable is unbound.
+lookupVar :: Term Int -> UniM (Term Int)
+lookupVar t@(Stat _ _) = pure t
+lookupVar t@(Var v) = do
+  c <- get
+  case cVars c Map.!? v of
+    Just v' -> lookupVar (Var v')
+    Nothing -> pure $ case cTerms c Map.!? v of
+      Nothing           -> t
+      Just (name, args) -> Stat name args
+
+-- | A simple state monad transformer over the list monad for easy backtracking.
+-- Needs to be changed when implementing cuts.
+type UniM = StateT Context []
+
+-- | A faster version of 'nub'.
+fastNub :: (Ord a) => [a] -> [a]
+fastNub = Set.toList . Set.fromList
+
+varMap :: (Foldable a) => a String -> UniM (Map.Map String Int)
+varMap a = do
+  c <- get
+  let i = cVarIdx c
+      vars = fastNub $ 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 String -> UniM (a Int, Map.Map String Int)
+understand a = do
+  vmap <- varMap a
+  pure (fmap (vmap Map.!) a, vmap)
+
+satisfy :: Term Int -> UniM ()
+satisfy (Var _)          = undefined
+satisfy (Stat name args) = do
+  c <- get
+  (Def dName dArgs dTerms, _) <- understand =<< lift (cDb c)
+  lift $ guard $ name == dName -- Not sure if 'lift' is really necessary
+  unifyTerms args dArgs
+  satisfyTerms dTerms
+
+satisfyTerms :: [Term Int] -> UniM ()
+satisfyTerms = traverse_ satisfy
+
+unify :: Term Int -> Term Int -> UniM ()
+unify t1 t2 = do
+  t1' <- lookupVar t1
+  t2' <- lookupVar t2
+  case (t1', t2') of
+    (Stat name1 args1, Stat name2 args2) -> do
+      lift $ guard $ name1 == name2
+      unifyTerms args1 args2
+    (Var v1, Stat name2 args2) -> learnTerm v1 name2 args2
+    (Stat name1 args1, Var v2) -> learnTerm v2 name1 args1
+    (Var v1, Var v2) -> learnVar v1 v2 -- The order shouldn't really matter
+
+unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
+unifyTerms t1 t2 = do
+  lift $ guard $ length t1 == length t2
+  sequenceA_ $ zipWith unify t1 t2
+
+run :: Term String -> UniM (Map.Map String (Term Int))
+run t = do
+  (t2, vmap) <- understand t
+  satisfy t2
+  traverse (lookupVar . Var) vmap
+
+exampleDb :: [Def String]
+exampleDb =
+  [ Def "food" [Stat "burger" []] []
+  , Def "food" [Stat "sandwich" []] []
+  , Def "meal" [Var "X"] [Stat "food" [Var "X"]]
+  ]
+
+burgerIsMeal :: Term String
+burgerIsMeal = Stat "meal" [Stat "burger" []]
+
+whatIsMeal :: Term String
+whatIsMeal = Stat "meal" [Var "X"]

From 2b88420a2a9f9525fa4a8983a76de80a0fb2c048 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Fri, 11 Dec 2020 16:59:56 +0000
Subject: [PATCH 11/39] Rename from props to propa-tools

---
 README.md                              |  5 +++--
 package.yaml                           |  6 +++---
 props.cabal => propa-tools.cabal       | 18 ++++++++----------
 src/{Props => Propa}/Lambda/Display.hs |  4 ++--
 src/{Props => Propa}/Lambda/Term.hs    |  2 +-
 src/{Props => Propa}/Prolog.hs         |  2 +-
 6 files changed, 18 insertions(+), 19 deletions(-)
 rename props.cabal => propa-tools.cabal (78%)
 rename src/{Props => Propa}/Lambda/Display.hs (98%)
 rename src/{Props => Propa}/Lambda/Term.hs (98%)
 rename src/{Props => Propa}/Prolog.hs (99%)

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/package.yaml b/package.yaml
index b6c0015..a20f19a 100644
--- a/package.yaml
+++ b/package.yaml
@@ -1,4 +1,4 @@
-name: props
+name: propa-tools
 version: 0.1.0.0
 license: MIT
 author: Garmelon <joscha@plugh.de>
@@ -21,7 +21,7 @@ library:
   source-dirs: src
 
 executables:
-  props:
+  propa-tools-exe:
     main: Main.hs
     source-dirs: app
     ghc-options:
@@ -29,4 +29,4 @@ executables:
     - -rtsopts
     - -with-rtsopts=-N
     dependencies:
-    - props
+    - propa-tools
diff --git a/props.cabal b/propa-tools.cabal
similarity index 78%
rename from props.cabal
rename to propa-tools.cabal
index 581e772..5d6bc04 100644
--- a/props.cabal
+++ b/propa-tools.cabal
@@ -3,10 +3,8 @@ cabal-version: 1.18
 -- This file has been generated from package.yaml by hpack version 0.34.2.
 --
 -- see: https://github.com/sol/hpack
---
--- hash: 78cab4f7dbc3221eeb49550721e77438db654b072638fcbe9a383fd915dbf277
 
-name:           props
+name:           propa-tools
 version:        0.1.0.0
 author:         Garmelon <joscha@plugh.de>
 maintainer:     Garmelon <joscha@plugh.de>
@@ -22,11 +20,11 @@ extra-doc-files:
 
 library
   exposed-modules:
-      Props.Lambda.Display
-      Props.Lambda.Term
-      Props.Prolog
+      Propa.Lambda.Display
+      Propa.Lambda.Term
+      Propa.Prolog
   other-modules:
-      Paths_props
+      Paths_propa_tools
   hs-source-dirs:
       src
   build-depends:
@@ -36,17 +34,17 @@ library
     , transformers
   default-language: Haskell2010
 
-executable props
+executable propa-tools-exe
   main-is: Main.hs
   other-modules:
-      Paths_props
+      Paths_propa_tools
   hs-source-dirs:
       app
   ghc-options: -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
     , containers
-    , props
+    , propa-tools
     , text
     , transformers
   default-language: Haskell2010
diff --git a/src/Props/Lambda/Display.hs b/src/Propa/Lambda/Display.hs
similarity index 98%
rename from src/Props/Lambda/Display.hs
rename to src/Propa/Lambda/Display.hs
index 452d6d6..22cca89 100644
--- a/src/Props/Lambda/Display.hs
+++ b/src/Propa/Lambda/Display.hs
@@ -2,7 +2,7 @@
 
 -- | This module contains functions useful for displaying 'Term's.
 
-module Props.Lambda.Display
+module Propa.Lambda.Display
   ( Name
   , findConstNames
   , makeVarNamesUnique
@@ -18,7 +18,7 @@ import           Control.Monad.Trans.State
 import qualified Data.Set                  as Set
 import qualified Data.Text                 as T
 
-import           Props.Lambda.Term
+import           Propa.Lambda.Term
 
 -- | The name of a variable or a constant.
 type Name = T.Text
diff --git a/src/Props/Lambda/Term.hs b/src/Propa/Lambda/Term.hs
similarity index 98%
rename from src/Props/Lambda/Term.hs
rename to src/Propa/Lambda/Term.hs
index 4db56ee..0b801d1 100644
--- a/src/Props/Lambda/Term.hs
+++ b/src/Propa/Lambda/Term.hs
@@ -1,7 +1,7 @@
 -- | This module contains 'Term', the base type for lambda expressions. It also
 -- contains a few utility functions for operating on it.
 
-module Props.Lambda.Term
+module Propa.Lambda.Term
   ( Term(..)
   , vars
   , mapVars
diff --git a/src/Props/Prolog.hs b/src/Propa/Prolog.hs
similarity index 99%
rename from src/Props/Prolog.hs
rename to src/Propa/Prolog.hs
index 3ca4234..cca62a4 100644
--- a/src/Props/Prolog.hs
+++ b/src/Propa/Prolog.hs
@@ -1,4 +1,4 @@
-module Props.Prolog where
+module Propa.Prolog where
 
 import           Control.Monad
 import           Data.Foldable

From b20bbb732e28ebd4722e0f9eab821fd21586da8c Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sat, 12 Dec 2020 17:23:44 +0000
Subject: [PATCH 12/39] Split up Prolog.hs

---
 propa-tools.cabal                        |  3 +-
 src/Propa/Prolog/Types.hs                | 36 ++++++++++++++++
 src/Propa/{Prolog.hs => Prolog/Unify.hs} | 52 ++++--------------------
 3 files changed, 45 insertions(+), 46 deletions(-)
 create mode 100644 src/Propa/Prolog/Types.hs
 rename src/Propa/{Prolog.hs => Prolog/Unify.hs} (71%)

diff --git a/propa-tools.cabal b/propa-tools.cabal
index 5d6bc04..51d278b 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -22,7 +22,8 @@ library
   exposed-modules:
       Propa.Lambda.Display
       Propa.Lambda.Term
-      Propa.Prolog
+      Propa.Prolog.Types
+      Propa.Prolog.Unify
   other-modules:
       Paths_propa_tools
   hs-source-dirs:
diff --git a/src/Propa/Prolog/Types.hs b/src/Propa/Prolog/Types.hs
new file mode 100644
index 0000000..66dc338
--- /dev/null
+++ b/src/Propa/Prolog/Types.hs
@@ -0,0 +1,36 @@
+module Propa.Prolog.Types
+  ( Term(..)
+  , Def(..)
+  ) where
+
+data Term a
+  = Var a
+  | Stat String [Term a]
+  deriving (Show)
+
+instance Functor Term where
+  fmap f (Var a)          = Var $ f a
+  fmap f (Stat name args) = Stat name $ fmap (fmap f) args
+
+instance Foldable Term where
+  foldMap f (Var a)       = f a
+  foldMap f (Stat _ args) = foldMap (foldMap f) args
+
+instance Traversable Term where
+  traverse f (Var a)          = Var <$> f a
+  traverse f (Stat name args) = Stat name <$> traverse (traverse f) args
+
+data Def a = Def String [Term a] [Term a]
+  deriving (Show)
+
+instance Functor Def where
+  fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms)
+
+instance Foldable Def where
+  foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms
+
+instance Traversable Def where
+  traverse f (Def dName dArgs dTerms)
+    =   Def dName
+    <$> traverse (traverse f) dArgs
+    <*> traverse (traverse f) dTerms
diff --git a/src/Propa/Prolog.hs b/src/Propa/Prolog/Unify.hs
similarity index 71%
rename from src/Propa/Prolog.hs
rename to src/Propa/Prolog/Unify.hs
index cca62a4..1aad033 100644
--- a/src/Propa/Prolog.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -1,4 +1,9 @@
-module Propa.Prolog where
+module Propa.Prolog.Unify
+  ( Context(..)
+  , newContext
+  , UniM
+  , run
+  ) where
 
 import           Control.Monad
 import           Data.Foldable
@@ -8,37 +13,7 @@ import           Control.Monad.Trans.State
 import qualified Data.Map                  as Map
 import qualified Data.Set                  as Set
 
-data Term a
-  = Var a
-  | Stat String [Term a]
-  deriving (Show)
-
-instance Functor Term where
-  fmap f (Var a)          = Var $ f a
-  fmap f (Stat name args) = Stat name $ fmap (fmap f) args
-
-instance Foldable Term where
-  foldMap f (Var a)       = f a
-  foldMap f (Stat _ args) = foldMap (foldMap f) args
-
-instance Traversable Term where
-  traverse f (Var a)          = Var <$> f a
-  traverse f (Stat name args) = Stat name <$> traverse (traverse f) args
-
-data Def a = Def String [Term a] [Term a]
-  deriving (Show)
-
-instance Functor Def where
-  fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms)
-
-instance Foldable Def where
-  foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms
-
-instance Traversable Def where
-  traverse f (Def dName dArgs dTerms)
-    =   Def dName
-    <$> traverse (traverse f) dArgs
-    <*> traverse (traverse f) dTerms
+import           Propa.Prolog.Types
 
 data Context = Context
   { cDb     :: [Def String]
@@ -128,16 +103,3 @@ run t = do
   (t2, vmap) <- understand t
   satisfy t2
   traverse (lookupVar . Var) vmap
-
-exampleDb :: [Def String]
-exampleDb =
-  [ Def "food" [Stat "burger" []] []
-  , Def "food" [Stat "sandwich" []] []
-  , Def "meal" [Var "X"] [Stat "food" [Var "X"]]
-  ]
-
-burgerIsMeal :: Term String
-burgerIsMeal = Stat "meal" [Stat "burger" []]
-
-whatIsMeal :: Term String
-whatIsMeal = Stat "meal" [Var "X"]

From 2803808116491c6aaf481da86b9add11314be116 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sat, 12 Dec 2020 17:24:23 +0000
Subject: [PATCH 13/39] Use T.Text instead of String

---
 src/Propa/Prolog/Types.hs |  9 +++++++--
 src/Propa/Prolog/Unify.hs | 15 ++++++++-------
 2 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/Propa/Prolog/Types.hs b/src/Propa/Prolog/Types.hs
index 66dc338..4130589 100644
--- a/src/Propa/Prolog/Types.hs
+++ b/src/Propa/Prolog/Types.hs
@@ -1,11 +1,14 @@
 module Propa.Prolog.Types
   ( Term(..)
   , Def(..)
+  , Db
   ) where
 
+import qualified Data.Text as T
+
 data Term a
   = Var a
-  | Stat String [Term a]
+  | Stat T.Text [Term a]
   deriving (Show)
 
 instance Functor Term where
@@ -20,7 +23,7 @@ instance Traversable Term where
   traverse f (Var a)          = Var <$> f a
   traverse f (Stat name args) = Stat name <$> traverse (traverse f) args
 
-data Def a = Def String [Term a] [Term a]
+data Def a = Def T.Text [Term a] [Term a]
   deriving (Show)
 
 instance Functor Def where
@@ -34,3 +37,5 @@ instance Traversable Def where
     =   Def dName
     <$> traverse (traverse f) dArgs
     <*> traverse (traverse f) dTerms
+
+type Db a = [Def a]
diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 1aad033..2d79486 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -12,23 +12,24 @@ 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
 
 data Context = Context
-  { cDb     :: [Def String]
+  { cDb     :: Db T.Text
   , cVarIdx :: Int
   , cVars   :: Map.Map Int Int
-  , cTerms  :: Map.Map Int (String, [Term Int])
+  , cTerms  :: Map.Map Int (T.Text, [Term Int])
   } deriving (Show)
 
-newContext :: [Def String] -> Context
+newContext :: [Def T.Text] -> Context
 newContext db = Context db 0 Map.empty Map.empty
 
 learnVar :: Int -> Int -> UniM ()
 learnVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
 
-learnTerm :: Int -> String -> [Term Int] -> UniM ()
+learnTerm :: Int -> T.Text -> [Term Int] -> UniM ()
 learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c}
 
 -- | Look up a variable, first in the var map and then the term map. Returns
@@ -53,7 +54,7 @@ type UniM = StateT Context []
 fastNub :: (Ord a) => [a] -> [a]
 fastNub = Set.toList . Set.fromList
 
-varMap :: (Foldable a) => a String -> UniM (Map.Map String Int)
+varMap :: (Foldable a) => a T.Text -> UniM (Map.Map T.Text Int)
 varMap a = do
   c <- get
   let i = cVarIdx c
@@ -64,7 +65,7 @@ varMap a = do
 
 -- | Convert a definition's variables to unique integers that are not already in
 -- use in the current context.
-understand :: (Functor a, Foldable a) => a String -> UniM (a Int, Map.Map String Int)
+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)
@@ -98,7 +99,7 @@ unifyTerms t1 t2 = do
   lift $ guard $ length t1 == length t2
   sequenceA_ $ zipWith unify t1 t2
 
-run :: Term String -> UniM (Map.Map String (Term Int))
+run :: Term T.Text -> UniM (Map.Map T.Text (Term Int))
 run t = do
   (t2, vmap) <- understand t
   satisfy t2

From 3aa3cb9f4116b941d16838115bac88918e894ee3 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sat, 12 Dec 2020 17:56:27 +0000
Subject: [PATCH 14/39] Encapsulate unification

Now, only a single "run" function is exported that properly performs unification
and outputs a term with nice variable names again.
---
 src/Propa/Prolog/Unify.hs | 48 +++++++++++++++++++++++++++++----------
 1 file changed, 36 insertions(+), 12 deletions(-)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 2d79486..b438939 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -1,12 +1,13 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Propa.Prolog.Unify
-  ( Context(..)
-  , newContext
-  , UniM
-  , run
+  ( run
   ) where
 
 import           Control.Monad
 import           Data.Foldable
+import           Data.List
+import           Data.Tuple
 
 import           Control.Monad.Trans.Class
 import           Control.Monad.Trans.State
@@ -32,10 +33,10 @@ learnVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
 learnTerm :: Int -> T.Text -> [Term Int] -> UniM ()
 learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c}
 
--- | Look up a variable, first in the var map and then the term map. Returns
--- statements unchanged.
+-- | 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 unbound.
+-- If this returns a variable, then that variable is not bound.
 lookupVar :: Term Int -> UniM (Term Int)
 lookupVar t@(Stat _ _) = pure t
 lookupVar t@(Var v) = do
@@ -99,8 +100,31 @@ unifyTerms t1 t2 = do
   lift $ guard $ length t1 == length t2
   sequenceA_ $ zipWith unify t1 t2
 
-run :: Term T.Text -> UniM (Map.Map T.Text (Term Int))
-run t = do
-  (t2, vmap) <- understand t
-  satisfy t2
-  traverse (lookupVar . Var) vmap
+varNames :: [T.Text]
+varNames = do
+  num <- "" : map (T.pack . show) [(1::Integer)..]
+  char <- alphabet
+  pure $ char <> num
+  where
+    alphabet = map T.singleton ['A'..'Z']
+
+findVarNaming :: Map.Map T.Text Int -> [Term Int] -> Map.Map Int T.Text
+findVarNaming known terms =
+  let knownNaming = Map.fromList $ map swap $ Map.toList known
+      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
+
+run :: Db T.Text -> Term T.Text -> [Map.Map T.Text (Term T.Text)]
+run db t = map fst $ runStateT helper $ newContext db
+  where
+    helper = do
+      (t2, vmap) <- understand t
+      satisfy t2
+      tmap <- traverse (lookupVar . Var) vmap
+      let naming = findVarNaming vmap $ Map.elems tmap
+      pure $ fmap (naming Map.!) <$> tmap

From 6905c7e1cd5e338e999dcc40b04a94fbe5008460 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sat, 12 Dec 2020 20:01:49 +0100
Subject: [PATCH 15/39] Run unification on multiple terms

---
 src/Propa/Prolog/Unify.hs | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index b438939..51cfdf3 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -2,6 +2,7 @@
 
 module Propa.Prolog.Unify
   ( run
+  , runOne
   ) where
 
 import           Control.Monad
@@ -51,7 +52,8 @@ lookupVar t@(Var v) = do
 -- Needs to be changed when implementing cuts.
 type UniM = StateT Context []
 
--- | A faster version of 'nub'.
+-- | A faster version of 'nub' that doesn't preserve order and doesn't work on
+-- infinite lists.
 fastNub :: (Ord a) => [a] -> [a]
 fastNub = Set.toList . Set.fromList
 
@@ -72,7 +74,7 @@ understand a = do
   pure (fmap (vmap Map.!) a, vmap)
 
 satisfy :: Term Int -> UniM ()
-satisfy (Var _)          = undefined
+satisfy (Var _) = pure ()
 satisfy (Stat name args) = do
   c <- get
   (Def dName dArgs dTerms, _) <- understand =<< lift (cDb c)
@@ -119,12 +121,23 @@ findVarNaming known terms =
       unknownNaming = Map.fromList $ zip (sort $ Set.toList unknownVars) availVarNames
   in  knownNaming <> unknownNaming
 
-run :: Db T.Text -> Term T.Text -> [Map.Map T.Text (Term T.Text)]
-run db t = map fst $ runStateT helper $ newContext db
+newtype Terms a = Terms { unTerms :: [Term a] }
+
+instance Functor Terms where
+  fmap f (Terms ts) = Terms $ fmap (fmap f) ts
+
+instance Foldable Terms where
+  foldMap f (Terms ts) = foldMap (foldMap f) ts
+
+run :: Db T.Text -> [Term T.Text] -> [Map.Map T.Text (Term T.Text)]
+run db terms = map fst $ runStateT helper $ newContext db
   where
     helper = do
-      (t2, vmap) <- understand t
-      satisfy t2
+      (terms2, vmap) <- understand $ Terms terms
+      satisfyTerms $ unTerms terms2
       tmap <- traverse (lookupVar . Var) vmap
       let naming = findVarNaming vmap $ Map.elems tmap
       pure $ fmap (naming Map.!) <$> tmap
+
+runOne :: Db T.Text -> Term T.Text -> [Map.Map T.Text (Term T.Text)]
+runOne db term = run db [term]

From 655fe97cbc79f1de4ed8fb75f6d12a0106432a11 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 15:22:56 +0000
Subject: [PATCH 16/39] Fix run output

Now, the run output contains the terms with the variables resolved as far as
possible.
---
 src/Propa/Prolog/Unify.hs | 55 ++++++++++++++++++++++++++-------------
 1 file changed, 37 insertions(+), 18 deletions(-)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 51cfdf3..3b010b2 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -18,6 +18,20 @@ 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) => Map.Map a a -> a -> a
+follow m v = maybe v (follow m) $ m Map.!? v
+
+-- | 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
@@ -39,29 +53,23 @@ learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cT
 --
 -- If this returns a variable, then that variable is not bound.
 lookupVar :: Term Int -> UniM (Term Int)
-lookupVar t@(Stat _ _) = pure t
-lookupVar t@(Var v) = do
+lookupVar (Var v) = do
   c <- get
-  case cVars c Map.!? v of
-    Just v' -> lookupVar (Var v')
-    Nothing -> pure $ case cTerms c Map.!? v of
-      Nothing           -> t
-      Just (name, args) -> Stat name args
+  let lastV = follow (cVars c) v
+  pure $ case cTerms c Map.!? lastV of
+    Nothing           -> Var lastV
+    Just (name, args) -> Stat name args
+lookupVar t@(Stat _ _) = pure t
 
 -- | A simple state monad transformer over the list monad for easy backtracking.
 -- Needs to be changed when implementing cuts.
 type UniM = StateT Context []
 
--- | A faster version of 'nub' that doesn't preserve order and doesn't work on
--- infinite lists.
-fastNub :: (Ord a) => [a] -> [a]
-fastNub = Set.toList . Set.fromList
-
 varMap :: (Foldable a) => a T.Text -> UniM (Map.Map T.Text Int)
 varMap a = do
   c <- get
   let i = cVarIdx c
-      vars = fastNub $ toList a
+      vars = deduplicate $ toList a
       vmap = Map.fromList $ zip vars [i..]
   put c{cVarIdx = i + Map.size vmap}
   pure vmap
@@ -110,9 +118,10 @@ varNames = do
   where
     alphabet = map T.singleton ['A'..'Z']
 
-findVarNaming :: Map.Map T.Text Int -> [Term Int] -> Map.Map Int T.Text
-findVarNaming known terms =
-  let knownNaming = Map.fromList $ map swap $ Map.toList known
+findVarNaming :: Map.Map T.Text Int -> Map.Map Int Int -> [Term Int] -> Map.Map Int T.Text
+findVarNaming known vars terms =
+  let knownLookedUp = fmap (follow vars) known
+      knownNaming = Map.fromList $ reverse $ map swap $ Map.toList knownLookedUp
       knownNames = Map.keysSet known
       knownVars = Map.keysSet knownNaming
       termVars = Set.fromList $ concatMap toList terms
@@ -121,6 +130,15 @@ findVarNaming known terms =
       unknownNaming = Map.fromList $ zip (sort $ Set.toList unknownVars) availVarNames
   in  knownNaming <> unknownNaming
 
+resolveVars :: Term Int -> UniM (Term Int)
+resolveVars t = do
+  t2 <- lookupVar t
+  case t2 of
+    (Var v) -> pure $ Var v
+    (Stat name args) -> do
+      args2 <- traverse resolveVars args
+      pure $ Stat name args2
+
 newtype Terms a = Terms { unTerms :: [Term a] }
 
 instance Functor Terms where
@@ -135,8 +153,9 @@ run db terms = map fst $ runStateT helper $ newContext db
     helper = do
       (terms2, vmap) <- understand $ Terms terms
       satisfyTerms $ unTerms terms2
-      tmap <- traverse (lookupVar . Var) vmap
-      let naming = findVarNaming vmap $ Map.elems tmap
+      tmap <- traverse (resolveVars . Var) vmap
+      c <- get
+      let naming = findVarNaming vmap (cVars c) $ Map.elems tmap
       pure $ fmap (naming Map.!) <$> tmap
 
 runOne :: Db T.Text -> Term T.Text -> [Map.Map T.Text (Term T.Text)]

From 52310c766f5ec8a7216932196d95ed38b01cecca Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 19:01:37 +0000
Subject: [PATCH 17/39] Add example terms for testing

---
 propa-tools.cabal           |  1 +
 src/Propa/Prolog/Example.hs | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 src/Propa/Prolog/Example.hs

diff --git a/propa-tools.cabal b/propa-tools.cabal
index 51d278b..4d4c553 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -22,6 +22,7 @@ library
   exposed-modules:
       Propa.Lambda.Display
       Propa.Lambda.Term
+      Propa.Prolog.Example
       Propa.Prolog.Types
       Propa.Prolog.Unify
   other-modules:
diff --git a/src/Propa/Prolog/Example.hs b/src/Propa/Prolog/Example.hs
new file mode 100644
index 0000000..91ded59
--- /dev/null
+++ b/src/Propa/Prolog/Example.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Example where
+
+import qualified Data.Text          as T
+
+import           Propa.Prolog.Types
+
+db :: Db T.Text
+db =
+  [ Def "append" [Stat "nil" [], Var "Y", Var "Y"] []
+  , Def "append" [Stat "cons" [Var "X", Var "XS"], Var "Y", Stat "cons" [Var "X", Var "Z"]] [Stat "append" [Var "XS", Var "Y", Var "Z"]]
+  ]
+
+l12 :: Term T.Text
+l12 = Stat "cons" [Stat "1" [], Stat "cons" [Stat "2" [], Stat "nil" []]]
+
+l345 :: Term T.Text
+l345 = Stat "cons" [Stat "3" [], Stat "cons" [Stat "4" [], Stat "cons" [Stat "5" [], Stat "nil" []]]]

From 18e5acd6931b5fc8fbb60e47942b3ec1c9af585d Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 19:01:55 +0000
Subject: [PATCH 18/39] Convert terms and definitions to strings

---
 propa-tools.cabal           |  1 +
 src/Propa/Prolog/Display.hs | 39 +++++++++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 src/Propa/Prolog/Display.hs

diff --git a/propa-tools.cabal b/propa-tools.cabal
index 4d4c553..0286fc7 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -22,6 +22,7 @@ library
   exposed-modules:
       Propa.Lambda.Display
       Propa.Lambda.Term
+      Propa.Prolog.Display
       Propa.Prolog.Example
       Propa.Prolog.Types
       Propa.Prolog.Unify
diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
new file mode 100644
index 0000000..17fb399
--- /dev/null
+++ b/src/Propa/Prolog/Display.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Display
+  ( displayTerm
+  , displayTerms
+  , displayDef
+  , displayDefs
+  , displayResult
+  ) where
+
+import qualified Data.Map           as Map
+import qualified Data.Text          as T
+
+import           Propa.Prolog.Types
+
+displayStat :: T.Text -> [Term T.Text] -> T.Text
+displayStat name []   = name
+displayStat name args = name <> "(" <> T.intercalate ", " (map displayTerm args) <> ")"
+
+displayTerm :: Term T.Text -> T.Text
+displayTerm (Var v)          = v
+displayTerm (Stat name args) = displayStat name args
+
+displayTerms :: [Term T.Text] -> T.Text
+displayTerms terms = T.intercalate ",\n" (map displayTerm terms) <> "."
+
+displayDef :: Def T.Text -> T.Text
+displayDef (Def name args []) = displayStat name args <> "."
+displayDef (Def name args terms)
+  =  displayStat name args
+  <> " :-\n"
+  <> T.intercalate ",\n" (map (\t -> "    " <> displayTerm t) terms)
+  <> "."
+
+displayDefs :: [Def T.Text] -> T.Text
+displayDefs = T.intercalate "\n" . map displayDef
+
+displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
+displayResult = T.intercalate "\n" . map (\(k, v) -> k <> " = " <> displayTerm v) . Map.assocs

From 60c2c2fe6dd38d1761153acc160ce94331f12520 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 20:09:19 +0000
Subject: [PATCH 19/39] Parse terms and definitions

---
 package.yaml              |  1 +
 propa-tools.cabal         |  3 ++
 src/Propa/Prolog/Parse.hs | 81 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+)
 create mode 100644 src/Propa/Prolog/Parse.hs

diff --git a/package.yaml b/package.yaml
index a20f19a..497600f 100644
--- a/package.yaml
+++ b/package.yaml
@@ -14,6 +14,7 @@ extra-doc-files:
 dependencies:
 - base >= 4.7 && < 5
 - containers
+- megaparsec
 - text
 - transformers
 
diff --git a/propa-tools.cabal b/propa-tools.cabal
index 0286fc7..e95a440 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -24,6 +24,7 @@ library
       Propa.Lambda.Term
       Propa.Prolog.Display
       Propa.Prolog.Example
+      Propa.Prolog.Parse
       Propa.Prolog.Types
       Propa.Prolog.Unify
   other-modules:
@@ -33,6 +34,7 @@ library
   build-depends:
       base >=4.7 && <5
     , containers
+    , megaparsec
     , text
     , transformers
   default-language: Haskell2010
@@ -47,6 +49,7 @@ executable propa-tools-exe
   build-depends:
       base >=4.7 && <5
     , containers
+    , megaparsec
     , propa-tools
     , text
     , transformers
diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
new file mode 100644
index 0000000..f26a2ac
--- /dev/null
+++ b/src/Propa/Prolog/Parse.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Propa.Prolog.Parse
+  ( parseTerms
+  , parseDb
+  ) where
+
+import           Control.Monad
+import           Data.Bifunctor
+import           Data.Char
+import           Data.Void
+
+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 ")")
+
+-- Building blocks
+
+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
+
+pStat :: Parser (T.Text, [Term T.Text])
+pStat = do
+  name <- pName
+  terms <- parens (pTerm `sepBy1` symbol ",") <|> pure []
+  pure (name, terms)
+
+pTerm :: Parser (Term T.Text)
+pTerm = (Var <$> pVarName) <|> (uncurry Stat <$> pStat)
+
+pTerms :: Parser [Term T.Text]
+pTerms = (pTerm `sepBy1` symbol ",") <* symbol "."
+
+pDef :: Parser (Def T.Text)
+pDef = do
+  name <- pName
+  args <- parens (pTerm `sepBy1` symbol ",") <|> pure []
+  terms <- (symbol ":-" *> (pTerm `sepBy1` symbol ",")) <|> pure []
+  void $ symbol "."
+  pure $ Def name args terms
+
+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) path input
+
+parseTerms :: FilePath -> T.Text -> Either T.Text [Term T.Text]
+parseTerms = parseHelper pTerms
+
+parseDb :: FilePath -> T.Text -> Either T.Text (Db T.Text)
+parseDb = parseHelper pDefs

From 10ab319620e09004158604f853191e963c58f882 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 20:23:28 +0000
Subject: [PATCH 20/39] Filter out results of type "A = A"

---
 src/Propa/Prolog/Display.hs | 6 +++++-
 src/Propa/Prolog/Types.hs   | 2 +-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index 17fb399..46d84f2 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -36,4 +36,8 @@ displayDefs :: [Def T.Text] -> T.Text
 displayDefs = T.intercalate "\n" . map displayDef
 
 displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
-displayResult = T.intercalate "\n" . map (\(k, v) -> k <> " = " <> displayTerm v) . Map.assocs
+displayResult
+  = T.intercalate "\n"
+  . map (\(k, v) -> k <> " = " <> displayTerm v)
+  . filter (\(k, v) -> v /= Var k)
+  . Map.assocs
diff --git a/src/Propa/Prolog/Types.hs b/src/Propa/Prolog/Types.hs
index 4130589..d526509 100644
--- a/src/Propa/Prolog/Types.hs
+++ b/src/Propa/Prolog/Types.hs
@@ -9,7 +9,7 @@ import qualified Data.Text as T
 data Term a
   = Var a
   | Stat T.Text [Term a]
-  deriving (Show)
+  deriving (Show, Eq)
 
 instance Functor Term where
   fmap f (Var a)          = Var $ f a

From 8a81cd9e774012b74346346a7c93c6d70899078d Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 20:23:44 +0000
Subject: [PATCH 21/39] Add Debug module for easier testing

---
 propa-tools.cabal         |  1 +
 src/Propa/Prolog/Debug.hs | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 src/Propa/Prolog/Debug.hs

diff --git a/propa-tools.cabal b/propa-tools.cabal
index e95a440..6e42b52 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -22,6 +22,7 @@ library
   exposed-modules:
       Propa.Lambda.Display
       Propa.Lambda.Term
+      Propa.Prolog.Debug
       Propa.Prolog.Display
       Propa.Prolog.Example
       Propa.Prolog.Parse
diff --git a/src/Propa/Prolog/Debug.hs b/src/Propa/Prolog/Debug.hs
new file mode 100644
index 0000000..1814ad7
--- /dev/null
+++ b/src/Propa/Prolog/Debug.hs
@@ -0,0 +1,18 @@
+{-# 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 :: T.Text -> T.Text -> IO ()
+parseAndRun dbText termsText = T.putStrLn $ either id id $ do
+  db <- parseDb "<input>" dbText
+  terms <- parseTerms "<input>" termsText
+  pure $ T.intercalate "\n" $ map displayResult $ run db terms

From 659f1a9d33761976fb52a2c446317e8aff2141c4 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 20:31:48 +0000
Subject: [PATCH 22/39] Parse until eof

---
 src/Propa/Prolog/Parse.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index f26a2ac..3a239ef 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -72,7 +72,7 @@ pDefs = many pDef
 parseHelper :: Parser a -> FilePath -> T.Text -> Either T.Text a
 parseHelper p path input
   = first (T.pack . errorBundlePretty)
-  $ parse (space *> p) path input
+  $ parse (space *> p <* eof) path input
 
 parseTerms :: FilePath -> T.Text -> Either T.Text [Term T.Text]
 parseTerms = parseHelper pTerms

From adebcdd26cae287a2924061b47ee7f2c1aeec906 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 20:35:49 +0000
Subject: [PATCH 23/39] Add some comments

---
 src/Propa/Prolog/Unify.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 3b010b2..e16994f 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -110,6 +110,8 @@ unifyTerms t1 t2 = do
   lift $ guard $ length t1 == length t2
   sequenceA_ $ zipWith unify t1 t2
 
+-- Figuring out how to display the result of the unification
+
 varNames :: [T.Text]
 varNames = do
   num <- "" : map (T.pack . show) [(1::Integer)..]
@@ -139,6 +141,7 @@ resolveVars t = do
       args2 <- traverse resolveVars args
       pure $ Stat name args2
 
+-- | Helper type so I can resolve variables in multiple terms simultaneously.
 newtype Terms a = Terms { unTerms :: [Term a] }
 
 instance Functor Terms where

From 0d52c07f681cbe8bf48ef92c3db98d9c5f2871d9 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 20:51:56 +0000
Subject: [PATCH 24/39] Parse lists

Correctly printing them comes next.
---
 src/Propa/Prolog/Parse.hs | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index 3a239ef..ac85a11 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -33,6 +33,9 @@ symbol = L.symbol space
 parens :: Parser a -> Parser a
 parens = between (symbol "(") (symbol ")")
 
+brackets :: Parser a -> Parser a
+brackets = between (symbol "[") (symbol "]")
+
 -- Building blocks
 
 pName :: Parser T.Text
@@ -44,6 +47,18 @@ pName = lexeme $ unquotedName <|> quotedName
 pVarName :: Parser T.Text
 pVarName = lexeme $ takeWhile1P (Just "uppercase character") isUpper
 
+pCons :: Parser (Term T.Text)
+pCons = brackets $ do
+  elems <- pTerm `sepBy1` symbol ","
+  void $ symbol "|"
+  rest <- pTerm
+  pure $ foldr (\a b -> Stat "[|]" [a, b]) rest elems
+
+pList :: Parser (Term T.Text)
+pList = do
+  elems <- brackets $ pTerm `sepBy` symbol ","
+  pure $ foldr (\a b -> Stat "[|]" [a, b]) (Stat "[]" []) elems
+
 pStat :: Parser (T.Text, [Term T.Text])
 pStat = do
   name <- pName
@@ -51,7 +66,11 @@ pStat = do
   pure (name, terms)
 
 pTerm :: Parser (Term T.Text)
-pTerm = (Var <$> pVarName) <|> (uncurry Stat <$> pStat)
+pTerm
+  =   (Var <$> pVarName)
+  <|> (uncurry Stat <$> pStat)
+  <|> try pCons
+  <|> pList
 
 pTerms :: Parser [Term T.Text]
 pTerms = (pTerm `sepBy1` symbol ",") <* symbol "."

From 2d5a8ece55d53decbe06f8520a0b2d3671d18f44 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 21:04:15 +0000
Subject: [PATCH 25/39] Display lists

---
 src/Propa/Prolog/Display.hs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index 46d84f2..436784a 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -17,9 +17,15 @@ displayStat :: T.Text -> [Term T.Text] -> T.Text
 displayStat name []   = name
 displayStat name args = name <> "(" <> T.intercalate ", " (map displayTerm args) <> ")"
 
+displayList :: Term T.Text -> T.Text
+displayList (Stat "[|]" [a, b]) = "," <> displayTerm a <> displayList b
+displayList (Stat "[]" [])      = "]"
+displayList t                   = "|" <> displayTerm t <> "]"
+
 displayTerm :: Term T.Text -> T.Text
-displayTerm (Var v)          = v
-displayTerm (Stat name args) = displayStat name args
+displayTerm (Var v)             = v
+displayTerm (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b
+displayTerm (Stat name args)    = displayStat name args
 
 displayTerms :: [Term T.Text] -> T.Text
 displayTerms terms = T.intercalate ",\n" (map displayTerm terms) <> "."

From e4e5c801f305bd89d6b94ee1d8acefb6813b18a8 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 21:19:24 +0000
Subject: [PATCH 26/39] Escape names properly

---
 src/Propa/Prolog/Display.hs | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index 436784a..acd15b7 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -8,14 +8,33 @@ module Propa.Prolog.Display
   , 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 :: T.Text -> [Term T.Text] -> T.Text
-displayStat name []   = name
-displayStat name args = name <> "(" <> T.intercalate ", " (map displayTerm args) <> ")"
+displayStat name [] = displayName name
+displayStat name args
+  = displayName name
+  <> "("
+  <> T.intercalate ", " (map displayTerm args)
+  <> ")"
 
 displayList :: Term T.Text -> T.Text
 displayList (Stat "[|]" [a, b]) = "," <> displayTerm a <> displayList b

From 1547561fa5123f2357fb64111c233844292b4a1b Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 21:55:24 +0000
Subject: [PATCH 27/39] Switch name quotes to single quotes

---
 src/Propa/Prolog/Parse.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index ac85a11..6aba6b4 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -42,7 +42,7 @@ 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 '"')
+    quotedName = fmap T.pack $ C.char '\'' *> manyTill L.charLiteral (C.char '\'')
 
 pVarName :: Parser T.Text
 pVarName = lexeme $ takeWhile1P (Just "uppercase character") isUpper

From 744091de01821e65c14f004605a7306e0c8f7ee4 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 21:56:47 +0000
Subject: [PATCH 28/39] Parse expressions

Only '=' for now.
---
 package.yaml              |  1 +
 propa-tools.cabal         |  2 ++
 src/Propa/Prolog/Parse.hs | 21 +++++++++++++++------
 3 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/package.yaml b/package.yaml
index 497600f..ea4d11c 100644
--- a/package.yaml
+++ b/package.yaml
@@ -15,6 +15,7 @@ dependencies:
 - base >= 4.7 && < 5
 - containers
 - megaparsec
+- parser-combinators
 - text
 - transformers
 
diff --git a/propa-tools.cabal b/propa-tools.cabal
index 6e42b52..2ac17e0 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -36,6 +36,7 @@ library
       base >=4.7 && <5
     , containers
     , megaparsec
+    , parser-combinators
     , text
     , transformers
   default-language: Haskell2010
@@ -51,6 +52,7 @@ executable propa-tools-exe
       base >=4.7 && <5
     , containers
     , megaparsec
+    , parser-combinators
     , propa-tools
     , text
     , transformers
diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index 6aba6b4..004b15e 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -10,10 +10,11 @@ import           Data.Bifunctor
 import           Data.Char
 import           Data.Void
 
-import qualified Data.Text                  as T
+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 qualified Text.Megaparsec.Char           as C
+import qualified Text.Megaparsec.Char.Lexer     as L
 
 import           Propa.Prolog.Types
 
@@ -71,15 +72,23 @@ pTerm
   <|> (uncurry Stat <$> pStat)
   <|> try pCons
   <|> pList
+  <|> parens pExpr
+
+pExpr :: Parser (Term T.Text)
+pExpr = makeExprParser pTerm
+  [ [ binary "=" ]
+  ]
+  where
+    binary name = InfixL $ (\a b -> Stat name [a, b]) <$ symbol name
 
 pTerms :: Parser [Term T.Text]
-pTerms = (pTerm `sepBy1` symbol ",") <* symbol "."
+pTerms = (pExpr `sepBy1` symbol ",") <* symbol "."
 
 pDef :: Parser (Def T.Text)
 pDef = do
   name <- pName
-  args <- parens (pTerm `sepBy1` symbol ",") <|> pure []
-  terms <- (symbol ":-" *> (pTerm `sepBy1` symbol ",")) <|> pure []
+  args <- parens (pExpr `sepBy1` symbol ",") <|> pure []
+  terms <- (symbol ":-" *> (pExpr `sepBy1` symbol ",")) <|> pure []
   void $ symbol "."
   pure $ Def name args terms
 

From 90669d01f28d0d94c5cc54edc96bc358c99d5033 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 23:23:37 +0000
Subject: [PATCH 29/39] Remove examples for testing

---
 propa-tools.cabal           |  1 -
 src/Propa/Prolog/Example.hs | 19 -------------------
 2 files changed, 20 deletions(-)
 delete mode 100644 src/Propa/Prolog/Example.hs

diff --git a/propa-tools.cabal b/propa-tools.cabal
index 2ac17e0..8a5af23 100644
--- a/propa-tools.cabal
+++ b/propa-tools.cabal
@@ -24,7 +24,6 @@ library
       Propa.Lambda.Term
       Propa.Prolog.Debug
       Propa.Prolog.Display
-      Propa.Prolog.Example
       Propa.Prolog.Parse
       Propa.Prolog.Types
       Propa.Prolog.Unify
diff --git a/src/Propa/Prolog/Example.hs b/src/Propa/Prolog/Example.hs
deleted file mode 100644
index 91ded59..0000000
--- a/src/Propa/Prolog/Example.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Propa.Prolog.Example where
-
-import qualified Data.Text          as T
-
-import           Propa.Prolog.Types
-
-db :: Db T.Text
-db =
-  [ Def "append" [Stat "nil" [], Var "Y", Var "Y"] []
-  , Def "append" [Stat "cons" [Var "X", Var "XS"], Var "Y", Stat "cons" [Var "X", Var "Z"]] [Stat "append" [Var "XS", Var "Y", Var "Z"]]
-  ]
-
-l12 :: Term T.Text
-l12 = Stat "cons" [Stat "1" [], Stat "cons" [Stat "2" [], Stat "nil" []]]
-
-l345 :: Term T.Text
-l345 = Stat "cons" [Stat "3" [], Stat "cons" [Stat "4" [], Stat "cons" [Stat "5" [], Stat "nil" []]]]

From d90f2c6a2c1f8281bde77374e30742fbbe723091 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 23:23:59 +0000
Subject: [PATCH 30/39] Separate out Stat from Term

---
 src/Propa/Prolog/Debug.hs   |  6 +--
 src/Propa/Prolog/Display.hs | 28 ++++++------
 src/Propa/Prolog/Parse.hs   | 33 +++++++-------
 src/Propa/Prolog/Types.hs   | 42 +++++++++++-------
 src/Propa/Prolog/Unify.hs   | 86 ++++++++++++++++++-------------------
 5 files changed, 100 insertions(+), 95 deletions(-)

diff --git a/src/Propa/Prolog/Debug.hs b/src/Propa/Prolog/Debug.hs
index 1814ad7..b9f1971 100644
--- a/src/Propa/Prolog/Debug.hs
+++ b/src/Propa/Prolog/Debug.hs
@@ -12,7 +12,7 @@ import           Propa.Prolog.Parse
 import           Propa.Prolog.Unify
 
 parseAndRun :: T.Text -> T.Text -> IO ()
-parseAndRun dbText termsText = T.putStrLn $ either id id $ do
+parseAndRun dbText statsText = T.putStrLn $ either id id $ do
   db <- parseDb "<input>" dbText
-  terms <- parseTerms "<input>" termsText
-  pure $ T.intercalate "\n" $ map displayResult $ run db terms
+  stats <- parseStats "<input>" statsText
+  pure $ T.intercalate "\n" $ map displayResult $ run db stats
diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index acd15b7..79608b6 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -28,33 +28,33 @@ displayName name
       , ("\t", "\\t")
       ]
 
-displayStat :: T.Text -> [Term T.Text] -> T.Text
-displayStat name [] = displayName name
-displayStat name args
+displayStat :: Stat T.Text -> T.Text
+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 (Stat "[|]" [a, b]) = "," <> displayTerm a <> displayList b
-displayList (Stat "[]" [])      = "]"
-displayList t                   = "|" <> displayTerm t <> "]"
+displayList (TStat (Stat "[|]" [a, b])) = "," <> displayTerm a <> displayList b
+displayList (TStat (Stat "[]" []))      = "]"
+displayList t                           = "|" <> displayTerm t <> "]"
 
 displayTerm :: Term T.Text -> T.Text
-displayTerm (Var v)             = v
-displayTerm (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b
-displayTerm (Stat name args)    = displayStat name args
+displayTerm (TVar v)  = v
+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 name args []) = displayStat name args <> "."
-displayDef (Def name args terms)
-  =  displayStat name args
+displayDef (Def stat []) = displayStat stat <> "."
+displayDef (Def stat stats)
+  =  displayStat stat
   <> " :-\n"
-  <> T.intercalate ",\n" (map (\t -> "    " <> displayTerm t) terms)
+  <> T.intercalate ",\n" (map (\t -> "    " <> displayStat t) stats)
   <> "."
 
 displayDefs :: [Def T.Text] -> T.Text
@@ -64,5 +64,5 @@ displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
 displayResult
   = T.intercalate "\n"
   . map (\(k, v) -> k <> " = " <> displayTerm v)
-  . filter (\(k, v) -> v /= Var k)
+  . filter (\(k, v) -> v /= TVar k)
   . Map.assocs
diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index 004b15e..682d24e 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Propa.Prolog.Parse
-  ( parseTerms
+  ( parseStats
   , parseDb
   ) where
 
@@ -53,23 +53,26 @@ pCons = brackets $ do
   elems <- pTerm `sepBy1` symbol ","
   void $ symbol "|"
   rest <- pTerm
-  pure $ foldr (\a b -> Stat "[|]" [a, b]) rest elems
+  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 -> Stat "[|]" [a, b]) (Stat "[]" []) elems
+  pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems
 
-pStat :: Parser (T.Text, [Term T.Text])
+pStat :: Parser (Stat T.Text)
 pStat = do
   name <- pName
   terms <- parens (pTerm `sepBy1` symbol ",") <|> pure []
-  pure (name, terms)
+  pure $ Stat name terms
+
+pStats :: Parser [Stat T.Text]
+pStats = (pStat `sepBy1` symbol ",") <* symbol "."
 
 pTerm :: Parser (Term T.Text)
 pTerm
-  =   (Var <$> pVarName)
-  <|> (uncurry Stat <$> pStat)
+  =   (TVar <$> pVarName)
+  <|> (TStat <$> pStat)
   <|> try pCons
   <|> pList
   <|> parens pExpr
@@ -79,18 +82,14 @@ pExpr = makeExprParser pTerm
   [ [ binary "=" ]
   ]
   where
-    binary name = InfixL $ (\a b -> Stat name [a, b]) <$ symbol name
-
-pTerms :: Parser [Term T.Text]
-pTerms = (pExpr `sepBy1` symbol ",") <* symbol "."
+    binary name = InfixL $ (\a b -> TStat $ Stat name [a, b]) <$ symbol name
 
 pDef :: Parser (Def T.Text)
 pDef = do
-  name <- pName
-  args <- parens (pExpr `sepBy1` symbol ",") <|> pure []
-  terms <- (symbol ":-" *> (pExpr `sepBy1` symbol ",")) <|> pure []
+  stat <- pStat
+  stats <- (symbol ":-" *> (pStat `sepBy1` symbol ",")) <|> pure []
   void $ symbol "."
-  pure $ Def name args terms
+  pure $ Def stat stats
 
 pDefs :: Parser [Def T.Text]
 pDefs = many pDef
@@ -102,8 +101,8 @@ parseHelper p path input
   = first (T.pack . errorBundlePretty)
   $ parse (space *> p <* eof) path input
 
-parseTerms :: FilePath -> T.Text -> Either T.Text [Term T.Text]
-parseTerms = parseHelper pTerms
+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
index d526509..485f44b 100644
--- a/src/Propa/Prolog/Types.hs
+++ b/src/Propa/Prolog/Types.hs
@@ -1,41 +1,51 @@
 module Propa.Prolog.Types
-  ( Term(..)
+  ( Stat(..)
+  , Term(..)
   , 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
-  = Var a
-  | Stat T.Text [Term a]
+  = TVar a
+  | TStat (Stat a)
   deriving (Show, Eq)
 
 instance Functor Term where
-  fmap f (Var a)          = Var $ f a
-  fmap f (Stat name args) = Stat name $ fmap (fmap f) args
+  fmap f (TVar a)  = TVar $ f a
+  fmap f (TStat s) = TStat $ fmap f s
 
 instance Foldable Term where
-  foldMap f (Var a)       = f a
-  foldMap f (Stat _ args) = foldMap (foldMap f) args
+  foldMap f (TVar a)  = f a
+  foldMap f (TStat s) = foldMap f s
 
 instance Traversable Term where
-  traverse f (Var a)          = Var <$> f a
-  traverse f (Stat name args) = Stat name <$> traverse (traverse f) args
+  traverse f (TVar a)  = TVar <$> f a
+  traverse f (TStat s) = TStat <$> traverse f s
 
-data Def a = Def T.Text [Term a] [Term a]
+data Def a = Def (Stat a) [Stat a]
   deriving (Show)
 
 instance Functor Def where
-  fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms)
+  fmap f (Def stat stats) = Def (fmap f stat) (fmap f <$> stats)
 
 instance Foldable Def where
-  foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms
+  foldMap f (Def stat stats) = foldMap f stat <> foldMap (foldMap f) stats
 
 instance Traversable Def where
-  traverse f (Def dName dArgs dTerms)
-    =   Def dName
-    <$> traverse (traverse f) dArgs
-    <*> traverse (traverse f) dTerms
+  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
index e16994f..2caae9f 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -2,7 +2,6 @@
 
 module Propa.Prolog.Unify
   ( run
-  , runOne
   ) where
 
 import           Control.Monad
@@ -36,30 +35,30 @@ data Context = Context
   { cDb     :: Db T.Text
   , cVarIdx :: Int
   , cVars   :: Map.Map Int Int
-  , cTerms  :: Map.Map Int (T.Text, [Term Int])
+  , cStats  :: Map.Map Int (Stat Int)
   } deriving (Show)
 
 newContext :: [Def T.Text] -> Context
 newContext db = Context db 0 Map.empty Map.empty
 
-learnVar :: Int -> Int -> UniM ()
-learnVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
+bindVar :: Int -> Int -> UniM ()
+bindVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
 
-learnTerm :: Int -> T.Text -> [Term Int] -> UniM ()
-learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c}
+bindStat :: Int -> Stat Int -> UniM ()
+bindStat k s = modify $ \c -> c{cStats = Map.insert k s $ cStats 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.
 lookupVar :: Term Int -> UniM (Term Int)
-lookupVar (Var v) = do
+lookupVar (TVar v) = do
   c <- get
   let lastV = follow (cVars c) v
-  pure $ case cTerms c Map.!? lastV of
-    Nothing           -> Var lastV
-    Just (name, args) -> Stat name args
-lookupVar t@(Stat _ _) = pure t
+  pure $ case cStats c Map.!? lastV of
+    Nothing -> TVar lastV
+    Just s  -> TStat s
+lookupVar t@(TStat _) = pure t
 
 -- | A simple state monad transformer over the list monad for easy backtracking.
 -- Needs to be changed when implementing cuts.
@@ -81,33 +80,34 @@ understand a = do
   vmap <- varMap a
   pure (fmap (vmap Map.!) a, vmap)
 
-satisfy :: Term Int -> UniM ()
-satisfy (Var _) = pure ()
-satisfy (Stat name args) = do
+satisfy :: Stat Int -> UniM ()
+satisfy s = do
   c <- get
-  (Def dName dArgs dTerms, _) <- understand =<< lift (cDb c)
-  lift $ guard $ name == dName -- Not sure if 'lift' is really necessary
-  unifyTerms args dArgs
-  satisfyTerms dTerms
+  (Def dStat dStats, _) <- understand =<< lift (cDb c)
+  unifyStat s dStat
+  satisfyStats dStats
 
-satisfyTerms :: [Term Int] -> UniM ()
-satisfyTerms = traverse_ satisfy
+satisfyStats :: [Stat Int] -> UniM ()
+satisfyStats = traverse_ satisfy
+
+unifyStat :: Stat Int -> Stat Int -> UniM ()
+unifyStat (Stat name1 args1) (Stat name2 args2) = do
+  guard $ name1 == name2
+  unifyTerms args1 args2
 
 unify :: Term Int -> Term Int -> UniM ()
 unify t1 t2 = do
   t1' <- lookupVar t1
   t2' <- lookupVar t2
   case (t1', t2') of
-    (Stat name1 args1, Stat name2 args2) -> do
-      lift $ guard $ name1 == name2
-      unifyTerms args1 args2
-    (Var v1, Stat name2 args2) -> learnTerm v1 name2 args2
-    (Stat name1 args1, Var v2) -> learnTerm v2 name1 args1
-    (Var v1, Var v2) -> learnVar v1 v2 -- The order shouldn't really matter
+    (TStat s1, TStat s2) -> unifyStat s1 s2
+    (TVar v, TStat s)    -> bindStat v s
+    (TStat s, TVar v)    -> bindStat v s
+    (TVar v1, TVar v2)   -> bindVar v1 v2 -- The order shouldn't really matter
 
 unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
 unifyTerms t1 t2 = do
-  lift $ guard $ length t1 == length t2
+  guard $ length t1 == length t2
   sequenceA_ $ zipWith unify t1 t2
 
 -- Figuring out how to display the result of the unification
@@ -136,30 +136,26 @@ resolveVars :: Term Int -> UniM (Term Int)
 resolveVars t = do
   t2 <- lookupVar t
   case t2 of
-    (Var v) -> pure $ Var v
-    (Stat name args) -> do
-      args2 <- traverse resolveVars args
-      pure $ Stat name args2
+    (TVar v) -> pure $ TVar v
+    (TStat (Stat name args)) -> TStat . Stat name <$> traverse resolveVars args
 
--- | Helper type so I can resolve variables in multiple terms simultaneously.
-newtype Terms a = Terms { unTerms :: [Term a] }
+-- | Helper type so I can resolve variables in multiple statements
+-- simultaneously.
+newtype Stats a = Stats { unStats :: [Stat a] }
 
-instance Functor Terms where
-  fmap f (Terms ts) = Terms $ fmap (fmap f) ts
+instance Functor Stats where
+  fmap f (Stats ts) = Stats $ fmap (fmap f) ts
 
-instance Foldable Terms where
-  foldMap f (Terms ts) = foldMap (foldMap f) ts
+instance Foldable Stats where
+  foldMap f (Stats ts) = foldMap (foldMap f) ts
 
-run :: Db T.Text -> [Term T.Text] -> [Map.Map T.Text (Term T.Text)]
-run db terms = map fst $ runStateT helper $ newContext db
+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
-      (terms2, vmap) <- understand $ Terms terms
-      satisfyTerms $ unTerms terms2
-      tmap <- traverse (resolveVars . Var) vmap
+      (stats2, vmap) <- understand $ Stats stats
+      satisfyStats $ unStats stats2
+      tmap <- traverse (resolveVars . TVar) vmap
       c <- get
       let naming = findVarNaming vmap (cVars c) $ Map.elems tmap
       pure $ fmap (naming Map.!) <$> tmap
-
-runOne :: Db T.Text -> Term T.Text -> [Map.Map T.Text (Term T.Text)]
-runOne db term = run db [term]

From 2220c48f6c516c0741097c0a99573150d0308b3c Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 23:35:07 +0000
Subject: [PATCH 31/39] Clean up unification

---
 src/Propa/Prolog/Unify.hs | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 2caae9f..020e9a6 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -51,14 +51,14 @@ bindStat k s = modify $ \c -> c{cStats = Map.insert k s $ cStats c}
 -- Returns statements unchanged.
 --
 -- If this returns a variable, then that variable is not bound.
-lookupVar :: Term Int -> UniM (Term Int)
-lookupVar (TVar v) = do
+lookupTerm :: Term Int -> UniM (Term Int)
+lookupTerm (TVar v) = do
   c <- get
   let lastV = follow (cVars c) v
   pure $ case cStats c Map.!? lastV of
     Nothing -> TVar lastV
     Just s  -> TStat s
-lookupVar t@(TStat _) = pure t
+lookupTerm t@(TStat _) = pure t
 
 -- | A simple state monad transformer over the list monad for easy backtracking.
 -- Needs to be changed when implementing cuts.
@@ -80,25 +80,25 @@ understand a = do
   vmap <- varMap a
   pure (fmap (vmap Map.!) a, vmap)
 
-satisfy :: Stat Int -> UniM ()
-satisfy s = do
+satisfyStat :: Stat Int -> UniM ()
+satisfyStat stat = do
   c <- get
   (Def dStat dStats, _) <- understand =<< lift (cDb c)
-  unifyStat s dStat
+  unifyStat stat dStat
   satisfyStats dStats
 
 satisfyStats :: [Stat Int] -> UniM ()
-satisfyStats = traverse_ satisfy
+satisfyStats = traverse_ satisfyStat
 
 unifyStat :: Stat Int -> Stat Int -> UniM ()
 unifyStat (Stat name1 args1) (Stat name2 args2) = do
   guard $ name1 == name2
   unifyTerms args1 args2
 
-unify :: Term Int -> Term Int -> UniM ()
-unify t1 t2 = do
-  t1' <- lookupVar t1
-  t2' <- lookupVar t2
+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
     (TVar v, TStat s)    -> bindStat v s
@@ -108,10 +108,12 @@ unify t1 t2 = do
 unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
 unifyTerms t1 t2 = do
   guard $ length t1 == length t2
-  sequenceA_ $ zipWith unify t1 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)..]
@@ -120,6 +122,9 @@ varNames = do
   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 Int -> [Term Int] -> Map.Map Int T.Text
 findVarNaming known vars terms =
   let knownLookedUp = fmap (follow vars) known
@@ -132,9 +137,10 @@ findVarNaming known vars terms =
       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 <- lookupVar t
+  t2 <- lookupTerm t
   case t2 of
     (TVar v) -> pure $ TVar v
     (TStat (Stat name args)) -> TStat . Stat name <$> traverse resolveVars args

From d473c8443f23ab10d477a723a09327bcca3e45e3 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 23:50:48 +0000
Subject: [PATCH 32/39] Correctly parse expressions

---
 src/Propa/Prolog/Parse.hs | 38 +++++++++++++++++++++++++++-----------
 1 file changed, 27 insertions(+), 11 deletions(-)

diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index 682d24e..9b50271 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -37,7 +37,7 @@ parens = between (symbol "(") (symbol ")")
 brackets :: Parser a -> Parser a
 brackets = between (symbol "[") (symbol "]")
 
--- Building blocks
+-- Names
 
 pName :: Parser T.Text
 pName = lexeme $ unquotedName <|> quotedName
@@ -48,6 +48,29 @@ pName = lexeme $ unquotedName <|> quotedName
 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 term, not variable"
+    (TStat s) -> pure s
+
+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 pExpr
+
+pStats :: Parser [Stat T.Text]
+pStats = (pStat `sepBy1` symbol ",") <* symbol "."
+
+-- Terms
+
 pCons :: Parser (Term T.Text)
 pCons = brackets $ do
   elems <- pTerm `sepBy1` symbol ","
@@ -60,19 +83,10 @@ pList = do
   elems <- brackets $ pTerm `sepBy` symbol ","
   pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems
 
-pStat :: Parser (Stat T.Text)
-pStat = do
-  name <- pName
-  terms <- parens (pTerm `sepBy1` symbol ",") <|> pure []
-  pure $ Stat name terms
-
-pStats :: Parser [Stat T.Text]
-pStats = (pStat `sepBy1` symbol ",") <* symbol "."
-
 pTerm :: Parser (Term T.Text)
 pTerm
   =   (TVar <$> pVarName)
-  <|> (TStat <$> pStat)
+  <|> (TStat <$> pPlainStat)
   <|> try pCons
   <|> pList
   <|> parens pExpr
@@ -84,6 +98,8 @@ pExpr = makeExprParser pTerm
   where
     binary name = InfixL $ (\a b -> TStat $ Stat name [a, b]) <$ symbol name
 
+-- Definitions
+
 pDef :: Parser (Def T.Text)
 pDef = do
   stat <- pStat

From a647b9e26f581e87ce144d208c3fccea78d7ba14 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 23:53:13 +0000
Subject: [PATCH 33/39] Display empty results and no results differently

---
 src/Propa/Prolog/Debug.hs   | 13 +++++++++----
 src/Propa/Prolog/Display.hs |  9 +++++----
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/src/Propa/Prolog/Debug.hs b/src/Propa/Prolog/Debug.hs
index b9f1971..38866ee 100644
--- a/src/Propa/Prolog/Debug.hs
+++ b/src/Propa/Prolog/Debug.hs
@@ -12,7 +12,12 @@ import           Propa.Prolog.Parse
 import           Propa.Prolog.Unify
 
 parseAndRun :: T.Text -> T.Text -> IO ()
-parseAndRun dbText statsText = T.putStrLn $ either id id $ do
-  db <- parseDb "<input>" dbText
-  stats <- parseStats "<input>" statsText
-  pure $ T.intercalate "\n" $ map displayResult $ run db stats
+parseAndRun dbText statsText = T.putStrLn $ case results of
+  Left e   -> e
+  Right [] -> "No."
+  Right rs -> T.intercalate "\n" rs
+  where
+    results = do
+      db <- parseDb "<input>" dbText
+      stats <- parseStats "<input>" statsText
+      pure $ map displayResult $ run db stats
diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index 79608b6..ff07066 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -61,8 +61,9 @@ displayDefs :: [Def T.Text] -> T.Text
 displayDefs = T.intercalate "\n" . map displayDef
 
 displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
-displayResult
+displayResult m | Map.null m = "Yes."
+displayResult m
   = T.intercalate "\n"
-  . map (\(k, v) -> k <> " = " <> displayTerm v)
-  . filter (\(k, v) -> v /= TVar k)
-  . Map.assocs
+  $ map (\(k, v) -> k <> " = " <> displayTerm v)
+  $ filter (\(k, v) -> v /= TVar k)
+  $ Map.assocs m

From 90f97c4c30c42eac13307c796f51fe892c3dcb0c Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Sun, 13 Dec 2020 23:59:14 +0000
Subject: [PATCH 34/39] Rename parsers for consistency

---
 src/Propa/Prolog/Parse.hs | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index 9b50271..9148821 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -57,6 +57,7 @@ pTermToStat p = do
     (TVar _)  -> fail "expected term, not variable"
     (TStat s) -> pure s
 
+-- | Parse a statement of the form @name(args)@.
 pPlainStat :: Parser (Stat T.Text)
 pPlainStat = do
   name <- pName
@@ -64,7 +65,7 @@ pPlainStat = do
   pure $ Stat name terms
 
 pStat :: Parser (Stat T.Text)
-pStat = pPlainStat <|> pTermToStat pExpr
+pStat = pPlainStat <|> pTermToStat pTerm
 
 pStats :: Parser [Stat T.Text]
 pStats = (pStat `sepBy1` symbol ",") <* symbol "."
@@ -83,16 +84,17 @@ pList = do
   elems <- brackets $ pTerm `sepBy` symbol ","
   pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems
 
-pTerm :: Parser (Term T.Text)
-pTerm
+-- | Parse a term that is not an expression.
+pPlainTerm :: Parser (Term T.Text)
+pPlainTerm
   =   (TVar <$> pVarName)
   <|> (TStat <$> pPlainStat)
   <|> try pCons
   <|> pList
-  <|> parens pExpr
+  <|> parens pTerm
 
-pExpr :: Parser (Term T.Text)
-pExpr = makeExprParser pTerm
+pTerm :: Parser (Term T.Text)
+pTerm = makeExprParser pPlainTerm
   [ [ binary "=" ]
   ]
   where

From 54214ed10c68f7fa8526802fc470d76c83e22a37 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 14 Dec 2020 00:18:57 +0000
Subject: [PATCH 35/39] Properly display the empty list

---
 src/Propa/Prolog/Display.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index ff07066..433dfc7 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -29,6 +29,7 @@ displayName name
       ]
 
 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)

From bf50628483e66cf5e7e2ee13bfc2d61c45dcfdf1 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 14 Dec 2020 11:16:26 +0000
Subject: [PATCH 36/39] Make parseAndRun nicer to use in ghci

It now no longer requires -XOverloadedStrings
---
 src/Propa/Prolog/Debug.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Propa/Prolog/Debug.hs b/src/Propa/Prolog/Debug.hs
index 38866ee..22655b2 100644
--- a/src/Propa/Prolog/Debug.hs
+++ b/src/Propa/Prolog/Debug.hs
@@ -11,13 +11,13 @@ import           Propa.Prolog.Display
 import           Propa.Prolog.Parse
 import           Propa.Prolog.Unify
 
-parseAndRun :: T.Text -> T.Text -> IO ()
-parseAndRun dbText statsText = T.putStrLn $ case results of
+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 "<input>" dbText
-      stats <- parseStats "<input>" statsText
+      db <- parseDb "<db>" $ T.pack dbStr
+      stats <- parseStats "<query>" $ T.pack statsStr
       pure $ map displayResult $ run db stats

From 01fa10fefb0b577210881f53490e4ff3a6c0212c Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 14 Dec 2020 11:21:42 +0000
Subject: [PATCH 37/39] Fix when "Yes." is displayed.

It is now displayed whenever a solution is found but no variable assignments is
printed.
---
 src/Propa/Prolog/Display.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index 433dfc7..d4e1eeb 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -62,9 +62,9 @@ displayDefs :: [Def T.Text] -> T.Text
 displayDefs = T.intercalate "\n" . map displayDef
 
 displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
-displayResult m | Map.null m = "Yes."
 displayResult m
-  = T.intercalate "\n"
-  $ map (\(k, v) -> k <> " = " <> displayTerm v)
-  $ filter (\(k, v) -> v /= TVar k)
-  $ Map.assocs 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

From 09a42340fc5e29d69601ab1bd46e33cbb728c436 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 14 Dec 2020 13:46:44 +0000
Subject: [PATCH 38/39] Add integers

---
 src/Propa/Prolog/Display.hs |  1 +
 src/Propa/Prolog/Parse.hs   |  4 +++-
 src/Propa/Prolog/Types.hs   |  9 ++++++++
 src/Propa/Prolog/Unify.hs   | 42 +++++++++++++++++--------------------
 4 files changed, 32 insertions(+), 24 deletions(-)

diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs
index d4e1eeb..d943b34 100644
--- a/src/Propa/Prolog/Display.hs
+++ b/src/Propa/Prolog/Display.hs
@@ -45,6 +45,7 @@ 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
diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs
index 9148821..4b9d9c5 100644
--- a/src/Propa/Prolog/Parse.hs
+++ b/src/Propa/Prolog/Parse.hs
@@ -54,7 +54,8 @@ pTermToStat :: Parser (Term T.Text) -> Parser (Stat T.Text)
 pTermToStat p = do
   term <- p
   case term of
-    (TVar _)  -> fail "expected term, not variable"
+    (TVar _)  -> fail "expected statement, not variable"
+    (TInt _)  -> fail "expected statement, not integer"
     (TStat s) -> pure s
 
 -- | Parse a statement of the form @name(args)@.
@@ -88,6 +89,7 @@ pList = do
 pPlainTerm :: Parser (Term T.Text)
 pPlainTerm
   =   (TVar <$> pVarName)
+  <|> (TInt <$> L.signed (pure ()) L.decimal)
   <|> (TStat <$> pPlainStat)
   <|> try pCons
   <|> pList
diff --git a/src/Propa/Prolog/Types.hs b/src/Propa/Prolog/Types.hs
index 485f44b..ca6236f 100644
--- a/src/Propa/Prolog/Types.hs
+++ b/src/Propa/Prolog/Types.hs
@@ -1,6 +1,7 @@
 module Propa.Prolog.Types
   ( Stat(..)
   , Term(..)
+  , tVar
   , Def(..)
   , Db
   ) where
@@ -21,21 +22,29 @@ instance Traversable Stat where
 
 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)
 
diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 020e9a6..9adb323 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -4,6 +4,7 @@ module Propa.Prolog.Unify
   ( run
   ) where
 
+import           Control.Applicative
 import           Control.Monad
 import           Data.Foldable
 import           Data.List
@@ -21,8 +22,8 @@ import           Propa.Prolog.Types
 
 -- | Start at a value and follow the map's entries until the end of the chain of
 -- references.
-follow :: (Ord a) => Map.Map a a -> a -> a
-follow m v = maybe v (follow m) $ m Map.!? v
+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.
@@ -34,31 +35,23 @@ deduplicate = Set.toList . Set.fromList
 data Context = Context
   { cDb     :: Db T.Text
   , cVarIdx :: Int
-  , cVars   :: Map.Map Int Int
-  , cStats  :: Map.Map Int (Stat Int)
+  , cTerms  :: Map.Map Int (Term Int)
   } deriving (Show)
 
 newContext :: [Def T.Text] -> Context
-newContext db = Context db 0 Map.empty Map.empty
+newContext db = Context db 0 Map.empty
 
-bindVar :: Int -> Int -> UniM ()
-bindVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c}
-
-bindStat :: Int -> Stat Int -> UniM ()
-bindStat k s = modify $ \c -> c{cStats = Map.insert k s $ cStats c}
+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 (TVar v) = do
+lookupTerm t = do
   c <- get
-  let lastV = follow (cVars c) v
-  pure $ case cStats c Map.!? lastV of
-    Nothing -> TVar lastV
-    Just s  -> TStat s
-lookupTerm t@(TStat _) = pure t
+  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.
@@ -101,9 +94,10 @@ unifyTerm t1 t2 = do
   t2' <- lookupTerm t2
   case (t1', t2') of
     (TStat s1, TStat s2) -> unifyStat s1 s2
-    (TVar v, TStat s)    -> bindStat v s
-    (TStat s, TVar v)    -> bindStat v s
-    (TVar v1, TVar v2)   -> bindVar v1 v2 -- The order shouldn't really matter
+    (TInt i1, TInt i2)   -> guard $ i1 == i2
+    (TVar v, t)          -> bindTerm v t
+    (t, TVar v)          -> bindTerm v t
+    (_, _)               -> empty
 
 unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
 unifyTerms t1 t2 = do
@@ -125,9 +119,10 @@ varNames = do
 -- | 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 Int -> [Term Int] -> Map.Map Int T.Text
+findVarNaming :: Map.Map T.Text Int -> Map.Map Int (Term Int) -> [Term Int] -> Map.Map Int T.Text
 findVarNaming known vars terms =
-  let knownLookedUp = fmap (follow vars) known
+  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
@@ -142,7 +137,8 @@ resolveVars :: Term Int -> UniM (Term Int)
 resolveVars t = do
   t2 <- lookupTerm t
   case t2 of
-    (TVar v) -> pure $ TVar v
+    (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
@@ -163,5 +159,5 @@ run db stats = map fst $ runStateT helper $ newContext db
       satisfyStats $ unStats stats2
       tmap <- traverse (resolveVars . TVar) vmap
       c <- get
-      let naming = findVarNaming vmap (cVars c) $ Map.elems tmap
+      let naming = findVarNaming vmap (cTerms c) $ Map.elems tmap
       pure $ fmap (naming Map.!) <$> tmap

From f0e291a84d926f25b89930c0b466946e5403d551 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 14 Dec 2020 13:59:13 +0000
Subject: [PATCH 39/39] Prevent infinite loop unifying variable with itself

---
 src/Propa/Prolog/Unify.hs | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 9adb323..50991ec 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -93,11 +93,12 @@ 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, t)          -> bindTerm v t
-    (t, TVar v)          -> bindTerm v t
-    (_, _)               -> empty
+    (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