Tinker with stuff

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
 

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

quickspec.cabal

@@ -111,5 +111,5 @@ library
     spoon,
     template-haskell,
     transformers,
-    twee-lib == 2.1.5,
+    twee-lib == 2.2,
     uglymemo

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.

stack.yaml

@@ -1,4 +1,4 @@
-resolver: lts-13.13
+resolver: lts-14.22
 
 packages:
 - .