diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,12 @@ +# Changelog + +## 0.1.0.0 - 2026-06-09 + +* Initial release of microecta +* Extract the small ECTA core and term-search compatibility layer into a + Cabal-only package. +* Add ECTA pruning +* Add sparse path tries, a dependency-light benchmark harness, and baked + compile-time RTS caps so optimized builds stay inside the 512M target. +* Document the main API, pruning callbacks, module map, dependency surface, + and benchmark baseline. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,31 @@ +Copyright Jimmy Koppel (c) 2021-2025 +Copyright Matthias Pall Gissurarson (c) 2026 + +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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,186 @@ +# microecta + +`microecta` is a small equality-constrained tree automata library extracted +from the [`ecta`](https://hackage.haskell.org/package/ecta) package. + +It keeps the core ECTA engine and the tiny term-search compatibility layer used +by downstream projects. + +The intent is similar to the relationship between `microlens` and `lens`: keep +the useful core small, direct, and quick to build. + +## Core API + +The main entry point is `Data.ECTA`. + +```haskell +import Data.ECTA +import Data.ECTA.Paths +import Data.ECTA.Term +``` + +An ECTA is a `Node`, which is a set of outgoing `Edge`s. An `Edge` has a symbol, +child nodes, and optional equality constraints over paths into those children. + +```haskell +intType :: Node +intType = Node [Edge "Int" []] + +maybeIntType :: Node +maybeIntType = Node [Edge "Maybe" [intType]] + +sameChildren :: Edge +sameChildren = + mkEdge + "Pair" + [intType, intType] + (mkEqConstraints [[path [0], path [1]]]) +``` + +Useful operations: + +- `union` combines alternatives. +- `intersect` keeps terms accepted by both automata. +- `reducePartially` propagates equality constraints and removes impossible + alternatives. +- `withoutRedundantEdges` removes alternatives implied by other alternatives. +- `nodeRepresents` checks concrete term membership. +- `nodeRepresentsTemplate` checks pruning-template membership; a template + symbol named `` acts as a wildcard. +- `getAllTerms` and `getAllTermsPrune` enumerate accepted terms. + +## Pruning API + +`getAllTermsPrune` exposes partially enumerated `TermFragment`s to pruning +oracles. `Data.ECTA` also exports `fragRepresents`, the helper used by the +original pruning path to compare those fragments against known concrete +`Term`s. + +A pruning oracle receives the caller's state, the UVar being expanded, and +either: + +- `Right node`, before that ECTA node is expanded +- `Left fragment`, after a `TermFragment` has been produced + +Return `True` to discard the current nondeterministic branch, or `False` to +keep enumerating with the updated state. + +```haskell +prunedTerms :: [Term] -> Node -> [Term] +prunedTerms forbidden = + getAllTermsPrune () $ \() _ event -> + case event of + Right node -> + pure (any (nodeRepresentsTemplate node) forbidden, ()) + Left fragment -> do + represented <- fragRepresents True fragment forbidden + pure (represented, ()) +``` + +For repeated reduction, downstream code usually wants: + +```haskell +reduceFully :: Node -> Node +reduceFully = fixUnbounded (withoutRedundantEdges . reducePartially) +``` + +`Application.TermSearch.TermSearch` exports that helper directly. + +## Term-Search Compatibility Layer + +The `Application.TermSearch.*` modules are intentionally tiny. They provide only +the pieces that downstream projects still use: + +- `TypeSkeleton` +- `typeToFta` +- `filterType` +- small type constructors and helpers: `arrowType`, `mkDatatype`, `typeConst`, + `genVar`, and `constFunc` + +## Module Map + +- `Data.ECTA` is the main ECTA API: node and edge construction, intersection, + reduction, traversal, and enumeration. +- `Data.ECTA.Paths` and `Data.ECTA.Term` expose the public path, equality + constraint, symbol, and concrete term types used by `Data.ECTA`. +- `Application.TermSearch.*` is the small compatibility layer for downstream + term-search-shaped type encodings. +- `Data.ECTA.Internal.*` contains the equality-constrained tree automata + engine. These modules are exposed for downstream code that already relies on + lower-level operations, but new code should start with `Data.ECTA`. +- `Data.Interned.Extended.HashTableBased`, `Data.Memoization`, + `Data.Persistent.UnionFind`, and `Utility.*` are support modules used by the + engine. Import them directly only when extending or debugging the internals. + +## Dependency Surface + +The library dependency set is intentionally small: + +- `containers`, `unordered-containers` +- `hashable`, `hashtables`, `intern` +- `mtl`, `transformers` +- `text` +- `equivalence` + +`equivalence` is retained for equality-constraint closure in the path logic. + +## Performance Notes + +The core still uses the original hash-consing, memoization, union-find, +recursive-node, and path/equality-constraint machinery. Those are the hard parts +of ECTA and are intentionally kept. + +The old dense `PathTrie` representation compiled poorly at `-O2` under a +512M compiler memory cap. `microecta` uses a sparse `PathTrie` with a compact +single-child fast path. In the current benchmark suite this preserves the +important runtime shape while allowing the library and benchmark to build at +`-O2` with the baked 512M cap. + +Run the benchmark suite with: + +```sh +cabal v2-bench bench:micro-bench --enable-optimization=2 --ghc-options=-O2 --benchmark-options='1 +RTS -s -M512M -RTS' +``` + +The benchmark harness is deliberately dependency-light and prints CSV: + +```text +benchmark,cpu_seconds,repeats,checksum +``` + +The suite covers the current high-risk core paths: + +- path lookup in term-search-shaped nodes +- equality-constraint construction and descent +- finite and recursive intersection +- recursive-path reduction +- filtered term-search reduction and enumeration + +The current optimized local snapshot, using GHC 9.12.2, multiplier `1`, and +`+RTS -s -M512M -RTS`, is about 5.436 GB allocated, 4.29 MB maximum residency, +and roughly 1.1-1.2s elapsed on the maintainer machine. Treat that as a +regression guard, not a portable absolute number. + +Use a larger first argument for longer runs: + +```sh +cabal v2-bench bench:micro-bench --enable-optimization=2 --ghc-options=-O2 --benchmark-options='3 +RTS -s -M512M -RTS' +``` + +## Build + +This package is Cabal-only. + +```sh +cabal v2-build all -j1 +cabal v2-test unit-tests -j1 +``` + +The library has compiler RTS options baked in: + +```text ++RTS -K512M -M512M -RTS +``` + +That cap is intentional: it catches compile-time memory regressions before they +kill small development environments. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +import Distribution.Simple + +main = defaultMain diff --git a/benchmarks/Benchmarks.hs b/benchmarks/Benchmarks.hs new file mode 100644 --- /dev/null +++ b/benchmarks/Benchmarks.hs @@ -0,0 +1,231 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Main (main) where + +import Control.Exception (evaluate) +import qualified Data.Text as Text +import System.CPUTime (getCPUTime) +import System.Environment (getArgs) +import Text.Printf (printf) + +import Application.TermSearch.Dataset (typeToFta) +import Application.TermSearch.TermSearch (filterType, reduceFully) +import Application.TermSearch.Type (TypeSkeleton (..)) +import Application.TermSearch.Utils ( + arrowType, + constFunc, + mkDatatype, + theArrowNode, + typeConst, + ) +import Data.ECTA +import Data.ECTA.Internal.ECTA.Operations (reduceEqConstraints) +import Data.ECTA.Paths +import Data.ECTA.Term (Symbol (Symbol)) + +data Bench = Bench + { benchName :: String + , benchRepeats :: Int + , benchAction :: Int -> IO Int + } + +main :: IO () +main = do + multiplier <- parseMultiplier <$> getArgs + putStrLn "benchmark,cpu_seconds,repeats,checksum" + mapM_ (runBench multiplier) benchmarks + +parseMultiplier :: [String] -> Int +parseMultiplier [] = 1 +parseMultiplier (x : _) = + case reads x of + [(n, "")] -> max 1 n + _ -> 1 + +runBench :: Int -> Bench -> IO () +runBench multiplier Bench{benchName, benchRepeats, benchAction} = do + start <- getCPUTime + checksum <- loop totalRepeats 0 + end <- getCPUTime + let seconds = fromIntegral (end - start) / (10 ^ (12 :: Int) :: Double) + printf "%s,%.6f,%d,%d\n" benchName seconds totalRepeats checksum + where + totalRepeats = benchRepeats * multiplier + + loop 0 !acc = return acc + loop n !acc = do + x <- benchAction n + loop (n - 1) (acc + x) + +benchmarks :: [Bench] +benchmarks = + [ Bench "getPath/type-search-node" 2000 $ \i -> + forceNode $ getPath (path [2, 0, if i >= 0 then 2 else 1]) typeSearchNode + , Bench "mkEqConstraints/congruence" 600 $ \i -> + forceEqConstraints $ mkEqConstraints (congruencePathSets i) + , Bench "eqConstraintsDescend/wide-sparse" 4000 $ \i -> + forceEqConstraints $ eqConstraintsDescend wideSparseConstraints (i `rem` 16) + , Bench "intersect/finite-constrained" 800 $ \i -> + forceNode $ finiteChoiceNode i `intersect` constrainedChoiceNode i + , Bench "intersect/recursive-types" 300 $ \i -> + forceNode $ recursiveTypeA i `intersect` recursiveTypeB i + , Bench "reduce/recursive-paths" 120 $ \i -> + forceNodes $ reduceEqConstraints recursivePathConstraints EmptyConstraints (recursivePathNodes i) + , Bench "reduce/filter-maybe-int-size-2" 80 $ \i -> + forceNode $ reduceFully (filterMaybeIntSize2 i) + , Bench "reduce/filter-list-int-size-3" 20 $ \i -> + forceNode $ reduceFully (filterListIntSize3 i) + , Bench "enumerate/reduced-filter-maybe-int-size-2" 80 $ \i -> + forceInt $ length (take 64 (getAllTerms (reduceFully (filterMaybeIntSize2 i)))) + ] + +forceNode :: Node -> IO Int +forceNode n = forceInt (nodeCount n + edgeCount n) + +forceNodes :: [Node] -> IO Int +forceNodes = forceInt . sum . map (\n -> nodeCount n + edgeCount n) + +forceEqConstraints :: EqConstraints -> IO Int +forceEqConstraints = + forceInt + . sum + . map (sum . map (length . unPath) . unPathEClass) + . unsafeGetEclasses + +forceInt :: Int -> IO Int +forceInt = evaluate + +typeSearchNode :: Node +typeSearchNode = + appNode + (appNode (monoFunctionScope 0) (monoArgumentScope 0)) + (monoTermsOfSize 0 2) + +filterMaybeIntSize2 :: Int -> Node +filterMaybeIntSize2 i = + filterType + (monoTermsOfSize i 2) + (typeToFta $ TCons "Maybe" [TCons "Int" []]) + +filterListIntSize3 :: Int -> Node +filterListIntSize3 i = + filterType + (monoTermsOfSize i 3) + (typeToFta $ TCons "List" [TCons "Int" []]) + +monoTermsOfSize :: Int -> Int -> Node +monoTermsOfSize salt size = union (go size) + where + go 0 = [] + go 1 = [monoArgumentScope salt, monoFunctionScope salt] + go n = + [ appNode (union (go i)) (union (go (n - i))) + | i <- [1 .. n - 1] + ] + +appNode :: Node -> Node -> Node +appNode f x = + Node + [ mkEdge + "app" + [getPath (path [0, 2]) f, theArrowNode, f, x] + ( mkEqConstraints + [ [path [1], path [2, 0, 0]] + , [path [3, 0], path [2, 0, 1]] + , [path [0], path [2, 0, 2]] + ] + ) + ] + +monoArgumentScope :: Int -> Node +monoArgumentScope salt = + Node + [ constFunc (named "x" salt) (typeConst "Int") + , constFunc (named "y" salt) (typeConst "Int") + , constFunc (named "xs" salt) (mkDatatype "List" [typeConst "Int"]) + ] + +monoFunctionScope :: Int -> Node +monoFunctionScope salt = + Node + [ constFunc (named "idInt" salt) (arrowType intType intType) + , constFunc (named "JustInt" salt) (arrowType intType maybeIntType) + , constFunc (named "headInt" salt) (arrowType listIntType intType) + , constFunc (named "nilInt" salt) listIntType + , constFunc (named "consInt" salt) (arrowType intType (arrowType listIntType listIntType)) + ] + +named :: String -> Int -> Symbol +named prefix salt = Symbol $ Text.pack (prefix ++ show salt) + +intType :: Node +intType = typeConst "Int" + +maybeIntType :: Node +maybeIntType = mkDatatype "Maybe" [intType] + +listIntType :: Node +listIntType = mkDatatype "List" [intType] + +congruencePathSets :: Int -> [[Path]] +congruencePathSets salt = + [ [path [i], path [i + 1]] + | i <- [base .. base + 5] + ] + ++ [ [path [i, 0], path [i, 1]] + | i <- [base .. base + 5] + ] + where + base = salt `rem` 3 + +wideSparseConstraints :: EqConstraints +wideSparseConstraints = + mkEqConstraints + [ [path [i, 0], path [i, 1]] + | i <- [0 .. 15] + ] + +finiteChoiceNode :: Int -> Node +finiteChoiceNode salt = + Node + [ Edge (named "f" salt) [choiceAB salt, choiceAB salt] + , Edge (named "g" salt) [choiceAB salt, choiceAB salt] + ] + +constrainedChoiceNode :: Int -> Node +constrainedChoiceNode salt = + Node + [ mkEdge (named "f" salt) [choiceAB salt, choiceAB salt] (mkEqConstraints [[path [0], path [1]]]) + , Edge (named "g" salt) [choiceAB salt, choiceAB salt] + ] + +choiceAB :: Int -> Node +choiceAB salt = Node [Edge (named "a" salt) [], Edge (named "b" salt) []] + +recursivePathConstraints :: EqConstraints +recursivePathConstraints = mkEqConstraints [[path [0, 0, 0, 0], path [1, 0, 0]]] + +recursivePathNodes :: Int -> [Node] +recursivePathNodes salt = [infiniteFNode salt, infiniteFNode salt] + +infiniteFNode :: Int -> Node +infiniteFNode salt = createMu $ \r -> Node [Edge (named "f" salt) [r]] + +recursiveTypeA :: Int -> Node +recursiveTypeA salt = + createMu $ \r -> + Node + [ Edge (named "baseType" salt) [] + , Edge "->" [theArrowNode, r, r] + , Edge "Maybe" [r] + , Edge "List" [r] + ] + +recursiveTypeB :: Int -> Node +recursiveTypeB salt = + createMu $ \r -> + Node + [ Edge (named "baseType" salt) [] + , Edge "->" [theArrowNode, mkDatatype "List" [r], r] + , Edge "List" [r] + ] diff --git a/microecta.cabal b/microecta.cabal new file mode 100644 --- /dev/null +++ b/microecta.cabal @@ -0,0 +1,144 @@ +cabal-version: 2.4 +name: microecta +version: 0.1.0.0 +synopsis: Small equality-constrained tree automata core +description: A small equality-constrained tree automata core extracted from ecta. +homepage: https://github.com/Tritlo/microecta#readme +bug-reports: https://github.com/Tritlo/microecta/issues +category: Data +author: Jimmy Koppel, Matthias Pall Gissurarson +maintainer: mpg@mpg.is +copyright: 2021-2025 Jimmy Koppel, 2026 Matthias Pall Gissurarson +license: BSD-3-Clause +license-file: LICENSE +build-type: Simple +tested-with: ghc ==9.12.2 +extra-doc-files: + CHANGELOG.md + README.md + +source-repository head + type: git + location: https://github.com/Tritlo/microecta.git + +common warnings + ghc-options: -Wall + +common extensions + 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 + +library + import: warnings, extensions + hs-source-dirs: src + ghc-options: + +RTS + -K512M + -M512M + -RTS + + exposed-modules: + Application.TermSearch.Dataset + 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.Paths + Data.ECTA.Internal.Term + Data.ECTA.Paths + Data.ECTA.Term + Data.Interned.Extended.HashTableBased + Data.Memoization + Data.Persistent.UnionFind + Utility.Fixpoint + Utility.HashJoin + + other-modules: + Data.Text.Extended.Pretty + + build-depends: + base >=4.13 && <5, + containers >=0.7 && <0.8, + equivalence >=0.4.1 && <0.5, + hashable >=1.5.1.0 && <1.6, + hashtables >=1.4.2 && <1.5, + intern >=0.9.6 && <0.10, + mtl >=2.3.1 && <2.4, + text >=2.1.2 && <2.2, + transformers >=0.6.1.2 && <0.7, + unordered-containers >=0.2.21 && <0.3, + +test-suite unit-tests + import: warnings, extensions + type: exitcode-stdio-1.0 + main-is: Spec.hs + hs-source-dirs: test + ghc-options: + -threaded + -rtsopts + -with-rtsopts=-N + -Wno-orphans + + other-modules: + Data.Persistent.UnionFindSpec + ECTASpec + PathsSpec + Test.Generators.ECTA + Utility.HashJoinSpec + + build-depends: + QuickCheck, + base >=4.13 && <5, + containers, + equivalence >=0.4.1 && <0.5, + hashable, + hspec, + microecta, + mtl, + text, + unordered-containers, + +benchmark micro-bench + import: warnings, extensions + type: exitcode-stdio-1.0 + main-is: Benchmarks.hs + hs-source-dirs: benchmarks + ghc-options: + -O2 + -rtsopts + -with-rtsopts=-M512M + + build-depends: + base >=4.13 && <5, + microecta, + text, diff --git a/src/Application/TermSearch/Dataset.hs b/src/Application/TermSearch/Dataset.hs new file mode 100644 --- /dev/null +++ b/src/Application/TermSearch/Dataset.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE OverloadedStrings #-} + +{- | Conversion from the tiny compatibility type language to ECTA nodes. + +The old @Application.TermSearch.Dataset@ module contained the large Hoogle +table. @microecta@ keeps this module name only for downstream compatibility; the +only remaining operation is 'typeToFta'. +-} +module Application.TermSearch.Dataset ( + typeToFta, +) where + +import Data.ECTA + +import Application.TermSearch.Type +import Application.TermSearch.Utils + +-- | Translate a 'TypeSkeleton' into the ECTA encoding used by term search. +typeToFta :: TypeSkeleton -> Node +typeToFta (TVar v) = genVar 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) diff --git a/src/Application/TermSearch/TermSearch.hs b/src/Application/TermSearch/TermSearch.hs new file mode 100644 --- /dev/null +++ b/src/Application/TermSearch/TermSearch.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE OverloadedStrings #-} + +{- | Tiny term-search helpers retained from @ecta@. + +The full search engine and Hoogle dataset are intentionally absent. This module +keeps the two operations downstream code uses: constrain a term node by a type +node with 'filterType', and run the standard reduction loop with 'reduceFully'. +-} +module Application.TermSearch.TermSearch ( + filterType, + reduceFully, +) where + +import Data.ECTA +import Data.ECTA.Paths +import Utility.Fixpoint + +-- | Constrain a term-search node by equating its type child with a type node. +filterType :: Node -> Node -> Node +filterType n t = + Node [mkEdge "filter" [t, n] (mkEqConstraints [[path [0], path [1, 0]]])] + +-- | Repeatedly propagate constraints and remove redundant edges to a fixpoint. +reduceFully :: Node -> Node +reduceFully = fixUnbounded (withoutRedundantEdges . reducePartially) diff --git a/src/Application/TermSearch/Type.hs b/src/Application/TermSearch/Type.hs new file mode 100644 --- /dev/null +++ b/src/Application/TermSearch/Type.hs @@ -0,0 +1,32 @@ +{- | Small type language used by the compatibility term-search helpers. + +The original @ecta@ package carried a much larger term-search application. In +@microecta@, this module is just the lightweight type skeleton that downstream +projects use before translating types to ECTA nodes with +'Application.TermSearch.Dataset.typeToFta'. +-} +module Application.TermSearch.Type ( + TypeSkeleton (..), +) where + +import Data.Data (Data) +import Data.Hashable (Hashable (..)) +import Data.Text (Text) + +-- | Minimal first-order type syntax. +data TypeSkeleton + = -- | Type variable. + TVar Text + | -- | Function type. + TFun TypeSkeleton TypeSkeleton + | -- | Type constructor applied to zero or more arguments. + TCons Text [TypeSkeleton] + deriving (Eq, Ord, Show, Read, Data) + +instance Hashable TypeSkeleton where + hashWithSalt salt (TVar name) = + salt `hashWithSalt` (0 :: Int) `hashWithSalt` name + hashWithSalt salt (TFun fromType toType) = + salt `hashWithSalt` (1 :: Int) `hashWithSalt` fromType `hashWithSalt` toType + hashWithSalt salt (TCons name args) = + salt `hashWithSalt` (2 :: Int) `hashWithSalt` name `hashWithSalt` args diff --git a/src/Application/TermSearch/Utils.hs b/src/Application/TermSearch/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Application/TermSearch/Utils.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE OverloadedStrings #-} + +{- | Small constructors for the term-search ECTA encoding. + +These helpers deliberately stay as small wrappers around @Node@ and @Edge@. +They are here to preserve the useful surface area of @ecta@ without bringing +back the larger search application. +-} +module Application.TermSearch.Utils ( + typeConst, + theArrowNode, + arrowType, + mkDatatype, + constFunc, + genVar, +) where + +import Data.Text (Text) + +import Data.ECTA +import Data.ECTA.Term + +-- | Nullary type constructor. +typeConst :: Text -> Node +typeConst s = Node [Edge (Symbol s) []] + +-- | Marker node used as the first child of encoded function types. +theArrowNode :: Node +theArrowNode = Node [Edge "(->)" []] + +-- | Function type in the term-search encoding. +arrowType :: Node -> Node -> Node +arrowType n1 n2 = Node [Edge "->" [theArrowNode, n1, n2]] + +-- | Type constructor applied to encoded argument types. +mkDatatype :: Text -> [Node] -> Node +mkDatatype s ns = Node [Edge (Symbol s) ns] + +-- | Term symbol with a single child describing its type. +constFunc :: Symbol -> Node -> Edge +constFunc s t = Edge s [t] + +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" []] + +varPrefix :: Text +varPrefix = "__gen_var_" + +-- | Generate the canonical ECTA node for a type variable. +genVar :: Text -> Node +genVar "a" = var1 +genVar "b" = var2 +genVar "c" = var3 +genVar "d" = var4 +genVar "acc" = varAcc +genVar s = Node [Edge (Symbol $ varPrefix <> s) []] diff --git a/src/Data/ECTA.hs b/src/Data/ECTA.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA.hs @@ -0,0 +1,70 @@ +{- | Equality-constrained finite tree automata. + +This is the main public API for the ECTA core. + +A @Node@ represents a set of accepted terms. Each outgoing @Edge@ is one +alternative: it has a symbol, child nodes, and optional equality constraints +over paths into those children. @microecta@ keeps the original ECTA algorithms +for intersection, reduction, refolding, and enumeration, but leaves out the +larger application layers from @ecta@. + +The usual workflow is: + +1. Build nodes with @Node@, @Edge@, and 'mkEdge'. +2. Combine nodes with 'union' and 'intersect'. +3. Propagate equality constraints with 'reducePartially'. +4. Remove implied alternatives with 'withoutRedundantEdges'. +5. Check concrete or template membership with 'nodeRepresents' or + 'nodeRepresentsTemplate'. +6. Enumerate accepted terms with 'getAllTerms' or 'getAllTermsPrune'. + +Recursive automata are represented with 'createMu'. Internally nodes and edges +are hash-consed, so equality and memoized operations can use compact identities +instead of repeatedly traversing the same graph. +-} +module Data.ECTA ( + Edge (Edge), + mkEdge, + edgeChildren, + edgeSymbol, + Node (Node, EmptyNode), + nodeEdges, + numNestedMu, + createMu, + + -- * Operations + nodeMapChildren, + pathsMatching, + mapNodes, + refold, + unfoldBounded, + crush, + onNormalNodes, + nodeCount, + edgeCount, + maxIndegree, + union, + intersect, + withoutRedundantEdges, + reducePartially, + + -- * Membership + nodeRepresents, + edgeRepresents, + nodeRepresentsTemplate, + edgeRepresentsTemplate, + + -- * Enumeration + EnumerateM, + runEnumerateM, + TermFragment (..), + enumerateFully, + fragRepresents, + getAllTerms, + getAllTermsPrune, + getAllTruncatedTerms, +) where + +import Data.ECTA.Internal.ECTA.Enumeration +import Data.ECTA.Internal.ECTA.Operations +import Data.ECTA.Internal.ECTA.Type diff --git a/src/Data/ECTA/Internal/ECTA/Enumeration.hs b/src/Data/ECTA/Internal/ECTA/Enumeration.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Internal/ECTA/Enumeration.hs @@ -0,0 +1,726 @@ +{-# LANGUAGE OverloadedStrings #-} + +{- | Nondeterministic enumeration for ECTAs. + +Enumeration builds 'TermFragment's before expanding them to concrete @Term@s. +Equality constraints are represented by suspended path-trie obligations that +point at UVars. When enumeration descends through an edge, those obligations +descend with it; when an obligation reaches the current node, the corresponding +UVars are merged so future choices stay consistent. + +Most callers should use 'getAllTerms' or 'getAllTermsPrune'. The lower-level +state operations are exposed for pruning oracles and downstream tools that need +to inspect or steer enumeration. +-} +module Data.ECTA.Internal.ECTA.Enumeration ( + TermFragment (..), + termFragToTruncatedTerm, + SuspendedConstraint (..), + scGetPathTrie, + scGetUVar, + descendScs, + UVarValue (..), + EnumerationState (..), + uvarCounter, + uvarRepresentative, + uvarValues, + pruneDeps, + initEnumerationState, + EnumerateM, + getUVarRepresentative, + assimilateUvarVal, + mergeNodeIntoUVarVal, + getUVarValue, + getTermFragForUVar, + runEnumerateM, + getPruneDepsOf, + getPruneDeps, + addPruneDep, + deletePruneDep, + fragRepresents, + enumerateNode, + enumerateEdge, + ExpandableUVarResult (..), + firstExpandableUVar, + enumerateOutUVar, + enumerateOutFirstExpandableUVar, + enumerateFully, + expandTermFrag, + expandPartialTermFrag, + expandUVar, + getAllTruncatedTerms, + getAllTerms, + getAllTermsPrune, + enumPrune, +) where + +import Control.Monad (filterM, forM_, guard, mzero, void, zipWithM) +import Control.Monad.State.Strict (StateT (..), gets, modify') +import Control.Monad.Trans.Class (lift) +import qualified Data.IntMap as IntMap +import Data.Maybe (fromMaybe) +import Data.Semigroup (Max (..)) +import Data.Sequence (Seq ((:<|), (:|>))) +import qualified Data.Sequence as Sequence + +import Data.ECTA.Internal.ECTA.Operations +import Data.ECTA.Internal.ECTA.Type +import Data.ECTA.Paths +import Data.ECTA.Term +import qualified Data.IntSet as IntSet +import Data.Persistent.UnionFind (UVar, UVarGen, UnionFind, intToUVar, uvarToInt) +import qualified Data.Persistent.UnionFind as UnionFind +import Data.Text.Extended.Pretty + +------------------------------------------------------------------------------- + +--------------------------------------------------------------------------- +------------------------------- Term fragments ---------------------------- +--------------------------------------------------------------------------- + +-- | Partially enumerated term with holes for nodes that still need expansion. +data TermFragment + = -- | Concrete symbol with already-created child fragments. + TermFragmentNode !Symbol ![TermFragment] + | -- | Hole whose value is tracked in the enumeration state. + TermFragmentUVar UVar + deriving (Eq, Ord, Show) + +-- | Convert a fragment to a term, rendering holes as variable-like leaves. +termFragToTruncatedTerm :: TermFragment -> Term +termFragToTruncatedTerm (TermFragmentNode s ts) = Term s (map termFragToTruncatedTerm ts) +termFragToTruncatedTerm (TermFragmentUVar uv) = Term (Symbol $ "v" <> pretty (uvarToInt uv)) [] + +--------------------------------------------------------------------------- +------------------------------ Enumeration state -------------------------- +--------------------------------------------------------------------------- + +lens :: (Functor f) => (s -> a) -> (s -> a -> s) -> (a -> f a) -> s -> f s +lens getter setter f s = setter s <$> f (getter s) + +----------------------- +------- Suspended constraints +----------------------- + +-- | Equality obligation that has not yet reached the node it constrains. +data SuspendedConstraint = SuspendedConstraint !PathTrie !UVar + deriving (Eq, Ord, Show) + +-- | Remaining paths for a suspended equality obligation. +scGetPathTrie :: SuspendedConstraint -> PathTrie +scGetPathTrie (SuspendedConstraint pt _) = pt + +-- | UVar that must be merged when the suspended obligation is reached. +scGetUVar :: SuspendedConstraint -> UVar +scGetUVar (SuspendedConstraint _ uv) = uv + +-- | Push suspended obligations through child index @i@ and drop empty paths. +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 +----------------------- + +-- | Enumeration status for one UVar. +data UVarValue + = UVarUnenumerated + { contents :: !(Maybe Node) + -- ^ ECTA node still to enumerate, or 'Nothing' for pure constraint variables. + , constraints :: !(Seq SuspendedConstraint) + -- ^ Constraints that should be carried while enumerating this value. + } + | -- | UVar has been expanded to a fragment. + UVarEnumerated {termFragment :: !TermFragment} + | -- | UVar was merged into another representative and should no longer be used. + 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 +----------------------- + +-- | Mutable state threaded through nondeterministic enumeration branches. +data EnumerationState = EnumerationState + { _uvarCounter :: UVarGen + -- ^ Fresh UVar supply. + , _uvarRepresentative :: UnionFind + -- ^ Persistent union-find for equality-constrained UVars. + , _uvarValues :: Seq UVarValue + -- ^ Per-UVar contents indexed by 'uvarToInt'. + , _pruneDeps :: !(IntMap.IntMap [Term]) + {- ^ Pending prune checks keyed by suspended UVar id. + + A pruning oracle can use this to remember rewrite/template terms that + could not be checked until a particular UVar is expanded. The pruned + enumerator prioritizes expandable UVars that have entries here and + rechecks the stored terms when that UVar is enumerated. + -} + } + deriving (Eq, Ord, Show) + +-- | Lens-compatible accessor for the fresh UVar supply. +uvarCounter :: (Functor f) => (UVarGen -> f UVarGen) -> EnumerationState -> f EnumerationState +uvarCounter = lens _uvarCounter (\s c -> s{_uvarCounter = c}) + +-- | Lens-compatible accessor for representative UVar tracking. +uvarRepresentative :: (Functor f) => (UnionFind -> f UnionFind) -> EnumerationState -> f EnumerationState +uvarRepresentative = lens _uvarRepresentative (\s uf -> s{_uvarRepresentative = uf}) + +-- | Lens-compatible accessor for per-UVar enumeration values. +uvarValues :: (Functor f) => (Seq UVarValue -> f (Seq UVarValue)) -> EnumerationState -> f EnumerationState +uvarValues = lens _uvarValues (\s vals -> s{_uvarValues = vals}) + +{- | Lens for the oracle's pending prune checks. + +Pruning code uses this through helpers like 'getPruneDeps', 'addPruneDep', and +'deletePruneDep'. It is exported for lower-level oracles that need direct +access to the dependency map while composing their own enumeration actions. +-} +pruneDeps :: (Functor f) => (IntMap.IntMap [Term] -> f (IntMap.IntMap [Term])) -> EnumerationState -> f EnumerationState +pruneDeps = lens _pruneDeps (\s pds -> s{_pruneDeps = pds}) + +-- | Initial state whose root UVar contains the node being enumerated. +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)) + IntMap.empty + +--------------------------------------------------------------------------- +---------------------------- Enumeration monad ---------------------------- +--------------------------------------------------------------------------- + +--------------------- +-------- Monad +--------------------- + +-- | Nondeterministic enumeration state monad. +type EnumerateM = StateT EnumerationState [] + +-- | Run a lower-level enumeration action from an explicit state. +runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)] +runEnumerateM = runStateT + +-- Prune deps -- + +{- | Return all pending prune checks. + +This is mainly useful inside a pruning oracle. A caller can inspect the map +to decide whether it is currently resuming a suspended check or starting a +fresh one from the root fragment. +-} +getPruneDeps :: EnumerateM (IntMap.IntMap [Term]) +getPruneDeps = gets _pruneDeps + +{- | Return pending prune checks for a particular UVar id. + +The ids are the integer form of 'UVar's, via 'uvarToInt'. The enumerator uses +this after expanding a UVar to decide whether any previously suspended terms +should be checked against the new fragment. +-} +getPruneDepsOf :: Int -> EnumerateM (Maybe [Term]) +getPruneDepsOf uv = do + pd <- gets _pruneDeps + return (pd IntMap.!? uv) + +{- | Remember one term to check when the given UVar is expanded. + +Oracles use this when a prune test reaches an unexpanded 'TermFragmentUVar': +store the term that needs checking, return "not pruned" for now, and let the +pruned enumerator revisit the check after that UVar becomes concrete. +-} +addPruneDep :: Int -> Term -> EnumerateM () +addPruneDep uv rw = addPruneDeps uv [rw] + +addPruneDeps :: Int -> [Term] -> EnumerateM () +addPruneDeps uv rws = + modify' $ \s -> s{_pruneDeps = IntMap.insertWith (++) uv rws (_pruneDeps s)} + +{- | Clear pending prune checks for a UVar. + +The enumerator calls this when it resumes checks for an expanded UVar. Oracles +that consume entries from 'getPruneDeps' should delete them for the same +reason: each dependency is a one-shot request to recheck after expansion. +-} +deletePruneDep :: Int -> EnumerateM () +deletePruneDep uv = + modify' $ \s -> s{_pruneDeps = IntMap.delete uv (_pruneDeps s)} + +--------------------- +-------- UVar accessors +--------------------- + +nextUVar :: EnumerateM UVar +nextUVar = do + c <- gets _uvarCounter + let (c', uv) = UnionFind.nextUVar c + modify' $ \s -> s{_uvarCounter = c'} + return uv + +addUVarValue :: Maybe Node -> EnumerateM UVar +addUVarValue x = do + uv <- nextUVar + modify' $ \s -> s{_uvarValues = _uvarValues s :|> UVarUnenumerated x Sequence.Empty} + return uv + +-- | Return the current representative for a UVar, updating union-find state. +getUVarRepresentative :: UVar -> EnumerateM UVar +getUVarRepresentative uv = do + uf <- gets _uvarRepresentative + let (uv', uf') = UnionFind.find uv uf + modify' $ \s -> s{_uvarRepresentative = uf'} + return uv' + +-- | Look up the value for a UVar after path-compressing its representative. +getUVarValue :: UVar -> EnumerateM UVarValue +getUVarValue uv = do + uv' <- getUVarRepresentative uv + let idx = uvarToInt uv' + values <- gets _uvarValues + return $ Sequence.index values idx + +-- | Look up the fragment for an already-enumerated UVar. +getTermFragForUVar :: UVar -> EnumerateM TermFragment +getTermFragForUVar uv = termFragment <$> getUVarValue uv + +setUVarValue :: Int -> UVarValue -> EnumerateM () +setUVarValue idx val = + modify' $ \s -> s{_uvarValues = Sequence.update idx val (_uvarValues s)} + +modifyUVarValue :: Int -> (UVarValue -> UVarValue) -> EnumerateM () +modifyUVarValue idx f = do + values <- gets _uvarValues + setUVarValue idx (f (Sequence.index values idx)) + +--------------------- +-------- Creating UVar's +--------------------- + +pecToSuspendedConstraint :: PathEClass -> EnumerateM SuspendedConstraint +pecToSuspendedConstraint pec = do + uv <- addUVarValue Nothing + return $ SuspendedConstraint (getPathTrie pec) uv + +--------------------- +-------- Merging UVar's / nodes +--------------------- + +-- | Merge the source UVar into the target UVar, intersecting their constraints. +assimilateUvarVal :: UVar -> UVar -> EnumerateM () +assimilateUvarVal uvTarg uvSrc + | uvTarg == uvSrc = return () + | otherwise = do + values <- gets _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) + setUVarValue (uvarToInt uvTarg) v + setUVarValue (uvarToInt uvSrc) UVarEliminated + +-- | Intersect a node and inherited constraints into the value for a UVar. +mergeNodeIntoUVarVal :: UVar -> Node -> Seq SuspendedConstraint -> EnumerateM () +mergeNodeIntoUVarVal uv n scs = do + uv' <- getUVarRepresentative uv + let idx = uvarToInt uv' + modifyUVarValue idx (intersectUVarValue (UVarUnenumerated (Just n) scs)) + newValues <- gets _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 <- gets _uvarValues + + updated <- + traverse + ( \case + UVarUnenumerated n scs -> + UVarUnenumerated n + <$> mapM + ( \sc -> + SuspendedConstraint (scGetPathTrie sc) + <$> getUVarRepresentative (scGetUVar sc) + ) + scs + x -> return x + ) + values + + modify' $ \s -> s{_uvarValues = updated} + +--------------------- +-------- Core enumeration algorithm +--------------------- +-- + +-- | Enumerate one node under the suspended constraints currently in scope. +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 -> + modify' $ \s -> + s{_uvarRepresentative = UnionFind.union (scGetUVar x) (scGetUVar sc) (_uvarRepresentative s)} + uv <- getUVarRepresentative (scGetUVar x) + mapM_ (assimilateUvarVal uv) reps + + mergeNodeIntoUVarVal uv n descendantConstraints + return $ TermFragmentUVar uv + +-- | Enumerate one edge, introducing UVars for its equality classes. +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) <$> zipWithM (\i n -> enumerateNode (descendScs i scs') n) [0 ..] (edgeChildren e) + +--------------------- +-------- Enumeration-loop control +--------------------- + +-- | Result of looking for the next UVar that can be expanded. +data ExpandableUVarResult + = -- | Candidates exist, but all are blocked by suspended dependencies. + ExpansionStuck + | -- | Enumeration has no more UVar work to do. + ExpansionDone + | -- | The next unconstrained UVar to expand. + ExpansionNext !UVar + deriving (Show) + +-- Can speed this up with bitvectors + +findExpandableUVars :: EnumerateM (Maybe (IntMap.IntMap Bool)) +findExpandableUVars = do + values <- gets _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) False + (UVarUnenumerated (Just _) _) -> return $ IntMap.singleton (uvarToInt rep) False + _ -> return IntMap.empty + ) + [0 .. (Sequence.length values - 1)] + let candidates = IntMap.unions candidateMaps + + if IntMap.null candidates + then + return Nothing + else do + let ruledOut = + foldMap + ( \case + (UVarUnenumerated _ scs) -> + foldMap + (\sc -> IntMap.singleton (uvarToInt $ scGetUVar sc) True) + scs + _ -> IntMap.empty + ) + values + + let unconstrainedCandidateMap = IntMap.filter not (ruledOut <> candidates) + return (Just unconstrainedCandidateMap) + +-- | Find the next UVar that can be expanded without violating dependencies. +firstExpandableUVar :: EnumerateM ExpandableUVarResult +firstExpandableUVar = do + mb_unconstrainedCandidateMap <- findExpandableUVars + case mb_unconstrainedCandidateMap of + Nothing -> return ExpansionDone + Just unconstrainedCandidateMap -> + case IntMap.lookupMin unconstrainedCandidateMap of + Nothing -> return ExpansionStuck + Just (i, _) -> return $ ExpansionNext $ intToUVar i + +ruleMatches :: Bool -> TermFragment -> Term -> EnumerateM Bool +-- TODO: this should match types +ruleMatches _ _ (Term (Symbol "") _) = return True +ruleMatches + pruneSuspended + (TermFragmentNode "app" [_, _, tf_f, tf_v]) + (Term "app" [_, _, rw_f, rw_v]) = do + rw_f_m <- ruleMatches pruneSuspended tf_f rw_f + if not rw_f_m + then return False + else ruleMatches pruneSuspended tf_v rw_v +ruleMatches + _ + (TermFragmentNode ts [_]) + (Term rws [_]) = return (ts == rws) +ruleMatches pruneSuspended (TermFragmentUVar uv) rw = + do + val <- getUVarValue uv + case val of + UVarEnumerated t -> ruleMatches pruneSuspended t rw + _ -> return False +ruleMatches _ _ _ = return False + +{- | Test whether a partially enumerated fragment represents any given term. + +This is the helper a pruning oracle uses after receiving a @Left +TermFragment@ callback from 'getAllTermsPrune'. It understands the +Spectacular template shape used by the pruning code: @filter@ unwraps to its +body, @app@ compares the function and value positions, unary symbols compare +by symbol, and the term symbol @""@ is treated as a wildcard. + +The Boolean argument marks checks that are allowed to suspend on unexpanded +UVars. The current matcher only follows already-enumerated UVars; callers that +need explicit suspension can pair this with 'addPruneDep'. +-} +fragRepresents :: Bool -> TermFragment -> [Term] -> EnumerateM Bool +fragRepresents pruneSuspended (TermFragmentNode "filter" [_, t]) rwrs = fragRepresents pruneSuspended t rwrs +fragRepresents pruneSuspended tf@(TermFragmentNode "app" [_, _, f, v]) rwrs = do + tfMatches <- filterM (ruleMatches pruneSuspended tf) rwrs + if not (null tfMatches) + then return True + else do + r <- or <$> mapM (flip (fragRepresents False) rwrs) [f, v] + return r +fragRepresents pruneSuspended tf@(TermFragmentNode _ [_]) rwrs = + not . null <$> filterM (ruleMatches pruneSuspended tf) rwrs +fragRepresents pruneSuspended tf@(TermFragmentUVar uv) rwrs = + do + uvMatches <- filterM (ruleMatches pruneSuspended tf) rwrs + if not (null uvMatches) + then return True + else do + val <- getUVarValue uv + case val of + UVarEnumerated t -> fragRepresents pruneSuspended t rwrs + _ -> return False +fragRepresents _ tf _ = error $ "unrecognized frag! " ++ show tf + +-- | Expand one UVar, then update prune dependencies and referenced UVars. +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 + + setUVarValue (uvarToInt uv') (UVarEnumerated t) + pd <- getPruneDepsOf (uvarToInt uv) + case pd of + Just rws -> do + deletePruneDep (uvarToInt uv) + res <- fragRepresents True t rws + if res + then mzero + else return t + _ -> refreshReferencedUVars >> return t + +-- | Expand the next available UVar, failing when enumeration is done or stuck. +enumerateOutFirstExpandableUVar :: EnumerateM () +enumerateOutFirstExpandableUVar = do + muv <- firstExpandableUVar + case muv of + ExpansionNext uv -> void $ enumerateOutUVar uv + ExpansionDone -> mzero + ExpansionStuck -> mzero + +-- | Expand the root UVar until it represents a complete term. +enumerateFully :: EnumerateM () +enumerateFully = const () <$> enumerateFully' () False (\x _ _ -> return (False, x)) + +{- | Enumerate until the root term is complete, with optional oracle pruning. + +The oracle is called twice around each expandable UVar: + +* @Right node@ is passed before expanding the node, so callers can drop a + whole branch early when the current ECTA already represents a forbidden + template. +* @Left fragment@ is passed after expansion, so callers can reject the + concrete fragment or update their oracle state before enumeration + continues. + +The threaded state parameter belongs to the caller. Returning @True@ prunes +the current nondeterministic branch; returning @False@ keeps it. When +@usePruneHints@ is enabled, UVar ids in 'pruneDeps' are expanded first so +suspended checks resume promptly. +-} +enumerateFully' :: + forall a. + a -> + Bool -> + (a -> UVar -> Either TermFragment Node -> EnumerateM (Bool, a)) -> + EnumerateM Bool +enumerateFully' ost usePruneHints oracle = do + muv <- + if usePruneHints + then do + hints <- IntMap.keysSet <$> getPruneDeps + if IntSet.null hints + -- if we aren't targeting any terms, just expand the first one + then {-# SCC "no-hints" #-} firstExpandableUVar + else do + expandable <- findExpandableUVars + case expandable of + Nothing -> return ExpansionDone + Just ucm | IntMap.null ucm -> return ExpansionStuck + Just ucm -> + let expSet = IntMap.keysSet ucm + inters = IntSet.intersection expSet hints + in if not (IntSet.null inters) + then + return $ + ExpansionNext $ + intToUVar (IntSet.findMax inters) + else firstExpandableUVar + else firstExpandableUVar + case muv of + ExpansionStuck -> mzero + ExpansionDone -> return True + ExpansionNext uv -> + let continue ost' = do + tf <- enumerateOutUVar uv + (should_prune, ost'') <- oracle ost' uv (Left tf) + if should_prune + then mzero + else enumerateFully' ost'' usePruneHints oracle + in do + UVarUnenumerated (Just n) scs <- getUVarValue uv + case n of + Mu _ | scs == Sequence.empty -> return True + _ -> do + (should_prune, ost') <- oracle ost uv (Right n) + if should_prune then mzero else continue ost' + +--------------------- +-------- Expanding an enumerated term fragment into a term +--------------------- + +{- | Expand a fragment even if it still contains unenumerated UVars. + +Unlike 'expandTermFrag', this is safe for diagnostics and oracle logging while +enumeration is still in progress. Unexpanded non-recursive UVars become +placeholders named @@, where @N@ is the UVar id; recursive holes become +@Mu@. +-} +expandPartialTermFrag :: TermFragment -> EnumerateM Term +expandPartialTermFrag (TermFragmentNode s ts) = Term s <$> mapM expandPartialTermFrag ts +expandPartialTermFrag (TermFragmentUVar uv) = + do + val <- getUVarValue uv + case val of + UVarEnumerated t -> expandPartialTermFrag t + UVarUnenumerated (Just (Mu _)) _ -> return $ Term "Mu" [] + _ -> return $ Term (Symbol $ " pretty (uvarToInt uv) <> ">") [] + +-- | Expand a complete term fragment into a concrete 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" + +-- | Expand an already-enumerated UVar into a concrete term. +expandUVar :: UVar -> EnumerateM Term +expandUVar uv = do + UVarEnumerated t <- getUVarValue uv + expandTermFrag t + +--------------------- +-------- Full enumeration +--------------------- + +-- | Enumerate terms, replacing recursive holes with a truncation marker. +getAllTruncatedTerms :: Node -> [Term] +getAllTruncatedTerms n = map (termFragToTruncatedTerm . fst) $ + flip runEnumerateM (initEnumerationState n) $ do + enumerateFully + getTermFragForUVar (intToUVar 0) + +{- | Enumerate terms while letting an oracle prune branches. + +This is the public entry point for pruning-aware enumeration. The oracle has +type: + +@ +state -> UVar -> Either TermFragment Node -> EnumerateM (Bool, state) +@ + +It receives the caller state, the UVar being considered, and either the node +about to be expanded (@Right@) or the fragment just produced (@Left@). Return +@True@ to discard that branch, or @False@ with updated state to keep +enumerating. A typical Spectacular-style oracle uses @Right node@ with +'nodeRepresentsTemplate' to reject whole ECTA branches, and @Left fragment@ +with 'fragRepresents' to reject terms that match known rewrites/templates. +-} +getAllTermsPrune :: + forall a. + a -> + (a -> UVar -> Either TermFragment Node -> EnumerateM (Bool, a)) -> + Node -> + [Term] +getAllTermsPrune ost oracle n = + map fst $ flip runEnumerateM (initEnumerationState n) $ enumPrune ost oracle + +{- | Monadic form of 'getAllTermsPrune'. + +Use this when the caller is already composing lower-level enumeration actions +in 'EnumerateM'. Most callers should prefer 'getAllTermsPrune'. +-} +enumPrune :: forall a. a -> (a -> UVar -> Either TermFragment Node -> EnumerateM (Bool, a)) -> EnumerateM Term +enumPrune a oracle = do + finished <- enumerateFully' a True oracle + if finished then expandUVar (intToUVar 0) else mzero + +-- | Enumerate all complete terms represented by an ECTA. +getAllTerms :: Node -> [Term] +getAllTerms = getAllTermsPrune () (\_ _ _ -> return (False, ())) diff --git a/src/Data/ECTA/Internal/ECTA/Operations.hs b/src/Data/ECTA/Internal/ECTA/Operations.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Internal/ECTA/Operations.hs @@ -0,0 +1,708 @@ +{-# LANGUAGE OverloadedStrings #-} +-- For the 'Pathable' instance for 'Node' +{-# OPTIONS_GHC -Wno-orphans #-} + +{- | Core ECTA operations. + +This module contains traversal, intersection, union, reduction, and +constraint-propagation logic. Most users should import "Data.ECTA" instead; the +module is exposed so downstream code can reach lower-level helpers when needed. +-} +module Data.ECTA.Internal.ECTA.Operations ( + -- * Traversal + nodeMapChildren, + pathsMatching, + mapNodes, + crush, + onNormalNodes, + + -- * Unfolding + unfoldOuterRec, + refold, + nodeEdges, + unfoldBounded, + + -- * Size operations + nodeCount, + edgeCount, + maxIndegree, + + -- * Union + union, + + -- * Membership + nodeRepresents, + edgeRepresents, + + -- * Membership of templates + nodeRepresentsTemplate, + edgeRepresentsTemplate, + + -- * Intersection + intersect, + dropRedundantEdges, + intersectEdge, + + -- * Path operations + requirePath, + requirePathList, + + -- * Reduction + withoutRedundantEdges, + reducePartially, + reduceEdgeIntersection, + reduceEqConstraints, + + -- * Debugging + getSubnodeById, +) where + +import Control.Monad.State.Strict (MonadState (..), State, evalState, modify') +import qualified Data.HashMap.Strict as HashMap +import Data.Hashable (Hashable (..), hash) +import Data.List (inits, tails) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe (mapMaybe) +import Data.Monoid (First (..), Sum (..)) +import Data.Semigroup (Max (..)) +import Data.Set (Set) +import qualified Data.Set as Set + +import Data.ECTA.Internal.ECTA.Type +import Data.ECTA.Internal.Paths +import Data.ECTA.Internal.Term + +import Data.Interned.Extended.HashTableBased (Id) + +import Data.Memoization (MemoCacheTag (..), memo, memo2) +import Utility.Fixpoint +import Utility.HashJoin + +------------------------------------------------------------------------------------ + +mapWithIndex :: (Int -> a -> b) -> [a] -> [b] +mapWithIndex f = zipWith f [0 ..] + +atMay :: Int -> [a] -> Maybe a +atMay i xs + | i < 0 = Nothing + | otherwise = case drop i xs of + x : _ -> Just x + [] -> Nothing + +adjustAt :: Int -> (a -> a) -> [a] -> [a] +adjustAt i f xs + | i < 0 = xs + | otherwise = case splitAt i xs of + (prefix, x : suffix) -> prefix ++ f x : suffix + _ -> xs + +----------------------- +------ Traversal +----------------------- + +{- | Apply an edge transformation to the outgoing alternatives of a node. + +This is a shallow operation: for a normal @Node@ it maps over that node's +edges, and for a 'Mu' it first unfolds the outer recursion and then maps those +edges. It does not recursively traverse child nodes. Spectacular uses this +shape to push environment/equality-constraint edits across every immediate +alternative of an ECTA node without changing the node's children directly. +-} +nodeMapChildren :: (Edge -> Edge) -> Node -> Node +nodeMapChildren _ EmptyNode = EmptyNode +nodeMapChildren f n@(Mu _) = nodeMapChildren f (unfoldOuterRec n) +nodeMapChildren f (Node es) = Node (map f es) +nodeMapChildren _ (Rec _) = error "nodeMapChildren: unexpected Rec" + +{- | 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 $ mapWithIndex (\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 + +{- | Fold over all reachable nodes with sharing awareness. + +This name originates from the @crush@ operator in the Stratego language. +Although @m@ is only constrained to be a monoid, this function makes no +guarantees about traversal order. +-} +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)) + +-- | Run a fold function only on normal non-recursive nodes. +onNormalNodes :: (Monoid m) => (Node -> m) -> (Node -> m) +onNormalNodes f n@(Node _) = f n +onNormalNodes _ _ = mempty + +----------------------- +------ Folding +----------------------- + +-- | Unfold one outer 'Mu' layer. +unfoldOuterRec :: Node -> Node +unfoldOuterRec n@(Mu x) = x n +unfoldOuterRec _ = error "unfoldOuterRec: Must be called on a Mu node" + +-- | Outgoing alternatives of a node, unfolding one outer 'Mu' if needed. +nodeEdges :: Node -> [Edge] +nodeEdges (Node es) = es +nodeEdges n@(Mu _) = nodeEdges (unfoldOuterRec n) +nodeEdges _ = [] + +-- | Replace repeated unfoldings with recursive 'Mu' nodes where possible. +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 + +-- | Unfold recursive nodes at most the given number of rounds. +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 +------------ + +-- | Count reachable non-recursive nodes, sharing-aware. +nodeCount :: Node -> Int +nodeCount = getSum . crush (onNormalNodes $ const $ Sum 1) + +-- | Count reachable outgoing edges, sharing-aware. +edgeCount :: Node -> Int +edgeCount = getSum . crush (onNormalNodes go) + where + go (Node es) = Sum (length es) + go _ = mempty + +-- | Maximum number of outgoing alternatives on any reachable normal node. +maxIndegree :: Node -> Int +maxIndegree = getMax . crush (onNormalNodes go) + where + go (Node es) = Max (length es) + go _ = mempty + +------------ +------ Membership +------------ + +-- | Test whether a node accepts a concrete term. +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 + +-- | Test whether an edge accepts a concrete term. +edgeRepresents :: Edge -> Term -> Bool +edgeRepresents e = \t@(Term s ts) -> + s == edgeSymbol e + && childrenRepresent (edgeChildren e) ts + && all (eclassSatisfied t) (unsafeGetEclasses $ edgeEcs e) + where + childrenRepresent [] [] = True + childrenRepresent (n : ns) (t : ts) = nodeRepresents n t && childrenRepresent ns ts + childrenRepresent _ _ = False + + 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 #-} + +{- | Test whether a node can represent a template term. + +This is the pruning-oriented variant of 'nodeRepresents', not a concrete +membership predicate. It delegates to 'edgeRepresentsTemplate', whose template +language treats the exact symbol @""@ as a wildcard for the edge symbol and +checks only the template children that are present. Pruning oracles use this +before expanding a UVar: if the current node already represents a forbidden +rewrite/template, the whole branch can be dropped without enumerating a full +term. +-} +nodeRepresentsTemplate :: Node -> Term -> Bool +nodeRepresentsTemplate EmptyNode _ = False +nodeRepresentsTemplate (Node es) t = any (`edgeRepresentsTemplate` t) es +nodeRepresentsTemplate n@(Mu _) t = nodeRepresentsTemplate (unfoldOuterRec n) t +nodeRepresentsTemplate _ _ = False + +{- | Test whether one edge can represent a template term. + +The term matches normally when its symbol is the edge symbol. It also matches +when the term symbol is exactly @""@, in which case the symbol is treated +as a wildcard. This is a prefix-style matcher: supplied template children must +match, but omitted template children are unresolved holes. +-} +edgeRepresentsTemplate :: Edge -> Term -> Bool +edgeRepresentsTemplate e = \t@(Term s@(Symbol txt) ts) -> + let childrenSatisfied = and (zipWith nodeRepresentsTemplate (edgeChildren e) ts) + consSatisfied = all (eclassSatisfied t) (unsafeGetEclasses $ edgeEcs e) + in (s == edgeSymbol e && childrenSatisfied && consSatisfied) + || (txt == "" && childrenSatisfied && consSatisfied) + 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 +------------ + +{-# NOINLINE intersect #-} + +data RuleOutRes = Keep | RuledOutBy Edge + +-- | Remove edges that are subsumed by another edge with the same symbol. +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) + +-- | Intersect two edges when they have the same symbol. +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 + go e1 e2 = + mkEdge + (edgeSymbol e1) + (zipWith intersect (edgeChildren e1) (edgeChildren e2)) + (edgeEcs e1 `combineEqConstraints` edgeEcs e2) +{-# NOINLINE intersectEdgeSameSymbol #-} + +------------ +------ New intersection +------------ + +-- | Intersection of two ECTAs. +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 + { idFree :: Map Id Node + -- ^ Value of all free variables inside the term (so that we can unfold when necessary) + , idRecInt :: Set IntersectId + -- ^ Intersection problems we encountered previously (to avoid infinite unrolling) + } + 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) -> 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 a list of ECTAs by concatenating their alternatives. +union :: [Node] -> Node +union ns = case foldr collect (False, []) ns of + (False, _) -> EmptyNode + (_, es) -> Node es + where + collect EmptyNode acc = acc + collect n (_, es) = (True, nodeEdges n ++ es) + +unionMapMaybe :: (a -> Maybe Node) -> [a] -> Node +unionMapMaybe f xs = case foldr collect (False, []) xs of + (False, _) -> EmptyNode + (_, es) -> Node es + where + collect x acc = case f x of + Nothing -> acc + Just EmptyNode -> acc + Just n -> (True, nodeEdges n ++ snd acc) + +---------------------- +------ Path operations +---------------------- + +-- | Restrict an ECTA to terms that contain the given path. +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" + +-- | Variant of 'requirePath' for a child list. +requirePathList :: Path -> [Node] -> [Node] +requirePathList EmptyPath ns = ns +requirePathList (ConsPath p ps) ns = adjustAt p (requirePath ps) ns + +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) = unionMapMaybe goEdge es + where + goEdge :: Edge -> Maybe Node + goEdge (Edge _ ns) = getPath ps <$> atMay p ns + 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) (mapMaybe goEdge es) + where + goEdge :: Edge -> Maybe Node + goEdge (Edge _ ns) = atMay p ns + 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 (adjustAt p (modifyAtPath f ps) (edgeChildren e)) + 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 atMay p ns of + Nothing -> EmptyNode + Just n -> getPath ps n + + getAllAtPath EmptyPath _ = [] + getAllAtPath (ConsPath p ps) ns = case atMay p ns of + Nothing -> [] + Just n -> getAllAtPath ps n + + modifyAtPath _ EmptyPath ns = ns + modifyAtPath f (ConsPath p ps) ns = adjustAt p (modifyAtPath f ps) ns + +------------------------------------ +------ Reduction +------------------------------------ + +-- | Remove alternatives represented by another alternative in the same node. +withoutRedundantEdges :: Node -> Node +withoutRedundantEdges n = mapNodes dropReds n + where + dropReds (Node es) = Node (dropRedundantEdges es) + dropReds x = x + +--------------- +--- Reducing Equality Constraints +--------------- + +-- | Propagate equality constraints through one reduction pass. +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 every recursive cycle. + reduceWithInheritedEcs :: EqConstraints -> [Node] -> [Node] + reduceWithInheritedEcs EqContradiction children = map (const EmptyNode) children + reduceWithInheritedEcs inheritedEcs children = zipWith (\i -> reducePartially' (eqConstraintsDescend inheritedEcs i)) [0 ..] children +{-# NOINLINE reducePartially' #-} + +-- | Reduce an edge's children using inherited constraints from ancestors. +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 #-} + +-- | Apply local and inherited equality constraints to a child list. +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 EmptyConstraints EmptyConstraints origNs = origNs + 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 [] = EmptyNode + intersectList (n : ns) = foldr intersect n ns + + 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 [p1, p2] = [getPath p2 ns, getPath p1 ns] + 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) (drop 1 $ tails xs) + +--------------- +--- Debugging +--------------- + +-- | Find a reachable node by interned node id. +getSubnodeById :: Node -> Id -> Maybe Node +getSubnodeById n i = getFirst $ crush (onNormalNodes $ \x -> if nodeIdentity x == i then First (Just x) else First Nothing) n diff --git a/src/Data/ECTA/Internal/ECTA/Type.hs b/src/Data/ECTA/Internal/ECTA/Type.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Internal/ECTA/Type.hs @@ -0,0 +1,691 @@ +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | Interned node and edge representation for the ECTA core. +module Data.ECTA.Internal.ECTA.Type ( + RecNodeId (..), + Edge (.., Edge), + -- | Cache key for an uninterned edge. + pattern DEdge, + UninternedEdge (..), + mkEdge, + emptyEdge, + edgeChildren, + edgeEcs, + edgeSymbol, + setChildren, + Node (.., Node, Mu), + -- | Cache key for an uninterned node. + pattern DNode, + InternedNode (..), + InternedMu (..), + UninternedNode (..), + -- | Opaque identifier for recursive nodes created during intersection. + IntersectId, + pattern IntersectId, + nodeIdentity, + numNestedMu, + substFree, + freeVars, + modifyNode, + createMu, + shape, + matchMu, +) where + +import Data.Function (on) +import Data.Hashable (Hashable (..)) +import Data.List (sort) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import qualified Data.Set as Set + +import System.IO.Unsafe (unsafePerformIO) + +import Data.Interned.Extended.HashTableBased + +import Data.ECTA.Internal.Paths +import Data.ECTA.Internal.Term + +import Data.Memoization + +--------------------------------------------------------------------------------------------- + +----------------------------------------------------------------- +-------------------------- Mu node table ------------------------ +----------------------------------------------------------------- + +-- | Internal identifier for references to recursive ECTA nodes. +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) + +{- | 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. +-} + +-- | Pair of node identities naming the recursive node introduced by intersection. +data IntersectId + = -- Invariant: the two 'Id's should be ordered (guaranteed by the pattern synonym constructor) + UnsafeIntersectId !Id !Id + deriving (Eq, Ord, Show) + +-- | Smart pattern that stores the two ids in canonical order. +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 where + hashWithSalt salt (RecInt nodeId) = + salt `hashWithSalt` (0 :: Int) `hashWithSalt` nodeId + hashWithSalt salt (RecUnint nodeId) = + salt `hashWithSalt` (1 :: Int) `hashWithSalt` nodeId + hashWithSalt salt RecDepth = + salt `hashWithSalt` (2 :: Int) + hashWithSalt salt (RecIntersect intersectionId) = + salt `hashWithSalt` (3 :: Int) `hashWithSalt` intersectionId + +instance Hashable IntersectId where + hashWithSalt salt (UnsafeIntersectId left right) = + salt `hashWithSalt` left `hashWithSalt` right + +----------------------------------------------------------------- +----------------------------- Edges ----------------------------- +----------------------------------------------------------------- + +-- | One outgoing alternative of an ECTA node. +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) + +-- | Symbol at the root of terms accepted through this edge. +edgeSymbol :: Edge -> Symbol +edgeSymbol = uEdgeSymbol . uninternedEdge + +-- | Child automata for this edge. +edgeChildren :: Edge -> [Node] +edgeChildren = uEdgeChildren . uninternedEdge + +-- | Equality constraints over paths into 'edgeChildren'. +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 ---------------------------- +----------------------------------------------------------------- + +-- | Interned recursive node payload. +data InternedMu = MkInternedMu + { internedMuId :: {-# UNPACK #-} !Id + -- ^ 'Id' of the node itself + , internedMuBody :: !Node + {- ^ The body of the 'Mu' + + Recursive occurrences to this node should be + + > Rec (RecNodeId internedMuId) + -} + , internedMuShape :: !Node + {- ^ The body of the 'Mu', before it was assigned an 'Id' + + Invariant: + + > substFree internedMuId (Rec (RecUnint (numNestedMu internedMuBody)) internedMuBody + > == internedMuShape + -} + } + deriving (Show) + +-- | Interned non-recursive node payload. +data InternedNode = MkInternedNode + { internedNodeId :: {-# UNPACK #-} !Id + -- ^ The 'Id' of the node itself + , internedNodeEdges :: ![Edge] + -- ^ All outgoing edges + , internedNodeNumNestedMu :: !Int + -- ^ Maximum Mu nesting depth in the term + , internedNodeFree :: !(Set RecNodeId) + -- ^ Free variables in the term + } + deriving (Show) + +-- | ECTA node. +data Node + = -- | Interned node with one or more outgoing alternatives. + InternedNode {-# UNPACK #-} !InternedNode + | -- | Empty language. + EmptyNode + | -- | Interned recursive node. + InternedMu {-# UNPACK #-} !InternedMu + | -- | Recursive reference used inside a 'Mu'. + 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 +---------------------- + +-- | Stable interned identity for non-empty, interned nodes. +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 + +-- | Replace an edge's children while preserving its symbol and constraints. +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 ----------------------- +----------------------------------------------------------------- + +-- | Non-canonical node description used before hash-consing. +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) + + 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) where + hashWithSalt salt (DNode node) = salt `hashWithSalt` 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 ------------------------ +----------------------------------------------------------------- + +-- | Edge payload before interning. +data UninternedEdge = UninternedEdge + { uEdgeSymbol :: !Symbol + , uEdgeChildren :: ![Node] + , uEdgeEcs :: !EqConstraints + } + deriving (Eq, Show) + +instance Hashable UninternedEdge where + hashWithSalt salt (UninternedEdge symbol children ecs) = + salt `hashWithSalt` symbol `hashWithSalt` children `hashWithSalt` ecs + +instance Interned Edge where + type Uninterned Edge = UninternedEdge + data Description Edge = DEdge {-# UNPACK #-} !UninternedEdge + deriving (Eq) + + describe = DEdge + + identify i e = InternedEdge i e + + cache = edgeCache + +instance Hashable (Description Edge) where + hashWithSalt salt (DEdge edge) = salt `hashWithSalt` edge + +edgeCache :: Cache Edge +edgeCache = unsafePerformIO freshCache +{-# NOINLINE edgeCache #-} + +----------------------------------------------------------------- +----------------------- Smart constructors ---------------------- +----------------------------------------------------------------- + +------------------- +------ Edge constructors +------------------- + +-- | Build or match an unconstrained edge. +pattern Edge :: Symbol -> [Node] -> Edge +pattern Edge s ns <- (InternedEdge _ (UninternedEdge s ns _)) + where + Edge s ns = intern $ UninternedEdge s ns EmptyConstraints + +{-# COMPLETE Edge #-} + +-- | Edge that is guaranteed to be removed when a node is built. +emptyEdge :: Edge +emptyEdge = Edge "" [EmptyNode] + +isEmptyEdge :: Edge -> Bool +isEmptyEdge (Edge _ ns) = any (== EmptyNode) ns + +removeEmptyEdges :: [Edge] -> [Edge] +removeEmptyEdges = filter (not . isEmptyEdge) + +-- | Build an edge with equality constraints. +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 #-} + +-- | Build or match a non-empty node from outgoing alternatives. +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 $ Set.toList $ Set.fromList 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 diff --git a/src/Data/ECTA/Internal/Paths.hs b/src/Data/ECTA/Internal/Paths.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Internal/Paths.hs @@ -0,0 +1,570 @@ +{-# 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, + 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 (groupBy, isSubsequenceOf, nub, sort, sortBy) +import qualified Data.List as List +import Data.Maybe (mapMaybe) +import qualified Data.Text as Text + +import Data.Equivalence.Monad (classes, desc, equate, runEquivM) + +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 -------------------------------- +----------------------------------------------------------------------- + +-- | Path into an edge's children, represented as child indexes. +data Path = Path ![Int] + deriving (Eq, Ord, Show) + +-- | Extract the raw child-index list from a @Path@. +unPath :: Path -> [Int] +unPath (Path p) = p + +instance Hashable Path where + hashWithSalt salt (Path components) = salt `hashWithSalt` components + +-- | Build a @Path@ from child indexes. +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) + +-- | First path component. Unsafe on 'EmptyPath'. +pathHeadUnsafe :: Path -> Int +pathHeadUnsafe EmptyPath = error "pathHeadUnsafe: empty path" +pathHeadUnsafe (ConsPath p _) = p + +-- | Path without its first component. Unsafe on 'EmptyPath'. +pathTailUnsafe :: Path -> Path +pathTailUnsafe EmptyPath = error "pathTailUnsafe: empty path" +pathTailUnsafe (ConsPath _ ps) = ps + +instance Pretty Path where + pretty (Path ps) = Text.intercalate "." (map (Text.pack . show) ps) + +-- | Whether the first path is a prefix of the second path. +isSubpath :: Path -> Path -> Bool +isSubpath EmptyPath _ = True +isSubpath (ConsPath p1 ps1) (ConsPath p2 ps2) + | p1 == p2 = isSubpath ps1 ps2 +isSubpath _ _ = False + +-- | Whether the first path is a strict prefix of the second path. +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 --------------------------------- +-------------------------------------------------------------------------- + +-- | Things that can be inspected or edited by child-index paths. +class Pathable t t' | t -> t' where + -- | Result type used when a path is absent. + type Emptyable t' + + -- | Read the value at a path, returning the empty value when absent. + getPath :: Path -> t -> Emptyable t' + + -- | Read all values reachable at a path. + getAllAtPath :: Path -> t -> [t'] + + -- | Apply a local edit at a path. + modifyAtPath :: (t' -> t') -> Path -> t -> t + +----------------------------------------------------------------------- +---------------------------- Path tries ------------------------------- +----------------------------------------------------------------------- + +-- | Largest child index present in a trie node, if any. +getMaxNonemptyIndex :: PathTrie -> Maybe Int +getMaxNonemptyIndex EmptyPathTrie = Nothing +getMaxNonemptyIndex TerminalPathTrie = Nothing +getMaxNonemptyIndex (PathTrieSingleChild i _) = Just i +getMaxNonemptyIndex (PathTrie children) = Just $ fst (last children) + +--------------------- +------- Path tries +--------------------- + +{- | Trie of paths used to index equality constraints. + +Most constraint tries in the original workloads are either empty, terminal, or +one path component wide for many levels. `PathTrieSingleChild` keeps that hot +case compact. The multi-child case used to be a dense child table, which made +lookup cheap but forced GHC to optimise large recursive structure code. The +sparse representation keeps only non-empty children in sorted order. That +keeps union, ordering, and subsumption as linear merges over present children, +while avoiding the `-O2` compile-time memory blow-up from the dense code. + +Invariant for @PathTrie@: children are sorted by component, contain no +@EmptyPathTrie@ entries, and contain at least two children. Constructors are +exported for tests and compatibility, so functions that rebuild multi-child +tries should restore that invariant before returning. +-} +data PathTrie + = -- | No paths. + EmptyPathTrie + | -- | Exactly the empty path. + TerminalPathTrie + | -- | A compact node with exactly one child at the given path component. + PathTrieSingleChild {-# UNPACK #-} !Int !PathTrie + | -- | Sparse multi-child node. See the invariant on @PathTrie@. + PathTrie ![(Int, PathTrie)] + deriving (Eq, Show) + +instance Hashable PathTrie where + hashWithSalt salt EmptyPathTrie = salt `hashWithSalt` (0 :: Int) + hashWithSalt salt TerminalPathTrie = salt `hashWithSalt` (1 :: Int) + hashWithSalt salt (PathTrieSingleChild i pt) = + salt `hashWithSalt` (2 :: Int) `hashWithSalt` i `hashWithSalt` pt + hashWithSalt salt (PathTrie children) = + List.foldl' hashWithSalt (salt `hashWithSalt` (3 :: Int)) children + +-- | Check for the trie containing no paths. +isEmptyPathTrie :: PathTrie -> Bool +isEmptyPathTrie EmptyPathTrie = True +isEmptyPathTrie _ = False + +-- | Check for the trie containing exactly the empty path. +isTerminalPathTrie :: PathTrie -> Bool +isTerminalPathTrie TerminalPathTrie = True +isTerminalPathTrie _ = False + +-- | Whether a trie contains at least two distinct paths. +pathTrieHasAtLeastTwoPaths :: PathTrie -> Bool +pathTrieHasAtLeastTwoPaths = go False + where + go :: Bool -> PathTrie -> Bool + go _ EmptyPathTrie = False + go seenOne TerminalPathTrie = seenOne + go seenOne (PathTrieSingleChild _ pt) = go seenOne pt + go seenOne (PathTrie children) = goChildren seenOne children + + goChildren :: Bool -> [(Int, PathTrie)] -> Bool + goChildren _ [] = False + goChildren seenOne ((_, pt) : rest) + | go seenOne pt = True + | pathTrieHasAnyPath pt = + if seenOne + then True + else goChildren True rest + | otherwise = goChildren seenOne rest + + pathTrieHasAnyPath :: PathTrie -> Bool + pathTrieHasAnyPath EmptyPathTrie = False + pathTrieHasAnyPath TerminalPathTrie = True + pathTrieHasAnyPath (PathTrieSingleChild _ pt) = pathTrieHasAnyPath pt + pathTrieHasAnyPath (PathTrie children) = any (pathTrieHasAnyPath . snd) children + +-- | Compare sparse child lists as if they were dense vectors with empty cells. +comparePathTrieChildren :: [(Int, PathTrie)] -> [(Int, PathTrie)] -> Ordering +comparePathTrieChildren [] [] = EQ +comparePathTrieChildren [] _ = LT +comparePathTrieChildren _ [] = GT +comparePathTrieChildren ((i1, pt1) : rest1) ((i2, pt2) : rest2) = + case compare i1 i2 of + LT -> LT + GT -> GT + EQ -> case compare pt1 pt2 of + EQ -> comparePathTrieChildren rest1 rest2 + res -> res + +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 ((i2, pt2) : _)) = + case compare i1 i2 of + LT -> LT + GT -> GT + EQ -> case compare pt1 pt2 of + LT -> LT + GT -> GT + EQ -> LT -- children2 must have a second nonempty + compare (PathTrieSingleChild _ _) (PathTrie []) = + error "compare: invalid empty PathTrie children" + compare a@(PathTrie _) b@(PathTrieSingleChild _ _) = flipOrdering $ compare b a + compare (PathTrie children1) (PathTrie children2) = comparePathTrieChildren children1 children2 + +-- | Precondition: No path in the input is a subpath of another +toPathTrie :: [Path] -> PathTrie +toPathTrie [] = EmptyPathTrie +toPathTrie [EmptyPath] = TerminalPathTrie +toPathTrie ps@(firstPath : _) = + if all (\p -> pathHeadUnsafe p == pathHeadUnsafe firstPath) ps + then + PathTrieSingleChild (pathHeadUnsafe firstPath) (toPathTrie $ map pathTailUnsafe ps) + else + PathTrie children + where + groups = + groupBy ((==) `on` pathHeadUnsafe) $ + sortBy (compare `on` pathHeadUnsafe) ps + + children = + [ (pathHeadUnsafe groupHead, toPathTrie $ map pathTailUnsafe group) + | group@(groupHead : _) <- groups + ] + +-- | Convert a trie back to its sorted path list. +fromPathTrie :: PathTrie -> [Path] +fromPathTrie EmptyPathTrie = [] +fromPathTrie TerminalPathTrie = [EmptyPath] +fromPathTrie (PathTrieSingleChild i pt) = map (ConsPath i) $ fromPathTrie pt +fromPathTrie (PathTrie children) = + concatMap (\(i, pt) -> map (ConsPath i) $ fromPathTrie pt) children + +-- | Descend through one child index, returning 'EmptyPathTrie' if absent. +pathTrieDescend :: PathTrie -> Int -> PathTrie +pathTrieDescend EmptyPathTrie _ = EmptyPathTrie +pathTrieDescend TerminalPathTrie _ = EmptyPathTrie +pathTrieDescend (PathTrie children) i = + case lookup i children of + Nothing -> EmptyPathTrie + Just pt -> pt +pathTrieDescend (PathTrieSingleChild j pt') i + | i == j = pt' + | otherwise = EmptyPathTrie + +-------------------------------------------------------------------------- +---------------------- Equality constraints over paths ------------------- +-------------------------------------------------------------------------- + +--------------------------- +---------- Path E-classes +--------------------------- + +{- | Equality class of paths. + +The trie drives subsumption and descent; the path list keeps the older public +API and reduction code cheap to read. Values built by @PathEClass@ and +@mkPathEClassFromPathTrie@ keep the two views consistent. +-} +data PathEClass = PathEClass' + { getPathTrie :: !PathTrie + , getOrigPaths :: [Path] + } + deriving (Show) + +instance Eq PathEClass where + (==) = (==) `on` getPathTrie + +instance Ord PathEClass where + compare = compare `on` getPathTrie + +-- | Build or match an equality class from its sorted path list view. +pattern PathEClass :: [Path] -> PathEClass +pattern PathEClass ps <- PathEClass' _ ps + where + PathEClass ps = PathEClass' (toPathTrie $ nub ps) (sort $ nub ps) + +-- | Extract the paths in an equality class. +unPathEClass :: PathEClass -> [Path] +unPathEClass (PathEClass' _ paths) = paths + +instance Pretty PathEClass where + pretty pec = "{" <> (Text.intercalate "=" $ map pretty $ unPathEClass pec) <> "}" + +instance Hashable PathEClass where + hashWithSalt salt = hashWithSalt salt . getPathTrie + +-- | Build an equality class from a trie, deriving the path list lazily. +mkPathEClassFromPathTrie :: PathTrie -> PathEClass +mkPathEClassFromPathTrie pt = PathEClass' pt (fromPathTrie pt) + +-- | Whether one path in the first class strictly subsumes one path in the second. +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 children2) = case lookup i1 children2 of + Nothing -> False + Just pt2 -> go pt1 pt2 + go (PathTrie children1) (PathTrieSingleChild i2 pt2) = case lookup i2 children1 of + Nothing -> False + Just pt1 -> go pt1 pt2 + go (PathTrie children1) (PathTrie children2) = anyMatchingChild children1 children2 + + -- Both child lists are sorted, so this keeps the old dense-table behaviour + -- without scanning absent indexes or doing repeated linear lookups. + anyMatchingChild [] _ = False + anyMatchingChild _ [] = False + anyMatchingChild left@((i1, pt1) : rest1) right@((i2, pt2) : rest2) = + case compare i1 i2 of + LT -> anyMatchingChild rest1 right + GT -> anyMatchingChild left rest2 + EQ -> go pt1 pt2 || anyMatchingChild rest1 rest2 + +{- | Total ordering used when choosing constraint-propagation order. + +Strict subsumption comes first: if one equality class contains a path that is a +strict prefix of a path in another class, the shorter one must be processed +before the longer one. Incomparable classes use the reversed trie ordering. +That tie-break keeps term-search-shaped workloads in the old left-to-right +propagation order, which avoids extra reduction work in practice. +-} +completedSubsumptionOrdering :: PathEClass -> PathEClass -> Ordering +completedSubsumptionOrdering pec1 pec2 + | hasSubsumingMember pec1 pec2 = LT + | hasSubsumingMember pec2 pec1 = GT + | otherwise = compare pec2 pec1 + +-------------------------------- +---------- Equality constraints +-------------------------------- + +-- | Equality constraints attached to an ECTA edge. +data EqConstraints + = EqConstraints + { getEclasses :: [PathEClass] + -- ^ Must be sorted + } + | EqContradiction + deriving (Eq, Ord, Show) + +instance Hashable EqConstraints where + hashWithSalt salt (EqConstraints eclasses) = + salt `hashWithSalt` (0 :: Int) `hashWithSalt` eclasses + hashWithSalt salt EqContradiction = + salt `hashWithSalt` (1 :: Int) + +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 [] + +-- | Extract equality classes, failing on 'EqContradiction'. +unsafeGetEclasses :: EqConstraints -> [PathEClass] +unsafeGetEclasses EqContradiction = error "unsafeGetEclasses: Illegal argument 'EqContradiction'" +unsafeGetEclasses ecs = getEclasses ecs + +-- | Construct constraints without congruence closure or contradiction checks. +rawMkEqConstraints :: [[Path]] -> EqConstraints +rawMkEqConstraints = EqConstraints . map PathEClass + +-- | Check whether a constraint set is already contradictory. +constraintsAreContradictory :: EqConstraints -> Bool +constraintsAreContradictory = (== EqContradiction) + +--------- Construction + +-- | List-based reference implementation for 'hasSubsumingMember'. +hasSubsumingMemberListBased :: [Path] -> [Path] -> Bool +hasSubsumingMemberListBased ps1 ps2 = + any (\p1 -> any (isStrictSubpath p1) ps2) ps1 + +{- | Check whether a normalized path class forces a path equal to its subpath. + +After congruence closure, every subsumption cycle appears as an equality class +containing both a path and one of its strict prefixes. Such a class is +unsatisfiable for finite trees: it would require a subterm to be equal to a +proper descendant of itself. +-} +isContradicting :: [[Path]] -> Bool +isContradicting cs = any (\pec -> hasSubsumingMemberListBased pec pec) cs + +{- | Build normalized equality constraints. + +This performs equality-class completion, adds path congruences, and detects +contradictions caused by a path being forced equal to one of its strict +subpaths. The implementation is intentionally direct rather than clever because +constraint construction is not the main @microecta@ API boundary, and the +@equivalence@ package keeps this path fast enough for current workloads. +-} +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 inefficient + -- 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 [] = return [] + assertEquivs (x : xs) = mapM (equate x) xs + + complete :: (Ord a) => [[a]] -> [[a]] + complete initialClasses = runEquivM (: []) (++) $ do + mapM_ assertEquivs initialClasses + mapM desc =<< classes + +---------- Operations + +-- | Combine two constraint sets and normalize the result. +combineEqConstraints :: EqConstraints -> EqConstraints -> EqConstraints +combineEqConstraints EqContradiction _ = EqContradiction +combineEqConstraints _ EqContradiction = EqContradiction +combineEqConstraints EmptyConstraints EmptyConstraints = EmptyConstraints +combineEqConstraints ec1 ec2 = combineEqConstraintsMemo ec1 ec2 +{-# NOINLINE combineEqConstraints #-} + +combineEqConstraintsMemo :: EqConstraints -> EqConstraints -> EqConstraints +combineEqConstraintsMemo = memo2 (NameTag "combineEqConstraints") go + where + go ec1 ec2 = mkEqConstraints $ ecsGetPaths ec1 ++ ecsGetPaths ec2 +{-# NOINLINE combineEqConstraintsMemo #-} + +{- | Descend every path in a constraint set through one child index. + +Equality classes with fewer than two remaining paths are dropped immediately: +they no longer constrain anything after the descent. +-} +eqConstraintsDescend :: EqConstraints -> Int -> EqConstraints +eqConstraintsDescend EqContradiction _ = EqContradiction +eqConstraintsDescend EmptyConstraints _ = EmptyConstraints +eqConstraintsDescend ecs i = case mapMaybe (`pathEClassDescendNontrivial` i) (getEclasses ecs) of + [] -> EmptyConstraints + [eclass] -> EqConstraints [eclass] + eclasses -> EqConstraints $ sort eclasses + where + pathEClassDescendNontrivial (PathEClass' pt _) childIndex = + let pt' = pathTrieDescend pt childIndex + in if pathTrieHasAtLeastTwoPaths pt' + then Just (mkPathEClassFromPathTrie pt') + else Nothing + +{- | Conservative implication check between two constraint sets. + +This is intentionally cheaper than rebuilding the combined closure: every +class required by the second set must occur as a subsequence of some class in +the first set. That is sufficient for redundant-edge pruning, but it is not a +complete theorem prover for arbitrary constraint implication. +-} +constraintsImply :: EqConstraints -> EqConstraints -> Bool +constraintsImply EqContradiction _ = True +constraintsImply _ EqContradiction = False +constraintsImply ecs1 ecs2 = all (\cs -> any (isSubsequenceOf cs) (ecsGetPaths ecs1)) (ecsGetPaths ecs2) + +-- | Equality classes sorted for constraint propagation, if not contradictory. +subsumptionOrderedEclasses :: EqConstraints -> Maybe [PathEClass] +subsumptionOrderedEclasses ecs = case ecs of + EqContradiction -> Nothing + EqConstraints pecs -> Just $ sortBy completedSubsumptionOrdering pecs + +-- | Variant of 'subsumptionOrderedEclasses' that fails on contradiction. +unsafeSubsumptionOrderedEclasses :: EqConstraints -> [PathEClass] +unsafeSubsumptionOrderedEclasses (EqConstraints pecs) = sortBy completedSubsumptionOrdering pecs +unsafeSubsumptionOrderedEclasses EqContradiction = error $ "unsafeSubsumptionOrderedEclasses: unexpected EqContradiction" diff --git a/src/Data/ECTA/Internal/Term.hs b/src/Data/ECTA/Internal/Term.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Internal/Term.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE OverloadedStrings #-} + +{- | Symbols and concrete terms accepted by ECTAs. + +Terms are ordinary first-order trees. They are the concrete values produced by +the enumeration API in "Data.ECTA". +-} +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 Text.Read (Read (..)) + +import Data.Interned.Text (InternedText, internedTextId) + +import Data.ECTA.Paths +import Data.Text.Extended.Pretty + +--------------------------------------------------------------- +-------------------------- Symbols ---------------------------- +--------------------------------------------------------------- + +-- | Interned term or edge symbol. +data Symbol = Symbol' {-# UNPACK #-} !InternedText + deriving (Eq, Ord) + +-- | Build or match a symbol from text. +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 ---------------------------- +--------------------------------------------------------------- + +-- | Concrete first-order term. +data Term = Term !Symbol ![Term] + deriving (Eq, Ord, Read, Show) + +instance Hashable Term where + hashWithSalt salt (Term symbol children) = + salt `hashWithSalt` symbol `hashWithSalt` children + +instance Pretty Term where + pretty (Term s []) = pretty s + pretty (Term s ts) = pretty s <> "(" <> (Text.intercalate ", " $ map pretty ts) <> ")" + +--------------------- +------ Term ops +--------------------- + +atMay :: Int -> [a] -> Maybe a +atMay i xs + | i < 0 = Nothing + | otherwise = case drop i xs of + x : _ -> Just x + [] -> Nothing + +adjustAt :: Int -> (a -> a) -> [a] -> [a] +adjustAt i f xs + | i < 0 = xs + | otherwise = case splitAt i xs of + (prefix, x : suffix) -> prefix ++ f x : suffix + _ -> xs + +instance Pathable Term Term where + type Emptyable Term = Maybe Term + + getPath EmptyPath t = Just t + getPath (ConsPath p ps) (Term _ ts) = case atMay p ts 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 (adjustAt p (modifyAtPath f ps) ts) diff --git a/src/Data/ECTA/Paths.hs b/src/Data/ECTA/Paths.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Paths.hs @@ -0,0 +1,45 @@ +{- | Paths and equality constraints used by ECTA edges. + +Paths are lists of child indexes. For example, @path [1,0]@ means "the first +child of the second child" of an edge. Equality constraints group paths that +must denote equal subterms whenever an edge is used. + +Most users only need 'path', 'mkEqConstraints', 'EmptyConstraints', and the +query helpers. The trie and e-class types are exposed because some downstream +code inspects constraint structure directly, but they are still considered part +of the low-level ECTA machinery. +-} +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 diff --git a/src/Data/ECTA/Term.hs b/src/Data/ECTA/Term.hs new file mode 100644 --- /dev/null +++ b/src/Data/ECTA/Term.hs @@ -0,0 +1,7 @@ +-- | Public re-export of concrete terms and symbols. +module Data.ECTA.Term ( + Symbol (Symbol), + Term (..), +) where + +import Data.ECTA.Internal.Term diff --git a/src/Data/Interned/Extended/HashTableBased.hs b/src/Data/Interned/Extended/HashTableBased.hs new file mode 100644 --- /dev/null +++ b/src/Data/Interned/Extended/HashTableBased.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Tiny hash-consing abstraction backed by mutable cuckoo hash tables. +module Data.Interned.Extended.HashTableBased ( + Id, + Cache (..), + freshCache, + Interned (..), + intern, +) where + +import qualified Data.HashTable.IO as HT +import Data.Hashable +import Data.IORef +import GHC.IO (unsafeDupablePerformIO) + +-- | Dense identity assigned to each interned value. +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) + -- ^ Next id to allocate. + , content :: !(HT.CuckooHashTable (Description t) t) + -- ^ Map from structural descriptions to canonical interned values. + } + +-- | Allocate an empty interning cache. +freshCache :: IO (Cache t) +freshCache = + Cache + <$> newIORef 0 + <*> HT.new + +-- | Values that can be hash-consed through a global cache. +class + ( Eq (Description t) + , Hashable (Description t) + ) => + Interned t + where + -- | Hashable structural representation used as the cache key. + data Description t + + -- | Non-canonical input used to build an interned value. + type Uninterned t + + -- | Compute the cache key for an uninterned value. + describe :: Uninterned t -> Description t + + -- | Attach a freshly allocated identity to an uninterned value. + identify :: Id -> Uninterned t -> t + + -- | Process-global cache for this interned type. + cache :: Cache t + +-- | Return the canonical interned representative for an uninterned value. +intern :: (Interned t) => Uninterned t -> t +intern !bt = unsafeDupablePerformIO $ do + let c = cache + let refI = fresh c + let ht = content c + v <- HT.lookup ht dt + case v of + Nothing -> do + 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 diff --git a/src/Data/Memoization.hs b/src/Data/Memoization.hs new file mode 100644 --- /dev/null +++ b/src/Data/Memoization.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE OverloadedStrings #-} + +{- | Quick-and-dirty, thread-unsafe, hash-based memoization. + +The ECTA core relies on stable global memo tables for interning and recursive +graph operations. This module intentionally keeps that machinery tiny: each +call to 'memo' allocates one process-global hash table through +'unsafePerformIO'. +-} +module Data.Memoization ( + MemoCacheTag (..), + memo, + memo2, +) where + +import qualified Data.HashTable.IO as HT +import Data.Hashable (Hashable (..)) +import Data.Text (Text) +import System.IO.Unsafe (unsafePerformIO) + +-- | Human-readable name for a memo table. +data MemoCacheTag + = -- | Name a table for debugging and nested-table derivation. + NameTag Text + deriving (Eq, Ord, Show) + +instance Hashable MemoCacheTag where + hashWithSalt salt (NameTag name) = salt `hashWithSalt` name + +mkInnerTag :: MemoCacheTag -> MemoCacheTag +mkInnerTag (NameTag t) = NameTag (t <> "-inner") + +memoIO :: forall a b. (Eq a, Hashable a) => MemoCacheTag -> (a -> b) -> IO (a -> IO b) +memoIO _ f = do + ht :: HT.CuckooHashTable a b <- HT.new + let f' x = do + v <- HT.lookup ht x + case v of + Nothing -> do + let r = f x + HT.insert ht x r + return r + Just r -> return r + return f' + +-- | Memoize a pure unary function in a process-global mutable hash table. +memo :: (Eq a, Hashable a) => MemoCacheTag -> (a -> b) -> (a -> b) +memo tag f = + let f' = unsafePerformIO (memoIO tag f) + in \x -> unsafePerformIO (f' x) + +-- | Memoize a pure binary function as nested unary memo tables. +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) diff --git a/src/Data/Persistent/UnionFind.hs b/src/Data/Persistent/UnionFind.hs new file mode 100644 --- /dev/null +++ b/src/Data/Persistent/UnionFind.hs @@ -0,0 +1,115 @@ +{- | Lightweight union-find implementation suitable for nondeterministic search. + +Mutable union-find, as in @Data.Equivalence.Monad@, should be faster overall, +but enumeration branches in the list monad need a structure that can be copied +and backtracked cheaply. This module stores parent pointers in an 'IntMap' and +returns updated structures from 'find' and 'union'. +-} +module Data.Persistent.UnionFind ( + UVarGen, + initUVarGen, + nextUVar, + UVar, + uvarToInt, + intToUVar, + UnionFind, + empty, + withInitialValues, + union, + find, +) where + +import Control.Monad.State.Strict (State, execState, get, modify', put, runState) +import Data.Coerce (coerce) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap + +---------------------------------------------------------- + +--------------------------- +-------- UVarGen +--------------------------- + +-- | Fresh supply for enumeration variables. +newtype UVarGen = UVarGen Int + deriving (Eq, Ord, Show) + +-- | Initial variable supply. +initUVarGen :: UVarGen +initUVarGen = UVarGen 0 + +-- | Allocate one fresh variable and advance the supply. +nextUVar :: UVarGen -> (UVarGen, UVar) +nextUVar (UVarGen n) = (UVarGen (n + 1), UVar n) + +--------------------------- +-------- UVar +--------------------------- + +-- | Union-find variable identifier. +newtype UVar = UVar Int + deriving (Eq, Ord, Show) + +-- | Convert a variable to its dense integer id. +uvarToInt :: UVar -> Int +uvarToInt (UVar i) = i + +-- | Reconstruct a variable from its dense integer id. +intToUVar :: Int -> UVar +intToUVar = UVar + +--------------------------- +-------- Union-find data structure +--------------------------- + +{- | Persistent union-find forest. + +Roots store negative set sizes. Non-roots store their parent id. +-} +newtype UnionFind = UnionFind {getUnionFindMap :: IntMap Int} + deriving (Eq, Ord, Show) + +-- | Empty forest. Variables are inserted lazily by 'find'. +empty :: UnionFind +empty = UnionFind IntMap.empty + +-- | Forest containing each supplied variable as a singleton set. +withInitialValues :: [UVar] -> UnionFind +withInitialValues uvs = UnionFind $ IntMap.fromList $ map (,-1) $ coerce uvs + +--------------------------- +-------- Union-find operations +--------------------------- + +-- | Merge the two variable classes, preferring the larger class as root. +union :: UVar -> UVar -> UnionFind -> UnionFind +union uv1 uv2 uf = 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 a variable's representative and return the path-compressed forest. +find :: UVar -> UnionFind -> (UVar, UnionFind) +find uv uf = coerce runState (fst <$> findWithNegSize uv) uf diff --git a/src/Data/Text/Extended/Pretty.hs b/src/Data/Text/Extended/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Data/Text/Extended/Pretty.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | Minimal pretty-printing class that produces strict 'Text'. +module Data.Text.Extended.Pretty ( + Pretty (..), +) where + +import Data.Text (Text) +import qualified Data.Text as Text + +---------------------------------------------------------------------- + +-- | Convert a value to human-readable strict 'Text'. +class Pretty a where + -- | Render a value. + pretty :: a -> Text + +instance {-# OVERLAPPABLE #-} (Show a) => Pretty a where + pretty = Text.pack . show diff --git a/src/Utility/Fixpoint.hs b/src/Utility/Fixpoint.hs new file mode 100644 --- /dev/null +++ b/src/Utility/Fixpoint.hs @@ -0,0 +1,28 @@ +-- | Small fixpoint helpers used by reduction and constraint saturation. +module Utility.Fixpoint ( + fixUnbounded, + fixMaybe, +) where + +-------------------------------------------------------------- + +-- | Iterate until stable with no iteration bound. +fixUnbounded :: (Eq a) => (a -> a) -> a -> a +fixUnbounded f x = + let x' = f x + in if x' == x + then + x + else + fixUnbounded f x' + +-- | Iterate a partial step function until stable or failed. +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' diff --git a/src/Utility/HashJoin.hs b/src/Utility/HashJoin.hs new file mode 100644 --- /dev/null +++ b/src/Utility/HashJoin.hs @@ -0,0 +1,70 @@ +-- | Hash-table based grouping and joining helpers for interned structures. +module Utility.HashJoin ( + nubByIdSinglePass, + clusterByHash, + hashJoin, +) where + +import Control.Monad.ST (ST, runST) +import Data.Foldable (foldrM) + +import qualified Data.HashTable.ST.Cuckoo as HT + +------------------------------------- +--- Hash join / clustering / nub +-------------------------------- + +{- | Remove duplicates by a stable identity hash. + +Precondition: if @h x == h y@, then @x == y@. This is intended for interned +values where the integer id is already a complete identity. The output order is +reversed relative to first occurrence because callers only need set-like +behavior. +-} +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), ()) + +-- | Group values by hash. +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 + +-- | Join two lists by equal hash and combine matching pairs. +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 $ foldr (\v2 acc -> j x v2 : acc) res vs2 + ) + [] + l1 diff --git a/test/Data/Persistent/UnionFindSpec.hs b/test/Data/Persistent/UnionFindSpec.hs new file mode 100644 --- /dev/null +++ b/test/Data/Persistent/UnionFindSpec.hs @@ -0,0 +1,78 @@ +module Data.Persistent.UnionFindSpec (spec) where + +import Control.Monad.State (MonadState (..), State, evalState, modify) +import Control.Monad.Writer (MonadWriter (..), WriterT (..)) +import Data.Equivalence.Monad (EquivM, equate, equivalent, runEquivM) + +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) diff --git a/test/ECTASpec.hs b/test/ECTASpec.hs new file mode 100644 --- /dev/null +++ b/test/ECTASpec.hs @@ -0,0 +1,372 @@ +{-# LANGUAGE OverloadedStrings #-} + +module ECTASpec (spec) where + +import Control.Exception (evaluate) +import qualified Data.HashSet as HashSet +import Data.IORef (modifyIORef, newIORef, readIORef) +import Data.Set (Set) +import qualified Data.Set as Set +import qualified Data.Text as Text + +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 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 = ex3 + +_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" $ + getAllTerms ex1 `shouldSatisfy` ((== 2) . length) + + it "reduces paths constrained by equality constraints" $ + reducePartially ex2 `shouldBe` reducePartially ex1 + + it "nodeRepresents requires exact term arity" $ do + let n = Node [Edge "f" [constTerms ["a"], constTerms ["b"]]] + nodeRepresents n (Term "f" [Term "a" [], Term "b" []]) `shouldBe` True + nodeRepresents n (Term "f" [Term "a" []]) `shouldBe` False + nodeRepresents n (Term "f" [Term "a" [], Term "b" [], Term "c" []]) `shouldBe` False + + it "nodeRepresentsTemplate allows wildcard prefix templates" $ do + let n = Node [Edge "f" [constTerms ["a"], constTerms ["b"]]] + nodeRepresentsTemplate n (Term "" [Term "" [], Term "" []]) `shouldBe` True + nodeRepresentsTemplate n (Term "" []) `shouldBe` True + + describe "intersection" $ do + it "intersection commutes with getAllTerms" $ + property $ + mapSize (min 3) $ \n1 n2 -> + HashSet.fromList (getAllTerms $ intersect n1 n2) + `shouldBe` HashSet.intersection + (HashSet.fromList $ getAllTerms n1) + (HashSet.fromList $ getAllTerms 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] + + it "intersect is idempotent" $ + property $ + \n1 -> intersect n1 n1 == n1 + + 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" $ + getAllTerms (intersect intTest5 intTest6) `shouldBe` [Term "g" [Term "a" [], Term "b" []]] + + -- Intersection examples with Mu nodes + + it "intersect (one-step loop) with (its own unfolding: step, one-step)" $ + intersect intTest7 intTest8 `shouldBe` 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` intTest8 + + it "intersect with nested Mus" $ do + intersect intTest11 intTest12 `shouldBe` Node [Edge "f" [createMu $ \r -> Node [Edge "f" [r]]]] + + describe "reduction" $ do + it "reduction preserves getAllTerms" $ + property $ + mapSize (min 3) $ + \n -> HashSet.fromList (getAllTerms n) `shouldBe` HashSet.fromList (getAllTerms $ 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 $ f infiniteFNode, f $ 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 "reduction preserves enumeration on nodes without mu" $ + property $ + mapSize (min 3) $ + \n -> HashSet.fromList (getAllTerms 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']] diff --git a/test/PathsSpec.hs b/test/PathsSpec.hs new file mode 100644 --- /dev/null +++ b/test/PathsSpec.hs @@ -0,0 +1,141 @@ +module PathsSpec (spec) where + +import Data.List (nub, sort, subsequences, (\\)) + +import Test.Hspec +import Test.QuickCheck + +import Data.ECTA.Internal.Paths + +----------------------------------------------------------------- + +----------------------------------- +------ PathTrie testing utils +----------------------------------- + +----------------------------------- +------ 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 children) = + map snd children + ++ [ PathTrie children' + | children' <- subsequences children \\ [children] + , length children' >= 2 + ] + +----------------------------------- +------ 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 "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 "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) + -} diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,16 @@ +module Main (main) where + +import Test.Hspec (hspec) + +import qualified Data.Persistent.UnionFindSpec +import qualified ECTASpec +import qualified PathsSpec +import qualified Utility.HashJoinSpec + +main :: IO () +main = + hspec $ do + Data.Persistent.UnionFindSpec.spec + ECTASpec.spec + PathsSpec.spec + Utility.HashJoinSpec.spec diff --git a/test/Test/Generators/ECTA.hs b/test/Test/Generators/ECTA.hs new file mode 100644 --- /dev/null +++ b/test/Test/Generators/ECTA.hs @@ -0,0 +1,81 @@ +{-# 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) diff --git a/test/Utility/HashJoinSpec.hs b/test/Utility/HashJoinSpec.hs new file mode 100644 --- /dev/null +++ b/test/Utility/HashJoinSpec.hs @@ -0,0 +1,17 @@ +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 "nubByIdSinglePass is same as nub" $ + property $ + \(xs :: [Int]) -> sort (nub xs) == sort (nubByIdSinglePass id xs)