ecta-1.0.0.0: test/ECTASpec.hs
{-# LANGUAGE OverloadedStrings #-}
module ECTASpec ( spec ) where
import Control.Exception (evaluate)
import qualified Data.HashSet as HashSet
import Data.IORef ( newIORef, readIORef, modifyIORef )
import qualified Data.Text as Text
import Data.Set ( Set )
import qualified Data.Set as Set
import System.IO.Unsafe ( unsafePerformIO )
import Test.Hspec
import Test.QuickCheck
import Data.ECTA
import Data.ECTA.Internal.ECTA.Operations
import Data.ECTA.Internal.ECTA.Type
import Data.ECTA.Internal.Paths
import Data.ECTA.Term
import Application.TermSearch.TermSearch
import Test.Generators.ECTA ()
-----------------------------------------------------------------
constTerms :: [Symbol] -> Node
constTerms ss = Node (map (\s -> Edge s []) ss)
ex1 :: Node
ex1 = Node [mkEdge "f" [constTerms ["1", "2"], Node [Edge "g" [constTerms ["1", "2"]]]] (mkEqConstraints [[path [0], path [1,0]]])]
ex2 :: Node
ex2 = Node [mkEdge "f" [constTerms ["1", "2", "3"], Node [Edge "g" [constTerms ["1", "2", "4"]]]] (mkEqConstraints [[path [0], path [1,0]]])]
ex3 :: Node
ex3 = Node [Edge "f" [Node [Edge "g" [constTerms ["1", "2"]]]], Edge "h" [Node [Edge "i" [constTerms ["3", "4"]]]]]
ex3_root_doubled :: Node
ex3_root_doubled = Node [Edge "ff" [Node [Edge "g" [constTerms ["1", "2"]]]], Edge "hh" [Node [Edge "i" [constTerms ["3", "4"]]]]]
ex3_doubled :: Node
ex3_doubled = Node [Edge "f" [Node [Edge "g" [constTerms ["11", "22"]]]], Edge "h" [Node [Edge "i" [constTerms ["33", "44"]]]]]
doubleNodeSymbols :: Node -> Node
doubleNodeSymbols (Node es) = Node $ map doubleEdgeSymbol es
where
doubleEdgeSymbol :: Edge -> Edge
doubleEdgeSymbol (Edge (Symbol s) ns) = Edge (Symbol (Text.append s s)) ns
doubleNodeSymbols n = error $ "doubleNodeSymbols: unexpected " <> show n
testBigNode :: Node
testBigNode = union $ termsK EmptyNode True 4
_testUnreducedConstraint :: Edge
_testUnreducedConstraint = mkEdge "foo" [Node [Edge "A" [], Edge "B" []], Node [Edge "B" [], Edge "C" []]] (mkEqConstraints [[path [0], path [1]]])
bug062721NonIdempotentEqConstraintReduction :: (EqConstraints, [Node])
bug062721NonIdempotentEqConstraintReduction =
( EqConstraints {getEclasses = [PathEClass [Path [0],Path [2,0,2]],PathEClass [Path [1],Path [2,0,0]],PathEClass [Path [2,0,1],Path [3,0]]]}
, [(Node [(Edge "baseType" [])]),(Node [(Edge "(->)" [])]),(Node [(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "(->)" [])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])])] EqConstraints {getEclasses = [PathEClass [Path [0],Path [2,0,2]],PathEClass [Path [1],Path [2,0,0]],PathEClass [Path [2,0,1],Path [3,0]]]})]),(Node [(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "Maybe" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "(->)" [])]),(Node [(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "(->)" [])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])])] EqConstraints {getEclasses = [PathEClass [Path [0],Path [2,0,2]],PathEClass [Path [1],Path [2,0,0]],PathEClass [Path [2,0,1],Path [3,0]]]})]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])])] EqConstraints {getEclasses = [PathEClass [Path [0],Path [2,0,2]],PathEClass [Path [1],Path [2,0,0]],PathEClass [Path [2,0,1],Path [3,0]]]}),(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "(->)" [])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])]),(Node [(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "(->)" [])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])]),(Node [(Edge "g" [(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "baseType" [])]),(Node [(Edge "baseType" [])])])])]),(Edge "x" [(Node [(Edge "baseType" [])])]),(Edge "n" [(Node [(Edge "Int" [])])]),(Edge "$" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,1]],PathEClass [Path [1,2],Path [2,2]]]})])]),(Edge "replicate" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "Int" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])]),(createMu $ \x -> (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),x,x]),(Edge "Maybe" [x]),(Edge "List" [x])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [1,1],Path [2,2,1,0]],PathEClass [Path [1,2,1],Path [1,2,2],Path [2,1],Path [2,2,2]]]})])])])] EqConstraints {getEclasses = [PathEClass [Path [0],Path [2,0,2]],PathEClass [Path [1],Path [2,0,0]],PathEClass [Path [2,0,1],Path [3,0]]]})])] EqConstraints {getEclasses = [PathEClass [Path [0],Path [2,0,2]],PathEClass [Path [1],Path [2,0,0]],PathEClass [Path [2,0,1],Path [3,0]]]})])]
)
_bug062721NonIdempotentEqConstraintReductionGen :: Gen [Node]
_bug062721NonIdempotentEqConstraintReductionGen = return $ snd bug062721NonIdempotentEqConstraintReduction
infiniteFNode :: Node
infiniteFNode = createMu (\x ->(Node [Edge "f" [x]]))
_infiniteFGNode :: Node
_infiniteFGNode = createMu (\x ->(Node [Edge "f" [x], Edge "g" [x]]))
--------------------------------------------------------------
----------------------------- Main ---------------------------
--------------------------------------------------------------
spec :: Spec
spec = do
describe "Pathable" $ do
it "Node.getPath root" $
getPath (path []) testBigNode `shouldBe` testBigNode
it "Node.getPath one-level" $
getPath (path [0]) ex1 `shouldBe` (constTerms ["1", "2"])
it "Node.getPath merges multiple branches" $
getPath (path [0,0]) ex3 `shouldBe` (constTerms ["1", "2", "3", "4"])
it "Node.modifyAtPath modifies at root" $
modifyAtPath doubleNodeSymbols (path []) ex3 `shouldBe` ex3_root_doubled
it "Node.modifyAtPath modifies at path" $
modifyAtPath doubleNodeSymbols (path [0,0]) ex3 `shouldBe` ex3_doubled
describe "hash-consing" $ do
it "similar mu-nodes created independently are equal / have equal ids" $
createMu (\x -> Node [Edge "f" [x]]) `shouldBe` createMu (\x -> Node [Edge "f" [x]])
describe "ECTA-nodes" $ do
it "equality constraints constrain" $
naiveDenotation ex1 `shouldSatisfy` ((== 2) . length)
it "reduces paths constrained by equality constraints" $
reducePartially ex2 `shouldBe` reducePartially ex1
describe "intersection" $ do
it "intersection commutes with naiveDenotation" $
property $ mapSize (min 3) $ \n1 n2 -> HashSet.fromList (naiveDenotation $ intersect n1 n2)
`shouldBe` HashSet.intersection (HashSet.fromList $ naiveDenotation n1)
(HashSet.fromList $ naiveDenotation n2)
it "intersect is associative" $
property $ \n1 n2 n3 -> ((n1 `intersect` n2) `intersect` n3) == (n1 `intersect` (n2 `intersect` n3))
it "intersect is commutative" $
property $ \n1 n2 -> intersect n1 n2 == intersect n2 n1
it "intersect distributes over union" $
property $ \n1 n2 n3 -> intersect n1 (union [n2, n3]) == union [intersect n1 n2, intersect n1 n3]
-- intersect is NOT idempotent now because we eagerly dropRedundantEdges.
-- Example: (Node [(Edge "f" [(Node [(Edge "a" [])])]),(Edge "f" [(Node [(Edge "a" []),(Edge "b" [])])])])
-- `intersect` returns (Node [(Edge "f" [(Node [(Edge "a" [])])])])
--
-- it "intersect is idempotent" $
-- property $ \n1 -> intersect n1 n1 == refold n1 -- Note: we eagerly refold recursive nodes to prevent ECTA grows too large
describe "intersection examples" $ do
-- Intersection examples without Mu nodes
--
-- Note: Intersection between 1 and 3 is not well-defined: must be same-sorted.
it "remove leaf choice" $
intersect intTest1 intTest2 `shouldBe` intTest1
it "remove non-leaf choice" $
intersect intTest3 intTest4 `shouldBe` intTest3
-- This test is a bit indirect: the intersection results in a term with what I /think/ is an inaccessible branch.
-- Not sure if there is a clean-up pass we can do.
it "add constraints" $
naiveDenotation (intersect intTest5 intTest6) `shouldBe` [Term "g" [Term "a" [],Term "b" []]]
-- Intersection examples with Mu nodes
-- Note: `intersect` eagerly refolds recursive nodes
it "intersect (one-step loop) with (its own unfolding: step, one-step)" $
intersect intTest7 intTest8 `shouldBe` refold intTest8
it "intersect (one-step loop) with (two-step loop)" $
intersect intTest7 intTest9 `shouldBe` intTest9
it "intersect (one-step loop) with (one step, two-step loop)" $
intersect intTest7 intTest10 `shouldBe` intTest10
it "intersect (one step, one-step loop) with (two-step loop)" $
intersect intTest8 intTest9 `shouldBe` intTest10
it "intersect (one step, one-step loop) with (one step, two-step loop)" $
intersect intTest8 intTest10 `shouldBe` intTest10
it "intersect (two-step loop) with (one step, two-step loop)" $
intersect intTest9 intTest10 `shouldBe` refold intTest8
it "intersect with nested Mus" $ do
intersect intTest11 intTest12 `shouldBe` refold (Node [Edge "f" [createMu $ \r -> Node [Edge "f" [r]]]])
describe "reduction" $ do
it "reduction preserves naiveDenotation" $
property $ mapSize (min 3) $ \n -> HashSet.fromList (naiveDenotation n) `shouldBe` HashSet.fromList (naiveDenotation $ reducePartially n)
it "reducing a single constraint is idempotent 1" $
property $ \e -> let ns = edgeChildren e
ecs = edgeEcs e
ns' = reduceEqConstraints ecs EmptyConstraints ns
in ns' == reduceEqConstraints ecs EmptyConstraints ns'
it "reducing a single constraint is idempotent 2" $
property $ \e1 e2 -> let maybeE' = intersectEdge e1 e2
in (maybeE' /= Nothing) ==>
let Just e' = maybeE'
ns = edgeChildren e'
ecs = edgeEcs e'
ns' = reduceEqConstraints ecs EmptyConstraints ns
in ns' == reduceEqConstraints ecs EmptyConstraints ns'
-- TODO (6/29/21): Need a better way to visualize the type nodes. Cannot figure out why this fails.
-- Reversing the order that eclasses are processed seems to make no difference.
{-
it "reducing a constraint is idempotent: buggy input 6/27/21" $
forAllShrink bug062721NonIdempotentEqConstraintReductionGen shrink
(\ns -> let ecs = fst bug062721NonIdempotentEqConstraintReduction
ns' = reduceEqConstraints ecs EmptyConstraints ns
in ns' == reduceEqConstraints ecs EmptyConstraints ns')
-}
-- TODO: I've become less convinced this can actually be done in one pass. But this test passes.
it "leaf reduction means, for everything at a path, there is something matching at the other paths" $
property $ \e -> let e' = reduceEdgeIntersection EmptyConstraints e
ns = edgeChildren e' in
(e' /= emptyEdge && edgeEcs e' /= EmptyConstraints) ==>
and [intersect n1 n2 /= EmptyNode | ec <- unsafeGetEclasses (edgeEcs e')
, p1 <- unPathEClass ec
, p2 <- unPathEClass ec
, n1 <- getAllAtPath p1 ns
, let n2 = getPath p2 ns]
describe "(un)folding" $ do
it "unfolding a mu node once unfolds it once" $
unfoldOuterRec infiniteFNode `shouldBe` (Node [Edge "f" [infiniteFNode]])
it "recursive terms are unrolled to the depth of the constraints and no more" $
let ecs = (mkEqConstraints [[path [0,0,0,0], path [1,0,0]]])
ns = [infiniteFNode, infiniteFNode]
ns' = reduceEqConstraints ecs EmptyConstraints ns
ns'' = reduceEqConstraints ecs EmptyConstraints ns'
f = \n -> Node [Edge "f" [n]]
in (ns' == ns'') && ns' == [f $ f $ f infiniteFNode, f $ f infiniteFNode] `shouldBe` True
it "refold folds the simplest unrolled input" $
refold (Node [Edge "f" [infiniteFNode]]) `shouldBe` infiniteFNode
describe "traversals" $ do
it "mapNodes hits each node exactly once" $
-- Note: If the Arbitrary Node instance is changed to return empty or mu nodes, this will need to change
property $ \n -> unsafePerformIO $ do v <- newIORef 0
let n' = mapNodes (\m -> unsafePerformIO (modifyIORef v (+1) >> pure m)) n
let k = nodeCount n'
numInvocations <- k `seq` readIORef v
return $ k == numInvocations
it "nodeCount works on a trivial recursive node" $
nodeCount infiniteFNode `shouldBe` 1
describe "enumeration" $ do
it "naive and sophisticated enumeration are equivalent on nodes without mu" $
property $ mapSize (min 3) $
\n -> HashSet.fromList (naiveDenotation n) `shouldBe` HashSet.fromList (getAllTerms $ reducePartially n)
describe "counted nested Mu" $ do
it "no Mu" $
numNestedMu (Node [Edge "a" []]) `shouldBe` 0
it "single Mu" $
numNestedMu (Mu $ \x -> Node [Edge "f" [x]]) `shouldBe` 1
it "two parallel Mus" $
numNestedMu (Node [Edge "h" [Mu $ \x -> Node [Edge "g" [x]], Mu $ \x -> Node [Edge "h" [x]]]]) `shouldBe` 1
it "nested" $
numNestedMu (Mu $ \x -> Node [Edge "f" [x], Edge "g" [Mu $ \y -> Node [Edge "g" [y]]]]) `shouldBe` 2
describe "nested Mu" $
it "references to different Mu nodes are not confused" $
property $ do
-- Two nodes with very similar structure
-- We are precise about evaluation order here: what we are testing is that after the first term have been
-- interned, we do /NOT/ reuse that term when interning the second. (If we /did/ confuse different references
-- to 'Mu' nodes, @m@ looks precisely like the inner @Mu@ node of @n@.)
n <- evaluate $ Mu $ \r1 -> Mu $ \r2 -> Node [Edge "f" [r1], Edge "g" [r2], Edge "a" []]
m <- evaluate $ Mu $ \r -> Node [Edge "f" [r ], Edge "g" [r ], Edge "a" []]
-- This is a low-level test; crush doesn't work, because we don't see what 'InternedMu' caches.
let collectAllIds :: Node -> Set Int
collectAllIds EmptyNode = Set.empty
collectAllIds (InternedNode node) = Set.unions [
Set.singleton (internedNodeId node)
, Set.unions $ concatMap (map collectAllIds . edgeChildren) (internedNodeEdges node)
]
collectAllIds (InternedMu mu) = Set.unions [
Set.singleton (internedMuId mu)
, Set.union (collectAllIds (internedMuBody mu)) (collectAllIds (internedMuShape mu))
]
collectAllIds (Rec _) = Set.empty
Set.intersection (collectAllIds n) (collectAllIds m) `shouldBe` Set.empty
-------------------------------------
--- Example inputs for the intersection tests
-------------------------------------
-- | Single zero-argument term
intTest1 :: Node
intTest1 = Node [Edge "f" []]
-- | Two zero-argument terms
intTest2 :: Node
intTest2 = Node [Edge "f" [], Edge "g" []]
-- | Single one-argument term, two possible arguments
intTest3 :: Node
intTest3 = Node [Edge "f" [Node [Edge "a" [], Edge "b" []]]]
-- | Two one-argument terms, each two possible arguments (chosen from the same set)
intTest4 :: Node
intTest4 = Node [Edge "f" args, Edge "g" args]
where
args :: [Node]
args = [arg]
arg :: Node
arg = Node [Edge "a" [], Edge "b" []]
-- | Two two-argument terms, no choice for arguments
intTest5 :: Node
intTest5 = Node [Edge "f" args, Edge "g" args]
where
args :: [Node]
args = [argA, argB]
argA, argB :: Node
argA = Node [Edge "a" []]
argB = Node [Edge "b" []]
-- | Two two-argument terms, same choice for arguments, but constrain the two arguments to be the same if choosing f
intTest6 :: Node
intTest6 = Node [mkEdge "f" args cs, Edge "g" args]
where
args :: [Node]
args = [arg, arg]
arg :: Node
arg = Node [Edge "a" [], Edge "b" []]
cs :: EqConstraints
cs = mkEqConstraints [[path [0], path [1]]]
-- | f (f (f (... a)))
intTest7 :: Node
intTest7 = createMu $ \r -> Node [Edge "f" [r], Edge "a" []]
-- | intTest7, once unrolled
intTest8 :: Node
intTest8 = unfoldOuterRec intTest7
-- | Like intTest7, but with an 'inner' unrolling: two f edges before recursing
intTest9 :: Node
intTest9 = createMu $ \r -> Node [Edge "f" [Node [Edge "f" [r], Edge "a" []]], Edge "a" []]
-- | Like intTest9, but with a single additional node on top (not an unrolling: this would result in /two/ additional nodes)
intTest10 :: Node
intTest10 = Node [Edge "f" [intTest9], Edge "a" []]
-- | Example with nested Mu: refer to outer Mu
intTest11 :: Node
intTest11 = createMu $ \r -> createMu $ \_r' -> Node [Edge "f" [r]]
-- | Example with nested Mu: refer to inner Mu
intTest12 :: Node
intTest12 = createMu $ \_r -> createMu $ \r' -> Node [Edge "f" [r']]