From 6566efc21590ebbf37c04772f9f9c2451b5148a9 Mon Sep 17 00:00:00 2001
From: Nick Smallbone <nick@smallbone.se>
Date: Wed, 15 Apr 2020 14:39:12 +0200
Subject: [PATCH] Tinker with stuff

---
 examples/HugeLists.hs          |  2 +-
 notes                          |  4 ++++
 quickspec.cabal                |  2 +-
 src/QuickSpec/Internal/Term.hs | 32 ++++++++++++++++++++++++++++++++
 stack.yaml                     |  2 +-
 5 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/examples/HugeLists.hs b/examples/HugeLists.hs
index c2e1ef1..494acd9 100644
--- a/examples/HugeLists.hs
+++ b/examples/HugeLists.hs
@@ -1,7 +1,7 @@
 -- A stress test using lots and lots of list functions.
 {-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-}
 import QuickSpec
-import QuickSpec.Utils
+import QuickSpec.Internal.Utils
 import Data.List
 import Control.Monad
 
diff --git a/notes b/notes
index 9a71acc..2e18b39 100644
--- a/notes
+++ b/notes
@@ -1,3 +1,7 @@
+does regenerlise need to worry about restricting occurrences of the
+same var to have the same type? now we have the invariant that each
+var has a unique type
+
 NOTE:
 schema layer should somehow be the same, whether we're discovering
 equations or something else. maybe this means splitting lower layers
diff --git a/quickspec.cabal b/quickspec.cabal
index 0e93df6..03ceaf0 100644
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -111,5 +111,5 @@ library
     spoon,
     template-haskell,
     transformers,
-    twee-lib == 2.1.5,
+    twee-lib == 2.2,
     uglymemo
diff --git a/src/QuickSpec/Internal/Term.hs b/src/QuickSpec/Internal/Term.hs
index d2dbdf4..b044c66 100644
--- a/src/QuickSpec/Internal/Term.hs
+++ b/src/QuickSpec/Internal/Term.hs
@@ -15,6 +15,7 @@ import qualified Data.DList as DList
 import Twee.Base(Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)
 import Twee.Pretty
 import qualified Data.Map.Strict as Map
+import Data.Map(Map)
 import Data.List
 import Data.Ord
 
@@ -34,6 +35,37 @@ instance Typed Var where
   otherTypesDL _ = mzero
   typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x
 
+match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
+match (Var x) t = Just (Map.singleton x t)
+match (Fun f) (Fun g)
+  | f == g = Just Map.empty
+  | otherwise = Nothing
+match (f :$: x) (g :$: y) = do
+  m1 <- match f g
+  m2 <- match x y
+  guard (and [t == u | (t, u) <- Map.elems (Map.intersectionWith (,) m1 m2)])
+  return (Map.union m1 m2)
+
+unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))
+unify t u = loop Map.empty [(t, u)]
+  where
+    loop sub [] = Just sub
+    loop sub ((Fun f, Fun g):xs)
+      | f == g = loop sub xs
+    loop sub ((f :$: x, g :$: y):xs) =
+      loop sub ((f, g):(x, y):xs)
+    loop sub ((Var x, t):xs)
+      | t == Var x = loop sub xs
+      | x `elem` vars t = Nothing
+      | otherwise =
+        loop
+          (Map.insert x t (fmap (replace x t) sub))
+          [(replace x t u, replace x t v) | (u, v) <- xs]
+    loop sub ((t, Var x):xs) = loop sub ((Var x, t):xs)
+
+    replace x t (Var y) | x == y = t
+    replace _ _ t = t
+
 -- | A class for things that contain terms.
 class Symbolic f a | a -> f where
   -- | A different list of all terms contained in the thing.
diff --git a/stack.yaml b/stack.yaml
index 7a10130..31a2063 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,4 +1,4 @@
-resolver: lts-13.13
+resolver: lts-14.22
 
 packages:
 - .