ecta-1.0.0.0: test/PathsSpec.hs
module PathsSpec ( spec ) where
import Data.List ( (\\), nub, sort, subsequences )
import qualified Data.Vector as Vector
import Test.Hspec
import Test.QuickCheck
import Data.ECTA.Internal.Paths
import Data.ECTA.Internal.Paths.Zipper
-----------------------------------------------------------------
-----------------------------------
------ PathTrie testing utils
-----------------------------------
data PathTrieCommand = PathTrieZipperAscend Int
| PathTrieZipperDescend Int
deriving ( Show )
instance Arbitrary PathTrieCommand where
arbitrary = do b <- arbitrary
i <- chooseInt (0, 4)
return $ if b then PathTrieZipperAscend i else PathTrieZipperDescend i
shrink _ = []
invertPathTrieCommand :: PathTrieCommand -> PathTrieCommand
invertPathTrieCommand (PathTrieZipperAscend i) = PathTrieZipperDescend i
invertPathTrieCommand (PathTrieZipperDescend i) = PathTrieZipperAscend i
-- | A variant of pathTrieZipperDescend that allows for descending out of bounds.
-- Makes the "descend/ascend are inverses" property easy to write
extendedPathTrieZipperDescend :: PathTrieZipper -> Int -> PathTrieZipper
extendedPathTrieZipperDescend (PathTrieZipper (PathTrie v) z') i
| i >= Vector.length v = PathTrieZipper EmptyPathTrie (PathTrieAt i (PathTrie v) z')
extendedPathTrieZipperDescend z i = pathTrieZipperDescend z i
applyPathTrieCommand :: PathTrieCommand -> PathTrieZipper -> PathTrieZipper
applyPathTrieCommand (PathTrieZipperAscend i) z = pathTrieZipperAscend z i
applyPathTrieCommand (PathTrieZipperDescend i) z = extendedPathTrieZipperDescend z i
-----------------------------------
------ Random generation
-----------------------------------
instance Arbitrary Path where
arbitrary = path <$> listOf (chooseInt (0, 4))
shrink = map Path . shrink . unPath
instance Arbitrary PathTrie where
arbitrary = do paths <- suchThat arbitrary (\ps -> not (isContradicting [ps]))
return $ toPathTrie $ nub paths
shrink EmptyPathTrie = []
shrink TerminalPathTrie = []
shrink (PathTrieSingleChild _ pt) = [pt]
shrink (PathTrie vec) = let l = Vector.toList vec
in l ++ (map (PathTrie . Vector.fromList) (subsequences l \\ [l]))
-----------------------------------
------ Constructing test inputs
-----------------------------------
mkTestPaths1 :: [[Int]] -> [[Path]]
mkTestPaths1 = map (map (path . (:[])))
mkTestPathsN :: [[[Int]]] -> [[Path]]
mkTestPathsN = map (map path)
--------
spec :: Spec
spec = do
describe "subpath checking" $ do
it "empty path is always subpath" $
property $ \p -> isSubpath EmptyPath p
it "is subpath of concatenation" $
property $ \xs ys -> isSubpath (path xs) (path $ xs ++ ys)
it "non-empty concatenation is not subpath of orig" $
property $ \xs ys -> ys /= [] ==> not $ isSubpath (path $ xs ++ ys) (path xs)
it "empty path is strict subpath of nonempty" $
property $ \p -> p /= EmptyPath ==> isStrictSubpath EmptyPath p
it "nothing is strict subpath of itself" $
property $ \p -> not $ isStrictSubpath p p
describe "substSubpath" $ do
it "replaces prefix" $
property $ \xs ys zs -> substSubpath (path zs) (path ys) (path $ ys ++ xs) `shouldBe` path (zs ++ xs)
describe "path tries" $ do
it "fromPathTrie and toPathTrie are inverses" $ do
property $ \pt -> toPathTrie (fromPathTrie pt) == pt
it "comparing path trie is same as comparing list of paths" $ do
property $ \ps1 ps2 -> not (isContradicting [ps1] || isContradicting [ps2])
==> compare (toPathTrie $ nub ps1) (toPathTrie $ nub ps2)
== compare (sort $ nub ps1) (sort $ nub ps2)
it "unioning path trie same as unioning lists of paths, checking contradiction" $ do
property $ \pt1 pt2 -> case unionPathTrie pt1 pt2 of
Nothing -> isContradicting [fromPathTrie pt1 ++ fromPathTrie pt2]
Just pt' -> fromPathTrie pt' == (sort $ nub $ fromPathTrie pt1 ++ fromPathTrie pt2)
it "PathTrie-based hasSubsumingMember same as list-based implementation" $ do
property $ \pt1 pt2 -> let pec1 = PathEClass (fromPathTrie pt1)
pec2 = PathEClass (fromPathTrie pt2)
in hasSubsumingMember pec1 pec2 == hasSubsumingMemberListBased (unPathEClass pec1) (unPathEClass pec2)
describe "path trie zipper" $ do
it "smallestNonempty works" $ do
smallestNonempty (Vector.fromList [EmptyPathTrie, EmptyPathTrie, TerminalPathTrie, TerminalPathTrie, EmptyPathTrie]) `shouldBe` 2
it "largestNonempty works" $ do
largestNonempty (Vector.fromList [EmptyPathTrie, EmptyPathTrie, TerminalPathTrie, TerminalPathTrie, EmptyPathTrie]) `shouldBe` 3
it "ascending a zipper well beyond the root == adding ints to a path" $ do
forAll (listOf (chooseInt (0, 4))) $ \ns -> fromPathTrie (zipperCurPathTrie $ foldr (flip pathTrieZipperAscend) (pathTrieToZipper $ toPathTrie [EmptyPath]) ns) == [path ns]
it "a sequence of path trie zipper ascends/descends followed by its reverse yields the identity" $ do
property $ \actions pt -> (zipperCurPathTrie $ foldr applyPathTrieCommand (pathTrieToZipper pt) (reverse (map invertPathTrieCommand actions) ++ actions))
== pt
describe "PathEClass" $ do
it "both ways of getting list of paths from a PathEClass are identical" $ do
property $ \pt -> fromPathTrie (getPathTrie (PathEClass (fromPathTrie pt))) == getOrigPaths (PathEClass (fromPathTrie pt))
describe "mkEqConstraints" $ do
it "removes unitary" $
property $ \ps -> mkEqConstraints (map (:[]) ps) == EmptyConstraints
it "removes empty" $
property $ \n -> mkEqConstraints (replicate n []) == EmptyConstraints
it "completes equalities" $
mkEqConstraints (mkTestPaths1 [[1,2], [2,3], [4,5], [6,7], [7,1]]) `shouldBe` rawMkEqConstraints (sort $ mkTestPaths1 [[1,2,3,6,7], [4,5]])
it "adds congruences" $
mkEqConstraints (mkTestPathsN [[[0],[1]], [[2], [0]], [[0, 0], [0, 1]]]) `shouldBe` rawMkEqConstraints (sort $ (mkTestPathsN [[[0],[1],[2]], [[0, 0], [0, 1], [1, 0], [1,1], [2,0], [2,1]]]))
it "detects contradictions from congruences" $
-- This test input is from unifying `(a -> b) -> (a -> b)` and `(a -> (a -> a)) -> (a -> ([a] -> a))`
constraintsAreContradictory (mkEqConstraints $ mkTestPathsN [ [[1, 1], [2,1]]
, [[1, 1], [1, 2, 1], [1,2, 2], [2, 1], [2, 2, 1, 0], [2, 2, 2]]
, [[1, 2], [2, 2]]
])
`shouldBe` True
-- TODO: (6/23/21) QuickCheck generates very large lists, much larger than currently seen in actual inputs.
-- mkEqConstraints contains a very inefficient addCongruences implementation. Therefore, these run too slowly.
{-
describe "constraintsImply" $ do
modifyMaxSuccess (const 2) $
it "Implies removed constraints" $
property $ \cs1 cs2 -> length (concat cs1) < 300 && length (concat cs2) < 300
==> constraintsImply (mkEqConstraints $ cs1 ++ cs2) (mkEqConstraints cs1)
modifyMaxSuccess (const 2) $
it "Does not imply added constraints" $
property $ \cs1 cs2 -> length (concat cs1) < 300 && length (concat cs2) < 300
==> let ecs1 = mkEqConstraints $ cs1 ++ cs2
ecs2 = mkEqConstraints cs1
in ecs1 /= ecs2 ==> not (constraintsImply ecs2 ecs1)
-}