microecta (empty) → 0.1.0.0
raw patch · 30 files changed
+4732/−0 lines, 30 filesdep +QuickCheckdep +basedep +containerssetup-changed
Dependencies added: QuickCheck, base, containers, equivalence, hashable, hashtables, hspec, intern, microecta, mtl, text, transformers, unordered-containers
Files
- CHANGELOG.md +12/−0
- LICENSE +31/−0
- README.md +186/−0
- Setup.hs +3/−0
- benchmarks/Benchmarks.hs +231/−0
- microecta.cabal +144/−0
- src/Application/TermSearch/Dataset.hs +23/−0
- src/Application/TermSearch/TermSearch.hs +25/−0
- src/Application/TermSearch/Type.hs +32/−0
- src/Application/TermSearch/Utils.hs +60/−0
- src/Data/ECTA.hs +70/−0
- src/Data/ECTA/Internal/ECTA/Enumeration.hs +726/−0
- src/Data/ECTA/Internal/ECTA/Operations.hs +708/−0
- src/Data/ECTA/Internal/ECTA/Type.hs +691/−0
- src/Data/ECTA/Internal/Paths.hs +570/−0
- src/Data/ECTA/Internal/Term.hs +102/−0
- src/Data/ECTA/Paths.hs +45/−0
- src/Data/ECTA/Term.hs +7/−0
- src/Data/Interned/Extended/HashTableBased.hs +75/−0
- src/Data/Memoization.hs +54/−0
- src/Data/Persistent/UnionFind.hs +115/−0
- src/Data/Text/Extended/Pretty.hs +19/−0
- src/Utility/Fixpoint.hs +28/−0
- src/Utility/HashJoin.hs +70/−0
- test/Data/Persistent/UnionFindSpec.hs +78/−0
- test/ECTASpec.hs +372/−0
- test/PathsSpec.hs +141/−0
- test/Spec.hs +16/−0
- test/Test/Generators/ECTA.hs +81/−0
- test/Utility/HashJoinSpec.hs +17/−0
+ CHANGELOG.md view
@@ -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.
+ LICENSE view
@@ -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.
+ README.md view
@@ -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 `<v>` 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.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain
+ benchmarks/Benchmarks.hs view
@@ -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]+ ]
+ microecta.cabal view
@@ -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,
+ src/Application/TermSearch/Dataset.hs view
@@ -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)
+ src/Application/TermSearch/TermSearch.hs view
@@ -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)
+ src/Application/TermSearch/Type.hs view
@@ -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
+ src/Application/TermSearch/Utils.hs view
@@ -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) []]
+ src/Data/ECTA.hs view
@@ -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
+ src/Data/ECTA/Internal/ECTA/Enumeration.hs view
@@ -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 "<v>") _) = 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 @"<v>"@ 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 @<vN>@, 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 $ "<v" <> 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, ()))
+ src/Data/ECTA/Internal/ECTA/Operations.hs view
@@ -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 @"<v>"@ 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 @"<v>"@, 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 == "<v>" && 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
+ src/Data/ECTA/Internal/ECTA/Type.hs view
@@ -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
+ src/Data/ECTA/Internal/Paths.hs view
@@ -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"
+ src/Data/ECTA/Internal/Term.hs view
@@ -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)
+ src/Data/ECTA/Paths.hs view
@@ -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
+ src/Data/ECTA/Term.hs view
@@ -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
+ src/Data/Interned/Extended/HashTableBased.hs view
@@ -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
+ src/Data/Memoization.hs view
@@ -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)
+ src/Data/Persistent/UnionFind.hs view
@@ -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
+ src/Data/Text/Extended/Pretty.hs view
@@ -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
+ src/Utility/Fixpoint.hs view
@@ -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'
+ src/Utility/HashJoin.hs view
@@ -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
+ test/Data/Persistent/UnionFindSpec.hs view
@@ -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)
+ test/ECTASpec.hs view
@@ -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 "<v>" [Term "<v>" [], Term "<v>" []]) `shouldBe` True+ nodeRepresentsTemplate n (Term "<v>" []) `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']]
+ test/PathsSpec.hs view
@@ -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)+ -}
+ test/Spec.hs view
@@ -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
+ test/Test/Generators/ECTA.hs view
@@ -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)
+ test/Utility/HashJoinSpec.hs view
@@ -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)