Some rudimentary unification tests

test/PartialEvaluatorTests.hs

@@ -80,7 +80,7 @@ testPartialEvalPrograms =
                          ("Checking partial evaluation for term '" ++ show t' ++ "'") $
                          programTestOK (p', t', e'))
   [ (p1, t1, e1)
-  , (p2, t2, e2)
+  -- , (p2, t2, e2)
   ]
 
 
@@ -136,6 +136,7 @@ e1 =
     ())
   ()
 
+-- TODO: Test proper inlining of nested function calls
 p2 :: Program ()
 -- Check simpleAdd.con
 p2 = undefined

test/Spec.hs

@@ -2,7 +2,7 @@ import Test.Tasty
 
 import ParserTests
 import PartialEvaluatorTests
--- import UnificationTests
+import UnificationTests
 -- import PropertyCheckerTests
 
 
@@ -22,6 +22,10 @@ tests =
         , termParser
         , programTests
         ]
+    , testGroup "Unification: "
+        [
+          substitutionTests
+        ]
     , testGroup "Partial evaluator: "
         [
           partialEvaluatorTests

test/UnificationTests.hs

@@ -1,7 +1,45 @@
 module UnificationTests where
 
--- import Syntax
--- import Unification
+import Core.Syntax
+import Analysis.Unification
 
+import Test.Tasty
+import Test.Tasty.HUnit
+import Control.Monad (void)
 
-
+
+-- Export
+substitutionTests :: TestTree
+substitutionTests =
+  testGroup "Computing a substitution -- t[v/x]: "
+    substituteVars
+
+
+-- Helpers
+computeSubstitutionOK :: (Show a, Eq a) => Pattern a -> Term a
+                                        -> Term a -> Term a -> Assertion
+computeSubstitutionOK x t v e =
+  assertEqual "Should be equal after substitution."
+    e (substitute x t v)
+
+
+-- Substitution
+substituteVars :: [TestTree]
+substituteVars =
+  map (\(x, t, v, e) -> testCase
+                        ("(" ++ show t ++ ")[" ++ show v ++ "/" ++ show x ++ "]" ++
+                         " should give " ++ show e) $
+                        computeSubstitutionOK x t v e)
+  [ ( Variable "x" ()
+    , Plus (Pattern (Variable "x" ())) (Pattern (Value (Number 3 ()))) ()
+    , Pattern (Value (Number 5 ()))
+    , Plus (Pattern (Value (Number 5 ()))) (Pattern (Value (Number 3 ()))) ())
+  , ( Variable "x" ()
+    , Plus (Pattern (Variable "x" ())) (Pattern (Variable "y" ())) ()
+    , Pattern (Value (Number 5 ()))
+    , Plus (Pattern (Value (Number 5 ()))) (Pattern (Variable "y" ())) ())
+  , ( PConstructor "Ctr" [Variable "x" (), Variable "y" ()] ()
+    , Plus (Pattern (Variable "x" ())) (Pattern (Variable "y" ())) ()
+    , TConstructor "Ctr" [Pattern (Value (Number 5 ())), Pattern (Value (Number 3 ()))] ()
+    , Plus (Pattern (Value (Number 5 ()))) (Pattern (Value (Number 3 ()))) ())
+  ]