ecta (empty) → 1.0.0.0
raw patch · 41 files changed
+6568/−0 lines, 41 filesdep +QuickCheckdep +arraydep +basesetup-changed
Dependencies added: QuickCheck, array, base, cmdargs, containers, criterion, ecta, equivalence, extra, fgl, hashable, hashtables, hspec, ilist, intern, language-dot, lens, mtl, pipes, pretty-simple, raw-strings-qq, text, time, unordered-containers, vector, vector-instances
Files
- ChangeLog.md +3/−0
- LICENSE +30/−0
- README.md +1/−0
- Setup.hs +2/−0
- app/Main.hs +51/−0
- benchmarks/Benchmarks.hs +18/−0
- benchmarks/TestData.hs +23/−0
- ecta.cabal +215/−0
- src/Application/SAT.hs +303/−0
- src/Application/TermSearch/Dataset.hs +1135/−0
- src/Application/TermSearch/Evaluation.hs +80/−0
- src/Application/TermSearch/TermSearch.hs +465/−0
- src/Application/TermSearch/Type.hs +46/−0
- src/Application/TermSearch/Utils.hs +163/−0
- src/Data/ECTA.hs +49/−0
- src/Data/ECTA/Internal/ECTA/Enumeration.hs +462/−0
- src/Data/ECTA/Internal/ECTA/Operations.hs +604/−0
- src/Data/ECTA/Internal/ECTA/Type.hs +642/−0
- src/Data/ECTA/Internal/ECTA/Visualization.hs +194/−0
- src/Data/ECTA/Internal/Paths.hs +465/−0
- src/Data/ECTA/Internal/Paths/Zipper.hs +118/−0
- src/Data/ECTA/Internal/Term.hs +83/−0
- src/Data/ECTA/Paths.hs +36/−0
- src/Data/ECTA/Term.hs +7/−0
- src/Data/HashTable/Extended.hs +26/−0
- src/Data/Interned/Extended/HashTableBased.hs +117/−0
- src/Data/Interned/Extended/SingleThreaded.hs +29/−0
- src/Data/Memoization.hs +168/−0
- src/Data/Memoization/Metrics.hs +22/−0
- src/Data/Persistent/UnionFind.hs +102/−0
- src/Data/Text/Extended/Pretty.hs +16/−0
- src/Utility/Fixpoint.hs +30/−0
- src/Utility/HashJoin.hs +82/−0
- test/CacheProfilingSpec.hs +52/−0
- test/Data/Persistent/UnionFindSpec.hs +78/−0
- test/ECTASpec.hs +351/−0
- test/PathsSpec.hs +179/−0
- test/SATSpec.hs +26/−0
- test/Spec.hs +1/−0
- test/Test/Generators/ECTA.hs +78/−0
- test/Utility/HashJoinSpec.hs +16/−0
+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for compact-coupled-terms++## Unreleased changes
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Jimmy Koppel here (c) 2021++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Author name here nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,1 @@+# ecta: A library for Equality-Constrained Tree Automata
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}++module Main where++import Data.List ( nub )+import qualified Data.Text as Text+import qualified Data.Text.IO as Text+import System.IO ( hFlush, stdout )++import System.Console.CmdArgs ( Data, Typeable, cmdArgs, argPos, auto, (&=), help )++import Data.ECTA+import Data.ECTA.Internal.ECTA.Enumeration+import Data.ECTA.Term+import Data.Persistent.UnionFind+import Application.TermSearch.Evaluation+import Application.TermSearch.Type++----------------------------------------------------------++printAllEdgeSymbols :: Node -> IO ()+printAllEdgeSymbols n = print $ nub $ crush (onNormalNodes $ \(Node es) -> map edgeSymbol es) n+++getTermsNoOccursCheck :: Node -> [Term]+getTermsNoOccursCheck n = map (termFragToTruncatedTerm . fst) $+ flip runEnumerateM (initEnumerationState n) $ do+ _ <- enumerateOutUVar (intToUVar 0)+ getTermFragForUVar (intToUVar 0)++--------------------------------------------------------------------------------++data HPPArgs = HPPArgs { benchmark :: String+ , ablation :: AblationType+ , timeoutLimit :: Int+ }+ deriving (Data, Typeable)++hppArgs :: HPPArgs+hppArgs = HPPArgs {+ benchmark = "" &= argPos 0+ , ablation = Default &= help "Ablation type. choices: [default, no-reduction, no-enumeration]"+ , timeoutLimit = 300 &= help "Timeout limit in seconds"+ } &= auto+++main :: IO ()+main = do+ query <- cmdArgs hppArgs+ runBenchmark (read $ benchmark query) (ablation query) (timeoutLimit query)
+ benchmarks/Benchmarks.hs view
@@ -0,0 +1,18 @@+module Main where++import Criterion.Main++import Data.ECTA+import Data.ECTA.Paths++import TestData++-----------------------------------------------------------------------+++main = do+ defaultMain [+ bgroup "pathable" [+ bench "getPath" $ whnf nodeCount $ getPath (path [2,0,2]) aBigNode+ ]+ ]
+ benchmarks/TestData.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE OverloadedStrings #-}++module TestData (+ aBigNode+ ) where++import Data.ECTA+import Data.ECTA.Internal.ECTA.Type+import Data.ECTA.Internal.Paths++------------------------------------------------------------------------------------++aBigNode :: Node+aBigNode =+ Node [+ mkEdge "app"+ [(Node [(Edge "baseType" [])]),(Node [(Edge "(->)" [])]),(Node [(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "Maybe" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "(->)" [])]),(Node [(mkEdge "app" [(Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])]),(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])] 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 "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] EqConstraints {getEclasses = [PathEClass [Path [2,1],Path [2,2,0]]]})])]),(Edge "foldr" [(Node [(mkEdge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])]),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])])),(Node [(Edge "->" [(Node [(Edge "(->)" [])]),(Node [(Edge "List" [(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])]),(Mu (Node [(Edge "baseType" []),(Edge "->" [(Node [(Edge "(->)" [])]),Rec,Rec]),(Edge "Maybe" [Rec]),(Edge "List" [Rec])]))])])])])] 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]]]})])]+ (mkEqConstraints $ [ [path [1], path [2, 0, 0]]+ , [path [2,0, 1], path [3, 0]]+ , [path [0], path [2, 0, 2]]+ ])+ ]+
+ ecta.cabal view
@@ -0,0 +1,215 @@+cabal-version: 1.12+name: ecta+version: 1.0.0.0+license: BSD3+license-file: LICENSE+copyright: 2021 Jimmy Koppel+maintainer: darmanithird@gmail.com+author: Jimmy Koppel+homepage: https://github.com/jkoppel/ecta#readme+bug-reports: https://github.com/jkoppel/ecta/issues+description:+ Please see the README on GitHub at <https://github.com/jkoppel/ecta#readme>++build-type: Simple+extra-source-files:+ README.md+ ChangeLog.md++source-repository head+ type: git+ location: https://github.com/jkoppel/ecta++flag profile-caches+ default: False+ manual: True++library+ exposed-modules:+ Application.SAT+ Application.TermSearch.Dataset+ Application.TermSearch.Evaluation+ Application.TermSearch.TermSearch+ Application.TermSearch.Type+ Application.TermSearch.Utils+ Data.ECTA+ Data.ECTA.Internal.ECTA.Enumeration+ Data.ECTA.Internal.ECTA.Operations+ Data.ECTA.Internal.ECTA.Type+ Data.ECTA.Internal.ECTA.Visualization+ Data.ECTA.Internal.Paths+ Data.ECTA.Internal.Paths.Zipper+ Data.ECTA.Internal.Term+ Data.ECTA.Paths+ Data.ECTA.Term+ Data.HashTable.Extended+ Data.Interned.Extended.HashTableBased+ Data.Interned.Extended.SingleThreaded+ Data.Memoization+ Data.Memoization.Metrics+ Data.Persistent.UnionFind+ Data.Text.Extended.Pretty+ Utility.Fixpoint+ Utility.HashJoin++ hs-source-dirs: src+ other-modules: Paths_ecta+ default-language: Haskell2010+ default-extensions:+ BangPatterns ConstraintKinds DataKinds DefaultSignatures+ DeriveDataTypeable DeriveGeneric EmptyDataDecls+ ExistentialQuantification FlexibleContexts FlexibleInstances+ FunctionalDependencies GADTs GeneralizedNewtypeDeriving+ KindSignatures LambdaCase MultiParamTypeClasses NamedFieldPuns+ PatternGuards PatternSynonyms RankNTypes ScopedTypeVariables+ StandaloneDeriving TupleSections TypeApplications TypeFamilies+ TypeOperators ViewPatterns++ ghc-options: -Wall+ build-depends:+ array >=0.5.4.0 && <0.6,+ base >=4.14.3.0 && <4.15,+ cmdargs >=0.10.21 && <0.11,+ containers >=0.6.5.1 && <0.7,+ equivalence >=0.3.5 && <0.4,+ extra >=1.7.9 && <1.8,+ fgl >=5.7.0.3 && <5.8,+ hashable >=1.3.0.0 && <1.4,+ hashtables >=1.2.4.2 && <1.3,+ ilist >=0.4.0.1 && <0.5,+ intern >=0.9.4 && <0.10,+ language-dot >=0.1.1 && <0.2,+ lens >=4.19.2 && <4.20,+ mtl >=2.2.2 && <2.3,+ pipes >=4.3.16 && <4.4,+ pretty-simple >=4.0.0.0 && <4.1,+ raw-strings-qq ==1.1.*,+ text >=1.2.4.1 && <1.3,+ time >=1.9.3 && <1.10,+ unordered-containers >=0.2.16.0 && <0.3,+ vector >=0.12.3.1 && <0.13,+ vector-instances ==3.4.*++ if flag(profile-caches)+ cpp-options: -DPROFILE_CACHES++executable hectare+ main-is: Main.hs+ hs-source-dirs: app+ other-modules: Paths_ecta+ default-language: Haskell2010+ default-extensions:+ BangPatterns ConstraintKinds DataKinds DefaultSignatures+ DeriveDataTypeable DeriveGeneric EmptyDataDecls+ ExistentialQuantification FlexibleContexts FlexibleInstances+ FunctionalDependencies GADTs GeneralizedNewtypeDeriving+ KindSignatures LambdaCase MultiParamTypeClasses NamedFieldPuns+ PatternGuards PatternSynonyms RankNTypes ScopedTypeVariables+ StandaloneDeriving TupleSections TypeApplications TypeFamilies+ TypeOperators ViewPatterns++ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall+ build-depends:+ base >=4.14.3.0 && <4.15,+ cmdargs >=0.10.21 && <0.11,+ containers >=0.6.5.1 && <0.7,+ ecta -any,+ hashable >=1.3.0.0 && <1.4,+ language-dot >=0.1.1 && <0.2,+ mtl >=2.2.2 && <2.3,+ pipes >=4.3.16 && <4.4,+ pretty-simple >=4.0.0.0 && <4.1,+ text >=1.2.4.1 && <1.3,+ time >=1.9.3 && <1.10,+ unordered-containers >=0.2.16.0 && <0.3,+ vector >=0.12.3.1 && <0.13++ if flag(profile-caches)+ cpp-options: -DPROFILE_CACHES++test-suite unit-tests+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ build-tool-depends: hspec-discover:hspec-discover -any+ hs-source-dirs: test+ other-modules:+ CacheProfilingSpec+ Data.Persistent.UnionFindSpec+ ECTASpec+ PathsSpec+ SATSpec+ Test.Generators.ECTA+ Utility.HashJoinSpec+ Paths_ecta++ default-language: Haskell2010+ default-extensions:+ BangPatterns ConstraintKinds DataKinds DefaultSignatures+ DeriveDataTypeable DeriveGeneric EmptyDataDecls+ ExistentialQuantification FlexibleContexts FlexibleInstances+ FunctionalDependencies GADTs GeneralizedNewtypeDeriving+ KindSignatures LambdaCase MultiParamTypeClasses NamedFieldPuns+ PatternGuards PatternSynonyms RankNTypes ScopedTypeVariables+ StandaloneDeriving TupleSections TypeApplications TypeFamilies+ TypeOperators ViewPatterns++ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -Wno-orphans+ build-depends:+ QuickCheck >=2.14.2 && <2.15,+ base >=4.14.3.0 && <4.15,+ cmdargs >=0.10.21 && <0.11,+ containers >=0.6.5.1 && <0.7,+ ecta -any,+ equivalence >=0.3.5 && <0.4,+ hashable >=1.3.0.0 && <1.4,+ hspec >=2.7.10 && <2.8,+ language-dot >=0.1.1 && <0.2,+ mtl >=2.2.2 && <2.3,+ pipes >=4.3.16 && <4.4,+ pretty-simple >=4.0.0.0 && <4.1,+ text >=1.2.4.1 && <1.3,+ time >=1.9.3 && <1.10,+ unordered-containers >=0.2.16.0 && <0.3,+ vector >=0.12.3.1 && <0.13++ if flag(profile-caches)+ cpp-options: -DPROFILE_CACHES++benchmark mainbench+ type: exitcode-stdio-1.0+ main-is: Benchmarks.hs+ hs-source-dirs: benchmarks+ other-modules:+ TestData+ Paths_ecta++ default-language: Haskell2010+ default-extensions:+ BangPatterns ConstraintKinds DataKinds DefaultSignatures+ DeriveDataTypeable DeriveGeneric EmptyDataDecls+ ExistentialQuantification FlexibleContexts FlexibleInstances+ FunctionalDependencies GADTs GeneralizedNewtypeDeriving+ KindSignatures LambdaCase MultiParamTypeClasses NamedFieldPuns+ PatternGuards PatternSynonyms RankNTypes ScopedTypeVariables+ StandaloneDeriving TupleSections TypeApplications TypeFamilies+ TypeOperators ViewPatterns++ ghc-options: -threaded -rtsopts -with-rtsopts=-N -O2+ build-depends:+ base >=4.14.3.0 && <4.15,+ cmdargs >=0.10.21 && <0.11,+ containers >=0.6.5.1 && <0.7,+ criterion >=1.5.13.0 && <1.6,+ ecta -any,+ hashable >=1.3.0.0 && <1.4,+ language-dot >=0.1.1 && <0.2,+ mtl >=2.2.2 && <2.3,+ pipes >=4.3.16 && <4.4,+ pretty-simple >=4.0.0.0 && <4.1,+ text >=1.2.4.1 && <1.3,+ time >=1.9.3 && <1.10,+ unordered-containers >=0.2.16.0 && <0.3,+ vector >=0.12.3.1 && <0.13++ if flag(profile-caches)+ cpp-options: -DPROFILE_CACHES
+ src/Application/SAT.hs view
@@ -0,0 +1,303 @@+{-# LANGUAGE OverloadedStrings #-}++-- | A very bad SAT solver written by reduction to ECTA+--+-- Also a constructive proof of the NP-hardness of finding+-- a term represented by an ECTA++module Application.SAT (+ -- * Data types+ Var+ , mkVar+ , CNF(..)+ , Clause(..)+ , Lit(..)++ -- * Solving+ , toEcta+ , allSolutions++ -- * Examples+ , ex1+ , ex2+ , ex3+ ) where++import Data.Hashable ( Hashable )+import Data.HashMap.Strict ( HashMap )+import qualified Data.HashMap.Strict as HashMap+import Data.HashSet ( HashSet )+import qualified Data.HashSet as HashSet+import Data.List ( elemIndex, sort )+import Data.Maybe ( fromJust )+import Data.String (IsString(..) )+import Data.Text ( Text )++import GHC.Generics ( Generic )++import Data.List.Index ( imap )++import Data.ECTA+import Data.ECTA.Paths+import Data.ECTA.Term+import Data.Text.Extended.Pretty+import Utility.Fixpoint++----------------------------------------------------------------++-------------------------------------------------------------------+------------------------- SAT variables ---------------------------+-------------------------------------------------------------------+++newtype Var = Var { unVar :: Text }+ deriving ( Eq, Ord, Show, Generic )++instance Hashable Var++instance IsString Var where+ fromString = Var . fromString++mkVar :: Text -> Var+mkVar = Var++_varToSymbol :: Var -> Symbol+_varToSymbol = Symbol . unVar++_varToNegSymbol :: Var -> Symbol+_varToNegSymbol v = Symbol ("~" <> unVar v)+++-------------------------------------------------------------------+----------------------- CNF representation ------------------------+-------------------------------------------------------------------++-- | Our construction generalizes to arbitrary NNF formulas,+-- and possibly to arbitrary SAT,+-- but we don't need to bother; just CNF is good enough++data CNF = And [Clause]+ deriving ( Eq, Ord, Show, Generic )++instance Hashable CNF++data Clause = Or [Lit]+ deriving ( Eq, Ord, Show, Generic )++instance Hashable Clause++data Lit = PosLit Var+ | NegLit Var+ deriving ( Eq, Ord, Show, Generic )++instance Hashable Lit++instance Pretty Lit where+ pretty (PosLit v) = unVar v+ pretty (NegLit v) = "~" <> unVar v++getLitVar :: Lit -> Var+getLitVar (PosLit v) = v+getLitVar (NegLit v) = v++---------------------+-------- Traversals+---------------------++-- | This is an updatable fold algebra; see "Dealing with Large Bananas"+data CNFAlg a = CNFAlg { runCNF :: CNF -> [a] -> a+ , runClause :: Clause -> [a] -> a+ , runLit :: Lit -> a+ }++_emptyAlg :: (Monoid m) => CNFAlg m+_emptyAlg = CNFAlg (const mempty) (const mempty) (const mempty)+++class FoldAlg a where+ foldAlg :: CNFAlg m -> a -> m++instance FoldAlg CNF where+ foldAlg alg c@(And clauses) = runCNF alg c (map (foldAlg alg) clauses)++instance FoldAlg Clause where+ foldAlg alg c@(Or lits) = runClause alg c (map (foldAlg alg) lits)++instance FoldAlg Lit where+ foldAlg alg l = runLit alg l++crushAlg :: (Monoid m) => (Lit -> m) -> CNFAlg m+crushAlg f = CNFAlg (const mconcat) (const mconcat) f++getVars :: CNF -> HashSet Var+getVars = foldAlg (crushAlg (HashSet.singleton . getLitVar))++-----+-- Lit paths+-----++newtype LitPaths = LitPaths { unLitPaths :: HashMap Lit [Path] }++instance Semigroup LitPaths where+ lp1 <> lp2 = LitPaths $ HashMap.unionWith mappend (unLitPaths lp1) (unLitPaths lp2)++instance Monoid LitPaths where+ mempty = LitPaths HashMap.empty++getLitPathsAlg :: CNFAlg LitPaths+getLitPathsAlg = CNFAlg { runCNF = \_ lps -> mconcat $ imap (\i lp -> LitPaths $ HashMap.map (map (ConsPath i)) $ unLitPaths lp) lps+ , runClause = \_ lps -> mconcat lps+ , runLit = \lit -> LitPaths $ HashMap.singleton lit [EmptyPath]+ }++_getLitPaths :: CNF -> LitPaths+_getLitPaths = foldAlg getLitPathsAlg++-------------------------------------------------------------------+------------------------- ECTA conversion -------------------------+-------------------------------------------------------------------++aNode :: Node+aNode = Node [Edge "a" []]++bNode :: Node+bNode = Node [Edge "b" []]++falseNode :: Node+falseNode = Node [Edge "0" []]++trueNode :: Node+trueNode = Node [Edge "1" []]++falseTerm :: Term+falseTerm = head $ naiveDenotation falseNode++trueTerm :: Term+trueTerm = head $ naiveDenotation trueNode++_trueOrFalseNode :: Node+_trueOrFalseNode = Node [Edge "0" [], Edge "1" []]++posVarNode :: Node+posVarNode = Node [Edge "" [falseNode, aNode], Edge "" [trueNode, bNode]]++negVarNode :: Node+negVarNode = Node [Edge "" [falseNode, bNode], Edge "" [trueNode, aNode]]++++-- | Encoding:+-- formula(assnNode, formulaNode)+--+-- assnNode:+-- * One edge, with one child per literal (2*numVars total)+-- * Each literal has two choices, true or false+-- * Use constraints to force each positive/negative pair of literals to match.+-- * E.g.: x1 node = choice of (0, a) or (1, b). ~x1 node = choice of (0, b) or (1, a)+-- If x1/~x1 have indices 0/1, then the constraint 0.1=1.1 constrains+-- x1/~x1 to be either true/false or false/true+--+-- formulaNode:+-- * One edge, having one child per clause+--+-- Clause nodes:+-- * One edge per literal in the clause, each corresponding to a choice of which variable+-- makes the clause true.+-- * Each edge has 2*numVars children containing a copy of the assnNode, followed by+-- a single child containing "1"+-- * Constrain said final child to be equal to the truth value of the corresponding literal+-- in those 2*numVars children which copy the assnNode+--+-- Top level constraints:+-- * Constrain the variable nodes in each clause node to be equal to the global variable assignments.++toEcta :: CNF -> Node+toEcta formula = Node [mkEdge "formula" [assnNode, formulaNode] litCopyingConstraints]+ where+ clauses :: [Clause]+ And clauses = formula++ numClauses :: Int+ numClauses = length clauses++ sortedVars :: [Var]+ sortedVars = sort $ HashSet.toList $ getVars formula++ numVars :: Int+ numVars = length sortedVars++ litToIndex :: Lit -> Int+ litToIndex (PosLit v) = 2 * fromJust (elemIndex v sortedVars)+ litToIndex (NegLit v) = 2 * fromJust (elemIndex v sortedVars) + 1++ assnNode :: Node+ assnNode = Node [mkEdge "assignment" (concatMap (const [posVarNode, negVarNode]) sortedVars)+ (mkEqConstraints $ map (\i -> [path [2*i, 1], path [2*i+1, 1]])+ [0..numVars - 1])+ ]++ formulaNode :: Node+ formulaNode = Node [Edge "clauses" (map mkClauseNode clauses)]++ mkClauseNode :: Clause -> Node+ mkClauseNode (Or lits) = Node (map mkLitChoiceEdge lits)+ where+ mkLitChoiceEdge :: Lit -> Edge+ mkLitChoiceEdge lit = mkEdge (Symbol $ "choice[" <> pretty lit <> "]")+ (concatMap (const [posVarNode, negVarNode]) sortedVars ++ [trueNode])+ (mkEqConstraints [[path [litToIndex lit, 0], path [2 * numVars]]])+++ litCopyingConstraints :: EqConstraints+ litCopyingConstraints = mkEqConstraints [path [0, i] : [path [1, c, i] | c <- [0..numClauses-1]]+ | i <- [0..2*numVars - 1]+ ]+++allSolutions :: CNF -> HashSet (HashMap Var Bool)+allSolutions formula = foldMap (HashSet.singleton . termToAssignment) $ getAllTerms $ fixUnbounded reducePartially $ toEcta formula+ where+ sortedVars :: [Var]+ sortedVars = sort $ HashSet.toList $ getVars formula++ evens :: [a] -> [a]+ evens [] = []+ evens [x] = [x]+ evens (x:_:l) = x : evens l++ termToAssignment :: Term -> HashMap Var Bool+ termToAssignment (Term _ [Term _ litVals, _]) = foldMap (\(var, Term "" [val, _]) -> HashMap.singleton var (termToBool val))+ (zip sortedVars (evens litVals))+ termToAssignment x = error $ "Unexpected " <> show x++ termToBool :: Term -> Bool+ termToBool t | t == falseTerm = False+ | t == trueTerm = True+ | otherwise = error "termToBool: Invalid argument"+++-------------------------------------------------------------------+------------------------ Example formulae -------------------------+-------------------------------------------------------------------++-- Naive generation: 2^30 * 3^4 possibilities+ex1 :: CNF+ex1 = And [ Or [PosLit "x1", PosLit "x2", PosLit "x3"]+ , Or [NegLit "x1", PosLit "x2", PosLit "x3"]+ , Or [PosLit "x1", NegLit "x2", PosLit "x3"]+ , Or [PosLit "x1", PosLit "x2", NegLit "x3"]+ ]++-- Naive generation: 2^14+ex2 :: CNF+ex2 = And [ Or [PosLit "x1", PosLit "x2"]+ , Or [NegLit "x1", NegLit "x2"]+ ]+++-- Partial reduction of the ECTA effectively performs unit propagation, solving this quickly.+ex3 :: CNF+ex3 = And [ Or [NegLit "x1"]+ , Or [PosLit "x1", PosLit "x2"]+ , Or [NegLit "x2", PosLit "x3"]+ ]
+ src/Application/TermSearch/Dataset.hs view
@@ -0,0 +1,1135 @@+{-# LANGUAGE OverloadedStrings #-}++module Application.TermSearch.Dataset where++import Data.ECTA+import Data.Map ( Map )+import Data.Text ( Text )++import Application.TermSearch.Type+import Application.TermSearch.Utils+++typeToFta :: TypeSkeleton -> Node+typeToFta (TVar "a" ) = var1+typeToFta (TVar "b" ) = var2+typeToFta (TVar "c" ) = var3+typeToFta (TVar "d" ) = var4+typeToFta (TVar "acc") = varAcc+typeToFta (TVar v) =+ error+ $ "Current implementation only supports function signatures with type variables a, b, c, d, and acc, but got "+ ++ show v+typeToFta (TFun t1 t2 ) = arrowType (typeToFta t1) (typeToFta t2)+typeToFta (TCons "Fun" [t1, t2]) = arrowType (typeToFta t1) (typeToFta t2)+typeToFta (TCons s ts ) = mkDatatype s (map typeToFta ts)++speciallyTreatedFunctions :: [Text]+speciallyTreatedFunctions =+ [ -- `($)` is hardcoded to only be in argument position+ "(Data.Function.$)"+ ,+ -- `id` is almost entirely useless, but clogs up the graph. Currently banned+ "Data.Function.id"+ ]++hooglePlusComponents :: [(Text, TypeSkeleton)]+hooglePlusComponents =+ [ ( "(Data.Bool.&&)"+ , TFun (TCons "Bool" []) (TFun (TCons "Bool" []) (TCons "Bool" []))+ )+ , ( "(Data.Bool.||)"+ , TFun (TCons "Bool" []) (TFun (TCons "Bool" []) (TCons "Bool" []))+ )+ , ( "(Data.Eq./=)"+ , TFun (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun (TVar "a") (TFun (TVar "a") (TCons "Bool" [])))+ )+ , ( "(Data.Eq.==)"+ , TFun (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun (TVar "a") (TFun (TVar "a") (TCons "Bool" [])))+ )+ , ( "(Data.Function.$)"+ , TFun (TFun (TVar "a") (TVar "b")) (TFun (TVar "a") (TVar "b"))+ )+ , ( "(GHC.List.!!)"+ , TFun (TCons "List" [TVar "a"]) (TFun (TCons "Int" []) (TVar "a"))+ )+ , ( "(GHC.List.++)"+ , TFun (TCons "List" [TVar "a"])+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ("@@hplusTCInstance@@0EqBool" , TCons "@@hplusTC@@Eq" [TCons "Bool" []])+ , ("@@hplusTCInstance@@0EqChar" , TCons "@@hplusTC@@Eq" [TCons "Char" []])+ , ("@@hplusTCInstance@@0EqDouble", TCons "@@hplusTC@@Eq" [TCons "Double" []])+ , ("@@hplusTCInstance@@0EqFloat" , TCons "@@hplusTC@@Eq" [TCons "Float" []])+ , ("@@hplusTCInstance@@0EqInt" , TCons "@@hplusTC@@Eq" [TCons "Int" []])+ , ("@@hplusTCInstance@@0EqUnit" , TCons "@@hplusTC@@Eq" [TCons "Unit" []])+ , ( "@@hplusTCInstance@@0IsString"+ , TCons "@@hplusTC@@IsString" [TCons "Builder" []]+ )+ , ( "@@hplusTCInstance@@0NumDouble"+ , TCons "@@hplusTC@@Num" [TCons "Double" []]+ )+ , ("@@hplusTCInstance@@0NumFloat", TCons "@@hplusTC@@Num" [TCons "Float" []])+ , ("@@hplusTCInstance@@0NumInt" , TCons "@@hplusTC@@Num" [TCons "Int" []])+ , ("@@hplusTCInstance@@0OrdBool" , TCons "@@hplusTC@@Ord" [TCons "Bool" []])+ , ("@@hplusTCInstance@@0OrdChar" , TCons "@@hplusTC@@Ord" [TCons "Char" []])+ , ( "@@hplusTCInstance@@0OrdDouble"+ , TCons "@@hplusTC@@Ord" [TCons "Double" []]+ )+ , ("@@hplusTCInstance@@0OrdFloat", TCons "@@hplusTC@@Ord" [TCons "Float" []])+ , ("@@hplusTCInstance@@0OrdInt" , TCons "@@hplusTC@@Ord" [TCons "Int" []])+ , ("@@hplusTCInstance@@0ShowBool", TCons "@@hplusTC@@Show" [TCons "Bool" []])+ , ("@@hplusTCInstance@@0ShowChar", TCons "@@hplusTC@@Show" [TCons "Char" []])+ , ( "@@hplusTCInstance@@0ShowDouble"+ , TCons "@@hplusTC@@Show" [TCons "Double" []]+ )+ , ( "@@hplusTCInstance@@0ShowFloat"+ , TCons "@@hplusTC@@Show" [TCons "Float" []]+ )+ , ("@@hplusTCInstance@@0ShowInt" , TCons "@@hplusTC@@Show" [TCons "Int" []])+ , ("@@hplusTCInstance@@0ShowUnit", TCons "@@hplusTC@@Show" [TCons "Unit" []])+ , ( "@@hplusTCInstance@@1Show"+ , TFun+ (TCons "@@hplusTC@@Show" [TVar "a"])+ (TFun (TCons "@@hplusTC@@Show" [TVar "b"])+ (TCons "@@hplusTC@@Show" [TCons "Either" [TVar "a", TVar "b"]])+ )+ )+ , ( "@@hplusTCInstance@@2Read"+ , TFun+ (TCons "@@hplusTC@@Read" [TVar "a"])+ (TFun (TCons "@@hplusTC@@Read" [TVar "b"])+ (TCons "@@hplusTC@@Read" [TCons "Either" [TVar "a", TVar "b"]])+ )+ )+ , ( "@@hplusTCInstance@@3Ord"+ , TFun+ (TCons "@@hplusTC@@Ord" [TVar "a"])+ (TFun (TCons "@@hplusTC@@Ord" [TVar "b"])+ (TCons "@@hplusTC@@Ord" [TCons "Either" [TVar "a", TVar "b"]])+ )+ )+ , ( "@@hplusTCInstance@@4Eq"+ , TFun+ (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun (TCons "@@hplusTC@@Eq" [TVar "b"])+ (TCons "@@hplusTC@@Eq" [TCons "Either" [TVar "a", TVar "b"]])+ )+ )+ , ( "@@hplusTCInstance@@6Semigroup"+ , TCons "@@hplusTC@@Semigroup" [TCons "Either" [TVar "a", TVar "b"]]+ )+ , ( "@@hplusTCInstance@@9Eq"+ , TFun (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TCons "@@hplusTC@@Eq" [TCons "List" [TVar "a"]])+ )+ , ( "Cons"+ , TFun (TVar "a") (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ("Data.Bool.False", TCons "Bool" [])+ , ("Data.Bool.True" , TCons "Bool" [])+ , ( "Data.Bool.bool"+ , TFun (TVar "a") (TFun (TVar "a") (TFun (TCons "Bool" []) (TVar "a")))+ )+ , ("Data.Bool.not" , TFun (TCons "Bool" []) (TCons "Bool" []))+ , ("Data.Bool.otherwise", TCons "Bool" [])+ , ( "Data.ByteString.Builder.byteString"+ , TFun (TCons "ByteString" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.byteStringHex"+ , TFun (TCons "ByteString" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.char7"+ , TFun (TCons "Char" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.char8"+ , TFun (TCons "Char" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.charUtf8"+ , TFun (TCons "Char" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.doubleBE"+ , TFun (TCons "Double" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.doubleDec"+ , TFun (TCons "Double" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.doubleHexFixed"+ , TFun (TCons "Double" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.doubleLE"+ , TFun (TCons "Double" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.floatBE"+ , TFun (TCons "Float" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.floatDec"+ , TFun (TCons "Float" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.floatHexFixed"+ , TFun (TCons "Float" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.floatLE"+ , TFun (TCons "Float" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.hPutBuilder"+ , TFun (TCons "Handle" [])+ (TFun (TCons "Builder" []) (TCons "IO" [TCons "Unit" []]))+ )+ , ( "Data.ByteString.Builder.int16BE"+ , TFun (TCons "Int16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int16Dec"+ , TFun (TCons "Int16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int16HexFixed"+ , TFun (TCons "Int16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int16LE"+ , TFun (TCons "Int16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int32BE"+ , TFun (TCons "Int32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int32Dec"+ , TFun (TCons "Int32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int32HexFixed"+ , TFun (TCons "Int32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int32LE"+ , TFun (TCons "Int32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int64BE"+ , TFun (TCons "Int64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int64Dec"+ , TFun (TCons "Int64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int64HexFixed"+ , TFun (TCons "Int64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int64LE"+ , TFun (TCons "Int64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int8"+ , TFun (TCons "Int8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int8Dec"+ , TFun (TCons "Int8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.int8HexFixed"+ , TFun (TCons "Int8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.intDec"+ , TFun (TCons "Int" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.integerDec"+ , TFun (TCons "Integer" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.lazyByteString"+ , TFun (TCons "ByteString" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.lazyByteStringHex"+ , TFun (TCons "ByteString" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.shortByteString"+ , TFun (TCons "ShortByteString" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.string7"+ , TFun (TCons "List" [TCons "Char" []]) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.string8"+ , TFun (TCons "List" [TCons "Char" []]) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.stringUtf8"+ , TFun (TCons "List" [TCons "Char" []]) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.toLazyByteString"+ , TFun (TCons "Builder" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Builder.word16BE"+ , TFun (TCons "Word16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word16Dec"+ , TFun (TCons "Word16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word16Hex"+ , TFun (TCons "Word16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word16HexFixed"+ , TFun (TCons "Word16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word16LE"+ , TFun (TCons "Word16" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word32BE"+ , TFun (TCons "Word32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word32Dec"+ , TFun (TCons "Word32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word32Hex"+ , TFun (TCons "Word32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word32HexFixed"+ , TFun (TCons "Word32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word32LE"+ , TFun (TCons "Word32" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word64BE"+ , TFun (TCons "Word64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word64Dec"+ , TFun (TCons "Word64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word64Hex"+ , TFun (TCons "Word64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word64HexFixed"+ , TFun (TCons "Word64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word64LE"+ , TFun (TCons "Word64" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word8"+ , TFun (TCons "Word8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word8Dec"+ , TFun (TCons "Word8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word8Hex"+ , TFun (TCons "Word8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.word8HexFixed"+ , TFun (TCons "Word8" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.wordDec"+ , TFun (TCons "Word" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Builder.wordHex"+ , TFun (TCons "Word" []) (TCons "Builder" [])+ )+ , ( "Data.ByteString.Lazy.all"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "Bool" []))+ )+ , ( "Data.ByteString.Lazy.any"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "Bool" []))+ )+ , ( "Data.ByteString.Lazy.append"+ , TFun (TCons "ByteString" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.appendFile"+ , TFun (TCons "List" [TCons "Char" []])+ (TFun (TCons "ByteString" []) (TCons "IO" [TCons "Unit" []]))+ )+ , ( "Data.ByteString.Lazy.break"+ , TFun+ (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" [])+ (TCons "Pair" [TCons "ByteString" [], TCons "ByteString" []])+ )+ )+ , ( "Data.ByteString.Lazy.concat"+ , TFun (TCons "List" [TCons "ByteString" []]) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.concatMap"+ , TFun (TFun (TCons "Word8" []) (TCons "ByteString" []))+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.cons"+ , TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.cons'"+ , TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.copy"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.count"+ , TFun (TCons "Word8" []) (TFun (TCons "ByteString" []) (TCons "Int64" []))+ )+ , ( "Data.ByteString.Lazy.cycle"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.drop"+ , TFun (TCons "Int64" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.dropWhile"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.elem"+ , TFun (TCons "Word8" []) (TFun (TCons "ByteString" []) (TCons "Bool" []))+ )+ , ( "Data.ByteString.Lazy.elemIndex"+ , TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "Maybe" [TCons "Int64" []]))+ )+ , ( "Data.ByteString.Lazy.elemIndexEnd"+ , TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "Maybe" [TCons "Int64" []]))+ )+ , ( "Data.ByteString.Lazy.elemIndices"+ , TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "List" [TCons "Int64" []]))+ )+ , ("Data.ByteString.Lazy.empty", TCons "ByteString" [])+ , ( "Data.ByteString.Lazy.filter"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.find"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "Maybe" [TCons "Word8" []]))+ )+ , ( "Data.ByteString.Lazy.findIndex"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "Maybe" [TCons "Int64" []]))+ )+ , ( "Data.ByteString.Lazy.findIndices"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "List" [TCons "Int64" []]))+ )+ , ( "Data.ByteString.Lazy.foldl"+ , TFun (TFun (TVar "a") (TFun (TCons "Word8" []) (TVar "a")))+ (TFun (TVar "a") (TFun (TCons "ByteString" []) (TVar "a")))+ )+ , ( "Data.ByteString.Lazy.foldl'"+ , TFun (TFun (TVar "a") (TFun (TCons "Word8" []) (TVar "a")))+ (TFun (TVar "a") (TFun (TCons "ByteString" []) (TVar "a")))+ )+ , ( "Data.ByteString.Lazy.foldl1"+ , TFun+ (TFun (TCons "Word8" []) (TFun (TCons "Word8" []) (TCons "Word8" [])))+ (TFun (TCons "ByteString" []) (TCons "Word8" []))+ )+ , ( "Data.ByteString.Lazy.foldl1'"+ , TFun+ (TFun (TCons "Word8" []) (TFun (TCons "Word8" []) (TCons "Word8" [])))+ (TFun (TCons "ByteString" []) (TCons "Word8" []))+ )+ , ( "Data.ByteString.Lazy.foldlChunks"+ , TFun (TFun (TVar "a") (TFun (TCons "ByteString" []) (TVar "a")))+ (TFun (TVar "a") (TFun (TCons "ByteString" []) (TVar "a")))+ )+ , ( "Data.ByteString.Lazy.foldr"+ , TFun (TFun (TCons "Word8" []) (TFun (TVar "a") (TVar "a")))+ (TFun (TVar "a") (TFun (TCons "ByteString" []) (TVar "a")))+ )+ , ( "Data.ByteString.Lazy.foldr1"+ , TFun+ (TFun (TCons "Word8" []) (TFun (TCons "Word8" []) (TCons "Word8" [])))+ (TFun (TCons "ByteString" []) (TCons "Word8" []))+ )+ , ( "Data.ByteString.Lazy.foldrChunks"+ , TFun (TFun (TCons "ByteString" []) (TFun (TVar "a") (TVar "a")))+ (TFun (TVar "a") (TFun (TCons "ByteString" []) (TVar "a")))+ )+ , ( "Data.ByteString.Lazy.fromChunks"+ , TFun (TCons "List" [TCons "ByteString" []]) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.fromStrict"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ("Data.ByteString.Lazy.getContents", TCons "IO" [TCons "ByteString" []])+ , ( "Data.ByteString.Lazy.group"+ , TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.groupBy"+ , TFun+ (TFun (TCons "Word8" []) (TFun (TCons "Word8" []) (TCons "Bool" [])))+ (TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.hGet"+ , TFun (TCons "Handle" [])+ (TFun (TCons "Int" []) (TCons "IO" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.hGetContents"+ , TFun (TCons "Handle" []) (TCons "IO" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.hGetNonBlocking"+ , TFun (TCons "Handle" [])+ (TFun (TCons "Int" []) (TCons "IO" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.hPut"+ , TFun (TCons "Handle" [])+ (TFun (TCons "ByteString" []) (TCons "IO" [TCons "Unit" []]))+ )+ , ( "Data.ByteString.Lazy.hPutNonBlocking"+ , TFun (TCons "Handle" [])+ (TFun (TCons "ByteString" []) (TCons "IO" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.hPutStr"+ , TFun (TCons "Handle" [])+ (TFun (TCons "ByteString" []) (TCons "IO" [TCons "Unit" []]))+ )+ , ( "Data.ByteString.Lazy.head"+ , TFun (TCons "ByteString" []) (TCons "Word8" [])+ )+ , ( "Data.ByteString.Lazy.index"+ , TFun (TCons "ByteString" []) (TFun (TCons "Int64" []) (TCons "Word8" []))+ )+ , ( "Data.ByteString.Lazy.init"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.inits"+ , TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.interact"+ , TFun (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ (TCons "IO" [TCons "Unit" []])+ )+ , ( "Data.ByteString.Lazy.intercalate"+ , TFun+ (TCons "ByteString" [])+ (TFun (TCons "List" [TCons "ByteString" []]) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.intersperse"+ , TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.isPrefixOf"+ , TFun (TCons "ByteString" [])+ (TFun (TCons "ByteString" []) (TCons "Bool" []))+ )+ , ( "Data.ByteString.Lazy.isSuffixOf"+ , TFun (TCons "ByteString" [])+ (TFun (TCons "ByteString" []) (TCons "Bool" []))+ )+ , ( "Data.ByteString.Lazy.iterate"+ , TFun (TFun (TCons "Word8" []) (TCons "Word8" []))+ (TFun (TCons "Word8" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.last"+ , TFun (TCons "ByteString" []) (TCons "Word8" [])+ )+ , ( "Data.ByteString.Lazy.length"+ , TFun (TCons "ByteString" []) (TCons "Int64" [])+ )+ , ( "Data.ByteString.Lazy.map"+ , TFun (TFun (TCons "Word8" []) (TCons "Word8" []))+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.mapAccumL"+ , TFun+ (TFun+ (TVar "acc")+ (TFun (TCons "Word8" []) (TCons "Pair" [TVar "acc", TCons "Word8" []]))+ )+ (TFun+ (TVar "acc")+ (TFun (TCons "ByteString" [])+ (TCons "Pair" [TVar "acc", TCons "ByteString" []])+ )+ )+ )+ , ( "Data.ByteString.Lazy.mapAccumR"+ , TFun+ (TFun+ (TVar "acc")+ (TFun (TCons "Word8" []) (TCons "Pair" [TVar "acc", TCons "Word8" []]))+ )+ (TFun+ (TVar "acc")+ (TFun (TCons "ByteString" [])+ (TCons "Pair" [TVar "acc", TCons "ByteString" []])+ )+ )+ )+ , ( "Data.ByteString.Lazy.maximum"+ , TFun (TCons "ByteString" []) (TCons "Word8" [])+ )+ , ( "Data.ByteString.Lazy.minimum"+ , TFun (TCons "ByteString" []) (TCons "Word8" [])+ )+ , ( "Data.ByteString.Lazy.notElem"+ , TFun (TCons "Word8" []) (TFun (TCons "ByteString" []) (TCons "Bool" []))+ )+ , ( "Data.ByteString.Lazy.null"+ , TFun (TCons "ByteString" []) (TCons "Bool" [])+ )+ , ( "Data.ByteString.Lazy.pack"+ , TFun (TCons "List" [TCons "Word8" []]) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.partition"+ , TFun+ (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" [])+ (TCons "Pair" [TCons "ByteString" [], TCons "ByteString" []])+ )+ )+ , ( "Data.ByteString.Lazy.putStr"+ , TFun (TCons "ByteString" []) (TCons "IO" [TCons "Unit" []])+ )+ , ( "Data.ByteString.Lazy.putStrLn"+ , TFun (TCons "ByteString" []) (TCons "IO" [TCons "Unit" []])+ )+ , ( "Data.ByteString.Lazy.readFile"+ , TFun (TCons "List" [TCons "Char" []]) (TCons "IO" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.repeat"+ , TFun (TCons "Word8" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.replicate"+ , TFun (TCons "Int64" []) (TFun (TCons "Word8" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.reverse"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.scanl"+ , TFun+ (TFun (TCons "Word8" []) (TFun (TCons "Word8" []) (TCons "Word8" [])))+ (TFun (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ )+ , ( "Data.ByteString.Lazy.singleton"+ , TFun (TCons "Word8" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.snoc"+ , TFun (TCons "ByteString" [])+ (TFun (TCons "Word8" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.span"+ , TFun+ (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" [])+ (TCons "Pair" [TCons "ByteString" [], TCons "ByteString" []])+ )+ )+ , ( "Data.ByteString.Lazy.split"+ , TFun+ (TCons "Word8" [])+ (TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.splitAt"+ , TFun+ (TCons "Int64" [])+ (TFun (TCons "ByteString" [])+ (TCons "Pair" [TCons "ByteString" [], TCons "ByteString" []])+ )+ )+ , ( "Data.ByteString.Lazy.splitWith"+ , TFun+ (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.stripPrefix"+ , TFun+ (TCons "ByteString" [])+ (TFun (TCons "ByteString" []) (TCons "Maybe" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.stripSuffix"+ , TFun+ (TCons "ByteString" [])+ (TFun (TCons "ByteString" []) (TCons "Maybe" [TCons "ByteString" []]))+ )+ , ( "Data.ByteString.Lazy.tail"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.tails"+ , TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.take"+ , TFun (TCons "Int64" [])+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.takeWhile"+ , TFun (TFun (TCons "Word8" []) (TCons "Bool" []))+ (TFun (TCons "ByteString" []) (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.toChunks"+ , TFun (TCons "ByteString" []) (TCons "List" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.toStrict"+ , TFun (TCons "ByteString" []) (TCons "ByteString" [])+ )+ , ( "Data.ByteString.Lazy.transpose"+ , TFun (TCons "List" [TCons "ByteString" []])+ (TCons "List" [TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.uncons"+ , TFun+ (TCons "ByteString" [])+ (TCons "Maybe" [TCons "Pair" [TCons "Word8" [], TCons "ByteString" []]])+ )+ , ( "Data.ByteString.Lazy.unfoldr"+ , TFun+ (TFun (TVar "a")+ (TCons "Maybe" [TCons "Pair" [TCons "Word8" [], TVar "a"]])+ )+ (TFun (TVar "a") (TCons "ByteString" []))+ )+ , ( "Data.ByteString.Lazy.unpack"+ , TFun (TCons "ByteString" []) (TCons "List" [TCons "Word8" []])+ )+ , ( "Data.ByteString.Lazy.unsnoc"+ , TFun+ (TCons "ByteString" [])+ (TCons "Maybe" [TCons "Pair" [TCons "ByteString" [], TCons "Word8" []]])+ )+ , ( "Data.ByteString.Lazy.unzip"+ , TFun (TCons "List" [TCons "Pair" [TCons "Word8" [], TCons "Word8" []]])+ (TCons "Pair" [TCons "ByteString" [], TCons "ByteString" []])+ )+ , ( "Data.ByteString.Lazy.writeFile"+ , TFun (TCons "List" [TCons "Char" []])+ (TFun (TCons "ByteString" []) (TCons "IO" [TCons "Unit" []]))+ )+ , ( "Data.ByteString.Lazy.zip"+ , TFun+ (TCons "ByteString" [])+ (TFun (TCons "ByteString" [])+ (TCons "List" [TCons "Pair" [TCons "Word8" [], TCons "Word8" []]])+ )+ )+ , ( "Data.ByteString.Lazy.zipWith"+ , TFun+ (TFun (TCons "Word8" []) (TFun (TCons "Word8" []) (TVar "a")))+ (TFun (TCons "ByteString" [])+ (TFun (TCons "ByteString" []) (TCons "List" [TVar "a"]))+ )+ )+ , ("Data.Either.Left" , TFun (TVar "a") (TCons "Either" [TVar "a", TVar "b"]))+ , ("Data.Either.Right", TFun (TVar "b") (TCons "Either" [TVar "a", TVar "b"]))+ , ( "Data.Either.either"+ , TFun+ (TFun (TVar "a") (TVar "c"))+ (TFun (TFun (TVar "b") (TVar "c"))+ (TFun (TCons "Either" [TVar "a", TVar "b"]) (TVar "c"))+ )+ )+ , ( "Data.Either.fromLeft"+ , TFun (TVar "a") (TFun (TCons "Either" [TVar "a", TVar "b"]) (TVar "a"))+ )+ , ( "Data.Either.fromRight"+ , TFun (TVar "b") (TFun (TCons "Either" [TVar "a", TVar "b"]) (TVar "b"))+ )+ , ( "Data.Either.isLeft"+ , TFun (TCons "Either" [TVar "a", TVar "b"]) (TCons "Bool" [])+ )+ , ( "Data.Either.isRight"+ , TFun (TCons "Either" [TVar "a", TVar "b"]) (TCons "Bool" [])+ )+ , ( "Data.Either.lefts"+ , TFun (TCons "List" [TCons "Either" [TVar "a", TVar "b"]])+ (TCons "List" [TVar "a"])+ )+ , ( "Data.Either.partitionEithers"+ , TFun (TCons "List" [TCons "Either" [TVar "a", TVar "b"]])+ (TCons "Pair" [TCons "List" [TVar "a"], TCons "List" [TVar "b"]])+ )+ , ( "Data.Either.rights"+ , TFun (TCons "List" [TCons "Either" [TVar "a", TVar "b"]])+ (TCons "List" [TVar "b"])+ )+ , ( "Data.List.group"+ , TFun+ (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TCons "List" [TVar "a"]]))+ )+ , ("Data.Maybe.Just" , TFun (TVar "a") (TCons "Maybe" [TVar "a"]))+ , ("Data.Maybe.Nothing", TCons "Maybe" [TVar "a"])+ , ( "Data.Maybe.catMaybes"+ , TFun (TCons "List" [TCons "Maybe" [TVar "a"]]) (TCons "List" [TVar "a"])+ )+ , ("Data.Maybe.fromJust", TFun (TCons "Maybe" [TVar "a"]) (TVar "a"))+ , ( "Data.Maybe.fromMaybe"+ , TFun (TVar "a") (TFun (TCons "Maybe" [TVar "a"]) (TVar "a"))+ )+ , ("Data.Maybe.isJust" , TFun (TCons "Maybe" [TVar "a"]) (TCons "Bool" []))+ , ("Data.Maybe.isNothing", TFun (TCons "Maybe" [TVar "a"]) (TCons "Bool" []))+ , ( "Data.Maybe.listToMaybe"+ , TFun (TCons "List" [TVar "a"]) (TCons "Maybe" [TVar "a"])+ )+ , ( "Data.Maybe.mapMaybe"+ , TFun (TFun (TVar "a") (TCons "Maybe" [TVar "b"]))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "b"]))+ )+ , ( "Data.Maybe.maybe"+ , TFun+ (TVar "b")+ (TFun (TFun (TVar "a") (TVar "b"))+ (TFun (TCons "Maybe" [TVar "a"]) (TVar "b"))+ )+ )+ , ( "Data.Maybe.maybeToList"+ , TFun (TCons "Maybe" [TVar "a"]) (TCons "List" [TVar "a"])+ )+ , ( "Data.Tuple.curry"+ , TFun (TFun (TCons "Pair" [TVar "a", TVar "b"]) (TVar "c"))+ (TFun (TVar "a") (TFun (TVar "b") (TVar "c")))+ )+ , ("Data.Tuple.fst", TFun (TCons "Pair" [TVar "a", TVar "b"]) (TVar "a"))+ , ("Data.Tuple.snd", TFun (TCons "Pair" [TVar "a", TVar "b"]) (TVar "b"))+ , ( "Data.Tuple.swap"+ , TFun (TCons "Pair" [TVar "a", TVar "b"])+ (TCons "Pair" [TVar "b", TVar "a"])+ )+ , ( "Data.Tuple.uncurry"+ , TFun (TFun (TVar "a") (TFun (TVar "b") (TVar "c")))+ (TFun (TCons "Pair" [TVar "a", TVar "b"]) (TVar "c"))+ )+ , ("GHC.Char.chr", TFun (TCons "Int" []) (TCons "Char" []))+ , ( "GHC.Char.eqChar"+ , TFun (TCons "Char" []) (TFun (TCons "Char" []) (TCons "Bool" []))+ )+ , ( "GHC.Char.neChar"+ , TFun (TCons "Char" []) (TFun (TCons "Char" []) (TCons "Bool" []))+ )+ , ( "GHC.List.all"+ , TFun (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"]) (TCons "Bool" []))+ )+ , ("GHC.List.and", TFun (TCons "List" [TCons "Bool" []]) (TCons "Bool" []))+ , ( "GHC.List.any"+ , TFun (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"]) (TCons "Bool" []))+ )+ , ( "GHC.List.break"+ , TFun+ (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"])+ (TCons "Pair" [TCons "List" [TVar "a"], TCons "List" [TVar "a"]])+ )+ )+ , ( "GHC.List.concat"+ , TFun (TCons "List" [TCons "List" [TVar "a"]]) (TCons "List" [TVar "a"])+ )+ , ( "GHC.List.concatMap"+ , TFun (TFun (TVar "a") (TCons "List" [TVar "b"]))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "b"]))+ )+ , ("GHC.List.cycle", TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ , ( "GHC.List.drop"+ , TFun (TCons "Int" [])+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.dropWhile"+ , TFun (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.elem"+ , TFun+ (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun (TVar "a") (TFun (TCons "List" [TVar "a"]) (TCons "Bool" [])))+ )+ , ( "GHC.List.filter"+ , TFun (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.foldl"+ , TFun (TFun (TVar "b") (TFun (TVar "a") (TVar "b")))+ (TFun (TVar "b") (TFun (TCons "List" [TVar "a"]) (TVar "b")))+ )+ , ( "GHC.List.foldl'"+ , TFun (TFun (TVar "b") (TFun (TVar "a") (TVar "b")))+ (TFun (TVar "b") (TFun (TCons "List" [TVar "a"]) (TVar "b")))+ )+ , ( "GHC.List.foldl1"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TVar "a")))+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ( "GHC.List.foldl1'"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TVar "a")))+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ( "GHC.List.foldr"+ , TFun (TFun (TVar "a") (TFun (TVar "b") (TVar "b")))+ (TFun (TVar "b") (TFun (TCons "List" [TVar "a"]) (TVar "b")))+ )+ , ( "GHC.List.foldr1"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TVar "a")))+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ("GHC.List.head", TFun (TCons "List" [TVar "a"]) (TVar "a"))+ , ("GHC.List.init", TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ , ( "GHC.List.iterate"+ , TFun (TFun (TVar "a") (TVar "a"))+ (TFun (TVar "a") (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.iterate'"+ , TFun (TFun (TVar "a") (TVar "a"))+ (TFun (TVar "a") (TCons "List" [TVar "a"]))+ )+ , ("GHC.List.last" , TFun (TCons "List" [TVar "a"]) (TVar "a"))+ , ("GHC.List.length", TFun (TCons "List" [TVar "a"]) (TCons "Int" []))+ , ( "GHC.List.lookup"+ , TFun+ (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun+ (TVar "a")+ (TFun (TCons "List" [TCons "Pair" [TVar "a", TVar "b"]])+ (TCons "Maybe" [TVar "b"])+ )+ )+ )+ , ( "GHC.List.map"+ , TFun (TFun (TVar "a") (TVar "b"))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "b"]))+ )+ , ( "GHC.List.maximum"+ , TFun (TCons "@@hplusTC@@Ord" [TVar "a"])+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ( "GHC.List.minimum"+ , TFun (TCons "@@hplusTC@@Ord" [TVar "a"])+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ( "GHC.List.notElem"+ , TFun+ (TCons "@@hplusTC@@Eq" [TVar "a"])+ (TFun (TVar "a") (TFun (TCons "List" [TVar "a"]) (TCons "Bool" [])))+ )+ , ("GHC.List.null", TFun (TCons "List" [TVar "a"]) (TCons "Bool" []))+ , ("GHC.List.or" , TFun (TCons "List" [TCons "Bool" []]) (TCons "Bool" []))+ , ( "GHC.List.product"+ , TFun (TCons "@@hplusTC@@Num" [TVar "a"])+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ("GHC.List.repeat", TFun (TVar "a") (TCons "List" [TVar "a"]))+ , ( "GHC.List.replicate"+ , TFun (TCons "Int" []) (TFun (TVar "a") (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.reverse"+ , TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"])+ )+ , ( "GHC.List.scanl"+ , TFun+ (TFun (TVar "b") (TFun (TVar "a") (TVar "b")))+ (TFun (TVar "b")+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "b"]))+ )+ )+ , ( "GHC.List.scanl'"+ , TFun+ (TFun (TVar "b") (TFun (TVar "a") (TVar "b")))+ (TFun (TVar "b")+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "b"]))+ )+ )+ , ( "GHC.List.scanl1"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TVar "a")))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.scanr"+ , TFun+ (TFun (TVar "a") (TFun (TVar "b") (TVar "b")))+ (TFun (TVar "b")+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "b"]))+ )+ )+ , ( "GHC.List.scanr1"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TVar "a")))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.span"+ , TFun+ (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"])+ (TCons "Pair" [TCons "List" [TVar "a"], TCons "List" [TVar "a"]])+ )+ )+ , ( "GHC.List.splitAt"+ , TFun+ (TCons "Int" [])+ (TFun (TCons "List" [TVar "a"])+ (TCons "Pair" [TCons "List" [TVar "a"], TCons "List" [TVar "a"]])+ )+ )+ , ( "GHC.List.sum"+ , TFun (TCons "@@hplusTC@@Num" [TVar "a"])+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ("GHC.List.tail", TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ , ( "GHC.List.take"+ , TFun (TCons "Int" [])+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.takeWhile"+ , TFun (TFun (TVar "a") (TCons "Bool" []))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "GHC.List.uncons"+ , TFun (TCons "List" [TVar "a"])+ (TCons "Maybe" [TCons "Pair" [TVar "a", TCons "List" [TVar "a"]]])+ )+ , ( "GHC.List.unzip"+ , TFun (TCons "List" [TCons "Pair" [TVar "a", TVar "b"]])+ (TCons "Pair" [TCons "List" [TVar "a"], TCons "List" [TVar "b"]])+ )+ , ( "GHC.List.unzip3"+ , TFun+ (TCons "List" [TCons "Pair" [TCons "Pair" [TVar "a", TVar "b"], TVar "c"]]+ )+ (TCons+ "Pair"+ [ TCons "Pair" [TCons "List" [TVar "a"], TCons "List" [TVar "b"]]+ , TCons "List" [TVar "c"]+ ]+ )+ )+ , ( "GHC.List.zip"+ , TFun+ (TCons "List" [TVar "a"])+ (TFun (TCons "List" [TVar "b"])+ (TCons "List" [TCons "Pair" [TVar "a", TVar "b"]])+ )+ )+ , ( "GHC.List.zip3"+ , TFun+ (TCons "List" [TVar "a"])+ (TFun+ (TCons "List" [TVar "b"])+ (TFun+ (TCons "List" [TVar "c"])+ (TCons "List"+ [TCons "Pair" [TCons "Pair" [TVar "a", TVar "b"], TVar "c"]]+ )+ )+ )+ )+ , ( "GHC.List.zipWith"+ , TFun+ (TFun (TVar "a") (TFun (TVar "b") (TVar "c")))+ (TFun (TCons "List" [TVar "a"])+ (TFun (TCons "List" [TVar "b"]) (TCons "List" [TVar "c"]))+ )+ )+ , ( "GHC.List.zipWith3"+ , TFun+ (TFun (TVar "a") (TFun (TVar "b") (TFun (TVar "c") (TVar "d"))))+ (TFun+ (TCons "List" [TVar "a"])+ (TFun (TCons "List" [TVar "b"])+ (TFun (TCons "List" [TVar "c"]) (TCons "List" [TVar "d"]))+ )+ )+ )+ , ("Nil", TCons "List" [TVar "a"])+ , ( "Pair"+ , TFun (TVar "a") (TFun (TVar "b") (TCons "Pair" [TVar "a", TVar "b"]))+ )+ , ( "Text.Show.show"+ , TFun (TCons "@@hplusTC@@Show" [TVar "a"])+ (TFun (TVar "a") (TCons "List" [TCons "Char" []]))+ )+ , ( "Text.Show.showChar"+ , TFun+ (TCons "Char" [])+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ , ( "Text.Show.showList"+ , TFun+ (TCons "@@hplusTC@@Show" [TVar "a"])+ (TFun+ (TCons "List" [TVar "a"])+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ )+ , ( "Text.Show.showListWith"+ , TFun+ (TFun+ (TVar "a")+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ (TFun+ (TCons "List" [TVar "a"])+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ )+ , ( "Text.Show.showParen"+ , TFun+ (TCons "Bool" [])+ (TFun+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ )+ , ( "Text.Show.showString"+ , TFun+ (TCons "List" [TCons "Char" []])+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ , ( "Text.Show.shows"+ , TFun+ (TCons "@@hplusTC@@Show" [TVar "a"])+ (TFun+ (TVar "a")+ (TFun (TCons "List" [TCons "Char" []]) (TCons "List" [TCons "Char" []]))+ )+ )+ , ( "Text.Show.showsPrec"+ , TFun+ (TCons "@@hplusTC@@Show" [TVar "a"])+ (TFun+ (TCons "Int" [])+ (TFun+ (TVar "a")+ (TFun (TCons "List" [TCons "Char" []])+ (TCons "List" [TCons "Char" []])+ )+ )+ )+ )+ ]++augumentedComponents :: [(Text, TypeSkeleton)]+augumentedComponents =+ [ + ( "(Data.Function..)"+ , TFun (TFun (TVar "b") (TVar "c"))+ (TFun (TFun (TVar "a") (TVar "b")) (TFun (TVar "a") (TVar "c")))+ )+ , ( "Data.Function.on"+ , TFun+ (TFun (TVar "b") (TFun (TVar "b") (TVar "c")))+ (TFun (TFun (TVar "a") (TVar "b"))+ (TFun (TVar "a") (TFun (TVar "a") (TVar "c")))+ )+ )+ , ( "Data.Function.flip"+ , TFun (TFun (TVar "a") (TFun (TVar "b") (TVar "c")))+ (TFun (TVar "b") (TFun (TVar "a") (TVar "c")))+ )+ , ( "Data.List.groupBy"+ , TFun+ (TFun (TVar "a") (TFun (TVar "a") (TCons "Bool" [])))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TCons "List" [TVar "a"]]))+ )+ , ( "Data.List.sortBy"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TCons "Ordering" [])))+ (TFun (TCons "List" [TVar "a"]) (TCons "List" [TVar "a"]))+ )+ , ( "Data.List.maximumBy"+ , TFun (TFun (TVar "a") (TFun (TVar "a") (TCons "Ordering" [])))+ (TFun (TCons "List" [TVar "a"]) (TVar "a"))+ )+ , ( "Data.Ord.compare"+ , TFun (TCons "@@hplusTC@@Ord" [TVar "a"])+ (TFun (TVar "a") (TFun (TVar "a") (TCons "Ordering" [])))+ )+ ]++hoogleComponents :: Map TypeSkeleton Text+hoogleComponents = fst (mkGroups hooglePlusComponents)++groupMapping :: Map Text Text+groupMapping = snd (mkGroups hooglePlusComponents)++-- switch to this when you run experiments on stackoverflow benchmarks+-- hoogleComponents :: Map TypeSkeleton Text+-- hoogleComponents = fst (mkGroups $ hooglePlusComponents ++ augumentedComponents)++-- groupMapping :: Map Text Text+-- groupMapping = snd (mkGroups $ hooglePlusComponents ++ augumentedComponents)
+ src/Application/TermSearch/Evaluation.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}++module Application.TermSearch.Evaluation+ ( runBenchmark+ ) where++import Control.Monad ( forM_ )+import Data.Time ( diffUTCTime+ , getCurrentTime+ )+import System.IO ( hFlush+ , stdout+ )+import System.Timeout++import qualified Data.Bifunctor as Bi+import qualified Data.Text as Text+import qualified Data.Text.IO as Text++import Data.ECTA+import Data.ECTA.Term++import Application.TermSearch.Dataset+import Application.TermSearch.TermSearch+import Application.TermSearch.Type+import Application.TermSearch.Utils++import qualified Data.Interned.Extended.HashTableBased as Interned+import Data.Interned.Extended.HashTableBased ( cache )+import qualified Data.Memoization as Memoization+import Data.Text.Extended.Pretty++printCacheStatsForReduction :: Node -> IO Node+printCacheStatsForReduction n = do+ let n' = reduceFully n+#ifdef PROFILE_CACHES+ Text.putStrLn $ "Nodes: " <> Text.pack (show (nodeCount n'))+ Text.putStrLn $ "Edges: " <> Text.pack (show (edgeCount n'))+ Text.putStrLn $ "Max indegree: " <> Text.pack (show (maxIndegree n'))+ Memoization.printAllCacheMetrics+ Text.putStrLn =<< (pretty <$> Interned.getMetrics (cache @Node))+ Text.putStrLn =<< (pretty <$> Interned.getMetrics (cache @Edge))+ Text.putStrLn ""+#endif+ hFlush stdout+ return n'++runBenchmark :: Benchmark -> AblationType -> Int -> IO ()+runBenchmark (Benchmark name size sol args res) ablation limit = do+ putStrLn $ "Running benchmark " ++ Text.unpack name++ let argNodes = map (Bi.bimap Symbol typeToFta) args+ let resNode = typeToFta res++ start <- getCurrentTime+ _ <- timeout (limit * 10 ^ (6 :: Int)) $ forM_ [1..size] $ synthesize argNodes resNode+ end <- getCurrentTime+ print $ "Time: " ++ show (diffUTCTime end start)+ hFlush stdout++ where+ synthesize :: [Argument] -> Node -> Int -> IO ()+ synthesize argNodes resNode sz = do+ let anyArg = Node (map (uncurry constArg) argNodes)+ let !filterNode = filterType (relevantTermsOfSize anyArg argNodes sz) resNode+ case ablation of+ NoReduction -> do+ prettyPrintAllTerms ablation (substTerm sol) filterNode+ NoOptimize -> do+ prettyPrintAllTerms ablation (substTerm sol) filterNode+ _ -> do+#ifdef PROFILE_CACHES+ reducedNode <- printCacheStatsForReduction filterNode+#else+ reducedNode <- reduceFullyAndLog filterNode+#endif+ -- let reducedNode = reduceFully filterNode+ let foldedNode = refold reducedNode+ prettyPrintAllTerms ablation (substTerm sol) foldedNode
+ src/Application/TermSearch/TermSearch.hs view
@@ -0,0 +1,465 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}++module Application.TermSearch.TermSearch where++import Data.List ( (\\)+ , permutations+ )+import Data.List.Extra ( nubOrd )+import qualified Data.Map as Map+import Data.Maybe ( fromMaybe )+import Data.Text ( Text )+import Data.Tuple ( swap )+import System.IO ( hFlush+ , stdout+ )++import Data.ECTA+import Data.ECTA.Paths+import Data.ECTA.Term+import Data.Text.Extended.Pretty+import Utility.Fixpoint++import Application.TermSearch.Dataset+import Application.TermSearch.Type+import Application.TermSearch.Utils++------------------------------------------------------------------------------++tau :: Node+tau = createMu+ (\n -> union+ ( [arrowType n n, var1, var2, var3, var4]+ ++ map (Node . (: []) . constructorToEdge n) usedConstructors+ )+ )+ where+ constructorToEdge :: Node -> (Text, Int) -> Edge+ constructorToEdge n (nm, arity) = Edge (Symbol nm) (replicate arity n)++ usedConstructors = allConstructors++allConstructors :: [(Text, Int)]+allConstructors =+ nubOrd (concatMap getConstructors (Map.keys hoogleComponents))+ \\ [("Fun", 2)]+ where+ getConstructors :: TypeSkeleton -> [(Text, Int)]+ getConstructors (TVar _ ) = []+ getConstructors (TFun t1 t2) = getConstructors t1 ++ getConstructors t2+ getConstructors (TCons nm ts) =+ (nm, length ts) : concatMap getConstructors ts++generalize :: Node -> Node+generalize n@(Node [_]) = Node+ [mkEdge s ns' (mkEqConstraints $ map pathsForVar vars)]+ where+ vars = [var1, var2, var3, var4, varAcc]+ nWithVarsRemoved = mapNodes (\x -> if x `elem` vars then tau else x) n+ (Node [Edge s ns']) = nWithVarsRemoved++ pathsForVar :: Node -> [Path]+ pathsForVar v = pathsMatching (== v) n+generalize n = error $ "cannot generalize: " ++ show n++-- Use of `getPath (path [0, 2]) n1` instead of `tau` effectively pre-computes some reduction.+-- Sometimes this can be desirable, but for enumeration,+app :: Node -> Node -> Node+app n1 n2 = Node+ [ mkEdge+ "app"+ [tau, theArrowNode, n1, n2]+ (mkEqConstraints+ [ [path [1], path [2, 0, 0]]+ , [path [3, 0], path [2, 0, 1]]+ , [path [0], path [2, 0, 2]]+ ]+ )+ ]++--------------------------------------------------------------------------------+------------------------------- Relevancy Encoding -----------------------------+--------------------------------------------------------------------------------++applyOperator :: Node+applyOperator = Node+ [ constFunc+ "$"+ (generalize $ arrowType (arrowType var1 var2) (arrowType var1 var2))+ , constFunc "id" (generalize $ arrowType var1 var1)+ ]++hoogleComps :: [Edge]+hoogleComps =+ filter+ (\e ->+ edgeSymbol e+ `notElem` map (Symbol . toMappedName) speciallyTreatedFunctions+ )+ $ map (uncurry parseHoogleComponent . swap)+ $ Map.toList hoogleComponents++anyFunc :: Node+anyFunc = Node hoogleComps++filterType :: Node -> Node -> Node+filterType n t =+ Node [mkEdge "filter" [t, n] (mkEqConstraints [[path [0], path [1, 0]]])]++termsK :: Node -> Bool -> Int -> [Node]+termsK _ _ 0 = []+termsK anyArg False 1 = [anyArg, anyFunc]+termsK anyArg True 1 = [anyArg, anyFunc, applyOperator]+termsK anyArg _ 2 =+ [ app anyListFunc (union [anyNonNilFunc, anyArg, applyOperator])+ , app fromJustFunc (union [anyNonNothingFunc, anyArg, applyOperator])+ , app (union [anyNonListFunc, anyArg]) (union (termsK anyArg True 1))+ ]+termsK anyArg _ k = map constructApp [1 .. (k - 1)]+ where+ constructApp :: Int -> Node+ constructApp i =+ app (union (termsK anyArg False i)) (union (termsK anyArg True (k - i)))++relevantTermK :: Node -> Bool -> Int -> [Argument] -> [Node]+relevantTermK anyArg includeApplyOp k [] = termsK anyArg includeApplyOp k+relevantTermK _ _ 1 [(x, t)] = [Node [constArg x t]]+relevantTermK anyArg _ k argNames+ | k < length argNames = []+ | otherwise = concatMap (\i -> map (constructApp i) allSplits) [1 .. (k - 1)]+ where+ allSplits = map (`splitAt` argNames) [0 .. (length argNames)]++ constructApp :: Int -> ([Argument], [Argument]) -> Node+ constructApp i (xs, ys) =+ let f = union (relevantTermK anyArg False i xs)+ x = union (relevantTermK anyArg True (k - i) ys)+ in app f x++relevantTermsOfSize :: Node -> [Argument] -> Int -> Node+relevantTermsOfSize anyArg args k = union $ concatMap (relevantTermK anyArg True k) (permutations args)++relevantTermsUptoK :: Node -> [Argument] -> Int -> Node+relevantTermsUptoK anyArg args k = union (map (relevantTermsOfSize anyArg args) [1 .. k])++prettyTerm :: Term -> Term+prettyTerm (Term "app" ns) = Term+ "app"+ [prettyTerm (ns !! (length ns - 2)), prettyTerm (ns !! (length ns - 1))]+prettyTerm (Term "filter" ns) = prettyTerm (last ns)+prettyTerm (Term s _ ) = Term s []++dropTypes :: Node -> Node+dropTypes (Node es) = Node (map dropEdgeTypes es)+ where+ dropEdgeTypes (Edge "app" [_, _, a, b]) =+ Edge "app" [dropTypes a, dropTypes b]+ dropEdgeTypes (Edge "filter" [_, a]) = Edge "filter" [dropTypes a]+ dropEdgeTypes (Edge s [_] ) = Edge s []+ dropEdgeTypes e = e+dropTypes n = n++getText :: Symbol -> Text+getText (Symbol s) = s++--------------------------+-------- Remove uninteresting terms+--------------------------++fromJustFunc :: Node+fromJustFunc =+ Node $ filter (\e -> edgeSymbol e `elem` maybeFunctions) hoogleComps++maybeFunctions :: [Symbol]+maybeFunctions =+ [ "Data.Maybe.fromJust"+ , "Data.Maybe.maybeToList"+ , "Data.Maybe.isJust"+ , "Data.Maybe.isNothing"+ ]++listReps :: [Text]+listReps = map+ toMappedName+ [ "Data.Maybe.listToMaybe"+ , "Data.Either.lefts"+ , "Data.Either.rights"+ , "Data.Either.partitionEithers"+ , "Data.Maybe.catMaybes"+ , "GHC.List.head"+ , "GHC.List.last"+ , "GHC.List.tail"+ , "GHC.List.init"+ , "GHC.List.null"+ , "GHC.List.length"+ , "GHC.List.reverse"+ , "GHC.List.concat"+ , "GHC.List.concatMap"+ , "GHC.List.sum"+ , "GHC.List.product"+ , "GHC.List.maximum"+ , "GHC.List.minimum"+ , "(GHC.List.!!)"+ , "(GHC.List.++)"+ ]++isListFunction :: Symbol -> Bool+isListFunction (Symbol sym) = sym `elem` listReps++maybeReps :: [Text]+maybeReps = map+ toMappedName+ [ "Data.Maybe.maybeToList"+ , "Data.Maybe.isJust"+ , "Data.Maybe.isNothing"+ , "Data.Maybe.fromJust"+ ]++isMaybeFunction :: Symbol -> Bool+isMaybeFunction (Symbol sym) = sym `elem` maybeReps++anyListFunc :: Node+anyListFunc = Node $ filter (isListFunction . edgeSymbol) hoogleComps++anyNonListFunc :: Node+anyNonListFunc = Node $ filter+ (\e -> not (isListFunction (edgeSymbol e))+ && not (isMaybeFunction (edgeSymbol e))+ )+ hoogleComps++anyNonNilFunc :: Node+anyNonNilFunc =+ Node $ filter (\e -> edgeSymbol e /= Symbol (toMappedName "Nil")) hoogleComps++anyNonNothingFunc :: Node+anyNonNothingFunc = Node $ filter+ (\e -> edgeSymbol e /= Symbol (toMappedName "Data.Maybe.Nothing"))+ hoogleComps++--------------------------------------------------------------------------------++reduceFully :: Node -> Node+reduceFully = fixUnbounded (withoutRedundantEdges . reducePartially)+-- reduceFully = fixUnbounded (reducePartially)++checkSolution :: Term -> [Term] -> IO ()+checkSolution _ [] = return ()+checkSolution target (s : solutions)+ | prettyTerm s == target = print $ pretty (prettyTerm s)+ | otherwise = do+ -- print $ pretty (prettyTerm s)+ -- print (s)+ checkSolution target solutions++reduceFullyAndLog :: Node -> IO Node+reduceFullyAndLog = go 0+ where+ go :: Int -> Node -> IO Node+ go i n = do+ putStrLn+ $ "Round "+ ++ show i+ ++ ": "+ ++ show (nodeCount n)+ ++ " nodes, "+ ++ show (edgeCount n)+ ++ " edges"+ hFlush stdout+ -- putStrLn $ renderDot $ toDot n+ -- print n+ let n' = withoutRedundantEdges (reducePartially n)+ if n == n' || i >= 30 then return n else go (i + 1) n'++--------------------------------------------------------------------------------+--------------------------------- Test Functions -------------------------------+--------------------------------------------------------------------------------++f1 :: Edge+f1 = constFunc "Nothing" (maybeType tau)++f2 :: Edge+f2 = constFunc "Just" (generalize $ arrowType var1 (maybeType var1))++f3 :: Edge+f3 = constFunc+ "fromMaybe"+ (generalize $ arrowType var1 (arrowType (maybeType var1) var1))++f4 :: Edge+f4 = constFunc "listToMaybe"+ (generalize $ arrowType (listType var1) (maybeType var1))++f5 :: Edge+f5 = constFunc "maybeToList"+ (generalize $ arrowType (maybeType var1) (listType var1))++f6 :: Edge+f6 = constFunc+ "catMaybes"+ (generalize $ arrowType (listType (maybeType var1)) (listType var1))++f7 :: Edge+f7 = constFunc+ "mapMaybe"+ (generalize $ arrowType (arrowType var1 (maybeType var2))+ (arrowType (listType var1) (listType var2))+ )++f8 :: Edge+f8 = constFunc "id" (generalize $ arrowType var1 var1)++f9 :: Edge+f9 = constFunc+ "replicate"+ (generalize $ arrowType (constrType0 "Int") (arrowType var1 (listType var1)))++f10 :: Edge+f10 = constFunc+ "foldr"+ (generalize $ arrowType (arrowType var1 (arrowType var2 var2))+ (arrowType var2 (arrowType (listType var1) var2))+ )++f11 :: Edge+f11 = constFunc+ "iterate"+ (generalize $ arrowType (arrowType var1 var1) (arrowType var1 (listType var1))+ )++f12 :: Edge+f12 = constFunc+ "(!!)"+ (generalize $ arrowType (listType var1) (arrowType (constrType0 "Int") var1))++f13 :: Edge+f13 = constFunc+ "either"+ (generalize $ arrowType+ (arrowType var1 var3)+ (arrowType (arrowType var2 var3)+ (arrowType (constrType2 "Either" var1 var2) var3)+ )+ )++f14 :: Edge+f14 = constFunc+ "Left"+ (generalize $ arrowType var1 (constrType2 "Either" var1 var2))++f15 :: Edge+f15 = constFunc "id" (generalize $ arrowType var1 var1)++f16 :: Edge+f16 = constFunc+ "(,)"+ (generalize $ arrowType var1 (arrowType var2 (constrType2 "Pair" var1 var2)))++f17 :: Edge+f17 =+ constFunc "fst" (generalize $ arrowType (constrType2 "Pair" var1 var2) var1)++f18 :: Edge+f18 =+ constFunc "snd" (generalize $ arrowType (constrType2 "Pair" var1 var2) var2)++f19 :: Edge+f19 = constFunc+ "foldl"+ (generalize $ arrowType (arrowType var2 (arrowType var1 var2))+ (arrowType var2 (arrowType (listType var1) var2))+ )++f20 :: Edge+f20 = constFunc+ "swap"+ ( generalize+ $ arrowType (constrType2 "Pair" var1 var2) (constrType2 "Pair" var2 var1)+ )++f21 :: Edge+f21 = constFunc+ "curry"+ (generalize $ arrowType (arrowType (constrType2 "Pair" var1 var2) var3)+ (arrowType var1 (arrowType var2 var3))+ )++f22 :: Edge+f22 = constFunc+ "uncurry"+ (generalize $ arrowType (arrowType var1 (arrowType var2 var3))+ (arrowType (constrType2 "Pair" var1 var2) var3)+ )++f23 :: Edge+f23 = constFunc "head" (generalize $ arrowType (listType var1) var1)++f24 :: Edge+f24 = constFunc "last" (generalize $ arrowType (listType var1) var1)++f25 :: Edge+f25 = constFunc+ "Data.ByteString.foldr"+ (generalize $ arrowType+ (arrowType (constrType0 "Word8") (arrowType var2 var2))+ (arrowType var2 (arrowType (constrType0 "ByteString") var2))+ )++f26 :: Edge+f26 = constFunc+ "unfoldr"+ (generalize $ arrowType+ (arrowType var1 (maybeType (constrType2 "Pair" (constrType0 "Word8") var1)))+ (arrowType var1 (constrType0 "ByteString"))+ )++f27 :: Edge+f27 = constFunc+ "Data.ByteString.foldrChunks"+ (generalize $ arrowType+ (arrowType (constrType0 "ByteString") (arrowType var2 var2))+ (arrowType var2 (arrowType (constrType0 "ByteString") var2))+ )++f28 :: Edge+f28 = constFunc+ "bool"+ ( generalize+ $ arrowType var1 (arrowType var1 (arrowType (constrType0 "Bool") var1))+ )++f29 :: Edge+f29 = constFunc+ "lookup"+ (generalize $ arrowType+ (constrType1 "@@hplusTC@@Eq" var1)+ (arrowType var1 (arrowType (constrType2 "Pair" var1 var2) (maybeType var2)))+ )++f30 :: Edge+f30 = constFunc "nil" (generalize $ listType var1)++--------------------------+------ Util functions+--------------------------++toMappedName :: Text -> Text+toMappedName x = fromMaybe x (Map.lookup x groupMapping)++prettyPrintAllTerms :: AblationType -> Term -> Node -> IO ()+prettyPrintAllTerms ablation sol n = do+ putStrLn $ "Expected: " ++ show (pretty sol)+ let ts = case ablation of+ NoEnumeration -> naiveDenotation n+ NoOptimize -> naiveDenotation n+ _ -> getAllTerms n+ checkSolution sol ts++substTerm :: Term -> Term+substTerm (Term (Symbol sym) ts) =+ Term (Symbol $ fromMaybe sym (Map.lookup sym groupMapping)) (map substTerm ts)++parseHoogleComponent :: Text -> TypeSkeleton -> Edge+parseHoogleComponent name t =+ constFunc (Symbol name) (generalize $ typeToFta t)
+ src/Application/TermSearch/Type.hs view
@@ -0,0 +1,46 @@+module Application.TermSearch.Type+ ( TypeSkeleton(..)+ , Benchmark(..)+ , Argument+ , Mode(..)+ , AblationType(..)+ ) where++import Data.Data ( Data )+import Data.Hashable ( Hashable )+import Data.Text ( Text )+import GHC.Generics ( Generic )++import Data.ECTA+import Data.ECTA.Term++data TypeSkeleton+ = TVar Text+ | TFun TypeSkeleton TypeSkeleton+ | TCons Text [TypeSkeleton]+ deriving (Eq, Ord, Show, Read, Data, Generic)++instance Hashable TypeSkeleton++data Benchmark = Benchmark { bmName :: Text+ , bmSize :: Int+ , bmSolution :: Term+ , bmArguments :: [(Text, TypeSkeleton)]+ , bmGoalType :: TypeSkeleton+ }+ deriving (Eq, Ord, Show, Read)++type Argument = (Symbol, Node)++data Mode+ = Normal+ | HKTV+ | Lambda+ deriving (Eq, Ord, Show, Data, Generic)++data AblationType+ = Default+ | NoReduction+ | NoEnumeration+ | NoOptimize+ deriving (Eq, Ord, Show, Data, Generic)
+ src/Application/TermSearch/Utils.hs view
@@ -0,0 +1,163 @@+{-# LANGUAGE OverloadedStrings #-}++module Application.TermSearch.Utils where++import Data.Map ( Map )+import qualified Data.Map as Map+import Data.Text ( Text )+import qualified Data.Text as Text++import Data.ECTA+import Data.ECTA.Paths+import Data.ECTA.Term++import Application.TermSearch.Type++--------------------------------------------------------------------------------+------------------------------- Type Constructors ------------------------------+--------------------------------------------------------------------------------++typeConst :: Text -> Node+typeConst s = Node [Edge (Symbol s) []]++constrType0 :: Text -> Node+constrType0 s = Node [Edge (Symbol s) []]++constrType1 :: Text -> Node -> Node+constrType1 s n = Node [Edge (Symbol s) [n]]++constrType2 :: Text -> Node -> Node -> Node+constrType2 s n1 n2 = Node [Edge (Symbol s) [n1, n2]]++maybeType :: Node -> Node+maybeType = constrType1 "Maybe"++listType :: Node -> Node+listType = constrType1 "List"++theArrowNode :: Node+theArrowNode = Node [Edge "(->)" []]++arrowType :: Node -> Node -> Node+arrowType n1 n2 = Node [Edge "->" [theArrowNode, n1, n2]]++appType :: Node -> Node -> Node+appType n1 n2 = Node [Edge "TyApp" [n1, n2]]++mkDatatype :: Text -> [Node] -> Node+mkDatatype s ns = Node [Edge (Symbol s) ns]++--------------------+------- Functions and arguments+--------------------++constFunc :: Symbol -> Node -> Edge+constFunc s t = Edge s [t]++constArg :: Symbol -> Node -> Edge+constArg = constFunc++var1, var2, var3, var4, varAcc :: Node+var1 = Node [Edge "var1" []]+var2 = Node [Edge "var2" []]+var3 = Node [Edge "var3" []]+var4 = Node [Edge "var4" []]+varAcc = Node [Edge "acc" []]++--------------------------------------------------------------------------------++--------------------+------- Component Grouping+--------------------++mkGroups :: [(Text, TypeSkeleton)] -> (Map TypeSkeleton Text, Map Text Text)+mkGroups [] = (Map.empty, Map.empty)+mkGroups ((name, typ):comps) = let (groups, nameToRepresentative) = mkGroups comps+ freshName = Text.pack ("f" <> show (Map.size groups))+ in if typ `Map.member` groups + then (groups, Map.insert name (groups Map.! typ) nameToRepresentative)+ else (Map.insert typ freshName groups, Map.insert name freshName nameToRepresentative)++getRepOf :: [(Text, [Text])] -> Text -> Text+getRepOf [] fname = error $ "cannot find " ++ show fname ++ " in any group"+getRepOf ((x, fnames):xs) fname+ | fname `elem` fnames = x+ | otherwise = getRepOf xs fname+++--------------------+------- Different cases of loops+--------------------++replicatorTau :: Node+replicatorTau = createMu+ (\n -> union+ ([var1, var2] ++ map (Node . (: []) . constructorToEdge n) usedConstructors)+ )+ where+ constructorToEdge :: Node -> (Text, Int) -> Edge+ constructorToEdge n (nm, arity) = Edge (Symbol nm) (replicate arity n)++ usedConstructors = [("Pair", 2)]++replicator :: Node+replicator = Node+ [ mkEdge+ "Pair"+ [ Node+ [ mkEdge "Pair"+ [replicatorTau, replicatorTau]+ (mkEqConstraints [[path [0, 0], path [0, 1], path [1]]])+ ]+ , Node [+ Edge "Pair" [replicatorTau, replicatorTau]]+ ]+ (mkEqConstraints [[path [0, 0], path [0, 1], path [1]]])+ ]++loop1 :: Node+loop1 = Node+ [ mkEdge+ "f"+ [ Node+ [ mkEdge+ "g"+ [ Node+ [ Edge+ "h"+ [ Node+ [ Edge "Pair" [replicatorTau, replicatorTau]+ , Edge "var2" []+ ]+ , Node [Edge "Pair" [replicatorTau, replicatorTau]]+ ]+ ]+ ]+ (mkEqConstraints [[path [0, 0], path [0, 1, 0]]])+ , Edge "gg" [Node [Edge "Pair" [var2, var2]]]+ ]+ ]+ (mkEqConstraints [[path [0, 0, 0], path [0, 0, 1]]])+ ]++loop2 :: Node+loop2 = Node+ [ mkEdge+ "g"+ [ Node+ [ mkEdge "Pair"+ [Node [Edge "List" [replicatorTau]], replicatorTau]+ (mkEqConstraints [[path [0, 0], path [1]]])+ , Edge "f" [var1, Node [Edge "List" [var1]]]+ ]+ , Node+ [ mkEdge "Pair"+ [Node [Edge "List" [replicatorTau]], replicatorTau]+ (mkEqConstraints [[path [0], path [1]]])+ , Edge "f" [var1, var1]+ ]+ ]+ (mkEqConstraints+ [[path [0, 1, 0], path [1, 1]], [path [0, 0], path [1, 0]]]+ )+ ]
+ src/Data/ECTA.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE CPP #-}++-- | Equality-constrained deterministic finite tree automata+--+-- Specialized to DAGs, plus at most one globally unique recursive node++module Data.ECTA (+ Edge(Edge)+ , mkEdge+ , edgeChildren+ , edgeSymbol++ , Node(Node, EmptyNode)+ , nodeEdges+ , numNestedMu+ , createMu++ -- * Operations+ , pathsMatching+ , mapNodes+ , refold+ , unfoldBounded+ , crush+ , onNormalNodes+ , nodeCount+ , edgeCount+ , maxIndegree+ , union+ , intersect+ , withoutRedundantEdges+ , reducePartially++ -- * Enumeration+ , EnumerateM+ , runEnumerateM+ , enumerateFully+ , getAllTerms+ , getAllTruncatedTerms+ , naiveDenotation+++ -- * Visualization / debugging+ , toDot+ ) where++import Data.ECTA.Internal.ECTA.Enumeration+import Data.ECTA.Internal.ECTA.Operations+import Data.ECTA.Internal.ECTA.Type+import Data.ECTA.Internal.ECTA.Visualization
+ src/Data/ECTA/Internal/ECTA/Enumeration.hs view
@@ -0,0 +1,462 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}++module Data.ECTA.Internal.ECTA.Enumeration (+ TermFragment(..)+ , termFragToTruncatedTerm++ , SuspendedConstraint(..)+ , scGetPathTrie+ , scGetUVar+ , descendScs+ , UVarValue(..)++ , EnumerationState(..)+ , uvarCounter+ , uvarRepresentative+ , uvarValues+ , initEnumerationState+++ , EnumerateM+ , getUVarRepresentative+ , assimilateUvarVal+ , mergeNodeIntoUVarVal+ , getUVarValue+ , getTermFragForUVar+ , runEnumerateM+++ , enumerateNode+ , enumerateEdge+ , firstExpandableUVar+ , enumerateOutUVar+ , enumerateOutFirstExpandableUVar+ , enumerateFully+ , expandTermFrag+ , expandUVar++ , getAllTruncatedTerms+ , getAllTerms+ , naiveDenotation+ ) where++import Control.Monad ( forM_, guard )+import Control.Monad.State.Strict ( StateT(..) )+import qualified Data.IntMap as IntMap+import Data.Maybe ( fromMaybe, isJust )+import Data.Monoid ( Any(..) )+import Data.Semigroup ( Max(..) )+import Data.Sequence ( Seq((:<|), (:|>)) )+import qualified Data.Sequence as Sequence+import Control.Monad.Identity ( Identity )++import Control.Lens ( use, ix, (%=), (.=) )+import Control.Lens.TH ( makeLenses )+import Pipes+import qualified Pipes.Prelude as Pipes++import Data.List.Index ( imapM )++import Data.ECTA.Internal.ECTA.Operations+import Data.ECTA.Internal.ECTA.Type+import Data.ECTA.Paths+import Data.ECTA.Term+import Data.Persistent.UnionFind ( UnionFind, UVar, uvarToInt, intToUVar, UVarGen )+import qualified Data.Persistent.UnionFind as UnionFind+import Data.Text.Extended.Pretty++-------------------------------------------------------------------------------+++---------------------------------------------------------------------------+------------------------------- Term fragments ----------------------------+---------------------------------------------------------------------------++data TermFragment = TermFragmentNode !Symbol ![TermFragment]+ | TermFragmentUVar UVar+ deriving ( Eq, Ord, Show )++termFragToTruncatedTerm :: TermFragment -> Term+termFragToTruncatedTerm (TermFragmentNode s ts) = Term s (map termFragToTruncatedTerm ts)+termFragToTruncatedTerm (TermFragmentUVar uv) = Term (Symbol $ "v" <> pretty (uvarToInt uv)) []++---------------------------------------------------------------------------+------------------------------ Enumeration state --------------------------+---------------------------------------------------------------------------++-----------------------+------- Suspended constraints+-----------------------++data SuspendedConstraint = SuspendedConstraint !PathTrie !UVar+ deriving ( Eq, Ord, Show )++scGetPathTrie :: SuspendedConstraint -> PathTrie+scGetPathTrie (SuspendedConstraint pt _) = pt++scGetUVar :: SuspendedConstraint -> UVar+scGetUVar (SuspendedConstraint _ uv) = uv++descendScs :: Int -> Seq SuspendedConstraint -> Seq SuspendedConstraint+descendScs i scs = Sequence.filter (not . isEmptyPathTrie . scGetPathTrie)+ $ fmap (\(SuspendedConstraint pt uv) -> SuspendedConstraint (pathTrieDescend pt i) uv)+ scs++-----------------------+------- UVarValue+-----------------------++data UVarValue = UVarUnenumerated { contents :: !(Maybe Node)+ , constraints :: !(Seq SuspendedConstraint)+ }+ | UVarEnumerated { termFragment :: !TermFragment }+ | UVarEliminated+ deriving ( Eq, Ord, Show )++intersectUVarValue :: UVarValue -> UVarValue -> UVarValue+intersectUVarValue (UVarUnenumerated mn1 scs1) (UVarUnenumerated mn2 scs2) =+ let newContents = case (mn1, mn2) of+ (Nothing, x ) -> x+ (x, Nothing) -> x+ (Just n1, Just n2) -> Just (intersect n1 n2)+ newConstraints = scs1 <> scs2+ in UVarUnenumerated newContents newConstraints++intersectUVarValue UVarEliminated _ = error "intersectUVarValue: Unexpected UVarEliminated"+intersectUVarValue _ UVarEliminated = error "intersectUVarValue: Unexpected UVarEliminated"+intersectUVarValue _ _ = error "intersectUVarValue: Intersecting with enumerated value not implemented"+++-----------------------+------- Top-level state+-----------------------++data EnumerationState = EnumerationState {+ _uvarCounter :: UVarGen+ , _uvarRepresentative :: UnionFind+ , _uvarValues :: Seq UVarValue+ }+ deriving ( Eq, Ord, Show )++makeLenses ''EnumerationState+++initEnumerationState :: Node -> EnumerationState+initEnumerationState n = let (uvg, uv) = UnionFind.nextUVar UnionFind.initUVarGen+ in EnumerationState uvg+ (UnionFind.withInitialValues [uv])+ (Sequence.singleton (UVarUnenumerated (Just n) Sequence.Empty))++++---------------------------------------------------------------------------+---------------------------- Enumeration monad ----------------------------+---------------------------------------------------------------------------++---------------------+-------- Monad+---------------------+++type EnumerateM = StateT EnumerationState []++runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)]+runEnumerateM = runStateT+++---------------------+-------- UVar accessors+---------------------++nextUVar :: EnumerateM UVar+nextUVar = do c <- use uvarCounter+ let (c', uv) = UnionFind.nextUVar c+ uvarCounter .= c'+ return uv++addUVarValue :: Maybe Node -> EnumerateM UVar+addUVarValue x = do uv <- nextUVar+ uvarValues %= (:|> (UVarUnenumerated x Sequence.Empty))+ return uv++getUVarValue :: UVar -> EnumerateM UVarValue+getUVarValue uv = do uv' <- getUVarRepresentative uv+ let idx = uvarToInt uv'+ values <- use uvarValues+ return $ Sequence.index values idx++getTermFragForUVar :: UVar -> EnumerateM TermFragment+getTermFragForUVar uv = termFragment <$> getUVarValue uv++getUVarRepresentative :: UVar -> EnumerateM UVar+getUVarRepresentative uv = do uf <- use uvarRepresentative+ let (uv', uf') = UnionFind.find uv uf+ uvarRepresentative .= uf'+ return uv'++---------------------+-------- Creating UVar's+---------------------++pecToSuspendedConstraint :: PathEClass -> EnumerateM SuspendedConstraint+pecToSuspendedConstraint pec = do uv <- addUVarValue Nothing+ return $ SuspendedConstraint (getPathTrie pec) uv+++---------------------+-------- Merging UVar's / nodes+---------------------++assimilateUvarVal :: UVar -> UVar -> EnumerateM ()+assimilateUvarVal uvTarg uvSrc+ | uvTarg == uvSrc = return ()+ | otherwise = do+ values <- use uvarValues+ let srcVal = Sequence.index values (uvarToInt uvSrc)+ let targVal = Sequence.index values (uvarToInt uvTarg)+ case srcVal of+ UVarEliminated -> return () -- Happens from duplicate constraints+ _ -> do+ let v = intersectUVarValue srcVal targVal+ guard (contents v /= Just EmptyNode)+ uvarValues.(ix $ uvarToInt uvTarg) .= v+ uvarValues.(ix $ uvarToInt uvSrc) .= UVarEliminated+++mergeNodeIntoUVarVal :: UVar -> Node -> Seq SuspendedConstraint -> EnumerateM ()+mergeNodeIntoUVarVal uv n scs = do+ uv' <- getUVarRepresentative uv+ let idx = uvarToInt uv'+ uvarValues.(ix idx) %= intersectUVarValue (UVarUnenumerated (Just n) scs)+ newValues <- use uvarValues+ guard (contents (Sequence.index newValues idx) /= Just EmptyNode)+++---------------------+-------- Variant maintainer+---------------------++-- This thing here might be a performance issue. UPDATE: Yes it is; clocked at 1/3 the time and 1/2 the+-- allocations of enumerateFully+--+-- It exists because it was easier to code / might actually be faster+-- to update referenced uvars here than inline in firstExpandableUVar.+-- There is no Sequence.foldMapWithIndexM.+refreshReferencedUVars :: EnumerateM ()+refreshReferencedUVars = do+ values <- use uvarValues+ updated <- traverse (\case UVarUnenumerated n scs ->+ UVarUnenumerated n <$>+ mapM (\sc -> SuspendedConstraint (scGetPathTrie sc)+ <$> getUVarRepresentative (scGetUVar sc))+ scs++ x -> return x)+ values++ uvarValues .= updated+++---------------------+-------- Core enumeration algorithm+---------------------++enumerateNode :: Seq SuspendedConstraint -> Node -> EnumerateM TermFragment+enumerateNode _ EmptyNode = mzero+enumerateNode scs n =+ let (hereConstraints, descendantConstraints) = Sequence.partition (\(SuspendedConstraint pt _) -> isTerminalPathTrie pt) scs+ in case hereConstraints of+ Sequence.Empty -> case n of+ Mu _ -> TermFragmentUVar <$> addUVarValue (Just n)+ Node es -> enumerateEdge scs =<< lift es+ _ -> error $ "enumerateNode: unexpected node " <> show n++ (x :<| xs) -> do reps <- mapM (getUVarRepresentative . scGetUVar) hereConstraints+ forM_ xs $ \sc -> uvarRepresentative %= UnionFind.union (scGetUVar x) (scGetUVar sc)+ uv <- getUVarRepresentative (scGetUVar x)+ mapM_ (assimilateUvarVal uv) reps++ mergeNodeIntoUVarVal uv n descendantConstraints+ return $ TermFragmentUVar uv++enumerateEdge :: Seq SuspendedConstraint -> Edge -> EnumerateM TermFragment+enumerateEdge scs e = do+ let highestConstraintIndex = getMax $ foldMap (\sc -> Max $ fromMaybe (-1) $ getMaxNonemptyIndex $ scGetPathTrie sc) scs+ guard $ highestConstraintIndex < length (edgeChildren e)++ newScs <- Sequence.fromList <$> mapM pecToSuspendedConstraint (unsafeGetEclasses $ edgeEcs e)+ let scs' = scs <> newScs+ TermFragmentNode (edgeSymbol e) <$> imapM (\i n -> enumerateNode (descendScs i scs') n) (edgeChildren e)+++---------------------+-------- Enumeration-loop control+---------------------++data ExpandableUVarResult = ExpansionStuck | ExpansionDone | ExpansionNext !UVar++-- Can speed this up with bitvectors+firstExpandableUVar :: EnumerateM ExpandableUVarResult+firstExpandableUVar = do+ values <- use uvarValues+ -- check representative uvars because only representatives are updated+ candidateMaps <- mapM (\i -> do rep <- getUVarRepresentative (intToUVar i)+ v <- getUVarValue rep+ case v of+ (UVarUnenumerated (Just (Mu _)) Sequence.Empty) -> return IntMap.empty+ (UVarUnenumerated (Just (Mu _)) _ ) -> return $ IntMap.singleton (uvarToInt rep) (Any False)+ (UVarUnenumerated (Just _) _) -> return $ IntMap.singleton (uvarToInt rep) (Any False)+ _ -> return IntMap.empty)+ [0..(Sequence.length values - 1)]+ let candidates = IntMap.unions candidateMaps++ if IntMap.null candidates then+ return ExpansionDone+ else do+ let ruledOut = foldMap+ (\case (UVarUnenumerated _ scs) -> foldMap+ (\sc -> IntMap.singleton (uvarToInt $ scGetUVar sc) (Any True))+ scs++ _ -> IntMap.empty)+ values++ let unconstrainedCandidateMap = IntMap.filter (not . getAny) (ruledOut <> candidates)+ case IntMap.lookupMin unconstrainedCandidateMap of+ Nothing -> return ExpansionStuck+ Just (i, _) -> return $ ExpansionNext $ intToUVar i++++enumerateOutUVar :: UVar -> EnumerateM TermFragment+enumerateOutUVar uv = do UVarUnenumerated (Just n) scs <- getUVarValue uv+ uv' <- getUVarRepresentative uv++ t <- case n of+ Mu _ -> enumerateNode scs (unfoldOuterRec n)+ _ -> enumerateNode scs n+++ uvarValues.(ix $ uvarToInt uv') .= UVarEnumerated t+ refreshReferencedUVars+ return t++enumerateOutFirstExpandableUVar :: EnumerateM ()+enumerateOutFirstExpandableUVar = do+ muv <- firstExpandableUVar+ case muv of+ ExpansionNext uv -> void $ enumerateOutUVar uv+ ExpansionDone -> mzero+ ExpansionStuck -> mzero++enumerateFully :: EnumerateM ()+enumerateFully = do+ muv <- firstExpandableUVar+ case muv of+ ExpansionStuck -> mzero+ ExpansionDone -> return ()+ ExpansionNext uv -> do UVarUnenumerated (Just n) scs <- getUVarValue uv+ if scs == Sequence.Empty then+ case n of+ Mu _ -> return ()+ _ -> enumerateOutUVar uv >> enumerateFully+ else+ enumerateOutUVar uv >> enumerateFully++---------------------+-------- Expanding an enumerated term fragment into a term+---------------------++expandTermFrag :: TermFragment -> EnumerateM Term+expandTermFrag (TermFragmentNode s ts) = Term s <$> mapM expandTermFrag ts+expandTermFrag (TermFragmentUVar uv) = do val <- getUVarValue uv+ case val of+ UVarEnumerated t -> expandTermFrag t+ UVarUnenumerated (Just (Mu _)) _ -> return $ Term "Mu" []+ _ -> error "expandTermFrag: Non-recursive, unenumerated node encountered"++expandUVar :: UVar -> EnumerateM Term+expandUVar uv = do UVarEnumerated t <- getUVarValue uv+ expandTermFrag t+++---------------------+-------- Full enumeration+---------------------++getAllTruncatedTerms :: Node -> [Term]+getAllTruncatedTerms n = map (termFragToTruncatedTerm . fst) $+ flip runEnumerateM (initEnumerationState n) $ do+ enumerateFully+ getTermFragForUVar (intToUVar 0)++getAllTerms :: Node -> [Term]+getAllTerms n = map fst $ flip runEnumerateM (initEnumerationState n) $ do+ enumerateFully+ expandUVar (intToUVar 0)+++-- | Inefficient enumeration+--+-- For ECTAs with 'Mu' nodes may produce an infinite list or may loop indefinitely, depending on the ECTAs. For example, for+--+-- > createMu $ \r -> Node [Edge "f" [r], Edge "a" []]+--+-- it will produce+--+-- > [ Term "a" []+-- > , Term "f" [Term "a" []]+-- > , Term "f" [Term "f" [Term "a" []]]+-- > , ...+-- > ]+--+-- This happens to work currently because non-recursive edges are interned before recursive edges.+--+-- TODO: It would be much nicer if this did fair enumeration. It would avoid the beforementioned dependency on interning+-- order, and it would give better enumeration for examples such as+--+-- > Node [Edge "h" [+-- > createMu $ \r -> Node [Edge "f" [r], Edge "a" []]+-- > , createMu $ \r -> Node [Edge "g" [r], Edge "b" []]+-- > ]]+--+-- This will currently produce+--+-- > [ Term "h" [Term "a" [], Term "b" []]+-- > , Term "h" [Term "a" [], Term "g" [Term "b" []]]+-- > , Term "h" [Term "a" [], Term "g" [Term "g" [Term "b" []]]]+-- > , ..+-- > ]+--+-- where it always unfolds the /second/ argument to @h@, never the first.+naiveDenotation :: Node -> [Term]+naiveDenotation = naiveDenotationBounded Nothing++-- | set a boundary on the depth of Mu node unfolding+-- if the boundary is set to @Just n@, then @n@ levels of Mu node unfolding will be performed+-- if the boundary is set to @Nothing@, then no boundary is set and the Mu nodes will be always unfolded+naiveDenotationBounded :: Maybe Int -> Node -> [Term]+naiveDenotationBounded maxDepth node = Pipes.toList $ every (go maxDepth node)+ where+ -- | Note that this code uses the decision that f(a,a) does not satisfy the constraint 0.0=1.0 because those paths are empty.+ -- It would be equally valid to say that it does.+ ecsSatisfied :: Term -> EqConstraints -> Bool+ ecsSatisfied t ecs = all (\ps -> isJust (getPath (head ps) t) && all (\p' -> getPath (head ps) t == getPath p' t) ps)+ (map unPathEClass $ unsafeGetEclasses ecs)++ go :: Maybe Int -> Node -> ListT Identity Term+ go _ EmptyNode = mzero+ go mbDepth n@(Mu _) = case mbDepth of+ Nothing -> go Nothing (unfoldOuterRec n)+ Just d | d <= 0 -> mzero+ | otherwise -> go (Just $ d - 1) (unfoldOuterRec n)+ go _ (Rec _) = error "naiveDenotation: unexpected Rec"+ go mbDepth (Node es) = do+ e <- Select $ each es++ children <- mapM (go mbDepth) (edgeChildren e)++ let res = Term (edgeSymbol e) children+ guard $ ecsSatisfied res (edgeEcs e)+ return res
+ src/Data/ECTA/Internal/ECTA/Operations.hs view
@@ -0,0 +1,604 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}++-- For the 'Pathable' instance for 'Node'+{-# OPTIONS_GHC -Wno-orphans #-}++module Data.ECTA.Internal.ECTA.Operations (+ -- * Traversal+ pathsMatching+ , mapNodes+ , crush+ , onNormalNodes++ -- * Unfolding+ , unfoldOuterRec+ , refold+ , nodeEdges+ , unfoldBounded++ -- * Size operations+ , nodeCount+ , edgeCount+ , maxIndegree++ -- * Union+ , union++ -- * Membership+ , nodeRepresents+ , edgeRepresents++ -- * Intersection+ , intersect+ , dropRedundantEdges+ , intersectEdge++ -- * Path operations+ , requirePath+ , requirePathList++ -- * Reduction+ , withoutRedundantEdges+ , reducePartially+ , reduceEdgeIntersection+ , reduceEqConstraints++ -- * Debugging+ , getSubnodeById+ ) where+++import Control.Monad.State.Strict ( evalState, State, MonadState(..), modify' )+import Data.Hashable ( hash, Hashable(..) )+import qualified Data.HashMap.Strict as HashMap+import Data.List ( inits, tails )+import Data.Maybe ( catMaybes )+import Data.Monoid ( Sum(..), First(..) )+import Data.Semigroup ( Max(..) )+import Data.Map.Strict ( Map )+import qualified Data.Map.Strict as Map+import Data.Set ( Set )+import qualified Data.Set as Set++import Control.Lens ( (&), ix, (^?), (%~) )+import Data.List.Index ( imap )++import Data.ECTA.Internal.ECTA.Type+import Data.ECTA.Internal.Paths+import Data.ECTA.Internal.Term++-- Switch the comments on these lines to switch to ekmett's original `intern` library+-- instead of our single-threaded hashtable-based reimplementation.+import Data.Interned.Extended.HashTableBased ( Id )+-- import Data.Interned ( Interned(..), unintern, Id, Cache, mkCache )+-- import Data.Interned.Extended.SingleThreaded ( intern )++import Data.Memoization ( MemoCacheTag(..), memo, memo2 )+import Utility.Fixpoint+import Utility.HashJoin++------------------------------------------------------------------------------------+++-----------------------+------ Traversal+-----------------------++-- | Warning: Linear in number of paths, exponential in size of graph.+-- Only use for very small graphs.+pathsMatching :: (Node -> Bool) -> Node -> [Path]+pathsMatching _ EmptyNode = []+pathsMatching _ (Mu _) = [] -- Unsound!+pathsMatching f n@(Node es) = (concat $ map pathsMatchingEdge es)+ ++ if f n then [EmptyPath] else []+ where+ pathsMatchingEdge :: Edge -> [Path]+ pathsMatchingEdge (Edge _ ns) = concat $ imap (\i x -> map (ConsPath i) $ pathsMatching f x) ns+pathsMatching _ (Rec _) = error $ "pathsMatching: unexpected Rec"++-- | Precondition: For all i, f (Rec i) is either a Rec node meant to represent+-- the enclosing Mu, or contains no Rec node not beneath another Mu.+mapNodes :: (Node -> Node) -> Node -> Node+mapNodes f = go+ where+ -- | Memoized separately for each mapNodes invocation+ go :: Node -> Node+ go = memo (NameTag "mapNodes") go'+ {-# NOINLINE go #-}++ go' :: Node -> Node+ go' EmptyNode = EmptyNode+ go' (Node es) = f $ (Node $ map (\e -> setChildren e $ (map go (edgeChildren e))) es)+ go' (Mu n) = f $ Mu (go . n)+ go' (Rec i) = f $ Rec i++-- This name originates from the "crush" operator in the Stratego language. C.f.: the "crushtdT"+-- combinators in the KURE and compstrat libraries.+--+-- Although m is only constrained to be a monoid, crush makes no guarantees about ordering.+crush :: forall m. (Monoid m) => (Node -> m) -> Node -> m+crush f = \n -> evalState (go n) Set.empty+ where+ go :: (Monoid m) => Node -> State (Set Id) m+ go EmptyNode = return mempty+ go (Rec _) = return mempty+ go n@(InternedMu mu) = mappend (f n) <$> go (internedMuBody mu)+ go n@(InternedNode node) = do+ seen <- get+ let nId = nodeIdentity n+ if Set.member nId seen then+ return mempty+ else do+ modify' (Set.insert nId)+ mappend (f n) <$> (mconcat <$> mapM (\(Edge _ ns) -> mconcat <$> mapM go ns) (internedNodeEdges node))++onNormalNodes :: (Monoid m) => (Node -> m) -> (Node -> m)+onNormalNodes f n@(Node _) = f n+onNormalNodes _ _ = mempty++-----------------------+------ Folding+-----------------------++unfoldOuterRec :: Node -> Node+unfoldOuterRec n@(Mu x) = x n+unfoldOuterRec _ = error "unfoldOuterRec: Must be called on a Mu node"++nodeEdges :: Node -> [Edge]+nodeEdges (Node es) = es+nodeEdges n@(Mu _) = nodeEdges (unfoldOuterRec n)+nodeEdges _ = []++refold :: Node -> Node+refold = memo (NameTag "refold") go+ where+ go :: Node -> Node+ go n = if HashMap.null muNodeMap+ then n+ else fixUnbounded (mapNodes tryUnfold) n+ where+ muNodeMap = crush (\case x@(Mu _) -> HashMap.singleton (unfoldOuterRec x) x+ _ -> HashMap.empty)+ n++ tryUnfold x = case HashMap.lookup x muNodeMap of+ Just y -> y+ Nothing -> x++unfoldBounded :: Int -> Node -> Node+unfoldBounded 0 = mapNodes (\case Mu _ -> EmptyNode+ n -> n)+unfoldBounded k = unfoldBounded (k-1) . mapNodes (\case n@(Mu _) -> unfoldOuterRec n+ n -> n)+++------------+------ Size operations+------------++nodeCount :: Node -> Int+nodeCount = getSum . crush (onNormalNodes $ const $ Sum 1)++edgeCount :: Node -> Int+edgeCount = getSum . crush (onNormalNodes $ \(Node es) -> Sum (length es))++maxIndegree :: Node -> Int+maxIndegree = getMax . crush (onNormalNodes $ \(Node es) -> Max (length es))++------------+------ Membership+------------++nodeRepresents :: Node -> Term -> Bool+nodeRepresents EmptyNode _ = False+nodeRepresents (Node es) t = any (\e -> edgeRepresents e t) es+nodeRepresents n@(Mu _) t = nodeRepresents (unfoldOuterRec n) t+nodeRepresents _ _ = False++edgeRepresents :: Edge -> Term -> Bool+edgeRepresents e = \t@(Term s ts) -> s == edgeSymbol e+ && and (zipWith nodeRepresents (edgeChildren e) ts)+ && all (eclassSatisfied t) (unsafeGetEclasses $ edgeEcs e)+ where+ eclassSatisfied :: Term -> PathEClass -> Bool+ eclassSatisfied t pec = allTheSame $ map (\p -> getPath p t) $ unPathEClass pec++ allTheSame :: (Eq a) => [a] -> Bool+ allTheSame =+ \case+ [] -> True+ x:xs -> go x xs+ where+ go !_ [] = True+ go !x (!y:ys) = (x == y) && (go x ys)+ {-# INLINE allTheSame #-}++------------+------ Intersect+------------++_oldIntersect :: Node -> Node -> Node+_oldIntersect = memo2 (NameTag "intersect") go+ where+ go :: Node -> Node -> Node+ go n1 n2 = refold (nodeDropRedundantEdges (doIntersect n1 n2))+{-# NOINLINE intersect #-}+++-- 7/4/21: The unrolling strategy for intersection totally does not generalize beyond+-- recursive nodes which have a self cycle.+--+-- The following will enter an infinite recursion:+-- > t = createGloballyUniqueMu (\n -> Node [Edge "a" [Node [Edge "a" [n]]]])+-- > intersect t (Node [Edge "a" [t]])+doIntersect :: Node -> Node -> Node+doIntersect EmptyNode _ = EmptyNode+doIntersect _ EmptyNode = EmptyNode+doIntersect n@(Mu _) (Mu _) = n -- TODO: Update for multiple Mu's+doIntersect n1@(Mu _) n2 = doIntersect (unfoldOuterRec n1) n2+doIntersect n1 n2@(Mu _) = doIntersect n1 (unfoldOuterRec n2)+doIntersect n1@(Node es1) n2@(Node es2)+ | n1 == n2 = n1+ | n2 < n1 = intersect n2 n1+ -- `hash` gives a unique ID of the symbol because they're interned+ | otherwise = let joined = hashJoin (hash . edgeSymbol) intersectEdgeSameSymbol es1 es2+ in Node joined+ --Node $ dropRedundantEdges joined+ --mkNodeAlreadyNubbed $ dropRedundantEdges joined+doIntersect n1 n2 = error $ "doIntersect: Unexpected " <> show n1 <> " " <> show n2+++nodeDropRedundantEdges :: Node -> Node+nodeDropRedundantEdges (Node es) = Node $ dropRedundantEdges es+nodeDropRedundantEdges n = n++data RuleOutRes = Keep | RuledOutBy Edge++dropRedundantEdges :: [Edge] -> [Edge]+dropRedundantEdges origEs = concatMap reduceCluster $ {- traceShow (map (\es -> (length es, edgeSymbol $ head es)) clusters, length $ concatMap reduceCluster clusters)-} clusters+ where+ clusters = map (nubByIdSinglePass edgeId) $ clusterByHash (hash . edgeSymbol) origEs++ reduceCluster :: [Edge] -> [Edge]+ reduceCluster [] = []+ reduceCluster (e:es) = case ruleOut e es of+ -- Optimization: If e' > e, likely to be greater than other things;+ -- move it to front and rule out more stuff next iteration.+ --+ -- No noticeable difference in overall wall clock time (7/2/21),+ -- but a few % reduction in calls to intersectEdgeSameSymbol+ (RuledOutBy e', es') -> reduceCluster (e':es')+ (Keep, es') -> e : reduceCluster es'++ ruleOut :: Edge -> [Edge] -> (RuleOutRes, [Edge])+ ruleOut _ [] = (Keep, [])+ ruleOut e (x:xs) = let e' = intersectEdgeSameSymbol e x in+ if e' == x then+ ruleOut e xs+ else if e' == e then+ (RuledOutBy x, xs)+ else+ let (res, notRuledOut) = ruleOut e xs+ in (res, x : notRuledOut)++intersectEdge :: Edge -> Edge -> Maybe Edge+intersectEdge e1 e2+ | edgeSymbol e1 /= edgeSymbol e2 = Nothing+ | otherwise = Just $ intersectEdgeSameSymbol e1 e2++intersectEdgeSameSymbol :: Edge -> Edge -> Edge+intersectEdgeSameSymbol = memo2 (NameTag "intersectEdgeSameSymbol") go+ where+ go e1 e2+ | e2 < e1 = intersectEdgeSameSymbol e2 e1+#ifdef DEFENSIVE_CHECKS+ go (Edge s children1) (Edge _ children2)+ | length children1 /= length children2 = error $ "Different lengths encountered for children of symbol " <> show s+#endif+ go e1 e2 =+ mkEdge (edgeSymbol e1)+ (zipWith intersect (edgeChildren e1) (edgeChildren e2))+ (edgeEcs e1 `combineEqConstraints` edgeEcs e2)+{-# NOINLINE intersectEdgeSameSymbol #-}++------------+------ New intersection+------------++intersect :: Node -> Node -> Node+intersect l r = intersectOpen (emptyIntersectionDom, l, r)++------ Intersection internals++-- | Intersection domain+--+-- Information required to compute the intersection of open terms.+data IntersectionDom = ID {+ -- | Value of all free variables inside the term (so that we can unfold when necessary)+ idFree :: Map Id Node++ -- | Intersection problems we encountered previously (to avoid infinite unrolling)+ , idRecInt :: Set IntersectId+ }+ deriving (Show, Eq)++instance Hashable IntersectionDom where+ -- Implementation notes:+ --+ -- - Both `Map.toList` and `Set.toList` return elements in key-order, which is a suitable canonical form for hashing.+ -- - The cost of the hashing is linear in the size of the domain. If this becomes a concern, we could cache the hash.+ hashWithSalt s (ID free recInt) = hashWithSalt s (Map.toList free, Set.toList recInt)++emptyIntersectionDom :: IntersectionDom+emptyIntersectionDom = ID Map.empty Set.empty++intersectOpen :: (IntersectionDom, Node, Node) -> Node+{-# NOINLINE intersectOpen #-}+intersectOpen = memo (NameTag "intersectOpen") (\(dom, l, r) -> refold $ nodeDropRedundantEdges $ onNode dom l r)+ where+ onNode :: IntersectionDom -> Node -> Node -> Node+ onNode !dom l r =+ case (l, r) of+ -- Rule out empty cases first+ -- This justifies the use of nodeIdentity (@i@, @j@) for the other cases+ (EmptyNode, _) -> EmptyNode+ (_, EmptyNode) -> EmptyNode++ -- For closed terms, improve memoization performance by using the empty environment+ _ | Set.null (freeVars l), Set.null (freeVars r), not (Map.null (idFree dom)) -> intersect l r++ -- Special case for self-intersection (equality check is cheap of course: just uses the interned 'Id')+ _ | l == r, Set.null (freeVars l) -> l++ -- Always intersect nodes in the same order. This is important for two reasons:+ --+ -- 1. It will increase the probability of a cache hit (i.e., improve memoization)+ -- 2. It will increase the probability of being able to use 'ieRecInt'+ _ | l > r -> intersectOpen (dom, r, l)++ -- If we have seen this exact problem before, refer to enclosing Mu.+ _ | Set.member (IntersectId i j) (idRecInt dom) -> Rec (RecIntersect (IntersectId i j))++ -- When encountering a 'Mu', extend the domain appropriately.+ (InternedMu l' , InternedMu r') -> maybeMu $ intersectOpen (extendEnv [(i, l), (j, r)] , internedMuBody l' , internedMuBody r')+ (InternedMu l' , _ ) -> maybeMu $ intersectOpen (extendEnv [(i, l) ] , internedMuBody l' , r )+ (_ , InternedMu r') -> maybeMu $ intersectOpen (extendEnv [ (j, r)] , l , internedMuBody r')++ -- When encountering a free variable, look up the corresponding value in the environment.+ -- (Recall that the case for already-seen intersection problems is are handled above.)+ (Rec l' , _ ) -> intersectOpen (dom , findFreeVar l' , r )+ (_ , Rec r') -> intersectOpen (dom , l , findFreeVar r')++ -- Finally, the real intersection work happens here+ (InternedNode l', InternedNode r') ->+ Node $ hashJoin (hash . edgeSymbol)+ (\e e' -> intersectOpenEdge (dom, e, e'))+ (internedNodeEdges l')+ (internedNodeEdges r')+ where+ -- Node identities (should only be used (forced) if previously established the nodes are not empty)+ i, j :: Id+ i = nodeIdentity l+ j = nodeIdentity r++ -- Extend domain when we encounter a 'Mu'+ -- We might see one or two 'Mu's (if we happen to see a 'Mu' on both sides at once)+ extendEnv :: [(Id, Node)] -> IntersectionDom+ extendEnv bindings = ID {+ idFree = Map.union (Map.fromList bindings) (idFree dom)+ , idRecInt = Set.insert (IntersectId i j) (idRecInt dom)+ }++ -- Find value of free variables in the terms+ -- Since we assume the input terms are fully interned, we only deal with 'RecInt'.+ findFreeVar :: RecNodeId -> Node+ findFreeVar (RecInt intId) | Just n <- Map.lookup intId (idFree dom) = n+ findFreeVar recId = error $ "findFreeVar: unexpected " <> show recId++ -- We only insert a 'Mu' node when necessary.+ maybeMu :: Node -> Node+ maybeMu n+ | RecIntersect (IntersectId i j) `Set.member` freeVars n+ = Mu $ \recNode -> substFree (RecIntersect (IntersectId i j)) recNode n++ | otherwise+ = n++-- | Auxiliary to 'intersectOpen'.+intersectOpenEdge :: (IntersectionDom, Edge, Edge) -> Edge+{-# NOINLINE intersectOpenEdge #-}+intersectOpenEdge = memo (NameTag "intersectOpenEdge") (\(dom, l, r) -> onEdge dom l r)+ where+ onEdge :: IntersectionDom -> Edge -> Edge -> Edge+ onEdge !dom l r =+ mkEdge (edgeSymbol l)+ (zipWith (\a b -> intersectOpen (dom, a, b)) (edgeChildren l) (edgeChildren r))+ (edgeEcs l `combineEqConstraints` edgeEcs r)++------------+------ Union+------------++union :: [Node] -> Node+union ns = case filter (/= EmptyNode) ns of+ [] -> EmptyNode+ ns' -> Node (concat $ map nodeEdges ns')++----------------------+------ Path operations+----------------------++requirePath :: Path -> Node -> Node+requirePath EmptyPath n = n+requirePath _ EmptyNode = EmptyNode+requirePath p n@(Mu _) = requirePath p (unfoldOuterRec n)+requirePath (ConsPath p ps) (Node es) = Node $ map (\e -> setChildren e (requirePathList (ConsPath p ps) (edgeChildren e)))+ $ filter (\e -> length (edgeChildren e) > p)+ es+requirePath _ (Rec _) = error "requirePath: unexpected Rec"++requirePathList :: Path -> [Node] -> [Node]+requirePathList EmptyPath ns = ns+requirePathList (ConsPath p ps) ns = ns & ix p %~ requirePath ps++instance Pathable Node Node where+ type Emptyable Node = Node++ getPath _ EmptyNode = EmptyNode+ getPath EmptyPath n = n+ getPath p n@(Mu _) = getPath p (unfoldOuterRec n)+ getPath (ConsPath p ps) (Node es) = union $ map (getPath ps) (catMaybes (map goEdge es))+ where+ goEdge :: Edge -> Maybe Node+ goEdge (Edge _ ns) = ns ^? ix p+ getPath p n = error $ "getPath: unexpected path " <> show p <> " for node " <> show n++ getAllAtPath _ EmptyNode = []+ getAllAtPath EmptyPath n = [n]+ getAllAtPath p n@(Mu _) = getAllAtPath p (unfoldOuterRec n)+ getAllAtPath (ConsPath p ps) (Node es) = concatMap (getAllAtPath ps) (catMaybes (map goEdge es))+ where+ goEdge :: Edge -> Maybe Node+ goEdge (Edge _ ns) = ns ^? ix p+ getAllAtPath p n = error $ "getAllAtPath: unexpected path " <> show p <> " for node " <> show n++ modifyAtPath f EmptyPath n = f n+ modifyAtPath _ _ EmptyNode = EmptyNode+ modifyAtPath f p n@(Mu _) = modifyAtPath f p (unfoldOuterRec n)+ modifyAtPath f (ConsPath p ps) (Node es) = Node (map goEdge es)+ where+ goEdge :: Edge -> Edge+ goEdge e = setChildren e (edgeChildren e & ix p %~ modifyAtPath f ps)+ modifyAtPath _ p n = error $ "modifyAtPath: unexpected path " <> show p <> " for node " <> show n++instance Pathable [Node] Node where+ type Emptyable Node = Node++ getPath EmptyPath ns = union ns+ getPath (ConsPath p ps) ns = case ns ^? ix p of+ Nothing -> EmptyNode+ Just n -> getPath ps n++ getAllAtPath EmptyPath _ = []+ getAllAtPath (ConsPath p ps) ns = case ns ^? ix p of+ Nothing -> []+ Just n -> getAllAtPath ps n++ modifyAtPath _ EmptyPath ns = ns+ modifyAtPath f (ConsPath p ps) ns = ns & ix p %~ modifyAtPath f ps++++------------------------------------+------ Reduction+------------------------------------++withoutRedundantEdges :: Node -> Node+withoutRedundantEdges n = mapNodes dropReds n+ where+ dropReds (Node es) = Node (dropRedundantEdges es)+ dropReds x = x++---------------+--- Reducing Equality Constraints+---------------++reducePartially :: Node -> Node+reducePartially = reducePartially' EmptyConstraints++reducePartially' :: EqConstraints -> Node -> Node+reducePartially' = memo2 (NameTag "reducePartially'") go+ where+ go :: EqConstraints -> Node -> Node+ go _ EmptyNode = EmptyNode+ go _ (Mu n) = Mu n+ go inheritedEcs n@(Node _) = modifyNode n $ \es -> map (reduceChildren inheritedEcs)+ $ map (reduceEdgeIntersection inheritedEcs) es+ go _ (Rec _) = error "reducePartially: unexpected Rec"++ reduceChildren :: EqConstraints -> Edge -> Edge+ reduceChildren inheritedEcs e = setChildren e $ reduceWithInheritedEcs (inheritedEcs `combineEqConstraints` edgeEcs e) (edgeChildren e)++ -- | Reduce children with inherited constraints+ --+ -- This function is used to avoid infinite unfolding of recursive nodes,+ -- and we do this by passing constraints from the current edge and ancestors to descendants.+ -- For example, let `tau` be "any" node, and we define+ --+ -- > let n1 = Node [ mkEdge "Pair" [tau, tau] (mkEqConstraints [[path [0, 0], path [0, 1], path [1]]])]+ -- > let n2 = Node [ Edge "Pair" [tau, tau] ]+ -- > let n = Node [ mkEdge "Pair" [n1, n2] (mkEqConstraints [[path [0, 0], path [0, 1], path [1]]])]+ --+ -- We notice that, if we call `reducePartially n` without propagating constraints down to its children `n1` or `n2`,+ -- the `tau` can be infinitely expanded between rounds of reduction.+ --+ -- To break such cycles, we actively pass constraints down to children.+ -- In this example, we first call `reducePartially' EmptyConstraints n` at the top level, where the inherited constraint is empty,+ -- so we only need to consider the constraints from the current edge.+ -- Then, we pass the constraints `0.0=0.1=1` down to its children, and `n1` receives `0=1` and `n2` receives nothing.+ -- Next, we reduce the children of `n` by calling `reducePartially' (mkEqConstraints [[path [0], path [1]]]) n1`.+ -- At this node, we will have to combine the inherited constraints `0=1` and the local constraints `0.0=0.1=1`.+ -- Now, we can see that these two constraints contain a contradiction that requires `0=0.0=0.1`, so we can drop the edge.+ --+ -- TODO: this approach does not solve all cases of cycles. See the test case `loop2` in `src/Application/TermSearch/Utils.hs`.+ reduceWithInheritedEcs :: EqConstraints -> [Node] -> [Node]+ reduceWithInheritedEcs EqContradiction children = map (const EmptyNode) children+ reduceWithInheritedEcs inheritedEcs children = zipWith (\i -> reducePartially' (eqConstraintsDescend inheritedEcs i)) [0..] children++{-# NOINLINE reducePartially' #-}++reduceEdgeIntersection :: EqConstraints -> Edge -> Edge+reduceEdgeIntersection = memo2 (NameTag "reduceEdgeIntersection") go+ where+ go :: EqConstraints -> Edge -> Edge+ go ecs e = mkEdge (edgeSymbol e)+ (reduceEqConstraints (edgeEcs e) ecs (edgeChildren e))+ (edgeEcs e)+{-# NOINLINE reduceEdgeIntersection #-}++reduceEqConstraints :: EqConstraints -> EqConstraints -> [Node] -> [Node]+reduceEqConstraints = go+ where+ propagateEmptyNodes :: [Node] -> [Node]+ propagateEmptyNodes ns = if EmptyNode `elem` ns then map (const EmptyNode) ns else ns++ go :: EqConstraints -> EqConstraints -> [Node] -> [Node]+ go ecs inheritedEcs origNs+ | constraintsAreContradictory (ecs `combineEqConstraints` inheritedEcs) = map (const EmptyNode) origNs+ | otherwise = propagateEmptyNodes $ foldr reduceEClass withNeededChildren eclasses+ where+ eclasses = unsafeSubsumptionOrderedEclasses ecs++ -- | TODO: Replace with a "requirePathTrie"+ withNeededChildren = foldr requirePathList origNs (concatMap unPathEClass eclasses)++ intersectList :: [Node] -> Node+ intersectList ns = foldr intersect (head ns) (tail ns)++ _atPaths :: [Node] -> [Path] -> [Node]+ _atPaths ns ps = map (\p -> getPath p ns) ps++ reduceEClass :: PathEClass -> [Node] -> [Node]+ reduceEClass pec ns = foldr (\(p, nsRestIntersected) ns' -> modifyAtPath (intersect nsRestIntersected) p ns')+ ns+ (zip ps (toIntersect ns ps))+ where+ ps = unPathEClass pec++ toIntersect :: [Node] -> [Path] -> [Node]+ --toIntersect ns ps = replicate (length ps) $ intersectList $ map (nodeDropRedundantEdges . flip getPath ns) ps+ --toIntersect ns ps = map intersectList $ dropOnes $ map (nodeDropRedundantEdges . flip getPath ns) ps+ --toIntersect ns ps = replicate (length ps) $ intersectList $ map (flip getPath ns) ps+ toIntersect ns ps = map intersectList $ dropOnes $ map (`getPath` ns) ps++ -- | dropOnes [1,2,3,4] = [[2,3,4], [1,3,4], [1,2,4], [1,2,3]]+ dropOnes :: [a] -> [[a]]+ dropOnes xs = zipWith (++) (inits xs) (tail $ tails xs)++---------------+--- Debugging+---------------++getSubnodeById :: Node -> Id -> Maybe Node+getSubnodeById n i = getFirst $ crush (onNormalNodes $ \x -> if nodeIdentity x == i then First (Just x) else First Nothing) n
+ src/Data/ECTA/Internal/ECTA/Type.hs view
@@ -0,0 +1,642 @@+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}++module Data.ECTA.Internal.ECTA.Type (+ RecNodeId(..)++ , Edge(.., Edge)+ , UninternedEdge(..)+ , mkEdge+ , emptyEdge+ , edgeChildren+ , edgeEcs+ , edgeSymbol+ , setChildren++ , Node(.., Node, Mu)+ , InternedNode(..)+ , InternedMu(..)+ , UninternedNode(..)+ , IntersectId -- opaque+ , pattern IntersectId+ , nodeIdentity+ , numNestedMu+ , substFree+ , freeVars+ , modifyNode+ , createMu+ ) where++import Data.Function ( on )+import Data.Hashable ( Hashable(..) )+import Data.List ( sort )+import Data.Maybe ( fromMaybe )+import Data.Map.Strict ( Map )+import qualified Data.Map.Strict as Map+import Data.Set ( Set )+import qualified Data.Set as Set++import GHC.Generics ( Generic )++import System.IO.Unsafe ( unsafePerformIO )++import Data.List.Extra ( nubSort )++-- Switch the comments on these lines to switch to ekmett's original `intern` library+-- instead of our single-threaded hashtable-based reimplementation.+import Data.Interned.Extended.HashTableBased++-- NOTE 2/7/2022: This version is likely to break because there are nested calls to intern+-- for Mu nodes. See related comment in HashTableBased.hs+--import Data.Interned ( Interned(..), unintern, Id, Cache, mkCache )+--import Data.Interned.Extended.SingleThreaded ( intern )++import Data.ECTA.Internal.Paths+import Data.ECTA.Internal.Term+++import Data.Memoization++---------------------------------------------------------------------------------------------++-----------------------------------------------------------------+-------------------------- Mu node table ------------------------+-----------------------------------------------------------------++data RecNodeId =+ -- | Reference to the 'Id' of an interned 'Mu' node+ RecInt !Id++ -- | Reference to an as-yet uninterned 'Mu' node, for which the 'Id' is not yet known+ --+ -- The 'Int' argument is used to distinguish between multiple nested 'Mu' nodes.+ --+ -- NOTE: This is intentionally not an 'Id': it does not refer to the 'Id' of any interned node.+ | RecUnint Int++ -- | Placeholder variable that we use /only/ for depth calculations+ --+ -- The invariant that this is used /only/ for depth calculations, along with the observation that depth calculation+ -- does not depend on the exact choice of variable, justifies subtituting any other variable for 'RecDepth' in terms+ -- containing 'RecDepth' in all contexts.+ | RecDepth++ -- | Refer to Mu-node-to-be-constructed during intersection+ --+ -- TODO: It is obviously not very elegant to have a constructor here specifically for one algorithm. Ideally, we+ -- would parameterize 'Node' with the type of the identifiers in it. This might be useful also to rule out many+ -- other cases (specifically, most of the time we are dealing with fully interned nodes, and so the only+ -- constructor we expect is 'RecInt').+ | RecIntersect IntersectId+ deriving ( Eq, Ord, Show, Generic )++-- | Context-free references to a 'Mu' node introduced by 'intersect'+--+-- Background: This is a generalization of the idea to be able to refer to the "immediately enclosing binder", and then+-- only deal with graphs with the property that we never need to refer past that enclosing binder. This too would allow+-- us to refer to a 'Mu' node without knowing its 'Id', at the cost of requiring a substitution when we discover that+-- 'Id' to return this into a 'RecInt'. The generalization is that all we need to /some/ way to refer to that 'Mu' node+-- concretely, without 'Id', but we can: intersection introduces 'Mu' whenever it encounters a 'Mu' on the left or the+-- right, /and will then not introduce another 'Mu' for that same intersection problem (at least, not in the same+-- scope). This means that the 'Id' of the left and right operand will indeed uniquely identify the 'Mu' node to be+-- constructed by 'intersect'.+--+-- Furthermore, since we cache the free variables in a term, we have a cheap check to see if we need the 'Mu' node at+-- all. This means that /if/ the input graphs satisfy the property that there are references past 'Mu' nodes, the output+-- should too: we will not introduce redundant 'Mu' nodes.+--+-- NOTE: Although intersect has three cases in which it introduces 'Mu' nodes ('Mu' in both operands, 'Mu' in the left,+-- or 'Mu' in the right), we don't need that distinction here: we just need to know the 'Id' of the two operands, so+-- that if we see a call to intersect again /with those same two operands/ (no matter what kind of nodes they are), we+-- can refer to the newly constructed 'Mu' node.+data IntersectId =+ -- Invariant: the two 'Id's should be ordered (guaranteed by the pattern synonym constructor)+ UnsafeIntersectId !Id !Id+ deriving ( Eq, Ord, Show, Generic )++pattern IntersectId :: Id -> Id -> IntersectId+pattern IntersectId i j <- (UnsafeIntersectId i j)+ where+ IntersectId i j | i <= j = UnsafeIntersectId i j+ | otherwise = UnsafeIntersectId j i++instance Hashable RecNodeId+instance Hashable IntersectId++-----------------------------------------------------------------+----------------------------- Edges -----------------------------+-----------------------------------------------------------------++data Edge = InternedEdge { edgeId :: !Id+ , uninternedEdge :: !UninternedEdge+ }++instance Show Edge where+ show e | edgeEcs e == EmptyConstraints = "(Edge " ++ show (edgeSymbol e) ++ " " ++ show (edgeChildren e) ++ ")"+ | otherwise = "(mkEdge " ++ show (edgeSymbol e) ++ " " ++ show (edgeChildren e) ++ " " ++ show (edgeEcs e) ++ ")"++--instance Show Edge where+-- show e = "InternedEdge " ++ show (edgeId e) ++ " " ++ show (edgeSymbol e) ++ " " ++ show (edgeChildren e) ++ " " ++ show (edgeEcs e)++edgeSymbol :: Edge -> Symbol+edgeSymbol = uEdgeSymbol . uninternedEdge++edgeChildren :: Edge -> [Node]+edgeChildren = uEdgeChildren . uninternedEdge++edgeEcs :: Edge -> EqConstraints+edgeEcs = uEdgeEcs . uninternedEdge++instance Eq Edge where+ (InternedEdge {edgeId = n1}) == (InternedEdge {edgeId = n2}) = n1 == n2++instance Ord Edge where+ compare = compare `on` edgeId++instance Hashable Edge where+ hashWithSalt s e = s `hashWithSalt` (edgeId e)+++-----------------------------------------------------------------+------------------------------ Nodes ----------------------------+-----------------------------------------------------------------++data InternedMu = MkInternedMu {+ -- | 'Id' of the node itself+ internedMuId :: {-# UNPACK #-} !Id++ -- | The body of the 'Mu'+ --+ -- Recursive occurrences to this node should be+ --+ -- > Rec (RecNodeId internedMuId)+ , internedMuBody :: !Node++ -- | The body of the 'Mu', before it was assigned an 'Id'+ --+ -- Invariant:+ --+ -- > substFree internedMuId (Rec (RecUnint (numNestedMu internedMuBody)) internedMuBody+ -- > == internedMuShape+ , internedMuShape :: !Node+ }+ deriving (Show)++data InternedNode = MkInternedNode {+ -- | The 'Id' of the node itself+ internedNodeId :: {-# UNPACK #-} !Id++ -- | All outgoing edges+ , internedNodeEdges :: ![Edge]++ -- | Maximum Mu nesting depth in the term+ , internedNodeNumNestedMu :: !Int++ -- | Free variables in the term+ , internedNodeFree :: !(Set RecNodeId)+ }+ deriving (Show)++data Node = InternedNode {-# UNPACK #-} !InternedNode+ | EmptyNode+ | InternedMu {-# UNPACK #-} !InternedMu+ | Rec !RecNodeId++instance Eq Node where+ InternedNode l == InternedNode r = internedNodeId l == internedNodeId r+ InternedMu l == InternedMu r = internedMuId l == internedMuId r+ Rec l == Rec r = l == r+ EmptyNode == EmptyNode = True+ _ == _ = False++instance Show Node where+ show (InternedNode node) = "(Node " <> show (internedNodeEdges node) <> ")"+ show EmptyNode = "EmptyNode"+ show (InternedMu mu) = "(Mu " <> show (internedMuId mu) <> " " <> show (internedMuBody mu) <> ")"+ show (Rec n) = "(Rec " <> show n <> ")"++instance Ord Node where+ compare n1 n2 = compare (nodeDescriptorInt n1) (nodeDescriptorInt n2)+ where+ nodeDescriptorInt :: Node -> Int+ nodeDescriptorInt EmptyNode = -1+ nodeDescriptorInt (InternedNode node) = 3*i+ where+ i = internedNodeId node+ nodeDescriptorInt (InternedMu mu) = 3*i + 1+ where+ i = internedMuId mu+ nodeDescriptorInt (Rec recId) = 3*i + 2+ where+ i = case recId of+ RecInt nid -> nid+ _otherwise -> error $ "compare: unexpected " <> show recId+++instance Hashable Node where+ hashWithSalt s EmptyNode = s `hashWithSalt` (-1 :: Int)+ hashWithSalt s (InternedMu mu) = s `hashWithSalt` (-2 :: Int) `hashWithSalt` i+ where+ i = internedMuId mu+ hashWithSalt s (Rec i) = s `hashWithSalt` (-3 :: Int) `hashWithSalt` i+ hashWithSalt s (InternedNode node) = s `hashWithSalt` i+ where+ i = internedNodeId node++-- | Maximum number of nested Mus in the term+--+-- @O(1) provided that there are no unbounded Mu chains in the term.+numNestedMu :: Node -> Int+numNestedMu EmptyNode = 0+numNestedMu (InternedNode node) = internedNodeNumNestedMu node+numNestedMu (InternedMu mu) = 1 + numNestedMu (internedMuBody mu)+numNestedMu (Rec _) = 0++-- | Free variables in the term+--+-- @O(1) in the size of the graph, provided that there are no unbounded Mu chains in the term.+-- @O(log n)@ in the number of free variables in the graph, which we expect to be orders of magnitude smaller than the+-- size of the graph (indeed, we don't expect more than a handful).+freeVars :: Node -> Set RecNodeId+freeVars EmptyNode = Set.empty+freeVars (InternedNode node) = internedNodeFree node+freeVars (InternedMu mu) = Set.delete (RecInt (internedMuId mu)) (freeVars (internedMuBody mu))+freeVars (Rec i) = Set.singleton i++----------------------+------ Getters and setters+----------------------++nodeIdentity :: Node -> Id+nodeIdentity (InternedMu mu) = internedMuId mu+nodeIdentity (InternedNode node) = internedNodeId node+nodeIdentity (Rec (RecInt i)) = i+nodeIdentity n = error $ "nodeIdentity: unexpected node " <> show n++setChildren :: Edge -> [Node] -> Edge+setChildren e ns = mkEdge (edgeSymbol e) ns (edgeEcs e)++_dropEcs :: Edge -> Edge+_dropEcs e = Edge (edgeSymbol e) (edgeChildren e)+++-----------------------------------------------------------------+------------------------- Interning Nodes -----------------------+-----------------------------------------------------------------++data UninternedNode =+ UninternedNode ![Edge]+ | UninternedEmptyNode++ -- | Recursive node+ --+ -- The function should be parametric in the Id:+ --+ -- > substFree i (Rec j) (f i) == f j+ --+ -- See 'shape' for additional discussion.+ | UninternedMu !(RecNodeId -> Node)++instance Eq UninternedNode where+ UninternedNode es == UninternedNode es' = es == es'+ UninternedEmptyNode == UninternedEmptyNode = True+ UninternedMu mu == UninternedMu mu' = shape mu == shape mu'+ _ == _ = False++instance Hashable UninternedNode where+ hashWithSalt salt = go+ where+ go :: UninternedNode -> Int+ go UninternedEmptyNode = hashWithSalt salt (0 :: Int, ())+ go (UninternedNode es) = hashWithSalt salt (1 :: Int, es)+ go (UninternedMu mu) = hashWithSalt salt (2 :: Int, shape mu)++instance Interned Node where+ type Uninterned Node = UninternedNode+ data Description Node = DNode !UninternedNode+ deriving ( Eq, Generic )++ describe = DNode++ identify i (UninternedNode es) = InternedNode $ MkInternedNode {+ internedNodeId = i+ , internedNodeEdges = es+ , internedNodeNumNestedMu = maximum (0 : concatMap (map numNestedMu . edgeChildren) es) -- depth is always >= 0+ , internedNodeFree = Set.unions (concatMap (map freeVars . edgeChildren) es)+ }+ identify _ UninternedEmptyNode = EmptyNode+ identify i (UninternedMu n) = InternedMu $ MkInternedMu {+ internedMuId = i+ , internedMuBody = n (RecInt i)++ -- In order to establish the invariant for internedMuNoId, we need to know+ --+ -- > substFree internedMuId (Rec (RecUnint (numNestedMu internedMuBody)) internedMuBody+ -- > == internedMuShape+ --+ -- This follows from parametricity:+ --+ -- > internedMuShape+ -- > -- { definition of internedMuShape }+ -- > == shape n+ -- > -- { definition of shape }+ -- > == n (RecUnint (numNestedMu (n RecDepth)))+ -- > -- { by parametricity, depth is independent of the variable number }+ -- > == n (RecUnint (numNestedMu (n (RecInt i))))+ -- > -- { parametricity again }+ -- > == substFree i (Rec (RecUnint (numNestedMu (n (RecInt i)))) (n (RecInt i))+ -- > -- { definition of internedMuId and internedMuBody }+ -- > == substFree internedMuId (Rec (RecUnint (numNestedMu internedMuBody))) internedMuBody+ --+ -- QED.+ , internedMuShape = shape n+ }++ cache = nodeCache++instance Hashable (Description Node)++nodeCache :: Cache Node+nodeCache = unsafePerformIO freshCache+{-# NOINLINE nodeCache #-}++-- | Compute the " shape " of the body of a 'Mu'+--+-- During interning we need to know the shape of the body of a 'Mu' node /before/ we know the 'Id' of that node. We do+-- this by replacing any 'Rec' nodes in the node by placeholders. We have to be careful here however to correctly assign+-- placeholders in the presence of nested 'Mu' nodes. For example, if the user writes a term such as+--+-- > -- f (f (f ... (g (g (g ... a)))))+-- > Mu $ \r -> Node [+-- > Edge "f" [r]+-- > , Edge "g" [ Mu $ \r' -> Node [+-- > Edge "g" [r']+-- > , Edge "a" []+-- > ]+-- > ]+-- > ]+--+-- we should be careful not to accidentially identify @r@ and @r'@.+--+-- Precondition: the function must be parametric in the choice of variable names:+--+-- > substFree i (Rec j) (f i) == f j+--+-- Put another way, we must rule out /exotic terms/: in our case, exotic terms would be uninterned @Mu@ nodes that+-- have one shape when given one variable, and another shape when given a different variable. We do not have such terms.+-- (Of course, a function such as substitution /does/ do one thing if it sees one variable and another thing when it+-- sees a different variable, but this is okay: substitution is a function /on/ terms, mapping non-exotic terms to+-- non-exotic terms.)+--+-- Implementation note: We are calling the function twice: once to compute the depth of the node, and then a second time+-- to give it the right placeholder variable. Some observations:+--+-- o Semantically, this is okay; if we were working with a first order representation, it would be the equivalent of+-- first executing some kind of function @Node -> Int@, followed by some kind of substitution @Node -> Node@. It's the+-- same with the higher order representation, except that in /principle/ the function could do entirely different+-- things when given 'RecDepth' versus some other kind of placeholder; the parametricity precondition rules this out.+-- o It's slightly inefficient, but since this lives at the user interface boundary only, performance here is not+-- critical: internally we work with interned nodes only, and this function is not relevant.+-- o It /is/ important that the placeholder we pick here is uniquely determined by the node itself: this is what+-- justifies using 'shape' during interning.+shape :: (RecNodeId -> Node) -> Node+shape f = f (RecUnint (numNestedMu (f RecDepth)))++-----------------------------------------------------------------+------------------------ Interning Edges ------------------------+-----------------------------------------------------------------++data UninternedEdge = UninternedEdge { uEdgeSymbol :: !Symbol+ , uEdgeChildren :: ![Node]+ , uEdgeEcs :: !EqConstraints+ }+ deriving ( Eq, Show, Generic )++instance Hashable UninternedEdge++instance Interned Edge where+ type Uninterned Edge = UninternedEdge+ data Description Edge = DEdge {-# UNPACK #-} !UninternedEdge+ deriving ( Eq, Generic )++ describe = DEdge++ identify i e = InternedEdge i e++ cache = edgeCache++instance Hashable (Description Edge)++edgeCache :: Cache Edge+edgeCache = unsafePerformIO freshCache+{-# NOINLINE edgeCache #-}++-----------------------------------------------------------------+----------------------- Smart constructors ----------------------+-----------------------------------------------------------------++-------------------+------ Edge constructors+-------------------++pattern Edge :: Symbol -> [Node] -> Edge+pattern Edge s ns <- (InternedEdge _ (UninternedEdge s ns _)) where+ Edge s ns = intern $ UninternedEdge s ns EmptyConstraints++{-# COMPLETE Edge #-}++emptyEdge :: Edge+emptyEdge = Edge "" [EmptyNode]++isEmptyEdge :: Edge -> Bool+isEmptyEdge (Edge _ ns) = any (== EmptyNode) ns++removeEmptyEdges :: [Edge] -> [Edge]+removeEmptyEdges = filter (not . isEmptyEdge)++mkEdge :: Symbol -> [Node] -> EqConstraints -> Edge+mkEdge _ _ ecs+ | constraintsAreContradictory ecs = emptyEdge+mkEdge s ns ecs+ | otherwise = intern $ UninternedEdge s ns ecs+++-------------------+------ Node constructors+-------------------++{-# COMPLETE Node, EmptyNode, Mu, Rec #-}++pattern Node :: [Edge] -> Node+pattern Node es <- (InternedNode (internedNodeEdges -> es)) where+ Node = mkNode++mkNode :: [Edge] -> Node+mkNode es = case removeEmptyEdges es of+ [] -> EmptyNode+ es' -> intern $ UninternedNode $ nubSort es'++_mkNodeAlreadyNubbed :: [Edge] -> Node+_mkNodeAlreadyNubbed es = case removeEmptyEdges es of+ [] -> EmptyNode+ es' -> intern $ UninternedNode $ sort es'++-- | An optimized Node constructor that avoids the interning/preprocessing of the Node constructor+-- when nothing changes+modifyNode :: Node -> ([Edge] -> [Edge]) -> Node+modifyNode n@(Node es) f = let es' = f es in+ if es' == es then+ n+ else+ Node es'+modifyNode n _ = error $ "modifyNode: unexpected node " <> show n++_collapseEmptyEdge :: Edge -> Maybe Edge+_collapseEmptyEdge e@(Edge _ ns) = if any (== EmptyNode) ns then Nothing else Just e++------ Mu++-- | Pattern only a Mu constructor+--+-- When we go underneath a Mu constructor, we need to bind the corresponding Rec node to something: that's why pattern+-- matching on 'Mu' yields a function. Code that wants to traverse the term as-is should match on the interned+-- constructors instead (and then deal with the dangling references).+--+-- An identity function+--+-- > foo (Mu f) = Mu f+--+-- will run in O(1) time:+--+-- > foo (Mu f) = Mu f+-- > -- { expand view patern }+-- > foo node | Just f <- matchMu node = createMu f+-- > -- { case for @InternedMu mu@ }+-- > foo (InternedMu mu) | Just f <- matchMu (InternedMu m) = createMu f+-- > -- { definition of matchMu }+-- > foo (InternedMu mu) = let f = \n' ->+-- > if | n' == Rec (RecUnint (numNestedMu (internedMuBody mu))) ->+-- > internedMuShape mu+-- > | n' == Rec RecDepth ->+-- > internedMuShape mu+-- > | otherwise ->+-- > substFree (internedMuId mu) n' (internedMuBody mu)+-- > in createMu f+-- > -- { definition of createMu }+-- > foo (InternedMu mu) = intern $ UninternedMu (f . Rec)+--+-- At this point, `intern` will call `shape (f . Rec)`, which will call `f . Rec` twice: once with `RecDepth` to compute+-- the depth, and then once again with that depth to substitute a placeholder. Both of these special cases will use+-- 'internedMuShape' (and moreover, the depth calculation on 'internedMuShape' is @O(1)@).+pattern Mu :: (Node -> Node) -> Node+pattern Mu f <- (matchMu -> Just f)+ where+ Mu = createMu++-- | Construct recursive node+--+-- Implementation note: 'createMu' and 'matchMu' interact in non-trivial ways; see docs of the 'Mu' pattern synonym+-- for performance considerations.+createMu :: (Node -> Node) -> Node+createMu f = intern $ UninternedMu (f . Rec)++-- | Match on a 'Mu' node+--+-- Implementation note: 'createMu' and 'matchMu' interact in non-trivial ways; see docs of the 'Mu' pattern synonym+-- for performance considerations.+matchMu :: Node -> Maybe (Node -> Node)+matchMu (InternedMu mu) = Just $ \n' ->+ if | n' == Rec (RecUnint (numNestedMu (internedMuBody mu))) ->+ -- Special case justified by the invariant on 'internedMuShape'+ internedMuShape mu+ | n' == Rec RecDepth ->+ -- The use of 'RecDepth' implies that we are computing a depth:+ --+ -- > numNestedMu (substFree (internedMuId mu) (Rec RecDepth)) (internedMuBody mu))+ -- > -- { depth calculation does not depend on choice of variable }+ -- > == numNestedMu (substFree (internedMuId mu) Rec (RecUnint (numNestedMu (internedMuBody mu)))) (internedMuBody mu))+ -- > -- { invariant of internedMuShape }+ -- > == numNestedMu internedMuShape+ internedMuShape mu+ | otherwise ->+ substFree (RecInt (internedMuId mu)) n' (internedMuBody mu)++matchMu _otherwise = Nothing++-- | Substitution+--+-- @substFree i n@ will replace all occurrences of @Rec (RecNodeId i)@ by @n@. We appeal to the uniqueness of node IDs+-- and assume that all occurrences of @i@ must be free (in other words, that any occurrences of 'Mu' will have a+-- /different/ identifier.+--+-- Postcondition:+--+-- > substFree i (Rec (RecNodeId i)) == id+substFree :: RecNodeId -> Node -> Node -> Node+substFree old new = substFree' (Map.singleton old new)++-- | Generalization of 'substFree' to multiple binders.+substFree' :: Map RecNodeId Node -> Node -> Node+substFree' env node = case template node of+ Template f -> f env++------ Substitution internals++-- | The template of a something is that something with holes for as-yet unknown 'Id's+--+-- This datatype should satisfy two properties for 'template' to work correctly:+--+-- 1. Forcing the 'Template' to WHNF should not result in any recursive calls+-- (so that the recursion isn't totally unrolled before memoization can happen).+-- 2. But forcing the /function inside/ the 'Template' to WHNF /should/ result in all recursive calls to happen,+-- (/before/ the function is executed: executing the function should /not/ cause further calls to 'template').+--+-- The idea here is that a function returning a 'Template', the application of that 'Template' should not result in+-- further recursive calls to that function, so that any expensive computation done by that function is not repeated,+-- but is done independently of the environment (the 'Map') that we provide to the 'Template'. Put another way: the+-- function can be memoized independently of that environment. For substitution this may not matter very much, but for+-- other functions it could. Note however that the resulting 'Template' does build the graph on each invocation; this+-- may still be prohibitively expensive. See 'intersect' for an example of how we can avoid an environment altogether.+-- (This is not an option for substitution of course, where the environment is part of the API of the function.)+data Template a = Template (Map RecNodeId Node -> a)++-- | Commute @[]@ and 'Template'+--+-- Forces all elements in the list+sequenceTemplate :: [Template a] -> Template [a]+sequenceTemplate = Template . go []+ where+ go :: [Map RecNodeId Node -> a] -> [Template a] -> Map RecNodeId Node -> [a]+ go acc [] = \env -> reverse (map ($ env) acc)+ go acc (Template !f:fs) = go (f:acc) fs++-- | Extract the shape from a term+--+-- Somewhat serendipitously (or does this point to some deeper truth?) this also serves as a definition of substitution:+-- any free variables in the original node will become " holes " in the 'Template'.+--+-- We do not use the pattern synonyms here, because 'template' is used (through 'substFree') to /define/ those+-- pattern synonyms.+template :: Node -> Template Node+{-# NOINLINE template #-}+template = memo (NameTag "template") onNode+ where+ onNode :: Node -> Template Node+ onNode n = Template $+ case n of+ EmptyNode -> \_ -> EmptyNode+ InternedNode node -> case sequenceTemplate $ map templateEdge (internedNodeEdges node) of+ Template !f -> \env -> mkNode (f env)+ InternedMu mu -> case onNode (internedMuBody mu) of+ Template !f -> \env -> createMu $ \r -> f (Map.insert (RecInt (internedMuId mu)) r env)+ Rec i -> \env -> fromMaybe n (Map.lookup i env)++-- | Internal auxiliary to 'template'+templateEdge :: Edge -> Template Edge+{-# NOINLINE templateEdge #-}+templateEdge = memo (NameTag "templateEdge") onEdge+ where+ onEdge :: Edge -> Template Edge+ onEdge e =+ Template $ case sequenceTemplate (map template (edgeChildren e)) of+ Template !f -> setChildren e . f
+ src/Data/ECTA/Internal/ECTA/Visualization.hs view
@@ -0,0 +1,194 @@+{-# LANGUAGE OverloadedStrings #-}++module Data.ECTA.Internal.ECTA.Visualization (+ toDot+ ) where++import qualified Data.Text as Text++import qualified Data.Graph.Inductive as Fgl+import Data.List.Index ( imap )+import qualified Language.Dot.Syntax as Dot+++import Data.ECTA.Internal.ECTA.Operations ( maxIndegree, crush )+import Data.ECTA.Internal.ECTA.Type+import Data.ECTA.Internal.Paths ( EqConstraints )+import Data.ECTA.Internal.Term+import Data.Interned.Extended.HashTableBased ( Id )+import Data.Text.Extended.Pretty++---------------------------------------------------------------+----------------------- Visualization -------------------------+---------------------------------------------------------------++-----------------------+------ Partial graph+-----------------------++-- | We identify an edge by its /source/ node 'Id' and the index of the edge+type EdgeId = (Id, Int)++-- | Partial graph+--+-- This is used as an intermediate stage in rendering the graph: we 'crush' the graph, constructing a 'PartialGraph' at+-- every node in the graph, 'mappend' them all together and then construct an @fgl@ graph from that (which we then+-- export to @dotty@ format). This first step is independent from any @fgl@ or @dotty@ specific decisions.+data PartialGraph = PartialGraph {+ -- | IDs of all regular nodes in the graph+ partialNormal :: [Id]++ -- | IDs of all Mu nodes in the graph, along with the ID of their child+ --+ -- For now we explicitly assume that Mu nodes must have a regular node as a child node, and error out otherwise;+ -- see 'partialFromEdge' for motivation.+ , partialMu :: [(Id, Id)]++ -- | Edge nodes+ , partialEdges :: [(EdgeId, Symbol, EqConstraints)]++ -- | Transitions from nodes to edges+ --+ -- The 'Int' here is the index of the edge (i.e., the @i@th edge)+ --+ -- Invariant: The node 'Id' will be the Id of a /normal/ (non-Mu) node+ , partialFromNode :: [(Id, EdgeId)]++ -- | Transitions from edges to nodes+ --+ -- As for 'partialFromNode', the 'Int' is the index of the edge, but the node 'Id' here /might/ refer to a 'Mu'.+ -- This means that when rendering these edges, 'partialMu' should be taken into account: edges to Mu nodes should+ -- instead be rendered as edges to their regular 'Node' child (this motivates the assumption on 'partialMu').+ , partialFromEdge :: [(EdgeId, Id)]+ }+ deriving (Show)++instance Semigroup PartialGraph where+ a <> b = PartialGraph {+ partialNormal = combine partialNormal+ , partialMu = combine partialMu+ , partialEdges = combine partialEdges+ , partialFromNode = combine partialFromNode+ , partialFromEdge = combine partialFromEdge+ }+ where+ combine :: Semigroup a => (PartialGraph -> a) -> a+ combine f = f a <> f b++instance Monoid PartialGraph where+ mempty = PartialGraph {+ partialNormal = []+ , partialMu = []+ , partialEdges = []+ , partialFromNode = []+ , partialFromEdge = []+ }++mkPartialGraph :: Node -> PartialGraph+mkPartialGraph = crush onNode+ where+ onNode :: Node -> PartialGraph+ onNode EmptyNode = error "mkPartialGraph: impossible (crush does not invoke function on EmptyNode)"+ onNode (InternedNode node) = let (edgeNodes, fr, to) = unzip3 $ imap (onEdge nid) es in+ mempty {+ partialNormal = [nid]+ , partialEdges = edgeNodes+ , partialFromNode = fr+ , partialFromEdge = concat to+ }+ where+ nid = internedNodeId node+ es = internedNodeEdges node+ onNode (InternedMu mu) = case internedMuBody mu of+ InternedNode node -> mempty {+ partialMu = [(internedMuId mu, internedNodeId node)]+ }+ _otherwise -> error "mkPartialGraph: expected Node as a child of a Mu"+ onNode (Rec _) = mempty++ onEdge :: Id -- Id of the " from " node+ -> Int -- Index of the edge+ -> Edge -- The edge itself+ -> ( (EdgeId, Symbol, EqConstraints) -- The edge node+ , (Id, EdgeId) -- The " from " transition+ , [(EdgeId, Id)] -- The " to " transitions+ )+ onEdge nid i e = (+ (eid, edgeSymbol e, edgeEcs e)+ , (nid, eid)+ , map (\n -> (eid, nodeIdentity n)) $ edgeChildren e+ )+ where+ eid = (nid, i)++-----------------------+------ FGL graph construction+-----------------------++data FglNodeLabel = IdLabel Id | TransitionLabel Symbol EqConstraints+ deriving ( Eq, Ord, Show )++partialToFgl :: Int -> PartialGraph -> Fgl.Gr FglNodeLabel ()+partialToFgl maxNodeIndegree p =+ Fgl.mkGraph (nodeNodes ++ transitionNodes) (nodeToTransitionEdges ++ transitionToNodeEdges)+ where+ nodeNodes, transitionNodes :: [Fgl.LNode FglNodeLabel]+ nodeNodes = map (\ i -> (fglNodeId i, IdLabel $ i)) $ partialNormal p+ transitionNodes = map (\(i, s, cs) -> (fglEdgeId i, TransitionLabel s cs)) $ partialEdges p++ nodeToTransitionEdges, transitionToNodeEdges :: [Fgl.LEdge ()]+ nodeToTransitionEdges = map (\(nid, eid) -> (fglNodeId nid, fglEdgeId eid, ())) $ partialFromNode p+ transitionToNodeEdges = map (\(eid, nid) -> (fglEdgeId eid, fglNodeId' nid, ())) $ partialFromEdge p++ fglNodeId :: Id -> Fgl.Node+ fglNodeId nid = nid * (maxNodeIndegree + 1)++ -- " To " edges might transition to Mu nodes, in which case we want to an edge to their child node instead+ fglNodeId' :: Id -> Fgl.Node+ fglNodeId' nid = maybe (fglNodeId nid) fglNodeId (lookup nid $ partialMu p)++ fglEdgeId :: EdgeId -> Fgl.Node+ fglEdgeId (nid, i) = nid * (maxNodeIndegree + 1) + (i + 1)++toFgl :: Node -> Fgl.Gr FglNodeLabel ()+toFgl root = partialToFgl (maxIndegree root) (mkPartialGraph root)++-----------------------+------ Translate to dotty+-----------------------++fglToDot :: Fgl.Gr FglNodeLabel () -> Dot.Graph+fglToDot g = Dot.Graph Dot.StrictGraph Dot.DirectedGraph Nothing (nodeStmts ++ edgeStmts)+ where+ nodeStmts :: [Dot.Statement]+ nodeStmts = map renderNode $ Fgl.labNodes g++ edgeStmts :: [Dot.Statement]+ edgeStmts = map renderEdge $ Fgl.labEdges g++ renderNode :: Fgl.LNode FglNodeLabel -> Dot.Statement+ renderNode (fglId, l) = Dot.NodeStatement (Dot.NodeId (Dot.IntegerId $ toInteger fglId) Nothing)+ [ Dot.AttributeSetValue (Dot.NameId "label") (renderNodeLabel l)+ , Dot.AttributeSetValue (Dot.NameId "shape")+ (case l of+ IdLabel _ -> Dot.StringId "ellipse"+ TransitionLabel _ _ -> Dot.StringId "box")+ ]++ renderEdge :: Fgl.LEdge () -> Dot.Statement+ renderEdge (a, b, _) = Dot.EdgeStatement [ea, eb] []+ where+ ea = Dot.ENodeId Dot.NoEdge (Dot.NodeId (Dot.IntegerId $ toInteger a) Nothing)+ eb = Dot.ENodeId Dot.DirectedEdge (Dot.NodeId (Dot.IntegerId $ toInteger b) Nothing)++ renderNodeLabel :: FglNodeLabel -> Dot.Id+ renderNodeLabel (IdLabel l) = Dot.StringId ("q" ++ show l)+ renderNodeLabel (TransitionLabel s ecs) =+ Dot.StringId (Text.unpack $ pretty s <> " (" <> pretty ecs <> ")")++-- | To visualize an FTA:+-- 1) Call `prettyPrintDot $ toDot fta` from GHCI+-- 2) Copy the output to viz-js.jom or another GraphViz implementation+toDot :: Node -> Dot.Graph+toDot = fglToDot . toFgl+
+ src/Data/ECTA/Internal/Paths.hs view
@@ -0,0 +1,465 @@+{-# LANGUAGE OverloadedStrings #-}++-- | Representations of paths in an FTA, data structures for+-- equality constraints over paths, algorithms for saturating these constraints++module Data.ECTA.Internal.Paths (+ Path(.., EmptyPath, ConsPath)+ , unPath+ , path+ , Pathable(..)+ , pathHeadUnsafe+ , pathTailUnsafe+ , isSubpath+ , isStrictSubpath+ , substSubpath++ , smallestNonempty+ , largestNonempty+ , getMaxNonemptyIndex++ , PathTrie(..)+ , isEmptyPathTrie+ , isTerminalPathTrie+ , toPathTrie+ , fromPathTrie+ , pathTrieDescend++ , PathEClass(PathEClass, ..)+ , unPathEClass+ , hasSubsumingMember+ , completedSubsumptionOrdering++ , EqConstraints(.., EmptyConstraints)+ , rawMkEqConstraints+ , unsafeGetEclasses+ , hasSubsumingMemberListBased+ , isContradicting+ , mkEqConstraints+ , combineEqConstraints+ , eqConstraintsDescend+ , constraintsAreContradictory+ , constraintsImply+ , subsumptionOrderedEclasses+ , unsafeSubsumptionOrderedEclasses+ ) where++import Prelude hiding ( round )++import Data.Function ( on )+import Data.Hashable ( Hashable )+import Data.List ( isSubsequenceOf, nub, sort, sortBy )+import Data.Monoid ( Any(..) )+import Data.Semigroup ( Max(..) )+import qualified Data.Text as Text+import Data.Vector ( Vector )+import qualified Data.Vector as Vector+import Data.Vector.Instances ()+import GHC.Exts ( inline )+import GHC.Generics ( Generic )++import Data.Equivalence.Monad ( runEquivM, equate, desc, classes )++import Data.Memoization ( MemoCacheTag(..), memo2 )+import Data.Text.Extended.Pretty+import Utility.Fixpoint++-------------------------------------------------------+++-----------------------------------------------------------------------+--------------------------- Misc / general ----------------------------+-----------------------------------------------------------------------++flipOrdering :: Ordering -> Ordering+flipOrdering GT = LT+flipOrdering LT = GT+flipOrdering EQ = EQ++-----------------------------------------------------------------------+-------------------------------- Paths --------------------------------+-----------------------------------------------------------------------++data Path = Path ![Int]+ deriving (Eq, Ord, Show, Generic)++unPath :: Path -> [Int]+unPath (Path p) = p++instance Hashable Path++path :: [Int] -> Path+path = Path++{-# COMPLETE EmptyPath, ConsPath #-}++pattern EmptyPath :: Path+pattern EmptyPath = Path []++pattern ConsPath :: Int -> Path -> Path+pattern ConsPath p ps <- Path (p : (Path -> ps)) where+ ConsPath p (Path ps) = Path (p : ps)++pathHeadUnsafe :: Path -> Int+pathHeadUnsafe (Path ps) = head ps++pathTailUnsafe :: Path -> Path+pathTailUnsafe (Path ps) = Path (tail ps)++instance Pretty Path where+ pretty (Path ps) = Text.intercalate "." (map (Text.pack . show) ps)++isSubpath :: Path -> Path -> Bool+isSubpath EmptyPath _ = True+isSubpath (ConsPath p1 ps1) (ConsPath p2 ps2)+ | p1 == p2 = isSubpath ps1 ps2+isSubpath _ _ = False++isStrictSubpath :: Path -> Path -> Bool+isStrictSubpath EmptyPath EmptyPath = False+isStrictSubpath EmptyPath _ = True+isStrictSubpath (ConsPath p1 ps1) (ConsPath p2 ps2)+ | p1 == p2 = isStrictSubpath ps1 ps2+isStrictSubpath _ _ = False+++-- | Read `substSubpath p1 p2 p3` as `[p1/p2]p3`+--+-- `substSubpath replacement toReplace target` takes `toReplace`, a prefix of target,+-- and returns a new path in which `toReplace` has been replaced by `replacement`.+--+-- Undefined if toReplace is not a prefix of target+substSubpath :: Path -> Path -> Path -> Path+substSubpath replacement toReplace target = Path $ (unPath replacement) ++ drop (length $ unPath toReplace) (unPath target)+++--------------------------------------------------------------------------+---------------------------- Using paths ---------------------------------+--------------------------------------------------------------------------++-- | TODO: Should this be redone as a lens-library traversal?+-- | TODO: I am unhappy about this Emptyable design; makes one question whether+-- this should be a typeclass at all. (Terms/ECTAs differ in that+-- there is always an ECTA Node that represents the value at a path)+class Pathable t t' | t -> t' where+ type Emptyable t'+ getPath :: Path -> t -> Emptyable t'+ getAllAtPath :: Path -> t -> [t']+ modifyAtPath :: (t' -> t') -> Path -> t -> t+++-----------------------------------------------------------------------+---------------------------- Path tries -------------------------------+-----------------------------------------------------------------------++---------------------+------- Generic-ish utility functions+---------------------++-- | Precondition: A nonempty cell exists+smallestNonempty :: Vector PathTrie -> Int+smallestNonempty v = Vector.ifoldr (\i pt oldMin -> case pt of+ EmptyPathTrie -> oldMin+ _ -> i)+ maxBound+ v+++-- | Precondition: A nonempty cell exists+largestNonempty :: Vector PathTrie -> Int+largestNonempty v = Vector.ifoldl (\oldMin i pt -> case pt of+ EmptyPathTrie -> oldMin+ _ -> i)+ minBound+ v++getMaxNonemptyIndex :: PathTrie -> Maybe Int+getMaxNonemptyIndex EmptyPathTrie = Nothing+getMaxNonemptyIndex TerminalPathTrie = Nothing+getMaxNonemptyIndex (PathTrieSingleChild i _) = Just i+getMaxNonemptyIndex (PathTrie vec) = Just $ largestNonempty vec++---------------------+------- Path tries+---------------------++data PathTrie = EmptyPathTrie+ | TerminalPathTrie+ | PathTrieSingleChild {-# UNPACK #-} !Int !PathTrie+ | PathTrie !(Vector PathTrie) -- Invariant: Must have at least two nonempty nodes+ deriving ( Eq, Show, Generic )++instance Hashable PathTrie++isEmptyPathTrie :: PathTrie -> Bool+isEmptyPathTrie EmptyPathTrie = True+isEmptyPathTrie _ = False++isTerminalPathTrie :: PathTrie -> Bool+isTerminalPathTrie TerminalPathTrie = True+isTerminalPathTrie _ = False++comparePathTrieVectors :: Vector PathTrie -> Vector PathTrie -> Ordering+comparePathTrieVectors v1 v2 = foldr (\i res -> let (t1, t2) = (v1 `Vector.unsafeIndex` i, v2 `Vector.unsafeIndex` i)+ in case (isEmptyPathTrie t1, isEmptyPathTrie t2) of+ (False, True) -> LT+ (True, False) -> GT+ (True, True) -> res+ (False, False) -> case compare t1 t2 of+ LT -> LT+ GT -> GT+ EQ -> res)+ valueIfComponentsMatch+ [0..(min (Vector.length v1) (Vector.length v2) - 1)]+ where+ valueIfComponentsMatch = compare (Vector.length v1) (Vector.length v2)++instance Ord PathTrie where+ compare EmptyPathTrie EmptyPathTrie = EQ+ compare EmptyPathTrie _ = LT+ compare _ EmptyPathTrie = GT+ compare TerminalPathTrie TerminalPathTrie = EQ+ compare TerminalPathTrie _ = LT+ compare _ TerminalPathTrie = GT+ compare (PathTrieSingleChild i1 pt1) (PathTrieSingleChild i2 pt2)+ | i1 < i2 = LT+ | i1 > i2 = GT+ | otherwise = compare pt1 pt2+ compare (PathTrieSingleChild i1 pt1) (PathTrie v2) = let i2 = smallestNonempty v2 in+ case compare i1 i2 of+ LT -> LT+ GT -> GT+ EQ -> case compare pt1 (v2 `Vector.unsafeIndex` i2) of+ LT -> LT+ GT -> GT+ EQ -> LT -- v2 must have a second nonempty+ compare a@(PathTrie _) b@(PathTrieSingleChild _ _) = flipOrdering $ inline compare b a -- TODO: Check whether this inlining is effective+ compare (PathTrie v1) (PathTrie v2) = comparePathTrieVectors v1 v2+++-- | Precondition: No path in the input is a subpath of another+toPathTrie :: [Path] -> PathTrie+toPathTrie [] = EmptyPathTrie+toPathTrie [EmptyPath] = TerminalPathTrie+toPathTrie ps = if all (\p -> pathHeadUnsafe p == pathHeadUnsafe (head ps)) ps then+ PathTrieSingleChild (pathHeadUnsafe $ head ps) (toPathTrie $ map pathTailUnsafe ps)+ else+ PathTrie vec+ where+ maxIndex = getMax $ foldMap (Max . pathHeadUnsafe) ps++ -- TODO: Inefficient to use this; many passes. over the list.+ -- This may not be used in a place where perf matters, though+ pathsStartingWith :: Int -> [Path] -> [Path]+ pathsStartingWith i = concatMap (\case EmptyPath -> []+ ConsPath j p -> if i == j then [p] else [])++ vec = Vector.generate (maxIndex + 1) (\i -> toPathTrie $ pathsStartingWith i ps)++fromPathTrie :: PathTrie -> [Path]+fromPathTrie EmptyPathTrie = []+fromPathTrie TerminalPathTrie = [EmptyPath]+fromPathTrie (PathTrieSingleChild i pt) = map (ConsPath i) $ fromPathTrie pt+fromPathTrie (PathTrie v) = Vector.ifoldr (\i pt acc -> map (ConsPath i) (fromPathTrie pt) ++ acc) [] v++pathTrieDescend :: PathTrie -> Int -> PathTrie+pathTrieDescend EmptyPathTrie _ = EmptyPathTrie+pathTrieDescend TerminalPathTrie _ = EmptyPathTrie+pathTrieDescend (PathTrie v) i = if Vector.length v > i then+ v `Vector.unsafeIndex` i+ else+ EmptyPathTrie+pathTrieDescend (PathTrieSingleChild j pt') i+ | i == j = pt'+ | otherwise = EmptyPathTrie++--------------------------------------------------------------------------+---------------------- Equality constraints over paths -------------------+--------------------------------------------------------------------------++---------------------------+---------- Path E-classes+---------------------------++data PathEClass = PathEClass' { getPathTrie :: !PathTrie+ , getOrigPaths :: [Path] -- Intentionally lazy because+ -- not available when calling `mkPathEClassFromPathTrie`+ }+ deriving ( Show, Generic )++instance Eq PathEClass where+ (==) = (==) `on` getPathTrie++instance Ord PathEClass where+ compare = compare `on` getPathTrie++-- | TODO: This pattern (and the caching of the original path list) is a temporary affair+-- until we convert all clients of PathEclass to fully be based on tries+pattern PathEClass :: [Path] -> PathEClass+pattern PathEClass ps <- PathEClass' _ ps where+ PathEClass ps = PathEClass' (toPathTrie $ nub ps) (sort $ nub ps)++unPathEClass :: PathEClass -> [Path]+unPathEClass (PathEClass' _ paths) = paths++instance Pretty PathEClass where+ pretty pec = "{" <> (Text.intercalate "=" $ map pretty $ unPathEClass pec) <> "}"++instance Hashable PathEClass++mkPathEClassFromPathTrie :: PathTrie -> PathEClass+mkPathEClassFromPathTrie pt = PathEClass' pt (fromPathTrie pt)++pathEClassDescend :: PathEClass -> Int -> PathEClass+pathEClassDescend (PathEClass' pt _) i = mkPathEClassFromPathTrie $ pathTrieDescend pt i++hasSubsumingMember :: PathEClass -> PathEClass -> Bool+hasSubsumingMember pec1 pec2 = go (getPathTrie pec1) (getPathTrie pec2)+ where+ go :: PathTrie -> PathTrie -> Bool+ go EmptyPathTrie _ = False+ go _ EmptyPathTrie = False+ go TerminalPathTrie TerminalPathTrie = False+ go TerminalPathTrie _ = True+ go _ TerminalPathTrie = False+ go (PathTrieSingleChild i1 pt1) (PathTrieSingleChild i2 pt2) = if i1 == i2 then+ go pt1 pt2+ else+ False+ go (PathTrieSingleChild i1 pt1) (PathTrie v2) = case v2 Vector.!? i1 of+ Nothing -> False+ Just pt2 -> go pt1 pt2+ go (PathTrie v1) (PathTrieSingleChild i2 pt2) = case v1 Vector.!? i2 of+ Nothing -> False+ Just pt1 -> go pt1 pt2+ go (PathTrie v1) (PathTrie v2) = any (\i -> go (v1 `Vector.unsafeIndex` i) (v2 `Vector.unsafeIndex` i))+ [0..(min (Vector.length v1) (Vector.length v2) - 1)]+++-- | Extends the subsumption ordering to a total ordering by using the default lexicographic+-- comparison for incomparable elements.+-- | TODO: Optimization opportunity: Redundant work in the hasSubsumingMember calls+completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering+completedSubsumptionOrdering pec1 pec2+ | hasSubsumingMember pec1 pec2 = LT+ | hasSubsumingMember pec2 pec1 = GT+ -- This next line is some hacky magic. Basically, it means that for the+ -- Hoogle+/TermSearch workload, where there is no subsumption,+ -- constraints will be evaluated in left-to-right order (instead of the default+ -- right-to-left), which for that particular workload produces better+ -- constraint-propagation+ | otherwise = compare pec2 pec1++--------------------------------+---------- Equality constraints+--------------------------------++data EqConstraints = EqConstraints { getEclasses :: [PathEClass] -- ^ Must be sorted+ }+ | EqContradiction+ deriving ( Eq, Ord, Show, Generic )++instance Hashable EqConstraints++instance Pretty EqConstraints where+ pretty ecs = "{" <> (Text.intercalate "," $ map pretty (getEclasses ecs)) <> "}"++--------- Destructors and patterns++-- | Unsafe. Internal use only+ecsGetPaths :: EqConstraints -> [[Path]]+ecsGetPaths = map unPathEClass . getEclasses++pattern EmptyConstraints :: EqConstraints+pattern EmptyConstraints = EqConstraints []++unsafeGetEclasses :: EqConstraints -> [PathEClass]+unsafeGetEclasses EqContradiction = error "unsafeGetEclasses: Illegal argument 'EqContradiction'"+unsafeGetEclasses ecs = getEclasses ecs++rawMkEqConstraints :: [[Path]] -> EqConstraints+rawMkEqConstraints = EqConstraints . map PathEClass+++constraintsAreContradictory :: EqConstraints -> Bool+constraintsAreContradictory = (== EqContradiction)++--------- Construction+++hasSubsumingMemberListBased :: [Path] -> [Path] -> Bool+hasSubsumingMemberListBased ps1 ps2 = getAny $ mconcat [Any (isStrictSubpath p1 p2) | p1 <- ps1+ , p2 <- ps2]++-- | The real contradiction condition is a cycle in the subsumption ordering.+-- But, after congruence closure, this will reduce into a self-cycle in the subsumption ordering.+--+-- TODO; Prove this.+isContradicting :: [[Path]] -> Bool+isContradicting cs = any (\pec -> hasSubsumingMemberListBased pec pec) cs++-- Contains an inefficient implementation of the congruence closure algorithm+mkEqConstraints :: [[Path]] -> EqConstraints+mkEqConstraints initialConstraints = case completedConstraints of+ Nothing -> EqContradiction+ Just cs -> EqConstraints $ sort $ map PathEClass cs+ where+ removeTrivial :: (Eq a) => [[a]] -> [[a]]+ removeTrivial = filter (\x -> length x > 1) . map nub++ -- Reason for the extra "complete" in this line:+ -- The first simplification done to the constraints is eclass-completion,+ -- to remove redundancy and shrink things before the very inefficienc+ -- addCongruences step (important in tests; less so in realistic input).+ -- The last simplification must also be completion, to give a valid value.+ completedConstraints = fixMaybe round $ complete $ removeTrivial initialConstraints++ round :: [[Path]] -> Maybe [[Path]]+ round cs = let cs' = addCongruences cs+ cs'' = complete cs'+ in if isContradicting cs'' then+ Nothing+ else+ Just cs''++ addCongruences :: [[Path]] -> [[Path]]+ addCongruences cs = cs ++ [map (\z -> substSubpath z x y) left | left <- cs, right <- cs, x <- left, y <- right, isStrictSubpath x y]++ assertEquivs xs = mapM (\y -> equate (head xs) y) (tail xs)++ complete :: (Ord a) => [[a]] -> [[a]]+ complete initialClasses = runEquivM (:[]) (++) $ do+ mapM_ assertEquivs initialClasses+ mapM desc =<< classes++---------- Operations++combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints+combineEqConstraints = memo2 (NameTag "combineEqConstraints") go+ where+ go EqContradiction _ = EqContradiction+ go _ EqContradiction = EqContradiction+ go ec1 ec2 = mkEqConstraints $ ecsGetPaths ec1 ++ ecsGetPaths ec2+{-# NOINLINE combineEqConstraints #-}++eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints+eqConstraintsDescend EqContradiction _ = EqContradiction+eqConstraintsDescend ecs i = EqConstraints $ sort $ map (`pathEClassDescend` i) (getEclasses ecs)++-- A faster implementation would be: Merge the eclasses of both, run mkEqConstraints (or at least do eclass completion),+-- check result equal to ecs2+constraintsImply :: EqConstraints -> EqConstraints -> Bool+constraintsImply EqContradiction _ = True+constraintsImply _ EqContradiction = False+constraintsImply ecs1 ecs2 = all (\cs -> any (isSubsequenceOf cs) (ecsGetPaths ecs1)) (ecsGetPaths ecs2)++++subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass]+subsumptionOrderedEclasses ecs = case ecs of+ EqContradiction -> Nothing+ EqConstraints pecs -> Just $ sortBy completedSubsumptionOrdering pecs++unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass]+unsafeSubsumptionOrderedEclasses (EqConstraints pecs) = sortBy completedSubsumptionOrdering pecs+unsafeSubsumptionOrderedEclasses EqContradiction = error $ "unsafeSubsumptionOrderedEclasses: unexpected EqContradiction"
+ src/Data/ECTA/Internal/Paths/Zipper.hs view
@@ -0,0 +1,118 @@+-- | These were used in an earlier version of the enumeration algorithm, but no longer.+--+-- They are being kept around just in case.+++module Data.ECTA.Internal.Paths.Zipper (+ unionPathTrie++ , InvertedPathTrie(..)++ , PathTrieZipper(..)+ , emptyPathTrieZipper+ , pathTrieToZipper+ , zipperCurPathTrie+ , pathTrieZipperDescend+ , pathTrieZipperAscend+ , unionPathTrieZipper+ ) where++import qualified Data.Vector as Vector+import qualified Data.Vector.Mutable as Vector ( unsafeWrite )++import GHC.Exts ( inline )++import Data.ECTA.Internal.Paths++-----------------------------------------------------------------------++---------------------+------- Path trie union+------- (7/9/21: only used as utility for unionPathTrieZipper)+---------------------++unionPathTrie :: PathTrie -> PathTrie -> Maybe PathTrie+unionPathTrie EmptyPathTrie pt = Just pt+unionPathTrie pt EmptyPathTrie = Just pt+unionPathTrie TerminalPathTrie TerminalPathTrie = Just TerminalPathTrie+unionPathTrie TerminalPathTrie _ = Nothing+unionPathTrie _ TerminalPathTrie = Nothing+unionPathTrie (PathTrieSingleChild i1 pt1) (PathTrieSingleChild i2 pt2) =+ if i1 == i2 then+ PathTrieSingleChild i1 <$> unionPathTrie pt1 pt2+ else+ Just $ PathTrie $ Vector.generate (1 + max i1 i2) $ \j -> if j == i1 then+ pt1+ else if j == i2 then+ pt2+ else+ EmptyPathTrie+unionPathTrie (PathTrieSingleChild i pt) (PathTrie vec) =+ if Vector.length vec > i then+ do updated <- unionPathTrie pt (vec `Vector.unsafeIndex` i)+ Just $ PathTrie $ Vector.modify (\v -> Vector.unsafeWrite v i updated) vec+ else+ Just $ PathTrie $ Vector.generate (i+1) $ \j -> if j < Vector.length vec then+ vec `Vector.unsafeIndex` j+ else if j == i then+ pt+ else+ EmptyPathTrie+++unionPathTrie pt1@(PathTrie _) pt2@(PathTrieSingleChild _ _) = inline unionPathTrie pt2 pt1 -- TODO: Check whether this inlining is effective+unionPathTrie (PathTrie vec1) (PathTrie vec2) =+ let newLength = max (Vector.length vec1) (Vector.length vec2)+ smallerLength = min (Vector.length vec1) (Vector.length vec2)+ bigVec = if Vector.length vec1 > Vector.length vec2 then vec1 else vec2+ smallVec = if Vector.length vec1 > Vector.length vec2 then vec2 else vec1+ in fmap PathTrie $ Vector.generateM newLength $ \i -> if i >= smallerLength then+ return (bigVec `Vector.unsafeIndex` i)+ else+ unionPathTrie (bigVec `Vector.unsafeIndex` i) (smallVec `Vector.unsafeIndex` i)++++---------------------+------- Zippers+---------------------++data InvertedPathTrie = PathZipperRoot+ | PathTrieAt {-# UNPACK #-} !Int !PathTrie !InvertedPathTrie+ deriving ( Eq, Ord, Show )++data PathTrieZipper = PathTrieZipper !PathTrie !InvertedPathTrie+ deriving ( Eq, Ord, Show )++emptyPathTrieZipper :: PathTrieZipper+emptyPathTrieZipper = PathTrieZipper EmptyPathTrie PathZipperRoot++pathTrieToZipper :: PathTrie -> PathTrieZipper+pathTrieToZipper pt = PathTrieZipper pt PathZipperRoot++zipperCurPathTrie :: PathTrieZipper -> PathTrie+zipperCurPathTrie (PathTrieZipper pt _) = pt++unionInvertedPathTrie :: InvertedPathTrie -> InvertedPathTrie -> Maybe InvertedPathTrie+unionInvertedPathTrie PathZipperRoot ipt = Just ipt+unionInvertedPathTrie ipt PathZipperRoot = Just ipt+unionInvertedPathTrie (PathTrieAt i1 pt1 ipt1) (PathTrieAt i2 pt2 ipt2) =+ if i1 /= i2 then+ Nothing+ else+ PathTrieAt i1 <$> unionPathTrie pt1 pt2 <*> unionInvertedPathTrie ipt1 ipt2+++unionPathTrieZipper :: PathTrieZipper -> PathTrieZipper -> Maybe PathTrieZipper+unionPathTrieZipper (PathTrieZipper pt1 ipt1) (PathTrieZipper pt2 ipt2) =+ PathTrieZipper <$> unionPathTrie pt1 pt2 <*> unionInvertedPathTrie ipt1 ipt2++pathTrieZipperDescend :: PathTrieZipper -> Int -> PathTrieZipper+pathTrieZipperDescend (PathTrieZipper pt z) i = PathTrieZipper (pathTrieDescend pt i) (PathTrieAt i pt z)++-- | The semantics of this may not be what you expect: Path trie zippers do not support editing currently, only traversing.+-- The value at the cursor (as well as the index) is ignored except when traversing above the root, where it uses those+-- values to extend the path trie upwards.+pathTrieZipperAscend :: PathTrieZipper -> Int -> PathTrieZipper+pathTrieZipperAscend (PathTrieZipper pt PathZipperRoot) i = PathTrieZipper (PathTrieSingleChild i pt) PathZipperRoot+pathTrieZipperAscend (PathTrieZipper _ (PathTrieAt _ pt' ipt)) _ = PathTrieZipper pt' ipt
+ src/Data/ECTA/Internal/Term.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE OverloadedStrings #-}++module Data.ECTA.Internal.Term (+ Symbol(.., Symbol)++ , Term(..)+ ) where+++import Data.Hashable ( Hashable(..) )+import qualified Data.Interned as OrigInterned+import Data.Maybe ( maybeToList )+import Data.String (IsString(..) )+import Data.Text ( Text )+import qualified Data.Text as Text+import GHC.Generics ( Generic )+import Text.Read ( Read(..) )++import Data.Interned.Text ( InternedText, internedTextId )+++import Control.Lens ( (&), ix, (^?), (%~) )++import Data.ECTA.Paths+import Data.Text.Extended.Pretty++---------------------------------------------------------------+-------------------------- Symbols ----------------------------+---------------------------------------------------------------++data Symbol = Symbol' {-# UNPACK #-} !InternedText+ deriving ( Eq, Ord )++pattern Symbol :: Text -> Symbol+pattern Symbol t <- Symbol' (OrigInterned.unintern -> t) where+ Symbol t = Symbol' (OrigInterned.intern t)++{-# COMPLETE Symbol #-}++instance Pretty Symbol where+ pretty (Symbol t) = t++instance Show Symbol where+ show (Symbol it) = show it++instance Hashable Symbol where+ hashWithSalt s (Symbol' t) = s `hashWithSalt` (internedTextId t)++instance IsString Symbol where+ fromString = Symbol . fromString++instance Read Symbol where+ readPrec = Symbol <$> readPrec++---------------------------------------------------------------+---------------------------- Terms ----------------------------+---------------------------------------------------------------++data Term = Term !Symbol ![Term]+ deriving ( Eq, Ord, Read, Show, Generic )++instance Hashable Term++instance Pretty Term where+ pretty (Term s []) = pretty s+ pretty (Term s ts) = pretty s <> "(" <> (Text.intercalate ", " $ map pretty ts) <> ")"++---------------------+------ Term ops+---------------------++instance Pathable Term Term where+ type Emptyable Term = Maybe Term++ getPath EmptyPath t = Just t+ getPath (ConsPath p ps) (Term _ ts) = case ts ^? ix p of+ Nothing -> Nothing+ Just t -> getPath ps t++ getAllAtPath p t = maybeToList $ getPath p t++ modifyAtPath f EmptyPath t = f t+ modifyAtPath f (ConsPath p ps) (Term s ts) = Term s (ts & ix p %~ modifyAtPath f ps)
+ src/Data/ECTA/Paths.hs view
@@ -0,0 +1,36 @@+module Data.ECTA.Paths (+ -- * Paths+ Path(EmptyPath, ConsPath)+ , unPath+ , path+ , Pathable(..)+ , pathHeadUnsafe+ , pathTailUnsafe+ , isSubpath++ , PathTrie(TerminalPathTrie)+ , isEmptyPathTrie+ , isTerminalPathTrie+ , getMaxNonemptyIndex+ , toPathTrie+ , fromPathTrie+ , pathTrieDescend++ , PathEClass(getPathTrie)+ , unPathEClass+ , hasSubsumingMember+ , completedSubsumptionOrdering++ -- * Equality constraints over paths+ , EqConstraints(EmptyConstraints)+ , unsafeGetEclasses+ , mkEqConstraints+ , combineEqConstraints+ , eqConstraintsDescend+ , constraintsAreContradictory+ , constraintsImply+ , subsumptionOrderedEclasses+ , unsafeSubsumptionOrderedEclasses+ ) where++import Data.ECTA.Internal.Paths
+ src/Data/ECTA/Term.hs view
@@ -0,0 +1,7 @@+module Data.ECTA.Term (+ Symbol(Symbol)++ , Term(..)+ ) where++import Data.ECTA.Internal.Term
+ src/Data/HashTable/Extended.hs view
@@ -0,0 +1,26 @@+module Data.HashTable.Extended (+ getKeys+ , resetHashTable+ , AnyHashTable(..)+ ) where+++import Data.Hashable ( Hashable )+import Data.HashTable.Class ( HashTable )+import qualified Data.HashTable.IO as HT+++------------------------------------------------------------------------------++getKeys :: (HashTable h) => HT.IOHashTable h k v -> IO [k]+getKeys ht = HT.foldM f [] ht+ where f !l !(k, _) = return (k : l)++resetHashTable :: AnyHashTable -> IO ()+resetHashTable (AnyHashTable ht) = do+ keys <- getKeys ht+ mapM_ (\k -> HT.mutate ht k (const (Nothing, ()))) keys+++data AnyHashTable where+ AnyHashTable :: (HashTable h, Eq k, Hashable k) => HT.IOHashTable h k v -> AnyHashTable
+ src/Data/Interned/Extended/HashTableBased.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE CPP #-}++module Data.Interned.Extended.HashTableBased+ ( Id+ , Cache(..)+ , freshCache+ , cacheSize+ , resetCache++#ifdef PROFILE_CACHES+ , getMetrics+#endif++ , Interned(..)+ , intern+ ) where++import Data.Hashable+import qualified Data.HashTable.IO as HT+import Data.IORef+import GHC.IO ( unsafeDupablePerformIO )++import Data.HashTable.Extended++#ifdef PROFILE_CACHES+import Data.Memoization.Metrics ( CacheMetrics(CacheMetrics) )+#endif++----------------------------------------------------------------------------------------------------------++--------------------+------- Caches+--------------------++type Id = Int++-- | Tried using the BasicHashtable size function to remove need for this IORef+-- ( see https://github.com/gregorycollins/hashtables/pull/68 ), but it was slower+data Cache t = Cache { fresh :: !(IORef Id)+ , content :: !(HT.CuckooHashTable (Description t) t)+#ifdef PROFILE_CACHES+ , queryCount :: !(IORef Int)+ , missCount :: !(IORef Int)+#endif+ }++freshCache :: IO (Cache t)+freshCache = Cache <$> newIORef 0+ <*> HT.new+#ifdef PROFILE_CACHES+ <*> newIORef 0+ <*> newIORef 0+#endif++cacheSize :: Cache t -> IO Int+cacheSize Cache {fresh = refI} = readIORef refI++resetCache :: (Interned t) => Cache t -> IO ()+resetCache _c@(Cache {fresh=refI, content=ht}) = do+ writeIORef refI 0+ resetHashTable (AnyHashTable ht)+#ifdef PROFILE_CACHES+ writeIORef (queryCount _c) 0+ writeIORef (missCount _c) 0+#endif++bumpQueryCount :: Cache t -> IO ()+#ifdef PROFILE_CACHES+bumpQueryCount Cache {queryCount = ref} = modifyIORef ref (+1)+#else+bumpQueryCount _ = return ()+#endif+{-# INLINE bumpQueryCount #-}++bumpMissCount :: Cache t -> IO ()+#ifdef PROFILE_CACHES+bumpMissCount Cache {missCount = ref} = modifyIORef ref (+1)+#else+bumpMissCount _ = return ()+#endif+{-# INLINE bumpMissCount #-}+++#ifdef PROFILE_CACHES+getMetrics :: Cache t -> IO CacheMetrics+getMetrics Cache {queryCount = qc, missCount = mc} = CacheMetrics <$> readIORef qc <*> readIORef mc+#endif++--------------------+------- Interning+--------------------++class ( Eq (Description t)+ , Hashable (Description t)+ ) => Interned t where+ data Description t+ type Uninterned t+ describe :: Uninterned t -> Description t+ identify :: Id -> Uninterned t -> t+ cache :: Cache t++intern :: Interned t => Uninterned t -> t+intern !bt = unsafeDupablePerformIO $ do+ let c = cache+ let refI = fresh c+ let ht = content c+ bumpQueryCount c+ v <- HT.lookup ht dt+ case v of+ Nothing -> do bumpMissCount c+ i <- atomicModifyIORef' refI (\i -> (i + 1, i))+ let t = identify i bt+ HT.insert ht dt t+ return t+ Just t -> return t+ where+ !dt = describe bt
+ src/Data/Interned/Extended/SingleThreaded.hs view
@@ -0,0 +1,29 @@+module Data.Interned.Extended.SingleThreaded (+ intern+ ) where+++import Data.Array+import Data.Hashable+import qualified Data.HashMap.Strict as HashMap+import Data.IORef+import GHC.IO (unsafeDupablePerformIO)++import Data.Interned.Internal hiding ( intern )++--------------------------------------------------++intern :: Interned t => Uninterned t -> t+intern !bt = unsafeDupablePerformIO $ modifyAdvice $ do+ CacheState i m <- readIORef slot+ case HashMap.lookup dt m of+ Nothing -> do let t = identify (wid * i + r) bt+ writeIORef slot (CacheState (i + 1) (HashMap.insert dt t m))+ return t+ Just t -> return t+ where+ slot = getCache cache ! r+ !dt = describe bt+ !hdt = hash dt+ !wid = cacheWidth dt+ r = hdt `mod` wid
+ src/Data/Memoization.hs view
@@ -0,0 +1,168 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}++-- | Quick-and-dirty, thread-unsafe, hash-based memoization.++module Data.Memoization (+ MemoCacheTag(..)++ , resetAllCaches+#ifdef PROFILE_CACHES+ , getAllCacheMetrics+ , printAllCacheMetrics+#endif++ , memoIO+ , memo+ , memo2+ ) where++import Data.Hashable ( Hashable )+import qualified Data.HashTable.IO as HT+import Data.Text ( Text )+import GHC.Generics ( Generic )+import System.IO.Unsafe ( unsafePerformIO )++import Data.HashTable.Extended++import Data.Text.Extended.Pretty++#ifdef PROFILE_CACHES+import Data.IORef ( IORef, newIORef, readIORef, writeIORef, modifyIORef )+import Data.List ( sort )+import Data.Memoization.Metrics ( CacheMetrics(CacheMetrics) )++import qualified Data.Text.IO as Text+#endif++-----------------------------------------------------------------++-------------------------------------------------------------+------------------ Caches and cache metrics -----------------+-------------------------------------------------------------++--------------+---- Memo cache+--------------++#ifdef PROFILE_CACHES+-- | Slightly ill-named. Tracks statistics and hash tables for all memo-caches under a given tag.+-- Multiple caches may be collapsed into the same tag.+data MemoCache = MemoCache { queryCount :: !(IORef Int)+ , missCount :: !(IORef Int)+ , contents :: ![AnyHashTable]+ }++mkCache:: AnyHashTable -> IO MemoCache+mkCache ht = MemoCache <$> newIORef 0 <*> newIORef 0 <*> pure [ht]++resetCache :: MemoCache -> IO ()+resetCache c = do+ writeIORef (queryCount c) 0+ writeIORef (missCount c) 0+ mapM_ resetHashTable (contents c)+#else+type MemoCache = ()+#endif++bumpQueryCount :: MemoCache -> IO ()+#ifdef PROFILE_CACHES+bumpQueryCount c = modifyIORef (queryCount c) (+1)+#else+bumpQueryCount _ = return ()+#endif+++bumpMissCount :: MemoCache -> IO ()+#ifdef PROFILE_CACHES+bumpMissCount c = modifyIORef (missCount c) (+1)+#else+bumpMissCount _ = return ()+#endif++--------------+---- Tags+--------------++data MemoCacheTag = NameTag Text+ deriving ( Eq, Ord, Show, Generic )++instance Hashable MemoCacheTag++mkInnerTag :: MemoCacheTag -> MemoCacheTag+mkInnerTag (NameTag t) = NameTag (t <> "-inner")++instance Pretty MemoCacheTag where+ pretty (NameTag t) = t++--------------+---- Global metrics store+--------------++#ifdef PROFILE_CACHES+memoCaches :: HT.CuckooHashTable MemoCacheTag MemoCache+memoCaches = unsafePerformIO $ HT.new+{-# NOINLINE memoCaches #-}+#endif++initMetrics :: MemoCacheTag -> AnyHashTable -> IO MemoCache+#ifdef PROFILE_CACHES+initMetrics tag ht = do+ newC <- mkCache ht+ HT.mutate memoCaches+ tag+ (\case Nothing -> (Just newC, newC)+ Just c -> let c' = c { contents = ht : contents c}+ in (Just c', c'))+#else+initMetrics _ _ = return ()+#endif++resetAllCaches :: IO ()+#ifdef PROFILE_CACHES+resetAllCaches = HT.mapM_ (\(_, c) -> resetCache c) memoCaches+#else+resetAllCaches = return ()+#endif++#ifdef PROFILE_CACHES+getAllCacheMetrics :: IO [(MemoCacheTag, CacheMetrics)]+getAllCacheMetrics = HT.foldM (\l (k, v) -> getMetrics v >>= \v' -> return ((k, v') : l)) [] memoCaches+ where+ getMetrics :: MemoCache -> IO CacheMetrics+ getMetrics c = CacheMetrics <$> readIORef (queryCount c) <*> readIORef (missCount c)++printAllCacheMetrics :: IO ()+printAllCacheMetrics = do metrics <- getAllCacheMetrics+ mapM_ (\(tag, cm)-> Text.putStrLn $ "(" <> pretty tag <> ")\t" <> pretty cm)+ (sort metrics)+#endif++-------------------------------------------------------------+------------------------ Memoization ------------------------+-------------------------------------------------------------+++memoIO :: forall a b. (Eq a, Hashable a) => MemoCacheTag -> (a -> b) -> IO (a -> IO b)+memoIO tag f = do+ ht :: HT.CuckooHashTable a b <- HT.new+ cache <- initMetrics tag (AnyHashTable ht)+ let f' x = do bumpQueryCount cache+ v <- HT.lookup ht x+ case v of+ Nothing -> do bumpMissCount cache+ let r = f x+ HT.insert ht x r+ return r++ Just r -> return r+ return f'+++memo :: (Eq a, Hashable a) => MemoCacheTag -> (a -> b) -> (a -> b)+memo tag f = let f' = unsafePerformIO (memoIO tag f)+ in \x -> unsafePerformIO (f' x)++memo2 :: (Eq a, Hashable a, Eq b, Hashable b) => MemoCacheTag -> (a -> b -> c) -> a -> b -> c+memo2 tag f = memo tag (memo (mkInnerTag tag) . f)
+ src/Data/Memoization/Metrics.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE OverloadedStrings #-}++module Data.Memoization.Metrics (+ CacheMetrics(..)+ ) where+++import qualified Data.Text as Text++import Data.Text.Extended.Pretty++----------------------------------------------------------++data CacheMetrics = CacheMetrics { queryCount :: {-# UNPACK #-} !Int+ , missCount :: {-# UNPACK #-} !Int+ }+ deriving ( Eq, Ord, Show )+++instance Pretty CacheMetrics where+ pretty cm = "Misses/Queries: " <> (Text.pack $ show $ missCount cm) <> " / " <> (Text.pack $ show $ queryCount cm)+
+ src/Data/Persistent/UnionFind.hs view
@@ -0,0 +1,102 @@+-- | Lightweight union-find implementation suitable for use with nondeterminism++-- Mutable union-find, as in Data.Equivalence.Monad, should be faster overall,+-- but this persistent implementation is suitable for use in nondeterministic search+-- (e.g.: in the list monad)++module Data.Persistent.UnionFind (+ UVarGen+ , initUVarGen+ , nextUVar++ , UVar+ , uvarToInt+ , intToUVar++ , UnionFind+ , empty+ , withInitialValues+ , union+ , find+ ) where++import Control.Monad.State.Strict ( State, runState, execState, get, put, modify' )+import Data.Coerce ( coerce )+import Data.IntMap.Strict ( IntMap )+import qualified Data.IntMap.Strict as IntMap+++----------------------------------------------------------++---------------------------+-------- UVarGen+---------------------------++newtype UVarGen = UVarGen Int+ deriving ( Eq, Ord, Show )++initUVarGen :: UVarGen+initUVarGen = UVarGen 0++nextUVar :: UVarGen -> (UVarGen, UVar)+nextUVar (UVarGen n) = (UVarGen (n+1), UVar n)+++---------------------------+-------- UVar+---------------------------++newtype UVar = UVar Int+ deriving ( Eq, Ord, Show )++uvarToInt :: UVar -> Int+uvarToInt (UVar i) = i++intToUVar :: Int -> UVar+intToUVar = UVar++---------------------------+-------- Union-find data structure+---------------------------++newtype UnionFind = UnionFind { getUnionFindMap :: IntMap Int }+ deriving ( Eq, Ord, Show )++empty :: UnionFind+empty = UnionFind IntMap.empty++withInitialValues :: [UVar] -> UnionFind+withInitialValues uvs = UnionFind $ IntMap.fromList $ map (,-1) $ coerce uvs++---------------------------+-------- Union-find operations+---------------------------++union :: UVar -> UVar -> UnionFind -> UnionFind+union uv1 uv2 uf+ | otherwise = flip execState uf $ do+ (uv1Rep, negativeUv1Size) <- findWithNegSize uv1+ (uv2Rep, negativeUv2Size) <- findWithNegSize uv2+ if uv1Rep == uv2Rep then+ return ()+ else if negativeUv1Size > negativeUv2Size then+ do modify' (coerce (IntMap.insert @Int) uv1Rep uv2Rep)+ modify' (coerce (IntMap.insert @Int) uv2Rep (negativeUv1Size + negativeUv2Size))+ else+ do modify' (coerce (IntMap.insert @Int) uv2Rep uv1Rep)+ modify' (coerce (IntMap.insert @Int) uv1Rep (negativeUv1Size + negativeUv2Size))++findWithNegSize :: UVar -> State UnionFind (UVar, Int)+findWithNegSize uv = do+ m <- get+ case coerce (IntMap.lookup @Int) uv m of+ Nothing -> put (coerce (IntMap.insert @Int) uv (-1 :: Int) m) >> return (uv, -1)+ Just x+ | x < 0 -> return (uv, x)+ | otherwise -> do (rep,size) <- findWithNegSize (UVar x)+ put (coerce (IntMap.insert @Int) uv rep m)+ return (rep, size)+++find :: UVar -> UnionFind -> (UVar, UnionFind)+find uv uf = coerce runState (fst <$> findWithNegSize uv) uf
+ src/Data/Text/Extended/Pretty.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE UndecidableInstances #-}++module Data.Text.Extended.Pretty (+ Pretty(..)+ ) where++import Data.Text ( Text )+import qualified Data.Text as Text++----------------------------------------------------------------------++class Pretty a where+ pretty :: a -> Text++instance {-# OVERLAPPABLE #-} (Show a) => Pretty a where+ pretty = Text.pack . show
+ src/Utility/Fixpoint.hs view
@@ -0,0 +1,30 @@+module Utility.Fixpoint (+ fix+ , fixUnbounded+ , fixMaybe+ ) where++--------------------------------------------------------------++fix :: (Show a, Eq a) => Int -> (a -> a) -> a -> a+fix (-1) _ _ = error "fix: Exceeded maxIters"+fix maxIters f x = let x' = f x in+ if x' == x then+ x+ else+ fix (maxIters - 1) f x'++fixUnbounded :: (Eq a) => (a -> a) -> a -> a+fixUnbounded f x = let x' = f x in+ if x' == x then+ x+ else+ fixUnbounded f x'++fixMaybe :: (Eq a) => (a -> Maybe a) -> a -> Maybe a+fixMaybe f x = case f x of+ Nothing -> Nothing+ Just x' -> if x' == x then+ Just x+ else+ fixMaybe f x'
+ src/Utility/HashJoin.hs view
@@ -0,0 +1,82 @@+module Utility.HashJoin (+ nubById+ , nubByIdSinglePass+ , hashClusterIdNub+ , clusterByHash+ , hashJoin+ ) where++import Control.Monad ( forM_, void )+import Control.Monad.ST ( ST, runST )+import Data.Foldable ( foldrM )++import qualified Data.HashTable.ST.Cuckoo as HT++-------------------------------------+--- Hash join / clustering / nub+-------------------------------------+++-- | PRECONDITION: (h x == h y) => x == y+nubById :: (a -> Int) -> [a] -> [a]+nubById _ [x] = [x]+nubById h ls = runST $ do+ ht <- HT.newSized 101+ mapM_ (\x -> HT.insert ht (h x) x) ls+ HT.foldM (\res (_, v) -> return $ v : res) [] ht++nubByIdSinglePass :: forall a. (a -> Int) -> [a] -> [a]+nubByIdSinglePass _ [x] = [x]+nubByIdSinglePass h ls = runST (go ls [] =<< HT.new)+ where+ go :: [a] -> [a] -> HT.HashTable s Int Bool -> ST s [a]+ go [] acc _ = return acc+ go (x:xs) acc ht = do alreadyPresent <- HT.mutate ht+ (h x)+ (\case Nothing -> (Just True, False)+ Just _ -> (Just True, True))+ if alreadyPresent then+ go xs acc ht+ else+ go xs (x:acc) ht+++maybeAddToHt :: v -> Maybe [v] -> (Maybe [v], ())+maybeAddToHt v = \case Nothing -> (Just [v], ())+ Just vs -> (Just (v : vs), ())++-- This is testing slower than running clusterByHash and nubByIdSinglePass separately. How?+hashClusterIdNub :: (a -> Int) -> (a -> Int) -> [a] -> [[a]]+hashClusterIdNub _ _ [x] = [[x]]+hashClusterIdNub hCluster hNub ls = runST $ do+ clusters <- HT.new+ seen <- HT.new++ forM_ ls $ \x -> do+ alreadyPresent <- HT.mutate seen+ (hNub x)+ (\case Nothing -> (Just True, False)+ Just _ -> (Just True, True))+ if alreadyPresent then+ return ()+ else do+ void $ HT.mutate clusters (hCluster x) (maybeAddToHt x)++ HT.foldM (\res (_, vs) -> return $ vs : res) [] clusters++clusterByHash :: (a -> Int) -> [a] -> [[a]]+clusterByHash h ls = runST $ do+ ht <- HT.new+ mapM_ (\x -> HT.mutate ht (h x) (maybeAddToHt x)) ls+ HT.foldM (\res (_, vs) -> return $ vs : res) [] ht++hashJoin :: (a -> Int) -> (a -> a -> b) -> [a] -> [a] -> [b]+hashJoin h j l1 l2 = runST $ do+ ht2 <- HT.new+ mapM_ (\x -> HT.mutate ht2 (h x) (maybeAddToHt x)) l2+ foldrM (\x res -> do maybeCluster <- HT.lookup ht2 (h x)+ case maybeCluster of+ Nothing -> return res+ Just vs2 -> return $ [j x v2 | v2 <- vs2] ++ res )+ []+ l1
+ test/CacheProfilingSpec.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}++module CacheProfilingSpec ( spec ) where++import Test.Hspec++import Test.Generators.ECTA ()++#ifdef PROFILE_CACHES+import Test.QuickCheck+import Test.QuickCheck.Monadic++import Data.ECTA+import TermSearch+#endif++-----------------------------------------------------------------+++--------------------------------------------------------------+----------------------------- Main ---------------------------+--------------------------------------------------------------++#ifdef PROFILE_CACHES+spec :: Spec+spec = do++ describe "Broken test: same result before and after resetting caches" $ do+ {-+ it "QuickCheck property" $+ property $ \n -> monadicIO $ do+ let n1 = reducePartially n+ nodeCount n1 `seq` run resetAllEctaCaches+ let n2 = reducePartially n+ assert $ n1 == n2++ it "Fixed input" $+ -- Easier to do this than to figure out how to do IO in pure HSpec+ property $ \() -> monadicIO $ do+ let n = size2+ let n1 = reducePartially n+ nodeCount n1 `seq` run resetAllEctaCaches_BrokenDoNotUse+ let n2 = reducePartially n+ assert $ n1 == n2+ -}+ return ()++#else+spec :: Spec+spec = return ()+#endif
+ test/Data/Persistent/UnionFindSpec.hs view
@@ -0,0 +1,78 @@+module Data.Persistent.UnionFindSpec ( spec ) where++import Control.Monad.State ( State, evalState, MonadState(..), modify )+import Control.Monad.Writer ( WriterT(..), MonadWriter(..) )+import Data.Equivalence.Monad ( EquivM, runEquivM, equate, equivalent )++import Test.Hspec+import Test.QuickCheck++import Data.Persistent.UnionFind+++-----------------------------------------------------------+++--------------------------------------------------------------+--------------------------- Commands -------------------------+--------------------------------------------------------------++type EquivTestM s = WriterT [Bool] (EquivM s [UVar] UVar)++-- Needed to work with ST type constraints+newtype ForAllEquivM c v a = ForAllEquivM { unForAllEquivM :: forall s. EquivM s c v a }++runEquivTestM :: (forall s. EquivTestM s a) -> (a, [Bool])+runEquivTestM = \m -> runEquivM (:[]) (++) (unForAllEquivM $ runWriterT' m)+ where+ runWriterT' :: (forall s. EquivTestM s a) -> ForAllEquivM [UVar] UVar (a, [Bool])+ runWriterT' m = ForAllEquivM $ runWriterT m++type PersistentUFTestM = WriterT [Bool] (State UnionFind)++runPersistentUFTestM :: PersistentUFTestM a -> (a, [Bool])+runPersistentUFTestM m = evalState (runWriterT m) empty++data UnionFindCommand = Union UVar UVar+ | CheckEquiv UVar UVar+ deriving ( Show )+++interpCommandEquiv :: UnionFindCommand -> EquivTestM s ()+interpCommandEquiv (Union uv1 uv2) = equate uv1 uv2+interpCommandEquiv (CheckEquiv uv1 uv2) = tell . (:[]) =<< equivalent uv1 uv2++interpCommandPersistentUF :: UnionFindCommand -> PersistentUFTestM ()+interpCommandPersistentUF (Union uv1 uv2) = modify (union uv1 uv2)+interpCommandPersistentUF (CheckEquiv uv1 uv2) = do uf <- get+ let (uv1Rep, uf') = find uv1 uf+ let (uv2Rep, uf'') = find uv2 uf'+ put uf''+ tell [uv1Rep == uv2Rep]++++--------------------------------------------------------------+-------------------------- Generators ------------------------+--------------------------------------------------------------++instance Arbitrary UVar where+ arbitrary = intToUVar <$> chooseInt (0, 10)+ shrink _ = []++instance Arbitrary UnionFindCommand where+ arbitrary = oneof [ Union <$> arbitrary <*> arbitrary+ , CheckEquiv <$> arbitrary <*> arbitrary+ ]++ shrink _ = []++--------------------------------------------------------------+----------------------------- Main ---------------------------+--------------------------------------------------------------++spec :: Spec+spec = do+ it "random stream of union/check-equiv commands gives same result as EquivM library" $+ property $ \cmds -> runEquivTestM (mapM_ @[] interpCommandEquiv cmds)+ == runPersistentUFTestM (mapM_ @[] interpCommandPersistentUF cmds)
+ test/ECTASpec.hs view
@@ -0,0 +1,351 @@+{-# 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']]
+ test/PathsSpec.hs view
@@ -0,0 +1,179 @@+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)+ -}+
+ test/SATSpec.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE OverloadedStrings #-}++module SATSpec ( spec ) where++import qualified Data.HashMap.Strict as HashMap+import qualified Data.HashSet as HashSet+import Test.Hspec++import Application.SAT++-----------------------------------------------------------------++smallFormula :: CNF+smallFormula = And [ Or [PosLit "x1", PosLit "x2"]+ , Or [NegLit "x1", NegLit "x2"]+ ]++--------++spec :: Spec+spec = do+ describe "SAT test inputs" $ do+ it "solves a 2-var, 2-clause problem" $+ allSolutions smallFormula `shouldBe` (HashSet.fromList [ HashMap.fromList [("x1", True), ("x2", False)]+ , HashMap.fromList [("x1", False), ("x2", True)]+ ])
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ test/Test/Generators/ECTA.hs view
@@ -0,0 +1,78 @@+{-# Language OverloadedStrings #-}++module Test.Generators.ECTA () where++import Prelude hiding ( max )++import Control.Monad ( replicateM )+import Data.List ( subsequences, (\\) )++import Test.QuickCheck++import Data.ECTA+import Data.ECTA.Internal.ECTA.Type+import Data.ECTA.Paths+import Data.ECTA.Term++-----------------------------------------------------------------------------------------------+++-- Cap size at 3 whenever you will generate all denotations+_MAX_NODE_DEPTH :: Int+_MAX_NODE_DEPTH = 5++capSize :: Int -> Gen a -> Gen a+capSize max g = sized $ \n -> if n > max then+ resize max g+ else+ g++instance Arbitrary Node where+ arbitrary = capSize _MAX_NODE_DEPTH $ sized $ \_n -> do+ k <- chooseInt (1, 3) -- TODO: Should this depend on n?+ Node <$> replicateM k arbitrary++ shrink EmptyNode = []+ shrink (Node es) = [Node es' | s <- subsequences es \\ [es], es' <- mapM shrink s] ++ concatMap (\e -> edgeChildren e) es+ shrink (Mu _) = []+ shrink (Rec _) = []+++testEdgeTypes :: [(Symbol, Int)]+testEdgeTypes = [ ("f", 1)+ , ("g", 2)+ , ("h", 1)+ , ("w", 3)+ , ("a", 0)+ , ("b", 0)+ , ("c", 0)+ ]++testConstants :: [Symbol]+testConstants = map fst $ filter ((== 0) . snd) testEdgeTypes++randPathPair :: [Node] -> Gen [Path]+randPathPair ns = do p1 <- randPath ns+ p2 <- randPath ns+ return [p1, p2]++randPath :: [Node] -> Gen Path+randPath [] = return EmptyPath+randPath ns = do i <- chooseInt (0, length ns - 1)+ let Node es = ns !! i+ ns' <- edgeChildren <$> elements es+ b <- arbitrary+ if b then return (path [i]) else ConsPath i <$> randPath ns'++instance Arbitrary Edge where+ arbitrary =+ sized $ \n -> case n of+ 0 -> Edge <$> elements testConstants <*> pure []+ _ -> do (sym, arity) <- elements testEdgeTypes+ ns <- replicateM arity (resize (n-1) (arbitrary `suchThat` (/= EmptyNode)))+ numConstraintPairs <- elements [0,0,1,1,2,3]+ ps <- replicateM numConstraintPairs (randPathPair ns)+ return $ mkEdge sym ns (mkEqConstraints ps)++ shrink e = mkEdge (edgeSymbol e) <$> (mapM shrink (edgeChildren e)) <*> pure (edgeEcs e)+
+ test/Utility/HashJoinSpec.hs view
@@ -0,0 +1,16 @@+module Utility.HashJoinSpec ( spec) where++import Data.List ( nub, sort )++import Test.Hspec+import Test.QuickCheck++import Utility.HashJoin++-----------------------------------------------------------------++spec :: Spec+spec = do+ describe "hash utilities" $ do+ it "nubById is same as nub" $+ property $ \(xs :: [Int]) -> sort (nub xs) == sort (nubById id xs)